Function check_ordering_cert 

pub fn check_ordering_cert(cert: &OrderingCert, clauses: &[Vec<Lit>]) -> bool

Re-check an OrderingCert against the raw clauses from scratch, trusting nothing about how it was produced: verify that for its element/edge identification EVERY totality, antisymmetry, transitivity, and no-maximum clause is present. true iff the certificate genuinely witnesses a complete GT(n) core (which is unsatisfiable), so the formula is UNSAT.