----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:25:56 2003 The command was "../../bin/otter". The process ID is 5887. 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). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). set(sos_queue). assign(max_mem,5000). assign(stats_level,1). list(usable). 0 [] x=x. 0 [] x+y=y+x. 0 [] x*y=y*x. 0 [] (x+y)+z=x+y+z. 0 [] (x*y)*z=x*y*z. 0 [] x+x*y=x. 0 [] x* (x+y)=x. end_of_list. list(sos). 0 [] x+y*z= (x+y)* (x+z). 0 [] a* (b+c)!=a*b+a*c. end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] x=x. ** KEPT (pick-wt=7): 2 [] x+y=y+x. ** KEPT (pick-wt=7): 3 [] x*y=y*x. ** KEPT (pick-wt=11): 4 [] (x+y)+z=x+y+z. ---> New Demodulator: 5 [new_demod,4] (x+y)+z=x+y+z. ** KEPT (pick-wt=11): 6 [] (x*y)*z=x*y*z. ---> New Demodulator: 7 [new_demod,6] (x*y)*z=x*y*z. ** KEPT (pick-wt=7): 8 [] x+x*y=x. ---> New Demodulator: 9 [new_demod,8] x+x*y=x. ** KEPT (pick-wt=7): 10 [] x* (x+y)=x. ---> New Demodulator: 11 [new_demod,10] x* (x+y)=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x+y=y+x. Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x*y=y*x. >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. ------------> process sos: ** KEPT (pick-wt=13): 12 [] x+y*z= (x+y)* (x+z). ---> New Demodulator: 13 [new_demod,12] x+y*z= (x+y)* (x+z). ** KEPT (pick-wt=17): 15 [copy,14,demod,13,flip.1] (a*b+a)* (a*b+c)!=a* (b+c). >>>> Starting back demodulation with 13. >> back demodulating 8 with 13. >>>> Starting back demodulation with 17. ======= end of input processing ======= =========== start of search =========== Starting on level 1, last kept clause of level 0 is 17. Starting on level 1, last kept clause of level 0 is 17. given clause #1: (wt=13) 12 [] x+y*z= (x+y)* (x+z). given clause #2: (wt=17) 15 [copy,14,demod,13,flip.1] (a*b+a)* (a*b+c)!=a* (b+c). given clause #3: (wt=9) 16 [back_demod,8,demod,13] (x+x)* (x+y)=x. Starting on level 2, last kept clause of level 1 is 44. Starting on level 2, last kept clause of level 1 is 44. given clause #4: (wt=13) 18 [para_into,12.1.1.2,10.1.1,flip.1] (x+y)* (x+y+z)=x+y. given clause #5: (wt=13) 20 [para_into,12.1.1,2.1.1] x*y+z= (z+x)* (z+y). given clause #6: (wt=13) 21 [copy,20,flip.1] (x+y)* (x+z)=y*z+x. given clause #7: (wt=17) 24 [para_from,12.1.1,4.1.1.1] (x+y)* (x+z)+u=x+y*z+u. given clause #8: (wt=17) 26 [para_into,15.1.1.1.1,3.1.1] (b*a+a)* (a*b+c)!=a* (b+c). given clause #9: (wt=13) 27 [para_into,15.1.1.1,2.1.1,demod,13,17] a* (a*b+c)!=a* (b+c). given clause #10: (wt=17) 28 [para_into,15.1.1.2.1,3.1.1] (a*b+a)* (b*a+c)!=a* (b+c). given clause #11: (wt=19) 29 [para_into,15.1.1.2,2.1.1,demod,13] (a*b+a)* (c+a)* (c+b)!=a* (b+c). given clause #12: (wt=17) 30 [para_into,15.1.1,3.1.1] (a*b+c)* (a*b+a)!=a* (b+c). given clause #13: (wt=21) 31 [para_into,16.1.1.1,12.1.1,demod,7] (x*y+x)* (x*y+y)* (x*y+z)=x*y. given clause #14: (wt=17) 33 [para_into,16.1.1.1,4.1.1,demod,5] (x+y+x+y)* (x+y+z)=x+y. Starting on level 3, last kept clause of level 2 is 209. Starting on level 3, last kept clause of level 2 is 209. given clause #15: (wt=23) 45 [para_into,18.1.1.1,12.1.1,demod,7,13] (x+y)* (x+z)* (x+y*z+u)= (x+y)* (x+z). given clause #16: (wt=19) 47 [para_into,18.1.1.1,4.1.1,demod,5,5] (x+y+z)* (x+y+z+u)=x+y+z. given clause #17: (wt=13) 49 [para_into,18.1.1.1,2.1.1] (x+y)* (y+x+z)=y+x. given clause #18: (wt=13) 53 [para_into,18.1.1.2.2,2.1.1] (x+y)* (x+z+y)=x+y. given clause #19: (wt=13) 55 [para_into,18.1.1.2,2.1.1,demod,5] (x+y)* (y+z+x)=x+y. given clause #20: (wt=5) 57 [para_into,18.1.1,16.1.1,flip.1] x+x=x. given clause #21: (wt=13) 59 [para_into,18.1.1,3.1.1] (x+y+z)* (x+y)=x+y. given clause #22: (wt=11) 61 [back_demod,43,demod,58] x* (x+y)*z=x*z. -------- PROOF -------- ----> UNIT CONFLICT at 0.03 sec ----> 399 [binary,397.1,376.1] $F. Length of proof is 13. Level of proof is 4. ---------------- PROOF ---------------- 2 [] x+y=y+x. 6 [] (x*y)*z=x*y*z. 8 [] x+x*y=x. 11,10 [] x* (x+y)=x. 13,12 [] x+y*z= (x+y)* (x+z). 14 [] a* (b+c)!=a*b+a*c. 15 [copy,14,demod,13,flip.1] (a*b+a)* (a*b+c)!=a* (b+c). 16 [back_demod,8,demod,13] (x+x)* (x+y)=x. 18 [para_into,12.1.1.2,10.1.1,flip.1] (x+y)* (x+y+z)=x+y. 20 [para_into,12.1.1,2.1.1] x*y+z= (z+x)* (z+y). 21 [copy,20,flip.1] (x+y)* (x+z)=y*z+x. 29 [para_into,15.1.1.2,2.1.1,demod,13] (a*b+a)* (c+a)* (c+b)!=a* (b+c). 43 [para_from,16.1.1,6.1.1.1,flip.1] (x+x)* (x+y)*z=x*z. 58,57 [para_into,18.1.1,16.1.1,flip.1] x+x=x. 61 [back_demod,43,demod,58] x* (x+y)*z=x*z. 129 [para_into,29.1.1.2.2,2.1.1] (a*b+a)* (c+a)* (b+c)!=a* (b+c). 357,356 [para_from,57.1.1,21.1.1.1,demod,11,flip.1] x*y+x=x. 376 [back_demod,129,demod,357] a* (c+a)* (b+c)!=a* (b+c). 397 [para_into,61.1.1.2.1,2.1.1] x* (y+x)*z=x*z. 399 [binary,397.1,376.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 22 clauses generated 476 clauses kept 231 clauses forward subsumed 363 clauses back subsumed 0 Kbytes malloced 542 ----------- times (seconds) ----------- user CPU time 0.03 (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) para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.01 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 5887 finished Wed Aug 6 14:25:56 2003