Theorem 4: Equivalential Calculus, XGK 1#1 PYO

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Wed Jun  3 13:22:37 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) | -P(e(x,y)) | P(y).
end_of_list.

list(sos).
2 [] P(e(x,e(e(y,e(z,x)),e(z,y)))).
3 [] -P(e(e(e(a,e(b,c)),c),e(b,a))).
end_of_list.
OTTER sets dynamic_demod, because back_demod is set.
OTTER sets order_eq, because dynamic_demod is set.

Resetting weight limit to 20.
----> UNIT CONFLICT at 407.50 sec ----> 15324 [binary,15323,3] .
Level of proof is 13, length is 19.

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

1 [] -P(x) | -P(e(x,y)) | P(y).
2 [] P(e(x,e(e(y,e(z,x)),e(z,y)))).
3 [] -P(e(e(e(a,e(b,c)),c),e(b,a))).
4 [hyper,2,1,2] P(e(e(x,e(y,e(z,e(e(u,e(v,z)),e(v,u))))),e(y,x))).
6 [hyper,4,1,2] P(e(e(e(e(x,e(y,z)),e(y,x)),e(z,u)),u)).
8 [hyper,6,1,6] P(e(x,x)).
9 [hyper,6,1,4] P(e(e(x,e(e(y,e(z,x)),e(z,y))),e(u,u))).
13 [hyper,8,1,2] P(e(e(x,e(y,e(z,z))),e(y,x))).
18 [hyper,13,1,2] P(e(e(x,e(x,y)),y)).
21 [hyper,13,1,2] P(e(e(x,e(y,e(e(z,e(u,e(v,v))),e(u,z)))),e(y,x))).
39 [hyper,18,1,13] P(e(x,e(y,e(y,e(x,e(z,z)))))).
42 [hyper,18,1,2] P(e(e(x,e(y,e(e(z,e(z,u)),u))),e(y,x))).
108 [hyper,39,1,4] P(e(x,e(y,e(y,x)))).
133 [hyper,108,1,2] P(e(e(x,e(y,e(z,e(u,e(u,z))))),e(y,x))).
146 [hyper,9,1,2] P(e(e(x,e(y,e(e(z,e(e(u,e(v,z)),e(v,u))),e(w,w)))),e(y,x))).
682 [hyper,42,1,18] P(e(x,e(y,e(y,e(x,e(e(z,e(z,u)),u)))))).
2253 [hyper,133,1,2] P(e(e(e(x,e(x,y)),e(y,z)),z)).
8738 [hyper,682,1,4] P(e(x,e(y,e(e(z,e(z,y)),x)))).
8897 [hyper,8738,1,2253] P(e(e(x,e(x,y)),e(z,e(z,y)))).
9048 [hyper,8897,1,21] P(e(e(x,e(y,e(z,z))),e(u,e(u,e(y,x))))).
13855 [hyper,9048,1,4] P(e(x,e(e(y,z),e(e(z,e(y,x)),e(u,u))))).
15323 [hyper,13855,1,146] P(e(e(e(x,e(y,z)),z),e(y,x))).
15324 [binary,15323,3] .

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

-------------- statistics -------------
clauses input                  3
clauses given                587
clauses generated         177109
demod & eval rewrites          0
clauses wt,lit,sk delete  102987
tautologies deleted            0
clauses forward subsumed   58802
  (subsumed by sos)        12239
clauses kept               15320
new demodulators               0
empty clauses                  1
clauses back demodulated       0
clauses back subsumed          0
sos size                   14735
Kbytes malloced             8047

----------- times (seconds) -----------
run time           407.53                   (run time  0 hr, 6 min, 47 sec)
system time         41.90
input time           0.01
  clausify time      0.00
hyper_res time      72.62
pre_process time   100.67
  demod time         0.00
  weigh cl time     15.72
  for_sub time      18.83
  renumber time     18.15
  keep cl time      21.08
  print_cl time      0.00
  conflict time      4.38
post_process time  223.50
  back demod time    0.00
  back_sub time    223.01
lex_rpo time         0.00
The job finished        Wed Jun  3 13:30:09 1992