----- OTTER 2.2, July 1991 ----- The job began on altair.mcs.anl.gov, Wed Jun 3 13:31:24 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(n(b),n(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 13. ----> UNIT CONFLICT at 2184.96 sec ----> 16257 [binary,16256,6] . Level of proof is 13, length is 24. ---------------- 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))). 5 [] P(i(i(n(x),n(y)),i(y,x))). 6 [] -P(i(i(a,b),i(n(b),n(a)))). 7 [hyper,2,1,2] P(i(x,i(y,i(z,y)))). 13 [hyper,3,1,5] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))). 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))). 18 [hyper,4,1,7] P(i(i(i(x,i(y,x)),z),z)). 21 [hyper,15,1,5] P(i(n(x),i(x,y))). 22 [hyper,15,1,4] P(i(x,i(i(x,y),y))). 27 [hyper,21,1,3] P(i(i(i(x,y),z),i(n(x),z))). 33 [hyper,22,1,5] P(i(i(i(i(n(x),n(y)),i(y,x)),z),z)). 37 [hyper,22,1,3] P(i(i(i(i(x,y),y),z),i(x,z))). 59 [hyper,18,1,15] P(i(x,x)). 63 [hyper,59,1,22] P(i(i(i(x,x),y),y)). 238 [hyper,13,1,63] P(i(i(n(x),n(i(y,y))),x)). 284 [hyper,238,1,27] P(i(n(n(x)),x)). 320 [hyper,284,1,5] P(i(x,n(n(x)))). 321 [hyper,284,1,3] P(i(i(x,y),i(n(n(x)),y))). 378 [hyper,320,1,22] P(i(i(i(x,n(n(x))),y),y)). 1651 [hyper,378,1,14] P(i(i(x,y),i(x,n(n(y))))). 1762 [hyper,33,1,14] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))). 2121 [hyper,37,1,14] P(i(i(x,i(y,z)),i(y,i(x,z)))). 3351 [hyper,1651,1,37] P(i(x,i(i(x,y),n(n(y))))). 5608 [hyper,3351,1,321] P(i(n(n(x)),i(i(x,y),n(n(y))))). 15901 [hyper,5608,1,2121] P(i(i(x,y),i(n(n(x)),n(n(y))))). 16256 [hyper,1762,1,15901] P(i(i(x,y),i(n(y),n(x)))). 16257 [binary,16256,6] . ------------ end of proof ------------- -------------- statistics ------------- clauses input 6 clauses given 2768 clauses generated 3214280 demod & eval rewrites 0 clauses wt,lit,sk delete 1712800 tautologies deleted 0 clauses forward subsumed 1485230 (subsumed by sos) 16917 clauses kept 16250 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 24 sos size 13466 Kbytes malloced 7216 ----------- times (seconds) ----------- run time 2185.01 (run time 0 hr, 36 min, 25 sec) system time 689.15 input time 0.00 clausify time 0.00 hyper_res time 845.48 pre_process time 1215.06 demod time 0.00 weigh cl time 271.12 for_sub time 272.29 renumber time 270.75 keep cl time 18.23 print_cl time 0.00 conflict time 3.61 post_process time 26.66 back demod time 0.00 back_sub time 25.92 lex_rpo time 0.00 The job finished Wed Jun 3 14:26:09 1992