Next: Theorem 6: Many-valued Sentential
Up: Summary of Otter Outputs
Previous: Theorem 4: Equivalential Calculus,
----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Wed Jun 3 14:27:00 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(i(i(x,y),z),i(i(z,x),i(u,x)))).
3 [] -P(i(i(a,b),i(i(b,c),i(a,c)))).
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.
Resetting weight limit to 18.
Resetting weight limit to 16.
----> UNIT CONFLICT at 7711.98 sec ----> 17866 [binary,17865,3] .
Level of proof is 40, length is 94.
---------------- PROOF ----------------
1 [] -P(x) | -P(i(x,y)) | P(y).
2 [] P(i(i(i(x,y),z),i(i(z,x),i(u,x)))).
3 [] -P(i(i(a,b),i(i(b,c),i(a,c)))).
4 [hyper,2,1,2] P(i(i(i(i(x,y),i(z,y)),i(y,u)),i(v,i(y,u)))).
5 [hyper,4,1,4] P(i(x,i(i(y,z),i(z,i(y,z))))).
6 [hyper,4,1,2] P(i(i(i(x,i(y,z)),i(i(u,y),i(v,y))),i(w,i(i(u,y),i(v,y))))).
7 [hyper,5,1,5] P(i(i(x,y),i(y,i(x,y)))).
12 [hyper,7,1,2] P(i(i(i(x,i(y,x)),y),i(z,y))).
15 [hyper,6,1,12] P(i(x,i(i(y,z),i(z,z)))).
19 [hyper,6,1,2] P(i(i(i(x,i(i(y,z),i(u,z))),i(v,i(z,w))),i(v6,i(v,i(z,w))))).
20 [hyper,15,1,15] P(i(i(x,y),i(y,y))).
23 [hyper,20,1,12] P(i(i(x,y),i(x,y))).
24 [hyper,20,1,2] P(i(i(i(x,x),y),i(z,y))).
26 [hyper,23,1,2] P(i(i(i(x,y),x),i(z,x))).
27 [hyper,24,1,24] P(i(x,i(y,i(z,z)))).
28 [hyper,24,1,23] P(i(x,i(y,y))).
31 [hyper,24,1,4] P(i(x,i(y,i(z,y)))).
32 [hyper,28,1,28] P(i(x,x)).
38 [hyper,31,1,32] P(i(x,i(y,x))).
41 [hyper,38,1,27] P(i(x,i(y,i(z,i(u,u))))).
45 [hyper,38,1,2] P(i(x,i(i(i(y,z),u),i(i(u,y),i(v,y))))).
47 [hyper,38,1,2] P(i(i(i(x,i(y,z)),y),i(u,y))).
48 [hyper,26,1,2] P(i(i(i(x,y),i(y,z)),i(u,i(y,z)))).
53 [hyper,41,1,38] P(i(x,i(y,i(z,i(u,i(v,v)))))).
61 [hyper,19,1,2] P(i(x,i(i(i(i(y,z),i(u,z)),v),i(z,v)))).
80 [hyper,47,1,2] P(i(i(i(x,y),i(z,i(y,u))),i(v,i(z,i(y,u))))).
85 [hyper,53,1,38] P(i(x,i(y,i(z,i(u,i(v,i(w,w))))))).
92 [hyper,48,1,2] P(i(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y)))).
122 [hyper,45,1,2] P(i(i(i(i(i(x,y),z),i(i(z,x),i(u,x))),v),i(w,v))).
130 [hyper,61,1,85] P(i(i(i(i(x,y),i(z,y)),u),i(y,u))).
138 [hyper,130,1,26] P(i(x,i(y,i(z,x)))).
139 [hyper,130,1,2] P(i(x,i(i(i(y,x),z),i(u,z)))).
166 [hyper,138,1,2] P(i(i(i(x,i(y,i(z,u))),z),i(v,z))).
338 [hyper,92,1,2] P(i(x,i(i(i(i(y,z),u),z),i(y,z)))).
353 [hyper,338,1,338] P(i(i(i(i(x,y),z),y),i(x,y))).
362 [hyper,353,1,2] P(i(i(i(x,y),i(i(x,y),z)),i(u,i(i(x,y),z)))).
970 [hyper,362,1,47] P(i(x,i(i(i(y,i(z,u)),z),z))).
973 [hyper,362,1,26] P(i(x,i(i(i(y,z),y),y))).
974 [hyper,362,1,24] P(i(x,i(i(i(y,y),z),z))).
991 [hyper,973,1,973] P(i(i(i(x,y),x),x)).
1004 [hyper,991,1,2] P(i(i(x,i(x,y)),i(z,i(x,y)))).
1005 [hyper,974,1,991] P(i(i(i(x,x),y),y)).
1016 [hyper,970,1,1005] P(i(i(i(x,i(y,z)),y),y)).
1027 [hyper,1016,1,2] P(i(i(x,i(y,i(x,z))),i(u,i(y,i(x,z))))).
1072 [hyper,1004,1,1004] P(i(x,i(i(y,i(y,z)),i(y,z)))).
1083 [hyper,1072,1,1072] P(i(i(x,i(x,y)),i(x,y))).
1104 [hyper,1083,1,166] P(i(i(i(x,i(y,i(z,u))),z),z)).
1114 [hyper,1083,1,92] P(i(i(i(x,i(y,z)),i(u,y)),i(u,y))).
1118 [hyper,1083,1,80] P(i(i(i(x,y),i(z,i(y,u))),i(z,i(y,u)))).
1124 [hyper,1083,1,48] P(i(i(i(x,y),i(y,z)),i(y,z))).
1155 [hyper,1104,1,2] P(i(i(x,i(y,i(z,i(x,u)))),i(v,i(y,i(z,i(x,u)))))).
1177 [hyper,1124,1,2] P(i(i(i(x,y),i(z,x)),i(u,i(z,x)))).
1374 [hyper,1177,1,1083] P(i(i(i(x,y),i(z,x)),i(z,x))).
1565 [hyper,1027,1,139] P(i(x,i(i(i(y,z),u),i(z,u)))).
1566 [hyper,1027,1,2] P(i(x,i(i(y,z),i(i(i(z,u),y),z)))).
1567 [hyper,1027,1,1083] P(i(i(x,i(y,i(x,z))),i(y,i(x,z)))).
1577 [hyper,1565,1,1565] P(i(i(i(x,y),z),i(y,z))).
1588 [hyper,1577,1,2] P(i(x,i(i(x,y),i(z,y)))).
1592 [hyper,1577,1,122] P(i(x,i(y,i(i(y,z),i(u,z))))).
1645 [hyper,1588,1,2] P(i(i(i(i(i(x,y),z),i(u,z)),x),i(v,x))).
1661 [hyper,1566,1,1592] P(i(i(x,y),i(i(i(y,z),x),y))).
1672 [hyper,1661,1,1588] P(i(i(i(i(i(x,y),i(z,y)),u),x),i(i(x,y),i(z,y)))).
1703 [hyper,1661,1,1004] P(i(i(i(i(x,i(y,z)),u),i(y,i(y,z))),i(x,i(y,z)))).
1741 [hyper,1661,1,138] P(i(i(i(i(x,i(y,z)),u),z),i(x,i(y,z)))).
1762 [hyper,1661,1,47] P(i(i(i(i(x,y),z),i(i(u,i(y,v)),y)),i(x,y))).
1765 [hyper,1661,1,26] P(i(i(i(i(x,y),z),i(i(y,u),y)),i(x,y))).
2492 [hyper,1645,1,1083] P(i(i(i(i(i(x,y),z),i(u,z)),x),x)).
4636 [hyper,1762,1,2492] P(i(i(i(i(i(x,i(i(y,z),u)),i(y,z)),v),z),i(y,z))).
7184 [hyper,1155,1,1083] P(i(i(x,i(y,i(z,i(x,u)))),i(y,i(z,i(x,u))))).
10842 [hyper,4636,1,1765] P(i(i(i(x,i(i(i(y,z),y),u)),i(i(y,z),y)),y)).
10924 [hyper,10842,1,1672] P(i(i(x,y),i(i(i(x,z),x),y))).
10927 [hyper,10924,1,1588] P(i(i(i(x,y),x),i(i(x,z),i(u,z)))).
10951 [hyper,10927,1,1741] P(i(x,i(y,i(i(x,z),i(u,z))))).
10953 [hyper,10927,1,1703] P(i(x,i(i(x,y),y))).
11237 [hyper,10953,1,10924] P(i(i(i(x,y),x),i(i(x,z),z))).
11252 [hyper,10953,1,1661] P(i(i(i(i(i(x,y),y),z),x),i(i(x,y),y))).
11310 [hyper,10951,1,1577] P(i(x,i(y,i(i(i(z,x),u),i(v,u))))).
11344 [hyper,11237,1,1741] P(i(x,i(y,i(i(x,z),z)))).
11355 [hyper,11237,1,2] P(i(i(i(i(x,y),y),i(x,z)),i(u,i(x,z)))).
11414 [hyper,11344,1,1577] P(i(x,i(y,i(i(i(z,x),u),u)))).
12034 [hyper,11355,1,1083] P(i(i(i(i(x,y),y),i(x,z)),i(x,z))).
12131 [hyper,12034,1,11414] P(i(x,i(i(i(y,i(i(x,z),z)),u),u))).
12134 [hyper,12034,1,11310] P(i(x,i(i(i(y,i(i(x,z),z)),u),i(v,u)))).
12136 [hyper,12034,1,10951] P(i(x,i(i(i(i(x,y),y),z),i(u,z)))).
12188 [hyper,12131,1,1374] P(i(i(i(x,i(i(i(y,z),u),u)),y),y)).
12191 [hyper,12131,1,1114] P(i(i(i(x,i(i(i(y,i(z,u)),v),v)),z),z)).
12238 [hyper,12136,1,1567] P(i(i(i(i(x,y),y),z),i(x,z))).
12442 [hyper,12188,1,11252] P(i(i(x,i(i(i(x,y),z),z)),i(i(i(x,y),z),z))).
13088 [hyper,12134,1,1118] P(i(i(i(x,i(i(i(y,z),u),u)),v),i(z,v))).
13109 [hyper,12191,1,1672] P(i(i(x,y),i(i(i(z,i(x,u)),y),y))).
13927 [hyper,13088,1,1672] P(i(i(i(x,y),z),i(i(i(u,x),z),z))).
14592 [hyper,12442,1,13109] P(i(i(i(i(x,y),i(x,z)),y),y)).
14632 [hyper,14592,1,13927] P(i(i(i(x,i(i(y,z),i(y,u))),z),z)).
14829 [hyper,14632,1,1672] P(i(i(x,i(y,z)),i(i(y,x),i(y,z)))).
15113 [hyper,14829,1,10951] P(i(i(x,y),i(x,i(i(y,z),i(u,z))))).
16490 [hyper,15113,1,12238] P(i(x,i(i(x,y),i(i(y,z),i(u,z))))).
17865 [hyper,16490,1,7184] P(i(i(x,y),i(i(y,z),i(x,z)))).
17866 [binary,17865,3] .
------------ end of proof -------------
-------------- statistics -------------
clauses input 3
clauses given 3096
clauses generated 8341570
demod & eval rewrites 0
clauses wt,lit,sk delete 2972221
tautologies deleted 0
clauses forward subsumed 5351487
(subsumed by sos) 83872
clauses kept 17862
new demodulators 0
empty clauses 1
clauses back demodulated 0
clauses back subsumed 386
sos size 14449
Kbytes malloced 10729
----------- times (seconds) -----------
run time 7714.75 (run time 2 hr, 8 min, 34 sec)
system time 1863.38
input time 0.01
clausify time 0.00
hyper_res time 2863.86
pre_process time 4227.72
demod time 0.00
weigh cl time 736.90
for_sub time 1461.46
renumber time 866.73
keep cl time 33.44
print_cl time 0.00
conflict time 4.74
post_process time 455.12
back demod time 0.00
back_sub time 450.01
lex_rpo time 0.00
The job finished Wed Jun 3 17:07:15 1992
Karen D. Toonen
1998-11-18