The proof system resolution over parities (Res(\oplus)) operates with disjunctions of linear equations (linear clauses) over \mathbb{F}_2; it extends the resolution proof system by incorporating linear algebra over \mathbb{F}_2. Over the years, several exponential lower bounds on the size of tree-like Res(\oplus) refutations have been established. However, proving a superpolynomial ... more >>>