Function nullstellensatz_refutes 

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

Does a degree-d Nullstellensatz refutation exist over GF(2)? Sound: such a certificate exists only when the formula is unsatisfiable. Complete at d = num_vars (full degree decides any instance). Bounded to num_vars ≤ 20 (the explicit monomial basis).