pub fn ordering_principle(n: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
The linear ordering principle GT(n): no finite strict total order lacks a maximal element — yet
this formula asserts exactly that, so it is UNSAT. x[i][j] (index i*n + j) reads “i < j”.
Antisymmetry + totality + transitivity force a linear order, and the “every element has a greater
one” clauses then contradict finiteness. A canonical resolution-hard family — it stresses the
CDCL core / cutting-plane reasoning rather than a matching or parity specialist.