Next: Settings and Set of
Up: An Entry in the Contest
Previous: Introduction
Otter and ROO proved all seven theorems in the basic set and the
first five of the ten problems in the equality set.
See Section 3 for the options settings and set of suport used.
Tables 1 and 2 list the results on the two sets for Otter, for ROO
running with 8 processors, and for ROO with 12 processors.
The Otter jobs were run on SPARCstation 2. We used Otter 2.2, the version
that was released in July 1991.
The ROO jobs were run on an Alliant FX/2800 with 12 (Intel i860) processors.
The version of ROO we used is based on Otter 2.2xa+ (June 1992).
Table:
Results for Basic Theorems
| |
Otter |
ROO-8 |
ROO-12 |
| Theorem 1: x2=e Group |
| proof time |
0.20 |
0.32 |
0.32 |
| generated |
222 |
2300 |
1867 |
| kept |
13 |
30 |
40 |
| memory (K) |
31 |
728 |
564 |
| Theorem 2: Commutator |
| proof time |
35.60 |
26.89 |
25.97 |
| generated |
20575 |
88838 |
131429 |
| kept |
4505 |
3684 |
1697 |
| memory (K) |
1564 |
12515 |
12670 |
| Theorem 3: x2=x Ring |
| proof time |
145.41 |
35.57 |
38.18 |
| generated |
56025 |
134744 |
221890 |
| kept |
13990 |
4316 |
2736 |
| memory (K) |
4342 |
14333 |
18739 |
| Theorem 4: XGK |
| proof time |
407.50 |
159.87 |
55.37 |
| generated |
177109 |
663722 |
263233 |
| kept |
15320 |
16519 |
9466 |
| memory (K) |
8047 |
19539 |
22189 |
| Theorem 5: Imp-4 (CD-67) |
| proof time |
7711.98 |
1051.55 |
909.95 |
| generated |
8341570 |
7171447 |
8182376 |
| kept |
17862 |
14855 |
17666 |
| memory (K) |
10729 |
13983 |
15098 |
| Theorem 6: MV-1 (CD-57) |
| proof time |
17.68 |
4.37 |
14.71 |
| generated |
16687 |
24159 |
114051 |
| kept |
4837 |
1024 |
2000 |
| memory (K) |
2171 |
6479 |
12161 |
| Theorem 7: MV-2 (CD-60) |
| proof time |
2184.96 |
427.89 |
152.53 |
| generated |
3214280 |
4311090 |
1997084 |
| kept |
16250 |
12374 |
10750 |
| memory (K) |
7216 |
13664 |
13755 |
|
Table:
Results for Equality Problems
| |
Otter |
ROO-8 |
ROO-12 |
| Theorem EQ-1: Commutator |
| proof time |
1.49 |
0.76 |
0.86 |
| generated |
542 |
1727 |
2144 |
| kept |
114 |
91 |
89 |
| memory (K) |
255 |
1208 |
1460 |
| Theorem EQ-2: Robbins, c+c=c |
| proof time |
98.19 |
18.63 |
13.43 |
| generated |
50001 |
56067 |
59151 |
| kept |
4548 |
2450 |
1235 |
| memory (K) |
5652 |
12676 |
13342 |
| Theorem EQ-3: TBA |
| proof time |
16.78 |
4.10 |
3.16 |
| generated |
3945 |
9307 |
11170 |
| kept |
1030 |
620 |
378 |
| memory (K) |
1564 |
4880 |
5043 |
| Theorem EQ-4: Group single axiom |
| proof time |
44.12 |
10.56 |
9.25 |
| generated |
3417 |
11778 |
16118 |
| kept |
2507 |
1015 |
863 |
| memory (K) |
4470 |
13889 |
17110 |
| Theorem EQ-5: Wajsberg algebra |
| proof time |
2248.86 |
425.99 |
491.67 |
| generated |
1012625 |
971543 |
1437272 |
| kept |
5897 |
4374 |
4022 |
| memory (K) |
6801 |
13376 |
14525 |
|
Next: Settings and Set of
Up: An Entry in the Contest
Previous: Introduction
Karen D. Toonen
1998-11-18