Theorem 3: x²=x Rings are Commutative (P-form)

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Wed Jun  3 13:19:36 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 [] -S(x,y,u) | -S(y,z,v) | -S(u,z,w) | S(x,v,w).
2 [] -S(x,y,u) | -S(y,z,v) | -S(x,v,w) | S(u,z,w).
3 [] -S(x,y,u) | -S(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) | -S(u,x,y) | S(v,x,y).
8 [] -eq(u,v) | -S(x,u,y) | S(x,v,y).
9 [] -eq(u,v) | -S(x,y,u) | S(x,y,v).
10 [] -eq(u,v) | eq(j(u,x),j(v,x)).
11 [] -eq(u,v) | eq(j(x,u),j(x,v)).
12 [] -eq(u,v) | eq(g(u),g(v)).
13 [] -S(x,y,z) | S(y,x,z).
14 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
15 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).
16 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4).
17 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4).
18 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4).
19 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4).
20 [] -P(x,y,u) | -P(x,y,v) | eq(u,v).
21 [] -eq(u,v) | -P(u,x,y) | P(v,x,y).
22 [] -eq(u,v) | -P(x,u,y) | P(x,v,y).
23 [] -eq(u,v) | -P(x,y,u) | P(x,y,v).
24 [] -eq(u,v) | eq(f(u,x),f(v,x)).
25 [] -eq(u,v) | eq(f(x,u),f(x,v)).
end_of_list.

list(sos).
26 [] S(0,x,x).
27 [] S(x,0,x).
28 [] S(g(x),x,0).
29 [] S(x,g(x),0).
30 [] S(x,y,j(x,y)).
31 [] P(0,x,0).
32 [] P(x,0,0).
33 [] P(x,y,f(x,y)).
34 [] P(x,x,x).
35 [] P(a,b,c).
36 [] -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 145.41 sec ----> 14124 [binary,14123,36] .
Level of proof is 16, length is 41.

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

1 [] -S(x,y,u) | -S(y,z,v) | -S(u,z,w) | S(x,v,w).
2 [] -S(x,y,u) | -S(y,z,v) | -S(x,v,w) | S(u,z,w).
3 [] -S(x,y,u) | -S(x,y,v) | eq(u,v).
13 [] -S(x,y,z) | S(y,x,z).
14 [] -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
15 [] -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).
16 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -P(x,v3,v4) | S(v1,v2,v4).
17 [] -P(x,y,v1) | -P(x,z,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(x,v3,v4).
18 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -P(v3,x,v4) | S(v1,v2,v4).
19 [] -P(y,x,v1) | -P(z,x,v2) | -S(y,z,v3) | -S(v1,v2,v4) | P(v3,x,v4).
20 [] -P(x,y,u) | -P(x,y,v) | eq(u,v).
23 [] -eq(u,v) | -P(x,y,u) | P(x,y,v).
26 [] S(0,x,x).
27 [] S(x,0,x).
28 [] S(g(x),x,0).
29 [] S(x,g(x),0).
30 [] S(x,y,j(x,y)).
31 [] P(0,x,0).
32 [] P(x,0,0).
33 [] P(x,y,f(x,y)).
34 [] P(x,x,x).
35 [] P(a,b,c).
36 [] -P(b,a,c).
37 [hyper,35,15,35,34] P(c,b,c).
38 [hyper,35,14,34,35] P(a,c,c).
43,42 [hyper,28,3,27] eq(g(0),0).
44 [hyper,28,2,28,27] S(0,x,g(g(x))).
63 [hyper,30,19,34,37,30] P(j(b,c),b,j(b,c)).
92 [hyper,30,17,38,34,30] P(a,j(c,a),j(c,a)).
120 [hyper,30,13] S(x,y,j(y,x)).
126,125 [hyper,30,3,27] eq(j(x,0),x).
128,127 [hyper,30,3,26] eq(j(0,x),x).
131 [hyper,30,2,30,28,demod,126] S(j(x,g(y)),y,x).
139 [hyper,30,1,28,30,demod,128] S(g(x),j(x,y),y).
150,149 [hyper,33,20,32] eq(f(x,0),0).
152,151 [hyper,33,20,31] eq(f(0,x),0).
193 [hyper,33,18,34,33,29,demod,152] S(x,f(g(x),x),0).
248 [hyper,33,16,34,33,29,demod,150] S(x,f(x,g(x)),0).
258 [hyper,33,16,33,34,28,demod,150] S(f(x,g(x)),x,0).
325,324 [hyper,44,3,30,demod,128] eq(g(g(x)),x).
450 [hyper,120,2,120,28,demod,128] S(j(g(x),y),x,y).
475 [hyper,120,1,28,120,demod,126] S(g(x),j(y,x),y).
1477 [hyper,139,3,30] eq(j(g(x),j(x,y)),y).
1905 [hyper,193,2,29,131,demod,43,126,325,43,126] S(0,f(x,g(x)),x).
2976 [hyper,248,3,30] eq(j(x,f(x,g(x))),0).
3558 [hyper,258,2,30,131,demod,43,126] S(j(x,f(y,g(y))),y,x).
7630,7629 [hyper,1905,3,120,demod,126] eq(f(x,g(x)),x).
7631 [hyper,1905,2,450,248,demod,43,128,43,128,7630,43,128,43,128,7630,7630] S(x,x,0).
7632 [hyper,1905,1,475,248,demod,128] S(g(x),0,x).
7636 [hyper,1905,1,258,120,demod,7630,7630] S(x,j(y,x),y).
7637 [hyper,1905,1,258,30,demod,7630,7630] S(x,j(x,y),y).
7793 [back_demod,3558,demod,7630] S(j(x,y),y,x).
7836,7835 [back_demod,2976,demod,7630] eq(j(x,x),0).
8850 [hyper,63,17,34,120,120,demod,7836] P(j(b,c),j(b,j(b,c)),0).
9362,9361 [hyper,7632,3,120,demod,128] eq(g(x),x).
10116,10115 [back_demod,1477,demod,9362] eq(j(x,j(x,y)),y).
10286 [back_demod,8850,demod,10116] P(j(b,c),c,0).
10433 [hyper,92,19,34,7793,7631] P(c,j(c,a),0).
11007 [hyper,10286,19,34,7636,120,demod,128] P(b,c,c).
11206 [hyper,11007,15,33,35] P(f(b,a),b,c).
11469 [hyper,10433,17,34,7637,120,demod,128] P(c,a,c).
12377 [hyper,11206,15,33,34] P(c,a,f(b,a)).
14119 [hyper,12377,20,11469] eq(f(b,a),c).
14123 [hyper,14119,23,33] P(b,a,c).
14124 [binary,14123,36] .

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

-------------- statistics -------------
clauses input                 36
clauses given                120
clauses generated          56025
demod & eval rewrites      77893
tautologies deleted            1
clauses forward subsumed   53529
  (subsumed by sos)        19775
clauses kept               13990
new demodulators              97
empty clauses                  1
clauses back demodulated   11495
clauses back subsumed         39
sos size                    2410
Kbytes malloced             4342

----------- times (seconds) -----------
run time           145.46                   (run time  0 hr, 2 min, 25 sec)
system time         20.87
input time           0.04
  clausify time      0.00
hyper_res time      20.44
pre_process time    52.21
  demod time        12.31
  weigh cl time      0.00
  for_sub time      18.56
  renumber time      2.96
  keep cl time       7.94
  print_cl time      0.00
  conflict time      5.10
post_process time   71.27
  back demod time   63.58
  back_sub time      7.18
lex_rpo time         0.00
The job finished        Wed Jun  3 13:22:23 1992