Years of experimentation with theorem-proving systems[4,9,3,5,6] has caused us to accumulate a wide variety of variations and parameters to control our basic theorem-proving algorithm. The typical user need know about only a few of them. This contest forced us to consider how we would set them if there were to be parameterless versions of Otter and ROO. Most of the above settings just represent common sense. The value of max_mem did have to be carefully chosen so that we could get proofs of all of these theorems with the same value.
We used the ``standard'' version of Otter for these runs. This set of problems forced us to make some changes to ROO in order to better emulate the pick_given_ratio strategy in the parallel setting.
We thank Ross Overbeek for proposing this exercise, and hope that others found it as useful as we did.