usage: drabt [ <option> ... ] <pre.cnf> [ <drat.proof> [ <post.cnf> ] ]

-h    print this usage information
      (also printed if <pre.cnf> is missing)

-f    complete forward checking (default)
-b    partial backward checking (not implemented yet)
-p    enable plain mode and ignore all 'd' lines
-S    run in forward SAT mode (do not necessarily check for refutation)

-v                   increase verbose level
                     (default 0, compiled in maximum 1)

-M | --more-details  print more details in error messages (line numbers)
                     (needs more memory, default in verbose mode)

-L | --less-details  print less details in error messages
                     (needs less memory, default in non-verbose mode)

-I | --ignore-warnings   ignore and do not even print warnings

-P | --pedantic      turns warnings into errors
                     (for instance abort if 'p' header is missing)

-s | --sloppy        ignore certain (ignorable) errors
                     (like 'd' clauses which do not exist anymore)

--force-non-binary   assume proof is in non-binary format

<pre.cnf>      antecedent or input CNF in DIMACS format
<drat.proof>   DRAT proof showing <post.cnf> is implied by <pre.cnf>
<post.cnf>     consequent or implied CNF in DIMACS format

If <post.cnf> is omitted then the checker assumes that <post.cnf> just
contains the empty clause, which means that <drat.proof> is supposed
to be a DRAT refutation for <pre.cnf>.  If the file name <drat.proof>
is missing then the checker reads the DRAT proof file from <stdin>.

The tool has support for reading compressed CNFS and proofs in 'gzip',
'zip', 'bzip2', 'xz' and '7z' format, but relies on external tools to
do so, actually using pipes through the 'popen' command.  Decompression is
triggered if a given file name has a corresponding suffix, i.e., '.gz',
'.zip', 'bz2', '.xz' or '.7z' and thus of course does not work when
reading from <stdin>.

The proof is checked to be a valid DRAT proof of all the clauses in
<post.cnf> starting with the clauses in <pre.cnf>.  Since a DRAT proof
also contains deletion information, the clauses in <post.cnf> must not
only occur in the proof but should also still be present at the end of
the proof.  Further, not all clauses still alive at the end of the proof
have to be in <post.cnf>.

If the check succeeds 's VERIFIED' is printed on a single line.  In this
case the checker will produce a zero exit code.  If the check fails the
reason for the failure is explained as error message and the program
exits with a non zero exit code.