fact: Definition checker (d:dimacs) (c:certif) := let (nclauses, t, confl_id) := c in resolution_checker C.is_false (add_roots (S.make nclauses) d) t confl_id.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker