checker0: check resolution proof (%RES format).

expandtrace0: expand proof trace file (%RPT format) to
resolution proof (%RES format) on stdout, which should always be redirected.

See fileformat.txt for specifications for both formats.
The examples, *.prf* and *.tr*, are ASCII (A32), but large files should be
binary (L32 or B32).

cc -g -o checker0 checker0.c

cc -g -o expandtrace0 expandtrace0.c

checker0 ex1.cnf ex1.prfA

checker0 ex1.cnf ex3.prfA

checker0 ex1.cnf ex1.prfA32

checker0 ex1.cnf ex5-bad.prfA

checker0 ex2.cnf ex2A.prfA

checker0 ex2.cnf ex2B.prfA

expandtrace0 ex1.cnf ex1.trA32 > ex1-tr.prfA32

expandtrace0 ex1.cnf ex5-bad.trA > ex5-bad-tr.prfA

expandtrace0 ex2.cnf ex2B.trA > ex2B-tr.prfA

expandtrace0 ex1.cnf ex1.trA32 | checker0 ex1.cnf -


To track down format and syntax errors,
run in a debugger and set a breakpoint on fatalErr().
Begin execution and when it stops in fatalErr,
then go 'up' the call stack to see who called it and why.

Allen Van Gelder  avg@cs.ucsc.edu
May 23, 2004

ex2.cnf, ex2A.prfA, ex2B.prfA ex2B.trA are from Daniel Le Berre.