OTTER 3.0.2 on TPTP 1.1.1^{∗}

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

August 22, 1993

This report presents the results of Otter 3.0.2 on each of the 2652 problems TPTP 1.1.1. Each run

• was made on SPARC 2 computer (either altair.mcs.anl.gov or donner.mcs.anl.gov);

• had any equality axioms removed with TPTP2X transformation

     equality([s,t,f,p]);

• used the TPTP2X conversion

     otter(none,[set(auto),assign(max_seconds,600)])

(autonomous mode, which sets a memory limit of 12 megabytes, and with a time limit of 10 minutes).

In the tables below, for each problem we list either a proof time (in seconds), “time” (time limit), “memory” (memory limit of 12 MB), “sos” (sos list empty), or “term” (limit on depth of terms). (The strategy is incomplete, so “sos empty” does not indicate satisfiability.) Proofs were found in 1224 (46%) of the runs, 1327 were stopped by the time limit, 13 ran out of memory, 85 stopped because the sos list was empty, and 3 stopped because a clause with a very deep term was generated.

Table 1 gives the number of proofs that were found within several other time limits.

Table 1: Proofs Within Various Time Limits

Seconds  Proofs
1 458 (17%)
5 886 (33%)
30 1031 (39%)
60 1087 (41%)
300 1188 (45%)
600 1224 (46%)

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

ALG001-1  time BOO010-4  0.38 CAT009-3  time COL003-5 memory
ALG001-2  time BOO011-1  0.44 CAT009-4  time COL003-6 memory
ALG001-3 515.44 BOO011-2  sos CAT010-1  4.73 COL004-1  time
ALG002-1  3.06 BOO011-4  sos CAT010-4  time COL004-2  time
ANA001-1  time BOO012-1 66.81 CAT011-1  0.89 COL004-3  0.24
ANA002-1  time BOO012-2  0.35 CAT011-2  0.11 COL005-1  time
ANA002-2  time BOO012-3 506.20 CAT011-3 578.55 COL006-1  time
ANA002-3  time BOO012-4  0.34 CAT011-4  23.55 COL006-2  time
ANA002-4  time BOO013-1 26.25 CAT012-1  2.24 COL006-3  time
ANA003-1  time BOO013-2  0.48 CAT012-3 244.11 COL006-4  time
ANA003-2  time BOO013-3 27.64 CAT012-4  15.26 COL007-1  0.04
ANA003-3  time BOO013-4  0.48 CAT013-1  0.73 COL008-1  0.07
ANA003-4  time BOO014-1  time CAT013-3 581.42 COL009-1  3.70
ANA004-1  time BOO014-2 50.20 CAT013-4  19.12 COL010-1  0.12
ANA004-2  time BOO014-3  time CAT014-1  1.91 COL011-1  19.74
ANA004-3  time BOO014-4 40.38 CAT014-2  0.10 COL012-1  0.08
ANA004-4  time BOO015-1  time CAT014-3 585.66 COL013-1  0.07
ANA004-5  time BOO015-2  9.92 CAT014-4  19.23 COL014-1  0.05
ANA005-1  time BOO015-4 13.54 CAT015-3  sos COL015-1  0.10
ANA005-2  time BOO016-1 12.87 CAT015-4  sos COL016-1  0.07
ANA005-3  time BOO016-2  2.23 CAT016-3  0.25 COL017-1  0.14
ANA005-4  time BOO017-1 36.22 CAT016-4  0.13 COL018-1  0.06
ANA005-5  time BOO017-2  4.58 CAT017-3  0.20 COL019-1  0.34
BOO001-1  1.15 BOO018-4  time CAT017-4  0.39 COL020-1  0.34
BOO002-1 43.51 CAT001-1 13.59 CAT018-1  4.04 COL021-1  0.11
BOO002-2 45.99 CAT001-2  time CAT018-3  time COL022-1  0.13
BOO003-1 16.28 CAT001-3  3.60 CAT018-4  time COL023-1  1.13
BOO003-2  0.25 CAT001-4  time CAT019-1  0.17 COL024-1  0.12
BOO003-4  0.17 CAT002-1 28.74 CAT019-2  0.09 COL025-1  0.09
BOO004-1  2.71 CAT002-2  time CAT019-3  26.53 COL026-1  1.87
BOO004-2  1.66 CAT002-3 560.29 CAT019-4  time COL027-1  2.49
BOO004-4  0.36 CAT002-4 49.32 CAT019-5  time COL028-1  1.14
BOO005-1 10.07 CAT003-1 11.49 CAT019-6  time COL029-1  0.04
BOO005-2  sos CAT003-2  time CID001-1  0.15 COL030-1  0.17
BOO005-4  sos CAT003-3  time CID002-1  time COL031-1  0.14
BOO006-1 22.42 CAT003-4 531.51 CID003-1  time COL032-1  0.08
BOO006-2  0.33 CAT004-1 28.03 CID003-2  525.03 COL033-1  0.24
BOO006-4  0.33 CAT004-2  time CIV001-1  4.09 COL034-1  3.66
BOO007-1  time CAT004-3  time CIV002-1  time COL035-1  24.06
BOO007-2 130.23 CAT004-4  time CIV003-1  time COL036-1  time
BOO007-4  8.80 CAT005-1  2.77 CIV004-1  time COL037-1  time
BOO008-1 273.10 CAT005-3  0.39 COL001-1  3.52 COL038-1  time
BOO008-2 225.72 CAT005-4  0.75 COL001-2  0.69 COL039-1  19.47
BOO008-3  sos CAT006-1  2.78 COL002-1  2.01 COL040-1  25.90
BOO008-4 71.86 CAT006-3  0.38 COL002-2  21.24 COL041-1  1.62
BOO009-1 22.83 CAT006-4  0.50 COL002-3  time COL042-1  time
BOO009-2  1.82 CAT007-1  0.26 COL003-1 memory COL043-1  time
BOO009-4  0.38 CAT007-3 15.00 COL003-2 memory COL044-1  25.95
BOO010-1 11.58 CAT008-1  3.21 COL003-3 memory COL045-1  0.11
BOO010-2  1.62 CAT009-1  4.58 COL003-4 memory COL046-1  time

