----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:25:55 2003 The command was "../../bin/otter". The process ID is 5761. 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 [] x=x. 0 [] f(f(v,w,x),y,f(v,w,z))=f(v,w,f(x,y,z)). 0 [] f(y,x,x)=x. 0 [] f(x,x,y)=x. 0 [] f(g(y),y,x)=x. 0 [] f(x,y,g(y))=x. 0 [] g(g(a))!=a. end_of_list. SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. All clauses are units, and equality is present; the strategy will be Knuth-Bendix with positive clauses in sos. dependent: set(knuth_bendix). dependent: set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). ------------> process usable: ** KEPT (pick-wt=5): 1 [] g(g(a))!=a. ------------> process sos: ** KEPT (pick-wt=3): 2 [] x=x. ** KEPT (pick-wt=18): 3 [] f(f(x,y,z),u,f(x,y,v))=f(x,y,f(z,u,v)). ---> New Demodulator: 4 [new_demod,3] f(f(x,y,z),u,f(x,y,v))=f(x,y,f(z,u,v)). ** KEPT (pick-wt=6): 5 [] f(x,y,y)=y. ---> New Demodulator: 6 [new_demod,5] f(x,y,y)=y. ** KEPT (pick-wt=6): 7 [] f(x,x,y)=x. ---> New Demodulator: 8 [new_demod,7] f(x,x,y)=x. ** KEPT (pick-wt=7): 9 [] f(g(x),x,y)=y. ---> New Demodulator: 10 [new_demod,9] f(g(x),x,y)=y. ** KEPT (pick-wt=7): 11 [] f(x,y,g(y))=x. ---> New Demodulator: 12 [new_demod,11] f(x,y,g(y))=x. Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x=x. >>>> Starting back demodulation with 4. >>>> Starting back demodulation with 6. >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=3) 2 [] x=x. given clause #2: (wt=6) 5 [] f(x,y,y)=y. given clause #3: (wt=6) 7 [] f(x,x,y)=x. given clause #4: (wt=7) 9 [] f(g(x),x,y)=y. given clause #5: (wt=7) 11 [] f(x,y,g(y))=x. given clause #6: (wt=18) 3 [] f(f(x,y,z),u,f(x,y,v))=f(x,y,f(z,u,v)). given clause #7: (wt=6) 14 [para_into,3.1.1.1,7.1.1,demod,8,8] f(x,y,x)=x. given clause #8: (wt=15) 16 [para_into,3.1.1.1,5.1.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)). given clause #9: (wt=12) 37 [para_into,16.1.1.3,14.1.1,flip.1] f(x,y,f(y,z,x))=f(y,z,x). given clause #10: (wt=13) 39 [para_into,16.1.1.3,11.1.1] f(x,y,z)=f(z,x,f(x,y,g(x))). given clause #11: (wt=16) 13 [para_into,3.1.1.1,11.1.1] f(x,y,f(x,z,u))=f(x,z,f(g(z),y,u)). given clause #12: (wt=10) 60 [para_into,39.1.1,5.1.1,flip.1] f(x,y,f(y,x,g(y)))=x. given clause #13: (wt=10) 71 [para_into,13.1.1.3,14.1.1,demod,15,flip.1] f(x,y,f(g(y),z,x))=x. given clause #14: (wt=10) 80 [para_into,13.1.1,7.1.1,flip.1] f(x,y,f(g(y),x,z))=x. given clause #15: (wt=10) 120 [para_into,80.1.1.3,37.1.1] f(x,y,f(x,z,g(y)))=x. given clause #16: (wt=30) 17 [para_into,3.1.1.1,3.1.1] f(f(x,y,f(z,u,v)),w,f(f(x,y,z),u,v6))=f(f(x,y,z),u,f(f(x,y,v),w,v6)). given clause #17: (wt=10) 126 [para_into,80.1.1,39.1.1,demod,57] f(g(x),y,f(y,x,z))=y. given clause #18: (wt=7) 242 [para_into,126.1.1.3,5.1.1] f(g(x),y,x)=y. -------- PROOF -------- ----> UNIT CONFLICT at 0.03 sec ----> 266 [binary,264.1,1.1] $F. Length of proof is 8. Level of proof is 6. ---------------- PROOF ---------------- 1 [] g(g(a))!=a. 3 [] f(f(x,y,z),u,f(x,y,v))=f(x,y,f(z,u,v)). 5 [] f(x,y,y)=y. 7 [] f(x,x,y)=x. 11 [] f(x,y,g(y))=x. 13 [para_into,3.1.1.1,11.1.1] f(x,y,f(x,z,u))=f(x,z,f(g(z),y,u)). 16 [para_into,3.1.1.1,5.1.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)). 39 [para_into,16.1.1.3,11.1.1] f(x,y,z)=f(z,x,f(x,y,g(x))). 57,56 [para_into,39.1.1,16.1.1,flip.1] f(f(x,y,z),y,f(y,u,g(y)))=f(x,y,f(y,u,z)). 80 [para_into,13.1.1,7.1.1,flip.1] f(x,y,f(g(y),x,z))=x. 126 [para_into,80.1.1,39.1.1,demod,57] f(g(x),y,f(y,x,z))=y. 242 [para_into,126.1.1.3,5.1.1] f(g(x),y,x)=y. 264 [para_into,242.1.1,11.1.1] g(g(x))=x. 266 [binary,264.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 18 clauses generated 379 clauses kept 165 clauses forward subsumed 308 clauses back subsumed 0 Kbytes malloced 510 ----------- times (seconds) ----------- user CPU time 0.03 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) para_into time 0.00 para_from time 0.00 for_sub time 0.01 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 5761 finished Wed Aug 6 14:25:55 2003