For every $n >0$, we show the existence of a CNF tautology over $O(n^2)$ variables of width $O(\log n)$ such that it has a Polynomial Calculus Resolution refutation over $\{0,1\}$ variables of size $O(n^3polylog(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 [Sok20] and Razborov.

翻译：对于每个$n>0$，我们证明存在一个宽度为$O(\log n)$、变量数为$O(n^2)$的CNF重言式，该重言式在$\{0,1\}$变量上具有大小为$O(n^3polylog(n))$的多项式演算消解反驳，但在$\{+1,-1\}$变量上的任何多项式演算反驳所需规模为$2^{\Omega(n)}$。这表明多项式演算在$\{0,1\}$基与$\{+1,-1\}$基下的规模不可比（因为Tseitin重言式已在另一方向上给出分离结果），从而解答了Sokolov [Sok20]与Razborov提出的公开问题。