COL047-1  time COM003-2  0.39 GEO018-2  3.86 GEO044-2  time
COL048-1  0.10 COM004-1  0.14 GEO018-3  6.05 GEO044-3  time
COL049-1  6.86 GEO001-1  time GEO019-2  0.55 GEO045-2  time
COL050-1  0.08 GEO001-2  time GEO019-3  0.61 GEO045-3 10.76
COL051-1  0.09 GEO001-3  time GEO020-2  5.90 GEO046-2  time
COL052-1  0.09 GEO001-4  2.74 GEO020-3  4.04 GEO046-3 10.18
COL052-2  0.23 GEO002-1  time GEO021-2  3.86 GEO047-2  time
COL053-1  0.09 GEO002-2  time GEO021-3  6.15 GEO047-3  6.50
COL054-1  0.18 GEO002-3  0.81 GEO022-2 19.68 GEO048-2  time
COL055-1  0.05 GEO002-4  0.86 GEO022-3 18.43 GEO048-3  time
COL056-1  0.07 GEO003-1  2.47 GEO024-2  3.91 GEO049-2  time
COL057-1 12.29 GEO003-2  3.88 GEO024-3  2.89 GEO049-3  time
COL058-1  0.10 GEO003-3  1.47 GEO025-2  time GEO050-2  time
COL058-2  2.01 GEO004-1  time GEO025-3  time GEO050-3  time
COL058-3  0.25 GEO004-2  time GEO026-2 15.21 GEO051-2  time
COL059-1  0.42 GEO005-1  time GEO026-3 31.34 GEO051-3 100.29
COL060-1  time GEO005-2  time GEO027-2  time GEO052-2  time
COL060-2  0.14 GEO006-1  time GEO027-3  4.64 GEO052-3 98.24
COL060-3  0.07 GEO006-2  time GEO028-2  time GEO053-2  time
COL061-1  time GEO006-3 16.21 GEO028-3  time GEO053-3 16.47
COL061-2  0.19 GEO007-1  time GEO029-2  time GEO054-2  0.44
COL061-3  0.16 GEO007-2  time GEO029-3  time GEO054-3  0.46
COL062-1  time GEO007-3 272.77 GEO030-2 135.41 GEO055-2  0.47
COL062-2  0.16 GEO008-1  time GEO030-3 106.05 GEO055-3  0.52
COL062-3  0.11 GEO008-2  time GEO031-2  time GEO056-2  6.04
COL063-1  time GEO008-3  time GEO031-3  time GEO056-3  0.53
COL063-2  0.21 GEO009-1  time GEO032-2  time GEO057-2  2.67
COL063-3  0.24 GEO009-2  time GEO032-3  time GEO057-3  0.54
COL063-4  0.23 GEO009-3  time GEO033-2  time GEO058-2 40.02
COL063-5  0.22 GEO010-1  time GEO033-3  time GEO058-3  8.94
COL063-6  0.20 GEO010-2  time GEO034-2  time GEO059-2  time
COL064-1  time GEO010-3  time GEO034-3 108.38 GEO059-3  time
COL064-10 0.22 GEO011-1  time GEO035-2  1.28 GEO060-2  time
COL064-11 0.21 GEO011-2  0.54 GEO035-3  1.20 GEO061-2  time
COL064-2  0.24 GEO011-3  3.14 GEO036-2 466.92 GEO061-3  time
COL064-3  0.28 GEO011-4  0.75 GEO036-3 86.11 GEO062-2  time
COL064-4  0.27 GEO011-5  0.38 GEO037-2  time GEO062-3  time
COL064-5  0.30 GEO012-1  time GEO037-3  time GEO063-2  time
COL064-6  0.26 GEO012-2  time GEO038-2  3.71 GEO063-3  time
COL064-7  0.25 GEO012-3  time GEO038-3  1.98 GEO064-2  time
COL064-8  0.25 GEO013-1  time GEO039-2 29.69 GEO064-3  5.68
COL064-9  0.22 GEO013-2  time GEO039-3  1.01 GEO065-2  time
COL065-1  time GEO013-3 109.86 GEO040-2  time GEO065-3  5.66
COL066-1  time GEO014-2  0.56 GEO040-3  time GEO066-2  time
COL066-2  0.25 GEO015-2  1.72 GEO041-2  time GEO066-3  5.65
COL066-3  0.29 GEO015-3  0.63 GEO041-3  3.59 GEO067-2  4.54
COM001-1 0.09 GEO016-2  0.53 GEO042-2  time GEO067-3  3.29
COM002-1 0.14 GEO016-3  0.63 GEO042-3  time GEO068-2  time
COM002-2 0.27 GEO017-2  5.98 GEO043-2  time GEO068-3  time
COM003-1 time GEO017-3  4.08 GEO043-3  time GEO069-2  time

GEO069-3 112.81 GRP020-1 0.25 GRP048-2  0.09 GRP098-1 338.12
GEO070-2 time GRP021-1 0.30 GRP049-1 sos GRP099-1 time
GEO070-3  time GRP022-1 0.40 GRP050-1 53.61 GRP100-1 300.50
GEO071-2  time GRP022-2 0.10 GRP051-1  time GRP101-1  time
GEO071-3  time GRP023-1 0.12 GRP052-1  time GRP102-1  sos
GEO072-2  time GRP023-2 0.04 GRP053-1  sos GRP103-1 427.12
GEO072-3  time GRP024-4 time GRP054-1  time GRP104-1  time
GEO073-1  time GRP025-1 4.50 GRP055-1  sos GRP105-1  time
GEO073-2  time GRP025-2 3.31 GRP056-1  time GRP106-1  time
GEO073-3  time GRP025-3 4.69 GRP057-1  sos GRP107-1  time
GEO074-2  time GRP025-4 4.90 GRP058-1 15.77 GRP108-1  time
GEO075-2  time GRP026-1 13.60 GRP059-1 16.93 GRP109-1  time
GEO076-4  time GRP026-2 8.51 GRP060-1  sos GRP110-1  time
GEO077-4  time GRP026-3 13.32 GRP061-1  sos GRP111-1  time
GEO078-4  time GRP026-4 11.34 GRP062-1  sos GRP112-1  time
GEO078-5  time GRP027-1 0.89 GRP063-1  time GRP113-1  time
GEO079-1  0.07 GRP027-2 0.93 GRP064-1  time HEN001-1  0.10
GRA001-1  0.08 GRP028-1 0.05 GRP065-1  sos HEN001-3  0.09
GRP001-1  0.22 GRP028-2 0.13 GRP066-1  time HEN001-5  0.06
GRP001-2  0.17 GRP028-3 0.12 GRP067-1  time HEN002-1  0.10
GRP001-3  time GRP029-1 0.24 GRP068-1  time HEN002-2  0.10
GRP001-4  0.16 GRP029-2 0.24 GRP069-1  time HEN002-3  0.08
GRP001-5  0.14 GRP030-1 0.25 GRP070-1 283.28 HEN002-4  0.09
GRP002-1  time GRP031-1 0.20 GRP071-1  sos HEN002-5  0.07
GRP002-2  time GRP031-2 0.48 GRP072-1  time HEN003-1  0.78
GRP002-3  3.53 GRP032-3 0.15 GRP073-1  sos HEN003-2  0.79
GRP002-4  5.29 GRP033-3 0.20 GRP074-1  sos HEN003-3  0.38
GRP003-1  0.14 GRP033-4 0.25 GRP075-1 187.97 HEN003-4  0.42
GRP003-2  0.25 GRP034-3 0.24 GRP076-1 416.21 HEN003-5  1.81
GRP004-1  0.13 GRP034-4 0.28 GRP077-1  sos HEN004-1  2.60
GRP004-2  0.24 GRP035-3 1.20 GRP078-1 334.40 HEN004-2  2.49
GRP005-1  0.09 GRP036-3 0.29 GRP079-1 138.59 HEN004-3  1.53
GRP006-1  0.14 GRP037-3 1.83 GRP080-1  time HEN004-4  4.42
GRP007-1  0.10 GRP038-3 0.47 GRP081-1  time HEN004-5  4.87
GRP008-1 13.04 GRP039-1 time GRP082-1  sos HEN004-6  1.88
GRP009-1  0.55 GRP039-2 time GRP083-1  sos HEN005-1  1.02
GRP010-1  0.21 GRP039-3 time GRP084-1  time HEN005-2  1.73
GRP010-4  0.10 GRP039-4 time GRP085-1  3.18 HEN005-3  0.64
GRP011-4  0.13 GRP039-5 time GRP086-1  2.51 HEN005-4  3.90
GRP012-1  0.58 GRP039-6 time GRP087-1 35.30 HEN005-5  4.28
GRP012-2  1.23 GRP039-7 time GRP088-1  time HEN005-6  0.58
GRP012-3  4.75 GRP040-3 time GRP089-1  time HEN006-1  4.62
GRP012-4  0.18 GRP040-4 time GRP090-1  time HEN006-2  6.62
GRP013-1  0.98 GRP041-2 0.09 GRP091-1  time HEN006-3 43.70
GRP014-1  sos GRP042-2 0.06 GRP092-1  time HEN006-4  3.82
GRP015-1  time GRP043-2 0.08 GRP093-1  time HEN006-5  8.06
GRP016-1  time GRP044-2 0.10 GRP094-1  time HEN006-6 55.75
GRP017-1  0.22 GRP045-2 0.07 GRP095-1  time HEN006-7  4.64
GRP018-1  0.24 GRP046-2 0.10 GRP096-1 269.98 HEN007-1 25.81
GRP019-1  0.28 GRP047-2 0.11 GRP097-1  time HEN007-2  2.45

