Function php_refutation 

pub fn php_refutation(n: usize) -> PbConstraint

Refute the pigeonhole principle PHP(n, n−1) with the classic Cook–Coullard–Turán cutting- plane proof: sum all n “each pigeon in ≥1 hole” constraints with all n−1 “each hole holds ≤1 pigeon” constraints. Every x meets its ¬x and cancels, collapsing the whole system to the trivially-false 0 ≥ 1 in just 2n−1 additions — linear size, where resolution needs exponentially many steps. Returns the final derived constraint (a contradiction).