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 now three binaries for rupToRes: rupToRes_32_O3, rupToRes_32_O3_3GB,
and rupToRes_64_O3.
-rwxr-xr-x   1 avg       1300741 Oct  7 10:33 rupToRes_32_O3
-rwxr-xr-x   1 avg       1300741 Oct  7 10:26 rupToRes_32_O3_3GB
-rwxr-xr-x   1 avg       1413424 Oct  7 09:29 rupToRes_64_O3

All three are linux, statically linked.
All three now print a line with ERROR in it and exit with a nonzero code
if an error condition, such as out-of-memory, causes termination.

rupToRes_64_O3 requires a 64-bit kernel; it limits itself to 8 GB memory.

rupToRes_32_O3_3GB might run very slowly on a system with less than 4 GB
of real memory and might crash on a system with less than 4 GB virtual memory;
it limits itself to 3 GB memory.

rupToRes_32_O3 limits itself to 1 GB memory.  This has been adequate for
output RES proof files as large as 163 GB.

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 is better to be
on a local disk.  I have tested it with a remote-mounted (NFS) file system
and observed CPU usage of 3% to 5%, due to disk waits, but it works.
See README-checker3 for more details.

--Allen Van Gelder