HEN007-3 166.73 LCL011-1 110.04 LCL061-1  time LCL103-1 316.61
HEN007-4  0.51 LCL012-1  time LCL062-1  time LCL104-1  0.62
HEN007-5 60.73 LCL013-1  0.08 LCL063-1  time LCL105-1  time
HEN007-6  2.07 LCL014-1 238.48 LCL064-1  time LCL106-1  0.18
HEN008-1  0.99 LCL015-1  time LCL064-2 10.97 LCL107-1  0.89
HEN008-2  2.77 LCL016-1 408.46 LCL065-1  2.61 LCL108-1  1.81
HEN008-3  0.45 LCL017-1  time LCL066-1  1.28 LCL109-1  time
HEN008-4  2.12 LCL018-1 577.98 LCL067-1 407.95 LCL109-2  time
HEN008-5  0.26 LCL019-1  time LCL068-1  time LCL109-3  time
HEN008-6  0.38 LCL020-1  time LCL069-1  time LCL109-4  time
HEN009-1 18.59 LCL021-1  time LCL070-1 373.36 LCL109-5  0.60
HEN009-2  1.88 LCL022-1  1.39 LCL071-1 394.37 LCL109-6 131.59
HEN009-3 441.83 LCL023-1  4.53 LCL072-1 165.10 LCL110-1  1.60
HEN009-4  1.49 LCL024-1  time LCL073-1  time LCL110-2  0.94
HEN009-5  3.77 LCL025-1 58.52 LCL074-1  time LCL111-1  3.17
HEN009-6 17.94 LCL026-1 80.44 LCL075-1 15.53 LCL111-2 13.65
HEN010-1 15.11 LCL027-1  0.50 LCL076-1  0.74 LCL112-1  1.65
HEN010-2  3.34 LCL028-1  time LCL076-2  0.08 LCL112-2  1.12
HEN010-3  time LCL029-1  4.65 LCL076-3  9.80 LCL113-1  time
HEN010-4  9.04 LCL030-1  time LCL077-1  0.69 LCL113-2  1.15
HEN010-5  6.07 LCL031-1  time LCL077-2  9.16 LCL114-1  time
HEN010-6  7.70 LCL032-1  time LCL078-1  time LCL114-2  1.58
HEN010-7  2.54 LCL033-1  0.18 LCL079-1  0.09 LCL115-1 13.94
HEN011-1 210.26 LCL034-1 11.94 LCL080-1 97.91 LCL115-2  2.33
HEN011-2 141.76 LCL035-1  0.13 LCL080-2 78.91 LCL116-1  time
HEN011-3  time LCL036-1  3.30 LCL081-1  0.16 LCL116-2  2.91
HEN011-4 252.40 LCL037-1  time LCL082-1  0.26 LCL117-1  0.08
HEN011-5 471.79 LCL038-1  time LCL083-1 23.66 LCL118-1 11.77
HEN012-1  1.35 LCL039-1 181.16 LCL083-2  0.03 LCL119-1  time
HEN012-3  0.44 LCL040-1 176.52 LCL084-1  time LCL120-1 78.91
LAT001-1  time LCL041-1  3.91 LCL084-2  0.10 LCL121-1 172.08
LAT002-1  time LCL042-1  time LCL084-3  0.08 LCL122-1  time
LAT003-1  time LCL043-1  7.06 LCL085-1  time LCL123-1  time
LAT004-1  time LCL044-1  8.31 LCL086-1  0.75 LCL124-1  time
LAT005-1  6.94 LCL045-1  time LCL087-1  0.24 LCL125-1  time
LAT005-2  5.08 LCL046-1  0.15 LCL088-1  3.96 LCL126-1  0.24
LAT005-3  time LCL047-1  6.45 LCL089-1  4.01 LCL127-1  time
LAT005-4  time LCL048-1  6.52 LCL090-1  3.65 LCL128-1 179.66
LAT005-5 57.69 LCL049-1 67.38 LCL091-1  4.08 LCL129-1  time
LAT005-6 96.02 LCL050-1 66.82 LCL092-1  6.88 LCL130-1  0.23
LCL001-1  time LCL051-1 372.87 LCL093-1 169.47 LCL131-1 177.23
LCL002-1  time LCL052-1 66.88 LCL094-1  7.49 LCL132-1  0.27
LCL003-1  time LCL053-1 68.27 LCL095-1 19.42 LCL133-1  0.18
LCL004-1 36.16 LCL054-1  time LCL096-1 152.18 LCL134-1  0.25
LCL005-1  time LCL055-1 35.68 LCL097-1  6.13 LCL135-1  0.30
LCL006-1 585.17 LCL056-1 32.00 LCL098-1  9.95 LCL136-1  time
LCL007-1  0.05 LCL057-1 34.14 LCL099-1  time LCL137-1  time
LCL008-1  0.12 LCL058-1  time LCL100-1  time LCL138-1 139.83
LCL009-1  1.45 LCL059-1 31.92 LCL101-1  0.52 LCL139-1  1.22
LCL010-1  3.54 LCL060-1  time LCL102-1 50.41 LCL140-1  1.06

LCL141-1  1.61 LCL190-1 0.27 LCL239-1  sos MSC007-1.004  0.19
LCL142-1  time LCL191-1  sos LCL240-1  sos MSC007-1.005  0.94
LCL143-1  0.46 LCL192-1 14.82 LCL241-1  sos MSC007-1.006 13.55
LCL144-1  time LCL193-1 3.07 LCL242-1  sos MSC007-1.007 285.80
LCL145-1  time LCL194-1  sos LCL243-1  sos MSC007-1.008  time
LCL146-1 102.94 LCL195-1  sos LCL244-1  sos MSC007-1.009  time
LCL147-1  time LCL196-1 50.77 LCL245-1  sos MSC007-1.010  time
LCL148-1  time LCL197-1 1.29 LCL246-1  sos MSC007-1.011  time
LCL149-1  time LCL198-1 51.19 LCL247-1  sos MSC007-1.012  time
LCL150-1  time LCL199-1 0.78 LCL248-1  sos MSC007-1.013  time
LCL151-1  time LCL200-1 0.36 LCL249-1  sos MSC007-1.014  time
LCL152-1  time LCL201-1 6.45 LCL250-1  sos MSC007-1.015  time
LCL153-1  1.25 LCL202-1 2.58 LCL251-1  sos MSC007-2.002  0.11
LCL154-1  1.11 LCL203-1 2.53 LCL252-1  sos MSC007-2.003  3.10
LCL155-1  0.85 LCL204-1 6.52 LCL253-1  sos MSC007-2.004  time
LCL156-1  1.05 LCL205-1 2.62 LCL254-1  sos MSC007-2.005  time
LCL157-1  0.75 LCL206-1 2.62 LCL255-1  sos MSC007-2.006  time
LCL158-1  0.96 LCL207-1 1.92 LCL256-1  32.44 MSC007-2.007  time
LCL159-1  1.40 LCL208-1 29.96 LDA001-1  0.40 MSC007-2.008  time
LCL160-1  time LCL209-1  sos LDA002-1  2.77 MSC007-2.009  time
LCL161-1  0.35 LCL210-1 30.14 LDA003-1  0.36 MSC007-2.010  time
LCL162-1 54.96 LCL211-1 29.91 LDA004-1  time MSC007-2.011  time
LCL163-1 203.96 LCL212-1 0.10 LDA005-1  time MSC007-2.012  time
LCL164-1  1.74 LCL213-1 30.39 LDA005-2  time MSC007-2.013  time
LCL165-1  time LCL214-1 30.77 LDA006-1  time MSC007-2.014  time
LCL166-1  time LCL215-1 58.15 LDA006-2  time MSC007-2.015  time
LCL167-1  time LCL216-1 30.05 LDA007-1  47.32 MSC008-1.002 39.64
LCL168-1  time LCL217-1 29.54 LDA007-2  28.11 MSC008-1.006  time
LCL169-1  0.11 LCL218-1 19.71 LDA007-3  0.54 MSC008-1.010  time
LCL170-1  0.08 LCL219-1  sos LDA008-1  time MSC008-1.014  time
LCL171-1  0.09 LCL220-1  sos LDA008-2  time MSC008-1.018  time
LCL172-1  0.14 LCL221-1  sos LDA009-1  time MSC008-1.022  time
LCL173-1  0.18 LCL222-1  sos LDA009-2  time MSC008-2.002 26.88
LCL174-1  1.52 LCL223-1  sos LDA010-1  time NUM001-1  0.10
LCL175-1  0.12 LCL224-1  sos LDA010-2  228.65 NUM002-1  0.18
LCL176-1  0.13 LCL225-1  sos LDA011-1  time NUM003-1  0.12
LCL177-1  0.13 LCL226-1 1.52 LDA011-2  218.37 NUM004-1  0.52
LCL178-1  0.12 LCL227-1  sos LDA012-1  time NUM005-1  time
LCL179-1  sos LCL228-1  sos LDA012-2  13.81 NUM006-1  time
LCL180-1  sos LCL229-1  sos LDA013-1  0.87 NUM007-1  time
LCL181-1  sos LCL230-1  sos LDA014-1  time NUM008-1  time
LCL181-2  0.05 LCL230-2 0.04 MSC001-1  12.84 NUM009-1  48.00
LCL182-1 30.30 LCL231-1  sos MSC002-1  1.04 NUM010-1  time
LCL183-1  sos LCL232-1  sos MSC002-2  0.90 NUM011-1  time
LCL184-1  sos LCL233-1  sos MSC003-1  0.10 NUM012-1  time
LCL185-1  0.32 LCL234-1  sos MSC004-1  0.11 NUM013-1  time
LCL186-1  0.30 LCL235-1  sos MSC005-1  45.37 NUM014-1  0.07
LCL187-1  0.34 LCL236-1  sos MSC006-1  3.76 NUM015-1  0.13
LCL188-1  0.13 LCL237-1  sos MSC007-1.002  0.03 NUM016-1  0.11
LCL189-1  0.18 LCL238-1  sos MSC007-1.003  0.08 NUM016-2  0.10

