pub const PIGEONHOLE_EXAMPLES: &[(&str, &str)];Expand description
Pigeonhole examples: pigeons: N → PHP(N), N pigeons into N-1 holes. Opened in Hardware
mode; load_hardware_spec routes a pigeons: spec to the live solver, which animates the
doomed pigeon and emits a certified symmetry-breaking refutation (Hall witness + Heule PR proof,
no Z3) — the family every resolution-based solver (Kissat, CaDiCaL, Z3) needs 2^Ω(n) steps on.