----- Otter 3.3, August 2003 ----- The process was started by mccune on lemma.mcs.anl.gov, Mon Sep 15 12:17:31 2003 The command was "otter". The process ID is 2359. 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). assign(bsub_hint_add_wt,-1000). set(keep_hint_subsumers). assign(max_weight,0). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(sigint_interact). clear(detailed_history). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z)))=x. end_of_list. assign(max_proofs,3). list(passive). 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 2 [] f(f(A,A),f(A,B))!=A|$Ans(B_SS). 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(ONE_SS). end_of_list. list(hints2). 4 [] f(x,f(f(x,y),f(x,y)))=f(x,y). 5 [] f(f(x,y),f(x,x))=x. 6 [] f(f(f(f(x,y),f(y,z)),u),f(y,y))=y. 7 [] f(x,f(f(x,x),y))=f(x,x). 8 [] f(f(f(x,x),y),x)=f(x,x). 9 [] f(f(x,x),f(x,y))=x. 10 [] f(f(x,x),f(x,y))=x. 11 [] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(f(f(x,y),f(y,z)),y). 12 [] f(f(f(x,y),f(x,y)),x)=f(x,y). 13 [] f(f(f(x,y),f(y,z)),y)=f(y,f(f(x,y),f(y,z))). 14 [] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))). 15 [] f(f(f(f(x,y),f(x,z)),u),f(x,x))=x. 16 [] f(f(f(x,f(f(x,y),z)),u),f(f(x,y),f(x,y)))=f(x,y). 17 [] f(f(x,y),f(y,y))=y. 18 [] f(x,f(f(y,x),f(y,x)))=f(y,x). 19 [] f(f(x,x),f(y,x))=x. 20 [] f(x,f(y,f(x,x)))=f(x,x). 21 [] f(f(x,y),f(x,f(f(z,z),z)))=x. 22 [] f(f(f(x,f(f(y,x),z)),u),f(f(y,x),f(y,x)))=f(y,x). 23 [] f(f(x,f(f(y,z),f(z,u))),f(z,z))=z. 24 [] f(f(f(f(x,y),f(z,y)),u),f(y,y))=y. 25 [] f(x,f(f(x,y),f(f(z,z),z)))=f(x,y). 26 [] f(x,x)=f(x,f(f(y,y),y)). 27 [] f(x,f(f(y,y),y))=f(x,x). 28 [] f(x,f(y,f(y,y)))=f(x,x). 29 [] f(x,x)=f(x,f(y,f(y,y))). 30 [] f(x,f(f(x,y),f(z,f(z,z))))=f(x,y). 31 [] f(f(x,f(y,f(y,y))),f(z,x))=x. 32 [] f(f(x,f(f(y,z),f(y,u))),f(y,y))=y. 33 [] f(f(x,f(y,f(f(z,y),u))),f(f(z,y),f(z,y)))=f(z,y). 34 [] f(f(f(f(x,y),f(z,y)),u),f(y,f(f(v,v),v)))=y. 35 [] f(f(f(x,f(x,x)),f(y,f(y,y))),z)=f(x,f(x,x)). 36 [] f(x,f(x,x))=f(y,f(y,y)). 37 [] f(f(f(x,y),z),f(f(x,f(f(y,u),f(y,v))),f(x,f(f(y,u),f(y,v)))))=f(x,f(f(y,u),f(y,v))). 38 [] f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x). 39 [] f(f(x,y),f(y,x))=f(f(y,x),f(y,x)). 40 [] f(f(x,y),f(f(f(y,x),z),f(f(u,u),u)))=f(f(y,x),z). 41 [] f(x,f(f(y,x),f(x,y)))=f(y,x). 42 [] f(x,y)=f(y,x). 43 [] f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(y,x). 44 [] f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(y,x). 45 [] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,u),f(z,v)),y)))=f(f(f(z,u),f(z,v)),y). 46 [] f(f(x,y),z)=f(f(y,x),z). 47 [] f(x,f(y,z))=f(f(z,y),x). 48 [] f(f(x,y),z)=f(z,f(y,x)). 49 [] f(x,f(f(y,z),u))=f(f(f(z,y),u),x). 50 [] f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). 51 [] f(f(f(f(x,y),z),u),f(f(f(y,x),z),f(f(x,y),z)))=f(z,f(x,y)). 52 [] f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). 53 [] f(f(f(f(x,y),f(z,u)),v),f(f(f(y,x),f(u,z)),f(f(z,u),f(x,y))))=f(f(z,u),f(x,y)). 54 [] f(f(f(f(x,f(y,f(f(z,y),u))),z),v),f(f(z,y),f(z,y)))=f(z,y). 55 [] f(f(x,f(f(f(y,f(f(z,y),u)),v),z)),f(f(z,y),f(z,y)))=f(z,y). 56 [] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,v),f(z,u)),y)))=f(f(f(z,v),f(z,u)),y). 57 [] f(f(f(f(f(x,y),f(x,z)),u),f(f(f(x,z),f(x,y)),u)),f(f(u,x),v))=f(f(f(x,z),f(x,y)),u). 58 [] f(f(f(x,f(f(y,x),z)),f(x,u)),y)=f(y,x). 59 [] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(f(f(u,y),f(v,y)),x). 60 [] f(f(f(x,y),f(z,y)),f(f(u,v),f(u,y)))=f(f(f(x,y),f(z,y)),u). 61 [] f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(f(f(x,y),f(z,y)),u). 62 [] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(x,f(f(u,y),f(v,y))). 63 [] f(f(f(x,y),f(x,y)),z)=f(x,f(f(z,y),f(z,y))). 64 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 65 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 66 [] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. 67 [] f(x,f(f(x,y),f(f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))),u)))=f(x,y). 68 [] f(f(x,y),f(f(f(x,y),f(y,z)),y))=f(f(x,y),f(y,z)). 69 [] f(x,f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))))=f(x,y). 70 [] f(f(f(f(x,y),f(y,z)),y),f(y,y))=y. 71 [] f(f(x,x),f(x,x))=x. 72 [] f(x,f(f(x,f(f(x,x),y)),f(x,x)))=f(x,f(f(x,x),y)). 73 [] f(x,f(f(x,y),f(x,f(x,x))))=f(x,y). 74 [] f(f(f(f(x,y),f(y,f(y,f(y,y)))),z),f(y,f(f(x,x),x)))=y. end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 75 [] x=x. Following clause subsumed by 75 during input processing: 0 [copy,75,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=-977): 76 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. ---> New Demodulator: 77 [new_demod,76] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. >>>> Starting back demodulation with 77. >> BACK DEMODULATING HINT 65 WITH 77. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=-977) 76 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. >> BACK DEMODULATING HINT 66 WITH 79. >> BACK DEMODULATING HINT 67 WITH 81. given clause #2: (wt=-973) 80 [para_into,76,76] f(x,f(f(x,y),f(f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))),u)))=f(x,y). >> BACK DEMODULATING HINT 68 WITH 83. >> BACK DEMODULATING HINT 69 WITH 85. given clause #3: (wt=-979) 82 [para_into,80,76] f(f(x,y),f(f(f(x,y),f(y,z)),y))=f(f(x,y),f(y,z)). >> BACK DEMODULATING HINT 70 WITH 87. given clause #4: (wt=-985) 86 [para_into,82,76,demod,77] f(f(f(f(x,y),f(y,z)),y),f(y,y))=y. >> BACK DEMODULATING HINT 71 WITH 89. >> BACK DEMODULATING HINT 72 WITH 91. given clause #5: (wt=-991) 88 [para_into,86,86] f(f(x,x),f(x,x))=x. given clause #6: (wt=-979) 84 [para_into,80,80] f(x,f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))))=f(x,y). >> BACK DEMODULATING HINT 73 WITH 93. given clause #7: (wt=-985) 92 [para_into,84,88] f(x,f(f(x,y),f(x,f(x,x))))=f(x,y). >> BACK DEMODULATING HINT 74 WITH 95. given clause #8: (wt=-979) 90 [para_from,86,82,demod,87,87] f(x,f(f(x,f(f(x,x),y)),f(x,x)))=f(x,f(f(x,x),y)). given clause #9: (wt=-977) 94 [para_from,92,76] f(f(f(f(x,y),f(y,f(y,f(y,y)))),z),f(y,f(f(x,x),x)))=y. given clause #10: (wt=-957) 78 [para_into,76,76] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. >> BACK DEMODULATING HINT 4 WITH 97. given clause #11: (wt=-987) 96 [para_from,78,80] f(x,f(f(x,y),f(x,y)))=f(x,y). >> BACK DEMODULATING HINT 72 WITH 99. >> BACK DEMODULATING HINT 71 WITH 99. >> BACK DEMODULATING HINT 5 WITH 99. >> BACK DEMODULATING HINT 70 WITH 101. >> BACK DEMODULATING HINT 6 WITH 101. >> BACK DEMODULATING HINT 72 WITH 103. >> BACK DEMODULATING HINT 7 WITH 103. given clause #12: (wt=-991) 98 [para_into,96,78,demod,79,79] f(f(x,y),f(x,x))=x. >> BACK DEMODULATING HINT 8 WITH 105. given clause #13: (wt=-989) 102 [back_demod,90,demod,99,flip.1] f(x,f(f(x,x),y))=f(x,x). ----> UNIT CONFLICT at 0.06 sec ----> 108 [binary,106,2] $Ans(B_SS). Length of proof is 9. Level of proof is 6. ---------------- PROOF ---------------- 2 [] f(f(A,A),f(A,B))!=A|$Ans(B_SS). 77,76 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 79,78 [para_into,76,76] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. 80 [para_into,76,76] f(x,f(f(x,y),f(f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))),u)))=f(x,y). 82 [para_into,80,76] f(f(x,y),f(f(f(x,y),f(y,z)),y))=f(f(x,y),f(y,z)). 87,86 [para_into,82,76,demod,77] f(f(f(f(x,y),f(y,z)),y),f(y,y))=y. 90 [para_from,86,82,demod,87,87] f(x,f(f(x,f(f(x,x),y)),f(x,x)))=f(x,f(f(x,x),y)). 96 [para_from,78,80] f(x,f(f(x,y),f(x,y)))=f(x,y). 99,98 [para_into,96,78,demod,79,79] f(f(x,y),f(x,x))=x. 102 [back_demod,90,demod,99,flip.1] f(x,f(f(x,x),y))=f(x,x). 106 [para_into,102,98,demod,99] f(f(x,x),f(x,y))=x. 108 [binary,106,2] $Ans(B_SS). ------------ end of proof ------------- >> BACK DEMODULATING HINT 71 WITH 107. >> BACK DEMODULATING HINT 10 WITH 107. >> BACK DEMODULATING HINT 9 WITH 107. >> BACK DEMODULATING HINT 66 WITH 110. NEW HINT: 111 [bsub_wt=2147483647, bsub_add_wt=-1000] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),x),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. >> BACK DEMODULATING HINT 14 WITH 110. >> BACK DEMODULATING HINT 11 WITH 110. given clause #14: (wt=-991) 106 [para_into,102,98,demod,99] f(f(x,x),f(x,y))=x. >> BACK DEMODULATING HINT 12 WITH 113. >> BACK DEMODULATING HINT 72 WITH 115. given clause #15: (wt=-989) 104 [para_into,98,98] f(f(f(x,x),y),x)=f(x,x). >> BACK DEMODULATING HINT 111 WITH 117. NEW HINT: 120 [bsub_wt=2147483647, bsub_add_wt=-1000] f(f(x,y),f(x,f(f(x,f(f(x,f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. >> BACK DEMODULATING HINT 70 WITH 117. >> BACK DEMODULATING HINT 68 WITH 117. NEW HINT: 121 [bsub_wt=2147483647, bsub_add_wt=-1000] f(f(x,y),f(y,f(f(x,y),f(y,z))))=f(f(x,y),f(y,z)). >> BACK DEMODULATING HINT 13 WITH 117. >> BACK DEMODULATING HINT 11 WITH 117. >> BACK DEMODULATING HINT 66 WITH 119. >> BACK DEMODULATING HINT 14 WITH 119. >> BACK DEMODULATING HINT 11 WITH 119. given clause #16: (wt=-987) 112 [para_into,106,98] f(f(f(x,y),f(x,y)),x)=f(x,y). given clause #17: (wt=-985) 100 [para_into,96,76,demod,77,77] f(f(f(f(x,y),f(y,z)),u),f(y,y))=y. >> BACK DEMODULATING HINT 15 WITH 123. >> BACK DEMODULATING HINT 16 WITH 125. >> BACK DEMODULATING HINT 71 WITH 127. >> BACK DEMODULATING HINT 70 WITH 127. >> BACK DEMODULATING HINT 17 WITH 127. >> BACK DEMODULATING HINT 121 WITH 129. given clause #18: (wt=-991) 126 [para_into,100,98] f(f(x,y),f(y,y))=y. >> BACK DEMODULATING HINT 18 WITH 131. >> BACK DEMODULATING HINT 71 WITH 133. >> BACK DEMODULATING HINT 19 WITH 133. given clause #19: (wt=-991) 132 [para_from,126,112,demod,127,127] f(f(x,x),f(y,x))=x. >> BACK DEMODULATING HINT 74 WITH 135. >> BACK DEMODULATING HINT 72 WITH 135. >> BACK DEMODULATING HINT 20 WITH 135. >> BACK DEMODULATING HINT 21 WITH 137. >> BACK DEMODULATING HINT 22 WITH 139. given clause #20: (wt=-989) 134 [para_into,132,132] f(x,f(y,f(x,x)))=f(x,x). given clause #21: (wt=-987) 130 [para_from,126,98] f(x,f(f(y,x),f(y,x)))=f(y,x). >> BACK DEMODULATING HINT 23 WITH 141. >> BACK DEMODULATING HINT 24 WITH 143. given clause #22: (wt=-987) 136 [back_demod,94,demod,135,127] f(f(x,y),f(x,f(f(z,z),z)))=x. >> BACK DEMODULATING HINT 69 WITH 145. >> BACK DEMODULATING HINT 25 WITH 145. given clause #23: (wt=-989) 146 [para_from,136,132,demod,137] f(x,x)=f(x,f(f(y,y),y)). >> BACK DEMODULATING HINT 74 WITH 149. given clause #24: (wt=-989) 147 [copy,146,flip.1] f(x,f(f(y,y),y))=f(x,x). given clause #25: (wt=-989) 150 [para_into,147,132] f(x,f(y,f(y,y)))=f(x,x). given clause #26: (wt=-989) 151 [copy,150,flip.1] f(x,x)=f(x,f(y,f(y,y))). >> BACK DEMODULATING HINT 73 WITH 153. >> BACK DEMODULATING HINT 30 WITH 153. >> BACK DEMODULATING HINT 31 WITH 155. given clause #27: (wt=-987) 154 [para_from,151,132] f(f(x,f(y,f(y,y))),f(z,x))=x. given clause #28: (wt=-985) 122 [para_into,100,112] f(f(f(f(x,y),f(x,z)),u),f(x,x))=x. >> BACK DEMODULATING HINT 32 WITH 157. given clause #29: (wt=-985) 140 [para_from,130,100] f(f(x,f(f(y,z),f(z,u))),f(z,z))=z. >> BACK DEMODULATING HINT 33 WITH 159. given clause #30: (wt=-985) 142 [para_from,130,100] f(f(f(f(x,y),f(z,y)),u),f(y,y))=y. >> BACK DEMODULATING HINT 34 WITH 161. given clause #31: (wt=-985) 144 [para_into,136,136] f(x,f(f(x,y),f(f(z,z),z)))=f(x,y). given clause #32: (wt=-985) 152 [para_from,151,96] f(x,f(f(x,y),f(z,f(z,z))))=f(x,y). >> BACK DEMODULATING HINT 35 WITH 163. given clause #33: (wt=-985) 156 [para_into,122,130] f(f(x,f(f(y,z),f(y,u))),f(y,y))=y. given clause #34: (wt=-981) 116 [para_into,104,76,demod,110,flip.1] f(f(f(x,y),f(y,z)),y)=f(y,f(f(x,y),f(y,z))). given clause #35: (wt=-981) 148 [para_from,146,100] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(v,v),v)))=y. given clause #36: (wt=-981) 160 [para_into,142,146] f(f(f(f(x,y),f(z,y)),u),f(y,f(f(v,v),v)))=y. given clause #37: (wt=-981) 162 [para_into,152,154,flip.1] f(f(f(x,f(x,x)),f(y,f(y,y))),z)=f(x,f(x,x)). ----> UNIT CONFLICT at 0.18 sec ----> 165 [binary,164,3] $Ans(ONE_SS). Length of proof is 27. Level of proof is 17. ---------------- PROOF ---------------- 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(ONE_SS). 77,76 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 79,78 [para_into,76,76] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. 80 [para_into,76,76] f(x,f(f(x,y),f(f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))),u)))=f(x,y). 82 [para_into,80,76] f(f(x,y),f(f(f(x,y),f(y,z)),y))=f(f(x,y),f(y,z)). 84 [para_into,80,80] f(x,f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))))=f(x,y). 87,86 [para_into,82,76,demod,77] f(f(f(f(x,y),f(y,z)),y),f(y,y))=y. 88 [para_into,86,86] f(f(x,x),f(x,x))=x. 90 [para_from,86,82,demod,87,87] f(x,f(f(x,f(f(x,x),y)),f(x,x)))=f(x,f(f(x,x),y)). 92 [para_into,84,88] f(x,f(f(x,y),f(x,f(x,x))))=f(x,y). 94 [para_from,92,76] f(f(f(f(x,y),f(y,f(y,f(y,y)))),z),f(y,f(f(x,x),x)))=y. 96 [para_from,78,80] f(x,f(f(x,y),f(x,y)))=f(x,y). 99,98 [para_into,96,78,demod,79,79] f(f(x,y),f(x,x))=x. 100 [para_into,96,76,demod,77,77] f(f(f(f(x,y),f(y,z)),u),f(y,y))=y. 102 [back_demod,90,demod,99,flip.1] f(x,f(f(x,x),y))=f(x,x). 106 [para_into,102,98,demod,99] f(f(x,x),f(x,y))=x. 112 [para_into,106,98] f(f(f(x,y),f(x,y)),x)=f(x,y). 127,126 [para_into,100,98] f(f(x,y),f(y,y))=y. 132 [para_from,126,112,demod,127,127] f(f(x,x),f(y,x))=x. 135,134 [para_into,132,132] f(x,f(y,f(x,x)))=f(x,x). 137,136 [back_demod,94,demod,135,127] f(f(x,y),f(x,f(f(z,z),z)))=x. 146 [para_from,136,132,demod,137] f(x,x)=f(x,f(f(y,y),y)). 147 [copy,146,flip.1] f(x,f(f(y,y),y))=f(x,x). 150 [para_into,147,132] f(x,f(y,f(y,y)))=f(x,x). 151 [copy,150,flip.1] f(x,x)=f(x,f(y,f(y,y))). 152 [para_from,151,96] f(x,f(f(x,y),f(z,f(z,z))))=f(x,y). 154 [para_from,151,132] f(f(x,f(y,f(y,y))),f(z,x))=x. 162 [para_into,152,154,flip.1] f(f(f(x,f(x,x)),f(y,f(y,y))),z)=f(x,f(x,x)). 164 [para_into,162,126] f(x,f(x,x))=f(y,f(y,y)). 165 [binary,164,3] $Ans(ONE_SS). ------------ end of proof ------------- given clause #38: (wt=-989) 164 [para_into,162,126] f(x,f(x,x))=f(y,f(y,y)). given clause #39: (wt=-979) 114 [para_from,106,82,demod,107,107] f(x,f(f(x,f(f(x,y),z)),f(x,y)))=f(x,f(f(x,y),z)). >> BACK DEMODULATING HINT 72 WITH 167. given clause #40: (wt=-979) 124 [para_into,100,106] f(f(f(x,f(f(x,y),z)),u),f(f(x,y),f(x,y)))=f(x,y). >> BACK DEMODULATING HINT 37 WITH 169. given clause #41: (wt=-979) 128 [para_from,100,80,demod,117] f(f(x,y),f(y,f(f(x,y),f(y,z))))=f(f(x,y),f(y,z)). given clause #42: (wt=-979) 138 [para_from,132,100] f(f(f(x,f(f(y,x),z)),u),f(f(y,x),f(y,x)))=f(y,x). >> BACK DEMODULATING HINT 38 WITH 171. given clause #43: (wt=-983) 170 [para_into,138,136] f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x). >> BACK DEMODULATING HINT 40 WITH 174. given clause #44: (wt=-985) 172 [para_from,170,104] f(f(x,y),f(y,x))=f(f(y,x),f(y,x)). >> BACK DEMODULATING HINT 41 WITH 176. given clause #45: (wt=-993) 177 [para_into,172,172,demod,99,119,176] f(x,y)=f(y,x). >> BACK DEMODULATING HINT 43 WITH 179. >> BACK DEMODULATING HINT 44 WITH 181. >> BACK DEMODULATING HINT 72 WITH 183. >> BACK DEMODULATING HINT 72 WITH 185. given clause #46: (wt=-987) 175 [para_into,172,172,demod,107,119,flip.1] f(x,f(f(y,x),f(x,y)))=f(y,x). given clause #47: (wt=-983) 178 [para_from,177,170] f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(y,x). given clause #48: (wt=-983) 180 [para_from,177,170] f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(y,x). given clause #49: (wt=-979) 158 [para_into,140,154] f(f(x,f(y,f(f(z,y),u))),f(f(z,y),f(z,y)))=f(z,y). >> BACK DEMODULATING HINT 45 WITH 187. given clause #50: (wt=-979) 166 [para_into,114,130,demod,131,131] f(x,f(f(x,f(f(y,x),z)),f(y,x)))=f(x,f(f(y,x),z)). given clause #51: (wt=-979) 173 [para_from,170,136] f(f(x,y),f(f(f(y,x),z),f(f(u,u),u)))=f(f(y,x),z). given clause #52: (wt=-989) 188 [para_into,173,177,demod,145] f(f(x,y),z)=f(f(y,x),z). given clause #53: (wt=-989) 189 [para_into,188,177] f(x,f(y,z))=f(f(z,y),x). >> BACK DEMODULATING HINT 51 WITH 194. given clause #54: (wt=-989) 190 [copy,189,flip.1] f(f(x,y),z)=f(z,f(y,x)). given clause #55: (wt=-985) 191 [para_into,189,189] f(x,f(f(y,z),u))=f(f(f(z,y),u),x). given clause #56: (wt=-985) 192 [copy,191,flip.1] f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). given clause #57: (wt=-985) 195 [para_into,190,189] f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). >> BACK DEMODULATING HINT 53 WITH 197. given clause #58: (wt=-979) 182 [para_from,177,114] f(x,f(f(x,f(f(x,y),z)),f(y,x)))=f(x,f(f(x,y),z)). given clause #59: (wt=-979) 184 [para_from,177,114] f(x,f(f(x,f(f(y,x),z)),f(x,y)))=f(x,f(f(x,y),z)). given clause #60: (wt=-975) 118 [back_demod,109,demod,117] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))). given clause #61: (wt=-975) 193 [para_from,189,178] f(f(f(f(x,y),z),u),f(f(f(y,x),z),f(f(x,y),z)))=f(z,f(x,y)). given clause #62: (wt=-967) 196 [para_from,195,180] f(f(f(f(x,y),f(z,u)),v),f(f(f(y,x),f(u,z)),f(f(z,u),f(x,y))))=f(f(z,u),f(x,y)). given clause #63: (wt=-965) 168 [para_into,124,156] f(f(f(x,y),z),f(f(x,f(f(y,u),f(y,v))),f(x,f(f(y,u),f(y,v)))))=f(x,f(f(y,u),f(y,v))). >> BACK DEMODULATING HINT 54 WITH 199. given clause #64: (wt=-975) 198 [para_into,168,158,demod,159,159] f(f(f(f(x,f(y,f(f(z,y),u))),z),v),f(f(z,y),f(z,y)))=f(z,y). >> BACK DEMODULATING HINT 55 WITH 201. given clause #65: (wt=-975) 200 [para_into,198,192] f(f(x,f(f(f(y,f(f(z,y),u)),v),z)),f(f(z,y),f(z,y)))=f(z,y). given clause #66: (wt=-965) 186 [para_into,158,122] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,u),f(z,v)),y)))=f(f(f(z,u),f(z,v)),y). >> BACK DEMODULATING HINT 56 WITH 203. given clause #67: (wt=-965) 202 [para_into,186,177] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,v),f(z,u)),y)))=f(f(f(z,v),f(z,u)),y). >> BACK DEMODULATING HINT 57 WITH 205. given clause #68: (wt=-965) 204 [para_into,202,190] f(f(f(f(f(x,y),f(x,z)),u),f(f(f(x,z),f(x,y)),u)),f(f(u,x),v))=f(f(f(x,z),f(x,y)),u). >> BACK DEMODULATING HINT 58 WITH 207. given clause #69: (wt=-983) 206 [para_into,204,200,flip.1] f(f(f(x,f(f(y,x),z)),f(x,u)),y)=f(y,x). given clause #70: (wt=-975) 208 [para_into,206,160] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(f(f(u,y),f(v,y)),x). >> BACK DEMODULATING HINT 60 WITH 210. >> BACK DEMODULATING HINT 61 WITH 212. >> BACK DEMODULATING HINT 12 WITH 214. >> BACK DEMODULATING HINT 12 WITH 216. >> BACK DEMODULATING HINT 62 WITH 218. >> BACK DEMODULATING HINT 59 WITH 218. given clause #71: (wt=-987) 213 [para_into,208,154,flip.1] f(f(f(x,y),f(z,y)),z)=f(z,y). >> BACK DEMODULATING HINT 4 WITH 220. >> BACK DEMODULATING HINT 4 WITH 222. given clause #72: (wt=-987) 215 [para_into,208,106,flip.1] f(f(f(x,y),f(z,y)),x)=f(x,y). given clause #73: (wt=-987) 219 [para_into,213,190] f(x,f(f(x,y),f(z,y)))=f(x,y). >> BACK DEMODULATING HINT 72 WITH 224. >> BACK DEMODULATING HINT 68 WITH 224. given clause #74: (wt=-987) 221 [para_into,213,177] f(x,f(f(y,z),f(x,z)))=f(x,z). >> BACK DEMODULATING HINT 121 WITH 226. given clause #75: (wt=-985) 223 [para_into,219,106] f(x,f(f(x,f(y,z)),y))=f(x,f(y,z)). >> BACK DEMODULATING HINT 72 WITH 228. given clause #76: (wt=-985) 225 [para_into,221,106] f(x,f(y,f(x,f(y,z))))=f(x,f(y,z)). given clause #77: (wt=-979) 227 [para_into,223,188] f(x,f(f(x,f(f(y,z),u)),f(z,y)))=f(x,f(f(z,y),u)). given clause #78: (wt=-975) 209 [para_into,208,190] f(f(f(x,y),f(z,y)),f(f(u,v),f(u,y)))=f(f(f(x,y),f(z,y)),u). given clause #79: (wt=-975) 211 [para_into,208,177] f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(f(f(x,y),f(z,y)),u). given clause #80: (wt=-975) 217 [para_from,208,196,demod,212,210,194,flip.1] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(x,f(f(u,y),f(v,y))). given clause #81: (wt=-981) 229 [para_into,217,211] f(f(f(x,y),f(x,y)),z)=f(x,f(f(z,y),f(z,y))). ----> UNIT CONFLICT at 1.19 sec ----> 231 [binary,230,1] $Ans(A_SS). Length of proof is 66. Level of proof is 25. ---------------- PROOF ---------------- 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(A_SS). 77,76 [] f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z)))=y. 79,78 [para_into,76,76] f(f(x,y),f(x,f(f(x,f(f(f(f(z,x),f(x,u)),f(f(z,x),f(x,u))),f(f(z,x),f(x,u)))),f(f(x,f(f(z,z),z)),u))))=x. 80 [para_into,76,76] f(x,f(f(x,y),f(f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))),u)))=f(x,y). 82 [para_into,80,76] f(f(x,y),f(f(f(x,y),f(y,z)),y))=f(f(x,y),f(y,z)). 84 [para_into,80,80] f(x,f(f(x,y),f(f(f(z,x),f(z,x)),f(z,x))))=f(x,y). 87,86 [para_into,82,76,demod,77] f(f(f(f(x,y),f(y,z)),y),f(y,y))=y. 88 [para_into,86,86] f(f(x,x),f(x,x))=x. 90 [para_from,86,82,demod,87,87] f(x,f(f(x,f(f(x,x),y)),f(x,x)))=f(x,f(f(x,x),y)). 92 [para_into,84,88] f(x,f(f(x,y),f(x,f(x,x))))=f(x,y). 94 [para_from,92,76] f(f(f(f(x,y),f(y,f(y,f(y,y)))),z),f(y,f(f(x,x),x)))=y. 96 [para_from,78,80] f(x,f(f(x,y),f(x,y)))=f(x,y). 99,98 [para_into,96,78,demod,79,79] f(f(x,y),f(x,x))=x. 100 [para_into,96,76,demod,77,77] f(f(f(f(x,y),f(y,z)),u),f(y,y))=y. 102 [back_demod,90,demod,99,flip.1] f(x,f(f(x,x),y))=f(x,x). 104 [para_into,98,98] f(f(f(x,x),y),x)=f(x,x). 107,106 [para_into,102,98,demod,99] f(f(x,x),f(x,y))=x. 110,109 [para_into,102,76,flip.1] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(f(f(x,y),f(y,z)),y). 112 [para_into,106,98] f(f(f(x,y),f(x,y)),x)=f(x,y). 117,116 [para_into,104,76,demod,110,flip.1] f(f(f(x,y),f(y,z)),y)=f(y,f(f(x,y),f(y,z))). 119,118 [back_demod,109,demod,117] f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))). 122 [para_into,100,112] f(f(f(f(x,y),f(x,z)),u),f(x,x))=x. 124 [para_into,100,106] f(f(f(x,f(f(x,y),z)),u),f(f(x,y),f(x,y)))=f(x,y). 127,126 [para_into,100,98] f(f(x,y),f(y,y))=y. 130 [para_from,126,98] f(x,f(f(y,x),f(y,x)))=f(y,x). 132 [para_from,126,112,demod,127,127] f(f(x,x),f(y,x))=x. 135,134 [para_into,132,132] f(x,f(y,f(x,x)))=f(x,x). 137,136 [back_demod,94,demod,135,127] f(f(x,y),f(x,f(f(z,z),z)))=x. 138 [para_from,132,100] f(f(f(x,f(f(y,x),z)),u),f(f(y,x),f(y,x)))=f(y,x). 140 [para_from,130,100] f(f(x,f(f(y,z),f(z,u))),f(z,z))=z. 142 [para_from,130,100] f(f(f(f(x,y),f(z,y)),u),f(y,y))=y. 145,144 [para_into,136,136] f(x,f(f(x,y),f(f(z,z),z)))=f(x,y). 146 [para_from,136,132,demod,137] f(x,x)=f(x,f(f(y,y),y)). 147 [copy,146,flip.1] f(x,f(f(y,y),y))=f(x,x). 150 [para_into,147,132] f(x,f(y,f(y,y)))=f(x,x). 151 [copy,150,flip.1] f(x,x)=f(x,f(y,f(y,y))). 154 [para_from,151,132] f(f(x,f(y,f(y,y))),f(z,x))=x. 156 [para_into,122,130] f(f(x,f(f(y,z),f(y,u))),f(y,y))=y. 159,158 [para_into,140,154] f(f(x,f(y,f(f(z,y),u))),f(f(z,y),f(z,y)))=f(z,y). 160 [para_into,142,146] f(f(f(f(x,y),f(z,y)),u),f(y,f(f(v,v),v)))=y. 168 [para_into,124,156] f(f(f(x,y),z),f(f(x,f(f(y,u),f(y,v))),f(x,f(f(y,u),f(y,v)))))=f(x,f(f(y,u),f(y,v))). 170 [para_into,138,136] f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x). 172 [para_from,170,104] f(f(x,y),f(y,x))=f(f(y,x),f(y,x)). 173 [para_from,170,136] f(f(x,y),f(f(f(y,x),z),f(f(u,u),u)))=f(f(y,x),z). 176,175 [para_into,172,172,demod,107,119,flip.1] f(x,f(f(y,x),f(x,y)))=f(y,x). 177 [para_into,172,172,demod,99,119,176] f(x,y)=f(y,x). 178 [para_from,177,170] f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(y,x). 180 [para_from,177,170] f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(y,x). 186 [para_into,158,122] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,u),f(z,v)),y)))=f(f(f(z,u),f(z,v)),y). 188 [para_into,173,177,demod,145] f(f(x,y),z)=f(f(y,x),z). 189 [para_into,188,177] f(x,f(y,z))=f(f(z,y),x). 190 [copy,189,flip.1] f(f(x,y),z)=f(z,f(y,x)). 191 [para_into,189,189] f(x,f(f(y,z),u))=f(f(f(z,y),u),x). 192 [copy,191,flip.1] f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). 194,193 [para_from,189,178] f(f(f(f(x,y),z),u),f(f(f(y,x),z),f(f(x,y),z)))=f(z,f(x,y)). 195 [para_into,190,189] f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). 196 [para_from,195,180] f(f(f(f(x,y),f(z,u)),v),f(f(f(y,x),f(u,z)),f(f(z,u),f(x,y))))=f(f(z,u),f(x,y)). 198 [para_into,168,158,demod,159,159] f(f(f(f(x,f(y,f(f(z,y),u))),z),v),f(f(z,y),f(z,y)))=f(z,y). 200 [para_into,198,192] f(f(x,f(f(f(y,f(f(z,y),u)),v),z)),f(f(z,y),f(z,y)))=f(z,y). 202 [para_into,186,177] f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,v),f(z,u)),y)))=f(f(f(z,v),f(z,u)),y). 204 [para_into,202,190] f(f(f(f(f(x,y),f(x,z)),u),f(f(f(x,z),f(x,y)),u)),f(f(u,x),v))=f(f(f(x,z),f(x,y)),u). 206 [para_into,204,200,flip.1] f(f(f(x,f(f(y,x),z)),f(x,u)),y)=f(y,x). 208 [para_into,206,160] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(f(f(u,y),f(v,y)),x). 210,209 [para_into,208,190] f(f(f(x,y),f(z,y)),f(f(u,v),f(u,y)))=f(f(f(x,y),f(z,y)),u). 212,211 [para_into,208,177] f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(f(f(x,y),f(z,y)),u). 217 [para_from,208,196,demod,212,210,194,flip.1] f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(x,f(f(u,y),f(v,y))). 229 [para_into,217,211] f(f(f(x,y),f(x,y)),z)=f(x,f(f(z,y),f(z,y))). 230 [para_into,229,190] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 231 [binary,230,1] $Ans(A_SS). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 81 clauses generated 20988 para_from generated 9016 para_into generated 11972 demod & eval rewrites 24849 clauses wt,lit,sk delete 20574 tautologies deleted 0 clauses forward subsumed 365 (subsumed by sos) 31 unit deletions 0 factor simplifications 0 clauses kept 84 new demodulators 67 empty clauses 3 clauses back demodulated 17 clauses back subsumed 2 usable size 64 sos size 1 demodulators size 51 passive size 3 hot size 0 Kbytes malloced 479 ----------- times (seconds) ----------- user CPU time 1.19 (0 hr, 0 min, 1 sec) system CPU time 0.03 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) input time 0.01 clausify time 0.00 process input 0.00 pick given time 0.00 para_into time 0.06 para_from time 0.03 pre_process time 1.06 renumber time 0.02 demod time 0.68 order equalities 0.05 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.07 hints keep time 0.19 sort lits time 0.00 forward subsume 0.00 delete cl time 0.01 keep cl time 0.00 hints time 0.00 print_cl time 0.00 conflict time 0.00 new demod time 0.00 post_process time 0.01 back demod time 0.01 back subsume 0.00 factor time 0.00 unindex time 0.00 That finishes the proof of the theorem. Process 2359 finished Mon Sep 15 12:17:32 2003