Theorem EQ-1: The Commutator Theorem

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Fri Jun  5 14:33:33 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,e,f(x,x),g(x),h(x,x)]).

lrpo_lr_status([f(x,x)]).

list(usable).
0 [] (x = x).
0 [] (f(e,x) = x).
0 [] (f(g(x),x) = e).
0 [] (f(f(x,y),z) = f(x,f(y,z))).
0 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))).
end_of_list.

list(sos).
0 [] (f(x,f(x,x)) = e).
0 [] (h(h(a,b),b) != e).
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).
** KEPT: 2 [] (f(e,x) = x).
** KEPT: 4 [] (f(g(x),x) = e).
** KEPT: 6 [] (f(f(x,y),z) = f(x,f(y,z))).
** KEPT: 8 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))).

------------> process sos:
** KEPT: 10 [] (f(x,f(x,x)) = e).
** KEPT: 12 [demod,9,9,7,7,7] (f(a,f(b,f(g(a),f(g(b),f(b,f(g(f(a,f(b,f(g(a),
                g(b))))),g(b))))))) != e).

------------> done processing input.

----> UNIT CONFLICT at   1.49 sec ----> 156 [binary,155,1] .
Level of proof is 13, length is 19.

---------------- PROOF ----------------

1 [] (x = x).
3,2 [] (f(e,x) = x).
5,4 [] (f(g(x),x) = e).
7,6 [] (f(f(x,y),z) = f(x,f(y,z))).
9,8 [] (h(x,y) = f(x,f(y,f(g(x),g(y))))).
11,10 [] (f(x,f(x,x)) = e).
12 [demod,9,9,7,7,7] 
		(f(a,f(b,f(g(a),f(g(b),f(b,f(g(f(a,f(b,f(g(a),g(b))))),g(b))))))) != e).
13 [para_into,10,6,demod,7] (f(x,f(y,f(x,f(y,f(x,y))))) = e).
16,15 [para_from,10,6,demod,3,7] (f(y,f(y,f(y,x))) = x).
18,17 [para_into,15,10] (f(x,f(x,e)) = f(x,x)).
21 [para_into,15,4,demod,18] (f(g(x),g(x)) = x).
24,23 [para_into,15,10] (f(x,e) = x).
28,27 [para_from,21,6] (f(g(x),f(g(x),y)) = f(x,y)).
32,31 [para_into,27,21,demod,5] (f(x,g(x)) = e).
34,33 [para_into,27,15,demod,28] (f(g(x),y) = f(x,f(x,y))).
36,35 [para_into,27,10,demod,24,34,32,24] (g(x) = f(x,x)).
37 [back_demod,12,demod,36,36,36,36,7,36,7,7,7,7,7,36,7,7,7,7,7,7,7,7,7,7,7,11,24,7,16,7,16] 
                (f(a,f(b,f(b,f(a,f(a,f(b,f(b,f(a,f(b,f(a,f(a,b))))))))))) != e).
43,42 [para_from,13,15,demod,24] (f(y,f(x,f(y,f(x,y)))) = f(x,x)).
45,44 [para_into,42,6,demod,7,7] 
                (f(x,f(y,f(z,f(x,f(y,f(z,x)))))) = f(y,f(z,f(y,z)))).
48,47 [para_from,42,6,demod,7,7,7,7]
                (f(z,f(x,f(z,f(x,f(z,y))))) = f(x,f(x,y))).
56 [para_into,47,10,demod,24] (f(x,f(y,f(x,y))) = f(y,f(y,f(x,x)))).
62 [para_into,56,56,demod,7,7,16,11,24,7,7,7,7]
                (f(y,f(x,f(y,f(y,f(x,f(y,f(x,x))))))) = f(x,y)).
127 [para_from,62,47,demod,48] (f(x,f(y,f(y,x))) = f(y,f(x,f(x,y)))).
153,152 [para_from,127,56,demod,7,7,7,7,11,24,7,7]
                (f(x,f(y,f(y,f(x,f(y,f(x,f(x,y))))))) = f(y,f(y,f(x,f(y,y))))).
155 [back_demod,37,demod,153,45,43,11] (e != e).
156 [binary,155,1] .

------------ end of proof -------------

-------------- statistics -------------
clauses input                  7
clauses given                 19
clauses generated            542
demod & eval rewrites       1945
tautologies deleted            0
clauses forward subsumed     453
  (subsumed by sos)           31
clauses kept                 114
new demodulators              41
empty clauses                  1
clauses back demodulated      18
clauses back subsumed          0
sos size                      79
Kbytes malloced              255

----------- times (seconds) -----------
run time             1.53                   (run time  0 hr, 0 min, 1 sec)
system time          0.28
input time           0.01
  clausify time      0.00
  process input      0.02
para_into time       0.10
para_from time       0.03
pre_process time     1.22
  demod time         0.55
  weigh cl time      0.00
  for_sub time       0.06
  renumber time      0.05
  keep cl time       0.31
  print_cl time      0.01
  conflict time      0.03
post_process time    0.11
  back demod time    0.04
  back_sub time      0.07
lex_rpo time         0.13
The job finished        Fri Jun  5 14:33:35 1992