NUM017-1 175.92 NUM065-1 time NUM115-1 time NUM165-1 time
NUM017-2 174.93 NUM066-1 time NUM116-1 time NUM166-1 time
NUM018-1  time NUM067-1 time NUM117-1 time NUM167-1 time
NUM019-1  0.10 NUM068-1 time NUM118-1 time NUM168-1 time
NUM020-1  0.10 NUM069-1 time NUM119-1 time NUM169-1 time
NUM021-1  0.32 NUM070-1 time NUM120-1 time NUM170-1 time
NUM022-1  0.08 NUM071-1 time NUM121-1 time NUM171-1 time
NUM023-1  0.13 NUM072-1 time NUM122-1 time NUM172-1 time
NUM024-1 30.63 NUM073-1 time NUM123-1 time NUM173-1 time
NUM025-1  0.06 NUM074-1 time NUM124-1 time NUM174-1 time
NUM025-2  0.09 NUM075-1 time NUM125-1 time NUM175-1 time
NUM026-1  time NUM076-1 time NUM126-1 time NUM176-1 time
NUM027-1  time NUM077-1 time NUM127-1 time NUM177-1 time
NUM028-1  time NUM078-1 time NUM128-1 time NUM178-1 time
NUM029-1  time NUM079-1 time NUM129-1 time NUM179-1 time
NUM030-1  time NUM080-1 time NUM130-1 time NUM180-1 8.28
NUM031-1  time NUM081-1 time NUM131-1 time NUM181-1 time
NUM032-1  time NUM082-1 time NUM132-1 time NUM182-1 time
NUM033-1  time NUM083-1 time NUM133-1 time NUM183-1 53.84
NUM034-1  time NUM084-1 time NUM134-1 time NUM184-1 time
NUM035-1  time NUM085-1 time NUM135-1 time NUM185-1 time
NUM036-1  time NUM086-1 time NUM136-1 time NUM186-1 time
NUM037-1  time NUM087-1 time NUM137-1 time NUM187-1 time
NUM038-1  time NUM088-1 time NUM138-1 time NUM188-1 time
NUM039-1  time NUM089-1 time NUM139-1 time NUM189-1 time
NUM040-1  time NUM090-1 time NUM140-1 time NUM190-1 14.55
NUM041-1  time NUM091-1 time NUM141-1 time NUM191-1 time
NUM042-1  time NUM092-1 time NUM142-1 time NUM192-1 time
NUM043-1  time NUM093-1 time NUM143-1 time NUM193-1 time
NUM044-1  time NUM094-1 time NUM144-1 time NUM194-1 time
NUM045-1  time NUM095-1 time NUM145-1 time NUM195-1 time
NUM046-1  time NUM096-1 time NUM146-1 time NUM196-1 time
NUM047-1  time NUM097-1 time NUM147-1 time NUM197-1 time
NUM048-1  time NUM098-1 time NUM148-1 time NUM198-1 time
NUM049-1  time NUM099-1 time NUM149-1 time NUM199-1 time
NUM050-1  time NUM100-1 time NUM150-1 time NUM200-1 time
NUM051-1  time NUM101-1 time NUM151-1 time NUM201-1 time
NUM052-1  time NUM102-1 time NUM152-1 time NUM202-1 time
NUM053-1  time NUM103-1 time NUM153-1 time NUM203-1 time
NUM054-1  time NUM104-1 time NUM154-1 time NUM204-1 time
NUM055-1  time NUM105-1 time NUM155-1 time NUM205-1 time
NUM056-1  time NUM106-1 time NUM156-1 time NUM206-1 time
NUM057-1  time NUM107-1 time NUM157-1 time NUM207-1 time
NUM058-1  time NUM108-1 time NUM158-1 time NUM208-1 time
NUM059-1  time NUM109-1 time NUM159-1 time NUM209-1 time
NUM060-1  time NUM110-1 time NUM160-1 time NUM210-1 time
NUM061-1  time NUM111-1 time NUM161-1 time NUM211-1 time
NUM062-1  time NUM112-1 time NUM162-1 time NUM212-1 time
NUM063-1  time NUM113-1 time NUM163-1 time NUM213-1 time
NUM064-1  time NUM114-1 time NUM164-1 time NUM214-1 time

