----- 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 thm3.in". The process ID is 16995. % Reading file thm3.in. op(400,xfx,[*,+,^,v,/,\,#]). lrpo_multiset_status([_*_]). 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). clear(print_kept). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] x* (y*x)=y. 0 [] x*y=y*x. 0 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. end_of_list. list(passive). 1 [] (A*B)* (C*D)!= (A*C)* (B*D). 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=22): 6 [] (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. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=7) 3 [] x* (y*x)=y. ---> New Demodulator: 8 [new_demod,7] (x*y)*x=y. >>>> Starting back demodulation with 8. given clause #2: (wt=7) 5 [] x*y=y*x. ---> New Demodulator: 10 [new_demod,9] (x*y)*y=x. >>>> Starting back demodulation with 10. ---> New Demodulator: 12 [new_demod,11] x* (x*y)=y. >>>> Starting back demodulation with 12. given clause #3: (wt=7) 7 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. given clause #4: (wt=7) 9 [para_into,5.1.1,3.1.1,flip.1] (x*y)*y=x. given clause #5: (wt=7) 11 [para_from,5.1.1,3.1.1.2] x* (x*y)=y. given clause #6: (wt=22) 6 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. ---> New Demodulator: 15 [new_demod,14] (x* ((y*z)*u))*y= (x*z)*u. >>>> Starting back demodulation with 15. given clause #7: (wt=15) 14 [hyper,6,7] (x* ((y*z)*u))*y= (x*z)*u. ---> New Demodulator: 25 [new_demod,24] (x* ((y*z)*u))*z= (x*y)*u. ---> New Demodulator: 29 [new_demod,28] (x* (y* (z*u)))*z= (x*u)*y. ---> New Demodulator: 32 [new_demod,31] ((x* ((((y*z)*u)*v)*w))*z)*u= ((x*v)*w)*y. ---> New Demodulator: 34 [new_demod,33] ((((x*y)*z)*u)*y)*z=u*x. ---> New Demodulator: 36 [new_demod,35] (((x*y)*z)*u)*x= (u*y)*z. ---> New Demodulator: 38 [new_demod,37] x* (y* ((x*z)*u))= (y*z)*u. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 38. ---> New Demodulator: 46 [new_demod,45] (x* ((y*z)*u))* ((x*z)*u)=y. ---> New Demodulator: 49 [new_demod,48] ((x*y)*z)* (x* ((u*y)*z))=u. >>>> Starting back demodulation with 46. >>>> Starting back demodulation with 49. given clause #8: (wt=15) 16 [hyper,6,5] (x*y)* (z*u)= (x*u)* (z*y). ---> New Demodulator: 81 [new_demod,80] (x* (((y*z)* (u*v))*w))* (y*v)= (x* (u*z))*w. ---> New Demodulator: 83 [new_demod,82] (x*y)* ((x*z)* (u*y))=u*z. ---> New Demodulator: 85 [new_demod,84] ((x*y)* (z*u))* (z*y)=x*u. ---> New Demodulator: 87 [new_demod,86] ((x*y)* (z*u))* (x*u)=z*y. ---> New Demodulator: 89 [new_demod,88] (x*y)* ((z*y)* (x*u))=z*u. >>>> Starting back demodulation with 81. >>>> Starting back demodulation with 83. >>>> Starting back demodulation with 85. >>>> Starting back demodulation with 87. >>>> Starting back demodulation with 89. given clause #9: (wt=15) 21 [para_into,14.1.1.1.2.1,11.1.1] (x* (y*z))*u= (x* (u*y))*z. ---> New Demodulator: 93 [new_demod,92] (x* (y* (z* ((u*v)*w))))*u= (x* ((z*v)*w))*y. ---> New Demodulator: 95 [new_demod,94] (x* (y* (z*u)))*u= (x*z)*y. ---> New Demodulator: 101 [new_demod,100] ((x* (((y*z)*u)*v))* (w*y))*z= ((x*u)*v)*w. ---> New Demodulator: 103 [new_demod,102] ((x* (y*z))* (u*y))*z=x*u. ---> New Demodulator: 105 [new_demod,104] (((x*y)*z)* (u*x))*y=z*u. ---> New Demodulator: 109 [new_demod,108] (x* (((x* (y*z))*u)*y))*z=u. >>>> Starting back demodulation with 93. >>>> Starting back demodulation with 95. >>>> Starting back demodulation with 101. >>>> Starting back demodulation with 103. >>>> Starting back demodulation with 105. >>>> Starting back demodulation with 109. ---> New Demodulator: 121 [new_demod,120] (x* (((y* (z*u))*v)*w))* (y* (u*v))= (x*z)*w. ---> New Demodulator: 125 [new_demod,124] (x* (y*z))* ((x* (u*y))*z)=u. ---> New Demodulator: 127 [new_demod,126] ((x* (y*z))*u)*y=x* (z*u). ---> New Demodulator: 129 [new_demod,128] ((x* (y*z))*u)* (x* (z*u))=y. ---> New Demodulator: 131 [new_demod,130] x* ((y* (x*z))*u)=y* (z*u). >>>> Starting back demodulation with 121. >>>> Starting back demodulation with 125. >>>> Starting back demodulation with 127. >> back demodulating 108 with 127. >>>> Starting back demodulation with 129. >>>> Starting back demodulation with 131. given clause #10: (wt=15) 22 [para_into,14.1.1.1.2.1,9.1.1] (x* (y*z))* (y*u)= (x*u)*z. ---> New Demodulator: 143 [new_demod,142] ((x* (((y*z)*u)*v))*w)*z= ((x*u)*v)* (y*w). ---> New Demodulator: 145 [new_demod,144] ((x* (y*z))*u)*z=x* (y*u). ---> New Demodulator: 147 [new_demod,146] (((x*y)*z)*u)*y=z* (x*u). ---> New Demodulator: 153 [new_demod,152] (x* ((y* ((z*u)*v))*w))* ((y*u)*v)= (x*z)*w. >>>> Starting back demodulation with 143. >> back demodulating 100 with 143. >> back demodulating 31 with 143. >>>> Starting back demodulation with 145. >> back demodulating 102 with 145. >>>> Starting back demodulation with 147. >> back demodulating 104 with 147. >> back demodulating 33 with 147. >>>> Starting back demodulation with 153. ---> New Demodulator: 173 [new_demod,172] (x* (y*z))* ((x*u)*z)=y*u. ---> New Demodulator: 175 [new_demod,174] ((x*y)*z)* (x* (u*z))=u*y. >>>> Starting back demodulation with 173. >> back demodulating 124 with 173. >> back demodulating 45 with 173. >>>> Starting back demodulation with 175. >> back demodulating 128 with 175. >> back demodulating 48 with 175. given clause #11: (wt=15) 23 [para_into,14.1.1.1.2.1,7.1.1] (x* (y*z))* (u*y)= (x*u)*z. ----> UNIT CONFLICT at 0.01 sec ----> 190 [binary,189.1,1.1] $F. Length of proof is 4. Level of proof is 4. ---------------- PROOF ---------------- 1 [] (A*B)* (C*D)!= (A*C)* (B*D). 3 [] x* (y*x)=y. 6 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. 7 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. 14 [hyper,6,7] (x* ((y*z)*u))*y= (x*z)*u. 23 [para_into,14.1.1.1.2.1,7.1.1] (x* (y*z))* (u*y)= (x*u)*z. 189 [para_into,23.1.1.1.2,3.1.1] (x*y)* (z*u)= (x*z)* (y*u). 190 [binary,189.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 11 clauses generated 232 hyper_res generated 10 para_from generated 88 para_into generated 134 demod & eval rewrites 109 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 203 (subsumed by sos) 87 unit deletions 0 factor simplifications 0 clauses kept 153 new demodulators 35 empty clauses 1 clauses back demodulated 10 clauses back subsumed 0 usable size 12 sos size 131 demodulators size 25 passive size 1 hot size 0 Kbytes malloced 976 ----------- times (seconds) ----------- user CPU time 0.01 (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 16995 finished Mon Nov 14 15:26:22 2005