The proof checker DRAT-trim can be used to check whether a propositional
formula in the DIMACS format is unsatisfiable. Given a propositional formula
and a clausal proof, DRAT-trim validates that the proof is a certificate of
unsatisfiability of the formula. Clausal proofs should be in the DRAT format
which is used to validate the results of the SAT competitions.