pub fn witness_unit_propagation(n: usize) -> (usize, Vec<Vec<Lit>>)Expand description
A parametric UNSAT witness realizing the unit-propagation rung at any n ≥ 1: a variable and its
negation. Carving alone closes it, so its weakest crushing rung is ProofRung::Trivial.