----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:25:53 2003 The command was "../../bin/otter". The process ID is 5726. set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). list(usable). 0 [] -P(i(x,y))| -P(x)|P(y). 0 [] P(i(x,i(y,x))). 0 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 0 [] P(i(i(i(x,y),y),i(i(y,x),x))). 0 [] P(i(i(n(x),n(y)),i(y,x))). 0 [] -P(i(i(a,b),i(i(c,a),i(c,b))))|$ANS(MV_25). end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. This is a Horn set without equality. The strategy will be hyperresolution, with satellites in sos and nuclei in usable. dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -P(i(x,y))| -P(x)|P(y). ** KEPT (pick-wt=12): 2 [] -P(i(i(a,b),i(i(c,a),i(c,b))))|$ANS(MV_25). ------------> process sos: ** KEPT (pick-wt=6): 3 [] P(i(x,i(y,x))). ** KEPT (pick-wt=12): 4 [] P(i(i(x,y),i(i(y,z),i(x,z)))). ** KEPT (pick-wt=12): 5 [] P(i(i(i(x,y),y),i(i(y,x),x))). ** KEPT (pick-wt=10): 6 [] P(i(i(n(x),n(y)),i(y,x))). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=6) 3 [] P(i(x,i(y,x))). given clause #2: (wt=8) 7 [hyper,3,1,3] P(i(x,i(y,i(z,y)))). given clause #3: (wt=10) 6 [] P(i(i(n(x),n(y)),i(y,x))). given clause #4: (wt=10) 8 [hyper,7,1,3] P(i(x,i(y,i(z,i(u,z))))). given clause #5: (wt=12) 4 [] P(i(i(x,y),i(i(y,z),i(x,z)))). given clause #6: (wt=12) 5 [] P(i(i(i(x,y),y),i(i(y,x),x))). given clause #7: (wt=10) 16 [hyper,4,1,3] P(i(i(i(x,y),z),i(y,z))). given clause #8: (wt=7) 23 [hyper,16,1,6] P(i(n(x),i(x,y))). given clause #9: (wt=8) 24 [hyper,16,1,5] P(i(x,i(i(x,y),y))). given clause #10: (wt=8) 26 [hyper,16,1,3] P(i(x,i(y,i(z,x)))). given clause #11: (wt=12) 9 [hyper,6,1,3] P(i(x,i(i(n(y),n(z)),i(z,y)))). given clause #12: (wt=9) 28 [hyper,23,1,3] P(i(x,i(n(y),i(y,z)))). given clause #13: (wt=10) 20 [hyper,5,1,7] P(i(i(i(x,i(y,x)),z),z)). given clause #14: (wt=4) 59 [hyper,20,1,16] P(i(x,x)). given clause #15: (wt=6) 64 [hyper,59,1,3] P(i(x,i(y,y))). given clause #16: (wt=12) 10 [hyper,8,1,3] P(i(x,i(y,i(z,i(u,i(v,u)))))). given clause #17: (wt=8) 62 [hyper,59,1,26] P(i(x,i(y,i(z,z)))). given clause #18: (wt=8) 63 [hyper,59,1,24] P(i(i(i(x,x),y),y)). given clause #19: (wt=10) 25 [hyper,16,1,4] P(i(x,i(i(x,y),i(z,y)))). given clause #20: (wt=10) 30 [hyper,24,1,16] P(i(x,i(i(i(y,x),z),z))). given clause #21: (wt=16) 11 [hyper,4,1,4] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). given clause #22: (wt=10) 32 [hyper,24,1,3] P(i(x,i(y,i(i(y,z),z)))). given clause #23: (wt=10) 41 [hyper,26,1,16] P(i(x,i(y,i(z,i(u,x))))). given clause #24: (wt=10) 43 [hyper,26,1,3] P(i(x,i(y,i(z,i(u,y))))). given clause #25: (wt=10) 65 [hyper,64,1,26] P(i(x,i(y,i(z,i(u,u))))). given clause #26: (wt=14) 12 [hyper,4,1,3] P(i(x,i(i(y,z),i(i(z,u),i(y,u))))). given clause #27: (wt=10) 66 [hyper,64,1,24] P(i(i(i(x,i(y,y)),z),z)). given clause #28: (wt=10) 67 [hyper,64,1,4] P(i(i(i(x,x),y),i(z,y))). given clause #29: (wt=10) 77 [hyper,63,1,3] P(i(x,i(i(i(y,y),z),z))). given clause #30: (wt=10) 126 [hyper,11,1,20] P(i(i(x,y),i(x,i(z,y)))). given clause #31: (wt=14) 13 [hyper,4,1,8] P(i(i(i(x,i(y,i(z,y))),u),i(v,u))). given clause #32: (wt=9) 193 [hyper,126,1,23] P(i(n(x),i(y,i(x,z)))). given clause #33: (wt=10) 192 [hyper,126,1,24] P(i(x,i(y,i(i(x,z),z)))). given clause #34: (wt=11) 27 [hyper,23,1,4] P(i(i(i(x,y),z),i(n(x),z))). given clause #35: (wt=7) 269 [hyper,27,1,63] P(i(n(i(x,x)),y)). given clause #36: (wt=12) 14 [hyper,4,1,7] P(i(i(i(x,i(y,x)),z),i(u,z))). given clause #37: (wt=8) 278 [hyper,27,1,6] P(i(n(n(x)),i(y,x))). given clause #38: (wt=9) 268 [hyper,27,1,66] P(i(n(i(x,i(y,y))),z)). given clause #39: (wt=9) 274 [hyper,27,1,20] P(i(n(i(x,i(y,x))),z)). given clause #40: (wt=9) 275 [hyper,27,1,16] P(i(n(i(x,y)),i(y,z))). given clause #41: (wt=14) 15 [hyper,4,1,6] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))). given clause #42: (wt=9) 287 [hyper,269,1,3] P(i(x,i(n(i(y,y)),z))). given clause #43: (wt=10) 259 [hyper,27,1,27] P(i(n(i(x,y)),i(n(x),z))). given clause #44: (wt=10) 298 [hyper,278,1,126] P(i(n(n(x)),i(y,i(z,x)))). given clause #45: (wt=10) 305 [hyper,278,1,3] P(i(x,i(n(n(y)),i(z,y)))). given clause #46: (wt=16) 17 [hyper,5,1,4] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))). given clause #47: (wt=10) 348 [hyper,15,1,63] P(i(i(n(x),n(i(y,y))),x)). given clause #48: (wt=6) 418 [hyper,348,1,27] P(i(n(n(x)),x)). given clause #49: (wt=6) 426 [hyper,418,1,348] P(n(n(i(x,x)))). given clause #50: (wt=6) 433 [hyper,418,1,6] P(i(x,n(n(x)))). given clause #51: (wt=14) 18 [hyper,5,1,3] P(i(x,i(i(i(y,z),z),i(i(z,y),y)))). given clause #52: (wt=8) 435 [hyper,418,1,3] P(i(x,i(n(n(y)),y))). given clause #53: (wt=8) 442 [hyper,426,1,3] P(i(x,n(n(i(y,y))))). given clause #54: (wt=8) 443 [hyper,433,1,433] P(n(n(i(x,n(n(x)))))). given clause #55: (wt=8) 445 [hyper,433,1,126] P(i(x,i(y,n(n(x))))). given clause #56: (wt=12) 19 [hyper,5,1,8] P(i(i(i(x,i(y,i(z,y))),u),u)). given clause #57: (wt=8) 446 [hyper,433,1,66] P(n(n(i(x,i(y,y))))). given clause #58: (wt=8) 453 [hyper,433,1,20] P(n(n(i(x,i(y,x))))). given clause #59: (wt=8) 455 [hyper,433,1,16] P(i(x,n(n(i(y,x))))). given clause #60: (wt=8) 461 [hyper,433,1,3] P(i(x,i(y,n(n(y))))). given clause #61: (wt=14) 21 [hyper,16,1,4] P(i(i(i(x,y),z),i(i(i(u,x),y),z))). given clause #62: (wt=8) 462 [hyper,433,1,426] P(n(n(n(n(i(x,x)))))). given clause #63: (wt=8) 463 [hyper,433,1,418] P(n(n(i(n(n(x)),x)))). given clause #64: (wt=8) 640 [hyper,455,1,6] P(i(n(i(x,n(y))),y)). given clause #65: (wt=9) 449 [hyper,433,1,27] P(i(n(x),n(n(i(x,y))))). given clause #66: (wt=12) 22 [hyper,16,1,3] P(i(x,i(i(i(y,z),u),i(z,u)))). given clause #67: (wt=7) 768 [hyper,449,1,6] P(i(n(i(x,y)),x)). given clause #68: (wt=7) 790 [hyper,768,1,6] P(i(x,i(n(x),y))). given clause #69: (wt=9) 471 [hyper,433,1,269] P(n(n(i(n(i(x,x)),y)))). given clause #70: (wt=9) 492 [hyper,433,1,23] P(n(n(i(n(x),i(x,y))))). given clause #71: (wt=12) 29 [hyper,24,1,24] P(i(i(i(x,i(i(x,y),y)),z),z)). given clause #72: (wt=9) 531 [hyper,443,1,23] P(i(n(i(x,n(n(x)))),y)). given clause #73: (wt=9) 735 [hyper,462,1,23] P(i(n(n(n(i(x,x)))),y)). given clause #74: (wt=9) 746 [hyper,463,1,23] P(i(n(i(n(n(x)),x)),y)). given clause #75: (wt=9) 782 [hyper,768,1,433] P(n(n(i(n(i(x,y)),x)))). given clause #76: (wt=12) 31 [hyper,24,1,4] P(i(i(i(i(x,y),y),z),i(x,z))). -------- PROOF -------- 978 [binary,977.1,2.1] $ANS(MV_25). ----> UNIT CONFLICT at 0.05 sec ----> 978 [binary,977.1,2.1] $ANS(MV_25). Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 2 [] -P(i(i(a,b),i(i(c,a),i(c,b))))|$ANS(MV_25). 3 [] P(i(x,i(y,x))). 4 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 5 [] P(i(i(i(x,y),y),i(i(y,x),x))). 11 [hyper,4,1,4] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 16 [hyper,4,1,3] P(i(i(i(x,y),z),i(y,z))). 24 [hyper,16,1,5] P(i(x,i(i(x,y),y))). 31 [hyper,24,1,4] P(i(i(i(i(x,y),y),z),i(x,z))). 977 [hyper,31,1,11] P(i(i(x,y),i(i(z,x),i(z,y)))). 978 [binary,977.1,2.1] $ANS(MV_25). ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 76 clauses generated 3375 clauses kept 977 clauses forward subsumed 2404 clauses back subsumed 7 Kbytes malloced 670 ----------- times (seconds) ----------- user CPU time 0.05 (0 hr, 0 min, 0 sec) system CPU time 0.03 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 for_sub time 0.01 back_sub time 0.00 conflict time 0.00 That finishes the proof of the theorem. Process 5726 finished Wed Aug 6 14:25:54 2003