Within each set, all of the Otter jobs used the same settings. However, the settings for the basic set were substantially different from those for the equality set. The ROO jobs used settings slightly different from the Otter jobs, and (for small technical reasons) the ROO settings for the basic set varied slightly, depending on whether equality is present.
For the basic set, the initial set of support consisted of the positive input clauses, except (x=x). For the equality set, the initial set of support depended on whether the theorem has an obvious special hypothesis--if so, then the set of support was the special hypothesis and the denial of the conclusion; if not, the set of support consisted of all input clauses.
The rules for the equality set state that an ordering on the symbols may be input along with the input clauses. The ordering is used to orient equality literals.