pub fn witness_counting(pigeons: usize) -> (usize, Vec<Vec<Lit>>)Expand description
A parametric UNSAT witness realizing the counting rung: the pigeonhole principle with pigeons
pigeons and pigeons − 1 holes (crate::families::php). Resolution-exponential, invisible to GF(2)
parity, closed only by a counting / Hall cut — so the weakest rung is ProofRung::Counting.