----- Otter 3.3f, August 2004 ----- The process was started by mccune on cleo.thornwood, Mon Nov 14 15:26:22 2005 The command was "otter33f -f thm4.in". The process ID is 16996. % Reading file thm4.in. op(400,xfx,[*,+,^,v,/,\,#]). op(300,yf,@). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio,4). assign(max_mem,20000). 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(process_input). dependent: set(lrpo). set(hyper_res). set(para_from_units_only). set(para_into_units_only). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] x* (y*x)=y. 0 [] x*y=y*x. 0 [] e*e=e. 0 [] (x*e)+ (e*y)=x*y. 0 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. end_of_list. list(passive). 1 [] A+B!=e* (A*B). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 2 [] x=x. Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=7): 3 [] x* (y*x)=y. ---> New Demodulator: 4 [new_demod,3] x* (y*x)=y. ** KEPT (pick-wt=7): 5 [] x*y=y*x. ** KEPT (pick-wt=5): 6 [] e*e=e. ---> New Demodulator: 7 [new_demod,6] e*e=e. ** KEPT (pick-wt=11): 8 [] (x*e)+ (e*y)=x*y. ---> New Demodulator: 9 [new_demod,8] (x*e)+ (e*y)=x*y. ** KEPT (pick-wt=22): 10 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. >>>> Starting back demodulation with 4. Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] x*y=y*x. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=7) 3 [] x* (y*x)=y. given clause #2: (wt=5) 6 [] e*e=e. given clause #3: (wt=7) 5 [] x*y=y*x. given clause #4: (wt=7) 11 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. given clause #5: (wt=7) 13 [para_into,5.1.1,3.1.1,flip.1] (x*y)*y=x. given clause #6: (wt=11) 8 [] (x*e)+ (e*y)=x*y. given clause #7: (wt=7) 15 [para_from,5.1.1,3.1.1.2] x* (x*y)=y. given clause #8: (wt=11) 17 [para_into,8.1.1.1,13.1.1] x+ (e*y)= (x*e)*y. 30 back subsumes 29. 32 back subsumes 31. given clause #9: (wt=11) 19 [para_into,8.1.1.1,11.1.1,demod,18] (x*e)*y= (e*x)*y. given clause #10: (wt=11) 26 [copy,19,flip.1] (e*x)*y= (x*e)*y. given clause #11: (wt=22) 10 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. given clause #12: (wt=11) 27 [para_into,17.1.1.2,15.1.1] x+y= (x*e)* (e*y). given clause #13: (wt=11) 30 [back_demod,24,demod,28,14] x* (e*y)=x* (y*e). given clause #14: (wt=11) 32 [copy,30,flip.1] x* (y*e)=x* (e*y). given clause #15: (wt=11) 33 [para_into,19.1.1,15.1.1,flip.1] (e*x)* ((x*e)*y)=y. given clause #16: (wt=11) 35 [para_into,19.1.1,5.1.1] x* (y*e)= (e*y)*x. given clause #17: (wt=11) 36 [para_into,19.1.1,3.1.1,flip.1] (e*x)* (y* (x*e))=y. given clause #18: (wt=11) 38 [copy,35,flip.1] (e*x)*y=y* (x*e). given clause #19: (wt=11) 39 [para_from,19.1.1,15.1.1.2] (x*e)* ((e*x)*y)=y. given clause #20: (wt=11) 41 [para_from,19.1.1,11.1.1.1] ((e*x)*y)* (x*e)=y. given clause #21: (wt=11) 43 [para_into,26.1.1,5.1.1] x* (e*y)= (y*e)*x. given clause #22: (wt=11) 44 [para_into,26.1.1,3.1.1,flip.1] (x*e)* (y* (e*x))=y. given clause #23: (wt=11) 46 [copy,43,flip.1] (x*e)*y=y* (e*x). given clause #24: (wt=11) 47 [para_from,26.1.1,11.1.1.1] ((x*e)*y)* (e*x)=y. given clause #25: (wt=11) 58 [para_into,30.1.1,13.1.1,flip.1] (x* (e*y))* (y*e)=x. given clause #26: (wt=19) 49 [hyper,10,15] (x*y)* ((z*y)* ((z*u)*v))= (x*u)*v. 124 back subsumes 73. 124 back subsumes 64. 212 back subsumes 74. 212 back subsumes 65. given clause #27: (wt=11) 62 [para_from,30.1.1,13.1.1.1] (x* (y*e))* (e*y)=x. given clause #28: (wt=15) 50 [hyper,10,11] (x* ((y*z)*u))*y= (x*z)*u. given clause #29: (wt=13) 296 [para_into,50.1.1.1.2.1,6.1.1] (x* (e*y))*e= (x*e)*y. ----> UNIT CONFLICT at 0.02 sec ----> 494 [binary,492.1,1.1] $F. Length of proof is 15. Level of proof is 9. ---------------- PROOF ---------------- 1 [] A+B!=e* (A*B). 3 [] x* (y*x)=y. 5 [] x*y=y*x. 6 [] e*e=e. 8 [] (x*e)+ (e*y)=x*y. 10 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. 11 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. 13 [para_into,5.1.1,3.1.1,flip.1] (x*y)*y=x. 16,15 [para_from,5.1.1,3.1.1.2] x* (x*y)=y. 18,17 [para_into,8.1.1.1,13.1.1] x+ (e*y)= (x*e)*y. 19 [para_into,8.1.1.1,11.1.1,demod,18] (x*e)*y= (e*x)*y. 26 [copy,19,flip.1] (e*x)*y= (x*e)*y. 27 [para_into,17.1.1.2,15.1.1] x+y= (x*e)* (e*y). 44 [para_into,26.1.1,3.1.1,flip.1] (x*e)* (y* (e*x))=y. 50 [hyper,10,11] (x* ((y*z)*u))*y= (x*z)*u. 296 [para_into,50.1.1.1.2.1,6.1.1] (x* (e*y))*e= (x*e)*y. 303 [para_into,50.1.1.1.2,44.1.1] (x*y)*z= (x*e)* (y* (e*z)). 349 [copy,303,flip.1] (x*e)* (y* (e*z))= (x*y)*z. 424,423 [para_into,296.1.1,5.1.1,flip.1] (x*e)*y=e* (x* (e*y)). 445,444 [back_demod,349,demod,424,flip.1] (x*y)*z=e* (x* (e* (y* (e*z)))). 492 [back_demod,27,demod,445,16,16] x+y=e* (x*y). 494 [binary,492.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 29 clauses generated 1140 hyper_res generated 22 para_from generated 397 para_into generated 721 demod & eval rewrites 2642 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 1167 (subsumed by sos) 248 unit deletions 0 factor simplifications 0 clauses kept 416 new demodulators 76 empty clauses 1 clauses back demodulated 135 clauses back subsumed 6 usable size 20 sos size 255 demodulators size 52 passive size 1 hot size 0 Kbytes malloced 1953 ----------- times (seconds) ----------- user CPU time 0.02 (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) That finishes the proof of the theorem. Process 16996 finished Mon Nov 14 15:26:22 2005