The proof system, resolution over parities (Res($\oplus$)), merges traditional resolution with linear algebra over GF(2). Proving a superpolynomial lower bound on proof size within this system remains a challenging open question. For many years, such lower bounds were known only in tree-like cases. However, recent work by Efremenko, Garlik, and Itsykson [EGI, STOC 2024] established 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 proved that regular Res($\oplus$) cannot polynomially simulate resolution. Their proof employs an ad-hoc lifting technique, and the authors of [BCD, CCC 2024] have proposed an open research direction to develop a universal lifting technique for regular resolution over parities.

We introduce a lifting technique for the refutation complexity of regular Res($\oplus$) that is applicable to a variety of formulas. Rather than explicitly transforming proofs, our approach leverages strategies from games that define the associated first proof complexity measure, enabling us to establish lower bounds for the second proof complexity measure.

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. Furthermore, we present a method for transforming any formula with large resolution depth into a formula requiring exponential-size regular Res($\oplus$) refutations through a combination of mixing and constant-size lifting. We also provide an alternative and improved separation between resolution and regular Res($\oplus$): we construct an $n$-variable formula with a polynomial-size resolution refutation of depth $O(\sqrt{n})$ which requires regular Res($\oplus$) refutation of size $2^{\Omega(\sqrt{n})}$. In particular, it implies that depth $n$ Res($\oplus$) (where $n$ stands for the number of variables) is more powerful than regular Res($\oplus$).

Using the developed technique, we establish an exponential lower bound on the size of depth $cn\log \log n$ Res($\oplus$) refutations, with $c$ being a constant. The hard instances in this context are Tseitin formulas lifted with the $Maj_5$ gadget. Even depth $n$ Res($\oplus$) encompasses all conceivable definitions of regular Res($\oplus$). Consequently, this result provides an exponential lower bound for top-regular Res($\oplus$), thereby addressing the open question raised by Gryaznov, Pudlak, and Talebanfard [GPT, CCC 2022].

The new result obtained using the technique developed in the paper was added: an exponential lower bound for depth $cn \log\log n$ Res($\oplus$) refutations. Consequently, the structure of the paper and the title were revised.

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})}$.