Function heule_php_refutation 

pub fn heule_php_refutation(n: usize) -> CertifiedRefutation

The Heule–Kiesl–Biere short PR refutation of PHP(n): a polynomial-size, fully certified proof — where the lex-leader provably cannot scale on UNSAT instances.

It frees holes one at a time. To free the last active hole h of PHP(m), it forces every non-last pigeon i out of it with the clause ¬x(i, h), certified by the substitution witness “swap pigeon i with the last pigeon” — a PHP automorphism whose SR check conflicts at once on the hole-h conflict clause (so it is sound at any scale). That confines the remaining pigeons to one fewer hole, reducing PHP(m) → PHP(m-1); after O(n²) such units RUP closes. The whole refutation is checked against the original PHP(n) alone.