Theorem 6: Many-valued Sentential Calculus, CD-57

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

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

list(usable).
1 [] -P(x) | -P(i(x,y)) | P(y).
end_of_list.

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

----> UNIT CONFLICT at  17.68 sec ----> 4844 [binary,4843,6] .
Level of proof is 4, length is 5.

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

1 [] -P(x) | -P(i(x,y)) | P(y).
2 [] P(i(x,i(y,x))).
3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).
4 [] P(i(i(i(x,y),y),i(i(y,x),x))).
6 [] -P(i(i(a,b),i(i(c,a),i(c,b)))).
14 [hyper,3,1,3] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
15 [hyper,3,1,2] P(i(i(i(x,y),z),i(y,z))).
24 [hyper,4,1,15] P(i(x,i(i(x,y),y))).
49 [hyper,24,1,3] P(i(i(i(i(x,y),y),z),i(x,z))).
4843 [hyper,49,1,14] P(i(i(x,y),i(i(z,x),i(z,y)))).
4844 [binary,4843,6] .

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

-------------- statistics -------------
clauses input                  6
clauses given                181
clauses generated          16687
demod & eval rewrites          0
tautologies deleted            0
clauses forward subsumed   11850
  (subsumed by sos)         1683
clauses kept                4837
new demodulators               0
empty clauses                  1
clauses back demodulated       0
clauses back subsumed         11
sos size                    4650
Kbytes malloced             2171

----------- times (seconds) -----------
run time            17.69                   (run time  0 hr, 0 min, 17 sec)
system time          4.34
input time           0.02
  clausify time      0.00
hyper_res time       3.53
pre_process time    10.57
  demod time         0.00
  weigh cl time      0.00
  for_sub time       2.80
  renumber time      0.92
  keep cl time       4.46
  print_cl time      0.00
  conflict time      1.17
post_process time    2.63
  back demod time    0.00
  back_sub time      2.57
lex_rpo time         0.00
The job finished        Wed Jun  3 13:17:14 1992