----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Thu Jun 4 17:31:43 1992
The command was "otter22".
set(knuth_bendix).
set(index_for_back_demod).
set(process_input).
assign(max_mem,16000).
set(control_memory).
set(lex_rpo).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
lex([a,b,T,i(x,x),n(x)]).
lrpo_lr_status([i(x,x)]).
list(usable).
0 [] (x = x).
end_of_list.
list(sos).
0 [] (i(T,x) = x).
0 [] (i(i(x,y),i(i(y,z),i(x,z))) = T).
0 [] (i(i(x,y),y) = i(i(y,x),x)).
0 [] (i(i(n(x),n(y)),i(y,x)) = T).
0 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T).
end_of_list.
OTTER sets dynamic_demod_all, because knuth_bendix is set.
OTTER clears para_into_right, because knuth_bendix is set.
OTTER sets back_demod, because knuth_bendix is set.
OTTER sets para_from, because knuth_bendix is set.
OTTER sets para_into, because knuth_bendix is set.
OTTER clears para_from_right, because knuth_bendix is set.
OTTER sets dynamic_demod, because back_demod is set.
OTTER sets order_eq, because dynamic_demod is set.
------------> process usable:
** KEPT: 1 [] (x = x).
++++ cannot make into demodulator: 1 [] (x = x).
------------> process sos:
** KEPT: 2 [] (i(T,x) = x).
** KEPT: 4 [] (i(i(x,y),i(i(y,z),i(x,z))) = T).
** KEPT: 6 [] (i(i(x,y),y) = i(i(y,x),x)).
++++ cannot make into demodulator: 6 [] (i(i(x,y),y) = i(i(y,x),x)).
** KEPT: 7 [] (i(i(n(x),n(y)),i(y,x)) = T).
** KEPT: 9 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T).
------------> done processing input.
Resetting weight limit to 15.
----> UNIT CONFLICT at 2248.86 sec ----> 11462 [binary,11460,11350] .
Level of proof is 37, length is 85.
---------------- PROOF ----------------
3,2 [] (i(T,x) = x).
4 [] (i(i(x,y),i(i(y,z),i(x,z))) = T).
6 [] (i(i(x,y),y) = i(i(y,x),x)).
7 [] (i(i(n(x),n(y)),i(y,x)) = T).
9 [] (i(i(i(a,b),i(b,a)),i(b,a)) != T).
10 [para_into,6,6] (i(i(i(x,y),y),x) = i(i(x,i(y,x)),i(y,x))).
12 [para_into,6,2] (i(i(x,T),T) = i(x,x)).
21 [para_into,7,2] (i(i(n(x),n(T)),x) = T).
23 [para_from,7,6,demod,3] (i(i(i(x,y),i(n(y),n(x))),i(n(y),n(x))) = i(x,y)).
25 [para_into,21,6] (i(i(n(T),n(n(T))),n(n(T))) = T).
31 [para_from,21,6,demod,3] (i(i(x,i(n(x),n(T))),i(n(x),n(T))) = x).
35 [para_from,25,6,demod,3] (i(i(n(n(T)),i(n(T),n(n(T)))),i(n(T),n(n(T)))) = n(n(T))).
49 [para_into,4,2,demod,3] (i(x,i(i(x,y),y)) = T).
63 [para_into,4,2] (i(i(x,T),i(y,i(x,y))) = T).
92,91 [para_into,49,2,demod,3] (i(x,x) = T).
98,97 [para_into,49,12,demod,92] (i(x,T) = T).
102,101 [back_demod,63,demod,98,3] (i(y,i(x,y)) = T).
103 [back_demod,35,demod,102,3] (i(n(T),n(n(T))) = n(n(T))).
106,105 [back_demod,10,demod,102,3] (i(i(i(x,y),y),x) = i(y,x)).
111 [para_from,101,4,demod,3] (i(i(x,y),i(x,i(z,y))) = T).
113 [para_from,101,6,demod,3] (i(i(i(x,y),y),y) = i(x,y)).
115 [para_from,101,4,demod,3] (i(i(i(x,y),z),i(y,z)) = T).
151 [para_into,111,49,demod,3] (i(x,i(y,i(i(x,z),z))) = T).
194,193 [para_into,115,21,demod,3] (i(n(T),x) = T).
195 [para_into,115,7,demod,3] (i(n(x),i(x,y)) = T).
210,209 [back_demod,103,demod,194] (n(n(T)) = T).
219 [para_from,193,4,demod,3] (i(i(x,n(T)),i(x,y)) = T).
222,221 [para_from,193,6,demod,3] (i(i(x,n(T)),n(T)) = x).
229 [para_from,195,4,demod,3] (i(i(x,n(y)),i(x,i(y,z))) = T).
234,233 [para_from,195,6,demod,3] (i(i(i(x,y),n(x)),n(x)) = i(x,y)).
237 [para_from,221,7,demod,210,3] (i(n(i(x,n(T))),x) = T).
248,247 [para_from,237,7,demod,3] (i(x,i(n(x),n(T))) = T).
258,257 [back_demod,31,demod,248,3] (i(n(x),n(T)) = x).
259 [para_from,257,221] (i(x,n(T)) = n(x)).
264 [para_from,257,115] (i(i(i(x,n(y)),n(T)),y) = T).
272 [para_from,257,4,demod,194,3] (i(x,i(n(x),y)) = T).
275,274 [para_into,259,257] (n(n(x)) = x).
276 [para_into,259,221] (n(i(x,n(T))) = x).
278 [para_from,259,113,demod,222] (n(x) = i(x,n(T))).
288,287 [para_from,274,7] (i(i(n(x),y),i(n(y),x)) = T).
289 [para_from,274,7] (i(i(x,n(y)),i(y,n(x))) = T).
291 [para_from,278,7] (i(i(n(x),i(y,n(T))),i(y,x)) = T).
322,321 [para_from,219,6,demod,3] (i(i(i(x,y),i(x,n(T))),i(x,n(T))) = i(x,y)).
377 [para_into,151,6] (i(x,i(i(i(i(x,y),y),z),z)) = T).
417 [para_into,264,259] (i(n(i(x,n(y))),y) = T).
429 [para_into,417,274] (i(n(i(x,y)),n(y)) = T).
441 [para_into,429,6] (i(n(i(i(x,y),y)),n(x)) = T).
474,473 [para_into,287,274] (i(i(x,y),i(n(y),n(x))) = T).
479 [para_into,287,272,demod,275,3] (i(n(i(x,y)),x) = T).
491 [back_demod,23,demod,474,3] (i(n(y),n(x)) = i(x,y)).
496 [para_from,287,6,demod,3,288,3] (i(n(x),y) = i(n(y),x)).
500,499 [para_into,479,278] (i(i(i(x,y),n(T)),x) = T).
509 [para_into,491,278] (i(i(x,n(T)),n(y)) = i(y,x)).
511 [para_into,491,274] (i(x,n(y)) = i(y,n(x))).
513 [para_into,491,276] (i(n(x),y) = i(i(y,n(T)),x)).
520 [para_from,491,4] (i(i(n(x),y),i(i(y,n(z)),i(z,x))) = T).
530 [para_from,491,113,demod,234] (i(x,y) = i(n(y),n(x))).
533 [para_from,491,49] (i(n(x),i(i(y,x),n(y))) = T).
536,535 [para_from,491,6] (i(i(n(x),n(y)),n(y)) = i(i(x,y),n(x))).
540 [para_into,496,276] (i(x,y) = i(n(y),i(x,n(T)))).
565 [para_from,496,6] (i(i(n(x),y),x) = i(i(x,n(y)),n(y))).
569 [para_into,511,276] (i(x,y) = i(i(y,n(T)),n(x))).
598 [para_from,511,6] (i(i(x,n(y)),n(x)) = i(i(n(x),y),y)).
624,623 [para_into,530,105] (i(n(y),n(i(i(y,x),x))) = i(x,y)).
627 [para_into,530,6] (i(n(x),n(i(y,x))) = i(i(x,y),y)).
647 [para_from,530,4] (i(i(x,y),i(i(n(z),n(y)),i(x,z))) = T).
723 [para_into,289,278] (i(i(x,i(y,n(T))),i(y,n(x))) = T).
726,725 [para_into,289,530] (i(n(i(x,n(y))),n(i(y,n(x)))) = T).
771 [para_from,441,6,demod,3,624] (i(i(y,x),n(i(i(x,y),y))) = n(x)).
808 [para_into,509,276] (i(i(x,n(T)),y) = i(i(y,n(T)),x)).
1005 [para_from,533,4,demod,3] (i(i(i(i(x,y),n(x)),z),i(n(y),z)) = T).
1464,1463 [para_into,229,569,demod,258] (i(i(x,n(y)),i(y,i(x,z))) = T).
1470,1469 [para_into,229,513,demod,258] (i(i(x,y),i(n(y),i(x,z))) = T).
2855 [para_into,9,530] (i(i(i(n(b),n(a)),i(b,a)),i(b,a)) != T).
7827,7826 [para_from,725,627,demod,275,726,3] (n(i(y,n(x))) = i(i(x,n(y)),n(T))).
8405,8404 [para_into,771,723,demod,1464,3,3,7827] (n(i(y,i(x,n(T)))) = i(i(y,n(x)),n(T))).
8431,8430 [para_into,771,291,demod,1470,3,8405,3] (n(i(x,y)) = i(i(n(y),n(x)),n(T))).
10857 [para_from,565,113,demod,106] (i(i(n(y),x),x) = i(i(n(x),y),x)).
10860 [para_from,10857,233,demod,8431,275,8431,275,322] (i(i(n(x),y),x) = i(i(n(y),x),x)).
10862 [para_into,10860,274,demod,536] (i(i(x,y),n(x)) = i(i(y,x),n(y))).
10887 [para_into,10862,496,demod,275] (i(i(n(x),y),y) = i(i(x,n(y)),n(x))).
10936 [para_from,10887,598,demod,275,8431,275,275,8431,275,275,500,3]
(i(i(i(x,y),n(x)),i(i(y,x),n(T))) = y).
11090 [para_into,520,540,demod,258] (i(i(n(x),y),i(i(x,n(z)),i(z,y))) = T).
11114 [para_into,1005,647,demod,275,3] (i(n(x),i(i(n(y),z),i(i(z,x),y))) = T).
11184 [para_into,11090,808,demod,8431,275,3,258,258] (i(i(x,y),i(i(z,x),i(z,y))) = T).
11202 [para_from,11184,377,demod,3] (i(x,i(i(y,i(x,z)),i(y,z))) = T).
11213,11212 [para_into,11202,11202,demod,3] (i(i(x,i(y,z)),i(y,i(x,z))) = T).
11285 [para_from,11212,6,demod,3,11213,3] (i(x,i(y,z)) = i(y,i(x,z))).
11350 [para_from,11285,2855] (i(b,i(i(i(n(b),n(a)),i(b,a)),a)) != T).
11460 [para_into,11114,10936,demod,275,8431,275,8431,3,222]
(i(x,i(i(i(n(x),n(y)),i(x,y)),y)) = T).
11462 [binary,11460,11350] .
------------ end of proof -------------
-------------- statistics -------------
clauses input 6
clauses given 768
clauses generated 1012625
demod & eval rewrites 2793093
clauses wt,lit,sk delete 249150
tautologies deleted 0
clauses forward subsumed 761142
(subsumed by sos) 1097
clauses kept 5897
new demodulators 5564
empty clauses 1
clauses back demodulated 3558
clauses back subsumed 18
sos size 1655
Kbytes malloced 6801
----------- times (seconds) -----------
run time 2249.42 (run time 0 hr, 37 min, 29 sec)
system time 344.04
input time 0.01
clausify time 0.00
process input 0.01
para_into time 122.66
para_from time 115.25
pre_process time 1927.16
demod time 1567.96
weigh cl time 37.51
for_sub time 56.03
renumber time 69.31
keep cl time 9.72
print_cl time 0.00
conflict time 1.43
post_process time 65.32
back demod time 53.96
back_sub time 10.91
lex_rpo time 76.22
The job finished Thu Jun 4 18:15:07 1992