1----- Otter 3.3f, August 2004 ----- 2The process was started by mccune on gyro.thornwood, 3Mon Aug 2 15:30:37 2004 4The command was "../../bin/otter". The process ID is 8391. 5 6set(knuth_bendix). 7 dependent: set(anl_eq). 8 dependent: set(para_from). 9 dependent: set(para_into). 10 dependent: clear(para_from_right). 11 dependent: clear(para_into_right). 12 dependent: set(para_from_vars). 13 dependent: set(eq_units_both_ways). 14 dependent: set(dynamic_demod_all). 15 dependent: set(dynamic_demod). 16 dependent: set(order_eq). 17 dependent: set(back_demod). 18 dependent: set(process_input). 19 dependent: set(lrpo). 20assign(max_proofs,3). 21clear(print_kept). 22clear(print_new_demod). 23clear(print_back_demod). 24assign(stats_level,1). 25 26list(usable). 270 [] x=x. 28end_of_list. 29 30list(passive). 311 [] f(a,g(a))!=f(b,g(b))|$Ans(R_inverse). 322 [] f(a,f(b,g(b)))!=a|$Ans(R_ident). 333 [] f(f(a,b),c)!=f(a,f(b,c))|$Ans(assoc). 34end_of_list. 35 36list(sos). 370 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 38end_of_list. 39 40------------> process usable: 41** KEPT (pick-wt=3): 4 [] x=x. 42 Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x. 43 44------------> process sos: 45** KEPT (pick-wt=18): 5 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 46---> New Demodulator: 6 [new_demod,5] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 47>>>> Starting back demodulation with 6. 48 49======= end of input processing ======= 50 51=========== start of search =========== 52 53given clause #1: (wt=18) 5 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 54 55given clause #2: (wt=23) 9 [para_into,5.1.1.2.1.2.1,5.1.1] f(x,g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,x))))=u. 56 57given clause #3: (wt=28) 16 [para_into,9.1.1.2.1.1.1,5.1.1] f(x,g(f(f(y,f(z,g(z))),f(u,x))))=f(f(f(v,g(v)),g(f(y,u))),f(w,g(w))). 58 59given clause #4: (wt=24) 33 [para_into,16.1.1,9.1.1,flip.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(f(z,u))),z))),f(v,g(v)))=u. 60 61given clause #5: (wt=15) 56 [para_into,33.1.1.1.2.1,33.1.1] f(f(f(x,g(x)),g(g(y))),f(z,g(z)))=y. 62 63given clause #6: (wt=19) 71 [para_from,33.1.1,5.1.1.2.1.2] f(f(x,g(x)),g(f(y,z)))=f(f(u,g(u)),g(f(y,z))). 6493 back subsumes 71. 65 66given clause #7: (wt=13) 103 [back_demod,62,demod,97] f(x,f(y,g(y)))=f(x,f(z,g(z))). 67 68-------- PROOF -------- 110 [binary,109.1,1.1] $Ans(R_inverse). 69 70----> UNIT CONFLICT at 0.01 sec ----> 110 [binary,109.1,1.1] $Ans(R_inverse). 71 72Length of proof is 9. Level of proof is 7. 73 74---------------- PROOF ---------------- 75 761 [] f(a,g(a))!=f(b,g(b))|$Ans(R_inverse). 775 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 789 [para_into,5.1.1.2.1.2.1,5.1.1] f(x,g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,x))))=u. 7916 [para_into,9.1.1.2.1.1.1,5.1.1] f(x,g(f(f(y,f(z,g(z))),f(u,x))))=f(f(f(v,g(v)),g(f(y,u))),f(w,g(w))). 8034,33 [para_into,16.1.1,9.1.1,flip.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(f(z,u))),z))),f(v,g(v)))=u. 8154 [para_into,33.1.1.1.2.1.1,16.1.1] f(f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w)))))),f(v6,g(v6)))=f(u,f(v7,g(v7))). 8262 [copy,54,flip.1] f(x,f(y,g(y)))=f(f(f(z,g(z)),g(f(f(f(f(u,g(u)),g(f(v,x))),f(w,g(w))),f(v,f(v6,g(v6)))))),f(v7,g(v7))). 8371 [para_from,33.1.1,5.1.1.2.1.2] f(f(x,g(x)),g(f(y,z)))=f(f(u,g(u)),g(f(y,z))). 8497,96 [para_into,71.1.1,9.1.1,flip.1] f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w))))))=u. 85103 [back_demod,62,demod,97] f(x,f(y,g(y)))=f(x,f(z,g(z))). 86109 [para_from,103.1.1,33.1.1.1.2.1.1.2.1,demod,34] f(x,g(x))=f(y,g(y)). 87110 [binary,109.1,1.1] $Ans(R_inverse). 88 89------------ end of proof ------------- 90 91 92given clause #8: (wt=9) 109 [para_from,103.1.1,33.1.1.1.2.1.1.2.1,demod,34] f(x,g(x))=f(y,g(y)). 93 94given clause #9: (wt=14) 124 [para_from,109.1.1,5.1.1.2.1.2.1] f(x,g(f(g(y),f(f(z,g(z)),x))))=y. 95 96given clause #10: (wt=15) 93 [para_into,71.1.1.2.1,56.1.1,demod,57] f(f(x,g(x)),g(y))=f(f(z,g(z)),g(y)). 97156 back subsumes 91. 98158 back subsumes 100. 99 100given clause #11: (wt=15) 157 [para_into,93.1.1,109.1.1] f(x,g(x))=f(f(y,g(y)),g(f(z,g(z)))). 101 102given clause #12: (wt=15) 159 [copy,157,flip.1] f(f(x,g(x)),g(f(y,g(y))))=f(z,g(z)). 103 104given clause #13: (wt=11) 203 [para_from,159.1.1,33.1.1.1.2.1.1.2.1,demod,121] g(f(x,g(x)))=g(f(y,g(y))). 105 106given clause #14: (wt=16) 130 [para_into,124.1.1.2.1.2,109.1.1] f(g(f(x,g(x))),g(f(g(y),f(z,g(z)))))=y. 107 108given clause #15: (wt=16) 190 [para_from,157.1.1,9.1.1.2.1.1.1.2.1,demod,117] f(x,g(f(g(g(f(y,g(y)))),f(z,x))))=g(z). 109 110given clause #16: (wt=17) 206 [para_into,203.1.1.1.2,203.1.1] g(f(f(x,g(x)),g(f(y,g(y)))))=g(f(z,g(z))). 111 112given clause #17: (wt=17) 207 [copy,206,flip.1] g(f(x,g(x)))=g(f(f(y,g(y)),g(f(z,g(z))))). 113 114given clause #18: (wt=17) 241 [para_into,190.1.1,5.1.1,flip.1] g(f(f(x,g(x)),g(f(y,g(g(f(z,g(z))))))))=y. 115391 back subsumes 93. 116 117given clause #19: (wt=13) 391 [para_from,241.1.1,93.1.1.2,demod,242] f(f(x,g(x)),y)=f(f(z,g(z)),y). 118430 back subsumes 377. 119431 back subsumes 320. 120432 back subsumes 278. 121433 back subsumes 156. 122435 back subsumes 418. 123436 back subsumes 347. 124437 back subsumes 307. 125438 back subsumes 158. 126439 back subsumes 164. 127440 back subsumes 179. 128 129given clause #20: (wt=18) 229 [para_into,190.1.1.2.1.2,109.1.1] f(g(x),g(f(g(g(f(y,g(y)))),f(z,g(z)))))=g(x). 130 131given clause #21: (wt=16) 441 [para_into,229.1.1.1,241.1.1,demod,242] f(x,g(f(g(g(f(y,g(y)))),f(z,g(z)))))=x. 132 133given clause #22: (wt=12) 505 [para_from,441.1.1,33.1.1.1.2.1.1,demod,117] g(g(g(f(x,g(x)))))=f(y,g(y)). 134 135given clause #23: (wt=12) 537 [copy,505,flip.1] f(x,g(x))=g(g(g(f(y,g(y))))). 136 137given clause #24: (wt=14) 568 [para_from,537.1.1,241.1.1.1] g(g(g(g(f(x,g(x))))))=g(f(y,g(y))). 138 139given clause #25: (wt=14) 625 [copy,568,flip.1] g(f(x,g(x)))=g(g(g(g(f(y,g(y)))))). 140 141given clause #26: (wt=15) 562 [para_into,537.1.1,537.1.1] g(g(g(f(x,g(x)))))=g(g(g(f(y,g(y))))). 142 143given clause #27: (wt=13) 812 [para_from,562.1.1,130.1.1.2.1.1,demod,131] g(g(f(x,g(x))))=g(g(f(y,g(y)))). 144 145given clause #28: (wt=15) 577 [para_from,537.1.1,505.1.1.1.1.1] g(g(g(g(g(g(f(x,g(x))))))))=f(y,g(y)). 146 147given clause #29: (wt=15) 630 [copy,577,flip.1] f(x,g(x))=g(g(g(g(g(g(f(y,g(y)))))))). 148 149given clause #30: (wt=16) 478 [para_into,441.1.1,109.1.1] f(x,g(x))=f(g(g(f(y,g(y)))),f(z,g(z))). 150 151given clause #31: (wt=16) 480 [copy,478,flip.1] f(g(g(f(x,g(x)))),f(y,g(y)))=f(z,g(z)). 152-------- PROOF -------- 1296 [binary,1294.1,2.1] $Ans(R_ident). 153 154----> UNIT CONFLICT at 0.12 sec ----> 1296 [binary,1294.1,2.1] $Ans(R_ident). 155 156Length of proof is 33. Level of proof is 17. 157 158---------------- PROOF ---------------- 159 1602 [] f(a,f(b,g(b)))!=a|$Ans(R_ident). 1615 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 1629 [para_into,5.1.1.2.1.2.1,5.1.1] f(x,g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,x))))=u. 16316 [para_into,9.1.1.2.1.1.1,5.1.1] f(x,g(f(f(y,f(z,g(z))),f(u,x))))=f(f(f(v,g(v)),g(f(y,u))),f(w,g(w))). 16434,33 [para_into,16.1.1,9.1.1,flip.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(f(z,u))),z))),f(v,g(v)))=u. 16554 [para_into,33.1.1.1.2.1.1,16.1.1] f(f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w)))))),f(v6,g(v6)))=f(u,f(v7,g(v7))). 16657,56 [para_into,33.1.1.1.2.1,33.1.1] f(f(f(x,g(x)),g(g(y))),f(z,g(z)))=y. 16762 [copy,54,flip.1] f(x,f(y,g(y)))=f(f(f(z,g(z)),g(f(f(f(f(u,g(u)),g(f(v,x))),f(w,g(w))),f(v,f(v6,g(v6)))))),f(v7,g(v7))). 16871 [para_from,33.1.1,5.1.1.2.1.2] f(f(x,g(x)),g(f(y,z)))=f(f(u,g(u)),g(f(y,z))). 16993 [para_into,71.1.1.2.1,56.1.1,demod,57] f(f(x,g(x)),g(y))=f(f(z,g(z)),g(y)). 17097,96 [para_into,71.1.1,9.1.1,flip.1] f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w))))))=u. 171103 [back_demod,62,demod,97] f(x,f(y,g(y)))=f(x,f(z,g(z))). 172109 [para_from,103.1.1,33.1.1.1.2.1.1.2.1,demod,34] f(x,g(x))=f(y,g(y)). 173117,116 [para_from,109.1.1,33.1.1.1.2.1.1] f(f(f(x,g(x)),g(f(f(y,g(y)),z))),f(u,g(u)))=g(z). 174124 [para_from,109.1.1,5.1.1.2.1.2.1] f(x,g(f(g(y),f(f(z,g(z)),x))))=y. 175130 [para_into,124.1.1.2.1.2,109.1.1] f(g(f(x,g(x))),g(f(g(y),f(z,g(z)))))=y. 176157 [para_into,93.1.1,109.1.1] f(x,g(x))=f(f(y,g(y)),g(f(z,g(z)))). 177190 [para_from,157.1.1,9.1.1.2.1.1.1.2.1,demod,117] f(x,g(f(g(g(f(y,g(y)))),f(z,x))))=g(z). 178213 [para_from,130.1.1,33.1.1.1.2.1.1.2.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(z)),g(f(u,g(u)))))),f(v,g(v)))=g(f(g(z),f(w,g(w)))). 179217 [copy,213,flip.1] g(f(g(x),f(y,g(y))))=f(f(f(z,g(z)),g(f(f(f(u,g(u)),g(x)),g(f(v,g(v)))))),f(w,g(w))). 180229 [para_into,190.1.1.2.1.2,109.1.1] f(g(x),g(f(g(g(f(y,g(y)))),f(z,g(z)))))=g(x). 181242,241 [para_into,190.1.1,5.1.1,flip.1] g(f(f(x,g(x)),g(f(y,g(g(f(z,g(z))))))))=y. 182441 [para_into,229.1.1.1,241.1.1,demod,242] f(x,g(f(g(g(f(y,g(y)))),f(z,g(z)))))=x. 183478 [para_into,441.1.1,109.1.1] f(x,g(x))=f(g(g(f(y,g(y)))),f(z,g(z))). 184480 [copy,478,flip.1] f(g(g(f(x,g(x)))),f(y,g(y)))=f(z,g(z)). 185505 [para_from,441.1.1,33.1.1.1.2.1.1,demod,117] g(g(g(f(x,g(x)))))=f(y,g(y)). 186537 [copy,505,flip.1] f(x,g(x))=g(g(g(f(y,g(y))))). 187577 [para_from,537.1.1,505.1.1.1.1.1] g(g(g(g(g(g(f(x,g(x))))))))=f(y,g(y)). 188630 [copy,577,flip.1] f(x,g(x))=g(g(g(g(g(g(f(y,g(y)))))))). 189967 [para_from,577.1.1,130.1.1.1.1.2] f(g(f(g(g(g(g(g(f(x,g(x))))))),f(y,g(y)))),g(f(g(z),f(u,g(u)))))=z. 1901059 [para_from,630.1.1,56.1.1.1.1] f(f(g(g(g(g(g(g(f(x,g(x)))))))),g(g(y))),f(z,g(z)))=y. 1911189,1188 [para_from,480.1.1,441.1.1.2.1] f(x,g(f(y,g(y))))=x. 1921197,1196 [back_demod,217,demod,1189,117] g(f(g(x),f(y,g(y))))=g(g(x)). 1931227,1226 [back_demod,967,demod,1197,1197] f(g(g(g(g(g(g(f(x,g(x)))))))),g(g(y)))=y. 1941294 [back_demod,1059,demod,1227] f(x,f(y,g(y)))=x. 1951296 [binary,1294.1,2.1] $Ans(R_ident). 196 197------------ end of proof ------------- 198 1991439 back subsumes 1429. 2001440 back subsumes 1432. 201 202given clause #32: (wt=8) 1294 [back_demod,1059,demod,1227] f(x,f(y,g(y)))=x. 203 204given clause #33: (wt=8) 1393 [back_demod,529,demod,1295,1339,1331] f(f(x,y),g(y))=x. 205 206given clause #34: (wt=5) 1528 [back_demod,1463,demod,1501] g(g(x))=x. 207 208given clause #35: (wt=8) 1395 [back_demod,513,demod,1295,1295,1339,1331] f(g(x),f(x,y))=y. 209 210given clause #36: (wt=8) 1447 [back_demod,48,demod,1295,1337,1295,1295,1295,1444,flip.1] f(x,f(g(x),y))=y. 211 212given clause #37: (wt=8) 1504 [para_into,1393.1.1.1,109.1.1,demod,1499] f(f(x,g(x)),y)=y. 213 214given clause #38: (wt=8) 1516 [back_demod,1412,demod,1505,1499] f(f(g(x),x),y)=y. 215 216given clause #39: (wt=8) 1532 [back_demod,1403,demod,1505] f(x,f(g(y),y))=x. 217 218given clause #40: (wt=8) 1550 [para_from,1528.1.1,1393.1.1.2] f(f(x,g(y)),y)=x. 219 220given clause #41: (wt=9) 1439 [back_demod,89,demod,1295,1313,1339,1293] f(x,g(x))=f(g(y),y). 221 222given clause #42: (wt=9) 1440 [back_demod,82,demod,1295,1313,1339,1293] f(g(x),x)=f(y,g(y)). 223 224given clause #43: (wt=9) 1552 [para_into,1532.1.1,1516.1.1] f(g(x),x)=f(g(y),y). 225 226given clause #44: (wt=10) 1530 [back_demod,1345,demod,1529,1527] g(f(x,y))=f(g(y),g(x)). 227 228given clause #45: (wt=13) 1546 [back_demod,1437,demod,1531,1531,1531,1529,1529,1529] f(f(g(x),g(y)),f(f(y,x),z))=z. 229 230given clause #46: (wt=13) 1554 [para_from,1530.1.1,1447.1.1.2.1] f(f(x,y),f(f(g(y),g(x)),z))=z. 231 232given clause #47: (wt=13) 1557 [para_from,1530.1.1,1504.1.1.1.2] f(f(f(x,y),f(g(y),g(x))),z)=z. 233 234given clause #48: (wt=13) 1559 [para_from,1530.1.1,1550.1.1.1.2] f(f(x,f(g(y),g(z))),f(z,y))=x. 235 236given clause #49: (wt=13) 1561 [para_from,1530.1.1,1393.1.1.2] f(f(x,f(y,z)),f(g(z),g(y)))=x. 237 238given clause #50: (wt=13) 1563 [para_from,1530.1.1,1294.1.1.2.2] f(x,f(f(y,z),f(g(z),g(y))))=x. 239 240given clause #51: (wt=13) 1569 [para_into,1546.1.1.1.1,1528.1.1] f(f(x,g(y)),f(f(y,g(x)),z))=z. 241 242given clause #52: (wt=13) 1573 [para_into,1546.1.1.1.2,1528.1.1] f(f(g(x),y),f(f(g(y),x),z))=z. 243 244given clause #53: (wt=13) 1581 [para_into,1557.1.1.1.2.1,1528.1.1] f(f(f(x,g(y)),f(y,g(x))),z)=z. 245 246given clause #54: (wt=13) 1585 [para_into,1557.1.1.1.2.2,1528.1.1] f(f(f(g(x),y),f(g(y),x)),z)=z. 247 248given clause #55: (wt=13) 1589 [para_into,1559.1.1.1.2.1,1528.1.1] f(f(x,f(y,g(z))),f(z,g(y)))=x. 249 250given clause #56: (wt=13) 1593 [para_into,1559.1.1.1.2.2,1528.1.1] f(f(x,f(g(y),z)),f(g(z),y))=x. 251 252given clause #57: (wt=13) 1614 [para_into,1563.1.1.2.2.1,1528.1.1] f(x,f(f(y,g(z)),f(z,g(y))))=x. 253 254given clause #58: (wt=13) 1618 [para_into,1563.1.1.2.2.2,1528.1.1] f(x,f(f(g(y),z),f(g(z),y)))=x. 255 256given clause #59: (wt=14) 1542 [back_demod,1443,demod,1531,1531,1531,1529,1529] f(f(g(x),g(y)),f(y,z))=f(g(x),z). 257 258given clause #60: (wt=12) 1670 [para_into,1542.1.1.1.1,1528.1.1,demod,1529] f(f(x,g(y)),f(y,z))=f(x,z). 259-------- PROOF -------- 1718 [binary,1716.1,3.1] $Ans(assoc). 260 261----> UNIT CONFLICT at 0.20 sec ----> 1718 [binary,1716.1,3.1] $Ans(assoc). 262 263Length of proof is 76. Level of proof is 27. 264 265---------------- PROOF ---------------- 266 2673 [] f(f(a,b),c)!=f(a,f(b,c))|$Ans(assoc). 2685 [] f(x,g(f(y,f(f(f(z,g(z)),g(f(u,y))),x))))=u. 2699 [para_into,5.1.1.2.1.2.1,5.1.1] f(x,g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,x))))=u. 27016 [para_into,9.1.1.2.1.1.1,5.1.1] f(x,g(f(f(y,f(z,g(z))),f(u,x))))=f(f(f(v,g(v)),g(f(y,u))),f(w,g(w))). 27134,33 [para_into,16.1.1,9.1.1,flip.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(f(z,u))),z))),f(v,g(v)))=u. 27252 [para_into,33.1.1.1.2.1.1.2.1,9.1.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(z)),u))),f(v,g(v)))=g(f(f(f(f(w,g(w)),g(f(v6,z))),f(v7,g(v7))),f(v6,u))). 27354 [para_into,33.1.1.1.2.1.1,16.1.1] f(f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w)))))),f(v6,g(v6)))=f(u,f(v7,g(v7))). 27457,56 [para_into,33.1.1.1.2.1,33.1.1] f(f(f(x,g(x)),g(g(y))),f(z,g(z)))=y. 27560 [copy,52,flip.1] g(f(f(f(f(x,g(x)),g(f(y,z))),f(u,g(u))),f(y,v)))=f(f(f(w,g(w)),g(f(f(f(v6,g(v6)),g(z)),v))),f(v7,g(v7))). 27662 [copy,54,flip.1] f(x,f(y,g(y)))=f(f(f(z,g(z)),g(f(f(f(f(u,g(u)),g(f(v,x))),f(w,g(w))),f(v,f(v6,g(v6)))))),f(v7,g(v7))). 27771 [para_from,33.1.1,5.1.1.2.1.2] f(f(x,g(x)),g(f(y,z)))=f(f(u,g(u)),g(f(y,z))). 27893 [para_into,71.1.1.2.1,56.1.1,demod,57] f(f(x,g(x)),g(y))=f(f(z,g(z)),g(y)). 27997,96 [para_into,71.1.1,9.1.1,flip.1] f(f(x,g(x)),g(f(f(f(f(y,g(y)),g(f(z,u))),f(v,g(v))),f(z,f(w,g(w))))))=u. 280103 [back_demod,62,demod,97] f(x,f(y,g(y)))=f(x,f(z,g(z))). 281109 [para_from,103.1.1,33.1.1.1.2.1.1.2.1,demod,34] f(x,g(x))=f(y,g(y)). 282117,116 [para_from,109.1.1,33.1.1.1.2.1.1] f(f(f(x,g(x)),g(f(f(y,g(y)),z))),f(u,g(u)))=g(z). 283121,120 [para_from,109.1.1,33.1.1.1.2.1.1.2.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(f(z,g(z)))),u))),f(v,g(v)))=g(u). 284124 [para_from,109.1.1,5.1.1.2.1.2.1] f(x,g(f(g(y),f(f(z,g(z)),x))))=y. 285131,130 [para_into,124.1.1.2.1.2,109.1.1] f(g(f(x,g(x))),g(f(g(y),f(z,g(z)))))=y. 286157 [para_into,93.1.1,109.1.1] f(x,g(x))=f(f(y,g(y)),g(f(z,g(z)))). 287159 [copy,157,flip.1] f(f(x,g(x)),g(f(y,g(y))))=f(z,g(z)). 288190 [para_from,157.1.1,9.1.1.2.1.1.1.2.1,demod,117] f(x,g(f(g(g(f(y,g(y)))),f(z,x))))=g(z). 289203 [para_from,159.1.1,33.1.1.1.2.1.1.2.1,demod,121] g(f(x,g(x)))=g(f(y,g(y))). 290208 [para_into,130.1.1.1.1.2,203.1.1] f(g(f(f(x,g(x)),g(f(y,g(y))))),g(f(g(z),f(u,g(u)))))=z. 291213 [para_from,130.1.1,33.1.1.1.2.1.1.2.1] f(f(f(x,g(x)),g(f(f(f(y,g(y)),g(z)),g(f(u,g(u)))))),f(v,g(v)))=g(f(g(z),f(w,g(w)))). 292217 [copy,213,flip.1] g(f(g(x),f(y,g(y))))=f(f(f(z,g(z)),g(f(f(f(u,g(u)),g(x)),g(f(v,g(v)))))),f(w,g(w))). 293229 [para_into,190.1.1.2.1.2,109.1.1] f(g(x),g(f(g(g(f(y,g(y)))),f(z,g(z)))))=g(x). 294242,241 [para_into,190.1.1,5.1.1,flip.1] g(f(f(x,g(x)),g(f(y,g(g(f(z,g(z))))))))=y. 295441 [para_into,229.1.1.1,241.1.1,demod,242] f(x,g(f(g(g(f(y,g(y)))),f(z,g(z)))))=x. 296478 [para_into,441.1.1,109.1.1] f(x,g(x))=f(g(g(f(y,g(y)))),f(z,g(z))). 297480 [copy,478,flip.1] f(g(g(f(x,g(x)))),f(y,g(y)))=f(z,g(z)). 298496 [para_from,441.1.1,16.1.1.2.1.2] f(g(f(g(g(f(x,g(x)))),f(y,g(y)))),g(f(f(z,f(u,g(u))),v)))=f(f(f(w,g(w)),g(f(z,v))),f(v6,g(v6))). 299505 [para_from,441.1.1,33.1.1.1.2.1.1,demod,117] g(g(g(f(x,g(x)))))=f(y,g(y)). 300529 [para_from,441.1.1,5.1.1.2.1.2.1.1] f(x,g(f(y,f(f(f(g(g(f(z,g(z)))),f(u,g(u))),g(f(v,y))),x))))=v. 301536 [copy,496,flip.1] f(f(f(x,g(x)),g(f(y,z))),f(u,g(u)))=f(g(f(g(g(f(v,g(v)))),f(w,g(w)))),g(f(f(y,f(v6,g(v6))),z))). 302537 [copy,505,flip.1] f(x,g(x))=g(g(g(f(y,g(y))))). 303562 [para_into,537.1.1,537.1.1] g(g(g(f(x,g(x)))))=g(g(g(f(y,g(y))))). 304577 [para_from,537.1.1,505.1.1.1.1.1] g(g(g(g(g(g(f(x,g(x))))))))=f(y,g(y)). 305585 [para_from,537.1.1,16.1.1.2.1.2] f(g(x),g(f(f(y,f(z,g(z))),g(g(g(f(u,g(u))))))))=f(f(f(v,g(v)),g(f(y,x))),f(w,g(w))). 306622 [para_from,537.1.1,16.1.1.2.1.1.2] f(x,g(f(f(y,g(g(g(f(z,g(z)))))),f(u,x))))=f(f(f(v,g(v)),g(f(y,u))),f(w,g(w))). 307630 [copy,577,flip.1] f(x,g(x))=g(g(g(g(g(g(f(y,g(y)))))))). 308632 [copy,585,flip.1] f(f(f(x,g(x)),g(f(y,z))),f(u,g(u)))=f(g(z),g(f(f(y,f(v,g(v))),g(g(g(f(w,g(w)))))))). 309794 [para_from,562.1.1,241.1.1.1.1.2] g(f(f(g(g(f(x,g(x)))),g(g(g(f(y,g(y)))))),g(f(z,g(g(f(u,g(u))))))))=z. 310812 [para_from,562.1.1,130.1.1.2.1.1,demod,131] g(g(f(x,g(x))))=g(g(f(y,g(y)))). 311813 [para_from,562.1.1,103.1.1.2.2] f(x,f(g(g(f(y,g(y)))),g(g(g(f(z,g(z)))))))=f(x,f(u,g(u))). 312846 [copy,813,flip.1] f(x,f(y,g(y)))=f(x,f(g(g(f(z,g(z)))),g(g(g(f(u,g(u))))))). 313893 [para_from,812.1.1,441.1.1.2.1.1.1.1.2] f(x,g(f(g(g(f(g(f(y,g(y))),g(g(f(z,g(z))))))),f(u,g(u)))))=x. 314967 [para_from,577.1.1,130.1.1.1.1.2] f(g(f(g(g(g(g(g(f(x,g(x))))))),f(y,g(y)))),g(f(g(z),f(u,g(u)))))=z. 315982 [para_from,577.1.1,441.1.1.2.1.1.1.1.2] f(x,g(f(g(g(f(g(g(g(g(g(f(y,g(y))))))),f(z,g(z))))),f(u,g(u)))))=x. 3161048 [para_from,630.1.1,241.1.1.1.1] g(f(g(g(g(g(g(g(f(x,g(x)))))))),g(f(y,g(g(f(z,g(z))))))))=y. 3171059 [para_from,630.1.1,56.1.1.1.1] f(f(g(g(g(g(g(g(f(x,g(x)))))))),g(g(y))),f(z,g(z)))=y. 3181096 [para_from,630.1.1,241.1.1.1.2.1.2.1.1] g(f(f(x,g(x)),g(f(y,g(g(g(g(g(g(g(g(f(z,g(z))))))))))))))=y. 3191189,1188 [para_from,480.1.1,441.1.1.2.1] f(x,g(f(y,g(y))))=x. 3201197,1196 [back_demod,217,demod,1189,117] g(f(g(x),f(y,g(y))))=g(g(x)). 3211201,1200 [back_demod,208,demod,1189,1197] f(g(f(x,g(x))),g(g(y)))=y. 3221225,1224 [back_demod,982,demod,1197,1197] f(x,g(g(g(g(g(g(g(g(f(y,g(y)))))))))))=x. 3231227,1226 [back_demod,967,demod,1197,1197] f(g(g(g(g(g(g(f(x,g(x)))))))),g(g(y)))=y. 3241237,1236 [back_demod,893,demod,1201,1197] f(x,g(g(g(f(y,g(y))))))=x. 3251260 [back_demod,536,demod,1197] f(f(f(x,g(x)),g(f(y,z))),f(u,g(u)))=f(g(g(g(f(v,g(v))))),g(f(f(y,f(w,g(w))),z))). 3261293,1292 [back_demod,1096,demod,1225] g(f(f(x,g(x)),g(y)))=y. 3271295,1294 [back_demod,1059,demod,1227] f(x,f(y,g(y)))=x. 3281305,1304 [back_demod,846,demod,1295,1237,flip.1] f(x,g(g(f(y,g(y)))))=x. 3291331,1330 [back_demod,794,demod,1237,1305] g(f(g(g(f(x,g(x)))),g(y)))=y. 3301337,1336 [back_demod,632,demod,1295,1295,1237] f(f(x,g(x)),g(f(y,z)))=f(g(z),g(y)). 3311339,1338 [back_demod,622,demod,1237,1337,1295] f(x,g(f(y,f(z,x))))=f(g(z),g(y)). 3321345 [copy,1260,flip.1,demod,1295,1337,1295] f(g(g(g(f(x,g(x))))),g(f(y,z)))=f(g(z),g(y)). 3331393 [back_demod,529,demod,1295,1339,1331] f(f(x,y),g(y))=x. 3341443 [back_demod,60,demod,1337,1295,1337,1293,1295] g(f(f(g(x),g(y)),f(y,z)))=f(g(z),x). 3351463 [back_demod,1048,demod,1305] g(f(g(g(g(g(g(g(f(x,g(x)))))))),g(y)))=y. 3361499,1498 [para_into,1393.1.1.1,1393.1.1] f(x,g(g(y)))=f(x,y). 3371501,1500 [para_into,1393.1.1.1,630.1.1,demod,1499] f(g(g(g(g(g(g(f(x,g(x)))))))),y)=y. 3381527,1526 [back_demod,1200,demod,1499] f(g(f(x,g(x))),y)=y. 3391529,1528 [back_demod,1463,demod,1501] g(g(x))=x. 3401531,1530 [back_demod,1345,demod,1529,1527] g(f(x,y))=f(g(y),g(x)). 3411542 [back_demod,1443,demod,1531,1531,1531,1529,1529] f(f(g(x),g(y)),f(y,z))=f(g(x),z). 3421550 [para_from,1528.1.1,1393.1.1.2] f(f(x,g(y)),y)=x. 3431670 [para_into,1542.1.1.1.1,1528.1.1,demod,1529] f(f(x,g(y)),f(y,z))=f(x,z). 3441716 [para_into,1670.1.1.1,1550.1.1,demod,1529,flip.1] f(f(x,y),z)=f(x,f(y,z)). 3451718 [binary,1716.1,3.1] $Ans(assoc). 346 347------------ end of proof ------------- 348 349 350Search stopped by max_proofs option. 351 352 353Search stopped by max_proofs option. 354 355============ end of search ============ 356 357-------------- statistics ------------- 358clauses given 60 359clauses generated 2460 360clauses kept 1244 361clauses forward subsumed 3168 362clauses back subsumed 16 363Kbytes malloced 8789 364 365----------- times (seconds) ----------- 366user CPU time 0.20 (0 hr, 0 min, 0 sec) 367system CPU time 0.03 (0 hr, 0 min, 0 sec) 368wall-clock time 0 (0 hr, 0 min, 0 sec) 369 370That finishes the proof of the theorem. 371 372Process 8391 finished Mon Aug 2 15:30:37 2004 373