OTTER 3.0^{∗}

William McCune

Mathematics and Computer Science Division Argonne National Laboratory Argonne, Illinois 60439-4844, U.S.A. e-mail: mccune@mcs.anl.gov phone: 708-252-3065

Preprint MCS-P399-1193, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Ill., March 1994.

Otter is a clause-based theorem prover for first-order logic with equality. It offers the inference rules binary resolution, hyperresolution, unit-resulting resolution, and paramodulation; it also offers forward and backward subsumption, forward and backward demodulation (rewriting), term ordering, Knuth-Bendix completion, answer literals, and conversion of first-order formulas to clauses. Otter 3.0 can be used in two modes. In the ordinary mode, the user specifies inferences rules and a search strategy, and in the autonomous mode (new in Otter 3.0, see below) the user simply supplies a set of clauses. The goal in building Otter was to have a fast, production-quality theorem prover for experimenting with new methods and for assisting mathematicians and logicians with their research.

At the core of Otter is a straightforward mechanism, the given-clause algorithm, for drawing inferences and searching for a refutation with the set of support strategy. The given-clause algorithm operates mainly on two lists of clauses, sos and usable. At the start of the search, sos is the supported clauses, and usable is the nonsupported clauses. The main loop of the given-clause algorithm is the following.

    While (sos is not empty and no refutation has been found)
        1. Let given_clause be the `best' clause in sos;
        2. Move given_clause from sos to usable;
        3. Infer and process new clauses using the inference rules in
               effect; each new clause must have the given_clause as
               one of its parents and members of usable as its other
               parents;  new clauses that pass the retention tests
               are appended to sos;
    End of while loop.

Surrounding the core of Otter are many additional features, including weighting functions to guide and restrict the search, a simple interactive routine for modifying the search, a flexible syntax, and evaluable functions and enhanced term rewriting for “programming” searches.

New Features. Features new in Otter 3.0 include Prolog-style operator declaration, the hot-list strategy for emphasizing key clauses, interactive selection of given clauses, ordered hyperresolution, optimization for propositional problems, and an autonomous mode.

∗This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.

For the autonomous mode, the user supplies a set of clauses and/or nonclausal formulas, then Otter does a simple syntactic analysis, automatically setting parameters and assigning clauses to lists. The properties that are considered are whether the clauses are Horn, are propositional, involve equality, contain equality axioms, and are all units.

Experiments on TPTP. Table 1 lists the results of Otter in its autonomous mode for the problems of TPTP v1.0.0 [2]. TPTP problems involving equality contain equality axioms, and for those problems, we deleted the equality axioms and used paramodulation and demodulation instead.

The TPTP experiments were run on an i486 DX2-66 processor running the Linux operating system. (For Otter jobs, the Linux i486 is about 1.3 times faster than a SPARCstation 2.) For problems that are listed, the number of seconds taken to find a proof is shown. If a problem is not listed, then a proof was not found within ten minutes.

Availability. The Otter 3.0 distribution, including source code, many test problems, and the manual [1], is freely available by anonymous FTP from info@mcs.anl.gov; see the file pub/Otter/README. Otter 3.0 might be available for DOS and/or Macintosh operating systems in the near future. One can request information by e-mail from otter@mcs.anl.gov.

Table 1: TPTP Problem—Seconds to Proof

ALG001-3 418 ALG002-1  2
BOO001-1 <1 BOO002-1 34 BOO003-1 14 BOO003-2 <1 BOO004-1  2
BOO004-2  1 BOO005-1  8 BOO006-1 20 BOO006-2 <1 BOO007-2 100
BOO008-1 221 BOO008-2 173 BOO009-1 19 BOO009-2  1 BOO010-1  9
BOO010-2  1 BOO011-1 <1 BOO012-1 60 BOO012-2 <1 BOO012-3 407
BOO013-1 22 BOO013-2 <1 BOO013-3 23 BOO014-2 40 BOO016-1 11
BOO016-2 2 BOO017-1 31 BOO017-2 3
CAT001-1 14 CAT001-3  3 CAT002-1 31 CAT002-3 572 CAT002-4 53
CAT003-1 12 CAT003-4 577 CAT004-1 30 CAT005-1  2 CAT005-3 <1
CAT005-4 <1 CAT006-1  2 CAT006-3 <1 CAT006-4 <1 CAT007-1 <1
CAT007-3 13 CAT008-1 3 CAT009-1 4 CAT010-1 4 CAT011-1 <1
CAT011-2 <1 CAT011-3 548 CAT011-4 21 CAT012-1  2 CAT012-3 228
CAT012-4 14 CAT013-1 <1 CAT013-3 546 CAT013-4 18 CAT014-1  2
CAT014-2 <1 CAT014-3 551 CAT014-4 18 CAT016-3 <1 CAT016-4 <1
CAT017-3 <1 CAT017-4 <1 CAT018-1  3 CAT019-1 <1 CAT019-2 <1
CAT019-3 23
COL001-1 2 COL001-2 <1 COL002-1 1 COL002-2 14 COL004-3 <1
COL007-1 <1 COL008-1 <1 COL009-1  3 COL010-1 <1 COL011-1 13
COL012-1 <1 COL013-1 <1 COL014-1 <1 COL015-1 <1 COL016-1 <1
COL017-1 <1 COL018-1 <1 COL019-1 <1 COL020-1 <1 COL021-1 <1
COL022-1 <1 COL023-1 <1 COL024-1 <1 COL025-1 <1 COL026-1  1
COL027-1  2 COL028-1 <1 COL029-1 <1 COL030-1 <1 COL031-1 <1
COL032-1 <1 COL033-1 <1 COL034-1  2 COL035-1 19 COL039-1 13
COL040-1 17 COL041-1  1 COL044-1 17 COL045-1 <1 COL048-1 <1
COL049-1  5 COL050-1 <1 COL051-1 <1 COL052-1 <1 COL052-2 <1
COL053-1 <1 COL054-1 <1 COL055-1 <1 COL056-1 <1 COL057-1  8
COL058-1 <1 COL058-2  1 COL058-3 <1 COL059-1 <1 COL060-2 <1

Table 1: TPTP Problem—Seconds to Proof (continued)

COL060-3 <1 COL061-2 <1 COL061-3 <1 COL062-2 <1 COL062-3 <1
COL063-2 <1 COL063-3 <1 COL063-4 <1 COL063-5 <1 COL063-6 <1
COL064-10 <1 COL064-11 <1 COL064-2 <1 COL064-3 <1 COL064-4 <1
COL064-5 <1 COL064-6 <1 COL064-7 <1 COL064-8 <1 COL064-9 <1
COL066-2 <1 COL066-3 <1
COM001-1 <1 COM002-1 <1 COM002-2 <1
GEO002-3 <1 GEO003-1 2 GEO003-2 3 GEO003-3 1 GEO006-3 15
GEO007-3 255 GEO011-2 <1 GEO011-3  3 GEO011-4 <1 GEO011-5 <1
GEO013-3 101 GEO014-2 <1 GEO015-2  2 GEO015-3 <1 GEO016-2 <1
GEO016-3 <1 GEO017-2  5 GEO017-3  4 GEO018-2  4 GEO018-3  6
GEO019-2 <1 GEO019-3 <1 GEO020-2  5 GEO020-3  4 GEO021-2  3
GEO021-3  6 GEO022-2  17 GEO022-3 16 GEO024-2  4 GEO024-3  3
GEO026-2  14 GEO026-3  27 GEO027-3  4 GEO030-2 110 GEO030-3 93
GEO034-3  95 GEO035-2  1 GEO035-3  1 GEO036-2 469 GEO036-3 85
GEO038-2  3 GEO038-3  2 GEO039-2 27 GEO039-3 <1 GEO041-3  3
GEO045-3  10 GEO046-3  9 GEO047-3  6 GEO051-3 93 GEO052-3 92
GEO053-3  15 GEO054-2 <1 GEO054-3 <1 GEO055-2 <1 GEO055-3 <1
GEO056-2  6 GEO056-3 <1 GEO057-2  2 GEO057-3 <1 GEO058-2 38
GEO058-3  8 GEO064-3  5 GEO065-3  5 GEO066-3  5 GEO067-2  4
GEO067-3  3 GEO069-3 107
GRA001-1 <1
GRP001-1 <1 GRP001-2 <1 GRP001-4 <1 GRP001-5 <1 GRP002-3  2
GRP002-4  4 GRP003-1 <1 GRP003-2 <1 GRP004-1 <1 GRP004-2 <1
GRP005-1 <1 GRP006-1 <1 GRP007-1 <1 GRP008-1 11 GRP009-1 <1
GRP010-1 <1 GRP010-4 <1 GRP011-4 <1 GRP012-1 <1 GRP012-2 <1
GRP012-3  4 GRP012-4 <1 GRP013-1 <1 GRP017-1 <1 GRP018-1 <1
GRP019-1 <1 GRP020-1 <1 GRP021-1 <1 GRP022-1 <1 GRP022-2 <1
GRP023-1 <1 GRP023-2 <1 GRP025-1  4 GRP025-2  2 GRP025-3  4
GRP025-4  4 GRP026-1  11 GRP026-2  4 GRP026-3 11 GRP026-4  7
GRP027-1 <1 GRP027-2 <1 GRP028-1 <1 GRP029-1 <1 GRP029-2 <1
GRP030-1 <1 GRP031-1 <1 GRP031-2 <1 GRP032-3 <1 GRP033-3 <1
GRP033-4 <1 GRP034-3 <1 GRP034-4 <1 GRP035-3 <1 GRP036-3 <1
GRP037-3  2 GRP038-3 <1 GRP041-2 <1 GRP042-2 <1 GRP043-2 <1
GRP044-2 <1 GRP045-2 <1 GRP046-2 <1 GRP047-2 <1 GRP048-2 <1
GRP050-1  37 GRP058-1  10 GRP059-1 11 GRP070-1 225 GRP075-1 140
GRP076-1 313 GRP078-1 254 GRP079-1 100 GRP085-1  2 GRP086-1  2
GRP087-1  24 GRP096-1 211 GRP098-1 258 GRP100-1 224 GRP103-1 326
HEN001-1 <1 HEN001-3 <1 HEN001-5 <1 HEN002-1 <1 HEN002-2 <1
HEN002-3 <1 HEN002-4 <1 HEN002-5 <1 HEN003-1 <1 HEN003-2 <1
HEN003-3 <1 HEN003-4 <1 HEN003-5  2 HEN004-1  3 HEN004-2  2
HEN004-3  1 HEN004-4  4 HEN004-5  5 HEN004-6  2 HEN005-1 <1
HEN005-2  2 HEN005-3 <1 HEN005-4  4 HEN005-5  5 HEN005-6 <1
HEN006-1  4 HEN006-2  7 HEN006-3 52 HEN006-4  4 HEN006-5  8
HEN006-6  65 HEN006-7  4 HEN007-1 24 HEN007-2  2 HEN007-3 199
HEN007-4 <1 HEN007-5  61 HEN007-6  2 HEN008-1 <1 HEN008-2  3
HEN008-3 <1 HEN008-4  2 HEN008-5 <1 HEN008-6 <1 HEN009-1 18
HEN009-2  2 HEN009-3 518 HEN009-4  1 HEN009-5  3 HEN009-6 17
HEN010-1  14 HEN010-2  3 HEN010-4  7 HEN010-5  6 HEN010-6  8
HEN010-7  2 HEN011-1 209 HEN011-2 162 HEN011-4 255 HEN011-5 483
HEN012-1  1 HEN012-3 <1
LAT005-1 16 LAT005-2 5
LCL004-1  24 LCL006-1 419 LCL007-1 <1 LCL008-1 <1 LCL009-1 <1
LCL010-1 3 LCL011-1 75 LCL012-1 555 LCL013-1 <1 LCL014-1 164
LCL015-1 481 LCL016-1 272 LCL017-1 549 LCL018-1 379 LCL022-1 <1

Table 1: TPTP Problem—Seconds to Proof (continued)

LCL023-1  3 LCL024-1  516 LCL025-1  37 LCL026-1  53 LCL027-1  <1
LCL029-1  3 LCL030-1  420 LCL033-1  <1 LCL034-1  8 LCL035-1  <1
LCL036-1  2 LCL039-1  127 LCL040-1  113 LCL041-1  3 LCL043-1  4
LCL044-1  5 LCL046-1  <1 LCL047-1  4 LCL048-1  4 LCL049-1  42
LCL050-1  44 LCL051-1  223 LCL052-1  43 LCL053-1  46 LCL055-1  23
LCL056-1  20 LCL057-1  22 LCL059-1  20 LCL064-1  486 LCL064-2  8
LCL065-1  2 LCL066-1  <1 LCL067-1  249 LCL070-1  248 LCL071-1  253
LCL072-1  115 LCL075-1  9 LCL076-1  <1 LCL076-2  <1 LCL076-3  <1
LCL077-1  <1 LCL077-2  <1 LCL079-1  <1 LCL080-1  66 LCL080-2  52
LCL081-1  <1 LCL082-1  <1 LCL083-1  16 LCL083-2  <1 LCL084-2  <1
LCL084-3  <1 LCL086-1  <1 LCL087-1  <1 LCL088-1  2 LCL089-1  3
LCL090-1  2 LCL091-1  3 LCL092-1  4 LCL093-1  112 LCL094-1  5
LCL095-1  13 LCL096-1  105 LCL097-1  4 LCL098-1  6 LCL101-1  <1
LCL102-1  33 LCL103-1  221 LCL104-1  <1 LCL106-1  <1 LCL107-1  <1
LCL108-1  1 LCL109-5  <1 LCL109-6  102 LCL110-1  1 LCL110-2  <1
LCL111-1  2 LCL111-2  9 LCL112-1  <1 LCL112-2  <1 LCL113-2  <1
LCL114-2  1 LCL115-1  8 LCL115-2  2 LCL116-2  2 LCL117-1  <1
LCL118-1  8 LCL120-1  50 LCL121-1  120 LCL126-1  <1 LCL128-1  125
LCL130-1  <1 LCL131-1  122 LCL132-1  <1 LCL133-1  <1 LCL134-1  <1
LCL135-1  <1 LCL138-1  105 LCL139-1  <1 LCL140-1  <1 LCL141-1  <1
LCL143-1  <1 LCL146-1  107 LCL153-1  <1 LCL154-1  <1 LCL155-1  <1
LCL156-1  <1 LCL157-1  <1 LCL158-1  <1 LCL159-1  1 LCL161-1  <1
LCL162-1  40 LCL163-1  162 LCL164-1  1
LDA001-1  <1 LDA002-1  2 LDA003-1  <1 LDA007-1  40 LDA007-2  25
LDA007-3  <1 LDA010-2  195 LDA011-2  189 LDA012-2  11 LDA013-1  <1
MSC001-1  7 MSC002-1  <1 MSC002-2  <1 MSC003-1  <1 MSC004-1  <1
MSC005-1  29 MSC006-1  5 MSC007-1.002 <1 MSC007-1.003 <1 MSC007-1.004 <1
MSC007-1.005 <1 MSC007-1.006 9 MSC007-1.007 193 MSC007-2.002 <1 MSC007-2.003 3
MSC008-1.002 67
NUM001-1  <1 NUM002-1  <1 NUM003-1  <1 NUM004-1  <1 NUM009-1  40
NUM014-1  <1 NUM015-1  <1 NUM016-1  <1 NUM016-2  <1 NUM017-1  168
NUM017-2  168 NUM019-1  <1 NUM020-1  <1 NUM021-1  <1 NUM022-1  <1
NUM023-1  <1 NUM025-1  <1 NUM025-2  <1 NUM180-1  7 NUM183-1  45
NUM190-1  11 NUM228-1  10 NUM283-1.002 <1 NUM283-1.003 <1 NUM283-1.004 <1
NUM283-1.005 9 NUM284-1.002 <1 NUM284-1.003 <1 NUM284-1.004 <1 NUM284-1.005 <1
NUM284-1.006 <1 NUM284-1.007 <1 NUM284-1.008 <1 NUM284-1.009 <1 NUM284-1.010 <1
PLA002-1  <1 PLA003-1  <1
PRV001-1  <1 PRV002-1  2 PRV003-1  <1 PRV005-1  2 PRV006-1  <1
PRV008-1  2 PRV009-1  <1
PUZ001-1  <1 PUZ001-2  <1 PUZ002-1  <1 PUZ003-1  <1 PUZ004-1  <1
PUZ005-1  1 PUZ006-1  <1 PUZ007-1  <1 PUZ008-1  <1 PUZ008-2  <1
PUZ009-1  <1 PUZ011-1  <1 PUZ012-1  <1 PUZ013-1  <1 PUZ014-1  <1
PUZ016-1  4 PUZ018-1  <1
RNG001-1  31 RNG001-2  7 RNG001-3  77 RNG001-4  19 RNG001-5  32
RNG002-1  <1 RNG003-1  <1 RNG004-1  20 RNG004-2  31 RNG004-3  5
RNG005-1  4 RNG005-2  <1 RNG006-1  50 RNG006-2  8 RNG006-3  12
RNG007-1  11 RNG007-4  <1 RNG008-1  130 RNG008-2  183 RNG008-3  1
RNG008-4  1 RNG008-5  98 RNG008-6  164 RNG008-7  2 RNG010-1  <1
RNG010-2  <1 RNG011-5  <1 RNG012-6  <1 RNG013-6  <1 RNG014-6  <1
RNG015-6  <1 RNG016-6  1 RNG017-6  <1 RNG018-6  <1 RNG019-6  2
RNG019-7  1 RNG020-6  1 RNG020-7  1 RNG021-6  1 RNG021-7  1
RNG023-6  1 RNG023-7  1 RNG024-6  1 RNG024-7  1 RNG025-4  77
RNG025-5  115 RNG025-6  76 RNG025-7  116 RNG027-2  <1 RNG028-2  <1
RNG029-2  <1 RNG037-1  4 RNG037-2  <1 RNG038-1  <1 RNG038-2  <1

Table 1: TPTP Problem—Seconds to Proof (continued)

RNG039-1  10 RNG039-2  11 RNG040-1  <1 RNG040-2  1 RNG041-1  3
ROB002-1  <1 ROB003-1  <1 ROB004-1  1 ROB005-1  46 ROB008-1  <1
ROB009-1  <1 ROB010-1  <1 ROB011-1  <1 ROB013-1  <1 ROB014-2 216
ROB016-1  <1 ROB021-1  2 ROB022-1  2 ROB023-1  2 ROB025-1 313
SYN001-1.001 <1 SYN001-1.002 <1 SYN001-1.003 <1 SYN001-1.004 <1 SYN001-1.005 <1
SYN001-1.006 <1 SYN001-1.007 3 SYN001-1.008 11 SYN001-1.009 63 SYN001-1.010 449
SYN002-1.000 <1 SYN002-1.002 <1 SYN002-1.004 <1 SYN002-1.006 <1 SYN002-1.008 <1
SYN002-1.010 <1 SYN002-1.012 <1 SYN002-1.016 <1 SYN002-1.020 1 SYN002-1.030 3
SYN002-1.040 9 SYN002-1.050 25 SYN003-1.002 <1 SYN003-1.003 <1 SYN003-1.004 <1
SYN003-1.005 <1 SYN003-1.006 <1 SYN003-1.007 <1 SYN003-1.008 <1 SYN003-1.009 <1
SYN003-1.010 <1 SYN004-1.002 <1 SYN004-1.003 <1 SYN004-1.004 <1 SYN004-1.005 <1
SYN004-1.006 <1 SYN004-1.007 <1 SYN004-1.008 <1 SYN004-1.009 <1 SYN004-1.010 <1
SYN005-1.002 <1 SYN005-1.003 <1 SYN005-1.004 <1 SYN005-1.005 <1 SYN005-1.006 <1
SYN005-1.007 <1 SYN005-1.008 <1 SYN005-1.009 <1 SYN005-1.010 <1 SYN006-1  <1
SYN007-1.001 <1 SYN007-1.002 <1 SYN007-1.003 <1 SYN007-1.004 <1 SYN007-1.005 3
SYN007-1.006 13 SYN007-1.007 62 SYN008-1 <1 SYN009-1 <1 SYN010-1.002 <1
SYN010-1.005 <1 SYN010-1.010 <1 SYN010-2.002 <1 SYN010-2.005 <1 SYN010-2.010 <1
SYN010-3.002 <1 SYN010-3.005 <1 SYN010-3.010 2 SYN014-2  <1 SYN015-2  219
SYN028-1  <1 SYN029-1  <1 SYN030-1  <1 SYN031-1  <1 SYN032-1  <1
SYN033-1  <1 SYN034-1  <1 SYN035-1  <1 SYN036-3  2 SYN036-4  26
SYN037-1  74 SYN037-2  <1 SYN038-1  2 SYN039-1  2 SYN040-1  <1
SYN041-1  <1 SYN042-1  <1 SYN043-1  <1 SYN044-1  <1 SYN045-1  <1
SYN046-1  <1 SYN047-1  <1 SYN048-1  <1 SYN049-1  <1 SYN050-1  <1
SYN051-1  <1 SYN052-1  <1 SYN053-1  <1 SYN054-1  <1 SYN055-1  <1
SYN057-1  <1 SYN058-1  <1 SYN060-1  <1 SYN061-1  <1 SYN062-1  <1
SYN063-1  <1 SYN064-1  <1 SYN065-1  <1 SYN066-1  <1 SYN068-1  <1
SYN069-1  <1 SYN070-1  <1 SYN071-1  <1 SYN072-1  <1 SYN073-1  <1
SYN074-1  12 SYN075-1  2 SYN079-1  <1 SYN080-1  <1 SYN081-1  <1
SYN082-1  <1 SYN083-1  <1 SYN085-1.005 <1 SYN085-1.010 <1 SYN085-1.020 <1
SYN088-1.005 <1 SYN088-1.010 <1 SYN089-1.005 <1 SYN089-1.010 2 SYN089-1.020 22
SYN090-1.005 <1 SYN090-1.010 <1 SYN090-1.020 2 SYN093-1.005 1 SYN093-1.010 9
SYN093-1.020 130 SYN094-1.005 <1 SYN094-1.010 2 SYN094-1.020 6 SYN095-1.005 <1
SYN095-1.010 2 SYN095-1.020 17 SYN096-1.005 <1 SYN096-1.010 <1 SYN096-1.020 2
SYN097-1.005 3 SYN097-1.010 33 SYN097-1.020 538 SYN098-1.005 2 SYN098-1.010 6
SYN098-1.020 20 SYN099-1.005 <1 SYN099-1.010 6 SYN099-1.020 52 SYN100-1.005 <1
SYN100-1.010 2 SYN100-1.020 4 SYN101-1.005 5 SYN101-1.010 23 SYN101-1.020 140
SYN102-1.005 4 SYN102-1.010 7 SYN102-1.020 16
TOP002-2  <1 TOP004-1  <1 TOP004-2  <1 TOP005-2  <1
SET001-1  <1 SET002-1  31 SET003-1  <1 SET004-1  <1 SET006-1  <1
SET008-1  5 SET009-1  3 SET012-4  263 SET017-6  96 SET017-7  221
SET019-3  30 SET019-4  24 SET024-3  5 SET024-4  3 SET024-6  <1
SET024-7  2 SET025-3  4 SET025-4  2 SET025-6  2 SET025-7  3
SET027-3  583 SET027-4  559 SET027-6  4 SET027-7  4 SET043-5  <1
SET044-5  <1 SET045-5  <1 SET046-5  <1 SET050-6  7 SET051-6  6
SET052-6  8 SET053-6  8 SET054-6  <1 SET054-7  <1 SET055-6  81
SET055-7  <1 SET056-6  123 SET056-7  127 SET057-6  1 SET057-7  1
SET058-6  1 SET058-7  1 SET059-6  1 SET059-7  1 SET060-6  3
SET060-7  5 SET061-6  86 SET061-7  10 SET062-6  33 SET062-7  1
SET063-6  32 SET063-7  1 SET064-6  133 SET064-7  13 SET065-6  <1
SET065-7  1 SET072-6  197 SET072-7  403 SET073-6  83 SET073-7  2
SET074-6  83 SET074-7  2 SET075-6  67 SET075-7  2 SET077-6  <1
SET077-7  <1 SET078-6  1 SET078-7  1 SET079-6  100 SET079-7  2
SET080-6  <1 SET080-7  1 SET081-6  1 SET081-7  2 SET082-6  138
SET082-7  99 SET083-6  133 SET083-7  279 SET084-6  8 SET084-7  46

Table 1: TPTP Problem—Seconds to Proof (continued)

SET085-6 158 SET093-6 7 SET093-7 87 SET094-6 107 SET094-7 64
SET095-7 2 SET096-6 495 SET096-7 33 SET101-6 2 SET101-7 3
SET102-6 2 SET102-7 3 SET108-6 6 SET108-7 41 SET117-6 8
SET117-7 62 SET118-6 1 SET118-7 3 SET146-6 159 SET152-6 7
SET158-6 1 SET166-6 102 SET184-6 5 SET196-6 135 SET197-6 135
SET203-6 1 SET204-6 8 SET235-6 33 SET236-6 34 SET242-6 2
SET296-6 <1 SET411-6 52 SET479-6 185 SET506-6 43 SET507-6 87
SET510-6 156 SET516-6 443 SET517-6 491 SET553-6 476 SET558-6 1
SET559-6 293 SET561-6 310 SET562-6 427 SET563-6 120 SET564-6 102
SET565-6 291 SET566-6 118

References

[1] W. McCune. Otter 3.0 Reference Manual and Guide. Tech. report, Argonne National Laboratory, Argonne, Ill., 1993.

[2] C.B. Suttner, G. Sutcliffe, and T. Yemenis. The TPTP Problem Library (TPTP v1.0.0 - TR 13.11.93). Technical Report FKI-184-93, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University, Townsville, Australia, 1993.