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, and Itsykson [EGI, STOC 2024] proved an exponential lower bound for regular Res($\oplus$) that is strictly stronger than tree-like Res($\oplus$).
Bhattacharya, Chattopadhyay, and Dvorak [BCD, CCC 2024] have recently shown that regular Res($\oplus$) can not polynomially simulate resolution. The proof is based on add-hock lifting; the authors of [BCD, CCC 2024] posed an open research direction to develop a universal lifting technique for regular resolution over parities.

We develop a lifting technique to regular Res($\oplus$) refutation complexity that can be applied to various formulas. Our approach does not explicitly transform proofs but lifts strategies in games characterizing corresponding proof complexity measures. To lift strategies of resolution games to strategies of Res($\oplus$) games, we use the notion of closure introduced by Efremenko, Garlik, and Itsykson [EGI, STOC 2024]; it turns out that this notion can be perfectly combined with a stifling gadget lifting. At first, we demonstrate our approach by giving an elementary and beautiful lifting theorem showing that if a CNF formula $\phi$ requires resolution width $w$, then $\phi$ lifted by 1-stifling gadget (e.g., $Maj_3$) requires Res($\oplus$)-rank at least $w$.

Then we prove the lifting theorems for formulas that have good enough Delayer's strategies in the advanced Prover-Delayer games; such formula lifted by a 2-stifling gadget (e.g., $Maj_5$) requires regular Res($\oplus$) refutations of exponential size. Using this result, we show that lifted Tseitin formulas are hard for regular Res($\oplus$) (thus resolving the open question raised by [BCD, CCC 2024]). We also show that for every formula with a large resolution depth, we can apply mixing and constant-size lifting such that the final formula will require exponential size regular Res($\oplus$) refutations. Finally, we give an alternative and improved separation between resolution and regular Res($\oplus$): we construct an $n$-variable formula that has resolution refutation of size poly(n) but requires regular Res($\oplus$) refutation of size $2^{\Omega(\sqrt{n})}$.