Function polynomial_calculus_refutes 

pub fn polynomial_calculus_refutes(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    degree: usize,
) -> bool

Does a degree-d Polynomial Calculus refutation exist over GF(2)? PC is the dynamic strengthening of Nullstellensatz: start from the clause polynomials and close under (i) GF(2) linear combination and (ii) multiplication by a single variable, keeping every derived polynomial multilinear of degree ≤ d; the system is refuted iff the constant 1 is derived. Because an intermediate linear combination can cancel high-degree terms before the next multiply, degree-d PC certifies a superset of what degree-d Nullstellensatz can (which must hit each axiom with a single monomial in one shot). Sound — 1 is derivable only from an unsatisfiable system — and PC ⊇ NS, so it never refutes fewer. Complete at d = num_vars. Bounded to num_vars ≤ 20.