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. expandtrace1 is the 64-bit version, uses 10+ GB of virtual memory. "make >& make-4.log" compiles expandtrace1 without optimizations, with -g. On a 32-bit architecture expandtrace1 should come out as a 32-bit binary that is no different in behavior from expandtrace0, e.g., it uses 2.5 GB of virtual memory. gcc -c -Wall cbigopen.c <---- cbigopen needed for Linux and files > 2 GB. Leave out cbigopen.o on next two lines if unneeded. gcc -g -Wall -o expandtrace0 expandtrace0.c cbigopen.c gcc -O3 -Wall -o expandtrace0 expandtrace0.c cbigopen.c expandtrace1 ex1.cnf ex1.trA32 > ex1-tr.prfA32 expandtrace1 ex1.cnf ex5-bad.trA > ex5-bad-tr.prfA expandtrace1 ex2.cnf ex2B.trA > ex2B-tr.prfA 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 12, 2007 (original notes May 23, 2004) ex2.cnf, ex2A.prfA, ex2B.prfA ex2B.trA are from Daniel Le Berre. checker3 replaces checker0,1,2 checker1 attempts to use 64-bit ints and pointers to handle more than 4GB file. gcc -c -Wall cbigopen64.c <--- Linux, like cbigopen.o but 64-bit pointers. gcc -g -Wall -o checker1 checker1.c cbigopen64.o This really needs mmap to be robust. % gcc -c -Wall -m64 cbigopen64.c cbigopen64.c:1: sorry, unimplemented: 64-bit mode not compiled in gcc -g -Wall -m64 -o checker1 checker1.c cbigopen64.o will meet same fate.