NUM215-1 time NUM255-1  time NUM284-1.007 0.14 PUZ006-1  0.24
NUM216-1 time NUM255-2  time NUM284-1.008 0.25 PUZ007-1  0.83
NUM217-1 time NUM256-1  time NUM284-1.009 0.38 PUZ008-1  0.23
NUM218-1 time NUM256-2  time NUM284-1.010 0.83 PUZ008-2  0.42
NUM219-1 time NUM257-1  time NUM285-1  sos PUZ009-1  0.08
NUM220-1 time NUM257-2  time PLA001-1  sos PUZ010-1  time
NUM221-1 time NUM258-1  time PLA002-1  0.14 PUZ011-1  0.12
NUM222-1 time NUM258-2  time PLA002-2  time PUZ012-1  0.87
NUM223-1 time NUM259-1  time PLA003-1  0.20 PUZ013-1  0.12
NUM224-1 time NUM259-2  time PLA004-1  time PUZ014-1  0.14
NUM225-1 time NUM260-1  time PLA004-2  time PUZ015-1  time
NUM226-1 time NUM260-2  time PLA005-1  time PUZ016-1  5.69
NUM227-1 time NUM261-1  time PLA005-2  time PUZ017-1  time
NUM228-1 12.39 NUM261-2  time PLA006-1  2.25 PUZ018-1  0.21
NUM229-1 time NUM262-1  time PLA007-1  time PUZ019-1  memory
NUM230-1 time NUM262-2  time PLA008-1  time PUZ020-1  0.16
NUM231-1 time NUM263-1  time PLA009-1  time PUZ021-1  time
NUM232-1 time NUM263-2  time PLA009-2  time PUZ022-1  0.24
NUM233-1 time NUM264-1  time PLA010-1  time PUZ023-1  0.29
NUM234-1 time NUM264-2  time PLA011-1  time PUZ024-1  0.24
NUM235-1 time NUM265-1  time PLA011-2  time PUZ025-1  1.00
NUM236-1 time NUM266-1  time PLA012-1  time PUZ026-1  20.02
NUM237-1 time NUM267-1  time PLA013-1  time PUZ027-1  1.99
NUM238-1 time NUM268-1  time PLA014-1  time PUZ028-1  sos
NUM239-1 time NUM269-1  time PLA014-2  time PUZ028-2  sos
NUM240-1 time NUM270-1  time PLA015-1  time PUZ028-3  time
NUM241-1 time NUM271-1  time PLA016-1  time PUZ028-4  time
NUM242-1 time NUM272-1  time PLA017-1  2.10 PUZ029-1  0.11
NUM243-1 time NUM273-1  time PLA018-1  time PUZ030-0  1.05
NUM244-1 time NUM274-1  time PLA019-1  time PUZ030-1  48.76
NUM245-1 time NUM275-1  time PLA020-1  0.30 PUZ031-1  0.50
NUM245-2 time NUM276-1  time PLA021-1  time PUZ032-1  0.17
NUM246-1 time NUM277-1  time PLA022-1  time PUZ033-1  0.10
NUM246-2 time NUM278-1  time PLA022-2  time PUZ034-1.002  time
NUM247-1 time NUM279-1  time PLA023-1  time PUZ034-1.003  time
NUM247-2 time NUM279-2  time PRV001-1  0.61 PUZ034-1.004  time
NUM248-1 time NUM280-1  time PRV002-1  2.37 PUZ034-1.005  time
NUM248-2 time NUM281-1  time PRV003-1  0.19 PUZ034-1.006  time
NUM249-1 time NUM282-1  time PRV004-1  time PUZ034-1.007  time
NUM249-2 time NUM283-1.002 0.09 PRV005-1  2.11 PUZ034-1.008  time
NUM250-1 time NUM283-1.003 0.14 PRV006-1  0.22 PUZ034-1.009  time
NUM250-2 time NUM283-1.004 0.77 PRV007-1  time PUZ034-1.010  time
NUM251-1 time NUM283-1.005 34.23 PRV008-1  1.71 RNG001-1  40.66
NUM251-2 time NUM283-1.006 term PRV009-1  0.16 RNG001-2  8.24
NUM252-1 time NUM283-1.007 term PUZ001-1  0.12 RNG001-3  100.56
NUM252-2 time NUM284-1.002 0.09 PUZ001-2  0.38 RNG001-4  21.61
NUM253-1 time NUM284-1.003 0.09 PUZ002-1  0.13 RNG001-5  40.70
NUM253-2 time NUM284-1.004 0.09 PUZ003-1  0.11 RNG002-1  1.17
NUM254-1 time NUM284-1.005 0.13 PUZ004-1  0.08 RNG003-1  0.87
NUM254-2 time NUM284-1.006 0.16 PUZ005-1  1.81 RNG004-1  24.25

RNG004-2 35.25 RNG026-7  time ROB007-1  time SET015-3  time
RNG004-3  5.53 RNG027-1  time ROB007-2  time SET015-4  time
RNG005-1  5.14 RNG027-2  0.18 ROB007-3  time SET016-1  time
RNG005-2  1.02 RNG027-5  time ROB007-4  time SET016-3  time
RNG006-1 59.29 RNG027-6  time ROB008-1  0.30 SET016-6  time
RNG006-2  8.89 RNG027-7  time ROB009-1  0.46 SET016-7  time
RNG006-3 14.05 RNG027-8  time ROB010-1  0.22 SET017-3  time
RNG007-1 14.19 RNG027-9  time ROB011-1  0.52 SET017-4  time
RNG007-4  0.28 RNG028-1  time ROB012-1  time SET017-6 107.89
RNG007-5  time RNG028-2  0.12 ROB012-2  time SET017-7 242.95
RNG008-1 166.41 RNG028-5  time ROB013-1  0.19 SET018-1  time
RNG008-2 209.00 RNG028-6  time ROB014-1  time SET018-3  time
RNG008-3  2.12 RNG028-7  time ROB014-2 358.48 SET018-4  time
RNG008-4  1.94 RNG028-8  time ROB015-1  time SET018-6  time
RNG008-5 121.48 RNG028-9  time ROB015-2  time SET018-7  time
RNG008-6 213.42 RNG029-1  time ROB016-1  0.76 SET019-3 34.67
RNG008-7  2.82 RNG029-2  0.13 ROB017-1  time SET019-4 29.49
RNG009-5  time RNG029-5  time ROB018-1  time SET020-3  time
RNG009-7  time RNG029-6  time ROB019-1  time SET020-4  time
RNG010-1  0.26 RNG029-7  time ROB020-1  time SET020-6  time
RNG010-2  0.16 RNG030-6  time ROB020-2  time SET020-7  time
RNG010-5  time RNG030-7  time ROB021-1  2.62 SET021-3  time
RNG010-6  time RNG031-6  time ROB022-1  3.85 SET021-4  time
RNG010-7  time RNG031-7  time ROB023-1  2.81 SET021-6  time
RNG011-5  0.15 RNG032-6  time ROB024-1  time SET021-7  time
RNG012-6  0.50 RNG032-7  time ROB025-1 525.69 SET022-3  time
RNG013-6  0.44 RNG033-6  time SET001-1  0.08 SET022-4  time
RNG014-6  0.36 RNG033-7  time SET002-1 32.00 SET023-3  time
RNG015-6  0.40 RNG033-8  time SET003-1  0.16 SET023-4  time
RNG016-6  1.62 RNG033-9  time SET004-1  0.22 SET024-3  5.23
RNG017-6  0.56 RNG034-1  time SET005-1  time SET024-4  3.45
RNG018-6  0.33 RNG035-7  time SET006-1  0.16 SET024-6  1.23
RNG019-6  1.92 RNG036-7 memory SET007-1  time SET024-7  1.92
RNG019-7  1.92 RNG037-1  5.03 SET008-1  5.46 SET025-3  3.37
RNG020-6  1.94 RNG037-2  0.99 SET009-1  3.39 SET025-4  2.36
RNG020-7  1.83 RNG038-1  1.01 SET010-1  time SET025-6  2.24
RNG021-6  1.95 RNG038-2  1.05 SET011-1  time SET025-7  3.64
RNG021-7  1.82 RNG039-1  12.07 SET012-1  time SET025-8  time
RNG023-6  1.82 RNG039-2  13.26 SET012-2  time SET025-9  time
RNG023-7  1.61 RNG040-1  1.27 SET012-3  time SET027-3  time
RNG024-6  1.91 RNG040-2  1.74 SET012-4 261.14 SET027-4  time
RNG024-7  1.76 RNG041-1  3.62 SET013-1  time SET027-6  4.38
RNG025-1  time ROB001-1  time SET013-2  time SET027-7  4.49
RNG025-4 104.79 ROB002-1  0.37 SET013-3  time SET028-3  time
RNG025-5 156.93 ROB003-1  0.46 SET013-4  time SET028-4  time
RNG025-6 106.48 ROB004-1  2.23 SET014-2  time SET029-3  time
RNG025-7 160.81 ROB005-1  69.61 SET014-3  time SET029-4  time
RNG025-8  time ROB006-1  time SET014-4  time SET030-3  time
RNG025-9  time ROB006-2  time SET015-1  time SET030-4  time
RNG026-6  time ROB006-3  time SET015-2  time SET030-6  time

