Theorem 1: x²=e Groups are Commutative (P-form)

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Wed Jun  3 13:15:19 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)).
end_of_list.

list(sos).
13 [] P(e,x,x).
14 [] P(x,e,x).
15 [] P(g(x),x,e).
16 [] P(x,g(x),e).
17 [] P(x,y,f(x,y)).
18 [] P(x,x,e).
19 [] P(a,b,c).
20 [] -P(b,a,c).
end_of_list.
OTTER sets dynamic_demod, because back_demod is set.
OTTER sets order_eq, because dynamic_demod is set.

----> UNIT CONFLICT at   0.20 sec ----> 35 [binary,34,20] .
Level of proof is 3, length is 4.

---------------- 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).
13 [] P(e,x,x).
14 [] P(x,e,x).
18 [] P(x,x,e).
19 [] P(a,b,c).
20 [] -P(b,a,c).
21 [hyper,19,2,18,14] P(c,b,a).
22 [hyper,19,1,18,13] P(a,c,b).
23 [hyper,21,1,18,13] P(c,a,b).
34 [hyper,23,2,22,19] P(b,a,c).
35 [binary,34,20] .

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

-------------- statistics -------------
clauses input                 20
clauses given                  9
clauses generated            222
demod & eval rewrites         26
tautologies deleted            0
clauses forward subsumed     209
  (subsumed by sos)           13
clauses kept                  13
new demodulators               1
empty clauses                  1
clauses back demodulated       0
clauses back subsumed          0
sos size                      12
Kbytes malloced               31

----------- times (seconds) -----------
run time             0.22                   (run time  0 hr, 0 min, 0 sec)
system time          0.11
input time           0.02
  clausify time      0.00
hyper_res time       0.05
pre_process time     0.09
  demod time         0.01
  weigh cl time      0.00
  for_sub time       0.05
  renumber time      0.00
  keep cl time       0.00
  print_cl time      0.00
  conflict time      0.00
post_process time    0.01
  back demod time    0.00
  back_sub time      0.01
lex_rpo time         0.00
The job finished        Wed Jun  3 13:15:19 1992