----- 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 thm8.in". The process ID is 16999. % Reading file thm8.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(geometric_rule). set(geometric_rewrite_before). set(para_from). set(para_into). set(para_from_vars). set(para_into_vars). set(order_eq). set(back_demod). dependent: set(dynamic_demod). set(process_input). set(lrpo). clear(process_input). assign(max_weight,15). lex([A,e,_*_,_+_]). list(usable). 1 [] x=x. end_of_list. list(sos). 2 [] x+e=x. 3 [] e+x=x. 4 [] x* (y*x)=y. 5 [] x*y=y*x. end_of_list. list(demodulators). 6 [] x+e=x. 7 [] x* (y*x)=y. end_of_list. list(passive). 8 [] A+B!=e* (A*B). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=5) 2 [] x+e=x. given clause #2: (wt=5) 3 [] e+x=x. given clause #3: (wt=7) 4 [] x* (y*x)=y. given clause #4: (wt=7) 5 [] x*y=y*x. given clause #5: (wt=7) 9 [para_into,3.1.1.2,3.1.2] e+ (e+x)=x. given clause #6: (wt=9) 11 [para_into,4.1.1.1,3.1.2] (e+x)* (y*x)=y. given clause #7: (wt=9) 33 [para_into,9.1.1.2.2,3.1.1,gL-id] x+ (e+y)=x+y. given clause #8: (wt=7) 15 [para_into,4.1.1.2,4.1.1] (x*y)*x=y. given clause #9: (wt=15) 35 [para_into,11.1.1.2.1,11.1.1,gL-id] (x+y)* (z*y)= (x+u)* (z*u). given clause #10: (wt=7) 25 [para_into,5.1.1,4.1.1,flip.1] (x*y)*y=x. given clause #11: (wt=11) 19 [para_into,5.1.1.1,5.1.2] (x*y)*z=z* (y*x). given clause #12: (wt=7) 29 [back_demod,17,demod,28] x* (x*y)=y. given clause #13: (wt=9) 27 [para_into,5.1.1,3.1.2] e+ (x*y)=y*x. given clause #14: (wt=9) 41 [para_into,33.1.1.1,3.1.2,demod,34] (e+x)+y=x+y. given clause #15: (wt=11) 115 [para_into,27.1.2,3.1.2,gL-id] x+ (y*z)=x+ (z*y). given clause #16: (wt=11) 22 [para_into,5.1.1.2,5.1.2] x* (y*z)= (z*y)*x. given clause #17: (wt=15) 116 [para_from,27.1.1,33.1.1.2.2,gL-id] x+ (y+ (z*u))=x+ (y+ (u*z)). given clause #18: (wt=9) 49 [para_into,15.1.1.1,11.1.1] x* (e+y)=x*y. given clause #19: (wt=15) 117 [para_into,41.1.1.1.2,27.1.1,gL-id] (x+ (y*z))+u= (x+ (z*y))+u. given clause #20: (wt=9) 51 [para_from,15.1.1,11.1.1.2] (e+x)*y=x*y. given clause #21: (wt=11) 31 [para_from,5.1.1,4.1.1.2.2] (x*y)* (z* (y*x))=z. given clause #22: (wt=11) 40 [para_into,33.1.1.1,5.1.2,demod,34] (x*y)+z= (y*x)+z. given clause #23: (wt=11) 43 [para_into,15.1.1.1.1,5.1.2] ((x*y)*z)* (y*x)=z. given clause #24: (wt=11) 66 [para_into,25.1.1.1.2,5.1.2] (x* (y*z))* (z*y)=x. given clause #25: (wt=11) 77 [para_into,19.1.1,5.1.2] x* (y*z)=x* (z*y). given clause #26: (wt=13) 53 [para_into,35.1.1.1,2.1.1] x* (y*e)= (x+z)* (y*z). given clause #27: (wt=9) 194 [back_demod,106,demod,180] x* (e* (x+y))=y. given clause #28: (wt=9) 225 [para_from,194.1.1,29.1.1.2,flip.1] e* (x+y)=x*y. ----> UNIT CONFLICT at 0.07 sec ----> 233 [binary,231.1,8.1] $F. Length of proof is 11. Level of proof is 7. ---------------- PROOF ---------------- 2 [] x+e=x. 3 [] e+x=x. 4 [] x* (y*x)=y. 5 [] x*y=y*x. 8 [] A+B!=e* (A*B). 11 [para_into,4.1.1.1,3.1.2] (e+x)* (y*x)=y. 17 [para_into,4.1.1.2,3.1.2] x* (e+ (y*x))=y. 28,27 [para_into,5.1.1,3.1.2] e+ (x*y)=y*x. 29 [back_demod,17,demod,28] x* (x*y)=y. 35 [para_into,11.1.1.2.1,11.1.1,gL-id] (x+y)* (z*y)= (x+u)* (z*u). 53 [para_into,35.1.1.1,2.1.1] x* (y*e)= (x+z)* (y*z). 106 [para_into,29.1.1,35.1.2] (x+y)* ((x+z)*y)=z. 180,179 [para_into,53.1.1.2,5.1.2,flip.1] (x+y)* (z*y)=x* (e*z). 194 [back_demod,106,demod,180] x* (e* (x+y))=y. 225 [para_from,194.1.1,29.1.1.2,flip.1] e* (x+y)=x*y. 231 [para_from,225.1.1,29.1.1.2,flip.1] x+y=e* (x*y). 233 [binary,231.1,8.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 28 clauses generated 9335 para_from generated 3883 para_into generated 5403 gL rule generated 49 demod & eval rewrites 10725 clauses wt,lit,sk delete 2038 tautologies deleted 0 clauses forward subsumed 7207 (subsumed by sos) 630 unit deletions 0 factor simplifications 0 clauses kept 159 new demodulators 65 empty clauses 1 clauses back demodulated 69 clauses back subsumed 0 usable size 23 sos size 72 demodulators size 36 passive size 1 hot size 0 Kbytes malloced 1953 ----------- times (seconds) ----------- user CPU time 0.07 (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 16999 finished Mon Nov 14 15:26:22 2005