The propositional proof system resolution over parities (Res($\oplus$)) combines resolution and the linear algebra over GF(2). It is a challenging open question to prove a superpolynomial lower bound on the proof size in this system. For many years, superpolynomial lower bounds were known only in tree-like cases. Recently, Efremenko, Garlik, ... more >>>

Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res($\oplus$)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with ... more >>>