The script check-rup.csh (or check-rup-32.csh) should be looked at and
usually used, to run rupToRes and then checker3, to verify a RUP proof
that your solver produced.
You set a few variables in the beginning of the script and it handles
the details.

See rupToRes-32.log for the output generated by check-rup-32.csh.

There are two binaries for rupToRes: rupToRes_32_O3 and rupToRes_64_O3.
rupToRes_64_O3 requires a 64-bit kernel.
Both are linux, statically linked.
If you need sources, please contact me.  Since some of this code
comes from the zchaff project, I need to get permission.

rupToRes also sets its own limits for stacksize and corefilesize
and its standard output is reasonably concise, so running it without a script
is feasible, but dangerous without a limit on filesize, because the
proof output can be very long.

    ./rupToRes infile.cnf

the program expects infile.rup to be present and it writes infile.proof.
In normal usage, you follow up with verification:

    ./checker3 infile.cnf infile.proof

Note that infile.proof is accessed by mmap so it probably needs to be
on a local disk.  I have not tested it with a remote-mounted (NFS)
file system.  See README-checker3 for more details.

--Allen Van Gelder