Function decide_pigeonhole_unsat 

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

Decide whether e is a clean pigeonhole structure that is UNSAT. Returns true ONLY when the formula decomposes faithfully into at-least-one rows + fully-encoded (clique) at-most-one columns AND the bipartite matching is infeasible with a RE-VERIFIED Hall witness. false otherwise — for a non-pigeonhole formula, or a feasible one (the caller falls back to CDCL). Never a false true.