For every$n > 0$, we show the existence of a CNF tautology over$O(n^{2})$variables of width$O(\log {\it n})$such that it has a Polynomial Calculus Resolution refutation over$\{0,1\}$variables of size$O(n^{3} \text{polylog} (n))$but any Polynomial Calculus refutation over$\{+1, -1\}$variables requires size$2^{\Omega(n)}$. This shows that Polynomial Calculus sizes over the {0, 1} and$\{+1,\ -1\}$bases are incomparable (since Tseitin tautologies show a separation in the other direction) and answers an open problem posed by Sokolov [1] and Razborov [2].

A major open problem in proof complexity is to prove superpolynomial lower bounds for AC0[p]-Frege proofs. This system is the analog of AC0 [p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([28, 30]), there are no significant lower bounds for AC0 [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC0[p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC0 [p]-Frege lower bounds.