Function ns_refutes_polys 

pub fn ns_refutes_polys(num_vars: usize, gens: &[Poly], degree: usize) -> bool

Does a degree-d Nullstellensatz refutation exist over GF(2) for an arbitrary polynomial generator system — is 1 in the GF(2)-span of { m·g : deg(m·g) ≤ d }? The clause engine’s question asked of any generators, not just clause polynomials: the substrate for the linear encoding (exactly_one_linear_generators) and the symmetric-family machinery. The multiplier rule is exact — a product is admitted by its degree after multilinear collapse. (For clause polynomials this span equals the clause engine’s: a multiplier overlapping a positive literal kills the product, one overlapping a negative literal absorbs into a smaller multiplier — pinned by the differential test.) Degree-bounded enumeration, so it scales to num_vars ≤ 63.