SET031-3  time SET058-6  1.59 SET083-6 165.21 SET110-6  time
SET031-4  time SET058-7  1.74 SET083-7 334.27 SET110-7  time
SET032-3  time SET059-6  1.72 SET084-6  9.19 SET111-6  time
SET032-4  time SET059-7  1.80 SET084-7 55.09 SET111-7  time
SET032-6  time SET060-6  4.03 SET085-6 194.03 SET112-6  time
SET033-3  time SET060-7  6.06 SET085-7  time SET112-7  time
SET033-4  time SET061-6 105.25 SET086-6  time SET113-6  time
SET033-6  time SET061-7 11.32 SET086-7  time SET113-7  time
SET034-3  time SET062-6 40.16 SET087-6  time SET114-6  time
SET034-4  time SET062-7  1.35 SET087-7  time SET114-7  time
SET034-6  time SET063-6 39.25 SET088-6  time SET115-6  time
SET035-3  time SET063-7  1.33 SET088-7  time SET115-7  time
SET035-4  time SET064-6 160.42 SET089-6  time SET116-6  time
SET035-6  time SET064-7 15.83 SET089-7  time SET116-7  time
SET036-3  time SET065-6  1.31 SET090-6  time SET117-6  9.46
SET036-4  time SET065-7  1.47 SET090-7  time SET117-7 72.45
SET036-6  time SET066-6  time SET091-6  time SET118-6  1.52
SET037-3  time SET066-7  time SET091-7  time SET118-7  3.49
SET037-4  time SET067-6  time SET092-6  time SET119-6  time
SET037-6  time SET067-7  time SET092-7  time SET119-7  time
SET038-3  time SET068-6  time SET093-6  9.60 SET120-6  time
SET038-4  time SET068-7  time SET093-7 97.55 SET120-7  time
SET038-6  time SET069-6  time SET094-6 132.69 SET121-6  time
SET039-3  time SET069-7  time SET094-7 76.45 SET121-7  time
SET039-4  time SET070-6  time SET095-6  time SET122-6  time
SET040-3  time SET070-7  time SET095-7  2.06 SET122-7  time
SET040-4  time SET071-6  time SET096-6  time SET123-6  time
SET040-6  time SET071-7  time SET096-7 40.34 SET124-6  time
SET041-3  time SET072-6 230.01 SET097-6  time SET125-6  time
SET041-4  time SET072-7 485.58 SET097-7  time SET126-6  time
SET041-6  time SET073-6 104.43 SET098-6  time SET127-6  time
SET042-3  time SET073-7  2.67 SET098-7  time SET128-6  time
SET042-4  time SET074-6 104.72 SET099-6  time SET129-6  time
SET043-5  0.06 SET074-7  2.52 SET099-7  time SET130-6  time
SET044-5  0.07 SET075-6 83.70 SET100-6  time SET131-6  time
SET045-5  0.08 SET075-7  2.45 SET100-7  time SET132-6  time
SET046-5  0.06 SET076-6  time SET101-6  2.13 SET133-6  time
SET047-5  1.14 SET076-7  time SET101-7  3.57 SET134-6  time
SET050-6  8.47 SET077-6  0.78 SET102-6  2.27 SET135-6  time
SET051-6  8.12 SET077-7  0.99 SET102-7  3.54 SET136-6  time
SET052-6 10.21 SET078-6  1.38 SET103-6  time SET137-6  time
SET053-6  9.92 SET078-7  1.84 SET103-7  time SET138-6  time
SET054-6  0.86 SET079-6 121.92 SET104-6  time SET139-6  time
SET054-7  0.93 SET079-7  2.57 SET104-7  time SET140-6  time
SET055-6 99.04 SET080-6  1.29 SET105-6  time SET141-6  time
SET055-7  1.02 SET080-7  1.70 SET105-7  time SET142-6  time
SET056-6 150.44 SET081-6  1.43 SET108-6  7.20 SET143-6  time
SET056-7 156.83 SET081-7  2.62 SET108-7 48.50 SET144-6  time
SET057-6  1.56 SET082-6 169.62 SET109-6  time SET145-6  time
SET057-7  1.67 SET082-7 113.95 SET109-7  time SET146-6 186.67

SET147-6  time SET197-6 159.97 SET247-6 time SET297-6 time
SET148-6  time SET198-6  time SET248-6 time SET298-6 time
SET149-6  time SET199-6  time SET249-6 time SET299-6 time
SET150-6  time SET200-6  time SET250-6 time SET300-6 time
SET151-6  time SET201-6  time SET251-6 time SET301-6 time
SET152-6  8.03 SET202-6  time SET252-6 time SET302-6 time
SET153-6  time SET203-6  1.78 SET253-6 time SET303-6 time
SET154-6  time SET204-6  9.38 SET254-6 time SET304-6 time
SET155-6  time SET205-6  time SET255-6 time SET305-6 time
SET156-6  time SET206-6  time SET256-6 time SET306-6 time
SET157-6  time SET207-6  time SET257-6 time SET307-6 time
SET158-6  1.88 SET208-6  time SET258-6 time SET308-6 time
SET159-6  time SET209-6  time SET259-6 time SET309-6 time
SET160-6  time SET210-6  time SET260-6 time SET310-6 time
SET161-6  time SET211-6  time SET261-6 time SET311-6 time
SET162-6  time SET212-6  time SET262-6 time SET312-6 time
SET163-6  time SET213-6  time SET263-6 time SET313-6 time
SET164-6  time SET214-6  time SET264-6 time SET314-6 time
SET165-6  time SET215-6  time SET265-6 time SET315-6 time
SET166-6 122.14 SET216-6  time SET266-6 time SET316-6 time
SET167-6  time SET217-6  time SET267-6 time SET317-6 time
SET168-6  time SET218-6  time SET268-6 time SET318-6 time
SET169-6  time SET219-6  time SET269-6 time SET319-6 time
SET170-6  time SET220-6  time SET270-6 time SET320-6 time
SET171-6  time SET221-6  time SET271-6 time SET321-6 time
SET172-6  time SET222-6  time SET272-6 time SET322-6 time
SET173-6  time SET223-6  time SET273-6 time SET323-6 time
SET174-6  time SET224-6  time SET274-6 time SET324-6 time
SET175-6  time SET225-6  time SET275-6 time SET325-6 time
SET176-6  time SET226-6  time SET276-6 time SET326-6 time
SET177-6  time SET227-6  time SET277-6 time SET327-6 time
SET178-6  time SET228-6  time SET278-6 time SET328-6 time
SET179-6  time SET229-6  time SET279-6 time SET329-6 time
SET180-6  time SET230-6  time SET280-6 time SET330-6 time
SET181-6  time SET231-6  time SET281-6 time SET331-6 time
SET182-6  time SET232-6  time SET282-6 time SET332-6 time
SET183-6  time SET233-6  time SET283-6 time SET333-6 time
SET184-6  5.62 SET234-6  time SET284-6 time SET334-6 time
SET185-6  time SET235-6 40.36 SET285-6 time SET335-6 time
SET186-6  time SET236-6 41.07 SET286-6 time SET336-6 time
SET187-6  time SET237-6  time SET287-6 time SET337-6 time
SET188-6  time SET238-6  time SET288-6 time SET338-6 time
SET189-6  time SET239-6  time SET289-6 time SET339-6 time
SET190-6  time SET240-6  time SET290-6 time SET340-6 time
SET191-6  time SET241-6  time SET291-6 time SET341-6 time
SET192-6  time SET242-6  2.00 SET292-6 time SET342-6 time
SET193-6  time SET243-6  time SET293-6 time SET343-6 time
SET194-6  time SET244-6  time SET294-6 time SET344-6 time
SET195-6  time SET245-6  time SET295-6 time SET345-6 time
SET196-6 159.58 SET246-6  time SET296-6 0.95 SET346-6 time

