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 提出的一个公开问题。