Function refute_clausal 

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

Refute e by CUTTING PLANES when it is a cardinality/pigeonhole-shaped CNF. The pairwise encoding loses the cardinality structure, so we RECOVER it: the binary exclusions ¬(a∧b) form conflict cliques, each a genuine “at most one” group; summing those at_most(group,1) cardinality constraints with the positive “at least one” clauses cancels every literal against its negation and collapses a pigeonhole-shaped system to 0 ≥ 1 — POLYNOMIAL, where resolution/CDCL explode.

Returns true ONLY on a genuine cutting-plane contradiction (a sound UNSAT proof); false (the caller falls through) for any formula that does not collapse. Never a false true: each step is a sound cutting-plane inference, and the at-most-one constraints are implied by the verified exclusion cliques.