There are two binaries for checker3: checker3_32_O3 and checker3_64_O3.
checker3_32_O3 may be unable to process a proof over 4 GB (maybe 3 GB?);
it has not been tested to find out.
checker3_64_O3 requires a 64-bit kernel.
Both are linux, statically linked.

There are also checker3 and checker3_64_g, requiring a 64-bit kernel,
and dynamically linked.  The timestamps show checker3_32_O3 and checker3
are older.  checker3_64_g is compiled to run in gdb.

checker3_64_O3 and checker3_64_g 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 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.

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