SET347-6 time SET397-6 time SET447-6  time SET497-6  time
SET348-6 time SET398-6 time SET448-6  time SET498-6  time
SET349-6 time SET399-6 time SET449-6  time SET499-6  time
SET350-6 time SET400-6 time SET450-6  time SET500-6  time
SET351-6 time SET401-6 time SET451-6  time SET501-6  time
SET352-6 time SET402-6 time SET452-6  time SET502-6  time
SET353-6 time SET403-6 time SET453-6  time SET503-6  time
SET354-6 time SET404-6 time SET454-6  time SET504-6  time
SET355-6 time SET405-6 time SET455-6  time SET505-6  time
SET356-6 time SET406-6 time SET456-6  time SET506-6 53.41
SET357-6 time SET407-6 time SET457-6  time SET507-6 100.37
SET358-6 time SET408-6 time SET458-6  time SET508-6  time
SET359-6 time SET409-6 time SET459-6  time SET509-6  time
SET360-6 time SET410-6 time SET460-6  time SET510-6 187.26
SET361-6 time SET411-6 62.99 SET461-6  time SET511-6  time
SET362-6 time SET412-6 time SET462-6  time SET512-6  time
SET363-6 time SET413-6 time SET463-6  time SET513-6  time
SET364-6 time SET414-6 time SET464-6  time SET514-6  time
SET365-6 time SET415-6 time SET465-6  time SET515-6  time
SET366-6 time SET416-6 time SET466-6  time SET516-6 510.68
SET367-6 time SET417-6 time SET467-6  time SET517-6 560.16
SET368-6 time SET418-6 time SET468-6  time SET518-6  time
SET369-6 time SET419-6 time SET469-6  time SET519-6  time
SET370-6 time SET420-6 time SET470-6  time SET520-6  time
SET371-6 time SET421-6 time SET471-6  time SET521-6  time
SET372-6 time SET422-6 time SET472-6  time SET522-6  time
SET373-6 time SET423-6 time SET473-6  time SET523-6  time
SET374-6 time SET424-6 time SET474-6  time SET524-6  time
SET375-6 time SET425-6 time SET475-6  time SET525-6  time
SET376-6 time SET426-6 time SET476-6  time SET526-6  time
SET377-6 time SET427-6 time SET477-6  time SET527-6  time
SET378-6 time SET428-6 time SET478-6  time SET528-6  time
SET379-6 time SET429-6 time SET479-6 220.02 SET529-6  time
SET380-6 time SET430-6 time SET480-6  time SET530-6  time
SET381-6 time SET431-6 time SET481-6  time SET531-6  time
SET382-6 time SET432-6 time SET482-6  time SET532-6  time
SET383-6 time SET433-6 time SET483-6  time SET533-6  time
SET384-6 time SET434-6 time SET484-6  time SET534-6  time
SET385-6 time SET435-6 time SET485-6  time SET535-6  time
SET386-6 time SET436-6 time SET486-6  time SET536-6  time
SET387-6 time SET437-6 time SET487-6  time SET537-6  time
SET388-6 time SET438-6 time SET488-6  time SET538-6  time
SET389-6 time SET439-6 time SET489-6  time SET539-6  time
SET390-6 time SET440-6 time SET490-6  time SET540-6  time
SET391-6 time SET441-6 time SET491-6  time SET541-6  time
SET392-6 time SET442-6 time SET492-6  time SET542-6  time
SET393-6 time SET443-6 time SET493-6  time SET543-6  time
SET394-6 time SET444-6 time SET494-6  time SET544-6  time
SET395-6 time SET445-6 time SET495-6  time SET545-6  time
SET396-6 time SET446-6 time SET496-6  time SET546-6  time

SET547-6  time SYN002-1.050 84.94 SYN014-1  time SYN072-1  0.16
SET548-6  time SYN003-1.002 0.05 SYN014-2  0.19 SYN073-1  0.05
SET549-6  time SYN003-1.003 0.09 SYN015-1  time SYN074-1  13.12
SET550-6  time SYN003-1.004 0.09 SYN015-2 248.84 SYN075-1  2.84
SET551-6  time SYN003-1.005 0.12 SYN028-1  0.05 SYN076-1  time
SET552-6  time SYN003-1.006 0.13 SYN029-1  0.04 SYN077-1  time
SET553-6  582.27 SYN003-1.007 0.15 SYN030-1  0.07 SYN078-1  term
SET554-6  time SYN003-1.008 0.16 SYN031-1  0.10 SYN079-1  0.04
SET555-6  time SYN003-1.009 0.22 SYN032-1  0.07 SYN080-1  0.08
SET556-6  time SYN003-1.010 0.21 SYN033-1  0.05 SYN081-1  0.06
SET557-6  time SYN004-1.002 0.05 SYN034-1  0.07 SYN082-1  0.14
SET558-6  1.66 SYN004-1.003 0.06 SYN035-1  0.04 SYN083-1  0.04
SET559-6  374.72 SYN004-1.004 0.08 SYN036-1  time SYN084-1  sos
SET560-6  time SYN004-1.005 0.08 SYN036-2  time SYN085-1.005  0.04
SET561-6  386.50 SYN004-1.006 0.10 SYN036-3  2.50 SYN085-1.010  0.10
SET562-6  532.91 SYN004-1.007 0.12 SYN036-4  time SYN085-1.020  0.10
SET563-6  149.57 SYN004-1.008 0.11 SYN037-1 48.20 SYN086-1.005  sos
SET564-6  125.46 SYN004-1.009 0.10 SYN037-2  0.38 SYN086-1.010  sos
SET565-6  366.31 SYN004-1.010 0.17 SYN038-1  2.58 SYN086-1.020  sos
SET566-6  148.61 SYN005-1.002 0.07 SYN039-1  1.67 SYN087-1.005  sos
SET567-6  time SYN005-1.003 0.07 SYN040-1  0.05 SYN087-1.010  sos
SET568-6  time SYN005-1.004 0.05 SYN041-1  0.03 SYN087-1.020  sos
SET569-6  time SYN005-1.005 0.08 SYN044-1  0.08 SYN088-1.005  0.10
SET570-6  time SYN005-1.006 0.08 SYN045-1  0.05 SYN088-1.010  0.79
SET571-6  time SYN005-1.007 0.07 SYN046-1  0.04 SYN088-1.020 memory
SET572-6  time SYN005-1.008 0.10 SYN047-1  0.04 SYN089-1.005  0.45
SYN001-1.001  0.04 SYN005-1.009 0.10 SYN048-1  0.03 SYN089-1.010  2.83
SYN001-1.002  0.04 SYN005-1.010 0.09 SYN049-1  0.06 SYN089-1.020  27.12
SYN001-1.003  0.12 SYN006-1  0.08 SYN050-1  0.05 SYN090-1.005  0.35
SYN001-1.004  0.13 SYN007-1.001 0.03 SYN051-1  0.08 SYN090-1.010  0.83
SYN001-1.005  0.34 SYN007-1.002 0.03 SYN052-1  0.04 SYN090-1.020  1.95
SYN001-1.006  0.97 SYN007-1.003 0.16 SYN053-1  0.06 SYN091-1.005  sos
SYN001-1.007  3.04 SYN007-1.004 0.79 SYN054-1  0.07 SYN091-1.010  time
SYN001-1.008 13.18 SYN007-1.005 3.61 SYN055-1  0.10 SYN091-1.020  time
SYN001-1.009 72.00 SYN007-1.006 17.09 SYN056-1  sos SYN092-1.005  sos
SYN001-1.010 587.64 SYN007-1.007 80.17 SYN057-1  0.04 SYN092-1.010  sos
SYN001-1.011  time SYN008-1  0.06 SYN058-1  0.06 SYN092-1.020  time
SYN001-1.012  time SYN009-1  0.10 SYN059-1  sos SYN093-1.005  1.21
SYN001-1.013  time SYN010-1.002 0.06 SYN060-1  0.04 SYN093-1.010  11.93
SYN002-1.000  0.02 SYN010-1.005 0.10 SYN061-1  0.04 SYN093-1.020 179.61
SYN002-1.002  0.05 SYN010-1.010 0.33 SYN062-1  0.07 SYN094-1.005  0.85
SYN002-1.004  0.08 SYN010-2.002 0.09 SYN063-1  0.08 SYN094-1.010  2.43
SYN002-1.006  0.12 SYN010-2.005 0.27 SYN064-1  0.02 SYN094-1.020  7.85
SYN002-1.008  0.25 SYN010-2.010 1.13 SYN065-1  0.07 SYN095-1.005  0.55
SYN002-1.010  0.31 SYN010-3.002 0.15 SYN066-1  0.05 SYN095-1.010  3.01
SYN002-1.012  1.16 SYN010-3.005 0.60 SYN067-1  time SYN095-1.020  20.86
SYN002-1.016  2.12 SYN010-3.010 2.71 SYN068-1  0.07 SYN096-1.005  0.45
SYN002-1.020  3.82 SYN011-1  0.05 SYN069-1  0.10 SYN096-1.010  0.98
SYN002-1.030 12.17 SYN012-1  2.05 SYN070-1  0.16 SYN096-1.020  2.24
SYN002-1.040 31.06 SYN013-1  time SYN071-1  0.07 SYN097-1.005  3.55

