Function witness_parity 

pub fn witness_parity(n: usize) -> (usize, Vec<Vec<Lit>>)

A parametric UNSAT witness realizing the parity rung at any n ≥ 3: the odd XOR triangle x₀⊕x₁ = 1, x₁⊕x₂ = 1, x₂⊕x₀ = 1 (their sum is 1 ≠ 0), encoded in CNF. No unit propagates and no counting cut sees it — only a GF(2) parity refutation closes it, so the weakest rung is ProofRung::Parity.