pub fn disjoint_double_contradiction() -> (usize, Vec<Vec<Lit>>)Expand description
Two var-disjoint contradictions: vars {0,1} and {2,3}, each an unsatisfiable 2-variable block.
Its four RUP lemmas (1), (¬1), (3), (¬3) are derived from the originals alone — pairwise
independent proof steps, the cleanest place to see the commutation 2-cells on a real refutation.