Lower Bounds for Near-Quadratic-Depth Resolution over Parities

Resolution over parities (Res(⊕)) is a proof system introduced by Itsykson and Sokolov [MFCS ’14] as a stepping stone towards proving AC0[2]-Frege lower bounds. A recent line of work has established lower bounds against depth-restricted Res(⊕) refutations. Prior to this work, the state of the art was exponential lower bounds against depth O(N logN) Res(⊕) proved by Efremenko and Itsykson [CCC ’25], where N is the number of variables in the CNF. In this work we prove exponential lower bounds against depth O(N2−є) Res(⊕) refutations. The lifted Tseitin formula we consider has O(N) clauses of width 6, which lets the allowed depth be almost quadratic not only in the number of variables, but also in the CNF size. We also prove depth-restricted lower bounds for variants of the bit pigeonhole principle (BPHP), including an exponential lower bound for depth O(n2−є) Res(⊕) refutations of BPHP with n+1 pigeons and n holes.