Theorem 2: The Commutator Theorem (P-form)

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Wed Jun  3 13:13:02 1992
The command was "otter22".

set(hyper_res).
set(back_demod).
set(dynamic_demod_all).
assign(pick_given_ratio,5).
clear(print_kept).
assign(max_mem,20000).
set(control_memory).

list(usable).
1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).
3 [] -P(x,y,u) | -P(x,y,v) | eq(u,v).
4 [] eq(x,x).
5 [] -eq(x,y) | eq(y,x).
6 [] -eq(x,y) | -eq(y,z) | eq(x,z).
7 [] -eq(u,v) | -P(u,x,y) | P(v,x,y).
8 [] -eq(u,v) | -P(x,u,y) | P(x,v,y).
9 [] -eq(u,v) | -P(x,y,u) | P(x,y,v).
10 [] -eq(u,v) | eq(f(u,x),f(v,x)).
11 [] -eq(u,v) | eq(f(x,u),f(x,v)).
12 [] -eq(u,v) | eq(g(u),g(v)).
13 [] -P(x,x,y) | P(x,y,e).
14 [] -P(x,x,y) | P(y,x,e).
end_of_list.

list(sos).
15 [] P(e,x,x).
16 [] P(x,e,x).
17 [] P(g(x),x,e).
18 [] P(x,g(x),e).
19 [] P(x,y,f(x,y)).
20 [] P(a,b,c).
21 [] P(c,g(a),d).
22 [] P(d,g(b),h).
23 [] P(h,b,j).
24 [] P(j,g(h),k).
25 [] -P(k,g(b),e).
end_of_list.
OTTER sets dynamic_demod, because back_demod is set.
OTTER sets order_eq, because dynamic_demod is set.

----> UNIT CONFLICT at  35.60 sec ----> 4648 [binary,4647,49] .
Level of proof is 15, length is 37.

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

1 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
2 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).
3 [] -P(x,y,u) | -P(x,y,v) | eq(u,v).
9 [] -eq(u,v) | -P(x,y,u) | P(x,y,v).
13 [] -P(x,x,y) | P(x,y,e).
14 [] -P(x,x,y) | P(y,x,e).
15 [] P(e,x,x).
16 [] P(x,e,x).
17 [] P(g(x),x,e).
18 [] P(x,g(x),e).
19 [] P(x,y,f(x,y)).
20 [] P(a,b,c).
21 [] P(c,g(a),d).
22 [] P(d,g(b),h).
23 [] P(h,b,j).
24 [] P(j,g(h),k).
25 [] -P(k,g(b),e).
28 [hyper,17,2,17,16] P(e,x,g(g(x))).
37 [hyper,21,2,17,16] P(d,a,c).
39 [hyper,37,1,17,15] P(g(d),c,a).
41 [hyper,22,2,17,16] P(h,b,d).
45,44 [hyper,41,3,23] eq(j,d).
46 [hyper,41,1,17,15] P(g(h),d,b).
47 [back_demod,24,demod,45] P(d,g(h),k).
48 [hyper,19,14] P(f(x,x),x,e).
49 [hyper,19,13] P(x,f(x,x),e).
65,64 [hyper,19,3,16] eq(f(x,e),x).
67,66 [hyper,19,3,15] eq(f(e,x),x).
79 [hyper,19,2,19,19] P(f(x,y),z,f(x,f(y,z))).
80 [hyper,19,2,19,18,demod,65] P(f(x,y),g(y),x).
160 [hyper,39,2,18,19,demod,65] P(a,g(c),g(d)).
176 [hyper,46,2,18,19,demod,65] P(b,g(d),g(h)).
183,182 [hyper,28,3,19,demod,67] eq(g(g(x)),x).
192 [hyper,47,2,18,19,demod,183,65] P(k,h,d).
312 [hyper,48,1,20,19,demod,67] P(f(a,a),c,b).
317,316 [hyper,49,3,19] eq(f(x,f(x,x)),e).
319 [hyper,49,2,192,19,demod,65] P(d,f(h,h),k).
497 [hyper,176,3,19] eq(f(b,g(d)),g(h)).
705 [hyper,312,1,19,19] P(a,f(a,c),b).
715,714 [hyper,319,3,19] eq(f(d,f(h,h)),k).
932 [hyper,705,2,37,19] P(c,f(a,c),f(d,b)).
1180 [hyper,80,1,49,19,demod,67] P(x,x,g(x)).
1235,1234 [hyper,1180,3,19] eq(g(x),f(x,x)).
1256 [hyper,1180,2,19,160,demod,1235] P(f(a,c),c,f(d,d)).
1481,1480 [back_demod,497,demod,1235,1235] eq(f(b,f(d,d)),f(h,h)).
1534 [back_demod,25,demod,1235] -P(k,f(b,b),e).
1586,1585 [hyper,79,3,19] eq(f(f(x,y),z),f(x,f(y,z))).
3340,3339 [hyper,932,3,19] eq(f(c,f(a,c)),f(d,b)).
3736 [hyper,1256,2,48,19,demod,1586,3340,1586,1586,1481,715] P(e,c,f(a,k)).
3775 [hyper,3736,3,19,demod,67] eq(f(a,k),c).
3794 [hyper,3775,9,19] P(a,k,c).
3817 [hyper,3794,2,79,312,demod,317] P(e,k,b).
3959,3958 [hyper,3817,3,19,demod,67] eq(k,b).
4647 [back_demod,1534,demod,3959] -P(b,f(b,b),e).
4648 [binary,4647,49] .

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

-------------- statistics -------------
clauses input                 25
clauses given                165
clauses generated          20575
demod & eval rewrites      32696
tautologies deleted            0
clauses forward subsumed   18332
  (subsumed by sos)         6484
clauses kept                4505
new demodulators             117
empty clauses                  1
clauses back demodulated    2262
clauses back subsumed         60
sos size                    2089
Kbytes malloced             1564

----------- times (seconds) -----------
run time            35.65                   (run time  0 hr, 0 min, 35 sec)
system time          6.88
input time           0.01
  clausify time      0.00
hyper_res time       6.07
pre_process time    19.21
  demod time         6.33
  weigh cl time      0.00
  for_sub time       6.37
  renumber time      0.94
  keep cl time       2.18
  print_cl time      0.00
  conflict time      1.48
post_process time    9.71
  back demod time    7.73
  back_sub time      1.82
lex_rpo time         0.00
The job finished        Wed Jun  3 13:13:44 1992