----- Otter 3.3, August 2003 ----- The process was started by mccune on lemma.mcs.anl.gov, Mon Sep 15 12:17:32 2003 The command was "otter". The process ID is 2360. 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,25). assign(pick_given_ratio,4). set(discard_commutativity_consequences). 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(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,x))=f(y,f(y,y)). 0 [] f(x,f(x,x))=1. 0 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(A,f(f(B,B),B)),C)))!=A|$Ans(OL_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,x))=f(y,f(y,y)). ** KEPT (pick-wt=7): 6 [] f(x,f(x,x))=1. ---> New Demodulator: 7 [new_demod,6] f(x,f(x,x))=1. ** KEPT (pick-wt=23): 8 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(A,f(f(B,B),B)),C)))!=A|$Ans(OL_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. Following clause subsumed by 1 during input processing: 0 [copy,5,flip.1,demod,7,7] 1=1. >>>> Starting back demodulation with 7. >> back demodulating 5 with 7. ======= 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=7) 6 [] f(x,f(x,x))=1. given clause #3: (wt=9) 3 [] f(f(x,x),f(x,y))=x. given clause #4: (wt=7) 15 [para_into,3,6] f(f(x,x),1)=x. given clause #5: (wt=7) 21 [para_from,3,6] f(f(x,x),x)=1. given clause #6: (wt=11) 13 [para_into,3,3] f(x,f(f(x,x),y))=f(x,x). given clause #7: (wt=7) 28 [para_into,15,3] f(x,1)=f(x,x). given clause #8: (wt=7) 31 [copy,28,flip.1] f(x,x)=f(x,1). given clause #9: (wt=7) 45 [para_from,31,21] f(f(x,1),x)=1. given clause #10: (wt=7) 47 [para_from,31,15] f(f(x,1),1)=x. given clause #11: (wt=17) 32 [back_demod,25,demod,30] f(f(x,x),f(f(y,f(x,z)),1))=f(y,f(x,x)). given clause #12: (wt=7) 51 [para_from,31,6] f(x,f(x,1))=1. given clause #13: (wt=7) 60 [para_into,32,45,demod,30,48,48,30,48] f(x,y)=f(y,x). given clause #14: (wt=7) 75 [para_into,60,47,flip.1] f(1,f(x,1))=x. given clause #15: (wt=7) 79 [para_into,60,28] f(x,x)=f(1,x). given clause #16: (wt=11) 34 [back_demod,23,demod,30] f(x,f(f(y,x),1))=f(y,x). given clause #17: (wt=7) 80 [para_into,60,15,flip.1] f(1,f(x,x))=x. given clause #18: (wt=7) 84 [copy,79,flip.1] f(1,x)=f(x,x). given clause #19: (wt=7) 85 [para_from,60,51] f(x,f(1,x))=1. given clause #20: (wt=7) 87 [para_from,60,47] f(f(1,x),1)=x. given clause #21: (wt=13) 38 [back_demod,17,demod,30] f(f(x,x),f(y,f(f(x,z),1)))=x. given clause #22: (wt=7) 89 [para_from,60,45] f(f(1,x),x)=1. given clause #23: (wt=7) 99 [para_into,75,60] f(1,f(1,x))=x. given clause #24: (wt=7) 101 [para_from,75,3] f(f(1,1),x)=1. given clause #25: (wt=7) 103 [para_from,75,32,demod,95,flip.1] f(x,f(1,1))=1. given clause #26: (wt=11) 42 [back_demod,9,demod,30] f(x,f(f(f(x,y),y),1))=1. given clause #27: (wt=9) 53 [para_from,31,3] f(f(x,1),f(x,y))=x. given clause #28: (wt=9) 67 [para_into,32,31,demod,48,4,flip.1] f(f(x,y),f(x,x))=x. given clause #29: (wt=9) 94 [para_from,60,3] f(f(x,x),f(y,x))=x. given clause #30: (wt=9) 111 [para_from,79,3] f(f(1,x),f(x,y))=x. given clause #31: (wt=15) 44 [back_demod,2,demod,30,30] f(x,f(f(y,z),1))=f(y,f(f(x,z),1)). given clause #32: (wt=9) 115 [para_into,34,3,demod,4] f(f(x,y),f(x,1))=x. given clause #33: (wt=9) 160 [para_into,53,60] f(f(x,1),f(y,x))=x. given clause #34: (wt=9) 166 [para_into,67,60] f(f(x,y),f(y,y))=y. given clause #35: (wt=9) 170 [para_into,67,79] f(f(x,y),f(1,x))=x. given clause #36: (wt=11) 49 [para_from,31,13] f(x,f(f(x,1),y))=f(x,x). given clause #37: (wt=9) 180 [para_into,94,79] f(f(1,x),f(y,x))=x. given clause #38: (wt=9) 186 [para_from,94,34,demod,95] f(f(x,y),f(y,1))=y. given clause #39: (wt=9) 269 [para_into,166,79] f(f(x,y),f(1,y))=y. given clause #40: (wt=11) 71 [back_demod,63,demod,70] f(f(f(x,y),1),f(x,x))=1. given clause #41: (wt=15) 55 [back_demod,27,demod,50] f(f(f(f(B,A),f(A,C)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #42: (wt=11) 73 [para_from,32,13] f(x,f(y,f(x,x)))=f(x,x). given clause #43: (wt=11) 82 [para_into,60,13,flip.1] f(f(f(x,x),y),x)=f(x,x). given clause #44: (wt=11) 105 [back_demod,40,demod,104] f(x,f(f(y,f(x,x)),1))=1. given clause #45: (wt=11) 109 [para_from,79,13] f(x,f(f(1,x),y))=f(x,x). given clause #46: (wt=17) 56 [para_into,32,31] f(f(x,1),f(f(y,f(x,z)),1))=f(y,f(x,x)). given clause #47: (wt=11) 113 [para_into,34,60] f(x,f(f(x,y),1))=f(y,x). given clause #48: (wt=11) 117 [para_into,34,60] f(x,f(1,f(y,x)))=f(y,x). given clause #49: (wt=11) 119 [para_into,34,60] f(f(f(x,y),1),y)=f(x,y). given clause #50: (wt=11) 130 [para_into,38,47,demod,30,48] f(x,f(y,f(x,1)))=f(x,1). given clause #51: (wt=15) 58 [para_into,32,3,demod,4] f(x,f(f(y,f(f(x,x),z)),1))=f(y,x). given clause #52: (wt=11) 144 [para_from,89,32,demod,104,flip.1] f(f(1,f(x,y)),f(x,x))=1. given clause #53: (wt=11) 146 [para_into,42,60] f(x,f(f(f(y,x),y),1))=1. given clause #54: (wt=11) 152 [para_into,42,60] f(x,f(f(y,f(x,y)),1))=1. given clause #55: (wt=11) 154 [para_into,42,60] f(x,f(1,f(f(x,y),y)))=1. given clause #56: (wt=15) 61 [para_into,32,32,demod,4,4] f(x,f(f(y,f(z,f(x,x))),1))=f(y,x). given clause #57: (wt=11) 156 [para_into,42,60] f(f(f(f(x,y),y),1),x)=1. given clause #58: (wt=11) 168 [para_into,67,32,demod,4] f(f(x,f(y,y)),y)=f(y,y). given clause #59: (wt=11) 172 [para_into,67,53] f(f(f(x,1),y),x)=f(x,1). given clause #60: (wt=11) 174 [para_from,67,53] f(f(f(x,y),1),x)=f(x,y). given clause #61: (wt=21) 65 [para_into,32,32,demod,30,30,33] f(f(f(x,f(y,z)),1),f(f(x,f(y,y)),1))=f(x,f(y,y)). given clause #62: (wt=11) 188 [para_into,111,67] f(f(1,f(x,y)),x)=f(x,y). given clause #63: (wt=11) 190 [para_into,44,111,demod,108] f(x,f(y,1))=f(x,f(y,y)). given clause #64: (wt=11) 191 [para_into,44,89,demod,104,flip.1] f(f(1,x),f(f(y,x),1))=1. given clause #65: (wt=11) 193 [para_into,44,85,demod,104,flip.1] f(x,f(f(y,f(1,x)),1))=1. given clause #66: (wt=17) 77 [para_into,60,32,flip.1] f(f(f(x,f(y,z)),1),f(y,y))=f(x,f(y,y)). given clause #67: (wt=11) 198 [para_into,44,51,demod,104,flip.1] f(x,f(f(y,f(x,1)),1))=1. given clause #68: (wt=11) 200 [para_into,44,45,demod,104,flip.1] f(f(x,1),f(f(y,x),1))=1. given clause #69: (wt=11) 211 [para_into,44,21,demod,104,flip.1] f(f(x,x),f(f(y,x),1))=1. given clause #70: (wt=11) 213 [para_into,44,15,demod,48] f(x,f(y,1))=f(f(y,y),x). given clause #71: (wt=17) 91 [para_from,60,32] f(f(x,x),f(1,f(y,f(x,z))))=f(y,f(x,x)). given clause #72: (wt=11) 218 [para_into,44,32,demod,4] f(x,f(y,y))=f(x,f(y,1)). given clause #73: (wt=11) 221 [copy,213,flip.1] f(f(x,x),y)=f(y,f(x,1)). given clause #74: (wt=11) 240 [para_from,44,21,demod,120,114] f(f(x,y),f(f(y,x),1))=1. given clause #75: (wt=11) 244 [para_from,44,6,demod,120,114] f(f(f(x,y),1),f(y,x))=1. given clause #76: (wt=17) 92 [para_from,60,32] f(f(x,x),f(f(f(x,y),z),1))=f(z,f(x,x)). given clause #77: (wt=11) 250 [para_into,115,87] f(f(f(1,x),y),x)=f(1,x). given clause #78: (wt=11) 256 [para_into,160,87] f(x,f(y,f(1,x)))=f(1,x). given clause #79: (wt=11) 267 [para_into,166,115] f(f(x,f(y,1)),y)=f(y,1). given clause #80: (wt=11) 274 [para_from,166,111] f(f(1,f(x,y)),y)=f(x,y). given clause #81: (wt=17) 96 [para_from,60,32] f(f(x,x),f(f(y,f(z,x)),1))=f(y,f(x,x)). given clause #82: (wt=11) 282 [para_into,170,170] f(x,f(1,f(x,y)))=f(x,y). given clause #83: (wt=11) 290 [para_from,49,166,demod,30,93] f(x,f(y,y))=f(f(y,1),x). given clause #84: (wt=11) 291 [copy,290,flip.1] f(f(x,1),y)=f(y,f(x,x)). given clause #85: (wt=11) 296 [para_from,180,166] f(f(x,f(1,y)),y)=f(1,y). given clause #86: (wt=17) 98 [copy,91,flip.1] f(x,f(y,y))=f(f(y,y),f(1,f(x,f(y,z)))). given clause #87: (wt=11) 316 [para_into,71,170,demod,30] f(f(x,1),f(f(x,y),1))=1. given clause #88: (wt=11) 318 [para_into,71,60] f(f(f(x,y),1),f(y,y))=1. given clause #89: (wt=11) 322 [para_into,71,32,demod,4] f(f(f(x,f(y,y)),1),y)=1. given clause #90: (wt=11) 324 [para_into,71,269] f(f(f(f(1,x),y),1),x)=1. given clause #91: (wt=17) 107 [para_from,79,32] f(f(1,x),f(f(y,f(x,z)),1))=f(y,f(x,x)). given clause #92: (wt=11) 326 [para_into,71,166] f(f(f(f(x,x),y),1),x)=1. given clause #93: (wt=11) 328 [para_into,71,115] f(f(f(f(x,1),y),1),x)=1. given clause #94: (wt=11) 330 [para_into,71,79] f(f(f(x,y),1),f(1,x))=1. given clause #95: (wt=11) 334 [para_into,71,31] f(f(f(x,y),1),f(x,1))=1. given clause #96: (wt=13) 121 [para_into,38,79] f(f(1,x),f(y,f(f(x,z),1)))=x. given clause #97: (wt=11) 336 [para_into,71,60] f(f(x,x),f(f(x,y),1))=1. given clause #98: (wt=11) 355 [para_from,82,71,demod,16,30] f(x,f(f(f(x,x),y),1))=1. given clause #99: (wt=11) 363 [para_into,105,60] f(x,f(1,f(y,f(x,x))))=1. given clause #100: (wt=11) 409 [para_into,58,269,demod,108] f(x,f(y,y))=f(x,f(1,y)). given clause #101: (wt=13) 123 [para_into,38,31] f(f(x,1),f(y,f(f(x,z),1)))=x. given clause #102: (wt=11) 416 [para_into,58,89,demod,104,flip.1] f(f(1,f(f(x,x),y)),x)=1. given clause #103: (wt=11) 424 [copy,409,flip.1] f(x,f(1,y))=f(x,f(y,y)). given clause #104: (wt=11) 441 [para_into,144,170,demod,30] f(f(1,x),f(f(x,y),1))=1. given clause #105: (wt=11) 443 [para_into,144,117] f(f(1,f(x,y)),f(y,y))=1. given clause #106: (wt=15) 125 [para_into,38,3] f(x,f(y,f(f(f(x,x),z),1)))=f(x,x). given clause #107: (wt=11) 445 [para_into,144,56,demod,30,48] f(f(1,f(x,f(y,y))),y)=1. given clause #108: (wt=11) 449 [para_into,144,269] f(f(1,f(f(1,x),y)),x)=1. given clause #109: (wt=11) 451 [para_into,144,115] f(f(1,f(f(x,1),y)),x)=1. given clause #110: (wt=11) 453 [para_into,144,79] f(f(1,f(x,y)),f(1,x))=1. given clause #111: (wt=13) 128 [para_into,38,60] f(f(x,x),f(y,f(f(z,x),1)))=x. given clause #112: (wt=11) 457 [para_into,144,31] f(f(1,f(x,y)),f(x,1))=1. given clause #113: (wt=11) 459 [para_into,144,60] f(f(x,x),f(1,f(x,y)))=1. given clause #114: (wt=11) 463 [para_into,146,146,demod,88] f(f(f(f(x,y),x),1),y)=1. given clause #115: (wt=11) 473 [para_into,146,60] f(x,f(f(y,f(y,x)),1))=1. given clause #116: (wt=15) 132 [para_into,38,32,demod,4] f(x,f(y,f(f(z,f(x,x)),1)))=f(x,x). given clause #117: (wt=11) 477 [para_into,146,60] f(x,f(1,f(f(y,x),y)))=1. given clause #118: (wt=11) 487 [para_into,152,60] f(x,f(1,f(y,f(x,y))))=1. given clause #119: (wt=11) 489 [para_into,152,60] f(f(f(x,f(y,x)),1),y)=1. given clause #120: (wt=11) 519 [para_into,154,60] f(f(1,f(f(x,y),y)),x)=1. given clause #121: (wt=13) 134 [para_into,38,60] f(f(x,x),f(y,f(1,f(x,z))))=x. given clause #122: (wt=11) 559 [para_into,156,144,demod,81] f(f(x,1),f(1,f(x,y)))=1. given clause #123: (wt=11) 583 [para_from,172,144,demod,76,30] f(x,f(f(f(x,1),y),1))=1. given clause #124: (wt=11) 656 [para_from,190,113,demod,114] f(f(x,x),y)=f(f(x,1),y). given clause #125: (wt=11) 669 [copy,656,flip.1] f(f(x,1),y)=f(f(x,x),y). given clause #126: (wt=13) 136 [para_into,38,60] f(f(x,x),f(f(f(x,y),1),z))=x. given clause #127: (wt=11) 673 [para_into,191,180] f(f(1,f(x,y)),f(y,1))=1. given clause #128: (wt=11) 675 [para_into,191,130,demod,48] f(f(1,f(x,f(y,1))),y)=1. given clause #129: (wt=11) 683 [para_into,191,60] f(f(1,x),f(1,f(y,x)))=1. given clause #130: (wt=11) 685 [para_into,191,60] f(f(f(x,y),1),f(1,y))=1. given clause #131: (wt=13) 138 [para_into,38,60] f(f(x,f(f(y,z),1)),f(y,y))=y. given clause #132: (wt=11) 687 [para_from,191,146,demod,100] f(f(f(x,y),1),f(y,1))=1. given clause #133: (wt=11) 691 [para_into,193,188] f(x,f(f(f(1,x),y),1))=1. given clause #134: (wt=11) 693 [para_into,193,60] f(x,f(1,f(y,f(1,x))))=1. given clause #135: (wt=11) 695 [para_into,193,60] f(f(f(x,f(1,y)),1),y)=1. given clause #136: (wt=13) 141 [para_from,38,34,demod,39] f(f(x,f(f(y,z),1)),f(y,1))=y. given clause #137: (wt=11) 731 [para_into,198,60] f(x,f(1,f(y,f(x,1))))=1. given clause #138: (wt=11) 733 [para_into,198,60] f(f(f(x,f(y,1)),1),y)=1. given clause #139: (wt=11) 739 [para_into,200,60] f(f(x,1),f(1,f(y,x)))=1. given clause #140: (wt=11) 745 [para_into,211,60] f(f(x,x),f(1,f(y,x)))=1. given clause #141: (wt=15) 162 [para_from,53,38] f(x,f(y,f(f(f(x,1),z),1)))=f(x,1). given clause #142: (wt=11) 749 [para_into,213,188,demod,100,100] f(x,f(1,y))=f(f(y,y),x). given clause #143: (wt=11) 752 [copy,749,flip.1] f(f(x,x),y)=f(y,f(1,x)). given clause #144: (wt=11) 874 [para_into,240,60] f(f(x,y),f(1,f(y,x)))=1. given clause #145: (wt=11) 886 [para_into,244,60] f(f(1,f(x,y)),f(y,x))=1. given clause #146: (wt=15) 164 [para_from,53,32,demod,30,48] f(x,f(f(y,f(f(x,1),z)),1))=f(y,x). given clause #147: (wt=11) 932 [back_demod,373,demod,911] f(x,f(y,y))=f(f(1,y),x). given clause #148: (wt=11) 935 [copy,932,flip.1] f(f(1,x),y)=f(y,f(x,x)). given clause #149: (wt=11) 968 [para_from,256,191,demod,88] f(f(1,f(x,f(1,y))),y)=1. given clause #150: (wt=11) 1174 [para_into,330,250,demod,88] f(x,f(1,f(f(1,x),y)))=1. given clause #151: (wt=15) 176 [para_from,67,38,demod,30] f(f(f(x,y),1),f(z,f(x,1)))=f(x,y). given clause #152: (wt=11) 1176 [para_into,330,172,demod,48] f(x,f(1,f(f(x,1),y)))=1. given clause #153: (wt=11) 1178 [para_into,330,82,demod,16] f(x,f(1,f(f(x,x),y)))=1. given clause #154: (wt=11) 1263 [para_from,409,113,demod,114] f(f(1,x),y)=f(f(x,x),y). given clause #155: (wt=11) 1272 [copy,1263,flip.1] f(f(x,x),y)=f(f(1,x),y). given clause #156: (wt=19) 178 [para_from,67,32,demod,30,30] f(f(f(x,y),1),f(f(z,x),1))=f(z,f(f(x,y),1)). given clause #157: (wt=11) 1326 [para_into,441,60] f(f(1,x),f(1,f(x,y)))=1. given clause #158: (wt=11) 1334 [para_into,443,79] f(f(1,f(x,y)),f(1,y))=1. given clause #159: (wt=11) 1452 [para_into,463,60] f(f(f(x,f(x,y)),1),y)=1. given clause #160: (wt=11) 1456 [para_into,463,60] f(f(1,f(f(x,y),x)),y)=1. given clause #161: (wt=19) 179 [copy,178,flip.1] f(x,f(f(y,z),1))=f(f(f(y,z),1),f(f(x,y),1)). given clause #162: (wt=11) 1482 [para_into,473,60] f(x,f(1,f(y,f(y,x))))=1. given clause #163: (wt=11) 1572 [para_into,487,60] f(f(1,f(x,f(y,x))),y)=1. given clause #164: (wt=11) 1598 [para_into,519,473,demod,76] f(f(1,f(x,f(x,y))),y)=1. given clause #165: (wt=13) 284 [para_into,170,44] f(f(x,f(f(y,z),1)),f(1,y))=y. given clause #166: (wt=19) 182 [para_into,94,38,demod,30] f(f(f(x,f(f(y,z),1)),1),y)=f(x,f(f(y,z),1)). given clause #167: (wt=13) 353 [para_from,82,32,demod,30,48,4,30,flip.1] f(f(f(f(x,y),1),z),f(x,x))=x. given clause #168: (wt=13) 391 [para_from,113,180,demod,76] f(f(x,y),f(y,x))=f(f(x,y),1). given clause #169: (wt=13) 923 [para_into,92,109,demod,30,48,4,flip.1] f(f(f(1,f(x,y)),z),f(x,x))=x. given clause #170: (wt=13) 966 [para_from,256,92,demod,88,4,flip.1] f(f(x,f(1,f(y,z))),f(y,y))=y. given clause #171: (wt=19) 184 [para_into,94,32,demod,30,48] f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),1). given clause #172: (wt=13) 1000 [para_into,96,267,demod,48,95,flip.1] f(f(x,f(f(y,z),1)),f(z,z))=z. given clause #173: (wt=13) 1002 [para_into,96,250,demod,88,95,flip.1] f(f(f(1,f(x,y)),z),f(y,y))=y. given clause #174: (wt=13) 1008 [para_into,96,172,demod,48,95,flip.1] f(f(f(f(x,y),1),z),f(y,y))=y. given clause #175: (wt=13) 1070 [para_from,296,96,demod,88,95,flip.1] f(f(x,f(1,f(y,z))),f(z,z))=z. given clause #176: (wt=15) 197 [para_into,44,60] f(x,f(f(y,z),1))=f(z,f(f(x,y),1)). given clause #177: (wt=13) 1204 [para_into,121,117] f(f(1,x),f(y,f(f(z,x),1)))=x. given clause #178: (wt=13) 1210 [para_into,121,60] f(f(1,x),f(y,f(1,f(x,z))))=x. given clause #179: (wt=13) 1216 [para_into,121,213,demod,30] f(f(1,x),f(f(f(x,y),1),z))=x. given clause #180: (wt=13) 1278 [para_into,123,117] f(f(x,1),f(y,f(f(z,x),1)))=x. given clause #181: (wt=23) 202 [para_into,44,44] f(x,f(f(y,f(f(z,u),1)),1))=f(z,f(f(x,f(f(y,u),1)),1)). given clause #182: (wt=13) 1282 [para_into,123,60] f(f(x,1),f(y,f(1,f(x,z))))=x. given clause #183: (wt=13) 1288 [para_into,123,213,demod,30] f(f(x,1),f(f(f(x,y),1),z))=x. given clause #184: (wt=13) 1396 [para_into,128,60] f(f(x,x),f(y,f(1,f(z,x))))=x. given clause #185: (wt=13) 1402 [para_into,128,213,demod,30] f(f(x,x),f(f(f(y,x),1),z))=x. given clause #186: (wt=15) 214 [para_into,44,60] f(x,f(1,f(y,z)))=f(y,f(f(x,z),1)). given clause #187: (wt=13) 1406 [para_into,128,221] f(f(x,f(f(y,z),1)),f(z,1))=z. given clause #188: (wt=13) 1412 [para_from,128,117,demod,129] f(f(x,f(f(y,z),1)),f(1,z))=z. given clause #189: (wt=13) 1662 [para_into,134,221] f(f(x,f(1,f(y,z))),f(y,1))=y. given clause #190: (wt=13) 1670 [para_from,134,117,demod,135] f(f(x,f(1,f(y,z))),f(1,y))=y. given clause #191: (wt=15) 217 [para_into,44,60] f(f(f(x,y),1),z)=f(x,f(f(z,y),1)). given clause #192: (wt=13) 3350 [para_into,1070,79] f(f(x,f(1,f(y,z))),f(1,z))=z. given clause #193: (wt=13) 3352 [para_into,1070,31] f(f(x,f(1,f(y,z))),f(z,1))=z. given clause #194: (wt=13) 3354 [para_into,1070,932] f(f(1,x),f(y,f(1,f(z,x))))=x. given clause #195: (wt=13) 3356 [para_into,1070,290] f(f(x,1),f(y,f(1,f(z,x))))=x. given clause #196: (wt=15) 219 [copy,197,flip.1] f(x,f(f(y,z),1))=f(y,f(f(z,x),1)). given clause #197: (wt=15) 222 [copy,214,flip.1] f(x,f(f(y,z),1))=f(y,f(1,f(x,z))). given clause #198: (wt=15) 252 [para_into,115,44] f(x,f(f(f(f(x,y),z),y),1))=f(x,y). given clause #199: (wt=15) 306 [para_into,186,44] f(x,f(f(f(y,f(x,z)),z),1))=f(x,z). given clause #200: (wt=15) 340 [para_into,55,60] f(f(f(f(A,B),f(A,C)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #201: (wt=17) 226 [para_from,44,94,demod,30,48] f(f(x,y),f(x,f(f(z,y),1)))=f(f(x,y),1). given clause #202: (wt=15) 341 [para_into,55,60] f(f(f(f(B,A),f(C,A)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #203: (wt=15) 342 [para_into,55,60] f(f(f(f(A,C),f(B,A)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #204: (wt=15) 343 [para_into,55,60] f(f(D,f(f(B,A),f(A,C))),f(A,A))!=A|$Ans(OL_Sh). given clause #205: (wt=15) 344 [para_into,55,79] f(f(f(f(B,A),f(A,C)),D),f(1,A))!=A|$Ans(OL_Sh). given clause #206: (wt=17) 232 [para_from,44,94,demod,120,114] f(f(x,y),f(z,f(f(y,x),1)))=f(f(y,x),1). given clause #207: (wt=15) 345 [para_into,55,31] f(f(f(f(B,A),f(A,C)),D),f(A,1))!=A|$Ans(OL_Sh). given clause #208: (wt=15) 346 [para_into,55,60] f(f(A,A),f(f(f(B,A),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #209: (wt=15) 349 [para_into,82,44,demod,120,114,30,48] f(f(f(x,y),z),f(f(y,x),1))=f(y,x). given clause #210: (wt=15) 359 [para_from,82,44,demod,16,flip.1] f(f(f(x,x),y),f(f(z,x),1))=f(z,x). given clause #211: (wt=17) 260 [para_from,160,44,flip.1] f(f(x,1),f(f(y,f(z,x)),1))=f(y,f(x,1)). given clause #212: (wt=15) 378 [para_into,56,94] f(f(x,1),f(y,1))=f(f(y,y),f(x,x)). given clause #213: (wt=15) 385 [copy,378,flip.1] f(f(x,x),f(y,y))=f(f(y,1),f(x,1)). given clause #214: (wt=15) 420 [para_into,58,60] f(x,f(f(f(f(x,x),y),z),1))=f(z,x). given clause #215: (wt=15) 422 [para_into,58,60] f(x,f(1,f(y,f(f(x,x),z))))=f(y,x). given clause #216: (wt=17) 262 [para_into,166,44,demod,30,48] f(f(x,f(f(y,z),1)),f(x,z))=f(f(x,z),1). given clause #217: (wt=15) 530 [para_into,61,60] f(x,f(f(f(y,f(x,x)),z),1))=f(z,x). given clause #218: (wt=15) 532 [para_into,61,60] f(x,f(1,f(y,f(z,f(x,x)))))=f(y,x). given clause #219: (wt=15) 575 [para_into,168,44,demod,120,114,30,48] f(f(x,f(y,z)),f(f(z,y),1))=f(z,y). given clause #220: (wt=15) 579 [para_from,168,44,demod,16,flip.1] f(f(x,f(y,y)),f(f(z,y),1))=f(z,y). given clause #221: (wt=17) 271 [para_into,166,44,demod,120,114] f(f(x,f(f(y,z),1)),f(z,y))=f(f(y,z),1). given clause #222: (wt=15) 587 [para_from,172,44,demod,48,flip.1] f(f(f(x,1),y),f(f(z,x),1))=f(z,x). given clause #223: (wt=15) 645 [para_from,190,146] f(f(x,1),f(f(f(y,f(x,x)),y),1))=1. given clause #224: (wt=15) 654 [para_from,190,152,demod,544,46] f(x,f(1,f(f(y,1),f(x,f(y,y)))))=1. given clause #225: (wt=15) 657 [para_from,190,154] f(x,f(1,f(f(x,f(y,y)),f(y,1))))=1. given clause #226: (wt=17) 304 [para_from,180,44,flip.1] f(f(1,x),f(f(y,f(z,x)),1))=f(y,f(x,1)). given clause #227: (wt=15) 750 [para_into,213,156,flip.1] f(f(x,x),f(f(f(f(x,1),y),y),1))=1. given clause #228: (wt=15) 755 [para_from,213,146] f(f(x,1),f(f(f(f(x,x),y),y),1))=1. given clause #229: (wt=15) 758 [para_from,213,154] f(x,f(1,f(f(y,y),f(x,f(y,1)))))=1. given clause #230: (wt=15) 764 [para_from,213,152,demod,432,46] f(x,f(1,f(f(y,1),f(f(y,y),x))))=1. given clause #231: (wt=19) 312 [para_into,269,38] f(x,f(1,f(y,f(f(x,z),1))))=f(y,f(f(x,z),1)). given clause #232: (wt=15) 766 [para_from,213,154] f(x,f(1,f(f(f(y,y),x),f(y,1))))=1. given clause #233: (wt=15) 783 [para_into,91,269,demod,30,88] f(x,f(1,f(y,f(f(1,x),z))))=f(y,x). given clause #234: (wt=15) 785 [para_into,91,213,demod,4,30,48] f(x,f(1,f(y,f(f(x,1),z))))=f(y,x). given clause #235: (wt=15) 823 [para_from,218,146] f(f(x,x),f(f(f(y,f(x,1)),y),1))=1. given clause #236: (wt=17) 379 [para_into,56,60] f(f(x,1),f(f(f(x,y),z),1))=f(z,f(x,x)). given clause #237: (wt=15) 825 [para_into,221,218] f(f(x,x),f(y,1))=f(f(y,y),f(x,1)). given clause #238: (wt=15) 826 [para_into,221,213] f(f(x,x),f(y,y))=f(f(x,1),f(y,1)). given clause #239: (wt=15) 836 [copy,826,flip.1] f(f(x,1),f(y,1))=f(f(x,x),f(y,y)). given clause #240: (wt=15) 841 [para_from,221,154] f(f(x,x),f(1,f(f(y,f(x,1)),y)))=1. given clause #241: (wt=17) 381 [para_into,56,60] f(f(x,1),f(1,f(y,f(x,z))))=f(y,f(x,x)). given clause #242: (wt=15) 847 [para_from,221,91,demod,4,4] f(x,f(1,f(y,f(z,f(x,1)))))=f(y,x). given clause #243: (wt=15) 896 [para_into,92,269,demod,30,88] f(x,f(f(f(f(1,x),y),z),1))=f(z,x). given clause #244: (wt=15) 898 [para_into,92,213,demod,4,30,48] f(x,f(f(f(f(x,1),y),z),1))=f(z,x). given clause #245: (wt=15) 904 [para_into,92,221,demod,4,4] f(x,f(f(f(y,f(x,1)),z),1))=f(z,x). given clause #246: (wt=17) 386 [copy,381,flip.1] f(x,f(y,y))=f(f(y,1),f(1,f(x,f(y,z)))). given clause #247: (wt=15) 964 [para_from,250,44,demod,88,flip.1] f(f(f(1,x),y),f(f(z,x),1))=f(z,x). given clause #248: (wt=15) 974 [para_from,267,44,demod,48,flip.1] f(f(x,f(y,1)),f(f(z,y),1))=f(z,y). given clause #249: (wt=15) 1042 [para_into,290,221] f(f(x,x),f(y,1))=f(f(x,1),f(y,y)). given clause #250: (wt=15) 1045 [copy,1042,flip.1] f(f(x,1),f(y,y))=f(f(x,x),f(y,1)). given clause #251: (wt=19) 513 [para_into,154,44] f(x,f(1,f(f(y,f(f(x,z),1)),f(f(y,z),1))))=1. given clause #252: (wt=15) 1048 [para_from,290,55] f(f(A,1),f(f(f(B,A),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #253: (wt=15) 1057 [para_into,291,190] f(f(x,1),f(y,y))=f(f(y,1),f(x,x)). given clause #254: (wt=15) 1065 [para_from,291,154] f(f(x,1),f(1,f(f(y,f(x,x)),y)))=1. given clause #255: (wt=15) 1074 [para_from,296,44,demod,88,flip.1] f(f(x,f(1,y)),f(f(z,y),1))=f(z,y). given clause #256: (wt=17) 787 [para_into,91,79] f(f(1,x),f(1,f(y,f(x,z))))=f(y,f(x,x)). given clause #257: (wt=15) 1137 [para_into,107,94] f(f(1,x),f(y,1))=f(f(y,y),f(x,x)). given clause #258: (wt=15) 1145 [copy,1137,flip.1] f(f(x,x),f(y,y))=f(f(1,y),f(x,1)). given clause #259: (wt=15) 1236 [para_into,409,291] f(f(x,x),f(y,y))=f(f(y,1),f(1,x)). given clause #260: (wt=15) 1237 [para_into,409,221] f(f(x,x),f(y,1))=f(f(y,y),f(1,x)). given clause #261: (wt=17) 794 [para_into,91,117] f(f(x,x),f(1,f(y,f(z,x))))=f(y,f(x,x)). given clause #262: (wt=15) 1240 [copy,1236,flip.1] f(f(x,1),f(1,y))=f(f(y,y),f(x,x)). given clause #263: (wt=15) 1241 [copy,1237,flip.1] f(f(x,x),f(1,y))=f(f(y,y),f(x,1)). given clause #264: (wt=15) 1247 [para_from,409,146] f(f(x,x),f(f(f(y,f(1,x)),y),1))=1. given clause #265: (wt=15) 1251 [para_from,409,154] f(x,f(1,f(f(x,f(y,y)),f(1,y))))=1. given clause #266: (wt=21) 796 [para_into,91,44] f(f(x,x),f(1,f(y,f(z,f(f(x,u),1)))))=f(y,f(x,x)). given clause #267: (wt=15) 1306 [para_into,424,291] f(f(1,x),f(y,y))=f(f(y,1),f(x,x)). given clause #268: (wt=15) 1307 [copy,1306,flip.1] f(f(x,1),f(y,y))=f(f(1,y),f(x,x)). given clause #269: (wt=15) 1312 [para_from,424,146] f(f(1,x),f(f(f(y,f(x,x)),y),1))=1. given clause #270: (wt=15) 1319 [para_from,424,152,demod,544,90] f(x,f(1,f(f(1,y),f(x,f(y,y)))))=1. given clause #271: (wt=17) 798 [para_into,91,188,demod,638] f(f(x,x),f(1,f(f(x,y),z)))=f(z,f(x,x)). given clause #272: (wt=15) 1344 [para_into,125,60] f(x,f(y,f(1,f(f(x,x),z))))=f(x,x). given clause #273: (wt=15) 1426 [para_into,459,77,demod,30,48] f(f(x,f(y,z)),f(1,f(x,f(y,y))))=1. given clause #274: (wt=13) 7152 [para_into,1426,296,demod,81,81] f(f(f(x,y),f(y,z)),f(1,y))=1. given clause #275: (wt=13) 7158 [para_into,1426,250,demod,81,81] f(f(f(x,y),f(x,z)),f(1,x))=1. given clause #276: (wt=17) 799 [copy,787,flip.1] f(x,f(y,y))=f(f(1,y),f(1,f(x,f(y,z)))). given clause #277: (wt=13) 7306 [para_into,7152,847] f(f(f(x,y),f(z,y)),f(1,y))=1. given clause #278: (wt=13) 7344 [para_into,7152,60] f(f(f(x,y),f(z,x)),f(1,x))=1. given clause #279: (wt=13) 7348 [para_into,7152,847,demod,104,76,104,76] f(f(f(x,y),f(y,z)),f(y,1))=1. given clause #280: (wt=13) 7360 [para_into,7152,84] f(f(f(x,y),f(y,z)),f(y,y))=1. given clause #281: (wt=17) 804 [copy,794,flip.1] f(x,f(y,y))=f(f(y,y),f(1,f(x,f(z,y)))). given clause #282: (wt=13) 7362 [para_into,7152,749] f(f(x,x),f(f(y,x),f(x,z)))=1. given clause #283: (wt=13) 7366 [para_into,7152,60] f(f(1,x),f(f(y,x),f(x,z)))=1. given clause #284: (wt=13) 7468 [para_into,7158,847,demod,104,76,104,76] f(f(f(x,y),f(x,z)),f(x,1))=1. given clause #285: (wt=13) 7478 [para_into,7158,84] f(f(f(x,y),f(x,z)),f(x,x))=1. given clause #286: (wt=17) 806 [copy,798,flip.1] f(x,f(y,y))=f(f(y,y),f(1,f(f(y,z),x))). given clause #287: (wt=13) 7480 [para_into,7158,749] f(f(x,x),f(f(x,y),f(x,z)))=1. given clause #288: (wt=13) 7484 [para_into,7158,60] f(f(1,x),f(f(x,y),f(x,z)))=1. given clause #289: (wt=13) 7613 [para_into,7306,847,demod,104,76,104,76] f(f(f(x,y),f(z,y)),f(y,1))=1. given clause #290: (wt=13) 7619 [para_into,7306,84] f(f(f(x,y),f(z,y)),f(y,y))=1. given clause #291: (wt=19) 809 [para_from,91,269,demod,100] f(f(x,f(y,y)),f(x,f(y,z)))=f(1,f(x,f(y,z))). given clause #292: (wt=13) 7621 [para_into,7306,749] f(f(x,x),f(f(y,x),f(z,x)))=1. given clause #293: (wt=13) 7625 [para_into,7306,60] f(f(1,x),f(f(y,x),f(z,x)))=1. given clause #294: (wt=13) 7697 [para_into,7344,847,demod,104,76,104,76] f(f(f(x,y),f(z,x)),f(x,1))=1. given clause #295: (wt=13) 7707 [para_into,7344,84] f(f(f(x,y),f(z,x)),f(x,x))=1. given clause #296: (wt=17) 900 [para_into,92,79] f(f(1,x),f(f(f(x,y),z),1))=f(z,f(x,x)). given clause #297: (wt=13) 7709 [para_into,7344,749] f(f(x,x),f(f(x,y),f(z,x)))=1. given clause #298: (wt=13) 7713 [para_into,7344,60] f(f(1,x),f(f(x,y),f(z,x)))=1. given clause #299: (wt=13) 7787 [para_into,7348,60] f(f(x,1),f(f(y,x),f(x,z)))=1. given clause #300: (wt=13) 8123 [para_into,7468,60] f(f(x,1),f(f(x,y),f(x,z)))=1. given clause #301: (wt=17) 910 [para_into,92,117] f(f(x,x),f(f(f(y,x),z),1))=f(z,f(x,x)). given clause #302: (wt=13) 8364 [para_into,7613,60] f(f(x,1),f(f(y,x),f(z,x)))=1. given clause #303: (wt=13) 8686 [para_into,7697,60] f(f(x,1),f(f(x,y),f(z,x)))=1. given clause #304: (wt=15) 1428 [para_into,459,44] f(f(x,x),f(1,f(y,f(f(x,z),1))))=1. given clause #305: (wt=15) 1494 [para_into,132,60] f(x,f(y,f(1,f(z,f(x,x)))))=f(x,x). given clause #306: (wt=23) 912 [para_into,92,77,demod,30,48,30,48] f(f(x,f(y,z)),f(f(f(x,f(y,y)),u),1))=f(u,f(x,f(y,z))). given clause #307: (wt=15) 1514 [para_into,477,424] f(f(1,x),f(1,f(f(y,f(x,x)),y)))=1. given clause #308: (wt=15) 1516 [para_into,477,409] f(f(x,x),f(1,f(f(y,f(1,x)),y)))=1. given clause #309: (wt=15) 1518 [para_into,477,290] f(f(x,x),f(1,f(f(f(x,1),y),y)))=1. given clause #310: (wt=15) 1520 [para_into,477,213] f(f(x,1),f(1,f(f(f(x,x),y),y)))=1. given clause #311: (wt=23) 933 [copy,912,flip.1] f(x,f(y,f(z,u)))=f(f(y,f(z,u)),f(f(f(y,f(z,z)),x),1)). given clause #312: (wt=15) 1536 [para_into,477,409] f(x,f(1,f(f(f(y,y),x),f(1,y))))=1. given clause #313: (wt=15) 1538 [para_into,477,213] f(x,f(1,f(f(y,y),f(f(y,1),x))))=1. given clause #314: (wt=15) 1550 [para_into,487,409] f(x,f(1,f(f(y,y),f(x,f(1,y)))))=1. given clause #315: (wt=15) 1640 [para_into,134,424,demod,167] f(x,f(y,f(1,f(f(1,x),z))))=f(1,x). given clause #316: (wt=19) 938 [para_from,92,130] f(f(f(x,y),z),f(z,f(x,x)))=f(f(f(x,y),z),1). given clause #317: (wt=15) 1642 [para_into,134,291,demod,68] f(x,f(y,f(1,f(f(x,1),z))))=f(x,1). given clause #318: (wt=15) 1648 [para_into,134,221,demod,4] f(x,f(y,f(1,f(z,f(x,1)))))=f(x,x). given clause #319: (wt=15) 1684 [para_into,559,44] f(f(x,1),f(1,f(y,f(f(x,z),1))))=1. given clause #320: (wt=15) 1690 [para_into,656,424] f(f(x,x),f(y,y))=f(f(x,1),f(1,y)). given clause #321: (wt=17) 990 [para_into,96,113,demod,30,48,30,48] f(f(x,y),f(f(z,f(y,x)),1))=f(z,f(x,y)). given clause #322: (wt=15) 1691 [para_into,656,409] f(f(x,x),f(1,y))=f(f(x,1),f(y,y)). given clause #323: (wt=15) 1693 [copy,1690,flip.1] f(f(x,1),f(1,y))=f(f(x,x),f(y,y)). given clause #324: (wt=15) 1694 [copy,1691,flip.1] f(f(x,1),f(y,y))=f(f(x,x),f(1,y)). given clause #325: (wt=15) 1760 [para_into,683,96,demod,76] f(f(x,f(y,z)),f(1,f(x,f(z,z))))=1. given clause #326: (wt=19) 1021 [para_from,96,130] f(f(x,f(y,z)),f(x,f(z,z)))=f(f(x,f(y,z)),1). given clause #327: (wt=15) 1762 [para_into,683,92,demod,76] f(f(f(x,y),z),f(1,f(z,f(x,x))))=1. given clause #328: (wt=15) 1764 [para_into,683,44,demod,76] f(f(x,y),f(1,f(x,f(f(z,y),1))))=1. given clause #329: (wt=15) 1770 [para_into,685,134] f(f(x,1),f(1,f(y,f(1,f(x,z)))))=1. given clause #330: (wt=15) 1774 [para_into,685,128] f(f(x,1),f(1,f(y,f(f(z,x),1))))=1. given clause #331: (wt=17) 1043 [para_into,290,188,flip.1] f(f(x,1),f(1,f(f(x,x),y)))=f(f(x,x),y). given clause #332: (wt=15) 1786 [para_into,138,170,demod,30] f(f(x,f(y,1)),f(f(y,z),1))=f(y,z). given clause #333: (wt=15) 1793 [para_into,138,92,demod,30] f(f(x,f(y,y)),f(f(y,z),1))=f(y,z). given clause #334: (wt=15) 1798 [para_from,138,453] f(f(1,x),f(1,f(y,f(f(x,z),1))))=1. given clause #335: (wt=15) 1838 [para_into,745,44,demod,120,114] f(f(x,y),f(1,f(z,f(f(y,x),1))))=1. given clause #336: (wt=17) 1094 [para_into,98,60,flip.1] f(f(x,x),f(1,f(y,f(x,z))))=f(f(x,x),y). given clause #337: (wt=15) 1850 [para_into,749,519,flip.1] f(f(x,x),f(1,f(f(f(1,x),y),y)))=1. given clause #338: (wt=15) 1854 [para_into,749,291] f(f(1,x),f(y,y))=f(f(x,x),f(y,1)). given clause #339: (wt=15) 1857 [para_into,749,221] f(f(1,x),f(y,1))=f(f(x,x),f(y,y)). given clause #340: (wt=15) 1860 [copy,1854,flip.1] f(f(x,x),f(y,1))=f(f(1,x),f(y,y)). given clause #341: (wt=19) 1418 [para_from,128,269] f(x,f(1,f(y,f(f(z,x),1))))=f(y,f(f(z,x),1)). given clause #342: (wt=15) 1861 [copy,1857,flip.1] f(f(x,x),f(y,y))=f(f(1,x),f(y,1)). given clause #343: (wt=15) 1864 [para_from,749,477] f(x,f(1,f(f(y,y),f(f(1,y),x))))=1. given clause #344: (wt=15) 1885 [para_from,749,487] f(x,f(1,f(f(1,y),f(f(y,y),x))))=1. given clause #345: (wt=15) 1894 [para_into,752,749] f(f(x,x),f(y,y))=f(f(1,x),f(1,y)). given clause #346: (wt=23) 1652 [para_into,134,77,demod,30,48] f(f(x,f(y,z)),f(u,f(1,f(x,f(y,y)))))=f(f(x,f(y,z)),1). given clause #347: (wt=15) 1901 [para_into,752,424] f(f(x,x),f(y,y))=f(f(1,y),f(1,x)). given clause #348: (wt=15) 1902 [para_into,752,409] f(f(x,x),f(1,y))=f(f(y,y),f(1,x)). given clause #349: (wt=15) 1908 [copy,1894,flip.1] f(f(1,x),f(1,y))=f(f(x,x),f(y,y)). given clause #350: (wt=15) 1909 [copy,1901,flip.1] f(f(1,x),f(1,y))=f(f(y,y),f(x,x)). given clause #351: (wt=17) 1654 [para_into,134,44] f(f(x,x),f(y,f(1,f(z,f(f(x,u),1)))))=x. given clause #352: (wt=15) 1925 [para_from,752,134,demod,4] f(x,f(y,f(1,f(z,f(1,x)))))=f(x,x). given clause #353: (wt=15) 1957 [para_into,874,749] f(f(f(1,x),y),f(1,f(f(x,x),y)))=1. given clause #354: (wt=15) 2019 [para_into,164,296,demod,88,50,flip.1] f(f(x,f(1,f(f(y,1),z))),y)=f(y,y). given clause #355: (wt=15) 2043 [para_from,164,731] f(f(x,f(f(y,1),z)),f(1,f(x,y)))=1. given clause #356: (wt=19) 1676 [para_from,134,269] f(x,f(1,f(y,f(1,f(x,z)))))=f(y,f(1,f(x,z))). given clause #357: (wt=15) 2045 [para_from,164,198] f(f(x,f(f(y,1),z)),f(f(x,y),1))=1. given clause #358: (wt=15) 2087 [para_into,932,752] f(f(x,x),f(1,y))=f(f(1,x),f(y,y)). given clause #359: (wt=15) 2090 [copy,2087,flip.1] f(f(1,x),f(y,y))=f(f(x,x),f(1,y)). given clause #360: (wt=15) 2093 [para_from,932,55] f(f(1,A),f(f(f(B,A),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #361: (wt=15) 2102 [para_into,935,424] f(f(1,x),f(y,y))=f(f(1,y),f(x,x)). given clause #362: (wt=15) 2110 [back_demod,1363,demod,2108] f(x,f(f(1,y),z))=f(f(z,f(y,y)),x). given clause #363: (wt=15) 2111 [back_demod,1360,demod,2108] f(f(x,f(y,y)),z)=f(z,f(f(1,y),x)). given clause #364: (wt=15) 2126 [back_demod,1356,demod,2113,30] f(x,f(1,f(y,f(f(z,f(x,y)),1))))=1. given clause #365: (wt=15) 2128 [back_demod,1294,demod,2113,30] f(x,f(1,f(y,f(f(f(x,y),z),1))))=1. given clause #366: (wt=15) 2134 [back_demod,960,demod,2113] f(f(x,f(1,f(y,f(z,z)))),z)=f(1,z). given clause #367: (wt=15) 2138 [back_demod,1592,demod,2116] f(x,f(1,f(f(f(y,z),x),f(z,z))))=1. given clause #368: (wt=15) 2140 [back_demod,1488,demod,2116] f(x,f(1,f(f(x,f(y,z)),f(y,y))))=1. given clause #369: (wt=15) 2148 [back_demod,1010,demod,2116] f(f(f(x,y),z),f(1,f(z,f(y,y))))=1. given clause #370: (wt=15) 2152 [back_demod,919,demod,2116] f(x,f(1,f(f(f(y,z),x),f(y,y))))=1. given clause #371: (wt=17) 2150 [back_demod,1006,demod,2116] f(f(x,y),f(1,f(z,f(y,y))))=f(z,f(y,y)). given clause #372: (wt=15) 2158 [back_demod,1846,demod,2147] f(x,f(1,f(y,f(1,f(z,f(x,x))))))=1. given clause #373: (wt=15) 2211 [para_from,176,117,demod,177] f(f(x,f(y,1)),f(1,f(y,z)))=f(y,z). given clause #374: (wt=15) 2238 [para_from,1263,487] f(f(1,x),f(1,f(y,f(f(x,x),y))))=1. given clause #375: (wt=15) 2271 [para_into,178,745,demod,2113,30,104,2113,30,flip.1] f(f(x,x),f(1,f(y,f(f(z,x),1))))=1. given clause #376: (wt=17) 2154 [back_demod,591,demod,2116] f(f(x,y),f(1,f(z,f(x,x))))=f(z,f(x,x)). given clause #377: (wt=15) 2279 [para_into,178,683,demod,2113,30,104,2113,30,flip.1] f(f(1,x),f(1,f(y,f(f(z,x),1))))=1. given clause #378: (wt=15) 2288 [para_into,178,487,demod,2113,30,104,2113,30,flip.1] f(x,f(1,f(y,f(f(z,f(x,z)),1))))=1. given clause #379: (wt=15) 2290 [para_into,178,477,demod,2113,30,104,2113,30,flip.1] f(x,f(1,f(y,f(f(f(z,x),z),1))))=1. given clause #380: (wt=15) 2292 [para_into,178,473,demod,104,2147,30,flip.1] f(x,f(1,f(y,f(f(z,f(z,x)),1))))=1. given clause #381: (wt=21) 2164 [back_demod,1795,demod,2147,30] f(f(x,f(1,f(y,f(f(z,u),1)))),f(u,z))=f(f(z,u),1). given clause #382: (wt=15) 2315 [para_into,178,296,demod,88,175,flip.1] f(f(x,f(1,y)),f(f(y,z),1))=f(y,z). given clause #383: (wt=15) 2320 [para_into,178,250,demod,88,175,flip.1] f(f(f(1,x),y),f(f(x,z),1))=f(x,z). given clause #384: (wt=15) 2325 [para_into,178,172,demod,48,175,flip.1] f(f(f(x,1),y),f(f(x,z),1))=f(x,z). given clause #385: (wt=15) 2329 [para_into,178,154,demod,2113,30,104,2113,30,flip.1] f(x,f(1,f(y,f(f(f(x,z),z),1))))=1. given clause #386: (wt=17) 2170 [back_demod,1352,demod,2147,30] f(f(x,f(1,f(y,f(f(z,u),1)))),f(z,z))=z. given clause #387: (wt=15) 2345 [para_into,178,82,demod,16,175,flip.1] f(f(f(x,x),y),f(f(x,z),1))=f(x,z). given clause #388: (wt=15) 2386 [para_from,178,731] f(f(x,y),f(1,f(x,f(f(y,z),1))))=1. given clause #389: (wt=15) 2416 [para_into,1334,134] f(f(1,x),f(1,f(y,f(1,f(x,z)))))=1. given clause #390: (wt=15) 2434 [para_from,1452,96,demod,104,2116,flip.1] f(x,f(1,f(f(x,f(y,z)),f(z,z))))=1. given clause #391: (wt=21) 2176 [back_demod,236,demod,2147,30] f(f(x,y),f(z,f(1,f(u,f(f(y,x),1)))))=f(f(y,x),1). given clause #392: (wt=15) 2542 [para_into,284,328,demod,104,2147,100,flip.1] f(f(f(x,1),y),1)=f(1,f(y,f(x,x))). given clause #393: (wt=15) 2548 [para_into,284,269] f(f(x,f(y,1)),f(1,f(z,y)))=f(z,y). given clause #394: (wt=15) 2560 [para_into,284,92] f(f(x,f(y,y)),f(1,f(y,z)))=f(y,z). given clause #395: (wt=15) 2621 [back_demod,1776,demod,2577] f(x,f(1,f(y,f(1,f(z,f(1,x))))))=1. given clause #396: (wt=19) 2203 [para_from,176,107,demod,2116] f(f(1,x),f(f(y,z),1))=f(y,f(1,f(z,f(x,x)))). given clause #397: (wt=15) 2646 [back_demod,351,demod,2577] f(f(x,f(1,f(y,f(1,z)))),z)=f(z,z). given clause #398: (wt=15) 2662 [back_demod,2232,demod,2620] f(x,f(1,f(y,f(1,f(f(y,x),z)))))=1. given clause #399: (wt=15) 2664 [back_demod,2219,demod,2620] f(x,f(1,f(y,f(1,f(z,f(x,1))))))=1. given clause #400: (wt=15) 2674 [back_demod,1230,demod,2620] f(x,f(1,f(y,f(1,f(z,f(y,x))))))=1. given clause #401: (wt=19) 2204 [para_from,176,56,demod,2116] f(f(x,1),f(f(y,z),1))=f(y,f(1,f(z,f(x,x)))). given clause #402: (wt=15) 2682 [back_demod,2440,demod,2639] f(x,f(1,f(f(x,y),f(1,f(z,y)))))=1. given clause #403: (wt=15) 2684 [back_demod,2436,demod,2639] f(x,f(1,f(f(x,y),f(1,f(y,z)))))=1. given clause #404: (wt=15) 2697 [back_demod,2327,demod,2639] f(f(x,y),f(1,f(y,f(1,f(x,z)))))=1. given clause #405: (wt=15) 2701 [back_demod,2311,demod,2639] f(f(x,x),f(1,f(y,f(1,f(x,z)))))=1. given clause #406: (wt=17) 2217 [para_from,176,269] f(f(x,y),f(1,f(z,f(x,1))))=f(z,f(x,1)). given clause #407: (wt=15) 2703 [back_demod,2294,demod,2639] f(f(x,y),f(1,f(x,f(1,f(y,z)))))=1. given clause #408: (wt=15) 2705 [back_demod,2286,demod,2639] f(x,f(1,f(f(y,x),f(1,f(y,z)))))=1. given clause #409: (wt=15) 2718 [back_demod,1929,demod,2639,1677] f(f(x,f(1,y)),f(1,f(z,y)))=f(z,y). given clause #410: (wt=15) 2720 [back_demod,1596,demod,2639] f(x,f(1,f(f(y,x),f(1,f(z,y)))))=1. given clause #411: (wt=19) 2223 [copy,2203,flip.1] f(x,f(1,f(y,f(z,z))))=f(f(1,z),f(f(x,y),1)). given clause #412: (wt=15) 2722 [back_demod,1462,demod,2639] f(f(x,y),f(1,f(x,f(1,f(z,y)))))=1. given clause #413: (wt=15) 2730 [back_demod,1168,demod,2639] f(f(x,x),f(1,f(y,f(1,f(z,x)))))=1. given clause #414: (wt=15) 2732 [back_demod,1158,demod,2639] f(f(x,y),f(1,f(z,f(1,f(y,x)))))=1. given clause #415: (wt=15) 2734 [back_demod,931,demod,2639,1677] f(x,f(f(y,z),1))=f(z,f(1,f(y,x))). given clause #416: (wt=19) 2224 [copy,2204,flip.1] f(x,f(1,f(y,f(z,z))))=f(f(z,1),f(f(x,y),1)). given clause #417: (wt=15) 2735 [back_demod,909,demod,2639,1677] f(x,f(1,f(y,z)))=f(z,f(f(y,x),1)). given clause #418: (wt=15) 2736 [back_demod,605,demod,2639,1677] f(f(f(1,x),y),f(1,f(z,x)))=f(z,x). given clause #419: (wt=15) 2738 [back_demod,573,demod,2639] f(f(x,y),f(1,f(y,f(1,f(z,x)))))=1. given clause #420: (wt=15) 2885 [back_demod,1502,demod,2840] f(f(x,f(1,f(y,f(z,1)))),z)=f(z,z). given clause #421: (wt=21) 2333 [para_into,178,141,demod,175,2147,flip.1] f(f(x,f(f(y,z),1)),f(1,f(u,f(y,y))))=f(f(y,1),u). given clause #422: (wt=15) 2925 [back_demod,1019,demod,2840] f(f(x,f(y,z)),f(1,f(x,f(z,1))))=1. given clause #423: (wt=15) 2929 [back_demod,936,demod,2840] f(f(f(x,y),z),f(1,f(z,f(x,1))))=1. given clause #424: (wt=15) 2937 [back_demod,677,demod,2840] f(f(x,f(y,z)),f(1,f(x,f(y,1))))=1. given clause #425: (wt=15) 2997 [para_into,966,1272,demod,4] f(f(x,f(1,f(f(1,y),z))),y)=f(y,y). given clause #426: (wt=17) 2382 [para_from,178,267] f(f(x,f(f(y,z),1)),f(x,y))=f(f(x,y),1). given clause #427: (wt=15) 2999 [para_into,966,1263,demod,30,88] f(f(x,f(1,f(f(y,y),z))),y)=f(1,y). given clause #428: (wt=15) 3368 [para_from,1070,453] f(f(1,x),f(1,f(y,f(1,f(z,x)))))=1. given clause #429: (wt=15) 3402 [back_demod,2677,demod,3363] f(x,f(1,f(y,z)))=f(y,f(f(z,x),1)). given clause #430: (wt=15) 3403 [back_demod,2676,demod,3363] f(x,f(f(y,z),1))=f(z,f(1,f(x,y))). given clause #431: (wt=17) 2390 [para_from,178,130] f(f(x,y),f(x,f(f(y,z),1)))=f(f(x,y),1). given clause #432: (wt=15) 3414 [para_into,197,60] f(x,f(1,f(y,z)))=f(z,f(f(x,y),1)). given clause #433: (wt=15) 3423 [para_into,197,968,demod,76,2113,30,flip.1] f(x,f(1,f(y,f(f(z,f(y,x)),1))))=1. given clause #434: (wt=15) 3431 [para_into,197,457,demod,2113,30,flip.1] f(x,f(1,f(y,f(f(f(y,x),z),1))))=1. given clause #435: (wt=15) 3440 [para_into,197,44] f(x,f(f(y,z),1))=f(z,f(f(y,x),1)). given clause #436: (wt=17) 2544 [para_into,284,296,demod,88] f(f(x,y),f(1,f(z,f(1,y))))=f(z,f(1,y)). given clause #437: (wt=15) 3446 [copy,3414,flip.1] f(x,f(f(y,z),1))=f(y,f(1,f(z,x))). given clause #438: (wt=15) 3464 [para_from,197,731] f(f(x,y),f(1,f(y,f(f(z,x),1))))=1. given clause #439: (wt=15) 3784 [para_into,202,191,demod,76,3783,flip.1] f(x,f(1,f(y,f(1,f(f(x,y),z)))))=1. given clause #440: (wt=15) 3792 [para_into,202,79,demod,3783,100,2639,2620,118,1677,114,flip.1] f(f(1,f(x,y)),z)=f(y,f(1,f(x,z))). given clause #441: (wt=23) 2546 [para_into,284,284] f(f(x,f(y,1)),f(1,f(z,f(f(y,u),1))))=f(z,f(f(y,u),1)). given clause #442: (wt=15) 3894 [back_demod,1096,demod,3783] f(f(x,1),f(1,f(y,f(1,f(z,x)))))=1. given clause #443: (wt=15) 3903 [back_demod,203,demod,3783] f(x,f(1,f(y,f(1,f(z,f(x,y))))))=1. given clause #444: (wt=15) 3909 [back_demod,3595,demod,3793,3793,3793,786,3793] f(x,f(1,f(y,z)))=f(y,f(1,f(z,x))). given clause #445: (wt=15) 3910 [back_demod,3591,demod,3793,3793,50,81,3793,3793] f(x,f(1,f(y,z)))=f(z,f(1,f(y,x))). given clause #446: (wt=17) 2550 [para_into,284,267,demod,48] f(f(x,y),f(1,f(z,f(y,1))))=f(z,f(y,1)). given clause #447: (wt=15) 3912 [back_demod,3579,demod,3793] f(x,f(1,f(y,f(z,f(1,x)))))=f(y,x). given clause #448: (wt=15) 3918 [back_demod,3548,demod,3793] f(x,f(1,f(y,f(z,f(x,y)))))=f(y,x). given clause #449: (wt=15) 3921 [back_demod,3370,demod,3793,3793,3363] f(x,f(1,f(y,z)))=f(y,f(1,f(x,z))). given clause #450: (wt=15) 3932 [back_demod,3276,demod,3793,2620,3913,3793] f(x,f(1,f(y,z)))=f(z,f(1,f(x,y))). given clause #451: (wt=17) 2552 [para_into,284,250,demod,88] f(f(x,y),f(1,f(f(1,y),z)))=f(f(1,y),z). given clause #452: (wt=15) 3972 [back_demod,2945,demod,3793] f(f(x,1),f(1,f(y,f(y,f(x,z)))))=1. given clause #453: (wt=15) 3976 [back_demod,2919,demod,3793] f(f(x,1),f(1,f(y,f(y,f(z,x)))))=1. given clause #454: (wt=15) 3978 [back_demod,2917,demod,3793] f(f(x,1),f(1,f(y,f(f(x,z),y))))=1. given clause #455: (wt=15) 4004 [back_demod,2456,demod,3793] f(x,f(1,f(f(x,y),f(f(z,y),1))))=1. given clause #456: (wt=17) 2554 [para_into,284,172,demod,48] f(f(x,y),f(1,f(f(y,1),z)))=f(f(y,1),z). given clause #457: (wt=15) 4006 [back_demod,2454,demod,3793] f(x,f(1,f(f(x,y),f(f(y,z),1))))=1. given clause #458: (wt=15) 4008 [back_demod,2378,demod,3793,2620] f(x,f(1,f(y,f(1,f(z,f(z,x))))))=1. given clause #459: (wt=15) 4010 [back_demod,2284,demod,3793] f(x,f(1,f(f(y,x),f(f(y,z),1))))=1. given clause #460: (wt=15) 4014 [back_demod,2033,demod,3793] f(x,f(1,f(y,f(y,f(f(x,1),z)))))=1. given clause #461: (wt=17) 2556 [para_into,284,82,demod,16] f(f(x,y),f(1,f(f(y,y),z)))=f(f(y,y),z). given clause #462: (wt=15) 4016 [back_demod,2021,demod,3793] f(f(f(x,1),y),f(1,f(z,x)))=f(z,x). given clause #463: (wt=15) 4018 [back_demod,2005,demod,3793] f(x,f(1,f(f(f(f(y,1),z),x),y)))=1. given clause #464: (wt=15) 4020 [back_demod,1638,demod,3793] f(x,f(1,f(f(y,x),f(f(z,y),1))))=1. given clause #465: (wt=15) 4024 [back_demod,1330,demod,3793] f(f(x,x),f(1,f(y,f(f(x,z),y))))=1. given clause #466: (wt=19) 2580 [para_into,182,656,demod,2543,2116,275,2577] f(x,f(1,f(y,f(z,z))))=f(x,f(1,f(y,f(1,z)))). given clause #467: (wt=15) 4026 [back_demod,1328,demod,3793] f(f(x,x),f(1,f(y,f(y,f(z,x)))))=1. given clause #468: (wt=15) 4031 [back_demod,621,demod,3793] f(f(x,x),f(1,f(y,f(y,f(x,z)))))=1. given clause #469: (wt=15) 4229 [para_from,214,168,demod,3793,118,114,30,88] f(f(x,f(y,z)),f(1,f(z,y)))=f(z,y). given clause #470: (wt=15) 4262 [para_from,214,82,demod,3793,118,114,30,88] f(f(f(x,y),z),f(1,f(y,x)))=f(y,x). given clause #471: (wt=21) 2605 [back_demod,2335,demod,2577] f(f(x,f(f(y,z),1)),f(1,f(u,f(1,y))))=f(f(y,y),u). given clause #472: (wt=15) 4264 [para_from,214,13,demod,3793,118,114,3793,30,88] f(x,f(1,f(y,f(f(x,y),z))))=f(y,x). given clause #473: (wt=15) 4291 [para_into,1412,96] f(f(x,f(y,y)),f(1,f(z,y)))=f(z,y). given clause #474: (wt=15) 4313 [para_into,1670,170] f(f(x,f(1,y)),f(1,f(y,z)))=f(y,z). given clause #475: (wt=15) 4379 [para_from,217,34,demod,3783,3363,flip.1] f(f(f(x,y),1),z)=f(y,f(1,f(x,z))). given clause #476: (wt=19) 2648 [copy,2580,flip.1] f(x,f(1,f(y,f(1,z))))=f(x,f(1,f(y,f(z,z)))). given clause #477: (wt=15) 4456 [back_demod,3455,demod,4380,4380] f(x,f(1,f(y,f(1,f(z,f(x,z))))))=1. given clause #478: (wt=15) 4495 [back_demod,2009,demod,4380] f(x,f(1,f(f(x,f(f(y,1),z)),y)))=1. given clause #479: (wt=15) 4497 [back_demod,2007,demod,4380] f(f(f(f(x,1),y),z),f(1,f(z,x)))=1. given clause #480: (wt=15) 4589 [para_into,219,296,demod,76,76,flip.1] f(x,f(f(y,f(z,f(x,y))),1))=f(x,y). given clause #481: (wt=19) 2651 [copy,2602,flip.1,demod,2639,2155] f(x,f(1,f(y,f(z,z))))=f(y,f(1,f(x,f(1,z)))). given clause #482: (wt=15) 4591 [para_into,219,250,demod,76,76,flip.1] f(x,f(f(y,f(f(x,y),z)),1))=f(x,y). given clause #483: (wt=15) 4646 [para_into,222,1178,demod,104,flip.1] f(x,f(1,f(y,f(1,f(f(x,x),z)))))=1. given clause #484: (wt=15) 4648 [para_into,222,1176,demod,104,flip.1] f(x,f(1,f(y,f(1,f(f(x,1),z)))))=1. given clause #485: (wt=15) 4650 [para_into,222,1174,demod,104,flip.1] f(x,f(1,f(y,f(1,f(f(1,x),z)))))=1. given clause #486: (wt=19) 2654 [copy,2614,flip.1,demod,2639,2155] f(x,f(1,f(y,f(1,z))))=f(y,f(1,f(x,f(z,z)))). given clause #487: (wt=15) 4653 [para_into,222,477,demod,104,flip.1] f(x,f(1,f(y,f(1,f(f(z,x),z)))))=1. given clause #488: (wt=15) 4661 [para_into,222,154,demod,104,flip.1] f(x,f(1,f(y,f(1,f(f(x,z),z)))))=1. given clause #489: (wt=15) 4676 [para_into,222,82,demod,16,flip.1] f(f(f(x,x),y),f(1,f(z,x)))=f(z,x). given clause #490: (wt=15) 4690 [para_into,222,296,demod,76,76,flip.1] f(x,f(1,f(f(y,f(x,z)),z)))=f(x,z). given clause #491: (wt=19) 2686 [back_demod,2430,demod,2639] f(x,f(1,f(f(y,f(f(x,z),1)),f(1,f(y,z)))))=1. given clause #492: (wt=15) 4693 [para_into,222,250,demod,76,76,flip.1] f(x,f(1,f(f(f(x,y),z),y)))=f(x,y). given clause #493: (wt=15) 4813 [para_into,252,213,demod,30,4380] f(x,f(1,f(f(f(y,x),z),y)))=f(y,x). given clause #494: (wt=15) 4815 [para_into,252,197] f(x,f(f(y,f(f(y,x),z)),1))=f(y,x). given clause #495: (wt=15) 4825 [para_from,252,731] f(f(f(f(x,y),z),y),f(1,f(x,y)))=1. given clause #496: (wt=19) 2688 [back_demod,2375,demod,2639,1677] f(f(x,x),f(f(y,z),1))=f(z,f(1,f(y,f(x,1)))). given clause #497: (wt=15) 4827 [para_from,252,198] f(f(f(f(x,y),z),y),f(f(x,y),1))=1. given clause #498: (wt=15) 4911 [para_into,306,213,demod,30,4380] f(x,f(1,f(f(y,f(z,x)),z)))=f(z,x). given clause #499: (wt=15) 4923 [para_from,306,731] f(f(f(x,f(y,z)),z),f(1,f(y,z)))=1. given clause #500: (wt=15) 4925 [para_from,306,198] f(f(f(x,f(y,z)),z),f(f(y,z),1))=1. given clause #501: (wt=19) 2689 [back_demod,2374,demod,2639,1677] f(f(x,1),f(f(y,z),1))=f(z,f(1,f(y,f(x,x)))). given clause #502: (wt=15) 4963 [para_into,340,60] f(f(f(f(A,B),f(C,A)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #503: (wt=15) 4964 [para_into,340,60] f(f(f(f(A,C),f(A,B)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #504: (wt=15) 4965 [para_into,340,60] f(f(D,f(f(A,B),f(A,C))),f(A,A))!=A|$Ans(OL_Sh). given clause #505: (wt=15) 4966 [para_into,340,79] f(f(f(f(A,B),f(A,C)),D),f(1,A))!=A|$Ans(OL_Sh). given clause #506: (wt=19) 2690 [back_demod,2370,demod,2639,1677] f(f(x,x),f(f(y,z),1))=f(z,f(1,f(y,f(1,x)))). given clause #507: (wt=15) 4967 [para_into,340,31] f(f(f(f(A,B),f(A,C)),D),f(A,1))!=A|$Ans(OL_Sh). given clause #508: (wt=15) 4968 [para_into,340,932] f(f(1,A),f(f(f(A,B),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #509: (wt=15) 4969 [para_into,340,290] f(f(A,1),f(f(f(A,B),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #510: (wt=15) 4970 [para_into,340,60] f(f(A,A),f(f(f(A,B),f(A,C)),D))!=A|$Ans(OL_Sh). given clause #511: (wt=19) 2691 [back_demod,2369,demod,2639,1677] f(f(1,x),f(f(y,z),1))=f(z,f(1,f(y,f(x,x)))). given clause #512: (wt=15) 5039 [para_into,341,60] f(f(f(f(C,A),f(B,A)),D),f(A,A))!=A|$Ans(OL_Sh). given clause #513: (wt=15) 5040 [para_into,341,60] f(f(D,f(f(B,A),f(C,A))),f(A,A))!=A|$Ans(OL_Sh). given clause #514: (wt=15) 5041 [para_into,341,79] f(f(f(f(B,A),f(C,A)),D),f(1,A))!=A|$Ans(OL_Sh). given clause #515: (wt=15) 5042 [para_into,341,31] f(f(f(f(B,A),f(C,A)),D),f(A,1))!=A|$Ans(OL_Sh). given clause #516: (wt=19) 2699 [back_demod,2322,demod,2639,1677] f(x,f(1,f(y,f(z,1))))=f(f(z,z),f(f(y,x),1)). given clause #517: (wt=15) 5043 [para_into,341,932] f(f(1,A),f(f(f(B,A),f(C,A)),D))!=A|$Ans(OL_Sh). given clause #518: (wt=15) 5044 [para_into,341,290] f(f(A,1),f(f(f(B,A),f(C,A)),D))!=A|$Ans(OL_Sh). given clause #519: (wt=15) 5045 [para_into,341,60] f(f(A,A),f(f(f(B,A),f(C,A)),D))!=A|$Ans(OL_Sh). given clause #520: (wt=15) 5046 [para_into,342,60] f(f(D,f(f(A,C),f(B,A))),f(A,A))!=A|$Ans(OL_Sh). given clause #521: (wt=19) 2700 [back_demod,2317,demod,2639,1677] f(x,f(1,f(y,f(z,z))))=f(f(z,1),f(f(y,x),1)). given clause #522: (wt=15) 5047 [para_into,342,79] f(f(f(f(A,C),f(B,A)),D),f(1,A))!=A|$Ans(OL_Sh). given clause #523: (wt=15) 5048 [para_into,342,31] f(f(f(f(A,C),f(B,A)),D),f(A,1))!=A|$Ans(OL_Sh). given clause #524: (wt=15) 5049 [para_into,342,932] f(f(1,A),f(f(f(A,C),f(B,A)),D))!=A|$Ans(OL_Sh). given clause #525: (wt=15) 5050 [para_into,342,290] f(f(A,1),f(f(f(A,C),f(B,A)),D))!=A|$Ans(OL_Sh). given clause #526: (wt=19) 2707 [back_demod,2269,demod,2639,1677] f(x,f(1,f(y,f(1,z))))=f(f(z,z),f(f(y,x),1)). given clause #527: (wt=15) 5051 [para_into,342,60] f(f(A,A),f(f(f(A,C),f(B,A)),D))!=A|$Ans(OL_Sh). given clause #528: (wt=15) 5052 [para_into,343,79] f(f(D,f(f(B,A),f(A,C))),f(1,A))!=A|$Ans(OL_Sh). given clause #529: (wt=15) 5053 [para_into,343,31] f(f(D,f(f(B,A),f(A,C))),f(A,1))!=A|$Ans(OL_Sh). given clause #530: (wt=15) 5054 [para_into,343,932] f(f(1,A),f(D,f(f(B,A),f(A,C))))!=A|$Ans(OL_Sh). given clause #531: (wt=19) 2708 [back_demod,2266,demod,2639,1677] f(x,f(1,f(y,f(z,z))))=f(f(1,z),f(f(y,x),1)). given clause #532: (wt=15) 5055 [para_into,343,290] f(f(A,1),f(D,f(f(B,A),f(A,C))))!=A|$Ans(OL_Sh). given clause #533: (wt=15) 5056 [para_into,343,60] f(f(A,A),f(D,f(f(B,A),f(A,C))))!=A|$Ans(OL_Sh). given clause #534: (wt=15) 5112 [back_demod,4194,demod,5072,30] f(f(x,y),f(1,f(y,f(f(x,z),1))))=1. given clause #535: (wt=15) 5197 [para_from,232,107,demod,48] f(f(1,x),f(y,z))=f(f(z,y),f(x,x)). given clause #536: (wt=17) 2747 [para_from,182,284,demod,2543,30] f(f(x,f(1,f(y,f(f(z,u),1)))),f(1,z))=z. given clause #537: (wt=15) 5198 [para_from,232,56,demod,48] f(f(x,1),f(y,z))=f(f(z,y),f(x,x)). given clause #538: (wt=15) 5208 [copy,5197,flip.1] f(f(x,y),f(z,z))=f(f(1,z),f(y,x)). given clause #539: (wt=15) 5209 [copy,5198,flip.1] f(f(x,y),f(z,z))=f(f(z,1),f(y,x)). given clause #540: (wt=15) 5356 [para_into,385,219,demod,35,114,48] f(f(x,x),f(y,z))=f(f(z,y),f(x,1)). given clause #541: (wt=17) 2749 [para_from,182,141,demod,2543,30] f(f(x,f(1,f(y,f(f(z,u),1)))),f(z,1))=z. given clause #542: (wt=15) 5359 [copy,5356,flip.1] f(f(x,y),f(z,1))=f(f(z,z),f(y,x)). given clause #543: (wt=15) 5394 [para_into,420,1482,demod,104,3793,flip.1] f(f(x,f(f(y,y),z)),f(1,f(x,y)))=1. given clause #544: (wt=15) 5396 [para_into,420,487,demod,104,3793,flip.1] f(f(f(f(x,x),y),z),f(1,f(z,x)))=1. given clause #545: (wt=15) 5398 [para_into,420,477,demod,104,3793,flip.1] f(x,f(1,f(f(x,f(f(y,y),z)),y)))=1. given clause #546: (wt=17) 2753 [para_from,182,128,demod,2543,30] f(f(x,x),f(y,f(1,f(z,f(f(u,x),1)))))=x. given clause #547: (wt=15) 5406 [para_into,420,154,demod,104,3793,flip.1] f(x,f(1,f(f(f(f(y,y),z),x),y)))=1. given clause #548: (wt=15) 5426 [para_from,420,211,demod,30,48] f(f(f(f(x,x),y),z),f(f(z,x),1))=1. given clause #549: (wt=15) 5466 [para_from,422,211,demod,30,88] f(f(x,f(f(y,y),z)),f(f(x,y),1))=1. given clause #550: (wt=15) 5568 [para_into,530,1482,demod,104,3793,flip.1] f(f(x,f(y,f(z,z))),f(1,f(x,z)))=1. given clause #551: (wt=17) 2757 [para_from,182,123,demod,2543,30] f(f(x,1),f(y,f(1,f(z,f(f(x,u),1)))))=x. given clause #552: (wt=15) 5570 [para_into,530,487,demod,104,3793,flip.1] f(f(f(x,f(y,y)),z),f(1,f(z,y)))=1. given clause #553: (wt=15) 5572 [para_into,530,477,demod,104,3793,flip.1] f(x,f(1,f(f(x,f(y,f(z,z))),z)))=1. given clause #554: (wt=15) 5580 [para_into,530,154,demod,104,3793,flip.1] f(x,f(1,f(f(f(y,f(z,z)),x),z)))=1. given clause #555: (wt=15) 5600 [para_from,530,211,demod,30,48] f(f(f(x,f(y,y)),z),f(f(z,y),1))=1. given clause #556: (wt=17) 2759 [para_from,182,121,demod,2543,30] f(f(1,x),f(y,f(1,f(z,f(f(x,u),1)))))=x. given clause #557: (wt=15) 5640 [para_from,532,211,demod,30,88] f(f(x,f(y,f(z,z))),f(f(x,z),1))=1. given clause #558: (wt=15) 5812 [para_into,645,219,demod,48,35,114] f(f(x,y),f(f(f(z,f(y,x)),z),1))=1. given clause #559: (wt=15) 5834 [para_into,654,219,demod,48,35,114] f(x,f(1,f(f(y,z),f(x,f(z,y)))))=1. given clause #560: (wt=15) 5868 [para_into,657,219,demod,35,114,48] f(x,f(1,f(f(x,f(y,z)),f(z,y))))=1. given clause #561: (wt=19) 2830 [para_into,391,749,demod,2113] f(f(f(1,x),y),f(f(x,x),y))=f(1,f(y,f(x,x))). given clause #562: (wt=15) 5900 [para_into,304,932,demod,88,16] f(x,f(f(y,f(z,f(x,x))),1))=f(y,x). given clause #563: (wt=15) 5902 [para_into,304,1174,demod,100,48,5671,100] f(f(f(1,x),y),z)=f(z,f(y,f(x,x))). given clause #564: (wt=15) 5903 [para_into,304,731,demod,100,48,5666,100] f(f(x,f(y,1)),z)=f(z,f(x,f(y,y))). given clause #565: (wt=15) 5904 [para_into,304,693,demod,100,48,5669,100] f(f(x,f(1,y)),z)=f(z,f(x,f(y,y))). given clause #566: (wt=19) 2855 [back_demod,2751,demod,2840] f(x,f(y,f(1,f(z,f(1,f(u,f(x,1)))))))=f(x,x). given clause #567: (wt=15) 5917 [copy,5902,flip.1] f(x,f(y,f(z,z)))=f(f(f(1,z),y),x). given clause #568: (wt=15) 5918 [copy,5903,flip.1] f(x,f(y,f(z,z)))=f(f(y,f(z,1)),x). given clause #569: (wt=15) 5919 [copy,5904,flip.1] f(x,f(y,f(z,z)))=f(f(y,f(1,z)),x). given clause #570: (wt=15) 5942 [para_into,750,219,demod,35,114,48] f(f(x,y),f(f(f(f(y,x),z),z),1))=1. given clause #571: (wt=19) 2858 [back_demod,2709,demod,2840] f(x,f(1,f(f(y,y),z)))=f(z,f(1,f(x,f(y,1)))). given clause #572: (wt=15) 6038 [para_into,764,219,demod,48,35,114] f(x,f(1,f(f(y,z),f(f(z,y),x))))=1. given clause #573: (wt=15) 6073 [para_into,766,219,demod,35,114,48] f(x,f(1,f(f(f(y,z),x),f(z,y))))=1. given clause #574: (wt=15) 6121 [para_from,783,693] f(f(x,f(f(1,y),z)),f(1,f(x,y)))=1. given clause #575: (wt=15) 6131 [para_from,783,211,demod,30,88] f(f(x,f(f(1,y),z)),f(f(x,y),1))=1. given clause #576: (wt=19) 2860 [back_demod,2692,demod,2840] f(x,f(1,f(y,f(z,1))))=f(y,f(1,f(f(z,z),x))). given clause #577: (wt=15) 6241 [para_into,826,219,demod,35,114,48] f(f(x,y),f(z,z))=f(f(y,x),f(z,1)). given clause #578: (wt=15) 6242 [para_into,826,219,demod,35,114,48] f(f(x,x),f(y,z))=f(f(x,1),f(z,y)). given clause #579: (wt=15) 6243 [copy,6241,flip.1] f(f(x,y),f(z,1))=f(f(y,x),f(z,z)). given clause #580: (wt=15) 6244 [copy,6242,flip.1] f(f(x,1),f(y,z))=f(f(x,x),f(z,y)). given clause #581: (wt=21) 2871 [back_demod,1806,demod,2840] f(f(x,f(f(y,z),1)),f(1,f(u,f(y,1))))=f(u,f(y,1)). given clause #582: (wt=15) 6267 [para_into,841,219,demod,35,114,48] f(f(x,y),f(1,f(f(z,f(y,x)),z)))=1. given clause #583: (wt=15) 6341 [para_from,847,693] f(f(x,f(y,f(z,1))),f(1,f(x,z)))=1. given clause #584: (wt=15) 6351 [para_from,847,211,demod,30,88] f(f(x,f(y,f(z,1))),f(f(x,z),1))=1. given clause #585: (wt=15) 6381 [para_into,896,487,demod,104,3793,flip.1] f(f(f(f(1,x),y),z),f(1,f(z,x)))=1. given clause #586: (wt=23) 2891 [back_demod,1392,demod,2840] f(f(f(x,y),z),f(u,f(1,f(z,f(x,1)))))=f(f(f(x,y),z),1). given clause #587: (wt=15) 6383 [para_into,896,477,demod,104,3793,flip.1] f(x,f(1,f(f(x,f(f(1,y),z)),y)))=1. given clause #588: (wt=15) 6390 [para_into,896,154,demod,104,3793,flip.1] f(x,f(1,f(f(f(f(1,y),z),x),y)))=1. given clause #589: (wt=15) 6460 [para_into,904,487,demod,104,3793,flip.1] f(f(f(x,f(y,1)),z),f(1,f(z,y)))=1. given clause #590: (wt=15) 6462 [para_into,904,477,demod,104,3793,flip.1] f(x,f(1,f(f(x,f(y,f(z,1))),z)))=1. given clause #591: (wt=23) 2893 [back_demod,1390,demod,2840] f(f(x,f(y,z)),f(u,f(1,f(x,f(z,1)))))=f(f(x,f(y,z)),1). given clause #592: (wt=15) 6468 [para_into,904,154,demod,104,3793,flip.1] f(x,f(1,f(f(f(y,f(z,1)),x),z)))=1. given clause #593: (wt=15) 6631 [para_into,1074,1178,demod,6249,100] f(x,f(f(y,1),z))=f(x,f(f(y,y),z)). given clause #594: (wt=15) 6632 [para_into,1074,1176,demod,6262,100] f(x,f(f(y,y),z))=f(x,f(f(y,1),z)). given clause #595: (wt=15) 6633 [para_into,1074,1174,demod,5671,100] f(x,f(y,f(z,z)))=f(x,f(f(1,z),y)). given clause #596: (wt=23) 2941 [back_demod,627,demod,2840] f(f(x,f(y,z)),f(u,f(1,f(x,f(y,1)))))=f(f(x,f(y,z)),1). given clause #597: (wt=15) 6641 [para_into,1074,731,demod,5666,100] f(x,f(y,f(z,z)))=f(x,f(y,f(z,1))). given clause #598: (wt=15) 6642 [para_into,1074,693,demod,5669,100] f(x,f(y,f(z,z)))=f(x,f(y,f(1,z))). given clause #599: (wt=15) 6647 [copy,6633,flip.1] f(x,f(f(1,y),z))=f(x,f(z,f(y,y))). given clause #600: (wt=15) 6649 [copy,6641,flip.1] f(x,f(y,f(z,1)))=f(x,f(y,f(z,z))). given clause #601: (wt=23) 3023 [para_from,966,284] f(f(x,f(y,1)),f(1,f(z,f(1,f(y,u)))))=f(z,f(1,f(y,u))). given clause #602: (wt=15) 6650 [copy,6642,flip.1] f(x,f(y,f(1,z)))=f(x,f(y,f(z,z))). given clause #603: (wt=15) 6746 [para_into,1236,219,demod,35,114,48] f(f(x,x),f(y,z))=f(f(z,y),f(1,x)). given clause #604: (wt=15) 6750 [copy,6746,flip.1] f(f(x,y),f(1,z))=f(f(z,z),f(y,x)). given clause #605: (wt=15) 7086 [para_into,1426,752,demod,4] f(f(x,f(y,f(1,z))),f(1,f(x,z)))=1. given clause #606: (wt=21) 3029 [para_from,966,44,demod,2840,flip.1] f(f(x,f(1,f(y,z))),f(1,f(u,f(y,1))))=f(u,f(y,1)). given clause #607: (wt=15) 7116 [para_into,1426,964,demod,88] f(f(x,f(y,z)),f(1,f(x,f(1,y))))=1. given clause #608: (wt=15) 7144 [para_into,1426,932] f(f(x,f(y,z)),f(1,f(f(1,y),x)))=1. given clause #609: (wt=15) 7156 [para_into,1426,290] f(f(x,f(y,z)),f(1,f(f(y,1),x)))=1. given clause #610: (wt=15) 7164 [para_into,1426,60] f(f(x,f(y,z)),f(1,f(f(y,y),x)))=1. given clause #611: (wt=21) 3039 [para_into,184,923,demod,30,2113,30,924] f(f(x,y),f(x,f(1,f(z,f(f(y,u),1)))))=f(f(x,y),1). given clause #612: (wt=15) 7166 [para_into,1426,214,demod,2840] f(x,f(1,f(f(x,f(y,z)),f(y,1))))=1. given clause #613: (wt=15) 7206 [para_into,7152,932,demod,81] f(f(f(f(1,x),y),f(f(x,x),z)),x)=1. given clause #614: (wt=15) 7226 [para_into,7152,749,demod,100] f(f(f(f(x,x),y),f(f(1,x),z)),x)=1. given clause #615: (wt=15) 7232 [para_into,7152,424,demod,100] f(f(f(x,f(y,y)),f(f(1,y),z)),y)=1. given clause #616: (wt=25) 3064 [para_into,184,1272,demod,2769] f(f(f(1,x),f(y,z)),f(f(x,x),f(y,y)))=f(1,f(f(y,z),f(1,x))). given clause #617: (wt=15) 7236 [para_into,7152,409,demod,81] f(f(f(x,f(1,y)),f(f(y,y),z)),y)=1. given clause #618: (wt=15) 7242 [para_into,7152,290,demod,81] f(f(f(f(x,1),y),f(f(x,x),z)),x)=1. given clause #619: (wt=15) 7250 [para_into,7152,218,demod,81] f(f(f(x,f(y,1)),f(f(y,y),z)),y)=1. given clause #620: (wt=15) 7254 [para_into,7152,213,demod,76] f(f(f(f(x,x),y),f(f(x,1),z)),x)=1. given clause #621: (wt=25) 3066 [para_into,184,1263,demod,2113] f(f(f(x,x),f(y,z)),f(f(1,x),f(y,y)))=f(1,f(f(y,z),f(x,x))). given clause #622: (wt=15) 7258 [para_into,7152,190,demod,76] f(f(f(x,f(y,y)),f(f(y,1),z)),y)=1. given clause #623: (wt=15) 7262 [para_into,7152,180] f(f(x,f(f(y,x),z)),f(1,f(y,x)))=1. given clause #624: (wt=15) 7266 [para_into,7152,111] f(f(x,f(f(x,y),z)),f(1,f(x,y)))=1. given clause #625: (wt=15) 7302 [para_into,7152,935,demod,100] f(f(f(x,f(1,y)),f(z,f(y,y))),y)=1. given clause #626: (wt=25) 3068 [para_into,184,935,demod,2113] f(f(f(x,y),f(z,z)),f(f(1,z),f(x,x)))=f(1,f(f(x,y),f(z,z))). given clause #627: (wt=15) 7308 [para_into,7152,798,demod,81] f(f(f(x,f(y,y)),f(z,f(y,y))),y)=1. given clause #628: (wt=15) 7310 [para_into,7152,752,demod,81] f(f(f(x,f(y,y)),f(z,f(1,y))),y)=1. given clause #629: (wt=15) 7320 [para_into,7152,379,demod,76] f(f(f(x,f(y,1)),f(z,f(y,y))),y)=1. given clause #630: (wt=15) 7328 [para_into,7152,304,demod,100] f(f(f(x,f(1,y)),f(z,f(y,1))),y)=1. given clause #631: (wt=25) 3070 [para_into,184,752,demod,2769] f(f(f(x,y),f(1,z)),f(f(z,z),f(x,x)))=f(1,f(f(x,y),f(1,z))). given clause #632: (wt=15) 7332 [para_into,7152,260,demod,76] f(f(f(x,f(y,1)),f(z,f(y,1))),y)=1. given clause #633: (wt=15) 7336 [para_into,7152,221,demod,81] f(f(f(x,f(y,y)),f(z,f(y,1))),y)=1. given clause #634: (wt=15) 7342 [para_into,7152,170] f(f(f(x,f(y,z)),y),f(1,f(y,z)))=1. given clause #635: (wt=15) 7346 [para_into,7152,932,demod,88] f(f(f(x,f(y,y)),f(f(y,y),z)),y)=1. given clause #636: (wt=25) 3072 [para_into,184,669,demod,2543] f(f(f(x,x),f(y,z)),f(f(x,1),f(y,y)))=f(1,f(f(y,z),f(x,x))). given clause #637: (wt=15) 7350 [para_into,7152,749,demod,16] f(f(f(x,f(1,y)),f(f(1,y),z)),y)=1. given clause #638: (wt=15) 7356 [para_into,7152,213,demod,16] f(f(f(x,f(y,1)),f(f(y,1),z)),y)=1. given clause #639: (wt=15) 7396 [para_into,7158,304,demod,100] f(f(f(x,f(y,1)),f(f(1,y),z)),y)=1. given clause #640: (wt=15) 7428 [para_into,7158,935,demod,100] f(f(f(f(1,x),y),f(z,f(x,x))),x)=1. given clause #641: (wt=25) 3074 [para_into,184,656,demod,2769] f(f(f(x,1),f(y,z)),f(f(x,x),f(y,y)))=f(1,f(f(y,z),f(1,x))). given clause #642: (wt=15) 7430 [para_into,7158,798,demod,81] f(f(f(f(x,x),y),f(z,f(x,x))),x)=1. given clause #643: (wt=15) 7432 [para_into,7158,752,demod,81] f(f(f(f(x,x),y),f(z,f(1,x))),x)=1. given clause #644: (wt=15) 7442 [para_into,7158,379,demod,76] f(f(f(f(x,1),y),f(z,f(x,x))),x)=1. given clause #645: (wt=15) 7450 [para_into,7158,304,demod,100] f(f(f(f(1,x),y),f(z,f(x,1))),x)=1. given clause #646: (wt=25) 3076 [para_into,184,291,demod,2543] f(f(f(x,y),f(z,z)),f(f(z,1),f(x,x)))=f(1,f(f(x,y),f(z,z))). given clause #647: (wt=15) 7454 [para_into,7158,260,demod,76] f(f(f(f(x,1),y),f(z,f(x,1))),x)=1. given clause #648: (wt=15) 7458 [para_into,7158,221,demod,81] f(f(f(f(x,x),y),f(z,f(x,1))),x)=1. given clause #649: (wt=15) 7464 [para_into,7158,170] f(f(f(f(x,y),z),x),f(1,f(x,y)))=1. given clause #650: (wt=15) 7466 [para_into,7158,932,demod,88] f(f(f(f(x,x),y),f(f(x,x),z)),x)=1. given clause #651: (wt=25) 3078 [para_into,184,221,demod,2769] f(f(f(x,y),f(z,1)),f(f(z,z),f(x,x)))=f(1,f(f(x,y),f(1,z))). given clause #652: (wt=15) 7470 [para_into,7158,749,demod,16] f(f(f(f(1,x),y),f(f(1,x),z)),x)=1. given clause #653: (wt=15) 7474 [para_into,7158,213,demod,16] f(f(f(f(x,1),y),f(f(x,1),z)),x)=1. given clause #654: (wt=15) 7551 [para_into,7306,180] f(f(x,f(y,f(z,x))),f(1,f(z,x)))=1. given clause #655: (wt=15) 7555 [para_into,7306,111] f(f(x,f(y,f(x,z))),f(1,f(x,z)))=1. given clause #656: (wt=19) 3082 [para_into,184,119,demod,2116,68,120] f(f(x,f(y,z)),f(x,f(1,y)))=f(f(x,f(y,z)),1). given clause #657: (wt=15) 7615 [para_into,7306,749,demod,16] f(f(f(x,f(1,y)),f(z,f(1,y))),y)=1. given clause #658: (wt=15) 7657 [para_into,7344,304,demod,100] f(f(f(x,f(y,1)),f(z,f(1,y))),y)=1. given clause #659: (wt=15) 7699 [para_into,7344,749,demod,16] f(f(f(f(1,x),y),f(z,f(1,x))),x)=1. given clause #660: (wt=15) 7735 [para_into,7348,180] f(f(x,f(f(y,x),z)),f(f(y,x),1))=1. given clause #661: (wt=19) 3087 [para_into,184,31] f(f(x,f(y,z)),f(x,f(y,1)))=f(f(x,f(y,z)),1). given clause #662: (wt=15) 7739 [para_into,7348,111] f(f(x,f(f(x,y),z)),f(f(x,y),1))=1. given clause #663: (wt=15) 7779 [para_into,7348,170] f(f(f(x,f(y,z)),y),f(f(y,z),1))=1. given clause #664: (wt=15) 7835 [para_into,7362,1272,demod,167] f(x,f(f(y,f(x,x)),f(f(x,x),z)))=1. given clause #665: (wt=15) 7837 [para_into,7362,1263,demod,95] f(x,f(f(y,f(1,x)),f(f(1,x),z)))=1. given clause #666: (wt=25) 3089 [para_into,184,935,demod,2113] f(f(f(1,x),f(y,z)),f(f(y,y),f(x,x)))=f(1,f(f(y,z),f(x,x))). given clause #667: (wt=15) 7839 [para_into,7362,836,demod,4] f(x,f(f(y,f(x,1)),f(f(x,1),z)))=1. given clause #668: (wt=15) 7881 [para_into,7362,932,demod,4] f(x,f(f(f(1,x),y),f(f(x,x),z)))=1. given clause #669: (wt=15) 7897 [para_into,7362,749,demod,30,88] f(x,f(f(f(x,x),y),f(f(1,x),z)))=1. given clause #670: (wt=15) 7905 [para_into,7362,424,demod,30,88] f(x,f(f(y,f(x,x)),f(f(1,x),z)))=1. given clause #671: (wt=19) 3091 [para_into,184,932] f(f(x,f(y,z)),f(f(1,y),x))=f(f(x,f(y,z)),1). given clause #672: (wt=15) 7909 [para_into,7362,409,demod,4] f(x,f(f(y,f(1,x)),f(f(x,x),z)))=1. given clause #673: (wt=15) 7915 [para_into,7362,290,demod,4] f(x,f(f(f(x,1),y),f(f(x,x),z)))=1. given clause #674: (wt=15) 7923 [para_into,7362,218,demod,4] f(x,f(f(y,f(x,1)),f(f(x,x),z)))=1. given clause #675: (wt=15) 7927 [para_into,7362,213,demod,30,48] f(x,f(f(f(x,x),y),f(f(x,1),z)))=1. given clause #676: (wt=25) 3093 [para_into,184,752,demod,2769] f(f(f(x,x),f(y,z)),f(f(y,y),f(1,x)))=f(1,f(f(y,z),f(1,x))). given clause #677: (wt=15) 7931 [para_into,7362,190,demod,30,48] f(x,f(f(y,f(x,x)),f(f(x,1),z)))=1. given clause #678: (wt=15) 7935 [para_into,7362,180,demod,30,4380] f(x,f(1,f(y,f(x,f(f(y,x),z)))))=1. given clause #679: (wt=15) 7941 [para_into,7362,111,demod,30,4380] f(x,f(1,f(y,f(y,f(f(y,x),z)))))=1. given clause #680: (wt=15) 7985 [para_into,7362,935,demod,30,88] f(x,f(f(y,f(1,x)),f(z,f(x,x))))=1. given clause #681: (wt=25) 3096 [para_into,184,291,demod,2543] f(f(f(x,1),f(y,z)),f(f(y,y),f(x,x)))=f(1,f(f(y,z),f(x,x))). given clause #682: (wt=15) 7987 [para_into,7362,798,demod,4] f(x,f(f(y,f(x,x)),f(z,f(x,x))))=1. given clause #683: (wt=15) 7989 [para_into,7362,752,demod,4] f(x,f(f(y,f(x,x)),f(z,f(1,x))))=1. given clause #684: (wt=15) 7999 [para_into,7362,379,demod,30,48] f(x,f(f(y,f(x,1)),f(z,f(x,x))))=1. given clause #685: (wt=15) 8007 [para_into,7362,304,demod,30,88] f(x,f(f(y,f(1,x)),f(z,f(x,1))))=1. given clause #686: (wt=19) 3098 [para_into,184,290] f(f(x,f(y,z)),f(f(y,1),x))=f(f(x,f(y,z)),1). given clause #687: (wt=15) 8011 [para_into,7362,269,demod,30,4380] f(x,f(1,f(y,f(f(z,f(y,x)),x))))=1. given clause #688: (wt=15) 8015 [para_into,7362,260,demod,30,48] f(x,f(f(y,f(x,1)),f(z,f(x,1))))=1. given clause #689: (wt=15) 8019 [para_into,7362,221,demod,4] f(x,f(f(y,f(x,x)),f(z,f(x,1))))=1. given clause #690: (wt=15) 8025 [para_into,7362,170,demod,30,4380] f(x,f(1,f(y,f(f(z,f(y,x)),y))))=1. given clause #691: (wt=25) 3101 [para_into,184,221,demod,2769] f(f(f(x,x),f(y,z)),f(f(y,y),f(x,1)))=f(1,f(f(y,z),f(1,x))). given clause #692: (wt=15) 8115 [para_into,7468,170] f(f(f(f(x,y),z),x),f(f(x,y),1))=1. given clause #693: (wt=15) 8170 [para_into,7480,1272,demod,167] f(x,f(f(f(x,x),y),f(f(x,x),z)))=1. given clause #694: (wt=15) 8172 [para_into,7480,1263,demod,95] f(x,f(f(f(1,x),y),f(f(1,x),z)))=1. given clause #695: (wt=15) 8174 [para_into,7480,836,demod,4] f(x,f(f(f(x,1),y),f(f(x,1),z)))=1. given clause #696: (wt=19) 3106 [para_into,184,60] f(f(x,f(y,z)),f(f(y,y),x))=f(f(x,f(y,z)),1). given clause #697: (wt=15) 8200 [para_into,7480,304,demod,30,88] f(x,f(f(y,f(x,1)),f(f(1,x),z)))=1. given clause #698: (wt=15) 8238 [para_into,7480,935,demod,30,88] f(x,f(f(f(1,x),y),f(z,f(x,x))))=1. given clause #699: (wt=15) 8240 [para_into,7480,796,demod,4] f(x,f(f(f(x,x),y),f(z,f(x,x))))=1. given clause #700: (wt=15) 8242 [para_into,7480,752,demod,4] f(x,f(f(f(x,x),y),f(z,f(1,x))))=1. given clause #701: (wt=25) 3116 [back_demod,2156,demod,3048,30,2840] f(x,f(f(y,f(z,f(x,x))),f(y,f(u,f(1,f(z,f(x,1)))))))=f(y,x). given clause #702: (wt=15) 8252 [para_into,7480,379,demod,30,48] f(x,f(f(f(x,1),y),f(z,f(x,x))))=1. given clause #703: (wt=15) 8260 [para_into,7480,304,demod,30,88] f(x,f(f(f(1,x),y),f(z,f(x,1))))=1. given clause #704: (wt=15) 8264 [para_into,7480,269,demod,30,4380] f(x,f(1,f(y,f(f(f(y,x),z),x))))=1. given clause #705: (wt=15) 8268 [para_into,7480,260,demod,30,48] f(x,f(f(f(x,1),y),f(z,f(x,1))))=1. given clause #706: (wt=21) 3192 [para_into,1000,184,demod,48,30,2840] f(f(x,f(y,f(z,u))),f(1,f(y,f(z,1))))=f(y,f(z,z)). ----> UNIT CONFLICT at 120.30 sec ----> 38026 [binary,38024,20958] $Ans(OL_Sh). Length of proof is 46. Level of proof is 11. ---------------- 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. 6 [] f(x,f(x,x))=1. 8 [] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(A,f(f(B,B),B)),C)))!=A|$Ans(OL_Sh). 13 [para_into,3,3] f(x,f(f(x,x),y))=f(x,x). 15 [para_into,3,6] f(f(x,x),1)=x. 20,19 [para_into,3,2] f(x,f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)))=f(x,y). 22,21 [para_from,3,6] f(f(x,x),x)=1. 23 [para_from,3,2,flip.1] f(x,f(f(y,x),f(y,x)))=f(y,x). 25 [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)). 27 [back_demod,8,demod,22] f(f(f(f(B,A),f(A,C)),D),f(A,f(f(A,1),C)))!=A|$Ans(OL_Sh). 28 [para_into,15,3] f(x,1)=f(x,x). 30,29 [para_into,15,2,demod,20,flip.1] f(f(x,y),f(x,y))=f(f(x,y),1). 31 [copy,28,flip.1] f(x,x)=f(x,1). 32 [back_demod,25,demod,30] f(f(x,x),f(f(y,f(x,z)),1))=f(y,f(x,x)). 34 [back_demod,23,demod,30] f(x,f(f(y,x),1))=f(y,x). 44 [back_demod,2,demod,30,30] f(x,f(f(y,z),1))=f(y,f(f(x,z),1)). 45 [para_from,31,21] f(f(x,1),x)=1. 48,47 [para_from,31,15] f(f(x,1),1)=x. 50,49 [para_from,31,13] f(x,f(f(x,1),y))=f(x,x). 55 [back_demod,27,demod,50] f(f(f(f(B,A),f(A,C)),D),f(A,A))!=A|$Ans(OL_Sh). 60 [para_into,32,45,demod,30,48,48,30,48] f(x,y)=f(y,x). 68,67 [para_into,32,31,demod,48,4,flip.1] f(f(x,y),f(x,x))=x. 76,75 [para_into,60,47,flip.1] f(1,f(x,1))=x. 79 [para_into,60,28] f(x,x)=f(1,x). 88,87 [para_from,60,47] f(f(1,x),1)=x. 91 [para_from,60,32] f(f(x,x),f(1,f(y,f(x,z))))=f(y,f(x,x)). 95,94 [para_from,60,3] f(f(x,x),f(y,x))=x. 96 [para_from,60,32] f(f(x,x),f(f(y,f(z,x)),1))=f(y,f(x,x)). 100,99 [para_into,75,60] f(1,f(1,x))=x. 113 [para_into,34,60] f(x,f(f(x,y),1))=f(y,x). 115 [para_into,34,3,demod,4] f(f(x,y),f(x,1))=x. 166 [para_into,67,60] f(f(x,y),f(y,y))=y. 178 [para_from,67,32,demod,30,30] f(f(f(x,y),1),f(f(z,x),1))=f(z,f(f(x,y),1)). 180 [para_into,94,79] f(f(1,x),f(y,x))=x. 184 [para_into,94,32,demod,30,48] f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),1). 213 [para_into,44,15,demod,48] f(x,f(y,1))=f(f(y,y),x). 221 [copy,213,flip.1] f(f(x,x),y)=f(y,f(x,1)). 267 [para_into,166,115] f(f(x,f(y,1)),y)=f(y,1). 269 [para_into,166,79] f(f(x,y),f(1,y))=y. 340 [para_into,55,60] f(f(f(f(A,B),f(A,C)),D),f(A,A))!=A|$Ans(OL_Sh). 391 [para_from,113,180,demod,76] f(f(x,y),f(y,x))=f(f(x,y),1). 810,809 [para_from,91,269,demod,100] f(f(x,f(y,y)),f(x,f(y,z)))=f(1,f(x,f(y,z))). 1000 [para_into,96,267,demod,48,95,flip.1] f(f(x,f(f(y,z),1)),f(z,z))=z. 2382 [para_from,178,267] f(f(x,f(f(y,z),1)),f(x,y))=f(f(x,y),1). 2840,2839 [para_into,391,221,demod,810,flip.1] f(f(x,f(y,y)),1)=f(1,f(x,f(y,1))). 3192 [para_into,1000,184,demod,48,30,2840] f(f(x,f(y,f(z,u))),f(1,f(y,f(z,1))))=f(y,f(z,z)). 4965 [para_into,340,60] f(f(D,f(f(A,B),f(A,C))),f(A,A))!=A|$Ans(OL_Sh). 20958 [para_into,4965,79] f(f(D,f(f(A,B),f(A,C))),f(1,A))!=A|$Ans(OL_Sh). 38024 [para_into,3192,2382,demod,88,48,88,68] f(f(x,f(f(y,z),f(y,u))),f(1,y))=y. 38026 [binary,38024,20958] $Ans(OL_Sh). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 706 clauses generated 741449 para_from generated 324363 para_into generated 417086 demod & eval rewrites 2017727 clauses wt,lit,sk delete 42548 tautologies deleted 0 clauses forward subsumed 687812 (subsumed by sos) 24226 unit deletions 0 factor simplifications 0 clauses kept 22148 new demodulators 15877 empty clauses 1 clauses back demodulated 4863 clauses back subsumed 583 usable size 587 sos size 16115 demodulators size 12643 passive size 0 hot size 0 Kbytes malloced 24844 ----------- times (seconds) ----------- user CPU time 120.30 (0 hr, 2 min, 0 sec) system CPU time 2.85 (0 hr, 0 min, 2 sec) wall-clock time 123 (0 hr, 2 min, 3 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.97 para_into time 1.74 para_from time 2.64 pre_process time 21.03 renumber time 0.82 demod time 14.08 order equalities 0.64 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.71 hints keep time 0.00 sort lits time 0.00 forward subsume 1.88 delete cl time 0.45 keep cl time 0.81 hints time 0.00 print_cl time 0.00 conflict time 0.23 new demod time 0.20 post_process time 93.41 back demod time 75.35 back subsume 16.12 factor time 0.00 unindex time 7.39 That finishes the proof of the theorem. Process 2360 finished Mon Sep 15 12:19:35 2003