----- Otter 3.3, August 2003 ----- The process was started by mccune on lemma.mcs.anl.gov, Mon Sep 15 12:19:56 2003 The command was "otter". The process ID is 2370. 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(max_weight,23). assign(pick_given_ratio,4). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(sigint_interact). clear(detailed_history). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 0 [] f(f(x,x),f(x,y))=x. 0 [] f(x,f(x,f(x,y)))=f(x,y). 0 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(C,f(f(A,A),C)),C)))!=A|$Ans(OML_Sh). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] x=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=19): 2 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). ** KEPT (pick-wt=9): 3 [] f(f(x,x),f(x,y))=x. ---> New Demodulator: 4 [new_demod,3] f(f(x,x),f(x,y))=x. ** KEPT (pick-wt=11): 5 [] f(x,f(x,f(x,y)))=f(x,y). ---> New Demodulator: 6 [new_demod,5] f(x,f(x,f(x,y)))=f(x,y). ** KEPT (pick-wt=23): 7 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(C,f(f(A,A),C)),C)))!=A|$Ans(OML_Sh). Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). >>>> Starting back demodulation with 4. >>>> Starting back demodulation with 6. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=19) 2 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). given clause #2: (wt=9) 3 [] f(f(x,x),f(x,y))=x. given clause #3: (wt=11) 5 [] f(x,f(x,f(x,y)))=f(x,y). given clause #4: (wt=11) 8 [para_into,3,3] f(x,f(f(x,x),y))=f(x,x). given clause #5: (wt=11) 16 [para_into,5,3,demod,4] f(f(x,x),f(f(x,x),x))=x. given clause #6: (wt=23) 7 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(C,f(f(A,A),C)),C)))!=A|$Ans(OML_Sh). given clause #7: (wt=13) 12 [para_from,3,2,flip.1] f(x,f(f(y,x),f(y,x)))=f(y,x). given clause #8: (wt=9) 30 [para_into,12,3,demod,4,4] f(f(x,y),f(x,x))=x. given clause #9: (wt=9) 36 [para_from,12,3] f(f(x,x),f(y,x))=x. given clause #10: (wt=9) 40 [para_into,30,12] f(f(x,y),f(y,y))=y. given clause #11: (wt=15) 10 [para_into,3,2] f(f(x,x),f(y,f(f(x,z),f(x,z))))=x. given clause #12: (wt=11) 26 [para_into,12,8,demod,9,4,9] f(f(f(x,x),y),x)=f(x,x). given clause #13: (wt=11) 32 [para_from,12,8] f(x,f(y,f(x,x)))=f(x,x). given clause #14: (wt=11) 34 [para_from,12,5,demod,13] f(x,f(x,f(y,x)))=f(y,x). given clause #15: (wt=11) 46 [para_from,30,5,demod,31] f(f(x,y),f(f(x,y),x))=x. given clause #16: (wt=21) 14 [para_from,3,2,demod,4,flip.1] f(f(x,x),f(f(y,f(x,z)),f(y,f(x,z))))=f(y,f(x,x)). 99 back subsumes 96. 99 back subsumes 86. given clause #17: (wt=11) 60 [para_into,40,40] f(f(x,f(y,y)),y)=f(y,y). given clause #18: (wt=11) 64 [para_from,40,5,demod,41] f(f(x,y),f(f(x,y),y))=y. given clause #19: (wt=11) 99 [para_into,14,32,demod,33,4] f(f(x,x),y)=f(y,f(x,x)). 117 back subsumes 102. 117 back subsumes 99. given clause #20: (wt=7) 117 [para_into,99,99,demod,4,4] f(x,y)=f(y,x). given clause #21: (wt=19) 20 [para_into,8,2] f(x,f(y,f(f(f(x,x),z),f(f(x,x),z))))=f(x,x). given clause #22: (wt=11) 124 [para_into,117,64,flip.1] f(f(f(x,y),y),f(x,y))=y. given clause #23: (wt=11) 126 [para_into,117,46,flip.1] f(f(f(x,y),x),f(x,y))=x. given clause #24: (wt=11) 128 [para_into,117,34,flip.1] f(f(x,f(y,x)),x)=f(y,x). given clause #25: (wt=11) 130 [para_into,117,5,flip.1] f(f(x,f(x,y)),x)=f(x,y). given clause #26: (wt=21) 22 [para_from,8,2,demod,9,4,flip.1] f(x,f(f(y,f(f(x,x),z)),f(y,f(f(x,x),z))))=f(y,x). given clause #27: (wt=11) 135 [para_from,117,64] f(f(x,y),f(y,f(x,y)))=y. given clause #28: (wt=11) 137 [para_from,117,46] f(f(x,y),f(x,f(x,y)))=x. given clause #29: (wt=11) 139 [para_from,117,34] f(x,f(f(y,x),x))=f(y,x). given clause #30: (wt=11) 151 [para_from,117,5] f(x,f(f(x,y),x))=f(x,y). given clause #31: (wt=13) 38 [para_into,30,30] f(x,f(f(x,y),f(x,y)))=f(x,y). given clause #32: (wt=11) 153 [para_from,117,64] f(f(x,y),f(f(y,x),y))=y. given clause #33: (wt=11) 155 [para_from,117,64] f(f(x,y),f(f(y,x),x))=x. given clause #34: (wt=11) 177 [para_into,124,117] f(f(f(x,y),x),f(y,x))=x. given clause #35: (wt=11) 181 [para_into,124,117] f(f(x,f(y,x)),f(y,x))=x. given clause #36: (wt=15) 42 [para_into,30,2] f(f(x,f(f(y,z),f(y,z))),f(y,y))=y. given clause #37: (wt=11) 183 [para_into,124,117] f(f(f(x,y),y),f(y,x))=y. given clause #38: (wt=11) 185 [para_from,124,46] f(f(f(x,y),y),y)=f(x,y). given clause #39: (wt=11) 193 [para_into,126,117] f(f(x,f(x,y)),f(x,y))=x. given clause #40: (wt=11) 197 [para_from,126,46] f(f(f(x,y),x),x)=f(x,y). given clause #41: (wt=21) 44 [para_into,30,2] f(x,f(f(f(f(x,y),z),y),f(f(f(x,y),z),y)))=f(x,y). given clause #42: (wt=11) 227 [para_into,135,117] f(f(x,y),f(x,f(y,x)))=x. given clause #43: (wt=11) 231 [para_into,135,117] f(f(x,y),f(y,f(y,x)))=y. given clause #44: (wt=11) 247 [para_into,177,117] f(f(x,f(x,y)),f(y,x))=x. given clause #45: (wt=11) 257 [para_into,181,117] f(f(x,f(y,x)),f(x,y))=x. given clause #46: (wt=13) 48 [para_from,30,3] f(f(f(x,y),f(x,y)),x)=f(x,y). given clause #47: (wt=13) 52 [para_into,36,36] f(f(f(x,y),f(x,y)),y)=f(x,y). given clause #48: (wt=13) 145 [para_from,117,12] f(x,f(f(y,x),f(x,y)))=f(y,x). given clause #49: (wt=13) 147 [para_from,117,12] f(x,f(f(x,y),f(y,x)))=f(y,x). given clause #50: (wt=13) 337 [para_into,48,117] f(f(f(x,y),f(y,x)),y)=f(y,x). given clause #51: (wt=21) 50 [para_from,30,2,demod,31,flip.1] f(f(x,y),f(f(z,f(x,x)),f(z,f(x,x))))=f(z,f(x,x)). 371 back subsumes 360. 371 back subsumes 349. given clause #52: (wt=11) 371 [para_into,50,337,demod,342,342,366,342] f(x,f(y,z))=f(x,f(z,y)). 430 back subsumes 421. given clause #53: (wt=11) 420 [para_into,371,117] f(f(x,y),z)=f(z,f(y,x)). given clause #54: (wt=11) 430 [copy,420,flip.1] f(x,f(y,z))=f(f(z,y),x). 596 back subsumes 242. 596 back subsumes 241. given clause #55: (wt=11) 607 [para_into,430,117] f(f(x,y),z)=f(f(y,x),z). given clause #56: (wt=21) 54 [para_into,36,2,demod,4] f(f(x,y),f(x,f(f(z,y),f(z,y))))=f(f(x,y),f(x,y)). given clause #57: (wt=13) 339 [para_into,48,117] f(f(f(x,y),f(y,x)),x)=f(x,y). given clause #58: (wt=15) 72 [para_into,10,12,demod,13] f(f(x,x),f(y,f(f(z,x),f(z,x))))=x. given clause #59: (wt=15) 100 [para_into,14,26,demod,27,4,4,flip.1] f(f(f(f(x,y),f(x,y)),z),f(x,x))=x. 836 back subsumes 386. 837 back subsumes 387. 838 back subsumes 818. 843 back subsumes 406. 844 back subsumes 407. given clause #60: (wt=11) 836 [back_demod,796,demod,819] f(x,f(y,f(y,y)))=f(x,x). given clause #61: (wt=21) 56 [para_from,36,2,demod,37,flip.1] f(f(x,x),f(f(y,f(z,x)),f(y,f(z,x))))=f(y,f(x,x)). given clause #62: (wt=11) 837 [back_demod,780,demod,819] f(f(x,f(x,x)),y)=f(y,y). given clause #63: (wt=11) 838 [back_demod,384,demod,819] f(x,f(x,x))=f(y,f(y,y)). given clause #64: (wt=11) 843 [copy,836,flip.1] f(x,x)=f(x,f(y,f(y,y))). given clause #65: (wt=11) 844 [copy,837,flip.1] f(x,x)=f(f(y,f(y,y)),x). given clause #66: (wt=21) 58 [para_into,40,2,demod,4] f(f(x,f(f(y,z),f(y,z))),f(x,z))=f(f(x,z),f(x,z)). given clause #67: (wt=11) 964 [para_from,837,56,demod,41,37,flip.1] f(f(x,f(x,x)),f(y,y))=y. given clause #68: (wt=11) 974 [para_from,837,231,demod,971] f(f(x,x),f(y,f(y,y)))=x. given clause #69: (wt=13) 1056 [para_from,843,40] f(f(x,y),f(y,f(z,f(z,z))))=y. given clause #70: (wt=13) 1072 [para_from,843,54,demod,13,4] f(f(x,f(y,f(y,y))),f(z,x))=x. given clause #71: (wt=21) 62 [para_into,40,2] f(x,f(f(f(y,f(x,z)),z),f(f(y,f(x,z)),z)))=f(x,z). given clause #72: (wt=13) 1080 [para_from,843,30] f(f(x,y),f(x,f(z,f(z,z))))=x. given clause #73: (wt=13) 1090 [para_from,843,3] f(f(x,f(y,f(y,y))),f(x,z))=x. given clause #74: (wt=13) 1119 [para_from,844,40] f(f(x,y),f(f(z,f(z,z)),y))=y. given clause #75: (wt=13) 1134 [para_from,844,54,demod,13,4] f(f(f(x,f(x,x)),y),f(z,y))=y. given clause #76: (wt=21) 66 [para_from,40,2,demod,41,flip.1] f(f(x,y),f(f(z,f(y,y)),f(z,f(y,y))))=f(z,f(y,y)). given clause #77: (wt=13) 1142 [para_from,844,30] f(f(x,y),f(f(z,f(z,z)),x))=x. given clause #78: (wt=13) 1152 [para_from,844,3] f(f(f(x,f(x,x)),y),f(y,z))=y. given clause #79: (wt=15) 133 [back_demod,7,demod,129,9] f(f(f(f(B,A),f(A,C)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #80: (wt=15) 149 [para_from,117,10] f(f(x,x),f(f(f(x,y),f(x,y)),z))=x. given clause #81: (wt=17) 68 [para_into,10,40,demod,41] f(f(f(x,y),f(x,y)),f(z,f(y,y)))=f(x,y). given clause #82: (wt=15) 161 [para_from,117,10] f(f(x,x),f(y,f(f(x,z),f(z,x))))=x. given clause #83: (wt=15) 163 [para_from,117,10] f(f(x,x),f(y,f(f(z,x),f(x,z))))=x. given clause #84: (wt=15) 213 [para_into,22,124,demod,125,flip.1] f(f(f(f(x,x),y),y),x)=f(x,f(y,y)). given clause #85: (wt=15) 249 [para_from,177,22,demod,178,flip.1] f(f(f(x,f(y,y)),x),y)=f(y,f(x,x)). given clause #86: (wt=17) 70 [para_into,10,30,demod,31] f(f(f(x,y),f(x,y)),f(z,f(x,x)))=f(x,y). given clause #87: (wt=15) 259 [para_from,181,22,demod,182,flip.1] f(f(x,f(f(y,y),x)),y)=f(y,f(x,x)). given clause #88: (wt=15) 269 [para_into,42,139,demod,140] f(f(x,f(f(y,z),f(y,z))),f(z,z))=z. given clause #89: (wt=15) 271 [para_into,42,117] f(f(x,f(f(y,z),f(z,y))),f(z,z))=z. given clause #90: (wt=15) 277 [para_into,42,117] f(f(x,f(f(y,z),f(z,y))),f(y,y))=y. given clause #91: (wt=19) 76 [para_into,26,2] f(f(x,f(f(f(y,y),z),f(f(y,y),z))),y)=f(y,y). given clause #92: (wt=15) 323 [para_from,247,22,demod,248,flip.1] f(f(x,f(x,f(y,y))),y)=f(y,f(x,x)). given clause #93: (wt=15) 408 [para_into,371,371] f(x,f(y,f(z,u)))=f(x,f(f(u,z),y)). 1623 back subsumes 1487. given clause #94: (wt=15) 428 [copy,408,flip.1] f(x,f(f(y,z),u))=f(x,f(u,f(z,y))). given clause #95: (wt=15) 463 [para_from,371,231] f(f(f(x,y),z),f(z,f(z,f(y,x))))=z. given clause #96: (wt=21) 78 [para_from,26,10,demod,27,4] f(f(f(f(x,x),y),f(f(x,x),y)),f(z,x))=f(f(x,x),y). given clause #97: (wt=15) 465 [para_from,371,183] f(f(f(f(x,y),z),z),f(z,f(y,x)))=z. given clause #98: (wt=15) 471 [para_from,371,153] f(f(f(x,y),z),f(f(z,f(y,x)),z))=z. given clause #99: (wt=15) 498 [para_from,371,257] f(f(x,f(f(y,z),x)),f(x,f(z,y)))=x. given clause #100: (wt=15) 502 [para_from,371,227] f(f(x,f(y,z)),f(x,f(f(z,y),x)))=x. given clause #101: (wt=17) 80 [para_from,26,2,demod,27,4,flip.1] f(f(f(x,x),y),f(f(z,x),f(z,x)))=f(z,x). given clause #102: (wt=15) 504 [para_from,371,193] f(f(x,f(x,f(y,z))),f(x,f(z,y)))=x. given clause #103: (wt=15) 506 [para_from,371,155] f(f(x,f(y,z)),f(f(f(z,y),x),x))=x. given clause #104: (wt=15) 516 [para_from,371,137] f(f(x,f(y,z)),f(x,f(x,f(z,y))))=x. given clause #105: (wt=15) 522 [para_from,371,126] f(f(f(x,f(y,z)),x),f(x,f(z,y)))=x. given clause #106: (wt=21) 82 [para_from,32,2,demod,33,4,flip.1] f(x,f(f(y,f(z,f(x,x))),f(y,f(z,f(x,x)))))=f(y,x). given clause #107: (wt=15) 536 [para_from,371,177] f(f(f(x,f(y,z)),x),f(f(z,y),x))=x. given clause #108: (wt=15) 538 [para_from,371,46] f(f(x,f(y,z)),f(f(x,f(z,y)),x))=x. given clause #109: (wt=15) 550 [para_from,371,247] f(f(x,f(x,f(y,z))),f(f(z,y),x))=x. given clause #110: (wt=15) 569 [para_into,420,420] f(f(x,f(y,z)),u)=f(u,f(x,f(z,y))). 2262 back subsumes 2195. 2293 back subsumes 2186. given clause #111: (wt=23) 84 [para_into,34,10,demod,11] f(f(x,f(f(y,z),f(y,z))),f(f(x,f(f(y,z),f(y,z))),y))=y. given clause #112: (wt=15) 570 [para_into,420,371] f(f(x,f(y,z)),u)=f(u,f(f(z,y),x)). given clause #113: (wt=15) 572 [para_into,420,371] f(f(x,y),f(z,u))=f(f(u,z),f(y,x)). given clause #114: (wt=15) 575 [copy,569,flip.1] f(x,f(y,f(z,u)))=f(f(y,f(u,z)),x). 2599 back subsumes 1831. 2631 back subsumes 1826. 2655 back subsumes 1598. given clause #115: (wt=15) 576 [copy,570,flip.1] f(x,f(f(y,z),u))=f(f(u,f(z,y)),x). given clause #116: (wt=17) 88 [back_demod,74,demod,87] f(f(x,x),f(f(x,y),f(x,y)))=f(x,f(x,x)). given clause #117: (wt=15) 592 [para_from,420,371] f(x,f(y,f(z,u)))=f(x,f(y,f(u,z))). given clause #118: (wt=15) 593 [para_into,430,430] f(x,f(f(y,z),u))=f(f(f(z,y),u),x). given clause #119: (wt=15) 594 [para_into,430,371] f(x,f(y,f(z,u)))=f(f(f(u,z),y),x). given clause #120: (wt=15) 596 [para_into,430,420] f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). given clause #121: (wt=23) 90 [para_into,46,2] f(f(x,f(f(y,z),f(y,z))),f(f(y,f(f(x,z),f(x,z))),y))=y. given clause #122: (wt=15) 612 [copy,593,flip.1] f(f(f(x,y),z),u)=f(u,f(f(y,x),z)). given clause #123: (wt=15) 613 [copy,594,flip.1] f(f(f(x,y),z),u)=f(u,f(z,f(y,x))). given clause #124: (wt=15) 657 [para_from,430,231] f(f(f(x,y),z),f(z,f(f(y,x),z)))=z. given clause #125: (wt=15) 659 [para_from,430,183] f(f(f(f(x,y),z),z),f(f(y,x),z))=z. given clause #126: (wt=23) 92 [para_into,46,2] f(f(x,f(f(y,z),f(y,z))),f(f(y,f(f(x,z),f(x,z))),x))=x. given clause #127: (wt=15) 665 [para_from,430,153] f(f(f(x,y),z),f(f(f(y,x),z),z))=z. given clause #128: (wt=15) 692 [para_from,430,257] f(f(x,f(f(y,z),x)),f(f(z,y),x))=x. given clause #129: (wt=15) 740 [para_from,430,371] f(x,f(f(y,z),u))=f(x,f(f(z,y),u)). given clause #130: (wt=15) 746 [para_into,607,607] f(f(f(x,y),z),u)=f(f(z,f(y,x)),u). given clause #131: (wt=17) 97 [para_into,14,34,demod,35] f(f(x,x),f(f(y,x),f(y,x)))=f(x,f(x,x)). given clause #132: (wt=15) 747 [para_into,607,430] f(f(f(x,y),z),u)=f(f(f(y,x),z),u). given clause #133: (wt=15) 748 [para_into,607,420] f(f(x,f(y,z)),u)=f(f(x,f(z,y)),u). given clause #134: (wt=15) 749 [para_into,607,371] f(f(x,f(y,z)),u)=f(f(f(z,y),x),u). given clause #135: (wt=15) 776 [para_into,72,430] f(f(x,x),f(f(f(y,x),f(y,x)),z))=x. given clause #136: (wt=23) 103 [para_from,14,32] f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),f(x,f(y,z))). given clause #137: (wt=15) 778 [para_into,72,430] f(f(f(f(x,y),f(x,y)),z),f(y,y))=y. given clause #138: (wt=15) 810 [para_into,100,117] f(f(f(f(x,y),f(y,x)),z),f(y,y))=y. given clause #139: (wt=15) 816 [para_into,100,117] f(f(f(f(x,y),f(y,x)),z),f(x,x))=x. given clause #140: (wt=15) 865 [para_from,836,44,demod,53,862] f(x,f(f(x,y),f(z,f(z,z))))=f(x,y). given clause #141: (wt=23) 104 [para_from,14,40,demod,4] f(f(x,f(y,y)),f(x,f(y,z)))=f(f(x,f(y,z)),f(x,f(y,z))). given clause #142: (wt=15) 892 [para_from,836,607] f(f(x,x),y)=f(f(f(z,f(z,z)),x),y). given clause #143: (wt=15) 893 [para_from,836,420] f(f(x,x),y)=f(y,f(f(z,f(z,z)),x)). given clause #144: (wt=15) 922 [para_from,836,430] f(x,f(y,y))=f(f(f(z,f(z,z)),y),x). given clause #145: (wt=15) 923 [para_from,836,371] f(x,f(y,y))=f(x,f(f(z,f(z,z)),y)). given clause #146: (wt=19) 105 [para_from,14,10,demod,4,15] f(x,f(y,f(f(z,f(x,x)),f(z,f(x,x)))))=f(x,x). given clause #147: (wt=15) 925 [copy,892,flip.1] f(f(f(x,f(x,x)),y),z)=f(f(y,y),z). given clause #148: (wt=15) 926 [copy,893,flip.1] f(x,f(f(y,f(y,y)),z))=f(f(z,z),x). given clause #149: (wt=15) 927 [copy,922,flip.1] f(f(f(x,f(x,x)),y),z)=f(z,f(y,y)). given clause #150: (wt=15) 928 [copy,923,flip.1] f(x,f(f(y,f(y,y)),z))=f(x,f(z,z)). given clause #151: (wt=23) 107 [copy,103,flip.1] f(f(x,f(y,z)),f(x,f(y,z)))=f(f(x,f(y,z)),f(x,f(y,y))). 5043 back subsumes 3994. 5044 back subsumes 3997. 5052 back subsumes 4002. 5053 back subsumes 4003. given clause #152: (wt=15) 962 [para_from,837,231,demod,957] f(f(x,f(y,f(y,y))),x)=f(y,f(y,y)). given clause #153: (wt=15) 966 [para_from,837,257,demod,913] f(x,f(f(y,f(y,y)),x))=f(y,f(y,y)). given clause #154: (wt=15) 968 [para_from,837,227,demod,913] f(f(f(x,f(x,x)),y),y)=f(x,f(x,x)). given clause #155: (wt=15) 970 [para_from,837,181,demod,913] f(x,f(x,f(y,f(y,y))))=f(y,f(y,y)). given clause #156: (wt=23) 108 [copy,104,flip.1] f(f(x,f(y,z)),f(x,f(y,z)))=f(f(x,f(y,y)),f(x,f(y,z))). 5195 back subsumes 4101. 5196 back subsumes 4100. 5204 back subsumes 4103. 5205 back subsumes 4102. given clause #157: (wt=15) 972 [para_from,837,607] f(f(x,x),y)=f(f(x,f(z,f(z,z))),y). given clause #158: (wt=15) 973 [para_from,837,420] f(f(x,x),y)=f(y,f(x,f(z,f(z,z)))). given clause #159: (wt=15) 978 [para_from,837,430] f(x,f(y,y))=f(f(y,f(z,f(z,z))),x). given clause #160: (wt=15) 979 [para_from,837,371] f(x,f(y,y))=f(x,f(y,f(z,f(z,z)))). given clause #161: (wt=21) 109 [para_from,60,10,demod,61,4] f(f(f(x,f(y,y)),f(x,f(y,y))),f(z,y))=f(x,f(y,y)). given clause #162: (wt=15) 980 [copy,972,flip.1] f(f(x,f(y,f(y,y))),z)=f(f(x,x),z). given clause #163: (wt=15) 981 [copy,973,flip.1] f(x,f(y,f(z,f(z,z))))=f(f(y,y),x). given clause #164: (wt=15) 982 [copy,978,flip.1] f(f(x,f(y,f(y,y))),z)=f(z,f(x,x)). given clause #165: (wt=15) 983 [copy,979,flip.1] f(x,f(y,f(z,f(z,z))))=f(x,f(y,y)). given clause #166: (wt=17) 111 [para_from,60,2,demod,61,4,flip.1] f(f(x,f(y,y)),f(f(z,y),f(z,y)))=f(z,y). given clause #167: (wt=15) 1018 [para_from,838,607,demod,87] f(f(x,f(x,x)),y)=f(f(z,f(z,z)),y). 6156 back subsumes 951. given clause #168: (wt=15) 1019 [para_from,838,420,demod,87] f(f(x,f(x,x)),y)=f(y,f(z,f(z,z))). given clause #169: (wt=15) 1032 [para_from,838,430,demod,87] f(x,f(y,f(y,y)))=f(f(z,f(z,z)),x). 6364 back subsumes 6169. 6364 back subsumes 6156. given clause #170: (wt=15) 1033 [para_from,838,371,demod,87] f(x,f(y,f(y,y)))=f(x,f(z,f(z,z))). given clause #171: (wt=23) 113 [para_into,64,10,demod,11] f(x,f(x,f(y,f(f(x,z),f(x,z)))))=f(y,f(f(x,z),f(x,z))). given clause #172: (wt=15) 1052 [para_from,843,60] f(f(x,f(y,f(z,f(z,z)))),y)=f(y,y). given clause #173: (wt=15) 1060 [para_from,843,52] f(f(f(x,y),f(z,f(z,z))),y)=f(x,y). given clause #174: (wt=15) 1062 [para_from,843,48] f(f(f(x,y),f(z,f(z,z))),x)=f(x,y). given clause #175: (wt=15) 1070 [para_from,843,12] f(x,f(f(y,x),f(z,f(z,z))))=f(y,x). given clause #176: (wt=21) 120 [para_into,99,14,flip.1] f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y))=f(x,f(y,y)). given clause #177: (wt=15) 1078 [para_from,843,32] f(x,f(y,f(x,f(z,f(z,z)))))=f(x,x). given clause #178: (wt=15) 1088 [para_from,843,26] f(f(f(x,f(y,f(y,y))),z),x)=f(x,x). given clause #179: (wt=15) 1113 [para_from,844,44,demod,53,953] f(x,f(f(y,f(y,y)),f(x,z)))=f(x,z). given clause #180: (wt=15) 1115 [para_from,844,60] f(f(x,f(f(y,f(y,y)),z)),z)=f(z,z). given clause #181: (wt=19) 132 [para_into,117,2] f(x,f(f(y,z),f(y,z)))=f(f(f(x,z),f(x,z)),y). given clause #182: (wt=15) 1123 [para_from,844,52] f(f(f(x,f(x,x)),f(y,z)),z)=f(y,z). given clause #183: (wt=15) 1125 [para_from,844,48] f(f(f(x,f(x,x)),f(y,z)),y)=f(y,z). given clause #184: (wt=15) 1132 [para_from,844,12] f(x,f(f(y,f(y,y)),f(z,x)))=f(z,x). given clause #185: (wt=15) 1140 [para_from,844,32] f(x,f(y,f(f(z,f(z,z)),x)))=f(x,x). given clause #186: (wt=19) 134 [copy,132,flip.1] f(f(f(x,y),f(x,y)),z)=f(x,f(f(z,y),f(z,y))). given clause #187: (wt=15) 1150 [para_from,844,8] f(x,f(f(f(y,f(y,y)),x),z))=f(x,x). given clause #188: (wt=15) 1180 [para_into,964,844] f(f(x,f(x,x)),f(f(y,f(y,y)),z))=z. given clause #189: (wt=15) 1182 [para_into,964,843] f(f(x,f(x,x)),f(y,f(z,f(z,z))))=y. given clause #190: (wt=15) 1192 [para_into,974,844] f(f(f(x,f(x,x)),y),f(z,f(z,z)))=y. given clause #191: (wt=21) 141 [para_from,117,14] f(f(x,x),f(f(y,f(x,z)),f(f(x,z),y)))=f(y,f(x,x)). given clause #192: (wt=15) 1194 [para_into,974,843] f(f(x,f(y,f(y,y))),f(z,f(z,z)))=x. given clause #193: (wt=15) 1368 [para_into,133,117] f(f(f(f(A,B),f(A,C)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #194: (wt=15) 1369 [para_into,133,117] f(f(f(f(B,A),f(C,A)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #195: (wt=15) 1370 [para_into,133,430] f(f(f(f(C,A),f(B,A)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #196: (wt=21) 143 [para_from,117,14] f(f(x,x),f(f(f(x,y),z),f(z,f(x,y))))=f(z,f(x,x)). given clause #197: (wt=15) 1371 [para_into,133,420] f(f(f(f(A,C),f(A,B)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #198: (wt=15) 1372 [para_into,133,117] f(f(f(f(A,C),f(B,A)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #199: (wt=15) 1373 [para_into,133,420] f(f(D,f(f(A,C),f(B,A))),f(A,A))!=A|$Ans(OML_Sh). given clause #200: (wt=15) 1374 [para_into,133,117] f(f(D,f(f(B,A),f(A,C))),f(A,A))!=A|$Ans(OML_Sh). given clause #201: (wt=21) 157 [para_from,117,14] f(f(x,x),f(f(y,f(x,z)),f(y,f(z,x))))=f(y,f(x,x)). given clause #202: (wt=15) 1377 [para_into,133,430] f(f(A,A),f(f(f(B,A),f(A,C)),D))!=A|$Ans(OML_Sh). given clause #203: (wt=15) 1378 [para_into,133,420] f(f(A,A),f(D,f(f(B,A),f(A,C))))!=A|$Ans(OML_Sh). given clause #204: (wt=15) 1391 [para_into,149,117] f(f(x,x),f(f(f(y,x),f(x,y)),z))=x. given clause #205: (wt=15) 1399 [para_into,149,117] f(f(x,x),f(f(f(x,y),f(y,x)),z))=x. given clause #206: (wt=21) 159 [para_from,117,14] f(f(x,x),f(f(y,f(z,x)),f(y,f(x,z))))=f(y,f(x,x)). given clause #207: (wt=15) 1490 [para_into,213,420] f(x,f(y,f(f(x,x),y)))=f(x,f(y,y)). given clause #208: (wt=15) 1494 [para_into,213,117] f(x,f(f(f(x,x),y),y))=f(x,f(y,y)). given clause #209: (wt=15) 1512 [para_into,249,420] f(x,f(y,f(y,f(x,x))))=f(x,f(y,y)). given clause #210: (wt=15) 1516 [para_into,249,117] f(x,f(f(y,f(x,x)),y))=f(x,f(y,y)). given clause #211: (wt=19) 165 [para_from,117,2] f(x,f(f(y,z),f(z,y)))=f(y,f(f(x,z),f(x,z))). given clause #212: (wt=15) 2347 [para_from,569,133] f(f(D,f(f(B,A),f(C,A))),f(A,A))!=A|$Ans(OML_Sh). given clause #213: (wt=15) 2462 [para_from,570,133] f(f(D,f(f(C,A),f(B,A))),f(A,A))!=A|$Ans(OML_Sh). given clause #214: (wt=15) 2574 [para_from,572,133] f(f(f(f(C,A),f(A,B)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #215: (wt=15) 3288 [para_from,596,133] f(f(f(f(A,B),f(C,A)),D),f(A,A))!=A|$Ans(OML_Sh). given clause #216: (wt=19) 166 [para_from,117,2] f(x,f(f(y,z),f(z,y)))=f(z,f(f(x,y),f(x,y))). given clause #217: (wt=15) 3372 [para_from,612,133] f(f(A,A),f(f(f(A,C),f(B,A)),D))!=A|$Ans(OML_Sh). given clause #218: (wt=15) 3409 [para_from,612,133] f(f(D,f(f(A,B),f(A,C))),f(A,A))!=A|$Ans(OML_Sh). given clause #219: (wt=15) 3447 [para_from,613,133] f(f(A,A),f(D,f(f(A,C),f(B,A))))!=A|$Ans(OML_Sh). given clause #220: (wt=15) 3452 [para_from,613,133] f(f(D,f(f(A,C),f(A,B))),f(A,A))!=A|$Ans(OML_Sh). given clause #221: (wt=19) 167 [copy,165,flip.1] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(z,x))). given clause #222: (wt=15) 6910 [para_into,1368,570] f(f(D,f(f(C,A),f(A,B))),f(A,A))!=A|$Ans(OML_Sh). given clause #223: (wt=15) 6911 [para_into,1368,569] f(f(D,f(f(A,B),f(C,A))),f(A,A))!=A|$Ans(OML_Sh). given clause #224: (wt=15) 6916 [para_into,1368,613] f(f(A,A),f(D,f(f(A,C),f(A,B))))!=A|$Ans(OML_Sh). given clause #225: (wt=15) 6917 [para_into,1368,612] f(f(A,A),f(f(f(A,C),f(A,B)),D))!=A|$Ans(OML_Sh). given clause #226: (wt=19) 168 [copy,166,flip.1] f(x,f(f(y,z),f(y,z)))=f(y,f(f(z,x),f(x,z))). given clause #227: (wt=15) 6918 [para_into,1368,572] f(f(A,A),f(D,f(f(A,B),f(A,C))))!=A|$Ans(OML_Sh). given clause #228: (wt=15) 6919 [para_into,1368,430] f(f(A,A),f(f(f(A,B),f(A,C)),D))!=A|$Ans(OML_Sh). given clause #229: (wt=15) 6924 [para_into,1369,613] f(f(A,A),f(D,f(f(C,A),f(B,A))))!=A|$Ans(OML_Sh). given clause #230: (wt=15) 6925 [para_into,1369,612] f(f(A,A),f(f(f(C,A),f(B,A)),D))!=A|$Ans(OML_Sh). given clause #231: (wt=19) 169 [para_into,20,117] f(x,f(y,f(f(z,f(x,x)),f(f(x,x),z))))=f(x,x). given clause #232: (wt=15) 6926 [para_into,1369,572] f(f(A,A),f(D,f(f(B,A),f(C,A))))!=A|$Ans(OML_Sh). given clause #233: (wt=15) 6927 [para_into,1369,430] f(f(A,A),f(f(f(B,A),f(C,A)),D))!=A|$Ans(OML_Sh). given clause #234: (wt=15) 6968 [para_into,1377,596] f(f(A,A),f(f(f(A,B),f(C,A)),D))!=A|$Ans(OML_Sh). given clause #235: (wt=15) 6969 [para_into,1377,572] f(f(A,A),f(f(f(C,A),f(A,B)),D))!=A|$Ans(OML_Sh). given clause #236: (wt=19) 171 [para_into,20,117] f(x,f(y,f(f(f(x,x),z),f(z,f(x,x)))))=f(x,x). given clause #237: (wt=15) 6970 [para_into,1378,596] f(f(A,A),f(D,f(f(A,B),f(C,A))))!=A|$Ans(OML_Sh). given clause #238: (wt=15) 6971 [para_into,1378,572] f(f(A,A),f(D,f(f(C,A),f(A,B))))!=A|$Ans(OML_Sh). given clause #239: (wt=17) 187 [para_from,124,14,demod,125,flip.1] f(f(f(x,y),y),f(x,x))=f(f(x,x),f(y,y)). given clause #240: (wt=17) 251 [para_from,177,14,demod,178,flip.1] f(f(f(x,y),x),f(y,y))=f(f(y,y),f(x,x)). given clause #241: (wt=19) 173 [para_into,20,117] f(x,f(f(f(f(x,x),y),f(f(x,x),y)),z))=f(x,x). given clause #242: (wt=17) 267 [para_into,42,155,demod,156] f(f(x,f(y,y)),f(f(y,z),f(y,z)))=f(y,z). given clause #243: (wt=17) 457 [para_from,371,40] f(f(x,f(y,z)),f(f(y,z),f(z,y)))=f(y,z). given clause #244: (wt=17) 483 [para_from,371,36] f(f(f(x,y),f(x,y)),f(z,f(y,x)))=f(x,y). given clause #245: (wt=17) 540 [para_from,371,40] f(f(x,f(y,z)),f(f(z,y),f(z,y)))=f(z,y). given clause #246: (wt=19) 175 [para_from,20,5,flip.1] f(x,f(f(f(x,x),y),f(f(x,x),y)))=f(x,f(x,x)). given clause #247: (wt=17) 552 [para_from,371,36] f(f(f(x,y),f(y,x)),f(z,f(x,y)))=f(x,y). given clause #248: (wt=17) 556 [para_from,371,30] f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(x,y). given clause #249: (wt=17) 562 [para_from,371,3] f(f(f(x,y),f(y,x)),f(f(x,y),z))=f(x,y). given clause #250: (wt=17) 641 [para_from,430,40] f(f(x,f(y,z)),f(f(z,y),f(y,z)))=f(y,z). given clause #251: (wt=23) 179 [para_into,124,10,demod,11] f(f(x,f(y,f(f(x,z),f(x,z)))),x)=f(y,f(f(x,z),f(x,z))). given clause #252: (wt=17) 677 [para_from,430,36] f(f(f(x,y),f(x,y)),f(f(y,x),z))=f(x,y). given clause #253: (wt=17) 718 [para_from,430,40] f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x). given clause #254: (wt=17) 724 [para_from,430,36] f(f(f(x,y),f(y,x)),f(z,f(y,x)))=f(y,x). given clause #255: (wt=17) 728 [para_from,430,30] f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(x,y). given clause #256: (wt=23) 189 [para_from,124,2,demod,125,flip.1] f(f(f(x,y),y),f(f(z,f(x,y)),f(z,f(x,y))))=f(z,f(y,y)). given clause #257: (wt=17) 734 [para_from,430,3] f(f(f(x,y),f(y,x)),f(f(y,x),z))=f(y,x). given clause #258: (wt=17) 808 [para_into,100,227,demod,228] f(f(f(x,x),y),f(f(x,z),f(x,z)))=f(x,z). given clause #259: (wt=17) 839 [back_demod,115,demod,819] f(f(f(x,y),f(x,y)),f(y,y))=f(x,f(x,x)). given clause #260: (wt=17) 841 [back_demod,94,demod,819] f(f(f(x,y),f(x,y)),f(x,x))=f(x,f(x,x)). given clause #261: (wt=23) 191 [para_into,126,2] f(f(f(x,f(f(y,z),f(y,z))),y),f(y,f(f(x,z),f(x,z))))=y. given clause #262: (wt=17) 845 [para_into,836,607] f(x,f(f(y,z),f(f(z,y),f(y,z))))=f(x,x). given clause #263: (wt=17) 846 [para_into,836,420] f(x,f(f(y,z),f(f(y,z),f(z,y))))=f(x,x). given clause #264: (wt=17) 848 [para_into,836,420] f(x,f(f(f(y,z),f(y,z)),f(z,y)))=f(x,x). given clause #265: (wt=17) 850 [para_into,836,607] f(f(x,y),f(z,f(z,z)))=f(f(y,x),f(y,x)). given clause #266: (wt=23) 195 [para_into,126,2] f(f(f(x,f(f(y,z),f(y,z))),x),f(y,f(f(x,z),f(x,z))))=x. given clause #267: (wt=17) 851 [para_into,836,420] f(f(x,f(x,x)),f(y,z))=f(f(z,y),f(z,y)). given clause #268: (wt=17) 852 [copy,845,flip.1] f(x,x)=f(x,f(f(y,z),f(f(z,y),f(y,z)))). given clause #269: (wt=17) 853 [copy,846,flip.1] f(x,x)=f(x,f(f(y,z),f(f(y,z),f(z,y)))). given clause #270: (wt=17) 855 [copy,848,flip.1] f(x,x)=f(x,f(f(f(y,z),f(y,z)),f(z,y))). given clause #271: (wt=23) 199 [para_from,126,2,demod,127,flip.1] f(f(f(x,y),x),f(f(z,f(x,y)),f(z,f(x,y))))=f(z,f(x,x)). given clause #272: (wt=15) 8007 [para_into,199,103,demod,4,31] f(f(f(x,f(y,y)),x),f(x,f(y,z)))=x. given clause #273: (wt=15) 8033 [para_into,8007,979,demod,4] f(f(f(x,y),x),f(x,f(f(y,y),z)))=x. given clause #274: (wt=15) 8069 [para_into,8007,430] f(f(f(f(x,x),y),y),f(y,f(x,z)))=y. given clause #275: (wt=15) 8077 [para_into,8007,104,demod,4,31,31,31] f(f(f(x,y),x),f(x,f(f(x,y),z)))=x. given clause #276: (wt=23) 201 [para_into,128,10,demod,11] f(f(f(x,f(f(y,z),f(y,z))),y),f(x,f(f(y,z),f(y,z))))=y. given clause #277: (wt=15) 8087 [para_into,8007,12] f(f(f(x,y),y),f(y,f(f(x,y),z)))=y. given clause #278: (wt=15) 8107 [para_into,8007,570] f(f(x,f(f(y,y),x)),f(x,f(y,z)))=x. given clause #279: (wt=15) 8109 [para_into,8007,569] f(f(x,f(x,f(y,y))),f(x,f(y,z)))=x. given clause #280: (wt=15) 8123 [para_into,8007,1132] f(f(f(x,f(y,y)),x),f(x,f(z,y)))=x. given clause #281: (wt=19) 203 [para_from,128,14,demod,129,15,flip.1] f(f(f(x,y),f(z,f(x,y))),f(x,x))=f(z,f(x,x)). 9128 back subsumes 5269. 9129 back subsumes 4116. given clause #282: (wt=15) 8125 [para_into,8007,982,demod,1081] f(f(f(x,y),x),f(x,f(z,f(y,y))))=x. given clause #283: (wt=15) 8179 [para_into,8007,430] f(f(f(x,f(y,y)),x),f(f(z,y),x))=x. given clause #284: (wt=15) 8191 [para_into,8007,117] f(f(f(x,f(y,y)),x),f(f(y,z),x))=x. given clause #285: (wt=15) 8193 [para_into,8007,613] f(f(x,f(y,z)),f(x,f(f(y,y),x)))=x. given clause #286: (wt=23) 207 [para_from,130,2,demod,131] f(x,f(f(y,z),f(y,z)))=f(f(y,f(y,z)),f(f(x,y),f(x,y))). given clause #287: (wt=15) 8195 [para_into,8007,612] f(f(x,f(y,z)),f(f(f(y,y),x),x))=x. given clause #288: (wt=15) 8197 [para_into,8007,596] f(f(x,f(x,f(y,y))),f(f(y,z),x))=x. given clause #289: (wt=15) 8199 [para_into,8007,594] f(f(f(x,y),z),f(f(z,f(y,y)),z))=z. given clause #290: (wt=15) 8205 [para_into,8007,575] f(f(x,f(y,z)),f(f(x,f(z,z)),x))=x. given clause #291: (wt=23) 208 [copy,207,flip.1] f(f(x,f(x,y)),f(f(z,x),f(z,x)))=f(z,f(f(x,y),f(x,y))). given clause #292: (wt=15) 8207 [para_into,8007,572] f(f(f(x,y),z),f(z,f(z,f(x,x))))=z. given clause #293: (wt=15) 8213 [para_into,8007,430] f(f(f(x,y),z),f(f(z,f(x,x)),z))=z. given clause #294: (wt=15) 8215 [para_into,8007,420] f(f(x,f(y,z)),f(x,f(x,f(y,y))))=x. given clause #295: (wt=15) 8217 [para_into,8007,117] f(f(x,f(y,z)),f(f(x,f(y,y)),x))=x. given clause #296: (wt=21) 209 [para_into,22,117] f(x,f(f(y,f(z,f(x,x))),f(y,f(f(x,x),z))))=f(y,x). given clause #297: (wt=15) 8235 [para_into,8033,145,demod,642] f(f(f(x,y),y),f(y,f(f(y,x),z)))=y. given clause #298: (wt=15) 8243 [para_into,8033,117] f(f(f(x,y),y),f(y,f(f(x,x),z)))=y. given clause #299: (wt=15) 8267 [para_into,8033,420] f(f(x,f(y,x)),f(x,f(f(y,y),z)))=x. given clause #300: (wt=15) 8271 [para_into,8033,195,demod,39,39] f(x,f(f(x,y),f(f(x,x),z)))=f(x,y). given clause #301: (wt=19) 211 [para_into,22,128,demod,129,23,flip.1] f(f(f(f(x,x),y),f(z,f(f(x,x),y))),x)=f(z,x). given clause #302: (wt=15) 8275 [para_into,8033,124] f(x,f(f(y,x),f(f(x,x),z)))=f(y,x). given clause #303: (wt=15) 8277 [para_into,8033,117] f(f(x,f(x,y)),f(x,f(f(y,y),z)))=x. given clause #304: (wt=15) 8305 [para_into,8033,593] f(f(f(x,y),x),f(f(f(y,y),z),x))=x. given clause #305: (wt=15) 8307 [para_into,8033,576] f(f(f(x,y),x),f(f(z,f(y,y)),x))=x. given clause #306: (wt=21) 215 [para_into,22,117] f(x,f(f(f(f(x,x),y),z),f(z,f(f(x,x),y))))=f(z,x). given clause #307: (wt=15) 8317 [para_into,8033,613] f(f(x,f(f(y,y),z)),f(x,f(y,x)))=x. given clause #308: (wt=15) 8319 [para_into,8033,612] f(f(x,f(f(y,y),z)),f(f(y,x),x))=x. given clause #309: (wt=15) 8321 [para_into,8033,596] f(f(x,f(x,y)),f(f(f(y,y),z),x))=x. given clause #310: (wt=15) 8323 [para_into,8033,594] f(f(f(x,f(y,y)),z),f(f(z,y),z))=z. given clause #311: (wt=19) 217 [para_into,22,34,demod,35,87] f(x,f(f(y,f(x,x)),f(y,f(x,x))))=f(x,f(x,x)). given clause #312: (wt=15) 8329 [para_into,8033,575] f(f(x,f(y,f(z,z))),f(f(x,z),x))=x. given clause #313: (wt=15) 8331 [para_into,8033,572] f(f(f(f(x,x),y),z),f(z,f(z,x)))=z. given clause #314: (wt=15) 8337 [para_into,8033,430] f(f(f(f(x,x),y),z),f(f(z,x),z))=z. given clause #315: (wt=15) 8339 [para_into,8033,420] f(f(x,f(f(y,y),z)),f(x,f(x,y)))=x. given clause #316: (wt=19) 219 [para_into,22,26,demod,27,4,9,flip.1] f(f(f(f(f(x,x),y),f(f(x,x),y)),z),x)=f(x,x). given clause #317: (wt=15) 8341 [para_into,8033,117] f(f(x,f(f(y,y),z)),f(f(x,y),x))=x. given clause #318: (wt=15) 8357 [para_into,8069,1132] f(f(f(f(x,x),y),y),f(y,f(z,x)))=y. given clause #319: (wt=15) 8361 [para_into,8069,982,demod,1081] f(f(f(x,y),y),f(y,f(z,f(x,x))))=y. given clause #320: (wt=15) 8413 [para_into,8069,430] f(f(f(f(x,x),y),y),f(f(z,x),y))=y. given clause #321: (wt=21) 221 [para_into,22,117] f(x,f(f(y,f(f(x,x),z)),f(y,f(z,f(x,x)))))=f(y,x). given clause #322: (wt=15) 8423 [para_into,8069,117] f(f(f(f(x,x),y),y),f(f(x,z),y))=y. given clause #323: (wt=15) 8425 [para_into,8069,596] f(f(x,f(f(y,y),x)),f(f(y,z),x))=x. given clause #324: (wt=15) 8427 [para_into,8069,594] f(f(f(x,y),z),f(f(f(y,y),z),z))=z. given clause #325: (wt=15) 8433 [para_into,8069,575] f(f(x,f(y,z)),f(f(f(z,z),x),x))=x. given clause #326: (wt=21) 223 [para_into,22,117] f(x,f(f(y,f(f(x,x),z)),f(f(f(x,x),z),y)))=f(y,x). given clause #327: (wt=15) 8435 [para_into,8069,572] f(f(f(x,y),z),f(z,f(f(x,x),z)))=z. given clause #328: (wt=15) 8441 [para_into,8069,430] f(f(f(x,y),z),f(f(f(x,x),z),z))=z. given clause #329: (wt=15) 8505 [para_into,8077,420] f(f(x,f(y,x)),f(x,f(f(x,y),z)))=x. given clause #330: (wt=15) 8509 [para_into,8077,130] f(f(x,y),f(x,f(f(x,f(x,y)),z)))=x. given clause #331: (wt=21) 225 [para_into,22,117] f(f(f(x,f(f(y,y),z)),f(x,f(f(y,y),z))),y)=f(x,y). given clause #332: (wt=15) 8511 [para_into,8077,128] f(f(x,y),f(y,f(f(y,f(x,y)),z)))=y. given clause #333: (wt=15) 8515 [para_into,8077,117] f(f(x,f(x,y)),f(x,f(f(x,y),z)))=x. given clause #334: (wt=15) 8539 [para_into,8077,117] f(f(f(x,y),x),f(x,f(f(y,x),z)))=x. given clause #335: (wt=15) 8541 [para_into,8077,1132] f(f(f(x,y),x),f(x,f(z,f(x,y))))=x. given clause #336: (wt=23) 229 [para_into,135,10,demod,11] f(x,f(f(y,f(f(x,z),f(x,z))),x))=f(y,f(f(x,z),f(x,z))). given clause #337: (wt=15) 8551 [para_into,8077,420] f(f(f(x,y),x),f(x,f(z,f(y,x))))=x. given clause #338: (wt=15) 8559 [para_into,8077,199,demod,127] f(x,f(f(x,y),f(z,f(x,x))))=f(x,y). given clause #339: (wt=15) 8561 [para_into,8077,189,demod,125] f(x,f(f(y,x),f(z,f(x,x))))=f(y,x). given clause #340: (wt=15) 8575 [para_into,8077,593] f(f(f(x,y),x),f(f(f(y,x),z),x))=x. given clause #341: (wt=23) 233 [para_into,137,2] f(f(x,f(f(y,z),f(y,z))),f(y,f(y,f(f(x,z),f(x,z)))))=y. given clause #342: (wt=15) 8577 [para_into,8077,576] f(f(f(x,y),x),f(f(z,f(y,x)),x))=x. given clause #343: (wt=15) 8581 [para_into,8077,430] f(f(f(x,y),x),f(f(z,f(x,y)),x))=x. given clause #344: (wt=15) 8583 [para_into,8077,117] f(f(f(x,y),x),f(f(f(x,y),z),x))=x. given clause #345: (wt=15) 8587 [para_into,8077,613] f(f(x,f(f(x,y),z)),f(x,f(y,x)))=x. given clause #346: (wt=23) 237 [para_into,139,10,demod,11] f(f(x,f(f(y,z),f(y,z))),f(y,f(x,f(f(y,z),f(y,z)))))=y. given clause #347: (wt=15) 8589 [para_into,8077,612] f(f(x,f(f(x,y),z)),f(f(y,x),x))=x. given clause #348: (wt=15) 8591 [para_into,8077,596] f(f(x,f(x,y)),f(f(f(x,y),z),x))=x. given clause #349: (wt=15) 8593 [para_into,8077,594] f(f(f(x,f(y,z)),y),f(f(y,z),y))=y. given clause #350: (wt=15) 8595 [para_into,8077,575] f(f(x,f(y,f(x,z))),f(f(x,z),x))=x. given clause #351: (wt=23) 243 [para_into,155,2] f(f(x,f(f(y,z),f(y,z))),f(f(f(f(x,z),f(x,z)),y),y))=y. given clause #352: (wt=15) 8597 [para_into,8077,572] f(f(f(f(x,y),z),x),f(x,f(x,y)))=x. given clause #353: (wt=15) 8599 [para_into,8077,430] f(f(f(f(x,y),z),x),f(f(x,y),x))=x. given clause #354: (wt=15) 8601 [para_into,8077,420] f(f(x,f(f(x,y),z)),f(x,f(x,y)))=x. given clause #355: (wt=15) 8603 [para_into,8077,117] f(f(x,f(f(x,y),z)),f(f(x,y),x))=x. given clause #356: (wt=23) 253 [para_from,177,2,demod,178,flip.1] f(f(f(x,y),x),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(x,x)). given clause #357: (wt=15) 8649 [para_into,8087,420] f(f(x,f(x,y)),f(x,f(f(y,x),z)))=x. given clause #358: (wt=15) 8651 [para_into,8087,197] f(f(x,y),f(x,f(f(f(x,y),x),z)))=x. given clause #359: (wt=15) 8655 [para_into,8087,185] f(f(x,y),f(y,f(f(f(x,y),y),z)))=y. given clause #360: (wt=15) 8659 [para_into,8087,117] f(f(x,f(y,x)),f(x,f(f(y,x),z)))=x. given clause #361: (wt=23) 255 [para_into,181,10,demod,11] f(f(f(x,f(f(y,z),f(y,z))),y),y)=f(x,f(f(y,z),f(y,z))). given clause #362: (wt=15) 8661 [para_into,8087,1132] f(f(f(x,y),y),f(y,f(z,f(x,y))))=y. given clause #363: (wt=15) 8673 [para_into,8087,420] f(f(f(x,y),y),f(y,f(z,f(y,x))))=y. given clause #364: (wt=15) 8687 [para_into,8087,593] f(f(f(x,y),y),f(f(f(y,x),z),y))=y. given clause #365: (wt=15) 8689 [para_into,8087,576] f(f(f(x,y),y),f(f(z,f(y,x)),y))=y. given clause #366: (wt=23) 262 [para_from,181,2,demod,182,flip.1] f(f(x,f(y,x)),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(x,x)). given clause #367: (wt=15) 8693 [para_into,8087,430] f(f(f(x,y),y),f(f(z,f(x,y)),y))=y. given clause #368: (wt=15) 8695 [para_into,8087,117] f(f(f(x,y),y),f(f(f(x,y),z),y))=y. given clause #369: (wt=15) 8699 [para_into,8087,613] f(f(x,f(f(y,x),z)),f(x,f(x,y)))=x. given clause #370: (wt=15) 8701 [para_into,8087,612] f(f(x,f(f(y,x),z)),f(f(x,y),x))=x. given clause #371: (wt=21) 273 [para_into,42,26,demod,27,4] f(f(x,y),f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),z). given clause #372: (wt=15) 8703 [para_into,8087,596] f(f(x,f(y,x)),f(f(f(y,x),z),x))=x. given clause #373: (wt=15) 8705 [para_into,8087,594] f(f(f(x,f(y,z)),z),f(f(y,z),z))=z. given clause #374: (wt=15) 8707 [para_into,8087,575] f(f(x,f(y,f(z,x))),f(f(z,x),x))=x. given clause #375: (wt=15) 8709 [para_into,8087,572] f(f(f(f(x,y),z),y),f(y,f(x,y)))=y. given clause #376: (wt=19) 275 [para_into,42,14,demod,15,4] f(f(x,f(f(y,f(z,z)),f(y,f(z,z)))),z)=f(z,z). given clause #377: (wt=15) 8711 [para_into,8087,430] f(f(f(f(x,y),z),y),f(f(x,y),y))=y. given clause #378: (wt=15) 8713 [para_into,8087,420] f(f(x,f(f(y,x),z)),f(x,f(y,x)))=x. given clause #379: (wt=15) 8715 [para_into,8087,117] f(f(x,f(f(y,x),z)),f(f(y,x),x))=x. given clause #380: (wt=15) 8757 [para_into,8107,1132] f(f(x,f(f(y,y),x)),f(x,f(z,y)))=x. given clause #381: (wt=23) 283 [para_into,183,2] f(f(f(f(f(x,y),f(x,y)),z),z),f(x,f(f(z,y),f(z,y))))=z. given clause #382: (wt=15) 8761 [para_into,8107,982,demod,1081] f(f(x,f(y,x)),f(x,f(z,f(y,y))))=x. given clause #383: (wt=15) 8813 [para_into,8107,430] f(f(x,f(f(y,y),x)),f(f(z,y),x))=x. given clause #384: (wt=15) 8827 [para_into,8107,594] f(f(f(x,y),z),f(z,f(f(y,y),z)))=z. given clause #385: (wt=15) 8833 [para_into,8107,575] f(f(x,f(y,z)),f(x,f(f(z,z),x)))=x. given clause #386: (wt=23) 285 [para_from,183,2,demod,184,flip.1] f(f(f(x,y),y),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(y,y)). given clause #387: (wt=15) 8865 [para_into,8109,1132] f(f(x,f(x,f(y,y))),f(x,f(z,y)))=x. given clause #388: (wt=15) 8869 [para_into,8109,982,demod,1081] f(f(x,f(x,y)),f(x,f(z,f(y,y))))=x. given clause #389: (wt=15) 8919 [para_into,8109,430] f(f(x,f(x,f(y,y))),f(f(z,y),x))=x. given clause #390: (wt=15) 8929 [para_into,8109,594] f(f(f(x,y),z),f(z,f(z,f(y,y))))=z. given clause #391: (wt=23) 287 [para_into,185,10,demod,11] f(f(x,f(y,f(f(x,z),f(x,z)))),f(y,f(f(x,z),f(x,z))))=x. given clause #392: (wt=15) 8935 [para_into,8109,575] f(f(x,f(y,z)),f(x,f(x,f(z,z))))=x. given clause #393: (wt=15) 9187 [para_into,8125,613] f(f(x,f(y,f(z,z))),f(x,f(z,x)))=x. given clause #394: (wt=15) 9189 [para_into,8125,612] f(f(x,f(y,f(z,z))),f(f(z,x),x))=x. given clause #395: (wt=15) 9191 [para_into,8125,596] f(f(x,f(x,y)),f(f(z,f(y,y)),x))=x. given clause #396: (wt=19) 289 [para_from,185,22,demod,186,23,flip.1] f(f(f(x,f(f(y,y),z)),f(f(y,y),z)),y)=f(x,y). given clause #397: (wt=15) 9197 [para_into,8125,572] f(f(f(x,f(y,y)),z),f(z,f(z,y)))=z. given clause #398: (wt=15) 9203 [para_into,8125,420] f(f(x,f(y,f(z,z))),f(x,f(x,z)))=x. given clause #399: (wt=15) 10378 [para_into,8235,596] f(f(x,f(y,x)),f(f(f(x,y),z),x))=x. given clause #400: (wt=15) 10380 [para_into,8235,594] f(f(f(x,f(y,z)),y),f(f(z,y),y))=y. given clause #401: (wt=19) 291 [para_from,185,14,demod,186,15,flip.1] f(f(f(x,f(y,z)),f(y,z)),f(y,y))=f(x,f(y,y)). given clause #402: (wt=15) 10382 [para_into,8235,575] f(f(x,f(y,f(x,z))),f(f(z,x),x))=x. given clause #403: (wt=15) 10384 [para_into,8235,572] f(f(f(f(x,y),z),x),f(x,f(y,x)))=x. given clause #404: (wt=15) 10386 [para_into,8235,430] f(f(f(f(x,y),z),x),f(f(y,x),x))=x. given clause #405: (wt=15) 10412 [para_into,8243,593] f(f(f(x,y),y),f(f(f(x,x),z),y))=y. given clause #406: (wt=23) 297 [para_into,193,2] f(f(x,f(x,f(f(y,z),f(y,z)))),f(y,f(f(x,z),f(x,z))))=x. given clause #407: (wt=15) 10414 [para_into,8243,576] f(f(f(x,y),y),f(f(z,f(x,x)),y))=y. given clause #408: (wt=15) 10420 [para_into,8243,596] f(f(x,f(y,x)),f(f(f(y,y),z),x))=x. given clause #409: (wt=15) 10422 [para_into,8243,594] f(f(f(x,f(y,y)),z),f(f(y,z),z))=z. given clause #410: (wt=15) 10428 [para_into,8243,572] f(f(f(f(x,x),y),z),f(z,f(x,z)))=z. given clause #411: (wt=23) 299 [para_from,193,2,demod,194,flip.1] f(f(x,f(x,y)),f(f(z,f(x,y)),f(z,f(x,y))))=f(z,f(x,x)). given clause #412: (wt=15) 10434 [para_into,8243,430] f(f(f(f(x,x),y),z),f(f(x,z),z))=z. given clause #413: (wt=15) 10472 [para_into,8267,576] f(f(x,f(y,x)),f(f(z,f(y,y)),x))=x. given clause #414: (wt=15) 10478 [para_into,8267,594] f(f(f(x,f(y,y)),z),f(z,f(y,z)))=z. given clause #415: (wt=15) 10510 [para_into,8271,593] f(x,f(f(f(x,x),y),f(x,z)))=f(x,z). given clause #416: (wt=23) 301 [para_from,197,2,demod,198] f(x,f(f(y,z),f(y,z)))=f(f(f(y,z),y),f(f(x,y),f(x,y))). given clause #417: (wt=15) 10512 [para_into,8271,576] f(x,f(f(y,f(x,x)),f(x,z)))=f(x,z). given clause #418: (wt=15) 10514 [para_into,8271,572] f(x,f(f(y,f(x,x)),f(z,x)))=f(x,z). given clause #419: (wt=15) 10518 [para_into,8271,420] f(x,f(f(f(x,x),y),f(z,x)))=f(x,z). given clause #420: (wt=15) 10528 [para_into,8271,594] f(f(f(x,f(y,y)),f(y,z)),y)=f(y,z). given clause #421: (wt=23) 302 [copy,301,flip.1] f(f(f(x,y),x),f(f(z,x),f(z,x)))=f(z,f(f(x,y),f(x,y))). given clause #422: (wt=15) 10530 [para_into,8271,593] f(f(f(x,y),f(f(y,y),z)),y)=f(y,x). given clause #423: (wt=15) 10532 [para_into,8271,576] f(f(f(f(x,x),y),f(z,x)),x)=f(x,z). given clause #424: (wt=15) 10534 [para_into,8271,575] f(f(f(x,y),f(z,f(x,x))),x)=f(x,y). given clause #425: (wt=15) 10536 [para_into,8271,430] f(f(f(f(x,x),y),f(x,z)),x)=f(x,z). given clause #426: (wt=21) 303 [para_into,44,117] f(x,f(f(f(f(y,x),z),y),f(f(f(x,y),z),y)))=f(x,y). given clause #427: (wt=15) 10538 [para_into,8271,117] f(f(f(x,y),f(f(x,x),z)),x)=f(x,y). given clause #428: (wt=15) 10626 [para_into,8275,594] f(f(f(x,f(y,y)),f(z,y)),y)=f(z,y). given clause #429: (wt=15) 10628 [para_into,8275,575] f(f(f(x,y),f(z,f(y,y))),y)=f(x,y). given clause #430: (wt=15) 11450 [para_into,8505,8275] f(f(x,f(y,x)),f(x,f(z,f(x,y))))=x. given clause #431: (wt=21) 305 [para_into,44,117] f(x,f(f(f(y,f(x,z)),z),f(f(f(x,z),y),z)))=f(x,z). given clause #432: (wt=15) 11458 [para_into,8505,420] f(f(x,f(y,x)),f(x,f(z,f(y,x))))=x. given clause #433: (wt=15) 11470 [para_into,8505,576] f(f(x,f(y,x)),f(f(z,f(y,x)),x))=x. given clause #434: (wt=15) 11472 [para_into,8505,430] f(f(x,f(y,x)),f(f(z,f(x,y)),x))=x. given clause #435: (wt=15) 11474 [para_into,8505,594] f(f(f(x,f(y,z)),y),f(y,f(z,y)))=y. given clause #436: (wt=21) 307 [para_into,44,117] f(x,f(f(y,f(f(x,y),z)),f(f(f(x,y),z),y)))=f(x,y). given clause #437: (wt=15) 11476 [para_into,8505,575] f(f(x,f(y,f(x,z))),f(x,f(z,x)))=x. given clause #438: (wt=15) 11514 [para_into,8509,117] f(f(x,y),f(y,f(f(y,f(y,x)),z)))=y. given clause #439: (wt=15) 11534 [para_into,8509,117] f(f(x,y),f(x,f(f(x,f(y,x)),z)))=x. given clause #440: (wt=15) 11540 [para_into,8509,430] f(f(x,y),f(x,f(f(f(y,x),x),z)))=x. given clause #441: (wt=21) 309 [para_into,44,117] f(x,f(f(f(f(x,y),z),y),f(f(f(y,x),z),y)))=f(x,y). given clause #442: (wt=15) 11542 [para_into,8509,8275] f(f(x,y),f(x,f(z,f(x,f(x,y)))))=x. given clause #443: (wt=15) 11546 [para_into,8509,570] f(f(x,y),f(x,f(z,f(f(y,x),x))))=x. given clause #444: (wt=15) 11548 [para_into,8509,569] f(f(x,y),f(x,f(z,f(x,f(y,x)))))=x. given clause #445: (wt=15) 11550 [para_into,8509,420] f(f(x,y),f(x,f(z,f(f(x,y),x))))=x. given clause #446: (wt=21) 311 [para_into,44,117] f(x,f(f(f(f(x,y),z),y),f(f(z,f(x,y)),y)))=f(x,y). given clause #447: (wt=15) 11554 [para_into,8509,593] f(f(x,y),f(f(f(f(x,y),x),z),x))=x. given clause #448: (wt=15) 11556 [para_into,8509,576] f(f(x,y),f(f(z,f(f(x,y),x)),x))=x. given clause #449: (wt=15) 11560 [para_into,8509,430] f(f(x,y),f(f(z,f(x,f(x,y))),x))=x. given clause #450: (wt=15) 11562 [para_into,8509,117] f(f(x,y),f(f(f(x,f(x,y)),z),x))=x. given clause #451: (wt=21) 313 [para_into,44,117] f(x,f(f(f(f(x,y),z),y),f(y,f(f(x,y),z))))=f(x,y). given clause #452: (wt=15) 11564 [para_into,8509,596] f(f(x,y),f(f(f(y,f(y,x)),z),y))=y. given clause #453: (wt=15) 11566 [para_into,8509,594] f(f(f(x,f(y,f(y,z))),y),f(y,z))=y. given clause #454: (wt=15) 11568 [para_into,8509,575] f(f(x,f(y,f(x,f(x,z)))),f(x,z))=x. given clause #455: (wt=15) 11570 [para_into,8509,572] f(f(f(f(x,f(x,y)),z),x),f(y,x))=x. given clause #456: (wt=21) 315 [para_into,44,117] f(f(f(f(f(x,y),z),y),f(f(f(x,y),z),y)),x)=f(x,y). given clause #457: (wt=15) 11576 [para_into,8509,430] f(f(f(f(x,f(x,y)),z),x),f(x,y))=x. given clause #458: (wt=15) 11578 [para_into,8509,420] f(f(x,f(f(x,f(x,y)),z)),f(y,x))=x. given clause #459: (wt=15) 11580 [para_into,8509,117] f(f(x,f(f(x,f(x,y)),z)),f(x,y))=x. given clause #460: (wt=15) 11624 [para_into,8511,430] f(f(x,y),f(y,f(f(f(y,x),y),z)))=y. given clause #461: (wt=23) 317 [para_into,227,2] f(f(x,f(f(y,z),f(y,z))),f(y,f(f(f(x,z),f(x,z)),y)))=y. given clause #462: (wt=15) 11626 [para_into,8511,8275] f(f(x,y),f(y,f(z,f(y,f(x,y)))))=y. given clause #463: (wt=15) 11630 [para_into,8511,570] f(f(x,y),f(y,f(z,f(f(y,x),y))))=y. given clause #464: (wt=15) 11632 [para_into,8511,569] f(f(x,y),f(y,f(z,f(y,f(y,x)))))=y. given clause #465: (wt=15) 11634 [para_into,8511,420] f(f(x,y),f(y,f(z,f(f(x,y),y))))=y. given clause #466: (wt=23) 328 [para_from,247,2,demod,248,flip.1] f(f(x,f(x,y)),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(x,x)). given clause #467: (wt=15) 11638 [para_into,8511,593] f(f(x,y),f(f(f(f(x,y),y),z),y))=y. given clause #468: (wt=15) 11640 [para_into,8511,576] f(f(x,y),f(f(z,f(f(x,y),y)),y))=y. given clause #469: (wt=15) 11644 [para_into,8511,430] f(f(x,y),f(f(z,f(y,f(x,y))),y))=y. given clause #470: (wt=15) 11646 [para_into,8511,117] f(f(x,y),f(f(f(y,f(x,y)),z),y))=y. given clause #471: (wt=23) 331 [para_into,257,2] f(f(x,f(f(f(y,z),f(y,z)),x)),f(y,f(f(x,z),f(x,z))))=x. given clause #472: (wt=15) 11652 [para_into,8511,596] f(f(x,y),f(f(f(x,f(y,x)),z),x))=x. given clause #473: (wt=15) 11654 [para_into,8511,594] f(f(f(x,f(y,f(z,y))),y),f(z,y))=y. given clause #474: (wt=15) 11656 [para_into,8511,575] f(f(x,f(y,f(x,f(z,x)))),f(z,x))=x. given clause #475: (wt=15) 11658 [para_into,8511,572] f(f(f(f(x,f(y,x)),z),x),f(x,y))=x. given clause #476: (wt=23) 335 [para_from,257,2,demod,258,flip.1] f(f(x,f(y,x)),f(f(z,f(x,y)),f(z,f(x,y))))=f(z,f(x,x)). given clause #477: (wt=15) 11660 [para_into,8511,430] f(f(f(f(x,f(y,x)),z),x),f(y,x))=x. given clause #478: (wt=15) 11662 [para_into,8511,420] f(f(x,f(f(x,f(y,x)),z)),f(x,y))=x. given clause #479: (wt=15) 11664 [para_into,8511,117] f(f(x,f(f(x,f(y,x)),z)),f(y,x))=x. given clause #480: (wt=15) 11686 [para_into,8515,8275] f(f(x,f(x,y)),f(x,f(z,f(x,y))))=x. given clause #481: (wt=21) 365 [para_from,337,14,demod,342,338,342] f(f(x,y),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(x,y)). given clause #482: (wt=15) 11694 [para_into,8515,420] f(f(x,f(x,y)),f(x,f(z,f(y,x))))=x. given clause #483: (wt=15) 11706 [para_into,8515,593] f(f(x,f(x,y)),f(f(f(y,x),z),x))=x. given clause #484: (wt=15) 11708 [para_into,8515,576] f(f(x,f(x,y)),f(f(z,f(y,x)),x))=x. given clause #485: (wt=15) 11710 [para_into,8515,430] f(f(x,f(x,y)),f(f(z,f(x,y)),x))=x. given clause #486: (wt=21) 367 [para_from,337,10,demod,342,338] f(f(x,y),f(z,f(f(y,x),f(y,x))))=f(f(x,y),f(y,x)). given clause #487: (wt=15) 11712 [para_into,8515,594] f(f(f(x,f(y,z)),y),f(y,f(y,z)))=y. given clause #488: (wt=15) 11714 [para_into,8515,575] f(f(x,f(y,f(x,z))),f(x,f(x,z)))=x. given clause #489: (wt=15) 11724 [para_into,8539,594] f(f(f(x,f(y,z)),z),f(f(z,y),z))=z. given clause #490: (wt=15) 11726 [para_into,8539,575] f(f(x,f(y,f(z,x))),f(f(x,z),x))=x. given clause #491: (wt=21) 369 [para_from,337,42,demod,338,342] f(f(x,f(f(y,z),f(y,z))),f(z,y))=f(f(z,y),f(y,z)). given clause #492: (wt=15) 11728 [para_into,8539,572] f(f(f(f(x,y),z),y),f(y,f(y,x)))=y. given clause #493: (wt=15) 11730 [para_into,8539,430] f(f(f(f(x,y),z),y),f(f(y,x),y))=y. given clause #494: (wt=15) 11842 [para_into,8551,613] f(f(x,f(y,f(z,x))),f(x,f(z,x)))=x. given clause #495: (wt=15) 11844 [para_into,8551,572] f(f(f(x,f(y,z)),z),f(z,f(z,y)))=z. given clause #496: (wt=21) 372 [para_into,50,337,demod,338,338] f(f(x,y),f(f(f(x,x),z),f(f(x,x),z)))=f(f(x,x),z). given clause #497: (wt=15) 11846 [para_into,8551,420] f(f(x,f(y,f(z,x))),f(x,f(x,z)))=x. given clause #498: (wt=15) 12054 [para_into,8577,613] f(f(f(x,f(y,z)),z),f(z,f(y,z)))=z. given clause #499: (wt=15) 12822 [para_into,8651,596] f(f(x,y),f(f(f(f(y,x),y),z),y))=y. given clause #500: (wt=15) 12824 [para_into,8651,594] f(f(f(x,f(f(y,z),y)),y),f(y,z))=y. given clause #501: (wt=21) 374 [para_into,50,117] f(f(x,y),f(f(f(x,x),z),f(z,f(x,x))))=f(z,f(x,x)). given clause #502: (wt=15) 12826 [para_into,8651,575] f(f(x,f(y,f(f(x,z),x))),f(x,z))=x. given clause #503: (wt=15) 12828 [para_into,8651,572] f(f(f(f(f(x,y),x),z),x),f(y,x))=x. given clause #504: (wt=15) 12834 [para_into,8651,430] f(f(f(f(f(x,y),x),z),x),f(x,y))=x. given clause #505: (wt=15) 12836 [para_into,8651,420] f(f(x,f(f(f(x,y),x),z)),f(y,x))=x. given clause #506: (wt=21) 376 [para_into,50,44,demod,45,45] f(f(f(f(f(x,y),z),y),u),f(f(x,y),f(x,y)))=f(x,y). ----> UNIT CONFLICT at 45.15 sec ----> 15663 [binary,15661,3288] $Ans(OML_Sh). Length of proof is 33. Level of proof is 12. ---------------- PROOF ---------------- 2 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 4,3 [] f(f(x,x),f(x,y))=x. 5 [] f(x,f(x,f(x,y)))=f(x,y). 7 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(C,f(f(A,A),C)),C)))!=A|$Ans(OML_Sh). 9,8 [para_into,3,3] f(x,f(f(x,x),y))=f(x,x). 13,12 [para_from,3,2,flip.1] f(x,f(f(y,x),f(y,x)))=f(y,x). 14 [para_from,3,2,demod,4,flip.1] f(f(x,x),f(f(y,f(x,z)),f(y,f(x,z))))=f(y,f(x,x)). 31,30 [para_into,12,3,demod,4,4] f(f(x,y),f(x,x))=x. 33,32 [para_from,12,8] f(x,f(y,f(x,x)))=f(x,x). 34 [para_from,12,5,demod,13] f(x,f(x,f(y,x)))=f(y,x). 45,44 [para_into,30,2] f(x,f(f(f(f(x,y),z),y),f(f(f(x,y),z),y)))=f(x,y). 46 [para_from,30,5,demod,31] f(f(x,y),f(f(x,y),x))=x. 48 [para_from,30,3] f(f(f(x,y),f(x,y)),x)=f(x,y). 50 [para_from,30,2,demod,31,flip.1] f(f(x,y),f(f(z,f(x,x)),f(z,f(x,x))))=f(z,f(x,x)). 99 [para_into,14,32,demod,33,4] f(f(x,x),y)=f(y,f(x,x)). 103 [para_from,14,32] f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),f(x,f(y,z))). 117 [para_into,99,99,demod,4,4] f(x,y)=f(y,x). 127,126 [para_into,117,46,flip.1] f(f(f(x,y),x),f(x,y))=x. 129,128 [para_into,117,34,flip.1] f(f(x,f(y,x)),x)=f(y,x). 133 [back_demod,7,demod,129,9] f(f(f(f(B,A),f(A,C)),D),f(A,A))!=A|$Ans(OML_Sh). 146,145 [para_from,117,12] f(x,f(f(y,x),f(x,y)))=f(y,x). 197 [para_from,126,46] f(f(f(x,y),x),x)=f(x,y). 199 [para_from,126,2,demod,127,flip.1] f(f(f(x,y),x),f(f(z,f(x,y)),f(z,f(x,y))))=f(z,f(x,x)). 338,337 [para_into,48,117] f(f(f(x,y),f(y,x)),y)=f(y,x). 342,341 [para_into,145,145,demod,338,146] f(f(f(x,y),f(y,x)),f(f(x,y),f(y,x)))=f(x,y). 366,365 [para_from,337,14,demod,342,338,342] f(f(x,y),f(f(z,f(y,x)),f(z,f(y,x))))=f(z,f(x,y)). 371 [para_into,50,337,demod,342,342,366,342] f(x,f(y,z))=f(x,f(z,y)). 376 [para_into,50,44,demod,45,45] f(f(f(f(f(x,y),z),y),u),f(f(x,y),f(x,y)))=f(x,y). 420 [para_into,371,117] f(f(x,y),z)=f(z,f(y,x)). 430 [copy,420,flip.1] f(x,f(y,z))=f(f(z,y),x). 596 [para_into,430,420] f(f(x,y),f(z,u))=f(f(y,x),f(u,z)). 3288 [para_from,596,133] f(f(f(f(A,B),f(C,A)),D),f(A,A))!=A|$Ans(OML_Sh). 8007 [para_into,199,103,demod,4,31] f(f(f(x,f(y,y)),x),f(x,f(y,z)))=x. 8087 [para_into,8007,12] f(f(f(x,y),y),f(y,f(f(x,y),z)))=y. 8651 [para_into,8087,197] f(f(x,y),f(x,f(f(f(x,y),x),z)))=x. 12837,12836 [para_into,8651,420] f(f(x,f(f(f(x,y),x),z)),f(y,x))=x. 15661 [para_into,376,12836,demod,12837,12837,12837] f(f(f(f(x,y),f(z,x)),u),f(x,x))=x. 15663 [binary,15661,3288] $Ans(OML_Sh). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 506 clauses generated 707054 para_from generated 296597 para_into generated 410457 demod & eval rewrites 1337930 clauses wt,lit,sk delete 160585 tautologies deleted 0 clauses forward subsumed 540482 (subsumed by sos) 8816 unit deletions 0 factor simplifications 0 clauses kept 9075 new demodulators 6587 empty clauses 1 clauses back demodulated 692 clauses back subsumed 33 usable size 502 sos size 7848 demodulators size 5987 passive size 0 hot size 0 Kbytes malloced 10378 ----------- times (seconds) ----------- user CPU time 45.15 (0 hr, 0 min, 45 sec) system CPU time 2.85 (0 hr, 0 min, 2 sec) wall-clock time 48 (0 hr, 0 min, 48 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.56 para_into time 2.14 para_from time 1.70 pre_process time 28.00 renumber time 1.19 demod time 21.75 order equalities 0.74 unit deleletion 0.00 factor simplify 0.00 weigh cl time 1.04 hints keep time 0.00 sort lits time 0.00 forward subsume 0.97 delete cl time 0.62 keep cl time 0.26 hints time 0.00 print_cl time 0.00 conflict time 0.25 new demod time 0.10 post_process time 12.39 back demod time 9.64 back subsume 2.68 factor time 0.00 unindex time 0.64 That finishes the proof of the theorem. Process 2370 finished Mon Sep 15 12:20:44 2003