Function is_refutation 

pub fn is_refutation(
    clauses: &[(Lit, Lit)],
    num_vars: usize,
    var: usize,
) -> bool

Re-check an Unsat witness: in the implication graph, x reaches ¬x and ¬x reaches x (mutual implication ⇒ no value of x is consistent). A solver-free certificate.