Function nullstellensatz_refutes_symmetric 

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

Symmetry-reduced Nullstellensatz — the algebraic refutation collapsed by the formula’s symmetry. Full degree-d NS asks whether 1 lies in the GF(2)-span of the generators m·p_C, a Gaussian over up to C(n,≤d) monomial columns. When the formula has a symmetry group G, summing each generator’s G-orbit gives an invariant generator, and every invariant polynomial is constant on the monomial orbits (monomial_orbits) — so the same span check runs over just #orbits columns and #generator-orbits rows. For a symmetric family that is the difference between 2^Θ(n) and O(1).

Sound: each row is an honest GF(2)-sum of NS generators, so 1 in the reduced span is 1 in the full span — a real refutation, hence UNSAT. Incomplete (a refutation need not be G-invariant), and fail-closed: if a passed generator is not a genuine symmetry (an orbit step leaves the generator set) it declines rather than reduce unsoundly. generators must be automorphisms of clauses.