Function refute_via_parity 

pub fn refute_via_parity(e: &ProofExpr) -> bool

Recognize the XOR (parity) gadgets inside a CNF ProofExpr and refute via Gaussian elimination — the GF(2) shadow, as a fast-path for crate::sat::prove_unsat. A parity constraint x_{a} ⊕ … ⊕ x_{z} = r over k variables is encoded in CNF as exactly the 2^{k-1} clauses that forbid the wrong-parity assignments; we group clauses by their variable set, and whenever a group is precisely such a full wrong-parity bundle we recover its XorEquation.

Soundness (never a false true): a fully-present gadget’s clauses imply its XOR equation (they forbid exactly the assignments the equation forbids), so the recovered equations are all logical consequences of e. If that recognized linear subsystem is inconsistent over GF(2), then e is unsatisfiable. Partial or malformed gadgets are simply not recognized — we fall through, never guess. The parity refutation is itself re-checkable via is_refutation.