----- 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 5711. 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(e(x,y))| -P(x)|P(y). 0 [] P(e(e(x,y),e(e(x,z),e(z,y)))). 0 [] -P(e(e(a,b),e(e(c,b),e(a,c)))). 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(e(x,y))| -P(x)|P(y). ** KEPT (pick-wt=12): 2 [] -P(e(e(a,b),e(e(c,b),e(a,c)))). ------------> process sos: ** KEPT (pick-wt=12): 3 [] P(e(e(x,y),e(e(x,z),e(z,y)))). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=12) 3 [] P(e(e(x,y),e(e(x,z),e(z,y)))). given clause #2: (wt=16) 4 [hyper,3,1,3] P(e(e(e(x,y),z),e(z,e(e(x,u),e(u,y))))). given clause #3: (wt=16) 7 [hyper,4,1,3] P(e(e(e(x,y),e(y,z)),e(e(x,u),e(u,z)))). given clause #4: (wt=12) 8 [hyper,7,1,7] P(e(e(e(x,x),y),e(y,e(z,z)))). given clause #5: (wt=12) 11 [hyper,7,1,3] P(e(e(x,y),e(y,e(z,e(x,z))))). given clause #6: (wt=20) 5 [hyper,4,1,4] P(e(e(x,e(e(y,z),e(z,u))),e(e(e(y,u),v),e(v,x)))). given clause #7: (wt=12) 12 [hyper,8,1,8] P(e(e(e(x,x),e(y,y)),e(z,z))). given clause #8: (wt=4) 33 [hyper,12,1,12] P(e(x,x)). given clause #9: (wt=8) 35 [hyper,12,1,8] P(e(e(x,x),e(y,y))). given clause #10: (wt=8) 39 [hyper,33,1,11] P(e(x,e(y,e(x,y)))). given clause #11: (wt=20) 6 [hyper,4,1,3] P(e(e(e(e(x,y),z),u),e(u,e(z,e(e(x,v),e(v,y)))))). given clause #12: (wt=8) 40 [hyper,33,1,7] P(e(e(x,y),e(y,x))). given clause #13: (wt=8) 50 [hyper,39,1,33] P(e(x,e(e(y,y),x))). given clause #14: (wt=8) 79 [hyper,40,1,39] P(e(e(x,e(y,x)),y)). given clause #15: (wt=8) 86 [hyper,50,1,40] P(e(e(e(x,x),y),y)). given clause #16: (wt=20) 9 [hyper,7,1,4] P(e(e(e(x,y),e(y,z)),e(e(e(x,u),v),e(v,e(u,z))))). given clause #17: (wt=12) 15 [hyper,8,1,7] P(e(e(e(x,y),e(y,x)),e(z,z))). given clause #18: (wt=12) 18 [hyper,11,1,8] P(e(e(x,e(y,e(x,y))),e(z,z))). given clause #19: (wt=12) 27 [hyper,5,1,7] P(e(e(x,y),e(y,e(e(z,z),x)))). given clause #20: (wt=12) 41 [hyper,35,1,11] P(e(e(x,x),e(y,e(e(z,z),y)))). given clause #21: (wt=20) 10 [hyper,7,1,3] P(e(e(e(e(x,y),e(y,z)),u),e(u,e(e(x,v),e(v,z))))). given clause #22: (wt=12) 42 [hyper,35,1,4] P(e(e(x,x),e(e(y,z),e(z,y)))). given clause #23: (wt=12) 43 [hyper,39,1,39] P(e(x,e(e(y,e(z,e(y,z))),x))). given clause #24: (wt=12) 44 [hyper,39,1,11] P(e(e(x,e(y,x)),e(z,e(y,z)))). given clause #25: (wt=12) 45 [hyper,39,1,8] P(e(e(x,e(e(y,y),x)),e(z,z))). given clause #26: (wt=16) 13 [hyper,8,1,4] P(e(e(x,e(y,y)),e(e(e(z,z),u),e(u,x)))). given clause #27: (wt=12) 46 [hyper,39,1,7] P(e(e(x,y),e(y,e(e(x,z),z)))). given clause #28: (wt=8) 263 [hyper,46,1,86] P(e(x,e(e(x,y),y))). given clause #29: (wt=8) 304 [hyper,263,1,40] P(e(e(e(x,y),y),x)). given clause #30: (wt=12) 47 [hyper,39,1,5] P(e(e(e(x,e(x,y)),z),e(z,y))). given clause #31: (wt=16) 14 [hyper,8,1,3] P(e(e(e(e(x,x),y),z),e(z,e(y,e(u,u))))). given clause #32: (wt=8) 352 [hyper,47,1,86] P(e(e(x,e(x,y)),y)). given clause #33: (wt=8) 372 [hyper,47,1,40] P(e(e(e(x,y),x),y)). given clause #34: (wt=8) 399 [hyper,14,1,304] P(e(x,e(x,e(y,y)))). given clause #35: (wt=8) 419 [hyper,352,1,40] P(e(x,e(y,e(y,x)))). given clause #36: (wt=16) 16 [hyper,8,1,4] P(e(e(e(x,y),e(e(x,z),e(z,y))),e(u,u))). given clause #37: (wt=8) 431 [hyper,372,1,40] P(e(x,e(e(y,x),y))). given clause #38: (wt=8) 445 [hyper,399,1,40] P(e(e(x,e(y,y)),x)). given clause #39: (wt=12) 49 [hyper,39,1,35] P(e(x,e(e(e(y,y),e(z,z)),x))). given clause #40: (wt=12) 73 [hyper,40,1,39] P(e(x,e(e(e(y,z),e(z,y)),x))). given clause #41: (wt=16) 17 [hyper,11,1,11] P(e(e(x,e(y,e(z,y))),e(u,e(e(z,x),u)))). given clause #42: (wt=12) 74 [hyper,40,1,11] P(e(e(x,y),e(z,e(e(y,x),z)))). given clause #43: (wt=12) 77 [hyper,40,1,4] P(e(e(x,y),e(e(y,z),e(z,x)))). given clause #44: (wt=12) 78 [hyper,40,1,3] P(e(e(e(x,y),z),e(z,e(y,x)))). given clause #45: (wt=12) 80 [hyper,40,1,12] P(e(e(x,x),e(e(y,y),e(z,z)))). given clause #46: (wt=16) 19 [hyper,11,1,4] P(e(e(x,e(y,e(z,y))),e(e(z,u),e(u,x)))). given clause #47: (wt=12) 81 [hyper,40,1,11] P(e(e(x,e(y,e(z,y))),e(z,x))). given clause #48: (wt=12) 82 [hyper,40,1,8] P(e(e(x,e(y,y)),e(e(z,z),x))). given clause #49: (wt=12) 85 [hyper,40,1,3] P(e(e(e(x,y),e(y,z)),e(x,z))). -------- PROOF -------- ----> UNIT CONFLICT at 0.07 sec ----> 946 [binary,945.1,2.1] $F. Length of proof is 9. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -P(e(x,y))| -P(x)|P(y). 2 [] -P(e(e(a,b),e(e(c,b),e(a,c)))). 3 [] P(e(e(x,y),e(e(x,z),e(z,y)))). 4 [hyper,3,1,3] P(e(e(e(x,y),z),e(z,e(e(x,u),e(u,y))))). 7 [hyper,4,1,3] P(e(e(e(x,y),e(y,z)),e(e(x,u),e(u,z)))). 8 [hyper,7,1,7] P(e(e(e(x,x),y),e(y,e(z,z)))). 12 [hyper,8,1,8] P(e(e(e(x,x),e(y,y)),e(z,z))). 33 [hyper,12,1,12] P(e(x,x)). 40 [hyper,33,1,7] P(e(e(x,y),e(y,x))). 78 [hyper,40,1,3] P(e(e(e(x,y),z),e(z,e(y,x)))). 85 [hyper,40,1,3] P(e(e(e(x,y),e(y,z)),e(x,z))). 945 [hyper,85,1,78] P(e(e(x,y),e(e(z,y),e(x,z)))). 946 [binary,945.1,2.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 49 clauses generated 1839 clauses kept 945 clauses forward subsumed 897 clauses back subsumed 1 Kbytes malloced 670 ----------- times (seconds) ----------- user CPU time 0.07 (0 hr, 0 min, 0 sec) system CPU time 0.01 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.02 for_sub time 0.01 back_sub time 0.01 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 5711 finished Wed Aug 6 14:25:53 2003