There are two "production" binaries for checker3: checker3_32_O3 and checker3_64_O3. checker3_32_O3 is unable to process a proof over 4 GB (actually 3 GB+). checker3_64_O3 requires a 64-bit kernel. Both are linux, statically linked. There are also checker3 and checker3_64_g-SHARED, requiring a 64-bit kernel, and dynamically linked. The timestamps show checker3_32_O3 and checker3 are older. checker3_64_g-SHARED is compiled to run in gdb. checker3_64_O3 and checker3_64_g-SHARED will detect an error return from the mmap() call. The others will fail on SEGV quickly. For Solaris or OS/X you will need a different Makefile. Contact me if you need this. The Usage message for checker3 and variants mentions two optional arguments: infile.cnf infile.proof in_clauses cnf_lits. It should never need these, and they are hard to figure out correctly, so just supply the first two required arguments. checker3 also sets its own limits for stacksize and corefilesize and its output is reasonably concise, so running it without a script is feasible. ./checker3_64_O3 infile.cnf infile.proof Note that infile.proof is accessed by mmap so it probably needs to be on a local disk. On Intel/AMD machines it must be %RES L32 format. The idea is that this file can be larger than would fit in your combined real memory + swap space. However, the CPU usage will be around 10% due to lots of disk access. For NSF mounted disk, expect CPU usage of 3% to 5%. However, if it can get enough real memory, and there is no serious contention, the CPU usage is over 90%. If you need a program to produce a proof, zchaff0_32 does pretty well. --Allen Van Gelder