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