SYN097-1.010  42.19 SYN124-1 2.92 SYN174-1 2.85 SYN224-1 2.97
SYN097-1.020  time SYN125-1 3.64 SYN175-1 2.86 SYN225-1 4.14
SYN098-1.005  2.33 SYN126-1 3.40 SYN176-1 2.87 SYN226-1 2.82
SYN098-1.010  6.93 SYN127-1 3.49 SYN177-1 3.51 SYN227-1 3.70
SYN098-1.020  26.23 SYN128-1 3.58 SYN178-1 4.36 SYN228-1 3.87
SYN099-1.005  1.11 SYN129-1 3.70 SYN179-1 3.53 SYN229-1 2.91
SYN099-1.010  7.22 SYN130-1 2.56 SYN180-1 4.29 SYN230-1 2.89
SYN099-1.020  69.57 SYN131-1 2.54 SYN181-1 3.76 SYN231-1 2.90
SYN100-1.005  0.90 SYN132-1 2.51 SYN182-1 3.53 SYN232-1 2.83
SYN100-1.010  2.19 SYN133-1 2.50 SYN183-1 3.30 SYN233-1 2.90
SYN100-1.020  5.37 SYN134-1 2.90 SYN184-1 2.48 SYN234-1 3.98
SYN101-1.005  6.79 SYN135-1 2.90 SYN185-1 2.44 SYN235-1 3.90
SYN101-1.010  34.41 SYN136-1 2.85 SYN186-1 2.97 SYN236-1 2.82
SYN101-1.020 215.82 SYN137-1 3.01 SYN187-1 2.98 SYN237-1 2.59
SYN101-2.005  time SYN138-1 3.27 SYN188-1 3.17 SYN238-1 2.55
SYN101-2.010 memory SYN139-1 4.65 SYN189-1 3.23 SYN239-1 2.59
SYN101-2.020  sos SYN140-1 4.48 SYN190-1 3.43 SYN240-1 2.57
SYN101-3.005  time SYN141-1 3.61 SYN191-1 3.31 SYN241-1 2.57
SYN101-3.010  time SYN142-1 4.56 SYN192-1 3.46 SYN242-1 2.56
SYN101-3.020  time SYN143-1 4.50 SYN193-1 3.56 SYN243-1 2.68
SYN102-1.005  4.83 SYN144-1 4.61 SYN194-1 3.49 SYN244-1 2.64
SYN102-1.010  11.04 SYN145-1 2.44 SYN195-1 3.47 SYN245-1 2.63
SYN102-1.020  23.88 SYN146-1 2.51 SYN196-1 2.75 SYN246-1 2.65
SYN102-2.005  time SYN147-1 2.74 SYN197-1 2.63 SYN247-1 2.58
SYN102-2.010  time SYN148-1 3.17 SYN198-1 2.70 SYN248-1 2.82
SYN102-2.020  time SYN149-1 2.52 SYN199-1 2.72 SYN249-1 2.84
SYN102-3.005 memory SYN150-1 3.15 SYN200-1 2.81 SYN250-1 4.10
SYN102-3.010 memory SYN151-1 3.05 SYN201-1 3.74 SYN251-1 2.91
SYN102-3.020 memory SYN152-1 3.02 SYN202-1 4.38 SYN252-1 4.44
SYN103-1  2.55 SYN153-1 3.60 SYN203-1 3.44 SYN253-1 4.60
SYN104-1  2.44 SYN154-1 3.43 SYN204-1 4.45 SYN254-1 4.62
SYN105-1  2.66 SYN155-1 3.63 SYN205-1 4.40 SYN255-1 3.13
SYN106-1  2.63 SYN156-1 5.06 SYN206-1 3.93 SYN256-1 3.08
SYN107-1  3.18 SYN157-1 3.59 SYN207-1 3.37 SYN257-1 2.50
SYN108-1  3.00 SYN158-1 3.70 SYN208-1 3.53 SYN258-1 2.51
SYN109-1  3.06 SYN159-1 4.13 SYN209-1 3.40 SYN259-1 2.58
SYN110-1  4.07 SYN160-1 3.47 SYN210-1 3.40 SYN260-1 2.49
SYN111-1  3.12 SYN161-1 3.59 SYN211-1 3.30 SYN261-1 2.60
SYN112-1  2.80 SYN162-1 3.63 SYN212-1 3.23 SYN262-1 3.00
SYN113-1  3.24 SYN163-1 4.26 SYN213-1 3.51 SYN263-1 3.87
SYN114-1  2.52 SYN164-1 2.48 SYN214-1 3.47 SYN264-1 3.26
SYN115-1  3.65 SYN165-1 2.61 SYN215-1 3.52 SYN265-1 2.90
SYN116-1  3.34 SYN166-1 4.52 SYN216-1 2.74 SYN266-1 4.20
SYN117-1  3.48 SYN167-1 2.59 SYN217-1 2.68 SYN267-1 3.49
SYN118-1  2.52 SYN168-1 2.94 SYN218-1 2.76 SYN268-1 3.51
SYN119-1  2.48 SYN169-1 2.95 SYN219-1 2.96 SYN269-1 4.31
SYN120-1  2.56 SYN170-1 3.43 SYN220-1 2.95 SYN270-1 4.08
SYN121-1  2.88 SYN171-1 4.20 SYN221-1 2.95 SYN271-1 4.12
SYN122-1  2.90 SYN172-1 2.54 SYN222-1 2.94 SYN272-1 3.98
SYN123-1  2.79 SYN173-1 2.87 SYN223-1 2.85 SYN273-1 3.56

SYN274-1 2.50 SYN287-1 2.52 SYN300-1 3.79 TOP007-1 time
SYN275-1 2.56 SYN288-1 2.55 SYN301-1 3.32 TOP008-1 time
SYN276-1 2.43 SYN289-1 2.84 TOP001-1 time TOP009-1 time
SYN277-1 2.53 SYN290-1 2.70 TOP001-2 time TOP010-1 time
SYN278-1 2.56 SYN291-1 2.47 TOP002-1 time TOP011-1 time
SYN279-1 2.91 SYN292-1 2.48 TOP002-2 0.08 TOP012-1 time
SYN280-1 2.52 SYN293-1 2.78 TOP003-1 time TOP013-1 time
SYN281-1 2.75 SYN294-1 2.76 TOP003-2 time TOP014-1 time
SYN282-1 2.45 SYN295-1 2.49 TOP004-1 1.25 TOP015-1 time
SYN283-1 2.60 SYN296-1 2.64 TOP004-2 0.29 TOP016-1 time
SYN284-1 2.83 SYN297-1 2.56 TOP005-1 time TOP017-1 time
SYN285-1 3.30 SYN298-1 3.80 TOP005-2 0.52 TOP018-1 time
SYN286-1 2.71 SYN299-1 3.73 TOP006-1 time TOP019-1 time

References

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

[2] C.B. Suttner and G. Sutcliffe. The TPTP Problem Library (TPTP v1.1.1 - TR Date 7.7.94). Technical Report AR-94-03, Institut für Informatik, Technische Universität München, Munich, Germany; Technical Report 93/11, Department of Computer Science, James Cook University, Townsville, Australia, 1994.