----- 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 thm7.in". The process ID is 16998. % Reading file thm7.in. op(400,xfx,[*,+,^,v,/,\,#]). lrpo_multiset_status([m(_,_,_)]). 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). assign(pick_given_ratio,3). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] m(x,y,z)!=m(x,u,v)|m(w,y,z)=m(w,u,v). 0 [] m(x,y,y)=x. 0 [] m(x,y,z)=m(z,y,x). end_of_list. list(passive). 1 [] m(A,B,m(C,D,E))!=m(m(A,B,C),D,E). 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=18): 3 [] m(x,y,z)!=m(x,u,v)|m(w,y,z)=m(w,u,v). ** KEPT (pick-wt=6): 4 [] m(x,y,y)=x. ---> New Demodulator: 5 [new_demod,4] m(x,y,y)=x. ** KEPT (pick-wt=9): 6 [] m(x,y,z)=m(z,y,x). >>>> Starting back demodulation with 5. Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] m(x,y,z)=m(z,y,x). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=18) 3 [] m(x,y,z)!=m(x,u,v)|m(w,y,z)=m(w,u,v). given clause #2: (wt=6) 4 [] m(x,y,y)=x. given clause #3: (wt=9) 6 [] m(x,y,z)=m(z,y,x). ** KEPT (pick-wt=6): 7 [para_into,6.1.1,4.1.1,flip.1] m(x,x,y)=y. ---> New Demodulator: 8 [new_demod,7] m(x,x,y)=y. >>>> Starting back demodulation with 8. given clause #4: (wt=6) 7 [para_into,6.1.1,4.1.1,flip.1] m(x,x,y)=y. ** KEPT (pick-wt=12): 9 [hyper,7,3] m(x,y,m(y,z,u))=m(x,z,u). ---> New Demodulator: 10 [new_demod,9] m(x,y,m(y,z,u))=m(x,z,u). >>>> Starting back demodulation with 10. given clause #5: (wt=12) 9 [hyper,7,3] m(x,y,m(y,z,u))=m(x,z,u). ** KEPT (pick-wt=12): 11 [para_into,9.1.1.3,6.1.1] m(x,y,m(z,u,y))=m(x,u,z). ---> New Demodulator: 12 [new_demod,11] m(x,y,m(z,u,y))=m(x,u,z). ** KEPT (pick-wt=12): 13 [para_into,9.1.1,6.1.1] m(m(x,y,z),x,u)=m(u,y,z). ---> New Demodulator: 14 [new_demod,13] m(m(x,y,z),x,u)=m(u,y,z). >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 14. given clause #6: (wt=12) 11 [para_into,9.1.1.3,6.1.1] m(x,y,m(z,u,y))=m(x,u,z). ** KEPT (pick-wt=15): 15 [para_into,11.1.1.3,11.1.1] m(x,m(y,z,u),m(v,z,y))=m(x,u,v). ---> New Demodulator: 16 [new_demod,15] m(x,m(y,z,u),m(v,z,y))=m(x,u,v). ** KEPT (pick-wt=15): 17 [para_into,11.1.1.3,9.1.1] m(x,m(y,z,u),m(v,z,u))=m(x,y,v). ---> New Demodulator: 18 [new_demod,17] m(x,m(y,z,u),m(v,z,u))=m(x,y,v). ** KEPT (pick-wt=12): 19 [para_into,11.1.1,6.1.1] m(m(x,y,z),z,u)=m(u,y,x). ---> New Demodulator: 20 [new_demod,19] m(m(x,y,z),z,u)=m(u,y,x). >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 20. given clause #7: (wt=12) 13 [para_into,9.1.1,6.1.1] m(m(x,y,z),x,u)=m(u,y,z). ** KEPT (pick-wt=15): 21 [para_into,13.1.1.1,13.1.1] m(m(x,y,z),m(u,y,z),v)=m(v,u,x). ---> New Demodulator: 22 [new_demod,21] m(m(x,y,z),m(u,y,z),v)=m(v,u,x). ** KEPT (pick-wt=15): 23 [para_into,13.1.1,11.1.1] m(m(x,y,z),u,v)=m(m(v,u,x),y,z). ** KEPT (pick-wt=15): 24 [para_into,13.1.1,9.1.1] m(m(x,y,z),u,v)=m(m(x,u,v),y,z). >>>> Starting back demodulation with 22. ** KEPT (pick-wt=15): 25 [copy,23,flip.1] m(m(x,y,z),u,v)=m(m(z,u,v),y,x). given clause #8: (wt=12) 19 [para_into,11.1.1,6.1.1] m(m(x,y,z),z,u)=m(u,y,x). ** KEPT (pick-wt=15): 26 [para_into,19.1.1.1,11.1.1] m(m(x,y,z),m(z,y,u),v)=m(v,u,x). ---> New Demodulator: 27 [new_demod,26] m(m(x,y,z),m(z,y,u),v)=m(v,u,x). ** KEPT (pick-wt=15): 28 [para_into,19.1.1,11.1.1] m(m(x,y,z),u,v)=m(m(v,u,z),y,x). >>>> Starting back demodulation with 27. given clause #9: (wt=15) 15 [para_into,11.1.1.3,11.1.1] m(x,m(y,z,u),m(v,z,y))=m(x,u,v). ** KEPT (pick-wt=21): 29 [para_into,15.1.1.2,15.1.1] m(x,m(y,z,u),m(v,m(w,v6,z),y))=m(x,m(u,v6,w),v). ** KEPT (pick-wt=18): 30 [para_into,15.1.1.2,11.1.1] m(x,m(y,z,u),m(v,w,y))=m(x,m(u,z,w),v). ** KEPT (pick-wt=18): 31 [para_into,15.1.1.2,9.1.1] m(x,m(y,z,u),m(v,w,y))=m(x,m(w,z,u),v). ** KEPT (pick-wt=18): 32 [para_into,15.1.1.3,19.1.1] m(x,m(y,z,u),m(y,v,w))=m(x,u,m(w,v,z)). ** KEPT (pick-wt=18): 33 [para_into,15.1.1.3,13.1.1] m(x,m(y,z,u),m(y,v,w))=m(x,u,m(z,v,w)). ** KEPT (pick-wt=12): 34 [para_into,15.1.1.3,7.1.1] m(x,m(y,z,u),y)=m(x,u,z). ---> New Demodulator: 35 [new_demod,34] m(x,m(y,z,u),y)=m(x,u,z). ** KEPT (pick-wt=15): 36 [para_into,15.1.1.3,6.1.1] m(x,m(y,z,u),m(y,z,v))=m(x,u,v). ---> New Demodulator: 37 [new_demod,36] m(x,m(y,z,u),m(y,z,v))=m(x,u,v). ** KEPT (pick-wt=18): 38 [para_into,15.1.1,19.1.1] m(m(x,y,z),u,v)=m(m(v,u,m(z,y,w)),w,x). ** KEPT (pick-wt=18): 39 [para_into,15.1.1,13.1.1] m(m(x,y,z),u,v)=m(m(m(z,y,w),u,v),w,x). ** KEPT (pick-wt=21): 40 [copy,29,flip.1] m(x,m(y,z,u),v)=m(x,m(w,v6,y),m(v,m(u,z,v6),w)). ** KEPT (pick-wt=18): 41 [copy,30,flip.1] m(x,m(y,z,u),v)=m(x,m(w,z,y),m(v,u,w)). ** KEPT (pick-wt=18): 42 [copy,31,flip.1] m(x,m(y,z,u),v)=m(x,m(w,z,u),m(v,y,w)). ** KEPT (pick-wt=18): 43 [copy,32,flip.1] m(x,y,m(z,u,v))=m(x,m(w,v,y),m(w,u,z)). ** KEPT (pick-wt=18): 44 [copy,33,flip.1] m(x,y,m(z,u,v))=m(x,m(w,z,y),m(w,u,v)). >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 37. ** KEPT (pick-wt=18): 45 [copy,38,flip.1] m(m(x,y,m(z,u,v)),v,w)=m(m(w,u,z),y,x). ** KEPT (pick-wt=18): 46 [copy,39,flip.1] m(m(m(x,y,z),u,v),z,w)=m(m(w,y,x),u,v). ** KEPT (pick-wt=18): 47 [para_from,15.1.1,19.1.1.1] m(m(x,y,z),m(z,u,v),w)=m(w,m(v,u,y),x). ** KEPT (pick-wt=18): 48 [copy,47,flip.1] m(x,m(y,z,u),v)=m(m(v,u,w),m(w,z,y),x). given clause #10: (wt=12) 34 [para_into,15.1.1.3,7.1.1] m(x,m(y,z,u),y)=m(x,u,z). ** KEPT (pick-wt=15): 49 [para_into,34.1.1.2,19.1.1] m(x,m(y,z,u),m(u,z,v))=m(x,y,v). ---> New Demodulator: 50 [new_demod,49] m(x,m(y,z,u),m(u,z,v))=m(x,y,v). ** KEPT (pick-wt=12): 51 [para_into,34.1.1.2,11.1.1,demod,35,flip.1] m(x,m(y,z,u),u)=m(x,y,z). ---> New Demodulator: 52 [new_demod,51] m(x,m(y,z,u),u)=m(x,y,z). ** KEPT (pick-wt=15): 53 [para_into,34.1.1,19.1.1,flip.1] m(m(x,y,m(z,u,v)),v,u)=m(z,y,x). ---> New Demodulator: 54 [new_demod,53] m(m(x,y,m(z,u,v)),v,u)=m(z,y,x). ** KEPT (pick-wt=15): 55 [para_into,34.1.1,13.1.1,flip.1] m(m(m(x,y,z),u,v),z,y)=m(x,u,v). ---> New Demodulator: 56 [new_demod,55] m(m(m(x,y,z),u,v),z,y)=m(x,u,v). ** KEPT (pick-wt=12): 57 [para_into,34.1.1,6.1.1] m(x,m(x,y,z),u)=m(u,z,y). ---> New Demodulator: 58 [new_demod,57] m(x,m(x,y,z),u)=m(u,z,y). >>>> Starting back demodulation with 50. >>>> Starting back demodulation with 52. >>>> Starting back demodulation with 54. >>>> Starting back demodulation with 56. >>>> Starting back demodulation with 58. ** KEPT (pick-wt=15): 59 [para_from,34.1.1,11.1.1.3] m(x,y,m(z,u,v))=m(x,m(y,v,u),z). ** KEPT (pick-wt=18): 60 [para_from,34.1.1,15.1.1.2] m(x,m(y,z,u),m(v,m(w,u,z),y))=m(x,w,v). ---> New Demodulator: 61 [new_demod,60] m(x,m(y,z,u),m(v,m(w,u,z),y))=m(x,w,v). ** KEPT (pick-wt=15): 62 [para_from,34.1.1,19.1.1.1] m(m(x,y,z),u,v)=m(v,m(u,z,y),x). ** KEPT (pick-wt=15): 63 [copy,59,flip.1] m(x,m(y,z,u),v)=m(x,y,m(v,u,z)). >>>> Starting back demodulation with 61. ** KEPT (pick-wt=15): 64 [copy,62,flip.1] m(x,m(y,z,u),v)=m(m(v,u,z),y,x). given clause #11: (wt=12) 51 [para_into,34.1.1.2,11.1.1,demod,35,flip.1] m(x,m(y,z,u),u)=m(x,y,z). ** KEPT (pick-wt=15): 65 [para_into,51.1.1.2,51.1.1] m(x,m(y,z,u),v)=m(x,y,m(z,u,v)). ** KEPT (pick-wt=18): 66 [para_into,51.1.1.2,15.1.1] m(x,m(y,z,u),m(u,v,w))=m(x,y,m(w,v,z)). ** KEPT (pick-wt=15): 67 [para_into,51.1.1,19.1.1,flip.1] m(m(x,y,m(z,u,v)),z,u)=m(v,y,x). ---> New Demodulator: 68 [new_demod,67] m(m(x,y,m(z,u,v)),z,u)=m(v,y,x). ** KEPT (pick-wt=15): 69 [para_into,51.1.1,13.1.1,flip.1] m(m(m(x,y,z),u,v),x,y)=m(z,u,v). ---> New Demodulator: 70 [new_demod,69] m(m(m(x,y,z),u,v),x,y)=m(z,u,v). ** KEPT (pick-wt=12): 71 [para_into,51.1.1,6.1.1] m(x,m(y,z,x),u)=m(u,y,z). ---> New Demodulator: 72 [new_demod,71] m(x,m(y,z,x),u)=m(u,y,z). ** KEPT (pick-wt=15): 73 [copy,65,flip.1] m(x,y,m(z,u,v))=m(x,m(y,z,u),v). ** KEPT (pick-wt=18): 74 [copy,66,flip.1] m(x,y,m(z,u,v))=m(x,m(y,v,w),m(w,u,z)). >>>> Starting back demodulation with 68. >>>> Starting back demodulation with 70. >>>> Starting back demodulation with 72. ** KEPT (pick-wt=15): 75 [para_from,51.1.1,11.1.1.3] m(x,y,m(z,u,v))=m(x,m(u,v,y),z). ** KEPT (pick-wt=18): 76 [para_from,51.1.1,15.1.1.2] m(x,m(y,z,u),m(v,m(z,u,w),y))=m(x,w,v). ---> New Demodulator: 77 [new_demod,76] m(x,m(y,z,u),m(v,m(z,u,w),y))=m(x,w,v). ** KEPT (pick-wt=15): 78 [para_from,51.1.1,19.1.1.1] m(m(x,y,z),u,v)=m(v,m(y,z,u),x). ** KEPT (pick-wt=15): 79 [copy,75,flip.1] m(x,m(y,z,u),v)=m(x,u,m(v,y,z)). >>>> Starting back demodulation with 77. ** KEPT (pick-wt=15): 80 [copy,78,flip.1] m(x,m(y,z,u),v)=m(m(v,y,z),u,x). given clause #12: (wt=12) 57 [para_into,34.1.1,6.1.1] m(x,m(x,y,z),u)=m(u,z,y). ** KEPT (pick-wt=15): 81 [para_into,57.1.1.2,57.1.1] m(x,m(y,z,u),v)=m(v,y,m(x,u,z)). ** KEPT (pick-wt=15): 82 [para_into,57.1.1.2,19.1.1] m(m(x,y,z),m(u,y,x),v)=m(v,u,z). ---> New Demodulator: 83 [new_demod,82] m(m(x,y,z),m(u,y,x),v)=m(v,u,z). ** KEPT (pick-wt=12): 84 [para_into,57.1.1,15.1.1,flip.1] m(m(x,y,z),u,y)=m(z,u,x). ---> New Demodulator: 85 [new_demod,84] m(m(x,y,z),u,y)=m(z,u,x). ** KEPT (pick-wt=15): 86 [copy,81,flip.1] m(x,y,m(z,u,v))=m(z,m(y,v,u),x). >>>> Starting back demodulation with 83. >>>> Starting back demodulation with 85. ** KEPT (pick-wt=18): 87 [para_from,57.1.1,15.1.1.3] m(x,m(y,m(z,u,v),w),m(y,v,u))=m(x,w,z). ---> New Demodulator: 88 [new_demod,87] m(x,m(y,m(z,u,v),w),m(y,v,u))=m(x,w,z). >>>> Starting back demodulation with 88. given clause #13: (wt=15) 17 [para_into,11.1.1.3,9.1.1] m(x,m(y,z,u),m(v,z,u))=m(x,y,v). ** KEPT (pick-wt=18): 89 [para_into,17.1.1.3,57.1.1] m(x,m(y,m(z,u,v),w),m(w,v,u))=m(x,y,z). ---> New Demodulator: 90 [new_demod,89] m(x,m(y,m(z,u,v),w),m(w,v,u))=m(x,y,z). ** KEPT (pick-wt=18): 91 [para_into,17.1.1.3,13.1.1] m(x,m(y,z,u),m(u,v,w))=m(x,y,m(z,v,w)). ** KEPT (pick-wt=18): 92 [para_into,17.1.1,19.1.1] m(m(x,y,z),u,v)=m(m(v,u,m(w,y,z)),w,x). ** KEPT (pick-wt=18): 93 [para_into,17.1.1,13.1.1] m(m(x,y,z),u,v)=m(m(m(w,y,z),u,v),w,x). >>>> Starting back demodulation with 90. ** KEPT (pick-wt=18): 94 [copy,91,flip.1] m(x,y,m(z,u,v))=m(x,m(y,z,w),m(w,u,v)). ** KEPT (pick-wt=18): 95 [copy,92,flip.1] m(m(x,y,m(z,u,v)),z,w)=m(m(w,u,v),y,x). ** KEPT (pick-wt=18): 96 [copy,93,flip.1] m(m(m(x,y,z),u,v),x,w)=m(m(w,y,z),u,v). ** KEPT (pick-wt=21): 97 [para_from,17.1.1,15.1.1.2] m(x,m(y,z,u),m(v,m(z,w,v6),y))=m(x,m(u,w,v6),v). ** KEPT (pick-wt=18): 98 [para_from,17.1.1,19.1.1.1] m(m(x,y,z),m(z,u,v),w)=m(w,m(y,u,v),x). ** KEPT (pick-wt=21): 99 [copy,97,flip.1] m(x,m(y,z,u),v)=m(x,m(w,v6,y),m(v,m(v6,z,u),w)). ** KEPT (pick-wt=18): 100 [copy,98,flip.1] m(x,m(y,z,u),v)=m(m(v,y,w),m(w,z,u),x). given clause #14: (wt=12) 71 [para_into,51.1.1,6.1.1] m(x,m(y,z,x),u)=m(u,y,z). ** KEPT (pick-wt=15): 101 [para_into,71.1.1.2,51.1.1] m(x,m(y,z,u),v)=m(v,y,m(z,u,x)). ** KEPT (pick-wt=18): 102 [para_into,71.1.1.2,17.1.1] m(m(x,y,z),m(u,v,x),w)=m(w,u,m(v,y,z)). ** KEPT (pick-wt=18): 103 [para_into,71.1.1.2,15.1.1] m(m(x,y,z),m(u,v,x),w)=m(w,u,m(z,y,v)). ** KEPT (pick-wt=15): 104 [copy,101,flip.1] m(x,y,m(z,u,v))=m(v,m(y,z,u),x). ** KEPT (pick-wt=18): 105 [copy,102,flip.1] m(x,y,m(z,u,v))=m(m(w,u,v),m(y,z,w),x). ** KEPT (pick-wt=18): 106 [copy,103,flip.1] m(x,y,m(z,u,v))=m(m(w,u,z),m(y,v,w),x). ** KEPT (pick-wt=18): 107 [para_from,71.1.1,17.1.1.3] m(x,m(y,m(z,u,v),w),m(w,z,u))=m(x,y,v). ---> New Demodulator: 108 [new_demod,107] m(x,m(y,m(z,u,v),w),m(w,z,u))=m(x,y,v). ** KEPT (pick-wt=18): 109 [para_from,71.1.1,15.1.1.3] m(x,m(y,m(z,u,v),w),m(y,z,u))=m(x,w,v). ---> New Demodulator: 110 [new_demod,109] m(x,m(y,m(z,u,v),w),m(y,z,u))=m(x,w,v). >>>> Starting back demodulation with 108. >>>> Starting back demodulation with 110. given clause #15: (wt=12) 84 [para_into,57.1.1,15.1.1,flip.1] m(m(x,y,z),u,y)=m(z,u,x). ** KEPT (pick-wt=12): 111 [para_into,84.1.1.1,84.1.1,demod,85,flip.1] m(x,y,m(z,x,u))=m(z,y,u). ---> New Demodulator: 112 [new_demod,111] m(x,y,m(z,x,u))=m(z,y,u). ** KEPT (pick-wt=15): 113 [para_into,84.1.1.1,71.1.1] m(m(x,y,z),u,m(y,z,v))=m(x,u,v). ---> New Demodulator: 114 [new_demod,113] m(m(x,y,z),u,m(y,z,v))=m(x,u,v). ** KEPT (pick-wt=15): 115 [para_into,84.1.1.1,57.1.1] m(m(x,y,z),u,m(v,z,y))=m(x,u,v). ---> New Demodulator: 116 [new_demod,115] m(m(x,y,z),u,m(v,z,y))=m(x,u,v). ** KEPT (pick-wt=15): 117 [para_into,84.1.1.1,19.1.1] m(m(x,y,z),u,v)=m(x,u,m(z,y,v)). ** KEPT (pick-wt=18): 118 [para_into,84.1.1.1,17.1.1] m(m(x,y,z),u,m(y,v,w))=m(m(z,v,w),u,x). ** KEPT (pick-wt=18): 119 [para_into,84.1.1.1,15.1.1] m(m(x,y,z),u,m(v,w,y))=m(m(z,w,v),u,x). ** KEPT (pick-wt=15): 120 [para_into,84.1.1.1,13.1.1] m(m(x,y,z),u,v)=m(x,u,m(v,y,z)). ** KEPT (pick-wt=15): 121 [para_into,84.1.1.1,11.1.1] m(m(x,y,z),u,v)=m(m(z,y,v),u,x). ** KEPT (pick-wt=15): 122 [para_into,84.1.1.1,9.1.1] m(m(x,y,z),u,v)=m(m(v,y,z),u,x). ** KEPT (pick-wt=15): 123 [para_into,84.1.1,71.1.1,flip.1] m(x,m(y,z,m(u,v,x)),u)=m(v,y,z). ---> New Demodulator: 124 [new_demod,123] m(x,m(y,z,m(u,v,x)),u)=m(v,y,z). ** KEPT (pick-wt=15): 125 [para_into,84.1.1,57.1.1,flip.1] m(x,m(m(y,z,x),u,v),y)=m(z,v,u). ---> New Demodulator: 126 [new_demod,125] m(x,m(m(y,z,x),u,v),y)=m(z,v,u). ** KEPT (pick-wt=15): 127 [para_into,84.1.1,51.1.1] m(m(x,y,z),u,v)=m(z,m(u,v,y),x). ** KEPT (pick-wt=15): 128 [para_into,84.1.1,34.1.1] m(m(x,y,z),u,v)=m(z,m(y,v,u),x). ** KEPT (pick-wt=18): 129 [para_into,84.1.1,17.1.1] m(m(x,m(y,z,u),v),w,y)=m(v,m(w,z,u),x). ** KEPT (pick-wt=18): 130 [para_into,84.1.1,15.1.1] m(m(x,m(y,z,u),v),w,y)=m(v,m(u,z,w),x). ** KEPT (pick-wt=15): 131 [para_into,84.1.1,11.1.1] m(m(x,m(y,z,u),v),z,y)=m(v,u,x). ---> New Demodulator: 132 [new_demod,131] m(m(x,m(y,z,u),v),z,y)=m(v,u,x). ** KEPT (pick-wt=15): 133 [para_into,84.1.1,9.1.1] m(m(x,m(y,z,u),v),z,u)=m(v,y,x). ---> New Demodulator: 134 [new_demod,133] m(m(x,m(y,z,u),v),z,u)=m(v,y,x). >>>> Starting back demodulation with 112. >>>> Starting back demodulation with 114. >>>> Starting back demodulation with 116. ** KEPT (pick-wt=15): 135 [copy,117,flip.1] m(x,y,m(z,u,v))=m(m(x,u,z),y,v). ** KEPT (pick-wt=18): 136 [copy,118,flip.1] m(m(x,y,z),u,v)=m(m(v,w,x),u,m(w,y,z)). ** KEPT (pick-wt=18): 137 [copy,119,flip.1] m(m(x,y,z),u,v)=m(m(v,w,x),u,m(z,y,w)). ** KEPT (pick-wt=15): 138 [copy,120,flip.1] m(x,y,m(z,u,v))=m(m(x,u,v),y,z). ** KEPT (pick-wt=15): 139 [copy,121,flip.1] m(m(x,y,z),u,v)=m(m(v,y,x),u,z). >>>> Starting back demodulation with 124. >>>> Starting back demodulation with 126. ** KEPT (pick-wt=15): 140 [copy,127,flip.1] m(x,m(y,z,u),v)=m(m(v,u,x),y,z). ** KEPT (pick-wt=15): 141 [copy,128,flip.1] m(x,m(y,z,u),v)=m(m(v,y,x),u,z). ** KEPT (pick-wt=18): 142 [copy,129,flip.1] m(x,m(y,z,u),v)=m(m(v,m(w,z,u),x),y,w). ** KEPT (pick-wt=18): 143 [copy,130,flip.1] m(x,m(y,z,u),v)=m(m(v,m(w,z,y),x),u,w). >>>> Starting back demodulation with 132. >>>> Starting back demodulation with 134. ** KEPT (pick-wt=15): 144 [para_from,84.1.1,71.1.1.2] m(x,m(y,z,u),v)=m(v,m(u,x,y),z). ** KEPT (pick-wt=18): 145 [para_from,84.1.1,17.1.1.3] m(x,m(y,z,u),m(v,z,w))=m(x,y,m(w,u,v)). ** KEPT (pick-wt=18): 146 [para_from,84.1.1,15.1.1.3] m(x,m(y,z,u),m(v,z,w))=m(x,u,m(w,y,v)). ** KEPT (pick-wt=15): 147 [para_from,84.1.1,11.1.1.3] m(x,y,m(z,u,v))=m(x,u,m(v,y,z)). ** KEPT (pick-wt=15): 148 [para_from,84.1.1,51.1.1.2] m(x,m(y,z,u),v)=m(x,m(u,v,y),z). ** KEPT (pick-wt=15): 149 [para_from,84.1.1,34.1.1.2] m(x,m(y,z,u),m(u,v,y))=m(x,v,z). ---> New Demodulator: 150 [new_demod,149] m(x,m(y,z,u),m(u,v,y))=m(x,v,z). ** KEPT (pick-wt=18): 151 [para_from,84.1.1,17.1.1.2] m(x,m(y,z,u),m(v,z,w))=m(x,m(u,w,y),v). ** KEPT (pick-wt=18): 152 [para_from,84.1.1,15.1.1.2] m(x,m(y,z,u),m(v,z,m(u,w,y)))=m(x,w,v). ---> New Demodulator: 153 [new_demod,152] m(x,m(y,z,u),m(v,z,m(u,w,y)))=m(x,w,v). ** KEPT (pick-wt=15): 154 [para_from,84.1.1,57.1.1.2] m(m(x,y,z),m(z,u,x),v)=m(v,y,u). ---> New Demodulator: 155 [new_demod,154] m(m(x,y,z),m(z,u,x),v)=m(v,y,u). ** KEPT (pick-wt=15): 156 [para_from,84.1.1,19.1.1.1] m(m(x,y,z),u,v)=m(v,y,m(z,u,x)). ** KEPT (pick-wt=15): 157 [copy,144,flip.1] m(x,m(y,z,u),v)=m(z,m(u,v,y),x). ** KEPT (pick-wt=18): 158 [copy,145,flip.1] m(x,y,m(z,u,v))=m(x,m(y,w,u),m(v,w,z)). ** KEPT (pick-wt=18): 159 [copy,146,flip.1] m(x,y,m(z,u,v))=m(x,m(u,w,y),m(v,w,z)). >>>> Starting back demodulation with 150. ** KEPT (pick-wt=18): 160 [copy,151,flip.1] m(x,m(y,z,u),v)=m(x,m(u,w,y),m(v,w,z)). >>>> Starting back demodulation with 153. >>>> Starting back demodulation with 155. ** KEPT (pick-wt=15): 161 [copy,156,flip.1] m(x,y,m(z,u,v))=m(m(v,y,z),u,x). given clause #16: (wt=12) 111 [para_into,84.1.1.1,84.1.1,demod,85,flip.1] m(x,y,m(z,x,u))=m(z,y,u). ** KEPT (pick-wt=15): 162 [para_into,111.1.1.3,71.1.1] m(m(x,y,z),u,m(v,x,y))=m(z,u,v). ---> New Demodulator: 163 [new_demod,162] m(m(x,y,z),u,m(v,x,y))=m(z,u,v). ** KEPT (pick-wt=15): 164 [para_into,111.1.1.3,19.1.1] m(x,y,m(z,u,v))=m(m(v,u,x),y,z). ** KEPT (pick-wt=18): 165 [para_into,111.1.1.3,17.1.1] m(m(x,y,z),u,m(v,x,w))=m(v,u,m(w,y,z)). ** KEPT (pick-wt=18): 166 [para_into,111.1.1.3,15.1.1] m(m(x,y,z),u,m(v,z,w))=m(v,u,m(w,y,x)). ** KEPT (pick-wt=15): 167 [para_into,111.1.1.3,11.1.1] m(x,y,m(z,u,v))=m(z,y,m(v,u,x)). ** KEPT (pick-wt=15): 168 [para_into,111.1.1.3,9.1.1] m(x,y,m(z,u,v))=m(z,y,m(x,u,v)). ** KEPT (pick-wt=15): 169 [para_into,111.1.1,71.1.1] m(m(x,y,z),u,v)=m(x,m(u,v,y),z). ** KEPT (pick-wt=15): 170 [para_into,111.1.1,57.1.1] m(m(x,y,z),u,v)=m(x,m(y,v,u),z). ** KEPT (pick-wt=15): 171 [para_into,111.1.1,51.1.1,flip.1] m(x,m(y,z,m(x,u,v)),v)=m(u,y,z). ---> New Demodulator: 172 [new_demod,171] m(x,m(y,z,m(x,u,v)),v)=m(u,y,z). ** KEPT (pick-wt=15): 173 [para_into,111.1.1,34.1.1,flip.1] m(x,m(m(x,y,z),u,v),z)=m(y,v,u). ---> New Demodulator: 174 [new_demod,173] m(x,m(m(x,y,z),u,v),z)=m(y,v,u). >>>> Starting back demodulation with 163. ** KEPT (pick-wt=15): 175 [copy,164,flip.1] m(m(x,y,z),u,v)=m(z,u,m(v,y,x)). ** KEPT (pick-wt=18): 176 [copy,165,flip.1] m(x,y,m(z,u,v))=m(m(w,u,v),y,m(x,w,z)). ** KEPT (pick-wt=18): 177 [copy,166,flip.1] m(x,y,m(z,u,v))=m(m(v,u,w),y,m(x,w,z)). ** KEPT (pick-wt=15): 178 [copy,167,flip.1] m(x,y,m(z,u,v))=m(v,y,m(x,u,z)). ** KEPT (pick-wt=15): 179 [copy,169,flip.1] m(x,m(y,z,u),v)=m(m(x,u,v),y,z). ** KEPT (pick-wt=15): 180 [copy,170,flip.1] m(x,m(y,z,u),v)=m(m(x,y,v),u,z). >>>> Starting back demodulation with 172. >>>> Starting back demodulation with 174. ** KEPT (pick-wt=15): 181 [para_from,111.1.1,71.1.1.2] m(m(x,y,z),m(x,u,z),v)=m(v,y,u). ---> New Demodulator: 182 [new_demod,181] m(m(x,y,z),m(x,u,z),v)=m(v,y,u). ** KEPT (pick-wt=18): 183 [para_from,111.1.1,17.1.1.3] m(x,m(y,z,m(u,v,w)),m(u,z,w))=m(x,y,v). ---> New Demodulator: 184 [new_demod,183] m(x,m(y,z,m(u,v,w)),m(u,z,w))=m(x,y,v). ** KEPT (pick-wt=18): 185 [para_from,111.1.1,15.1.1.3] m(x,m(m(y,z,u),v,w),m(y,v,u))=m(x,w,z). ---> New Demodulator: 186 [new_demod,185] m(x,m(m(y,z,u),v,w),m(y,v,u))=m(x,w,z). ** KEPT (pick-wt=15): 187 [para_from,111.1.1,11.1.1.3] m(x,m(y,z,u),m(y,v,u))=m(x,v,z). ---> New Demodulator: 188 [new_demod,187] m(x,m(y,z,u),m(y,v,u))=m(x,v,z). ** KEPT (pick-wt=15): 189 [para_from,111.1.1,34.1.1.2] m(x,m(y,z,u),v)=m(x,m(y,v,u),z). ** KEPT (pick-wt=18): 190 [para_from,111.1.1,17.1.1.2] m(x,m(y,z,u),m(v,z,m(y,w,u)))=m(x,w,v). ---> New Demodulator: 191 [new_demod,190] m(x,m(y,z,u),m(v,z,m(y,w,u)))=m(x,w,v). ** KEPT (pick-wt=18): 192 [para_from,111.1.1,15.1.1.2] m(x,m(y,z,u),m(v,z,w))=m(x,m(y,w,u),v). ** KEPT (pick-wt=15): 193 [para_from,111.1.1,9.1.1.3] m(x,y,m(z,u,v))=m(x,u,m(z,y,v)). ** KEPT (pick-wt=15): 194 [para_from,111.1.1,57.1.1.2] m(x,m(y,z,u),v)=m(v,m(y,x,u),z). ** KEPT (pick-wt=15): 195 [para_from,111.1.1,13.1.1.1] m(m(x,y,z),u,v)=m(v,y,m(x,u,z)). >>>> Starting back demodulation with 182. >>>> Starting back demodulation with 184. >>>> Starting back demodulation with 186. >>>> Starting back demodulation with 188. >>>> Starting back demodulation with 191. ** KEPT (pick-wt=18): 196 [copy,192,flip.1] m(x,m(y,z,u),v)=m(x,m(y,w,u),m(v,w,z)). ** KEPT (pick-wt=15): 197 [copy,194,flip.1] m(x,m(y,z,u),v)=m(z,m(y,v,u),x). ** KEPT (pick-wt=15): 198 [copy,195,flip.1] m(x,y,m(z,u,v))=m(m(z,y,v),u,x). given clause #17: (wt=15) 21 [para_into,13.1.1.1,13.1.1] m(m(x,y,z),m(u,y,z),v)=m(v,u,x). ** KEPT (pick-wt=18): 199 [para_into,21.1.1.1,111.1.1] m(m(x,y,z),m(u,y,m(x,v,z)),w)=m(w,u,v). ---> New Demodulator: 200 [new_demod,199] m(m(x,y,z),m(u,y,m(x,v,z)),w)=m(w,u,v). ** KEPT (pick-wt=18): 201 [para_into,21.1.1.1,84.1.1] m(m(x,y,z),m(u,y,v),w)=m(w,u,m(z,v,x)). ** KEPT (pick-wt=18): 202 [para_into,21.1.1.1,71.1.1] m(m(x,y,z),m(u,m(y,z,v),x),w)=m(w,u,v). ---> New Demodulator: 203 [new_demod,202] m(m(x,y,z),m(u,m(y,z,v),x),w)=m(w,u,v). ** KEPT (pick-wt=18): 204 [para_into,21.1.1.1,57.1.1] m(m(x,y,z),m(u,m(v,z,y),x),w)=m(w,u,v). ---> New Demodulator: 205 [new_demod,204] m(m(x,y,z),m(u,m(v,z,y),x),w)=m(w,u,v). ** KEPT (pick-wt=21): 206 [para_into,21.1.1.1,21.1.1] m(m(x,y,z),m(u,m(y,v,w),x),v6)=m(v6,u,m(z,v,w)). ** KEPT (pick-wt=18): 207 [para_into,21.1.1.2,111.1.1] m(m(x,y,m(z,u,v)),m(z,y,v),w)=m(w,u,x). ---> New Demodulator: 208 [new_demod,207] m(m(x,y,m(z,u,v)),m(z,y,v),w)=m(w,u,x). ** KEPT (pick-wt=18): 209 [para_into,21.1.1.2,84.1.1] m(m(x,y,z),m(u,y,v),w)=m(w,m(v,z,u),x). ** KEPT (pick-wt=18): 210 [para_into,21.1.1.2,71.1.1] m(m(x,m(y,z,u),v),m(v,y,z),w)=m(w,u,x). ---> New Demodulator: 211 [new_demod,210] m(m(x,m(y,z,u),v),m(v,y,z),w)=m(w,u,x). ** KEPT (pick-wt=18): 212 [para_into,21.1.1.2,57.1.1] m(m(x,m(y,z,u),v),m(v,u,z),w)=m(w,y,x). ---> New Demodulator: 213 [new_demod,212] m(m(x,m(y,z,u),v),m(v,u,z),w)=m(w,y,x). ** KEPT (pick-wt=21): 214 [para_into,21.1.1.2,21.1.1] m(m(x,m(y,z,u),v),m(v,y,w),v6)=m(v6,m(w,z,u),x). ** KEPT (pick-wt=18): 215 [para_into,21.1.1,111.1.1] m(x,m(y,z,u),v)=m(m(x,m(w,z,u),v),y,w). >>>> Starting back demodulation with 200. ** KEPT (pick-wt=18): 216 [copy,201,flip.1] m(x,y,m(z,u,v))=m(m(v,w,z),m(y,w,u),x). >>>> Starting back demodulation with 203. >>>> Starting back demodulation with 205. ** KEPT (pick-wt=21): 217 [copy,206,flip.1] m(x,y,m(z,u,v))=m(m(w,v6,z),m(y,m(v6,u,v),w),x). >>>> Starting back demodulation with 208. ** KEPT (pick-wt=18): 218 [copy,209,flip.1] m(x,m(y,z,u),v)=m(m(v,w,z),m(u,w,y),x). >>>> Starting back demodulation with 211. >>>> Starting back demodulation with 213. ** KEPT (pick-wt=21): 219 [copy,214,flip.1] m(x,m(y,z,u),v)=m(m(v,m(w,z,u),v6),m(v6,w,y),x). ** KEPT (pick-wt=18): 220 [copy,215,flip.1] m(m(x,m(y,z,u),v),w,y)=m(x,m(w,z,u),v). ** KEPT (pick-wt=18): 221 [para_from,21.1.1,111.1.1.3] m(m(x,y,z),u,m(v,x,w))=m(m(w,y,z),u,v). ** KEPT (pick-wt=21): 222 [para_from,21.1.1,17.1.1.3] m(x,m(y,m(z,u,v),w),m(w,z,v6))=m(x,y,m(v6,u,v)). ** KEPT (pick-wt=21): 223 [para_from,21.1.1,15.1.1.3] m(x,m(y,m(z,u,v),w),m(y,z,v6))=m(x,w,m(v6,u,v)). ** KEPT (pick-wt=18): 224 [para_from,21.1.1,84.1.1.1] m(m(x,y,z),u,m(y,v,w))=m(x,u,m(z,v,w)). ** KEPT (pick-wt=18): 225 [copy,221,flip.1] m(m(x,y,z),u,v)=m(m(w,y,z),u,m(v,w,x)). ** KEPT (pick-wt=21): 226 [copy,222,flip.1] m(x,y,m(z,u,v))=m(x,m(y,m(w,u,v),v6),m(v6,w,z)). ** KEPT (pick-wt=21): 227 [copy,223,flip.1] m(x,y,m(z,u,v))=m(x,m(w,m(v6,u,v),y),m(w,v6,z)). ** KEPT (pick-wt=18): 228 [copy,224,flip.1] m(x,y,m(z,u,v))=m(m(x,w,z),y,m(w,u,v)). given clause #18: (wt=15) 23 [para_into,13.1.1,11.1.1] m(m(x,y,z),u,v)=m(m(v,u,x),y,z). ** KEPT (pick-wt=18): 229 [para_into,23.1.1.1,111.1.1] m(m(x,y,z),u,v)=m(m(v,u,w),y,m(x,w,z)). ** KEPT (pick-wt=18): 230 [para_into,23.1.1.1,84.1.1] m(m(x,y,z),u,v)=m(m(v,u,m(z,w,x)),y,w). ** KEPT (pick-wt=18): 231 [para_into,23.1.1.1,71.1.1] m(m(x,y,z),u,v)=m(m(v,u,w),m(y,z,w),x). ** KEPT (pick-wt=18): 232 [para_into,23.1.1.1,57.1.1] m(m(x,y,z),u,v)=m(m(v,u,w),m(w,z,y),x). ** KEPT (pick-wt=21): 233 [para_into,23.1.1.1,23.1.1] m(m(m(x,y,z),u,v),w,v6)=m(m(v6,w,m(z,u,v)),y,x). ** KEPT (pick-wt=21): 234 [para_into,23.1.1.1,21.1.1] m(m(x,y,z),u,v)=m(m(v,u,m(z,w,v6)),m(y,w,v6),x). ** KEPT (pick-wt=18): 235 [para_into,23.1.1,111.1.1,flip.1] m(m(m(x,m(y,z,u),v),w,y),z,u)=m(x,w,v). ---> New Demodulator: 236 [new_demod,235] m(m(m(x,m(y,z,u),v),w,y),z,u)=m(x,w,v). ** KEPT (pick-wt=18): 237 [para_into,23.1.1,71.1.1,flip.1] m(m(x,m(y,z,m(u,v,w)),u),v,w)=m(x,y,z). ---> New Demodulator: 238 [new_demod,237] m(m(x,m(y,z,m(u,v,w)),u),v,w)=m(x,y,z). ** KEPT (pick-wt=18): 239 [para_into,23.1.1,57.1.1,flip.1] m(m(x,m(m(y,z,u),v,w),y),z,u)=m(x,w,v). ---> New Demodulator: 240 [new_demod,239] m(m(x,m(m(y,z,u),v,w),y),z,u)=m(x,w,v). ** KEPT (pick-wt=15): 241 [para_into,23.1.1,6.1.1] m(x,y,m(z,u,v))=m(m(x,y,z),u,v). ----> UNIT CONFLICT at 0.01 sec ----> 242 [binary,241.1,1.1] $F. Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 1 [] m(A,B,m(C,D,E))!=m(m(A,B,C),D,E). 3 [] m(x,y,z)!=m(x,u,v)|m(w,y,z)=m(w,u,v). 4 [] m(x,y,y)=x. 6 [] m(x,y,z)=m(z,y,x). 7 [para_into,6.1.1,4.1.1,flip.1] m(x,x,y)=y. 9 [hyper,7,3] m(x,y,m(y,z,u))=m(x,z,u). 11 [para_into,9.1.1.3,6.1.1] m(x,y,m(z,u,y))=m(x,u,z). 13 [para_into,9.1.1,6.1.1] m(m(x,y,z),x,u)=m(u,y,z). 23 [para_into,13.1.1,11.1.1] m(m(x,y,z),u,v)=m(m(v,u,x),y,z). 241 [para_into,23.1.1,6.1.1] m(x,y,m(z,u,v))=m(m(x,y,z),u,v). 242 [binary,241.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 18 clauses generated 547 hyper_res generated 16 para_from generated 219 para_into generated 312 demod & eval rewrites 431 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 488 (subsumed by sos) 126 unit deletions 0 factor simplifications 0 clauses kept 185 new demodulators 55 empty clauses 1 clauses back demodulated 0 clauses back subsumed 0 usable size 19 sos size 166 demodulators size 55 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 16998 finished Mon Nov 14 15:26:22 2005