----- Otter 3.3f (UNM), August 2004 (mod 2005-apr-14, parse) ----- The process was started by veroff on pacaderm, Sat Jul 23 00:37:09 2005 The command was "otter -f median.in". The process ID is 24617. % Reading file median.in. lex([A,B,C,D,E,f(x,x,x)]). set(para_from). set(para_into). set(lex_order_vars). set(order_eq). set(dynamic_demod). set(back_demod). assign(dynamic_demod_depth,1). assign(dynamic_demod_rhs,4). assign(demod_limit,200). WARNING: clear(dynamic_demod_lex_dep) flag already clear. clear(dynamic_demod_lex_dep). set(input_sos_first). assign(bsub_hint_add_wt,-1024). set(keep_hint_subsumers). assign(pick_given_ratio,4). assign(max_weight,45). assign(change_limit_after,50). assign(new_max_weight,25). assign(max_mem,750000). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). WARNING: assign(heat,1) already has that value. assign(heat,1). weight_list(pick_given). weight(f(f($(1),$(1),$(1)),f($(1),$(1),$(1)),f($(1),$(1),$(1))),1). weight(f(x,x,$(1)),6). weight(f(x,$(1),x),6). weight(f($(1),x,x),6). weight(f(x,$(1),$(1)),3). weight(f($(1),x,$(1)),3). weight(f($(1),$(1),x),3). end_of_list. list(hot). 1 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). end_of_list. list(sos). 2 [] f(x,x,y)=x. 3 [] f(x,y,z)=f(y,x,z). 4 [] f(x,y,z)=f(x,z,y). 5 [] f(x,y,z)=f(z,y,x). 6 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 7 [] f(f(A,B,C),D,E)!=f(f(A,D,E),f(B,D,E),f(C,D,E)) # label("original"). 8 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(f(A,B,C),D,E) # label("original"). 9 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)) # label("original"). end_of_list. list(demodulators). 10 [] f(x,x,y)=x. 11 [] f(x,y,x)=x. 12 [] f(y,x,x)=x. 13 [] f(x,y,z)=f(y,x,z). 14 [] f(x,y,z)=f(x,z,y). 15 [] f(x,y,z)=f(z,y,x). end_of_list. list(hints2). 16 [] f(x,y,f(x,y,z))=f(x,y,z). 17 [] f(x,y,f(x,z,y))=f(x,y,z). 18 [] f(x,y,f(y,x,z))=f(x,y,z). 19 [] f(x,y,f(y,z,x))=f(x,y,z). 20 [] f(x,y,f(z,x,y))=f(x,y,z). 21 [] f(x,y,f(z,y,x))=f(x,y,z). 22 [] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z). 23 [] f(x,y,f(x,z,f(y,u,z)))=f(x,y,z). 24 [] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). 25 [] f(x,y,f(x,z,f(z,u,y)))=f(x,y,z). 26 [] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). 27 [] f(x,y,f(x,z,f(u,z,y)))=f(x,y,z). 28 [] f(x,y,f(z,x,f(y,z,u)))=f(x,y,z). 29 [] f(x,y,f(z,x,f(y,u,z)))=f(x,y,z). 30 [] f(x,y,f(z,x,f(z,y,u)))=f(x,y,z). 31 [] f(x,y,f(z,x,f(z,u,y)))=f(x,y,z). 32 [] f(x,y,f(z,x,f(u,y,z)))=f(x,y,z). 33 [] f(x,y,f(z,x,f(u,z,y)))=f(x,y,z). 34 [] f(y,x,f(x,z,f(y,z,u)))=f(x,y,z). 35 [] f(y,x,f(x,z,f(y,u,z)))=f(x,y,z). 36 [] f(y,x,f(x,z,f(z,y,u)))=f(x,y,z). 37 [] f(y,x,f(x,z,f(z,u,y)))=f(x,y,z). 38 [] f(y,x,f(x,z,f(u,y,z)))=f(x,y,z). 39 [] f(y,x,f(x,z,f(u,z,y)))=f(x,y,z). 40 [] f(y,x,f(z,x,f(y,z,u)))=f(x,y,z). 41 [] f(y,x,f(z,x,f(y,u,z)))=f(x,y,z). 42 [] f(y,x,f(z,x,f(z,y,u)))=f(x,y,z). 43 [] f(y,x,f(z,x,f(z,u,y)))=f(x,y,z). 44 [] f(y,x,f(z,x,f(u,y,z)))=f(x,y,z). 45 [] f(y,x,f(z,x,f(u,z,y)))=f(x,y,z). end_of_list. list(hints2). 46 [] f(x,x,y)=x. 47 [] f(x,z,y)=f(x,y,z). 48 [] f(y,z,x)=f(x,y,z). 49 [] f(f(A,D,E),f(A,D,E),f(C,D,E))!=f(f(A,A,C),D,E). 50 [] f(x,y,x)=x. 51 [] f(f(A,D,E),f(A,D,E),f(C,D,E))!=f(f(A,C,A),D,E). 52 [] f(f(A,D,E),f(A,D,E),f(C,D,E))!=f(A,D,E). end_of_list. list(hints2). 53 [] f(x,x,y)=x. 54 [] f(x,z,y)=f(x,y,z). 55 [] f(f(A,D,E),f(B,D,E),f(A,D,E))!=f(f(A,B,A),D,E). 56 [] x=x. 57 [] f(x,y,x)=x. 58 [] f(f(A,B,A),D,E)!=f(A,D,E). 59 [] f(A,D,E)!=f(A,D,E). end_of_list. list(hints2). 60 [] f(x,x,y)=x. 61 [] f(x,z,y)=f(x,y,z). 62 [] f(y,z,x)=f(x,y,z). 63 [] f(f(A,D,D),f(B,D,D),f(C,D,D))!=f(f(A,B,C),D,D). 64 [] x=x. 65 [] f(x,y,x)=x. 66 [] f(x,y,y)=y. 67 [] f(D,f(B,D,D),f(C,D,D))!=f(f(A,B,C),D,D). 68 [] f(f(A,B,C),D,D)!=f(D,D,f(C,D,D)). 69 [] f(f(A,B,C),D,D)!=f(D,D,D). 70 [] f(f(A,B,C),D,D)!=D. 71 [] D!=D. end_of_list. list(hints2). 72 [] f(x,x,y)=x. 73 [] f(y,z,x)=f(x,y,z). 74 [] f(f(A,D,E),f(B,D,E),f(B,D,E))!=f(f(A,B,B),D,E). 75 [] x=x. 76 [] f(x,y,y)=y. 77 [] f(f(A,B,B),D,E)!=f(B,D,E). 78 [] f(B,D,E)!=f(B,D,E). 79 [] $F. end_of_list. list(hints2). 80 [] f(x,x,y)=x. 81 [] f(x,z,y)=f(x,y,z). 82 [] f(y,z,x)=f(x,y,z). 83 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 84 [] f(f(A,D,B),f(B,D,B),f(C,D,B))!=f(f(A,B,C),D,B). 85 [] f(x,y,x)=x. 86 [] f(f(A,D,B),B,f(C,D,B))!=f(f(A,B,C),D,B). 87 [] f(y,x,z)=f(x,y,z). 88 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 89 [] f(f(x,y,z),y,u)=f(x,y,f(z,u,y)). 90 [] f(f(x,y,z),y,z)=f(x,y,z). 91 [] f(z,x,y)=f(x,y,z). 92 [] f(f(x,y,z),x,y)=f(z,x,y). 93 [] f(f(x,y,z),y,x)=f(z,x,y). 94 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 95 [] f(f(f(A,D,B),B,C),B,D)!=f(f(A,B,C),D,B). 96 [] $F. end_of_list. list(hints2). 97 [] f(x,z,y)=f(x,y,z). 98 [] f(y,z,x)=f(x,y,z). 99 [] f(x,x,y)=x. 100 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 101 [] f(f(A,D,A),f(B,D,A),f(C,D,A))!=f(f(A,B,C),D,A). 102 [] f(x,y,x)=x. 103 [] f(A,f(B,D,A),f(C,D,A))!=f(f(A,B,C),D,A). 104 [] f(f(C,D,A),A,f(B,D,A))!=f(f(A,B,C),D,A). 105 [] f(f(C,D,A),A,f(B,D,A))!=f(f(C,A,B),D,A). 106 [] f(f(x,y,z),y,u)=f(x,y,f(z,u,y)). 107 [] f(f(x,y,z),y,z)=f(x,y,z). 108 [] f(z,x,y)=f(x,y,z). 109 [] f(f(x,y,z),x,y)=f(z,x,y). 110 [] f(f(f(x,y,z),y,u),x,y)=f(f(z,y,u),x,y). 111 [] f(f(f(x,y,z),z,u),y,z)=f(f(x,z,u),y,z). 112 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 113 [] f(f(x,y,z),z,f(u,y,z))=f(f(x,z,u),y,z). 114 [] $F. end_of_list. list(hints2). 115 [] f(x,z,y)=f(x,y,z). 116 [] f(y,z,x)=f(x,y,z). 117 [] f(x,x,y)=x. 118 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 119 [] f(f(A,D,C),f(B,D,C),f(C,D,C))!=f(f(A,B,C),D,C). 120 [] f(x,y,x)=x. 121 [] f(f(A,D,C),f(B,D,C),C)!=f(f(A,B,C),D,C). 122 [] f(D,C,A)=f(A,D,C). 123 [] f(f(D,C,A),f(B,D,C),C)!=f(f(A,B,C),D,C). 124 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),y,f(u,y,w)). 125 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),y,f(u,w,y)). 126 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),f(u,w,y),y). 127 [] f(f(x,y,z),y,z)=f(x,y,z). 128 [] f(z,x,y)=f(x,y,z). 129 [] f(f(x,y,z),x,y)=f(z,x,y). 130 [] f(f(x,y,z),y,x)=f(z,x,y). 131 [] f(f(D,C,f(A,B,C)),C,D)!=f(f(D,C,A),f(B,D,C),C). 132 [] f(f(D,C,f(A,C,B)),C,D)!=f(f(D,C,A),f(B,D,C),C). 133 [] $F. end_of_list. list(hints2). 134 [] f(x,z,y)=f(x,y,z). 135 [] f(y,z,x)=f(x,y,z). 136 [] f(x,x,y)=x. 137 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 138 [] f(f(A,B,E),f(B,B,E),f(C,B,E))!=f(f(A,B,C),B,E). 139 [] f(x,y,x)=x. 140 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 141 [] f(f(A,B,E),f(B,B,E),f(C,B,E))!=f(f(A,B,C),E,B). 142 [] f(f(A,B,E),f(B,E,B),f(C,B,E))!=f(f(A,B,C),E,B). 143 [] f(f(A,B,E),B,f(C,B,E))!=f(f(A,B,C),E,B). 144 [] f(f(x,y,z),y,z)=f(x,y,z). 145 [] f(z,x,y)=f(x,y,z). 146 [] f(f(x,y,z),x,y)=f(z,x,y). 147 [] f(f(x,y,z),y,x)=f(z,x,y). 148 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 149 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 150 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 151 [] $F. end_of_list. list(hints2). 152 [] f(x,z,y)=f(x,y,z). 153 [] f(y,z,x)=f(x,y,z). 154 [] f(x,x,y)=x. 155 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 156 [] f(f(A,C,E),f(B,C,E),f(C,C,E))!=f(f(A,B,C),C,E). 157 [] f(x,y,x)=x. 158 [] f(y,x,z)=f(x,y,z). 159 [] f(z,y,x)=f(x,y,z). 160 [] f(z,x,y)=f(x,y,z). 161 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 162 [] f(f(A,C,E),f(B,C,E),f(C,C,E))!=f(f(A,B,C),E,C). 163 [] f(f(A,C,E),f(B,C,E),f(C,E,C))!=f(f(A,B,C),E,C). 164 [] f(f(A,C,E),f(B,C,E),C)!=f(f(A,B,C),E,C). 165 [] f(f(x,y,z),y,z)=f(x,y,z). 166 [] f(f(x,y,z),y,x)=f(z,y,x). 167 [] f(f(x,y,z),y,x)=f(z,x,y). 168 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 169 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 170 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 171 [] f(f(x,y,z),f(u,y,z),y)=f(f(u,y,x),z,y). 172 [] f(f(x,y,z),f(u,y,z),y)=f(f(x,u,y),z,y). 173 [] $F. end_of_list. list(hints2). 174 [] f(x,z,y)=f(x,y,z). 175 [] f(y,z,x)=f(x,y,z). 176 [] f(x,x,y)=x. 177 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 178 [] f(f(A,A,E),f(B,A,E),f(C,A,E))!=f(f(A,B,C),A,E). 179 [] f(x,y,x)=x. 180 [] f(y,x,z)=f(x,y,z). 181 [] f(z,y,x)=f(x,y,z). 182 [] f(z,x,y)=f(x,y,z). 183 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),y,f(u,y,w)). 184 [] f(f(A,A,E),f(B,A,E),f(C,A,E))!=f(f(A,B,C),E,A). 185 [] f(f(A,E,A),f(B,A,E),f(C,A,E))!=f(f(A,B,C),E,A). 186 [] f(A,f(B,A,E),f(C,A,E))!=f(f(A,B,C),E,A). 187 [] f(f(x,y,z),y,z)=f(x,y,z). 188 [] f(f(x,y,z),y,x)=f(z,y,x). 189 [] f(f(x,y,z),y,x)=f(z,x,y). 190 [] f(f(x,y,z),y,f(u,y,x))=f(f(z,y,u),x,y). 191 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 192 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 193 [] f(f(x,y,z),f(u,y,z),y)=f(f(u,y,x),z,y). 194 [] f(f(x,y,z),f(u,y,z),y)=f(f(y,x,u),z,y). 195 [] f(x,f(y,x,z),f(u,x,z))=f(f(x,y,u),z,x). 196 [] $F. end_of_list. list(hints2). 197 [] f(z,y,x)=f(x,y,z). 198 [] f(x,x,y)=x. 199 [] f(f(A,D,D),f(B,D,D),f(C,D,D))!=f(f(A,B,C),D,D). 200 [] f(x,y,y)=y. 201 [] f(z,x,x)=f(x,x,y). 202 [] f(x,f(y,x,x),z)=f(u,x,x). 203 [] f(f(x,y,y),f(z,y,y),u)=f(w,y,y). 204 [] $F. end_of_list. list(hints2). 205 [] f(y,x,z)=f(x,y,z). 206 [] f(x,z,y)=f(x,y,z). 207 [] f(x,x,y)=x. 208 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 209 [] f(f(A,D,B),f(B,D,B),f(C,D,B))!=f(f(A,B,C),D,B). 210 [] f(y,z,x)=f(x,y,z). 211 [] f(z,x,y)=f(x,y,z). 212 [] f(x,y,x)=x. 213 [] f(f(x,y,z),y,u)=f(x,y,f(z,u,y)). 214 [] f(f(x,y,z),y,z)=f(x,y,z). 215 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 216 [] f(f(x,y,z),x,y)=f(z,x,y). 217 [] f(f(x,y,z),y,x)=f(z,x,y). 218 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 219 [] f(f(x,y,z),z,f(u,y,z))=f(f(x,z,u),y,z). 220 [] f(f(x,y,z),f(z,u,z),f(w,y,z))=f(f(x,z,w),y,z). 221 [] $F. end_of_list. list(hints2). 222 [] f(y,x,z)=f(x,y,z). 223 [] f(x,z,y)=f(x,y,z). 224 [] f(x,x,y)=x. 225 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 226 [] f(f(A,D,A),f(B,D,A),f(C,D,A))!=f(f(A,B,C),D,A). 227 [] f(y,z,x)=f(x,y,z). 228 [] f(z,x,y)=f(x,y,z). 229 [] f(x,y,x)=x. 230 [] f(f(x,y,z),y,u)=f(x,y,f(z,u,y)). 231 [] f(f(x,y,z),y,z)=f(x,y,z). 232 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 233 [] f(f(x,y,z),x,y)=f(z,x,y). 234 [] f(f(x,y,z),y,x)=f(z,x,y). 235 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 236 [] f(f(x,y,z),z,f(u,y,z))=f(f(x,z,u),y,z). 237 [] f(f(x,y,z),z,f(u,y,z))=f(f(z,u,x),y,z). 238 [] f(x,f(y,z,x),f(u,z,x))=f(f(x,y,u),z,x). 239 [] f(f(x,y,x),f(z,u,x),f(w,u,x))=f(f(x,z,w),u,x). 240 [] $F. end_of_list. list(hints2). 241 [] f(y,x,z)=f(x,y,z). 242 [] f(x,z,y)=f(x,y,z). 243 [] f(x,x,y)=x. 244 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 245 [] f(f(A,B,E),f(B,B,E),f(C,B,E))!=f(f(A,B,C),B,E). 246 [] f(y,z,x)=f(x,y,z). 247 [] f(z,x,y)=f(x,y,z). 248 [] f(x,y,x)=x. 249 [] f(f(x,y,z),y,z)=f(x,y,z). 250 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 251 [] f(f(x,y,z),x,y)=f(z,x,y). 252 [] f(f(x,y,z),y,x)=f(z,x,y). 253 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 254 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 255 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 256 [] f(f(x,y,z),f(y,y,u),f(w,y,z))=f(f(x,y,w),z,y). 257 [] f(f(x,y,z),f(y,y,u),f(w,y,z))=f(f(x,y,w),y,z). 258 [] $F. end_of_list. list(hints2). 259 [] f(y,x,z)=f(x,y,z). 260 [] f(x,z,y)=f(x,y,z). 261 [] f(x,x,y)=x. 262 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 263 [] f(f(A,C,E),f(B,C,E),f(C,C,E))!=f(f(A,B,C),C,E). 264 [] f(y,z,x)=f(x,y,z). 265 [] f(z,x,y)=f(x,y,z). 266 [] f(x,y,x)=x. 267 [] f(f(x,y,z),y,z)=f(x,y,z). 268 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 269 [] f(f(x,y,z),x,y)=f(z,x,y). 270 [] f(f(x,y,z),y,x)=f(z,x,y). 271 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 272 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 273 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 274 [] f(f(x,y,z),f(u,y,z),y)=f(f(u,y,x),z,y). 275 [] f(f(x,y,z),f(u,y,z),y)=f(f(x,u,y),z,y). 276 [] f(f(x,y,z),f(u,y,z),f(y,y,w))=f(f(x,u,y),z,y). 277 [] f(f(x,y,z),f(u,y,z),f(y,y,w))=f(f(x,u,y),y,z). 278 [] $F. end_of_list. list(hints2). 279 [] f(y,x,z)=f(x,y,z). 280 [] f(x,z,y)=f(x,y,z). 281 [] f(x,x,y)=x. 282 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 283 [] f(f(A,A,E),f(B,A,E),f(C,A,E))!=f(f(A,B,C),A,E). 284 [] f(y,z,x)=f(x,y,z). 285 [] f(z,x,y)=f(x,y,z). 286 [] f(x,y,x)=x. 287 [] f(f(x,y,z),y,z)=f(x,y,z). 288 [] f(f(x,y,z),z,u)=f(y,z,f(x,z,u)). 289 [] f(f(x,y,z),x,y)=f(z,x,y). 290 [] f(f(x,y,z),y,x)=f(z,x,y). 291 [] f(f(f(x,y,z),z,u),z,y)=f(f(x,z,u),y,z). 292 [] f(f(x,y,z),z,f(u,z,y))=f(f(x,z,u),y,z). 293 [] f(f(x,y,z),y,f(u,y,z))=f(f(x,y,u),z,y). 294 [] f(f(x,y,z),f(u,y,z),y)=f(f(u,y,x),z,y). 295 [] f(f(x,y,z),f(u,y,z),y)=f(f(y,x,u),z,y). 296 [] f(x,f(y,x,z),f(u,x,z))=f(f(x,y,u),z,x). 297 [] f(f(x,x,y),f(z,x,u),f(w,x,u))=f(f(x,z,w),u,x). 298 [] f(f(x,x,y),f(z,x,u),f(w,x,u))=f(f(x,z,w),x,u). 299 [] $F. end_of_list. list(hints2). 300 [] f(y,x,z)=f(x,y,z). 301 [] f(x,z,y)=f(x,y,z). 302 [] f(x,x,y)=x. 303 [] f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). 304 [] f(f(A,D,C),f(B,D,C),f(C,D,C))!=f(f(A,B,C),D,C). 305 [] f(x,f(y,z,u),w)=f(x,w,f(y,u,z)). 306 [] f(y,z,x)=f(x,y,z). 307 [] f(z,x,y)=f(x,y,z). 308 [] f(x,y,x)=x. 309 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),y,f(u,y,w)). 310 [] f(f(x,y,z),y,z)=f(x,y,z). 311 [] f(f(x,y,z),x,y)=f(z,x,y). 312 [] f(f(x,y,z),y,x)=f(z,x,y). 313 [] f(f(x,y,f(z,y,u)),y,w)=f(f(x,y,z),f(u,w,y),y). 314 [] f(f(x,y,f(z,u,y)),y,w)=f(f(x,y,z),f(u,w,y),y). 315 [] f(f(x,y,z),f(u,x,y),y)=f(f(z,u,y),x,y). 316 [] f(f(x,y,z),f(u,y,z),z)=f(f(x,u,z),y,z). 317 [] f(f(x,y,z),f(u,y,z),f(z,w,z))=f(f(x,u,z),y,z). 318 [] $F. end_of_list. list(hints2). 319 [] f(x,z,y)=f(x,y,z). 320 [] f(z,y,x)=f(x,y,z). 321 [] f(x,x,y)=x. 322 [] f(f(A,D,E),f(B,D,E),f(A,D,E))!=f(f(A,B,A),D,E). 323 [] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). 324 [] f(x,y,x)=x. 325 [] f(x,y,f(z,z,u))=f(z,y,x). 326 [] f(f(x,y,x),z,u)=f(x,z,u). 327 [] f(f(x,y,z),u,f(x,y,z))=f(f(x,w,x),y,z). 328 [] $F. end_of_list. list(hints2). 329 [] f(x,z,y)=f(x,y,z). 330 [] f(z,y,x)=f(x,y,z). 331 [] f(x,x,y)=x. 332 [] f(f(A,D,E),f(B,D,E),f(B,D,E))!=f(f(A,B,B),D,E). 333 [] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). 334 [] f(x,y,y)=y. 335 [] f(x,y,f(z,z,u))=f(z,y,x). 336 [] f(z,x,x)=f(x,x,y). 337 [] f(x,f(y,x,x),z)=f(u,x,x). 338 [] f(f(x,y,x),z,u)=f(x,z,u). 339 [] f(f(x,y,y),z,u)=f(y,z,u). 340 [] f(x,f(y,z,u),f(y,z,u))=f(f(w,y,y),z,u). 341 [] $F. end_of_list. list(hints2). 342 [] f(x,z,y)=f(x,y,z). 343 [] f(z,y,x)=f(x,y,z). 344 [] f(x,x,y)=x. 345 [] f(f(A,D,E),f(A,D,E),f(C,D,E))!=f(f(A,A,C),D,E). 346 [] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). 347 [] f(x,y,y)=y. 348 [] f(x,y,f(z,z,u))=f(z,y,x). 349 [] f(z,x,x)=f(x,x,y). 350 [] f(f(x,y,x),z,u)=f(x,z,u). 351 [] f(f(x,y,z),f(x,y,z),u)=f(f(x,w,x),y,z). 352 [] f(x,x,y)=f(x,x,x). 353 [] f(f(x,y,z),f(x,y,z),u)=f(f(x,x,w),y,z). 354 [] $F. end_of_list. list(hints2). 355 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 356 [] f(y,x,z)=f(x,y,z). 357 [] f(x,x,y)=x. 358 [] f(x,y,x)=x. 359 [] f(y,x,x)=x. 360 [] f(y,x,z)=f(x,y,z). 361 [] f(x,z,y)=f(x,y,z). 362 [] f(z,y,x)=f(x,y,z). 363 [] f(x,y,f(x,y,z))=f(x,y,z). 364 [] f(x,y,f(x,z,y))=f(x,y,z). 365 [] f(x,y,f(z,x,y))=f(x,y,z). 366 [] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z). 367 [] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). 368 [] f(x,y,f(x,z,f(u,z,y)))=f(x,y,z). 369 [] f(y,x,f(x,z,f(y,z,u)))=f(x,y,z). 370 [] f(y,x,f(x,z,f(y,u,z)))=f(x,y,z). 371 [] f(y,x,f(x,z,f(u,y,z)))=f(x,y,z). 372 [] f(y,x,f(z,x,f(y,z,u)))=f(x,y,z). 373 [] f(y,x,f(z,x,f(u,y,z)))=f(x,y,z). 374 [] f(y,x,f(z,x,f(u,z,y)))=f(x,y,z). 375 [] f(x,x,y)=x. 376 [] f(y,x,z)=f(x,y,z). 377 [] f(x,z,y)=f(x,y,z). 378 [] f(z,y,x)=f(x,y,z). 379 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 380 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)) # label("original"). 381 [] f(x,y,z)=f(x,y,z). 382 [] f(z,x,f(x,u,y))=f(x,y,f(z,x,u)). 383 [] x=x. 384 [] f(u,x,f(x,y,f(x,w,z)))=f(x,y,f(x,z,f(u,x,w))). 385 [] f(x,f(y,x,z),f(x,u,w))=f(x,w,f(y,x,f(x,z,u))). 386 [] f(x,u,f(z,x,y))=f(x,y,f(z,x,u)). 387 [] f(z,x,f(u,x,y))=f(x,y,f(z,u,x)). 388 [] f(x,z,f(x,u,y))=f(x,y,f(x,z,u)). 389 [] f(u,x,f(x,w,f(x,z,y)))=f(x,y,f(x,z,f(u,x,w))). 390 [] f(z,x,f(x,y,u))=f(x,y,f(z,x,u)). 391 [] f(y,x,f(x,w,f(x,z,u)))=f(x,f(y,x,z),f(x,u,w)). 392 [] f(y,z,f(z,u,f(w,f(y,z,u),f(x,w5,f(y,z,u)))))=f(x,f(y,z,u),f(z,f(y,z,u),f(w,w5,f(y,z,u)))). 393 [] f(x,z,f(x,f(x,u,y),f(w5,u,w)))=f(x,y,f(x,z,f(u,w,f(x,w5,u)))). 394 [] f(u,x,f(x,y,f(u,w5,f(z,u,w))))=f(x,y,f(z,u,f(u,x,f(u,w,w5)))). 395 [] f(x,f(x,y,f(x,z,u)),f(u,w,w5))=f(x,f(x,y,z),f(u,w5,f(x,u,w))). 396 [] f(y,x,f(z,f(x,z,w5),f(z,u,w)))=f(x,f(y,x,z),f(z,u,f(z,w,w5))). 397 [] f(y,z,f(z,u,f(w,x,f(y,z,u))))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 398 [] f(y,z,f(z,u,f(x,w,f(y,z,u))))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 399 [] f(y,x,f(z,w,f(x,z,u)))=f(x,f(y,x,z),f(z,u,w)). 400 [] f(z,x,f(x,y,f(z,u,w)))=f(x,y,f(z,u,f(z,w,x))). 401 [] f(w,f(y,z,u),f(z,u,f(y,z,x)))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 402 [] f(z,f(y,z,u),f(x,w,f(y,z,u)))=f(x,f(y,z,u),f(y,z,f(z,u,w))). 403 [] f(u,x,f(x,y,f(z,u,w)))=f(x,y,f(z,u,f(u,x,w))). 404 [] f(x,z,f(u,y,f(x,y,w)))=f(x,y,f(x,z,f(u,y,w))). 405 [] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,w,f(x,y,u))). 406 [] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). 407 [] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). 408 [] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)). 409 [] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). 410 [] f(y,f(y,z,x),f(z,x,u))=f(x,f(y,z,x),f(y,z,u)). 411 [] f(x,f(x,y,z),f(x,y,u))=f(x,y,f(x,z,u)). 412 [] f(x,z,f(y,u,f(x,y,w)))=f(x,y,f(x,z,f(y,u,w))). 413 [] f(x,f(y,z,x),f(y,z,u))=f(y,z,x). 414 [] f(x,f(y,x,z),f(y,z,u))=f(y,x,z). 415 [] f(x,f(x,y,z),f(y,z,u))=f(x,y,z). 416 [] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(y,u,f(x,y,z)). 417 [] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). 418 [] f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,w))=f(x,y,z). 419 [] f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,w))=f(x,y,z). 420 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). 421 [] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,u)))=f(x,y,u). 422 [] f(f(x,y,z),f(y,u,f(x,y,w)),f(z,w5,f(x,y,z)))=f(x,y,z). 423 [] f(f(x,y,z),f(x,z,u),f(y,w,f(x,y,z)))=f(x,y,z). 424 [] f(f(x,y,z),f(y,u,f(x,y,z)),f(z,w,f(x,z,w5)))=f(x,y,z). 425 [] f(x,z,f(x,w,f(x,u,y)))=f(x,y,f(x,z,f(x,u,w))). 426 [] f(x,y,f(x,z,f(x,u,y)))=f(x,u,f(x,y,z)). 427 [] f(f(x,y,z),f(x,y,u),f(y,z,f(x,z,w)))=f(x,y,z). 428 [] f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,w)))=f(x,y,u). 429 [] f(f(x,y,f(x,z,u)),f(x,w,f(x,y,f(x,z,u))),f(y,w5,f(x,z,u)))=f(x,u,f(x,y,z)). 430 [] f(f(x,y,z),f(x,u,f(x,w,f(x,y,z))),f(w,f(x,w,f(x,y,z)),f(x,u,f(x,w,f(x,y,z)))))=f(x,z,f(x,w,y)). 431 [] f(f(x,y,z),f(y,z,u),f(u,w,f(y,z,u)))=f(y,z,u). 432 [] f(f(x,y,z),f(x,z,u),f(u,w,f(x,z,u)))=f(x,z,u). 433 [] f(x,f(y,z,u),f(y,z,x))=f(y,z,x). 434 [] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(x,w,f(y,z,u)))))=f(y,z,f(x,w,f(y,z,u))). 435 [] f(u,x,f(z,x,y))=f(x,y,f(z,u,x)). 436 [] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,x)))=f(w,f(y,z,u),f(y,z,x)). 437 [] f(f(x,y,z),f(x,u,f(y,z,w)),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 438 [] f(f(x,y,z),f(x,y,u),f(y,u,f(x,u,w)))=f(x,y,u). 439 [] f(z,y,f(x,y,u))=f(x,y,f(z,y,u)). 440 [] f(x,f(y,z,u),f(y,w,f(y,x,f(y,z,u))))=f(y,u,f(y,z,x)). 441 [] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). 442 [] f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,w)))=f(y,z,u). 443 [] f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,w)))=f(x,z,u). 444 [] f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,w)))=f(y,z,u). 445 [] f(x,f(y,z,u),f(z,u,x))=f(z,u,x). 446 [] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). 447 [] f(x,f(y,z,u),f(w,f(y,z,u),f(z,u,x)))=f(w,f(y,z,u),f(z,u,x)). 448 [] f(f(x,y,z),f(x,u,f(w,y,z)),f(w,y,z))=f(u,f(x,y,z),f(w,y,z)). 449 [] f(f(x,y,z),f(x,z,u),f(x,z,f(w,u,f(x,z,u))))=f(x,z,f(w,u,f(x,z,u))). 450 [] f(x,f(y,z,u),f(y,u,x))=f(y,u,x). 451 [] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). 452 [] f(x,y,f(z,u,f(x,y,u)))=f(x,y,u). 453 [] f(f(x,y,z),f(x,z,u),f(z,u,f(x,u,w)))=f(x,z,u). 454 [] f(x,f(x,y,f(x,z,u)),f(y,w,w5))=f(x,z,f(x,u,f(y,w5,f(x,y,w)))). 455 [] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). 456 [] f(f(x,y,f(z,u,w)),f(z,w,w5),f(y,f(z,u,w),f(z,w,w5)))=f(y,f(z,u,w),f(z,w,w5)). 457 [] f(f(x,y,z),f(x,z,f(u,x,y)),f(y,z,w))=f(x,y,z). 458 [] f(f(x,y,f(z,u,w)),f(x,y,f(z,w,f(x,u,w))),f(y,w5,f(z,u,w)))=f(x,y,f(z,u,w)). 459 [] f(f(x,y,z),f(y,z,f(x,y,u)),f(y,w,f(y,u,z)))=f(x,y,f(y,u,z)). 460 [] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,w))=f(z,u,f(x,y,z)). 461 [] f(x,f(x,y,z),f(x,u,f(y,z,w)))=f(x,u,f(x,y,z)). 462 [] f(f(x,y,f(z,u,y)),f(z,u,y),f(z,u,w))=f(z,u,y). 463 [] f(f(x,f(y,z,u),f(f(y,u,w),f(y,u,f(y,z,w)),f(y,w5,f(y,z,u)))),f(y,w,w6),f(y,w,f(y,z,u)))=f(y,w,f(y,z,u)). 464 [] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u). 465 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w). 466 [] f(f(x,y,z),f(y,z,f(x,z,u)),f(z,u,w))=f(z,u,f(x,y,z)). 467 [] f(x,y,f(f(x,z,u),f(w,w5,z),f(w,z,f(x,w5,z))))=f(x,z,f(x,y,f(w,w5,z))). 468 [] f(x,y,f(f(x,z,u),f(y,z,w),f(z,w,f(x,y,z))))=f(x,y,z). 469 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,w,z),f(w,z,w5))=f(y,w,z). 470 [] f(f(x,y,z),f(x,z,u),f(x,z,f(w,u,f(x,u,f(z,u,w5)))))=f(x,z,f(w,u,f(x,u,f(z,u,w5)))). 471 [] f(x,y,f(z,u,f(x,u,f(y,u,w))))=f(x,y,u). 472 [] f(f(x,y,z),f(y,z,f(x,z,u)),f(f(z,u,w),f(z,u,w5),f(w6,w,f(z,u,w))))=f(z,u,f(x,y,z)). 473 [] f(x,f(y,z,u),f(z,u,f(y,u,x)))=f(u,x,f(y,z,u)). 474 [] f(x,y,f(f(z,x,u),f(z,y,w),f(z,w,f(z,x,y))))=f(z,x,y). 475 [] f(x,f(y,z,f(z,x,f(z,u,w))),f(z,x,w))=f(z,x,w). 476 [] f(x,y,f(z,u,f(y,z,f(x,z,w))))=f(x,y,z). 477 [] f(x,f(x,y,z),f(u,y,f(x,y,z)))=f(x,y,z). 478 [] f(x,f(y,z,u),f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). 479 [] f(f(x,y,z),f(y,u,f(x,z,w)),f(y,u,f(u,w5,f(x,z,w))))=f(y,u,f(x,z,w)). 480 [] f(x,f(y,z,u),f(z,x,f(y,u,w)))=f(z,x,f(y,u,w)). 481 [] f(x,f(x,y,f(z,u,y)),f(z,u,w))=f(x,y,f(z,u,w)). 482 [] f(f(A,f(x,D,E),f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 483 [] f(f(A,f(x,D,f(y,D,E)),f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 484 [] f(x,f(x,y,z),f(u,y,f(y,z,w)))=f(x,y,z). 485 [] f(x,f(x,y,z),f(y,u,f(z,w,f(y,z,w5))))=f(x,y,z). 486 [] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). 487 [] f(x,f(x,y,f(z,u,w)),f(y,w5,f(y,z,w)))=f(x,y,f(z,u,w)). 488 [] f(x,f(x,y,f(z,u,w)),f(y,w5,f(y,u,w)))=f(x,y,f(z,u,w)). 489 [] f(x,f(x,y,f(z,u,w)),f(y,z,w))=f(x,y,f(z,u,w)). 490 [] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)). 491 [] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)). 492 [] f(f(x,y,z),f(x,z,u),f(w,u,f(x,z,u)))=f(x,z,u). 493 [] f(f(x,y,z),f(y,z,u),f(w,u,f(y,z,u)))=f(y,z,u). 494 [] f(f(x,y,z),f(x,y,u),f(w,u,f(x,y,u)))=f(x,y,u). 495 [] f(x,y,f(y,z,f(u,x,y)))=f(y,z,f(u,x,y)). 496 [] f(x,f(x,y,z),f(x,z,f(u,y,z)))=f(x,y,z). 497 [] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,w))=f(y,z,f(x,z,u)). 498 [] f(x,y,f(z,u,f(u,x,y)))=f(u,x,y). 499 [] f(x,y,f(z,u,f(x,u,y)))=f(x,u,y). 500 [] f(x,f(y,z,f(x,z,u)),f(u,w,f(x,z,u)))=f(x,z,u). 501 [] f(z,y,f(u,x,y))=f(x,y,f(z,u,y)). 502 [] f(z,y,f(x,u,y))=f(x,y,f(z,u,y)). 503 [] f(x,f(x,y,f(z,y,u)),f(w,z,f(x,z,y)))=f(x,z,y). 504 [] f(x,f(y,z,f(y,x,u)),f(u,w,f(y,x,u)))=f(y,x,u). 505 [] f(x,f(x,y,f(y,z,u)),f(y,z,f(x,z,w)))=f(x,y,z). 506 [] f(x,f(x,y,f(y,z,u)),f(z,w,f(x,y,z)))=f(x,y,z). 507 [] f(x,f(x,y,f(y,z,u)),f(u,w,f(x,y,u)))=f(x,y,u). 508 [] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(x,y,f(y,z,u)). 509 [] f(x,y,f(f(x,z,u),f(y,u,w),f(z,u,f(x,y,u))))=f(x,y,u). 510 [] f(f(x,y,z),f(u,y,w),f(u,y,f(x,y,w)))=f(x,y,f(u,y,w)). 511 [] f(f(x,y,z),f(y,u,w),f(y,u,f(x,y,w)))=f(y,w,f(x,y,u)). 512 [] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(u,w,w5)))=f(y,z,u). 513 [] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). 514 [] f(x,f(x,y,z),f(x,f(y,z,u),f(y,z,w)))=f(x,y,z). 515 [] f(f(x,y,z),f(x,y,f(y,u,z)),f(y,u,w))=f(x,y,f(y,u,z)). 516 [] f(f(x,y,z),f(x,u,w),f(x,u,f(x,z,w)))=f(x,w,f(x,z,u)). 517 [] f(f(x,y,z),f(y,u,w),f(y,u,f(y,z,w)))=f(y,w,f(y,z,u)). 518 [] f(x,f(x,y,z),f(f(x,y,z),f(x,u,w),f(y,z,w5)))=f(x,y,z). 519 [] f(f(x,y,z),f(x,f(x,y,z),f(x,u,w)),f(y,z,w5))=f(x,y,z). 520 [] f(x,f(y,z,x),f(f(u,y,z),f(y,z,x),f(x,w,w5)))=f(y,z,x). 521 [] f(x,f(y,z,u),f(y,z,f(z,x,u)))=f(y,z,f(z,x,u)). 522 [] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). 523 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). 524 [] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(w,f(x,y,z),f(x,z,u)). 525 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,y,f(x,z,u)). 526 [] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). 527 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,z,f(x,y,u)). 528 [] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(x,z,f(y,z,u)). 529 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,u,f(x,y,z)). 530 [] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(z,u,f(x,y,z)). 531 [] f(x,y,f(f(x,y,z),f(x,y,u),f(y,z,u)))=f(x,y,f(y,z,u)). 532 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 533 [] f(x,f(y,z,x),f(z,x,u))=f(x,u,f(y,z,x)). 534 [] f(f(x,y,z),f(y,z,u),f(y,z,f(x,z,u)))=f(z,u,f(x,y,z)). 535 [] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(u,f(x,y,z),f(x,z,w)). 536 [] f(x,f(y,z,x),f(y,x,u))=f(x,u,f(y,z,x)). 537 [] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(y,f(x,z,u),f(x,z,w)). 538 [] f(y,f(w,z,u),f(z,u,x))=f(x,f(y,z,u),f(w,z,u)). 539 [] f(x,f(y,x,z),f(x,u,z))=f(y,x,f(x,u,z)). 540 [] f(f(x,y,z),f(u,y,z),f(y,z,f(x,u,z)))=f(x,z,f(u,y,z)). 541 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(y,z,f(x,z,u)))=f(x,z,u). 542 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,f(x,y,z),f(x,z,u)). 543 [] f(x,f(y,z,u),f(z,u,f(x,y,u)))=f(u,f(x,z,u),f(y,z,u)). 544 [] f(x,f(y,z,x),f(y,x,f(y,u,z)))=f(y,z,x). 545 [] f(x,f(y,x,z),f(y,u,z))=f(y,x,z). 546 [] f(f(x,y,z),f(x,y,u),f(w,u,f(y,u,f(x,u,w5))))=f(x,y,u). 547 [] f(f(x,y,z),f(y,z,u),f(u,w,f(z,u,f(y,u,w5))))=f(y,z,u). 548 [] f(f(x,y,z),f(x,z,f(x,y,u)),f(w,y,z))=f(x,y,z). 549 [] f(x,y,f(z,y,f(u,x,y)))=f(z,y,f(u,x,y)). 550 [] f(f(x,y,z),f(x,u,f(y,z,u)),f(y,z,u))=f(y,z,u). 551 [] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)). 552 [] f(f(x,y,f(y,z,u)),f(x,z,u),f(y,z,u))=f(y,z,u). 553 [] f(x,f(x,y,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(x,y,z). 554 [] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(y,z,f(z,u,f(x,y,z))). 555 [] f(x,f(x,y,z),f(f(y,u,w),f(y,u,z),f(y,w,z)))=f(x,y,z). 556 [] f(x,f(y,z,u),f(y,x,u))=f(y,x,u). 557 [] f(x,y,f(f(x,z,u),f(z,y,w),f(z,y,f(x,z,w))))=f(x,z,y). 558 [] f(x,y,f(f(z,x,u),f(z,y,w),f(z,y,f(z,x,w))))=f(z,x,y). 559 [] f(x,f(y,z,u),f(x,w,f(z,w,f(y,u,w5))))=f(x,w,f(y,z,u)). 560 [] f(x,f(y,z,u),f(w,f(x,z,w),f(y,u,w5)))=f(x,w,f(y,z,u)). 561 [] f(x,y,f(x,f(z,y,u),f(y,u,f(x,z,u))))=f(x,y,u). 562 [] f(x,f(y,z,u),f(u,x,w))=f(x,w,f(y,u,f(z,u,x))). 563 [] f(x,f(y,z,u),f(z,f(y,w,f(y,w5,u)),f(y,z,u)))=f(y,z,u). 564 [] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(w,w5,w6)))=f(y,z,u). 565 [] f(f(x,y,z),f(x,f(x,y,z),f(u,w,w5)),f(y,z,w6))=f(x,y,z). 566 [] f(x,f(x,y,z),f(z,f(x,y,z),f(u,w,w5)))=f(x,y,z). 567 [] f(x,y,f(z,f(x,y,z),f(u,w,w5)))=f(x,y,z). 568 [] f(x,y,f(f(x,y,z),f(u,z,f(x,y,z)),f(w,w5,w6)))=f(x,y,z). 569 [] f(x,y,f(f(x,y,z),f(x,z,f(y,z,u)),f(w,w5,w6)))=f(x,y,z). 570 [] f(x,y,f(x,z,f(f(y,u,z),f(y,u,w),f(y,z,w))))=f(x,y,z). 571 [] f(x,f(y,z,u),f(z,x,u))=f(z,x,u). 572 [] f(y,f(z,x,u),f(z,u,w))=f(x,f(y,z,u),f(z,u,w)). 573 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,f(x,y,u),f(x,z,u)). 574 [] f(x,y,f(z,y,f(f(x,u,z),f(x,u,y),f(x,z,y))))=f(x,z,y). 575 [] f(x,f(y,z,f(y,u,w)),f(y,u,x))=f(y,u,x). 576 [] f(x,y,f(z,u,f(f(x,y,u),f(x,z,u),f(y,z,u))))=f(x,y,u). 577 [] f(f(x,y,f(y,z,f(x,y,u))),f(x,z,u),f(y,z,u))=f(y,z,u). 578 [] f(f(x,y,f(y,z,f(x,y,u))),f(x,u,z),f(y,u,z))=f(y,u,z). 579 [] f(x,f(y,z,u),f(y,z,f(y,x,u)))=f(y,f(y,x,z),f(y,x,u)). 580 [] f(x,f(y,z,u),f(y,u,f(y,x,z)))=f(y,z,f(y,x,u)). 581 [] f(x,f(y,z,f(u,z,x)),f(y,x,f(u,y,z)))=f(y,z,x). 582 [] f(x,y,f(f(z,x,u),f(z,y,u),f(x,y,u)))=f(x,y,u). 583 [] f(x,y,f(f(x,y,z),f(x,z,u),f(y,z,w)))=f(x,y,z). 584 [] f(x,y,f(f(z,x,y),f(z,x,u),f(z,y,w)))=f(z,x,y). 585 [] f(x,f(x,y,f(z,y,u)),f(x,u,f(z,y,u)))=f(x,y,u). 586 [] f(f(x,y,z),f(x,u,z),f(y,z,f(x,u,z)))=f(y,z,f(x,u,z)). 587 [] f(f(x,y,f(z,u,y)),f(z,u,w),f(z,u,y))=f(z,u,y). 588 [] f(f(x,y,f(z,u,y)),f(z,w,u),f(z,u,y))=f(z,u,y). 589 [] f(x,y,f(f(x,z,u),f(x,z,f(z,u,y)),f(z,u,y)))=f(x,z,y). 590 [] f(x,y,f(z,u,f(f(x,z,u),f(x,u,y),f(z,u,y))))=f(x,u,y). 591 [] f(x,y,f(z,u,f(f(z,u,x),f(z,u,y),f(u,x,y))))=f(u,x,y). 592 [] f(x,y,f(z,u,f(f(x,z,u),f(x,z,y),f(z,u,y))))=f(x,z,y). 593 [] f(x,y,f(x,z,f(f(z,u,y),f(z,u,w),f(z,y,w))))=f(x,z,y). 594 [] f(x,f(y,x,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(y,x,z). 595 [] f(x,f(x,y,z),f(f(x,y,z),f(y,u,w),f(y,w,z)))=f(x,y,z). 596 [] f(x,f(y,x,z),f(f(y,u,w),f(y,w,z),f(y,x,z)))=f(y,x,z). 597 [] f(x,f(y,z,x),f(f(y,u,z),f(y,u,w),f(y,z,x)))=f(y,z,x). 598 [] f(x,f(x,y,z),f(f(x,y,z),f(y,u,w),f(y,u,z)))=f(x,y,z). 599 [] f(x,f(y,x,z),f(f(y,u,w),f(y,u,z),f(y,x,z)))=f(y,x,z). 600 [] f(f(x,y,z),f(x,u,z),f(y,u,f(x,y,z)))=f(x,y,z). 601 [] f(f(x,y,z),f(x,u,f(y,u,z)),f(y,u,z))=f(y,u,z). 602 [] f(x,f(y,x,z),f(u,w,f(y,u,x)))=f(x,f(y,u,x),f(y,x,z)). 603 [] f(x,f(y,x,z),f(f(y,u,z),f(y,x,z),f(u,x,z)))=f(y,x,z). 604 [] f(x,f(y,z,x),f(x,f(u,y,z),f(y,z,w)))=f(y,z,x). 605 [] f(x,f(x,y,z),f(x,f(u,y,z),f(y,z,w)))=f(x,y,z). 606 [] f(w,f(y,z,u),f(z,u,x))=f(x,f(y,z,u),f(z,u,w)). 607 [] f(B,f(A,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 608 [] f(A,f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 609 [] f(z,f(y,u,x),f(y,u,w))=f(x,f(y,z,u),f(y,u,w)). 610 [] f(x,f(x,y,z),f(u,f(w,y,z),f(y,z,w5)))=f(x,y,z). 611 [] f(x,f(y,z,f(x,z,u)),f(y,u,w))=f(x,z,f(y,u,w)). 612 [] f(x,f(y,z,u),f(u,w,f(x,y,w)))=f(x,w,f(y,z,u)). 613 [] f(x,f(y,x,f(y,z,u)),f(x,u,f(y,z,u)))=f(y,x,u). 614 [] f(x,y,f(z,u,f(f(z,x,u),f(z,x,y),f(z,u,y))))=f(z,x,y). 615 [] f(x,f(y,z,f(y,u,x)),f(u,w,z))=f(y,x,f(u,w,z)). 616 [] f(x,f(y,x,z),f(u,w,f(y,u,x)))=f(x,z,f(y,u,x)). 617 [] f(x,f(y,x,f(z,y,u)),f(u,w,f(y,x,u)))=f(y,x,u). 618 [] f(x,f(y,z,u),f(z,u,f(y,x,w)))=f(z,u,f(y,x,w)). 619 [] f(f(x,y,z),f(x,u,z),f(u,z,f(x,u,w)))=f(x,u,z). 620 [] f(f(x,y,z),f(x,u,w),f(y,u,w))=f(u,w,f(x,y,z)). 621 [] f(f(x,y,z),f(x,u,w),f(z,u,w))=f(u,w,f(x,y,z)). 622 [] f(f(x,y,z),f(x,u,w),f(u,w,f(y,z,w5)))=f(u,w,f(x,y,z)). 623 [] f(f(x,y,z),f(x,u,w),f(y,z,w))=f(y,z,f(x,u,w)). 624 [] f(f(x,y,z),f(x,z,u),f(y,w,u))=f(x,z,f(y,w,u)). 625 [] f(f(x,y,z),f(x,u,w),f(z,u,f(y,u,w)))=f(u,w,f(x,y,z)). 626 [] f(f(A,C,f(B,D,E)),f(A,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 627 [] f(D,E,f(A,C,f(B,D,E)))!=f(D,E,f(A,B,C)). 628 [] f(D,E,f(f(A,B,C),f(A,C,E),f(B,D,E)))!=f(D,E,f(A,B,C)). 629 [] f(D,E,f(A,B,C))!=f(D,E,f(A,B,C)). 630 [] f(f(x,v,w),f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)) # label("original"). 631 [] f(f(x,f(x,v,w),f(x,v,w)),f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 632 [] f(f(x,f(x,v,f(y,v,w)),f(x,v,w)),f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 633 [] f(y,f(x,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 634 [] f(x,f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 635 [] f(f(x,z,f(y,v,w)),f(x,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 636 [] f(v,w,f(x,z,f(y,v,w)))=f(v,w,f(x,y,z)). 637 [] f(v,w,f(f(x,y,z),f(x,z,w),f(y,v,w)))=f(v,w,f(x,y,z)). 638 [] f(v,w,f(x,y,z))=f(v,w,f(x,y,z)). end_of_list. list(hints2). 639 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)) # label("Hint 1(1)"). 640 [] f(y,x,z)=f(x,y,z) # label("Hint 2(2)"). 641 [] f(x,x,y)=x # label("Hint 3(5)"). 642 [] f(x,y,x)=x # label("Hint 4(6)"). 643 [] f(y,x,x)=x # label("Hint 5(7)"). 644 [] f(y,x,z)=f(x,y,z) # label("Hint 6(8)"). 645 [] f(x,z,y)=f(x,y,z) # label("Hint 7(9)"). 646 [] f(z,y,x)=f(x,y,z) # label("Hint 8(10)"). 647 [] f(x,y,f(x,y,z))=f(x,y,z) # label("Hint 9(11)"). 648 [] f(x,y,f(x,z,y))=f(x,y,z) # label("Hint 10(12)"). 649 [] f(x,y,f(z,x,y))=f(x,y,z) # label("Hint 11(15)"). 650 [] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z) # label("Hint 12(17)"). 651 [] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z) # label("Hint 13(19)"). 652 [] f(y,x,f(x,z,f(y,z,u)))=f(x,y,z) # label("Hint 14(29)"). 653 [] f(y,x,f(z,x,f(u,y,z)))=f(x,y,z) # label("Hint 15(39)"). 654 [] f(x,x,y)=x # label("Hint 16(41)"). 655 [] f(y,x,z)=f(x,y,z) # label("Hint 17(42)"). 656 [] f(x,z,y)=f(x,y,z) # label("Hint 18(43)"). 657 [] f(z,y,x)=f(x,y,z) # label("Hint 19(44)"). 658 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)) # label("Hint 20(45)"). 659 [] f(D,E,f(f(A,B,C),f(A,C,E),f(B,D,E)))!=f(D,E,f(A,B,C)) # label("Hint 21(774)"). 660 [] f(x,y,z)=f(x,y,z) # label("Hint 22(862)"). 661 [] f(z,x,f(x,u,y))=f(x,y,f(z,x,u)) # label("Hint 23(863)"). 662 [] f(y,u,f(x,y,z))=f(x,y,f(y,z,u)) # label("Hint 24(864)"). 663 [] x=x # label("Hint 25(865)"). 664 [] f(u,x,f(x,y,f(x,v,z)))=f(x,y,f(x,z,f(u,x,v))) # label("Hint 26(866)"). 665 [] f(x,f(z,x,u),f(x,v,y))=f(x,y,f(z,x,f(x,u,v))) # label("Hint 27(867)"). 666 [] f(x,u,f(z,x,y))=f(x,y,f(z,x,u)) # label("Hint 28(868)"). 667 [] f(z,x,f(u,x,y))=f(x,y,f(z,u,x)) # label("Hint 29(869)"). 668 [] f(x,z,f(x,u,y))=f(x,y,f(x,z,u)) # label("Hint 30(870)"). 669 [] f(y,x,f(x,v,f(x,z,u)))=f(x,f(y,x,z),f(x,u,v)) # label("Hint 31(873)"). 670 [] f(x,y,f(x,z,f(x,y,u)))=f(x,u,f(x,y,z)) # label("Hint 32(882)"). 671 [] f(y,x,f(z,v,f(x,z,u)))=f(x,f(y,x,z),f(z,u,v)) # label("Hint 33(909)"). 672 [] f(x,f(x,y,z),f(x,z,u))=f(x,y,f(x,z,u)) # label("Hint 34(952)"). 673 [] f(y,u,f(x,z,y))=f(x,y,f(z,y,u)) # label("Hint 35(975)"). 674 [] f(x,f(y,z,u),f(z,x,v))=f(x,v,f(y,z,f(z,u,x))) # label("Hint 36(980)"). 675 [] f(x,u,f(x,y,f(z,u,v)))=f(x,y,f(z,u,f(x,u,v))) # label("Hint 37(989)"). 676 [] f(x,f(x,y,z),f(x,u,v))=f(x,y,f(x,u,f(x,v,z))) # label("Hint 38(991)"). 677 [] f(x,f(x,y,z),f(y,u,v))=f(x,z,f(y,v,f(x,y,u))) # label("Hint 39(992)"). 678 [] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)) # label("Hint 40(998)"). 679 [] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)) # label("Hint 41(1005)"). 680 [] f(y,z,f(z,u,f(x,f(y,z,u),f(z,v,w))))=f(x,f(y,z,u),f(z,v,f(z,w,f(y,z,u)))) # label("Hint 42(1007)"). 681 [] f(x,f(x,y,z),f(x,y,u))=f(x,y,f(x,z,u)) # label("Hint 43(1025)"). 682 [] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y) # label("Hint 44(1035)"). 683 [] f(z,f(x,y,z),f(x,y,u))=f(x,f(x,y,z),f(y,z,u)) # label("Hint 45(1040)"). 684 [] f(y,f(x,y,z),f(z,u,v))=f(x,y,f(z,u,f(y,z,v))) # label("Hint 46(1064)"). 685 [] f(v,f(x,z,f(y,z,u)),f(y,z,u))=f(x,f(y,z,u),f(y,z,f(z,u,v))) # label("Hint 47(1066)"). 686 [] f(y,z,f(x,u,f(x,y,v)))=f(x,y,f(y,z,f(x,u,v))) # label("Hint 48(1067)"). 687 [] f(y,f(x,y,z),f(u,w,f(z,u,v)))=f(x,y,f(z,u,f(y,z,f(u,v,w)))) # label("Hint 49(1090)"). 688 [] f(x,z,f(x,y,f(u,v,f(x,u,w))))=f(x,y,f(x,f(x,z,u),f(u,v,w))) # label("Hint 50(1095)"). 689 [] f(v,f(y,z,u),f(z,u,f(x,y,z)))=f(x,f(y,z,u),f(y,z,f(z,u,v))) # label("Hint 51(1115)"). 690 [] f(x,f(y,z,x),f(y,z,u))=f(y,z,x) # label("Hint 52(1132)"). 691 [] f(x,f(y,x,z),f(y,z,u))=f(y,x,z) # label("Hint 53(1139)"). 692 [] f(x,f(x,y,z),f(y,z,u))=f(x,y,z) # label("Hint 54(1148)"). 693 [] f(x,f(y,z,f(x,z,u)),f(z,v,f(y,z,u)))=f(x,z,f(y,z,u)) # label("Hint 55(1166)"). 694 [] f(x,f(x,y,f(y,z,u)),f(y,z,u))=f(x,y,f(y,z,u)) # label("Hint 56(1174)"). 695 [] f(x,f(x,y,z),f(y,u,f(y,z,v)))=f(x,y,z) # label("Hint 57(1176)"). 696 [] f(x,f(y,z,u),f(y,z,x))=f(y,z,x) # label("Hint 58(1178)"). 697 [] f(f(x,y,f(z,u,f(u,y,v))),f(z,u,f(u,y,v)),f(u,w,f(z,u,v)))=f(x,f(z,u,f(u,y,v)),f(u,y,f(z,u,v))) # label("Hint 59(1205)"). 698 [] f(x,f(x,y,z),f(y,u,f(z,v,f(y,z,w))))=f(x,y,z) # label("Hint 60(1299)"). 699 [] f(x,f(x,y,f(z,y,u)),f(y,v,f(z,y,u)))=f(z,y,f(x,y,u)) # label("Hint 61(1319)"). 700 [] f(u,x,f(z,x,y))=f(x,y,f(z,u,x)) # label("Hint 62(1327)"). 701 [] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,v))=f(z,y,u) # label("Hint 63(1362)"). 702 [] f(x,f(y,x,f(z,y,u)),f(y,v,f(z,y,u)))=f(z,y,f(y,u,x)) # label("Hint 64(1364)"). 703 [] f(x,y,f(z,f(y,z,f(y,u,v)),f(y,w,f(y,u,v))))=f(y,f(x,y,u),f(y,v,z)) # label("Hint 65(1515)"). 704 [] f(f(x,y,f(z,u,f(y,u,v))),f(y,u,f(z,u,v)),f(u,w,f(z,u,v)))=f(y,u,f(z,u,v)) # label("Hint 66(1713)"). 705 [] f(f(x,y,f(z,u,f(y,u,v))),f(u,v,f(y,z,u)),f(u,w,f(z,u,v)))=f(y,u,f(z,u,v)) # label("Hint 67(1749)"). 706 [] f(f(x,y,f(z,x,u)),f(x,v,f(z,x,u)),f(y,w,f(x,y,f(z,x,u))))=f(z,x,f(x,u,y)) # label("Hint 68(1929)"). 707 [] f(x,f(y,x,f(y,z,u)),f(y,v,f(y,z,u)))=f(y,z,f(y,x,u)) # label("Hint 69(2038)"). 708 [] f(y,f(x,y,z),f(y,u,v))=f(x,y,f(y,z,f(y,u,v))) # label("Hint 70(2227)"). 709 [] f(x,f(y,x,z),f(x,z,u))=f(y,x,f(x,z,u)) # label("Hint 71(2230)"). 710 [] f(x,f(y,z,u),f(v,f(y,z,u),f(y,z,x)))=f(v,f(y,z,u),f(y,z,x)) # label("Hint 72(2421)"). 711 [] f(f(x,y,z),f(x,u,f(y,z,v)),f(y,z,v))=f(u,f(x,y,z),f(y,z,v)) # label("Hint 73(2478)"). 712 [] f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,v))=f(x,y,z) # label("Hint 74(2612)"). 713 [] f(x,y,f(f(z,x,u),f(z,x,f(z,u,v)),f(x,u,w)))=f(z,x,f(x,u,y)) # label("Hint 75(2650)"). 714 [] f(x,v,f(x,y,f(x,z,f(v,v6,f(u,v,w)))))=f(x,y,f(x,z,f(u,v,f(x,v,f(v,w,v6))))) # label("Hint 76(2656)"). 715 [] f(x,f(x,y,f(x,z,u)),f(x,z,u))=f(x,y,f(x,z,u)) # label("Hint 77(2670)"). 716 [] f(x,y,f(x,z,f(x,u,y)))=f(x,z,f(x,u,y)) # label("Hint 78(2705)"). 717 [] f(x,f(x,y,f(z,u,f(x,z,v))),f(x,z,f(z,v,u)))=f(x,y,f(x,z,f(z,v,u))) # label("Hint 79(2847)"). 718 [] f(f(x,y,z),f(x,y,u),f(v,f(x,y,z),f(u,w,f(x,y,u))))=f(v,f(x,y,z),f(x,y,u)) # label("Hint 80(3276)"). 719 [] f(z,f(y,z,u),f(x,v,f(y,z,u)))=f(x,f(y,z,u),f(z,u,f(y,z,v))) # label("Hint 81(3278)"). 720 [] f(f(x,y,z),f(x,y,u),f(v,u,f(x,y,z)))=f(v,f(x,y,z),f(x,y,u)) # label("Hint 82(3280)"). 721 [] f(f(x,y,z),f(x,y,u),f(u,v,f(x,y,z)))=f(v,f(x,y,z),f(x,y,u)) # label("Hint 83(3301)"). 722 [] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)) # label("Hint 84(3324)"). 723 [] f(x,y,f(f(x,z,u),f(x,z,f(z,u,v)),f(x,u,w)))=f(x,z,f(x,y,u)) # label("Hint 85(3532)"). 724 [] f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,v))=f(x,y,z) # label("Hint 86(3560)"). 725 [] f(f(x,y,f(x,z,u)),f(x,u,f(x,v,f(x,y,z))),f(u,w,f(x,y,z)))=f(x,u,f(x,y,z)) # label("Hint 87(3572)"). 726 [] f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,v)))=f(x,y,u) # label("Hint 88(3620)"). 727 [] f(f(x,y,z),f(x,z,f(x,y,u)),f(y,z,v))=f(x,y,z) # label("Hint 89(3634)"). 728 [] f(f(x,f(y,z,u),f(y,u,f(y,z,v))),f(y,z,u),f(z,u,w))=f(y,z,u) # label("Hint 90(4917)"). 729 [] f(x,y,f(f(y,z,f(x,y,u)),f(y,v,f(x,y,u)),f(w,z,f(y,z,f(x,y,u)))))=f(y,u,f(x,y,z)) # label("Hint 91(5202)"). 730 [] f(x,y,f(y,f(x,y,z),f(x,u,v)))=f(y,z,f(x,v,f(x,y,u))) # label("Hint 92(5226)"). 731 [] f(x,y,f(z,f(z,x,u),f(z,v,w)))=f(x,y,f(z,v,f(z,x,f(z,u,w)))) # label("Hint 93(5229)"). 732 [] f(x,y,f(z,x,f(x,u,y)))=f(z,x,f(x,u,y)) # label("Hint 94(5348)"). 733 [] f(x,y,f(z,f(x,z,u),f(y,z,v)))=f(x,y,z) # label("Hint 95(5568)"). 734 [] f(x,f(y,z,f(x,z,u)),f(z,v,f(z,u,f(x,y,z))))=f(x,z,f(z,u,f(x,y,z))) # label("Hint 96(5721)"). 735 [] f(x,f(y,x,z),f(z,u,f(x,v,z)))=f(y,x,f(v,z,f(x,z,u))) # label("Hint 97(5723)"). 736 [] f(x,f(y,z,f(x,z,u)),f(z,u,f(x,y,z)))=f(x,z,f(z,u,f(x,y,z))) # label("Hint 98(5844)"). 737 [] f(x,f(x,y,z),f(z,u,f(x,z,v)))=f(x,y,f(z,u,f(x,z,v))) # label("Hint 99(5871)"). 738 [] f(x,f(x,y,f(z,u,f(x,z,v))),f(x,z,f(z,u,v)))=f(x,y,f(x,z,f(z,u,v))) # label("Hint 100(6001)"). 739 [] f(x,f(x,y,f(z,u,f(x,v,z))),f(x,w,z))=f(x,y,f(x,w,f(v,z,f(x,z,u)))) # label("Hint 101(6536)"). 740 [] f(x,f(x,y,z),f(u,v,f(x,u,f(u,w,v6))))=f(x,y,f(x,u,f(x,z,f(u,w,f(u,v,v6))))) # label("Hint 102(6561)"). 741 [] f(x,f(x,y,f(z,u,f(x,z,v))),f(x,z,w))=f(x,y,f(x,w,f(z,u,f(x,z,v)))) # label("Hint 103(6591)"). 742 [] f(x,f(x,y,z),f(u,v,f(x,u,f(z,u,w))))=f(x,y,f(x,u,f(z,f(x,z,u),f(u,v,w)))) # label("Hint 104(6809)"). 743 [] f(x,y,f(x,f(z,u,v),f(z,u,f(x,z,v))))=f(x,y,f(x,z,f(z,u,v))) # label("Hint 105(6974)"). 744 [] f(x,f(y,z,u),f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)) # label("Hint 106(7007)"). 745 [] f(x,z,f(x,y,f(z,v,f(z,w,u))))=f(x,y,f(z,f(x,z,u),f(z,v,w))) # label("Hint 107(7160)"). 746 [] f(x,y,f(z,f(x,z,y),f(y,u,v)))=f(x,z,y) # label("Hint 108(7501)"). 747 [] f(x,f(x,y,z),f(u,v,f(x,u,f(z,u,w))))=f(x,y,f(x,z,u)) # label("Hint 109(7771)"). 748 [] f(x,y,f(z,u,f(x,z,f(y,z,v))))=f(x,y,z) # label("Hint 110(7840)"). 749 [] f(f(x,y,f(z,u,f(y,u,v))),f(z,u,f(y,u,v)),f(u,w,f(z,u,v)))=f(x,f(y,u,f(z,u,v)),f(z,u,f(y,u,v))) # label("Hint 111(8284)"). 750 [] f(x,f(y,z,f(u,z,v)),f(u,z,f(y,z,v)))=f(y,z,f(u,z,v)) # label("Hint 112(8392)"). 751 [] f(x,f(y,z,f(u,z,v)),f(z,v,f(u,y,z)))=f(u,z,f(y,z,v)) # label("Hint 113(8402)"). 752 [] f(x,y,f(y,z,f(x,u,y)))=f(x,y,f(u,y,z)) # label("Hint 114(8432)"). 753 [] f(x,f(x,y,z),f(u,y,f(x,y,v)))=f(x,z,f(u,y,f(x,y,v))) # label("Hint 115(8623)"). 754 [] f(v,f(y,z,u),f(y,x,f(y,z,u)))=f(x,f(y,z,u),f(y,v,f(y,z,u))) # label("Hint 116(8647)"). 755 [] f(x,f(y,z,f(z,x,u)),f(z,x,u))=f(z,x,u) # label("Hint 117(8889)"). 756 [] f(x,y,f(z,u,f(y,z,f(x,z,v))))=f(x,y,z) # label("Hint 118(9165)"). 757 [] f(x,y,f(z,u,f(x,u,f(y,u,v))))=f(x,y,u) # label("Hint 119(9179)"). 758 [] f(x,y,f(z,f(x,u,v),f(y,f(x,u,v),f(x,w,f(x,u,v)))))=f(x,v,f(x,u,y)) # label("Hint 120(9861)"). 759 [] f(x,y,f(z,u,f(z,y,f(x,z,v))))=f(x,z,y) # label("Hint 121(10171)"). 760 [] f(x,y,f(z,u,f(x,y,u)))=f(x,y,u) # label("Hint 122(11215)"). 761 [] f(x,y,f(z,u,f(u,x,f(u,y,v))))=f(u,x,y) # label("Hint 123(11245)"). 762 [] f(x,f(z,u,v),f(v6,f(x,y,z),f(x,w,f(x,y,z))))=f(x,f(x,y,f(z,u,f(x,z,v))),f(w,v6,f(x,y,z))) # label("Hint 124(11962)"). 763 [] f(x,f(x,y,f(z,u,v)),f(z,u,v))=f(x,y,f(z,u,v)) # label("Hint 125(11969)"). 764 [] f(x,f(x,y,z),f(u,f(x,f(y,v,w),f(v6,f(x,y,z),f(y,v,w))),f(y,v,w)))=f(x,z,f(y,w,f(x,y,v))) # label("Hint 126(11980)"). 765 [] f(x,y,f(x,z,f(z,u,f(z,y,v))))=f(x,z,y) # label("Hint 127(11984)"). 766 [] f(x,f(x,y,z),f(y,u,f(x,v,f(x,y,w))))=f(x,z,f(y,u,f(x,v,f(x,y,w)))) # label("Hint 128(12003)"). 767 [] f(x,y,f(z,f(x,u,y),f(x,v,f(x,u,y))))=f(x,f(x,u,y),f(v,z,f(x,u,y))) # label("Hint 129(12127)"). 768 [] f(x,f(x,y,f(y,z,f(y,u,f(v,y,w)))),f(v,y,w))=f(y,w,f(x,v,y)) # label("Hint 130(12346)"). 769 [] f(x,f(y,x,z),f(y,u,f(y,z,v)))=f(y,x,z) # label("Hint 131(12497)"). 770 [] f(f(y,z,u),f(y,v,w),f(x,v,f(y,z,u)))=f(x,f(y,z,u),f(v,w,f(y,u,f(y,z,v)))) # label("Hint 132(13248)"). 771 [] f(f(x,y,z),f(x,y,u),f(y,z,f(v,x,y)))=f(v,f(x,y,z),f(y,u,f(x,y,z))) # label("Hint 133(13466)"). 772 [] f(x,f(y,z,f(u,v,f(y,u,w))),f(v6,f(x,y,u),f(y,z,f(u,v,f(y,u,w)))))=f(v6,f(x,y,u),f(y,z,f(u,v,f(y,u,w)))) # label("Hint 134(15209)"). 773 [] f(D,E,f(f(A,B,C),f(A,f(x,C,f(y,E,f(z,C,E))),f(A,C,E)),f(B,D,E)))!=f(D,E,f(A,B,C)) # label("Hint 135(15258)"). 774 [] f(x,f(y,z,u),f(v,f(x,y,u),f(y,z,u)))=f(v,f(x,y,u),f(y,z,u)) # label("Hint 136(15342)"). 775 [] f(x,f(y,z,u),f(y,z,f(y,u,x)))=f(y,x,f(y,z,u)) # label("Hint 137(15872)"). 776 [] f(x,f(y,z,u),f(f(x,v,f(y,z,u)),f(y,z,u),f(y,z,f(x,y,u))))=f(v,f(x,y,f(y,z,u)),f(y,z,u)) # label("Hint 138(16522)"). 777 [] f(x,f(y,z,u),f(z,x,u))=f(z,x,u) # label("Hint 139(16799)"). 778 [] f(x,f(y,z,u),f(z,u,x))=f(z,u,x) # label("Hint 140(17037)"). 779 [] f(x,f(y,z,u),f(v,f(y,z,u),f(z,u,f(x,v,f(y,z,u)))))=f(z,u,f(x,v,f(y,z,u))) # label("Hint 141(17055)"). 780 [] f(x,f(y,z,u),f(y,z,f(z,x,u)))=f(y,z,f(z,x,u)) # label("Hint 142(17742)"). 781 [] f(x,f(x,y,f(z,u,v)),f(y,u,v))=f(x,y,f(z,u,v)) # label("Hint 143(18121)"). 782 [] f(x,f(y,z,u),f(v,f(y,z,u),f(y,u,f(x,v,f(y,z,u)))))=f(y,u,f(x,v,f(y,z,u))) # label("Hint 144(18129)"). 783 [] f(f(x,y,z),f(x,y,f(z,f(y,z,u),f(y,v,u))),f(x,z,w))=f(x,y,z) # label("Hint 145(18153)"). 784 [] f(x,y,f(z,f(y,z,u),f(y,v,u)))=f(y,u,f(x,y,z)) # label("Hint 146(18155)"). 785 [] f(x,y,f(z,u,f(x,u,y)))=f(x,u,y) # label("Hint 147(18678)"). 786 [] f(f(x,y,z),f(x,y,f(z,f(y,z,f(u,v,w)),f(v,w,f(y,u,v)))),f(x,z,v6))=f(x,y,z) # label("Hint 148(18782)"). 787 [] f(x,y,f(z,f(y,z,f(u,v,w)),f(v,w,f(y,u,v))))=f(y,f(x,y,z),f(u,v,w)) # label("Hint 149(18786)"). 788 [] f(f(x,y,z),f(x,z,u),f(y,f(x,y,z),f(v,w,v6)))=f(x,y,z) # label("Hint 150(18832)"). 789 [] f(f(x,y,f(y,z,f(y,u,v))),f(y,z,u),f(z,u,w))=f(y,z,u) # label("Hint 151(19393)"). 790 [] f(f(x,y,z),f(x,u,v),f(x,v,f(x,y,z)))=f(x,v,f(x,y,z)) # label("Hint 152(19397)"). 791 [] f(f(x,y,f(x,z,u)),f(x,z,f(x,v,f(x,y,u))),f(x,w,v))=f(x,v,f(x,y,f(x,z,u))) # label("Hint 153(19431)"). 792 [] f(f(x,y,f(z,x,u)),f(x,f(z,x,u),f(v,w,f(z,x,u))),f(v,w,f(z,x,u)))=f(z,x,f(x,u,f(v,w,f(z,x,u)))) # label("Hint 154(19517)"). 793 [] f(f(x,y,z),f(x,z,f(x,y,u)),f(x,u,v))=f(x,u,f(x,y,z)) # label("Hint 155(19869)"). 794 [] f(x,f(y,z,f(y,u,f(x,y,v))),f(u,w,f(x,y,u)))=f(x,y,u) # label("Hint 156(20404)"). 795 [] f(x,y,f(z,u,f(u,x,y)))=f(u,x,y) # label("Hint 157(20432)"). 796 [] f(f(x,y,z),f(y,u,f(y,v,f(x,y,f(y,z,w)))),f(v,v6,f(y,v,f(x,y,z))))=f(y,v,f(x,y,z)) # label("Hint 158(20502)"). 797 [] f(x,f(y,z,f(z,u,f(x,z,v))),f(u,w,f(x,z,u)))=f(x,u,f(y,z,f(z,u,f(x,z,v)))) # label("Hint 159(21482)"). 798 [] f(x,y,f(z,u,f(u,y,f(x,u,v))))=f(x,u,y) # label("Hint 160(21508)"). 799 [] f(z,y,f(x,u,y))=f(x,y,f(z,u,y)) # label("Hint 161(21514)"). 800 [] f(x,f(y,z,u),f(z,v,f(z,x,f(z,w,f(y,z,u)))))=f(z,x,f(y,z,u)) # label("Hint 162(21517)"). 801 [] f(u,f(x,y,z),f(x,y,f(x,z,v)))=f(x,f(x,y,z),f(u,v,f(x,y,z))) # label("Hint 163(23572)"). 802 [] f(f(x,y,z),f(y,u,f(x,y,z)),f(f(x,y,z),f(x,z,v),f(w,v6,v7)))=f(x,y,z) # label("Hint 164(24235)"). 803 [] f(f(x,y,z),f(x,y,u),f(u,f(x,y,u),f(v,w,v6)))=f(x,y,u) # label("Hint 165(24313)"). 804 [] f(x,f(x,y,z),f(f(x,y,z),f(y,z,u),f(v,w,v6)))=f(x,y,z) # label("Hint 166(24325)"). 805 [] f(x,f(y,x,z),f(f(y,x,z),f(y,z,u),f(v,w,v6)))=f(y,x,z) # label("Hint 167(24453)"). 806 [] f(x,f(x,y,f(y,z,u)),f(f(x,y,f(y,z,u)),f(y,v,f(y,z,u)),f(w,v6,v7)))=f(y,u,f(x,y,z)) # label("Hint 168(25061)"). 807 [] f(x,f(y,f(x,y,z),f(x,u,z)),f(f(x,y,z),f(y,z,v),f(w,v6,v7)))=f(x,y,z) # label("Hint 169(25644)"). 808 [] f(f(x,y,f(z,y,u)),f(z,y,u),f(f(z,y,u),f(z,u,v),f(w,v6,v7)))=f(z,y,u) # label("Hint 170(25796)"). 809 [] f(f(x,y,f(x,z,u)),f(x,f(x,z,u),f(v,w,f(x,z,u))),f(v,w,f(x,z,u)))=f(x,z,f(x,u,f(v,w,f(x,z,u)))) # label("Hint 171(26362)"). 810 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,v,f(x,z,u)))=f(x,z,u) # label("Hint 172(26364)"). 811 [] f(x,f(y,z,x),f(f(y,z,x),f(y,z,u),f(v,w,v6)))=f(y,z,x) # label("Hint 173(26393)"). 812 [] f(f(x,y,f(y,z,f(y,u,v))),f(y,z,v),f(z,v,w))=f(y,z,v) # label("Hint 174(26918)"). 813 [] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,v))=f(z,u,f(x,y,z)) # label("Hint 175(26962)"). 814 [] f(f(x,y,f(y,z,f(y,u,v))),f(y,v,z),f(v,z,w))=f(y,v,z) # label("Hint 176(27036)"). 815 [] f(f(x,y,z),f(y,u,v),f(y,u,f(x,y,v)))=f(y,v,f(x,y,u)) # label("Hint 177(27085)"). 816 [] f(x,y,f(z,u,f(x,u,f(u,v,y))))=f(x,u,y) # label("Hint 178(27103)"). 817 [] f(f(x,y,z),f(x,u,v),f(x,u,f(x,z,v)))=f(x,v,f(x,z,u)) # label("Hint 179(27113)"). 818 [] f(x,f(y,z,u),f(y,u,x))=f(y,u,x) # label("Hint 180(27178)"). 819 [] f(x,y,f(z,u,f(u,x,f(u,v,y))))=f(u,x,y) # label("Hint 181(27197)"). 820 [] f(x,f(y,z,x),f(f(y,z,u),f(y,z,x),f(v,w,v6)))=f(y,z,x) # label("Hint 182(27258)"). 821 [] f(x,f(y,z,u),f(x,u,f(v,y,z)))=f(x,u,f(v,y,z)) # label("Hint 183(27303)"). 822 [] f(x,f(y,z,u),f(u,x,f(v,y,z)))=f(u,x,f(v,y,z)) # label("Hint 184(27312)"). 823 [] f(x,f(y,z,u),f(u,x,f(y,z,v)))=f(u,x,f(y,z,v)) # label("Hint 185(27403)"). 824 [] f(f(x,y,z),f(y,u,f(x,z,v)),f(y,u,f(u,w,f(x,z,v))))=f(y,u,f(x,z,v)) # label("Hint 186(27531)"). 825 [] f(x,f(y,z,u),f(z,x,f(y,u,v)))=f(z,x,f(y,u,v)) # label("Hint 187(27539)"). 826 [] f(x,f(y,z,f(x,y,u)),f(u,z,v))=f(x,y,f(u,z,v)) # label("Hint 188(27551)"). 827 [] f(f(x,y,z),f(x,z,u),f(v,y,f(y,z,f(x,y,w))))=f(x,y,z) # label("Hint 189(27602)"). 828 [] f(x,f(y,z,u),f(y,x,u))=f(y,x,u) # label("Hint 190(28269)"). 829 [] f(x,f(y,z,u),f(y,v,f(x,z,v)))=f(x,v,f(y,z,u)) # label("Hint 191(28987)"). 830 [] f(f(x,y,f(y,z,f(u,y,v))),f(u,y,z),f(u,z,w))=f(u,y,z) # label("Hint 192(29121)"). 831 [] f(f(x,y,f(z,y,f(u,y,v))),f(z,u,y),f(z,u,w))=f(z,u,y) # label("Hint 193(29540)"). 832 [] f(x,y,f(x,z,f(u,v,f(x,y,z))))=f(x,f(x,y,z),f(u,v,z)) # label("Hint 194(30300)"). 833 [] f(x,f(x,y,z),f(u,v,f(x,y,z)))=f(x,f(x,y,z),f(z,u,v)) # label("Hint 195(30302)"). 834 [] f(x,f(y,z,u),f(y,z,f(y,u,v)))=f(y,f(y,z,u),f(u,x,v)) # label("Hint 196(30314)"). 835 [] f(f(x,y,z),f(x,z,u),f(y,f(v,x,y),f(y,z,w)))=f(x,y,z) # label("Hint 197(31169)"). 836 [] f(f(x,y,z),f(x,y,u),f(x,y,v))=f(u,f(x,y,z),f(x,y,v)) # label("Hint 198(32143)"). 837 [] f(v,f(y,z,u),f(y,z,x))=f(x,f(y,z,u),f(y,z,v)) # label("Hint 199(32160)"). 838 [] f(f(x,y,z),f(x,y,u),f(x,u,v))=f(x,f(x,y,u),f(z,u,v)) # label("Hint 200(32309)"). 839 [] f(f(x,y,z),f(u,v,y),f(u,y,z))=f(y,f(x,u,v),f(u,y,z)) # label("Hint 201(32605)"). 840 [] f(f(x,y,z),f(x,y,u),f(u,f(x,v,u),f(y,u,w)))=f(x,y,u) # label("Hint 202(35265)"). 841 [] f(x,y,f(z,f(u,x,y),f(x,z,v)))=f(x,f(u,z,v),f(x,y,z)) # label("Hint 203(35312)"). 842 [] f(D,E,f(A,B,C))!=f(D,E,f(A,B,C)) # label("Hint 204(35470)"). 843 [] f(v,w,f(f(x,y,z),f(x,z,w),f(y,v,w)))=f(v,w,f(x,y,z)) # label("Hint 21(774)"). 844 [] f(v,w,f(f(x,y,z),f(x,f(x,z,f(y,w,f(z,z,w))),f(x,z,w)),f(y,v,w)))=f(v,w,f(x,y,z)) # label("Hint 135(15258)"). 845 [] f(v,w,f(x,y,z))=f(v,w,f(x,y,z)) # label("Hint 204(35470)"). end_of_list. list(hints2). 846 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 847 [] f(y,x,z)=f(x,y,z). 848 [] f(x,x,y)=x. 849 [] f(x,y,x)=x. 850 [] f(y,x,x)=x. 851 [] f(y,x,z)=f(x,y,z). 852 [] f(x,z,y)=f(x,y,z). 853 [] f(z,y,x)=f(x,y,z). 854 [] f(x,x,y)=x. 855 [] f(y,x,z)=f(x,y,z). 856 [] f(x,z,y)=f(x,y,z). 857 [] f(z,y,x)=f(x,y,z). 858 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 859 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)) # label("original"). 860 [] f(x,y,z)=f(x,y,z) # label("Hint 204(35470)"). 861 [] f(z,x,f(x,u,y))=f(x,y,f(z,x,u)) # label("Hint 24(864)"). 862 [] f(u,x,f(x,y,f(x,w,z)))=f(x,y,f(x,z,f(u,x,w))). 863 [] f(x,f(y,x,z),f(x,u,w))=f(x,w,f(y,x,f(x,z,u))) # label("Hint 27(867)"). 864 [] f(x,u,f(z,x,y))=f(x,y,f(z,x,u)) # label("Hint 28(868)"). 865 [] f(z,x,f(u,x,y))=f(x,y,f(z,u,x)) # label("Hint 35(975)"). 866 [] f(x,z,f(x,u,y))=f(x,y,f(x,z,u)). 867 [] f(z,x,f(x,y,u))=f(x,y,f(z,x,u)). 868 [] f(y,x,f(x,w,f(x,z,u)))=f(x,f(y,x,z),f(x,u,w)). 869 [] f(y,x,f(z,w,f(x,z,f(z,u,w5))))=f(x,f(y,x,z),f(z,u,f(z,w,w5))). 870 [] f(x,f(x,y,f(x,z,u)),f(u,w,w5))=f(x,f(x,y,z),f(u,w5,f(x,u,w))). 871 [] f(y,x,f(z,f(x,z,w5),f(z,u,w)))=f(x,f(y,x,z),f(z,u,f(z,w,w5))). 872 [] f(y,z,f(z,u,f(w,x,f(y,z,u))))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 873 [] f(y,z,f(z,u,f(x,w,f(y,z,u))))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 874 [] f(z,x,f(x,y,f(z,u,w)))=f(x,y,f(z,u,f(z,w,x))). 875 [] f(w,f(y,z,u),f(z,u,f(y,z,x)))=f(x,f(y,z,u),f(z,w,f(y,z,u))). 876 [] f(x,y,f(x,y,z))=f(x,y,z) # label("Hint 9(11)"). 877 [] f(y,x,f(z,u,f(x,z,w)))=f(x,f(y,x,z),f(z,u,w)) # label("Hint 46(1064)"). 878 [] f(x,f(y,x,z),f(x,u,f(y,x,z)))=f(y,x,f(x,z,u)). 879 [] f(x,f(x,y,f(x,z,u)),f(x,w,f(x,y,f(x,z,u))))=f(x,z,f(x,u,f(x,y,w))). 880 [] f(x,y,f(z,x,y))=f(z,x,y). 881 [] f(x,y,f(x,z,y))=f(x,z,y). 882 [] f(x,y,f(y,z,f(u,x,y)))=f(y,z,f(u,x,y)). 883 [] f(x,u,f(x,w,f(x,z,y)))=f(x,y,f(x,z,f(x,u,w))). 884 [] f(z,f(y,z,u),f(w5,f(y,z,u),f(x,w,f(y,z,u))))=f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(z,u,w5)))). 885 [] f(x,y,f(x,z,f(x,u,y)))=f(x,u,f(x,y,z)). 886 [] f(x,z,f(u,y,f(x,y,w)))=f(x,y,f(x,z,f(u,y,w))) # label("Hint 37(989)"). 887 [] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,w,f(x,y,u))) # label("Hint 39(992)"). 888 [] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)) # label("Hint 40(998)"). 889 [] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y) # label("Hint 44(1035)"). 890 [] f(y,f(y,x,z),f(x,z,u))=f(x,f(y,x,z),f(y,z,u)). 891 [] f(x,z,f(y,u,f(x,y,w)))=f(x,y,f(x,z,f(y,u,w))). 892 [] f(y,z,f(y,x,f(z,x,u)))=f(x,f(y,z,x),f(y,z,u)). 893 [] f(z,y,f(x,y,u))=f(x,y,f(z,y,u)). 894 [] f(x,y,f(z,u,f(x,y,z)))=f(x,y,z) # label(bd). 895 [] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). 896 [] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z) # label("Hint 12(17)"). 897 [] f(x,y,f(z,u,f(x,y,u)))=f(x,y,u) # label("Hint 122(11215)"). 898 [] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). 899 [] f(z,f(z,x,y),f(x,y,u))=f(x,y,f(z,x,f(z,y,u))). 900 [] f(y,z,f(y,x,f(z,w,f(z,x,u))))=f(x,f(y,z,x),f(y,z,f(z,u,w))). 901 [] f(x,f(x,y,z),f(x,u,f(z,w,w5)))=f(x,u,f(x,y,f(z,w,f(x,z,w5)))). 902 [] f(x,f(x,y,z),f(x,u,f(y,z,w)))=f(x,u,f(y,f(x,y,z),f(x,z,w))). 903 [] f(x,f(x,y,f(x,z,u)),f(u,w,f(x,y,z)))=f(x,u,f(x,y,z)). 904 [] f(z,f(z,x,y),f(x,y,f(y,w,u)))=f(x,y,f(z,x,f(y,u,f(z,y,w)))). 905 [] f(x,f(x,y,z),f(y,z,u))=f(x,y,z) # label("Hint 54(1148)"). 906 [] f(x,f(y,z,x),f(y,z,u))=f(y,z,x) # label("Hint 52(1132)"). 907 [] f(x,f(y,x,z),f(y,z,u))=f(y,x,z) # label("Hint 53(1139)"). 908 [] f(x,f(x,y,z),f(x,u,f(y,z,w)))=f(x,u,f(x,y,z)). 909 [] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u) # label("Hint 63(1362)"). 910 [] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). 911 [] f(f(x,y,z),f(x,y,f(y,u,z)),f(x,z,w))=f(x,y,z). 912 [] f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,w))=f(x,y,z) # label("Hint 74(2612)"). 913 [] f(f(x,y,z),f(x,z,f(u,x,y)),f(y,z,w))=f(x,y,z). 914 [] f(f(x,y,z),f(x,z,u),f(y,w,f(x,y,z)))=f(x,y,z). 915 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). 916 [] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,u)))=f(x,y,u). 917 [] f(f(x,y,z),f(y,u,f(x,y,w)),f(z,w5,f(x,y,z)))=f(x,y,z). 918 [] f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,w)))=f(x,y,u) # label("Hint 88(3620)"). 919 [] f(f(x,y,z),f(x,y,u),f(x,u,f(u,w,f(y,u,w5))))=f(x,y,u). 920 [] f(f(x,y,z),f(x,y,u),f(x,z,f(y,z,w)))=f(x,y,z). 921 [] f(f(x,y,z),f(x,y,u),f(y,u,f(x,u,w)))=f(x,y,u). 922 [] f(f(x,y,z),f(x,u,f(x,z,w)),f(y,w5,f(x,y,z)))=f(x,y,z). 923 [] f(x,f(y,z,u),f(y,z,x))=f(y,z,x) # label("Hint 58(1178)"). 924 [] f(x,f(y,x,z),f(y,u,f(y,z,w)))=f(y,x,z) # label("Hint 131(12497)"). 925 [] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(x,w,f(y,z,u)))))=f(y,z,f(x,w,f(y,z,u))). 926 [] f(u,x,f(z,x,y))=f(x,y,f(z,u,x)). 927 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,w,f(x,z,u)))=f(x,z,u) # label("Hint 172(26364)"). 928 [] f(f(x,y,z),f(x,z,u),f(u,w,f(x,z,u)))=f(x,z,u). 929 [] f(f(x,y,z),f(y,z,u),f(u,w,f(y,z,u)))=f(y,z,u). 930 [] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,x)))=f(w,f(y,z,u),f(y,z,x)) # label("Hint 72(2421)"). 931 [] f(f(x,y,z),f(x,u,f(y,z,w)),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)) # label("Hint 73(2478)"). 932 [] f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,w)))=f(x,z,u). 933 [] f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,w)))=f(y,z,u). 934 [] f(f(x,y,z),f(y,z,u),f(z,u,f(u,w,f(y,u,w5))))=f(y,z,u). 935 [] f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,w)))=f(y,z,u). 936 [] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). 937 [] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(y,u,f(x,y,z)). 938 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w) # label("Hint 174(26918)"). 939 [] f(x,f(y,z,u),f(z,u,x))=f(z,u,x) # label("Hint 140(17037)"). 940 [] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). 941 [] f(f(x,y,z),f(x,u,f(y,w,f(x,y,z))),f(x,u,f(u,w5,f(y,w,f(x,y,z)))))=f(x,u,f(y,w,f(x,y,z))). 942 [] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). 943 [] f(f(x,y,z),f(z,u,f(y,w,f(x,y,z))),f(z,u,f(u,w5,f(y,w,f(x,y,z)))))=f(z,u,f(y,w,f(x,y,z))). 944 [] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). 945 [] f(x,f(y,z,f(x,y,u)),f(y,w,f(y,z,u)))=f(x,y,f(y,z,u)). 946 [] f(x,f(y,z,u),f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)) # label("Hint 106(7007)"). 947 [] f(f(A,D,E),f(B,D,E),f(C,f(x,D,E),f(C,D,E)))!=f(D,E,f(A,B,C)). 948 [] f(f(B,D,E),f(C,D,E),f(C,f(A,D,E),f(B,D,E)))!=f(D,E,f(A,B,C)). 949 [] f(f(x,y,z),f(x,z,f(x,y,u)),f(x,u,w))=f(x,u,f(x,y,z)) # label("Hint 155(19869)"). 950 [] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,w))=f(z,u,f(x,y,z)) # label("Hint 175(26962)"). 951 [] f(f(x,y,f(z,u,y)),f(z,u,y),f(z,u,w))=f(z,u,y). 952 [] f(f(x,y,z),f(y,u,f(x,z,w)),f(y,u,f(u,w5,f(x,z,w))))=f(y,u,f(x,z,w)) # label("Hint 186(27531)"). 953 [] f(x,f(y,z,u),f(z,x,f(y,u,w)))=f(z,x,f(y,u,w)) # label("Hint 187(27539)"). 954 [] f(x,f(x,y,z),f(u,y,f(y,z,w)))=f(x,y,z). 955 [] f(x,f(x,y,z),f(y,u,f(y,w,z)))=f(x,y,z). 956 [] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)) # label("Hint 143(18121)"). 957 [] f(x,y,f(z,u,f(u,x,y)))=f(u,x,y) # label("Hint 157(20432)"). 958 [] f(x,y,f(z,u,f(x,u,y)))=f(x,u,y) # label("Hint 147(18678)"). 959 [] f(z,y,f(x,u,y))=f(x,y,f(z,u,y)) # label("Hint 161(21514)"). 960 [] f(x,f(y,z,f(x,z,u)),f(x,z,u))=f(x,z,u). 961 [] f(x,f(y,z,f(y,u,w)),f(y,u,x))=f(y,u,x). 962 [] f(f(x,y,z),f(y,z,f(x,z,u)),f(z,u,w))=f(z,u,f(x,y,z)). 963 [] f(f(x,y,z),f(u,y,w),f(u,y,f(x,y,w)))=f(x,y,f(u,y,w)). 964 [] f(f(x,y,z),f(y,u,w),f(y,u,f(x,y,w)))=f(y,w,f(x,y,u)) # label("Hint 177(27085)"). 965 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,u),f(z,u,w5))=f(y,z,u) # label("Hint 151(19393)"). 966 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,w,z),f(w,z,w5))=f(y,w,z) # label("Hint 176(27036)"). 967 [] f(f(x,y,f(x,z,f(x,u,w))),f(x,z,w),f(z,w,w5))=f(x,z,w). 968 [] f(x,y,f(z,u,f(x,u,f(y,u,w))))=f(x,y,u) # label("Hint 119(9179)"). 969 [] f(x,f(y,z,f(z,x,f(z,u,w))),f(z,x,w))=f(z,x,w). 970 [] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). 971 [] f(f(x,y,z),f(x,y,u),f(z,w,f(x,z,f(y,z,w5))))=f(x,y,z). 972 [] f(x,y,f(f(x,z,u),f(w,w5,z),f(w,z,f(x,w5,z))))=f(x,z,f(x,y,f(w,w5,z))). 973 [] f(x,y,f(f(x,z,u),f(y,z,w),f(z,w,f(x,y,z))))=f(x,y,z). 974 [] f(f(x,y,z),f(x,y,f(y,u,z)),f(y,u,w))=f(x,y,f(y,u,z)). 975 [] f(f(x,y,z),f(x,u,w),f(x,u,f(x,z,w)))=f(x,w,f(x,z,u)) # label("Hint 179(27113)"). 976 [] f(f(x,y,z),f(y,u,w),f(y,u,f(y,z,w)))=f(y,w,f(y,z,u)). 977 [] f(x,y,f(f(x,z,u),f(y,u,w),f(u,w,f(x,y,u))))=f(x,y,u). 978 [] f(x,y,f(y,f(x,y,z),f(x,u,z)))=f(x,y,z). 979 [] f(x,y,f(f(z,x,u),f(z,y,w),f(z,w,f(z,x,y))))=f(z,x,y). 980 [] f(x,f(y,z,u),f(y,z,f(z,x,u)))=f(y,z,f(z,x,u)) # label("Hint 142(17742)"). 981 [] f(x,f(y,z,x),f(y,u,f(y,z,w)))=f(y,z,x). 982 [] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). 983 [] f(x,y,f(z,y,f(u,x,y)))=f(z,y,f(u,x,y)). 984 [] f(x,y,f(z,x,f(x,u,y)))=f(z,x,f(x,u,y)) # label("Hint 94(5348)"). 985 [] f(x,f(y,x,z),f(x,u,z))=f(y,x,f(x,u,z)). 986 [] f(x,f(y,z,x),f(z,x,u))=f(x,u,f(y,z,x)). 987 [] f(f(x,y,z),f(x,u,f(y,z,u)),f(y,z,u))=f(y,z,u). 988 [] f(f(x,y,z),f(x,u,z),f(y,u,f(x,y,z)))=f(x,y,z). 989 [] f(x,f(y,x,z),f(y,u,z))=f(y,x,z). 990 [] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(u,w,w5)))=f(y,z,u). 991 [] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). 992 [] f(f(x,y,z),f(x,u,f(y,u,z)),f(y,u,z))=f(y,u,z). 993 [] f(x,y,f(x,z,f(z,u,y)))=f(x,z,y). 994 [] f(x,f(x,y,z),f(f(x,y,z),f(x,u,w),f(y,z,w5)))=f(x,y,z). 995 [] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,x,y) # label("Hint 181(27197)"). 996 [] f(x,y,f(z,u,f(x,u,f(u,w,y))))=f(x,u,y) # label("Hint 178(27103)"). 997 [] f(x,f(y,z,u),f(y,x,u))=f(y,x,u) # label("Hint 190(28269)"). 998 [] f(x,f(x,y,z),f(x,f(y,z,u),f(y,z,w)))=f(x,y,z). 999 [] f(x,f(x,y,f(z,u,y)),f(z,u,w))=f(x,y,f(z,u,w)). 1000 [] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). 1001 [] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(w,f(x,y,z),f(x,z,u)). 1002 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). 1003 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,y,f(x,z,u)). 1004 [] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(x,z,f(y,z,u)). 1005 [] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,u,f(x,y,z)). 1006 [] f(x,f(x,y,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(x,y,z). 1007 [] f(x,f(x,y,z),f(f(y,z,u),f(y,z,w),f(y,u,w)))=f(x,y,z). 1008 [] f(x,y,f(f(x,y,z),f(x,y,u),f(y,z,u)))=f(x,y,f(y,z,u)). 1009 [] f(x,f(x,y,z),f(f(y,u,w),f(y,u,z),f(y,w,z)))=f(x,y,z). 1010 [] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(u,f(x,y,z),f(x,z,w)). 1011 [] f(x,f(y,z,x),f(y,x,u))=f(x,u,f(y,z,x)). 1012 [] f(x,y,f(z,u,f(f(x,y,u),f(x,z,u),f(y,z,u))))=f(x,y,u). 1013 [] f(x,y,f(z,u,f(f(z,u,x),f(z,u,y),f(u,x,y))))=f(u,x,y). 1014 [] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)) # label("Hint 84(3324)"). 1015 [] f(x,f(y,z,x),f(y,x,f(y,u,z)))=f(y,z,x). 1016 [] f(x,f(y,z,u),f(z,x,u))=f(z,x,u) # label("Hint 139(16799)"). 1017 [] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). 1018 [] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). 1019 [] f(x,f(y,z,u),f(y,z,f(y,x,u)))=f(y,f(y,x,z),f(y,x,u)). 1020 [] f(x,y,f(f(x,z,u),f(z,y,w),f(z,y,f(x,z,w))))=f(x,z,y). 1021 [] f(x,y,f(f(z,x,u),f(z,y,w),f(z,y,f(z,x,w))))=f(z,x,y). 1022 [] f(x,f(y,z,u),f(u,x,w))=f(x,w,f(y,u,f(z,u,x))). 1023 [] f(x,f(y,z,u),f(z,f(y,w,f(y,w5,u)),f(y,z,u)))=f(y,z,u). 1024 [] f(x,y,f(z,u,f(f(x,z,u),f(x,y,u),f(z,y,u))))=f(x,y,u). 1025 [] f(x,f(y,z,u),f(x,w,f(z,w,f(y,u,w5))))=f(x,w,f(y,z,u)). 1026 [] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)) # label("Hint 183(27303)"). 1027 [] f(x,f(y,x,f(y,z,u)),f(x,u,f(y,z,u)))=f(y,x,u). 1028 [] f(x,f(x,y,z),f(f(x,y,z),f(y,u,w),f(y,w,z)))=f(x,y,z). 1029 [] f(x,f(x,y,f(z,y,u)),f(z,u,w))=f(x,y,f(z,u,w)). 1030 [] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)) # label("Hint 188(27551)"). 1031 [] f(x,f(y,x,z),f(f(y,u,w),f(y,w,z),f(y,x,z)))=f(y,x,z). 1032 [] f(x,f(y,z,x),f(f(y,u,z),f(y,u,w),f(y,z,x)))=f(y,z,x). 1033 [] f(x,f(y,z,u),f(z,w,f(y,w,x)))=f(w,x,f(y,z,u)). 1034 [] f(x,f(y,z,u),f(y,u,f(y,x,z)))=f(y,z,f(y,x,u)). 1035 [] f(f(x,y,z),f(x,y,f(u,w,w5)),f(u,w,w5))=f(x,y,f(u,w,w5)). 1036 [] f(x,f(x,y,z),f(f(x,y,z),f(y,z,u),f(w,w5,w6)))=f(x,y,z) # label("Hint 166(24325)"). 1037 [] f(f(x,y,f(z,x,u)),f(x,f(z,x,u),f(w,w5,w6)),f(w,w5,w6))=f(z,x,f(x,u,f(w,w5,w6))) # label("Hint 154(19517)"). 1038 [] f(x,y,f(x,z,f(f(y,u,z),f(y,u,w),f(y,z,w))))=f(x,y,z). 1039 [] f(x,y,f(x,z,f(f(z,u,y),f(z,u,w),f(z,y,w))))=f(x,z,y). 1040 [] f(x,f(y,x,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(y,x,z). 1041 [] f(f(x,y,f(x,z,u)),f(x,f(x,z,u),f(w,w5,w6)),f(w,w5,w6))=f(x,z,f(x,u,f(w,w5,w6))) # label("Hint 171(26362)"). 1042 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,w,u))=f(x,z,u). 1043 [] f(x,f(y,z,u),f(z,u,f(y,x,w)))=f(z,u,f(y,x,w)). 1044 [] f(f(x,y,z),f(u,w,w5),f(w,w5,f(y,z,u)))=f(w,w5,f(y,z,u)). 1045 [] f(f(x,y,z),f(x,y,f(x,z,u)),f(y,w,z))=f(x,y,z). 1046 [] f(f(x,y,z),f(y,z,u),f(y,z,f(x,u,w)))=f(y,z,f(x,u,w)). 1047 [] f(f(x,y,z),f(y,u,z),f(y,u,f(u,z,w)))=f(y,u,z). 1048 [] f(x,f(y,x,z),f(u,f(w,y,z),f(y,x,z)))=f(y,x,z). 1049 [] f(f(x,y,z),f(x,y,f(u,w,z)),f(u,w,w5))=f(x,y,f(u,w,z)). 1050 [] f(x,f(y,z,u),f(y,z,f(w,x,u)))=f(y,z,f(w,x,u)) # label("Hint 142(17742)"). 1051 [] f(x,y,f(z,u,f(x,y,w)))=f(x,y,f(z,u,w)) # label("Hint 41(1005)"). 1052 [] f(f(x,y,z),f(u,w,f(u,y,z)),f(u,y,z))=f(u,y,z). 1053 [] f(x,f(y,x,z),f(f(y,u,w),f(y,u,z),f(y,w,z)))=f(y,x,z). 1054 [] f(f(x,y,f(z,y,f(u,y,w))),f(z,u,y),f(z,u,w5))=f(z,u,y) # label("Hint 193(29540)"). 1055 [] f(f(x,y,z),f(x,u,w),f(y,u,w))=f(u,w,f(x,y,z)). 1056 [] f(f(x,y,z),f(y,u,w),f(z,u,w))=f(u,w,f(x,y,z)). 1057 [] f(f(x,y,z),f(x,u,w),f(z,u,w))=f(u,w,f(x,y,z)). 1058 [] f(f(x,y,z),f(x,u,w),f(u,w,f(y,z,w5)))=f(u,w,f(x,y,z)). 1059 [] f(f(x,y,z),f(x,u,w),f(y,u,w))=f(u,w,f(x,y,f(z,u,w))). 1060 [] f(x,f(x,y,z),f(f(u,w,w5),f(u,y,z),f(w,y,z)))=f(x,y,z). 1061 [] f(f(x,y,z),f(x,u,w),f(y,z,w))=f(y,z,f(x,u,w)). 1062 [] f(x,f(x,y,z),f(f(u,w,w5),f(u,y,z),f(w5,y,z)))=f(x,y,z). 1063 [] f(x,f(x,y,z),f(f(u,y,z),f(u,w,w5),f(y,z,w5)))=f(x,y,z). 1064 [] f(f(x,y,z),f(x,u,w),f(z,u,f(y,u,w)))=f(u,w,f(x,y,z)). 1065 [] f(f(B,C,f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). 1066 [] f(D,E,f(B,C,f(A,D,E)))!=f(D,E,f(A,B,C)). 1067 [] f(f(A,B,C),f(B,D,E),f(C,D,E))!=f(D,E,f(B,C,f(A,D,E))). 1068 [] f(x,f(x,y,z),f(f(x,y,z),f(u,w,w5),f(w5,y,z)))=f(x,y,z). 1069 [] f(x,f(x,y,z),f(f(u,w,w5),f(w5,y,z),f(x,y,z)))=f(x,y,z). 1070 [] f(x,f(y,z,x),f(f(u,y,z),f(u,w,w5),f(y,z,x)))=f(y,z,x). 1071 [] f(f(x,y,z),f(y,u,w),f(z,u,w))=f(u,w,f(y,z,f(x,u,w))). 1072 [] f(f(x,v,w),f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)) # label("original"). 1073 [] f(f(x,v,w),f(y,v,w),f(z,f(x,v,w),f(z,v,w)))=f(v,w,f(x,y,z)). 1074 [] f(f(y,v,w),f(z,v,w),f(z,f(x,v,w),f(y,v,w)))=f(v,w,f(x,y,z)). 1075 [] f(f(y,z,f(x,v,w)),f(y,v,w),f(z,v,w))=f(v,w,f(x,y,z)). 1076 [] f(v,w,f(y,z,f(x,v,w)))=f(v,w,f(x,y,z)). 1077 [] f(f(x,y,z),f(y,v,w),f(z,v,w))=f(v,w,f(y,z,f(x,v,w))). end_of_list. lex dependent demodulator: 13 [] f(x,y,z)=f(y,x,z). lex dependent demodulator: 14 [] f(x,y,z)=f(x,z,y). lex dependent demodulator: 15 [] f(x,y,z)=f(z,y,x). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=-2147483647) 2 [] f(x,x,y)=x. given clause #2: (wt=-2147483647) 3 [] f(x,y,z)=f(y,x,z). given clause #3: (wt=-2147483647) 4 [] f(x,y,z)=f(x,z,y). given clause #4: (wt=-2147483647) 5 [] f(x,y,z)=f(z,y,x). given clause #5: (wt=-2147483647) 6 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). >> BACK DEMODULATING HINT 876 WITH 1128. >> BACK DEMODULATING HINT 647 WITH 1128. >> BACK DEMODULATING HINT 363 WITH 1128. >> BACK DEMODULATING HINT 16 WITH 1128. given clause #6: (wt=-2147483647) 7 [] f(f(A,B,C),D,E)!=f(f(A,D,E),f(B,D,E),f(C,D,E)) # label("original"). given clause #7: (wt=-2147483647) 8 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(f(A,B,C),D,E) # label("original"). given clause #8: (wt=-2147483647) 9 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)) # label("original"). given clause #9: (wt=-1021) 1078 [para_into,2.1.1,2.1.1] x=x # label("Hint 204(35470)"). given clause #10: (wt=-1003) 1127 (heat=1) [para_into,1082.1.1,1.1.2,demod,15,11,15,13] f(x,y,f(x,y,z))=f(x,y,z) # label("Hint 9(11)"). >> BACK DEMODULATING HINT 880 WITH 1245. >> BACK DEMODULATING HINT 649 WITH 1245. >> BACK DEMODULATING HINT 365 WITH 1245. >> BACK DEMODULATING HINT 68 WITH 1245. >> BACK DEMODULATING HINT 20 WITH 1245. >> BACK DEMODULATING HINT 881 WITH 1247. >> BACK DEMODULATING HINT 879 WITH 1247. NEW HINT: 1279 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,w,f(x,y,f(x,z,u)))=f(x,z,f(x,u,f(x,y,w))). >> BACK DEMODULATING HINT 878 WITH 1247. NEW HINT: 1280 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,u,f(x,y,z))=f(x,y,f(x,z,u)). >> BACK DEMODULATING HINT 648 WITH 1247. >> BACK DEMODULATING HINT 364 WITH 1247. >> BACK DEMODULATING HINT 17 WITH 1247. given clause #11: (wt=39) 1079 [para_into,6.1.1.1,6.1.2,demod,15,13,15,13,13,15,13] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,y,f(x,w,z))). given clause #12: (wt=-1003) 1244 [para_from,1127.1.2,5.1.2,demod,15,13,flip.1] f(x,y,f(z,x,y))=f(z,x,y). given clause #13: (wt=-1003) 1246 [para_from,1127.1.2,4.1.2,demod,14,flip.1] f(x,y,f(x,z,y))=f(x,z,y). given clause #14: (wt=-997) 1081 [para_into,6.1.1.1,5.1.2,demod,15,13,13] f(x,y,f(z,x,u))=f(x,u,f(z,x,y)) # label("Hint 28(868)"). given clause #15: (wt=-997) 1082 [para_into,6.1.1.1,4.1.2,demod,15,13] f(x,y,f(z,u,x))=f(z,x,f(u,x,y)) # label("Hint 35(975)"). given clause #16: (wt=-987) 1080 [para_into,6.1.1.1,6.1.1,demod,13,15,13,13,13,flip.1] f(x,f(y,x,z),f(x,u,w))=f(x,w,f(y,x,f(x,z,u))) # label("Hint 27(867)"). >> BACK DEMODULATING HINT 765 WITH 2001. NEW HINT: 2302 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,y,f(x,z,f(z,u,f(y,z,w))))=f(x,y,z) # label(bd). >> BACK DEMODULATING HINT 889 WITH 2274. >> BACK DEMODULATING HINT 682 WITH 2274. >> BACK DEMODULATING HINT 409 WITH 2274. >> BACK DEMODULATING HINT 898 WITH 2305. >> BACK DEMODULATING HINT 441 WITH 2305. >> BACK DEMODULATING HINT 440 WITH 2305. >> BACK DEMODULATING HINT 895 WITH 2315. >> BACK DEMODULATING HINT 652 WITH 2315. >> BACK DEMODULATING HINT 369 WITH 2315. >> BACK DEMODULATING HINT 34 WITH 2315. >> BACK DEMODULATING HINT 695 WITH 2465. given clause #17: (wt=-997) 1086 [para_into,6.1.1,4.1.2,demod,15,13] f(x,y,f(z,x,u))=f(z,x,f(x,u,y)) # label("Hint 24(864)"). given clause #18: (wt=-997) 1748 [para_into,1082.1.2,1079.1.1,demod,10,14,15,14,13,1128,flip.1] f(x,y,f(z,y,u))=f(z,y,f(x,y,u)). >> BACK DEMODULATING HINT 894 WITH 2819. given clause #19: (wt=-997) 2273 (heat=1) [para_into,1931.1.2.3,1.1.2,demod,14,1634,15,13,flip.1] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y) # label("Hint 44(1035)"). >> BACK DEMODULATING HINT 897 WITH 2901. >> BACK DEMODULATING HINT 760 WITH 2901. >> BACK DEMODULATING HINT 452 WITH 2901. >> BACK DEMODULATING HINT 449 WITH 2901. >> BACK DEMODULATING HINT 896 WITH 2903. >> BACK DEMODULATING HINT 892 WITH 2903. NEW HINT: 3037 [bsub_wt=2147483647, bsub_add_wt=-1024] f(y,z,f(x,y,f(x,z,u)))=f(x,f(x,y,z),f(y,z,u)). >> BACK DEMODULATING HINT 650 WITH 2903. >> BACK DEMODULATING HINT 366 WITH 2903. >> BACK DEMODULATING HINT 22 WITH 2903. >> BACK DEMODULATING HINT 2302 WITH 3039. given clause #20: (wt=-997) 2304 [back_demod,1853,demod,13,13,1739,13,flip.1] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). given clause #21: (wt=27) 1083 [para_into,6.1.1.1,3.1.2,demod,15,13,13,13] f(x,y,f(x,z,u))=f(x,z,f(x,u,y)). >> BACK DEMODULATING HINT 904 WITH 3407. NEW HINT: 3426 [bsub_wt=2147483647, bsub_add_wt=-1024] f(z,f(x,y,z),f(x,y,f(y,u,w)))=f(x,y,f(x,z,f(y,u,f(y,z,w)))). given clause #22: (wt=-997) 2314 (heat=1) [para_into,2303.1.2,1.1.2,demod,12,11] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). >> BACK DEMODULATING HINT 651 WITH 3494. >> BACK DEMODULATING HINT 367 WITH 3494. >> BACK DEMODULATING HINT 24 WITH 3494. >> BACK DEMODULATING HINT 3037 WITH 3502. >> BACK DEMODULATING HINT 905 WITH 3502. >> BACK DEMODULATING HINT 904 WITH 3502. >> BACK DEMODULATING HINT 899 WITH 3502. >> BACK DEMODULATING HINT 890 WITH 3502. >> BACK DEMODULATING HINT 692 WITH 3502. >> BACK DEMODULATING HINT 683 WITH 3502. >> BACK DEMODULATING HINT 415 WITH 3502. >> BACK DEMODULATING HINT 410 WITH 3502. >> BACK DEMODULATING HINT 3037 WITH 3614. >> BACK DEMODULATING HINT 899 WITH 3614. >> BACK DEMODULATING HINT 30 WITH 3614. >> BACK DEMODULATING HINT 3426 WITH 3616. >> BACK DEMODULATING HINT 900 WITH 3616. NEW HINT: 3832 [bsub_wt=2147483647, bsub_add_wt=-1024] f(y,z,f(x,y,f(z,w,f(x,z,u))))=f(x,y,z). >> BACK DEMODULATING HINT 907 WITH 3659. >> BACK DEMODULATING HINT 902 WITH 3659. >> BACK DEMODULATING HINT 890 WITH 3659. >> BACK DEMODULATING HINT 691 WITH 3659. >> BACK DEMODULATING HINT 414 WITH 3659. >> BACK DEMODULATING HINT 910 WITH 3668. >> BACK DEMODULATING HINT 417 WITH 3668. >> BACK DEMODULATING HINT 909 WITH 3852. >> BACK DEMODULATING HINT 701 WITH 3852. >> BACK DEMODULATING HINT 464 WITH 3852. >> BACK DEMODULATING HINT 506 WITH 4071. >> BACK DEMODULATING HINT 942 WITH 4089. >> BACK DEMODULATING HINT 372 WITH 4089. >> BACK DEMODULATING HINT 40 WITH 4089. >> BACK DEMODULATING HINT 430 WITH 4366. NEW HINT: 4371 [bsub_wt=2147483647, bsub_add_wt=-1024] f(f(x,y,z),f(x,u,f(x,w,f(x,y,z))),f(w,f(x,u,f(x,w,f(x,y,z))),f(x,w,f(x,y,z))))=f(x,z,f(x,y,w)). >> BACK DEMODULATING HINT 981 WITH 4376. given clause #23: (wt=-1000) 3667 (heat=1) [para_from,3501.1.1,1.1.2.3,demod,14,12] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). >> BACK DEMODULATING HINT 419 WITH 4416. >> BACK DEMODULATING HINT 912 WITH 4420. NEW HINT: 4674 [bsub_wt=2147483647, bsub_add_wt=-1024] f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,w))=f(x,y,z) # label(bd). >> BACK DEMODULATING HINT 712 WITH 4420. >> BACK DEMODULATING HINT 418 WITH 4420. >> BACK DEMODULATING HINT 915 WITH 4427. >> BACK DEMODULATING HINT 420 WITH 4427. >> BACK DEMODULATING HINT 477 WITH 4450. >> BACK DEMODULATING HINT 755 WITH 4452. >> BACK DEMODULATING HINT 916 WITH 4456. >> BACK DEMODULATING HINT 421 WITH 4456. >> BACK DEMODULATING HINT 917 WITH 4938. >> BACK DEMODULATING HINT 422 WITH 4938. >> BACK DEMODULATING HINT 914 WITH 5062. >> BACK DEMODULATING HINT 423 WITH 5062. >> BACK DEMODULATING HINT 3426 WITH 5140. >> BACK DEMODULATING HINT 906 WITH 5140. >> BACK DEMODULATING HINT 900 WITH 5140. >> BACK DEMODULATING HINT 892 WITH 5140. >> BACK DEMODULATING HINT 690 WITH 5140. >> BACK DEMODULATING HINT 683 WITH 5140. >> BACK DEMODULATING HINT 413 WITH 5140. >> BACK DEMODULATING HINT 410 WITH 5140. >> BACK DEMODULATING HINT 424 WITH 5288. given clause #24: (wt=-1000) 3851 (heat=1) [para_from,3658.1.1,1.1.2.3,demod,14,12] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u) # label("Hint 63(1362)"). >> BACK DEMODULATING HINT 911 WITH 5312. >> BACK DEMODULATING HINT 913 WITH 5318. >> BACK DEMODULATING HINT 457 WITH 5318. given clause #25: (wt=-1000) 4415 [para_into,3667.1.1.1,2304.1.2,demod,13,2274,13] f(f(x,y,z),f(x,u,f(x,y,z)),f(y,z,w))=f(x,y,z). >> BACK DEMODULATING HINT 727 WITH 5645. >> BACK DEMODULATING HINT 4674 WITH 5647. >> BACK DEMODULATING HINT 713 WITH 5647. >> BACK DEMODULATING HINT 724 WITH 5960. >> BACK DEMODULATING HINT 723 WITH 5960. NEW HINT: 5965 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,z,f(x,y,u))=f(x,y,f(x,z,u)) # label(bd). given clause #26: (wt=39) 1084 [para_into,6.1.1,6.1.2,demod,15,13,15,13,13,13] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,w,f(x,z,y))). given clause #27: (wt=-1000) 4419 [para_into,3667.1.1.1,1086.1.2,demod,13,14,13,13,14] f(f(x,y,z),f(x,y,f(x,u,z)),f(y,z,w))=f(x,y,z) # label("Hint 74(2612)"). >> BACK DEMODULATING HINT 920 WITH 6949. >> BACK DEMODULATING HINT 427 WITH 6970. >> BACK DEMODULATING HINT 918 WITH 7014. >> BACK DEMODULATING HINT 726 WITH 7014. >> BACK DEMODULATING HINT 428 WITH 7014. >> BACK DEMODULATING HINT 919 WITH 7446. given clause #28: (wt=-1000) 4426 [para_into,3667.1.1.1,3.1.2] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). >> BACK DEMODULATING HINT 927 WITH 7694. >> BACK DEMODULATING HINT 810 WITH 7694. >> BACK DEMODULATING HINT 4371 WITH 7732. NEW HINT: 7944 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,w,f(x,y,z))=f(x,z,f(x,y,w)). given clause #29: (wt=-1000) 4455 [para_into,3667.1.1,5.1.2,demod,15,13,15,13,13,15,13] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,u)))=f(x,y,u). >> BACK DEMODULATING HINT 928 WITH 7994. >> BACK DEMODULATING HINT 432 WITH 7994. >> BACK DEMODULATING HINT 929 WITH 7996. >> BACK DEMODULATING HINT 431 WITH 7996. >> BACK DEMODULATING HINT 923 WITH 8050. >> BACK DEMODULATING HINT 696 WITH 8050. >> BACK DEMODULATING HINT 433 WITH 8050. given clause #30: (wt=-1000) 5061 [para_from,3667.1.2,3.1.2,demod,13,13,13,15,13,flip.1] f(f(x,y,z),f(x,z,u),f(y,w,f(x,y,z)))=f(x,y,z). >> BACK DEMODULATING HINT 922 WITH 8741. >> BACK DEMODULATING HINT 924 WITH 8887. >> BACK DEMODULATING HINT 769 WITH 8887. given clause #31: (wt=27) 1085 [para_into,6.1.1,5.1.2,demod,13,15,13,flip.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)). >> BACK DEMODULATING HINT 746 WITH 9216. >> BACK DEMODULATING HINT 742 WITH 9216. >> BACK DEMODULATING HINT 733 WITH 9259. given clause #32: (wt=-1000) 5311 [para_into,3851.1.1.1,1748.1.2,demod,13,13] f(f(x,y,z),f(x,y,f(y,u,z)),f(x,z,w))=f(x,y,z). given clause #33: (wt=-1000) 5317 [para_into,3851.1.1.1,6.1.2,demod,15,13,13,13,13] f(f(x,y,z),f(x,z,f(u,x,y)),f(y,z,w))=f(x,y,z). >> BACK DEMODULATING HINT 921 WITH 10127. >> BACK DEMODULATING HINT 438 WITH 10127. given clause #34: (wt=-1000) 5644 [para_into,4415.1.1.2,1083.1.2,demod,14] f(f(x,y,z),f(x,z,f(x,y,u)),f(y,z,w))=f(x,y,z) # label("Hint 89(3634)"). given clause #35: (wt=-1000) 5646 [para_into,4415.1.1.2,1083.1.1] f(f(x,y,z),f(x,y,f(x,z,u)),f(y,z,w))=f(x,y,z) # label(bd). given clause #36: (wt=37) 1087 [para_into,6.1.2.3,6.1.2,demod,13,13,13,15,13] f(x,f(y,x,z),f(x,u,w))=f(y,x,f(x,w,f(x,z,u))). >> BACK DEMODULATING HINT 938 WITH 11634. >> BACK DEMODULATING HINT 812 WITH 11634. >> BACK DEMODULATING HINT 465 WITH 11634. given clause #37: (wt=-1000) 5959 (heat=1) [para_into,5853.1.1,1.1.2,demod,14,3500,14,3494,1128] f(f(x,y,z),f(x,y,f(y,z,u)),f(x,z,w))=f(x,y,z) # label("Hint 86(3560)"). given clause #38: (wt=-1000) 6948 [para_into,4419.1.1.1,2304.1.2,demod,15,13,2819,15,14,13,14,15,13] f(f(x,y,z),f(x,y,u),f(x,z,f(y,z,w)))=f(x,y,z). given clause #39: (wt=-1000) 6969 [para_into,4419.1.1.1,5.1.2,demod,15,14,13,13,14,15] f(f(x,y,z),f(x,y,u),f(y,z,f(x,z,w)))=f(x,y,z). given clause #40: (wt=-1000) 7013 [para_into,4419.1.1,5.1.2,demod,15,14,13,15,13,14,15,13] f(f(x,y,z),f(x,y,u),f(x,u,f(y,u,w)))=f(x,y,u) # label("Hint 88(3620)"). >> BACK DEMODULATING HINT 453 WITH 14245. >> BACK DEMODULATING HINT 935 WITH 14247. >> BACK DEMODULATING HINT 444 WITH 14247. >> BACK DEMODULATING HINT 932 WITH 14249. >> BACK DEMODULATING HINT 443 WITH 14249. >> BACK DEMODULATING HINT 933 WITH 14271. >> BACK DEMODULATING HINT 442 WITH 14271. >> BACK DEMODULATING HINT 934 WITH 14467. given clause #41: (wt=39) 1088 [para_into,6.1.2.3,6.1.1,demod,13,15,13,13,13] f(x,y,f(z,x,f(x,u,w)))=f(z,x,f(x,u,f(x,w,y))). >> BACK DEMODULATING HINT 748 WITH 15806. given clause #42: (wt=-1000) 7993 [para_into,4455.1.1.1,2304.1.2,demod,15,13,2819,13,13,13] f(f(x,y,z),f(x,z,u),f(u,w,f(x,z,u)))=f(x,z,u). >> BACK DEMODULATING HINT 818 WITH 16055. >> BACK DEMODULATING HINT 790 WITH 16055. >> BACK DEMODULATING HINT 450 WITH 16055. >> BACK DEMODULATING HINT 936 WITH 16069. >> BACK DEMODULATING HINT 699 WITH 16069. NEW HINT: 16397 [bsub_wt=2147483647, bsub_add_wt=-1024] f(y,z,f(x,y,u))=f(x,y,f(y,z,u)) # label(bd). >> BACK DEMODULATING HINT 451 WITH 16069. given clause #43: (wt=-1000) 7995 [para_into,4455.1.1.1,2304.1.1] f(f(x,y,z),f(y,z,u),f(u,w,f(y,z,u)))=f(y,z,u). >> BACK DEMODULATING HINT 939 WITH 16863. >> BACK DEMODULATING HINT 778 WITH 16863. >> BACK DEMODULATING HINT 445 WITH 16863. >> BACK DEMODULATING HINT 940 WITH 16877. >> BACK DEMODULATING HINT 631 WITH 16877. NEW HINT: 17197 [bsub_wt=2147483647, bsub_add_wt=-1024] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(y,z,f(x,u,w)). >> BACK DEMODULATING HINT 446 WITH 16877. given clause #44: (wt=-1000) 10126 [para_into,5317.1.1,5.1.2,demod,15,13,15,13,14,15,13] f(f(x,y,z),f(x,y,u),f(y,u,f(x,u,w)))=f(x,y,u). given clause #45: (wt=-1000) 14244 [para_into,7013.1.1.1,2304.1.2,demod,15,13,2819,13,13] f(f(x,y,z),f(x,z,u),f(z,u,f(x,u,w)))=f(x,z,u). given clause #46: (wt=51) 1089 (heat=1) [para_into,1079.1.1.3.3,1.1.2,demod,13,15,13,13,14,13,flip.1] f(x,y,f(x,z,f(x,u,f(x,w,w5))))=f(x,z,f(x,u,f(x,w5,f(x,y,w)))). given clause #47: (wt=-1000) 14246 [para_into,7013.1.1.1,2304.1.1] f(f(x,y,z),f(y,z,u),f(y,u,f(z,u,w)))=f(y,z,u). >> BACK DEMODULATING HINT 43 WITH 20437. >> BACK DEMODULATING HINT 4371 WITH 20442. >> BACK DEMODULATING HINT 944 WITH 20442. >> BACK DEMODULATING HINT 374 WITH 20442. >> BACK DEMODULATING HINT 45 WITH 20442. given clause #48: (wt=-1000) 14248 [para_into,7013.1.1.1,2273.1.2,demod,14,2819] f(f(x,y,z),f(x,z,u),f(x,u,f(z,u,w)))=f(x,z,u). >> BACK DEMODULATING HINT 42 WITH 21203. given clause #49: (wt=-1000) 14270 [para_into,7013.1.1.1,5.1.2,demod,13,13] f(f(x,y,z),f(y,z,u),f(z,u,f(y,u,w)))=f(y,z,u). given clause #50: (wt=-999) 3501 [para_into,2314.1.1,1086.1.2,demod,13,14,13] f(x,f(x,y,z),f(y,z,u))=f(x,y,z) # label("Hint 54(1148)"). reducing weight limit to 25. given clause #51: (wt=49) 1090 (heat=1) [para_into,1079.1.1.3.3,1.1.1,demod,13,13,13,14,15,13,flip.1] f(x,f(x,y,f(x,z,u)),f(x,w,w5))=f(x,y,f(x,z,f(x,w,f(x,w5,u)))). given clause #52: (wt=-1000) 22818 (heat=1) [para_into,22472.1.1,1.1.2,demod,15,14,15,13] f(f(B,D,E),f(C,D,E),f(C,f(A,D,E),f(B,D,E)))!=f(D,E,f(A,B,C)). given clause #53: (wt=-999) 3658 [back_demod,2613,demod,15,14,3502,15,14,13,flip.1] f(x,f(y,x,z),f(y,z,u))=f(y,x,z) # label("Hint 53(1139)"). given clause #54: (wt=-999) 5139 (heat=1) [para_into,5036.1.1,1.1.2,demod,15,14,15,1245] f(x,f(y,z,x),f(y,z,u))=f(y,z,x) # label("Hint 52(1132)"). >> BACK DEMODULATING HINT 951 WITH 22850. >> BACK DEMODULATING HINT 462 WITH 22850. given clause #55: (wt=-1000) 22849 [para_from,5139.1.1,6.1.2.3,demod,14,12] f(f(x,y,f(z,u,y)),f(z,u,y),f(z,u,w))=f(z,u,y). given clause #56: (wt=69) 1091 (heat=1) [para_into,1079.1.1.3,1.1.1,demod,14,13,13,15,13,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(z,w5,f(y,z,u))))=f(w,f(y,z,u),f(y,z,f(z,u,f(x,w5,f(y,z,u))))). given clause #57: (wt=-999) 8049 [para_into,4455.1.1.3,2.1.1,demod,15,14] f(x,f(y,z,u),f(y,z,x))=f(y,z,x) # label("Hint 58(1178)"). >> BACK DEMODULATING HINT 954 WITH 22862. >> BACK DEMODULATING HINT 484 WITH 22862. >> BACK DEMODULATING HINT 955 WITH 22866. >> BACK DEMODULATING HINT 698 WITH 22868. >> BACK DEMODULATING HINT 485 WITH 22868. given clause #58: (wt=-999) 16054 [para_into,7993.1.1.3,2.1.1,demod,15,14] f(x,f(y,z,u),f(y,u,x))=f(y,u,x) # label("Hint 180(27178)"). >> BACK DEMODULATING HINT 783 WITH 22894. >> BACK DEMODULATING HINT 978 WITH 22898. >> BACK DEMODULATING HINT 786 WITH 22905. given clause #59: (wt=-999) 16068 [para_into,7993.1.1,1244.1.1,demod,15,14,14,15,14] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). given clause #60: (wt=-999) 16862 [para_into,7995.1.1.3,2.1.1,demod,15,14] f(x,f(y,z,u),f(z,u,x))=f(z,u,x) # label("Hint 140(17037)"). >> BACK DEMODULATING HINT 492 WITH 22912. >> BACK DEMODULATING HINT 494 WITH 22914. given clause #61: (wt=69) 1093 (heat=1) [para_into,1079.1.1,1.1.1,demod,14,13,13,15,13,flip.1] f(x,f(y,z,u),f(z,f(y,z,u),f(w,w5,f(y,z,u))))=f(y,z,f(z,u,f(w,f(y,z,u),f(x,w5,f(y,z,u))))). given clause #62: (wt=-1000) 22911 [para_into,16862.1.1.3,16068.1.1,demod,15,13,15,13,14,15,13,14,16055] f(f(x,y,z),f(x,z,u),f(w,u,f(x,z,u)))=f(x,z,u). given clause #63: (wt=-1000) 22913 [para_into,16862.1.1.3,5139.1.1,demod,14,14,8050] f(f(x,y,z),f(x,y,u),f(w,u,f(x,y,u)))=f(x,y,u). given clause #64: (wt=-999) 16876 [para_into,7995.1.1,1244.1.1,demod,15,14,14,15,14] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). >> BACK DEMODULATING HINT 493 WITH 22965. given clause #65: (wt=-1000) 22964 [para_into,16876.1.1,16862.1.2,demod,15,13,15,13,14,16863,14,15,13] f(f(x,y,z),f(y,z,u),f(w,u,f(y,z,u)))=f(y,z,u). given clause #66: (wt=49) 1094 (heat=1) [para_into,1079.1.2.3.3,1.1.2,demod,15,13,14,14,15,13,13,flip.1] f(x,y,f(x,z,f(u,w,f(x,w5,u))))=f(x,z,f(x,f(x,u,y),f(w5,u,w))). given clause #67: (wt=-999) 22472 [para_from,3501.1.2,9.1.1.3,demod,15,14,14] f(f(A,D,E),f(B,D,E),f(C,f(x,D,E),f(C,D,E)))!=f(D,E,f(A,B,C)). given clause #68: (wt=-999) 22474 [para_from,3501.1.2,9.1.1.1,demod,15,14,14] f(f(A,f(x,D,E),f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). given clause #69: (wt=-997) 2818 (heat=1) [para_into,2732.1.2.3,1.1.2,demod,15,13,15,13,13,2274] f(x,y,f(z,u,f(x,y,z)))=f(x,y,z) # label(bd). given clause #70: (wt=-997) 2900 [para_into,2273.1.1.3,1244.1.2,demod,14,14,13,1247,14] f(x,y,f(z,u,f(x,y,u)))=f(x,y,u) # label("Hint 122(11215)"). >> BACK DEMODULATING HINT 957 WITH 23006. >> BACK DEMODULATING HINT 795 WITH 23006. >> BACK DEMODULATING HINT 498 WITH 23006. >> BACK DEMODULATING HINT 958 WITH 23008. >> BACK DEMODULATING HINT 785 WITH 23008. >> BACK DEMODULATING HINT 499 WITH 23008. >> BACK DEMODULATING HINT 500 WITH 23010. >> BACK DEMODULATING HINT 370 WITH 23019. >> BACK DEMODULATING HINT 35 WITH 23019. given clause #71: (wt=67) 1095 (heat=1) [para_into,1079.1.2.3.3,1.1.1,demod,15,14,13,13,13,13,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(z,u,w5))))=f(w,f(y,z,u),f(w5,f(y,z,u),f(z,x,f(y,z,u)))). given clause #72: (wt=-997) 2902 [para_into,2273.1.1.3,1086.1.1,demod,13,14] f(x,y,f(x,z,f(y,z,u)))=f(x,y,z) # label("Hint 12(17)"). >> BACK DEMODULATING HINT 973 WITH 23091. >> BACK DEMODULATING HINT 468 WITH 23091. given clause #73: (wt=-997) 3218 [para_into,2304.1.2,1082.1.1,demod,13,2274,15,14,flip.1] f(x,y,f(z,u,y))=f(z,y,f(x,u,y)) # label("Hint 161(21514)"). >> BACK DEMODULATING HINT 960 WITH 23119. given clause #74: (wt=-997) 4088 [para_from,2314.1.2,2273.1.2,demod,14,2819,13,flip.1] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). given clause #75: (wt=-997) 20441 (heat=1) [para_into,20298.1.1.2,1.1.2,demod,15,14,15,13,16863,14467,flip.1] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). >> BACK DEMODULATING HINT 993 WITH 23149. >> BACK DEMODULATING HINT 25 WITH 23149. >> BACK DEMODULATING HINT 31 WITH 23151. >> BACK DEMODULATING HINT 507 WITH 23153. >> BACK DEMODULATING HINT 1017 WITH 23156. >> BACK DEMODULATING HINT 26 WITH 23156. given clause #76: (wt=-991) 1096 (heat=1) [para_into,1079.1.2.3,1.1.2,demod,15,13,11,13] f(x,y,f(x,z,f(x,y,u)))=f(x,u,f(x,y,z)) # label("Hint 32(882)"). given clause #77: (wt=-997) 23005 [para_into,2900.1.1,16862.1.2,demod,15,14,15,13,15,14,8050,15,14] f(x,y,f(z,u,f(u,x,y)))=f(u,x,y) # label("Hint 157(20432)"). given clause #78: (wt=-997) 23007 [para_into,2900.1.1,2304.1.2,demod,15,13,15,13,13,2274,15,13] f(x,y,f(z,u,f(x,u,y)))=f(x,u,y) # label("Hint 147(18678)"). given clause #79: (wt=-997) 23148 [para_into,20441.1.1,20441.1.2,demod,13,13,13,13,15,4089,15,14] f(x,y,f(x,z,f(z,u,y)))=f(x,z,y). >> BACK DEMODULATING HINT 23 WITH 23248. given clause #80: (wt=-997) 23155 (heat=1) [para_into,23141.1.1.3.3,1.1.2,demod,12,11,12,14] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). given clause #81: (wt=69) 1097 (heat=1) [para_into,1079.1.2.3,1.1.1,demod,14,13,13,15,13,flip.1] f(x,f(y,z,u),f(y,z,f(z,u,f(w,w5,f(y,z,u)))))=f(z,f(y,z,u),f(w,f(y,z,u),f(x,w5,f(y,z,u)))). given clause #82: (wt=-997) 23247 [para_into,23148.1.1,1083.1.1,demod,14] f(x,y,f(x,z,f(y,u,z)))=f(x,y,z). given clause #83: (wt=-995) 22820 (heat=1) [para_into,22474.1.1.1.2,1.1.1] f(f(A,f(x,D,f(y,D,E)),f(A,D,E)),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). given clause #84: (wt=-994) 3661 (heat=1) [para_into,3501.1.1.2,1.1.1,demod,13,15,13] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(y,u,f(x,y,z)). >> BACK DEMODULATING HINT 728 WITH 23300. >> BACK DEMODULATING HINT 509 WITH 23307. given clause #85: (wt=-994) 4937 (heat=1) [para_into,4455.1.1.1,1.1.2,demod,15,13,13] f(f(x,y,z),f(y,u,f(x,y,w)),f(z,w5,f(x,y,z)))=f(x,y,z). >> BACK DEMODULATING HINT 961 WITH 23320. >> BACK DEMODULATING HINT 575 WITH 23320. given clause #86: (wt=51) 1098 (heat=1) [para_into,1079.1.2,1.1.1,demod,13,15,13,14,13,13,flip.1] f(x,y,f(x,z,f(x,u,f(x,w,w5))))=f(x,u,f(x,w,f(x,w5,f(x,y,z)))). given clause #87: (wt=-994) 5287 (heat=1) [para_into,5061.1.1.2,1.1.2,demod,15,13,14] f(f(x,y,z),f(y,u,f(x,y,z)),f(z,w,f(x,z,w5)))=f(x,y,z). given clause #88: (wt=-994) 7445 (heat=1) [para_into,7013.1.1.3.3,1.1.2,demod,15,13] f(f(x,y,z),f(x,y,u),f(x,u,f(u,w,f(y,u,w5))))=f(x,y,u). given clause #89: (wt=-994) 7693 [para_into,4426.1.1.1.3,1127.1.1,demod,1128,14,1128] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,w,f(x,z,u)))=f(x,z,u) # label("Hint 172(26364)"). given clause #90: (wt=-994) 8740 [para_into,5061.1.1.2,1086.1.1,demod,14,13] f(f(x,y,z),f(x,u,f(x,z,w)),f(y,w5,f(x,y,z)))=f(x,y,z). given clause #91: (wt=49) 1099 (heat=1) [para_from,1079.1.1,1.1.2.3,demod,13,13,14,13,13] f(x,f(y,x,z),f(z,u,f(z,w,w5)))=f(y,x,f(z,w,f(x,z,f(z,u,w5)))). given clause #92: (wt=-994) 11633 [para_from,1087.1.1,4426.1.1.1,demod,14,13,14] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w) # label("Hint 174(26918)"). >> BACK DEMODULATING HINT 965 WITH 23379. >> BACK DEMODULATING HINT 789 WITH 23379. >> BACK DEMODULATING HINT 966 WITH 23381. >> BACK DEMODULATING HINT 814 WITH 23381. >> BACK DEMODULATING HINT 469 WITH 23381. >> BACK DEMODULATING HINT 967 WITH 23385. >> BACK DEMODULATING HINT 968 WITH 23393. >> BACK DEMODULATING HINT 757 WITH 23393. >> BACK DEMODULATING HINT 471 WITH 23393. >> BACK DEMODULATING HINT 470 WITH 23393. >> BACK DEMODULATING HINT 969 WITH 23395. >> BACK DEMODULATING HINT 475 WITH 23395. >> BACK DEMODULATING HINT 970 WITH 23414. >> BACK DEMODULATING HINT 971 WITH 23416. given clause #93: (wt=-994) 14466 (heat=1) [para_into,14270.1.1.3.3,1.1.2,demod,15,13] f(f(x,y,z),f(y,z,u),f(z,u,f(u,w,f(y,u,w5))))=f(y,z,u). >> BACK DEMODULATING HINT 547 WITH 23432. given clause #94: (wt=-994) 22843 [para_into,5139.1.1.2,1086.1.2,demod,15,13,13,13] f(f(x,y,z),f(x,z,f(x,y,u)),f(x,u,w))=f(x,u,f(x,y,z)) # label("Hint 155(19869)"). given clause #95: (wt=-994) 22844 [para_into,5139.1.1.2,1082.1.1] f(f(x,y,z),f(x,z,f(y,z,u)),f(z,u,w))=f(z,u,f(x,y,z)) # label("Hint 175(26962)"). given clause #96: (wt=51) 1100 (heat=1) [para_from,1079.1.1,1.1.1.1,demod,15,13,15,13] f(x,y,f(z,u,f(u,x,f(u,w,w5))))=f(u,x,f(x,y,f(u,w5,f(z,u,w)))). given clause #97: (wt=-994) 23090 (heat=1) [para_into,23059.1.1.3.2,1.1.2,demod,14,15,13,14] f(x,y,f(f(x,z,u),f(y,z,w),f(z,w,f(x,y,z))))=f(x,y,z). >> BACK DEMODULATING HINT 977 WITH 23497. >> BACK DEMODULATING HINT 979 WITH 23505. >> BACK DEMODULATING HINT 474 WITH 23505. given clause #98: (wt=-994) 23297 [para_into,3661.1.1.1,22849.1.2,demod,15,14,15,14,3668,13,15,14] f(f(x,y,z),f(y,z,f(x,z,u)),f(z,u,w))=f(z,u,f(x,y,z)). given clause #99: (wt=-994) 23302 [para_into,3661.1.2,1086.1.1] f(f(x,y,z),f(x,y,f(y,z,u)),f(y,u,w))=f(x,y,f(y,z,u)). given clause #100: (wt=-994) 23305 [para_from,3661.1.2,23005.1.2,demod,13,13,2274,15,14,13,15,14,flip.1] f(f(x,y,z),f(u,y,w),f(u,y,f(x,y,w)))=f(x,y,f(u,y,w)). given clause #101: (wt=69) 1101 (heat=1) [para_from,1079.1.1,1.1.1,demod,15,13,13,14,15,13,13,flip.1] f(x,y,f(y,z,f(u,f(w,w5,f(x,y,z)),f(x,y,z))))=f(w,f(x,y,z),f(y,f(x,y,z),f(w5,u,f(x,y,z)))). given clause #102: (wt=-994) 23306 [para_from,3661.1.2,20441.1.1.3,demod,15,14,15,13,13,14,15,13] f(x,y,f(f(x,z,u),f(y,u,w),f(z,u,f(x,y,u))))=f(x,y,u). given clause #103: (wt=-994) 23314 (heat=1) [para_into,23305.1.2,1.1.2,demod,13,13,15,13] f(f(x,y,z),f(y,u,w),f(y,u,f(x,y,w)))=f(y,w,f(x,y,u)) # label("Hint 177(27085)"). given clause #104: (wt=-994) 23327 [para_into,7445.1.1.3.3,22964.1.1,demod,1245,12] f(f(x,y,z),f(x,y,f(u,w,w5)),f(u,w,w5))=f(x,y,f(u,w,w5)). given clause #105: (wt=-994) 23378 [para_into,11633.1.1.1.3.3,23148.1.2,demod,15,14,2903] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,u),f(z,u,w5))=f(y,z,u) # label("Hint 151(19393)"). given clause #106: (wt=49) 1102 (heat=1) [para_from,1079.1.2,1.1.2.3,demod,13,13] f(x,f(y,x,z),f(x,u,f(x,w,w5)))=f(y,x,f(x,u,f(x,w5,f(x,z,w)))). given clause #107: (wt=-994) 23380 [para_into,11633.1.1.1.3,23148.1.2,demod,23149,14,13,14] f(f(x,y,f(y,z,f(y,u,w))),f(y,w,z),f(w,z,w5))=f(y,w,z) # label("Hint 176(27036)"). >> BACK DEMODULATING HINT 756 WITH 23607. >> BACK DEMODULATING HINT 476 WITH 23607. given clause #108: (wt=-994) 23384 [para_into,11633.1.1.1,3658.1.2,demod,13,14,16069] f(f(x,y,f(x,z,f(x,u,w))),f(x,z,w),f(z,w,w5))=f(x,z,w). given clause #109: (wt=-994) 23415 [para_from,11633.1.2,23005.1.2,demod,15,13,2901,15,14,13,13,15,13,15,13,flip.1] f(f(x,y,z),f(x,y,u),f(z,w,f(x,z,f(y,z,w5))))=f(x,y,z). given clause #110: (wt=-994) 23431 [para_into,14466.1.1.3,1085.1.2] f(f(x,y,z),f(y,z,u),f(u,w,f(z,u,f(y,u,w5))))=f(y,z,u). >> BACK DEMODULATING HINT 548 WITH 23630. given clause #111: (wt=51) 1103 (heat=1) [para_from,1079.1.2,1.1.1.1,demod,13,15,13,14,15,13,13] f(x,y,f(x,z,f(x,u,f(x,w,w5))))=f(x,w,f(x,y,f(x,z,f(x,u,w5)))). given clause #112: (wt=-1000) 23629 [para_into,23431.1.1,23314.1.2,demod,14,13,13,15,14,15,13,13,15,14,14,16877,15,12,15,14] f(f(x,y,z),f(x,z,f(x,y,u)),f(w,y,z))=f(x,y,z). given clause #113: (wt=-994) 23496 [para_into,23090.1.1.3.1,23148.1.2,demod,15,14,2903] f(x,y,f(f(x,z,u),f(y,u,w),f(u,w,f(x,y,u))))=f(x,y,u). given clause #114: (wt=-994) 23504 [para_from,23090.1.2,22849.1.2,demod,15,14,15,14,3668,13,13,15,14,flip.1] f(x,y,f(f(z,x,u),f(z,y,w),f(z,w,f(z,x,y))))=f(z,x,y). given clause #115: (wt=-994) 23528 [para_from,23305.1.2,1748.1.2,demod,13,13,13,15,13,flip.1] f(f(x,y,z),f(x,y,f(y,u,z)),f(y,u,w))=f(x,y,f(y,u,z)). given clause #116: (wt=49) 1104 (heat=1) [para_into,1080.1.1.2,1.1.2,demod,13,15,13,13,14,13] f(x,f(x,y,f(x,z,u)),f(x,w,w5))=f(x,w5,f(x,z,f(x,w,f(x,u,y)))). given clause #117: (wt=-994) 23557 [para_into,23314.1.1.1,23005.1.2,demod,15,13,2901,13,13] f(f(x,y,z),f(x,u,w),f(x,u,f(x,z,w)))=f(x,w,f(x,z,u)) # label("Hint 179(27113)"). given clause #118: (wt=-994) 23560 [para_into,23314.1.1.1,5.1.2,demod,13,13] f(f(x,y,z),f(y,u,w),f(y,u,f(y,z,w)))=f(y,w,f(y,z,u)). given clause #119: (wt=-993) 1165 (heat=1) [para_into,1087.1.2.3,1.1.2,demod,13,14,11,13] f(x,f(x,y,z),f(x,z,u))=f(x,y,f(x,z,u)) # label("Hint 34(952)"). given clause #120: (wt=-993) 1241 [para_from,1127.1.1,6.1.2.3,demod,13,13,13] f(x,f(y,x,z),f(x,z,u))=f(y,x,f(x,z,u)) # label("Hint 71(2230)"). >> BACK DEMODULATING HINT 3832 WITH 23700. >> BACK DEMODULATING HINT 904 WITH 23700. given clause #121: (wt=47) 1105 (heat=1) [para_into,1080.1.1.2,1.1.1,demod,13,13,13,13] f(x,f(x,y,f(x,z,u)),f(x,w,w5))=f(x,w5,f(x,f(x,y,z),f(x,u,w))). given clause #122: (wt=-993) 1857 (heat=1) [para_into,1746.1.2,1.1.2,demod,12,15,14,14,13,flip.1] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)) # label("Hint 40(998)"). given clause #123: (wt=-993) 2141 (heat=1) [para_from,1919.1.2,1.1.2,demod,11,14,flip.1] f(x,f(x,y,z),f(x,y,u))=f(x,y,f(x,z,u)) # label("Hint 43(1025)"). given clause #124: (wt=-993) 2464 (heat=1) [para_into,2340.1.2,1.1.2,demod,1128,14,13,14,1128,13,10] f(x,f(x,y,z),f(y,u,f(y,z,w)))=f(x,y,z) # label("Hint 57(1176)"). given clause #125: (wt=-993) 4375 (heat=1) [para_into,4370.1.1,1.1.2,demod,11,13,12,15,14,2315,12,15,13,12,14,flip.1] f(x,f(y,z,x),f(y,u,f(y,z,w)))=f(y,z,x). given clause #126: (wt=-977) 1106 (heat=1) [para_into,1080.1.1.3,1.1.2,demod,13,15,13,13,13,14,flip.1] f(x,f(x,y,f(x,z,u)),f(u,w,w5))=f(x,f(x,y,z),f(u,w5,f(x,u,w))). >> BACK DEMODULATING HINT 990 WITH 23820. >> BACK DEMODULATING HINT 512 WITH 23820. given clause #127: (wt=-994) 23819 [para_from,1106.1.1,7995.1.1.3,demod,15,13,1247,14] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(u,w,w5)))=f(y,z,u). >> BACK DEMODULATING HINT 994 WITH 23837. >> BACK DEMODULATING HINT 518 WITH 23837. >> BACK DEMODULATING HINT 519 WITH 23839. given clause #128: (wt=-996) 23836 [para_into,23819.1.1,1748.1.2,demod,15,14,15,13,15,14,15,13,15,14] f(x,f(x,y,z),f(f(x,y,z),f(x,u,w),f(y,z,w5)))=f(x,y,z). given clause #129: (wt=-994) 23838 [para_into,23819.1.1,5.1.2,demod,15,14,15,14,15,13,13,15,14] f(f(x,y,z),f(x,f(x,y,z),f(x,u,w)),f(y,z,w5))=f(x,y,z). given clause #130: (wt=-993) 4449 [para_into,3667.1.1,2304.1.1,demod,13,13,14,13] f(x,f(x,y,z),f(u,y,f(x,y,z)))=f(x,y,z). given clause #131: (wt=56) 1107 (heat=1) [para_into,1080.1.1.3,1.1.1,demod,14,13,14,15,13] f(f(x,y,z),f(x,y,f(y,z,u)),f(w,w5,f(x,y,z)))=f(u,f(x,y,z),f(w,f(x,y,z),f(y,w5,f(x,y,z)))). >> BACK DEMODULATING HINT 1073 WITH 23867. >> BACK DEMODULATING HINT 991 WITH 23867. >> BACK DEMODULATING HINT 947 WITH 23867. >> BACK DEMODULATING HINT 631 WITH 23867. >> BACK DEMODULATING HINT 513 WITH 23867. >> BACK DEMODULATING HINT 482 WITH 23867. given clause #132: (wt=-999) 23866 [para_from,1107.1.1,16054.1.1,demod,15,14,1739,12,15,14,flip.1] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). >> BACK DEMODULATING HINT 585 WITH 23881. NEW HINT: 23885 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,f(x,y,f(y,z,u)),f(x,u,f(y,z,u)))=f(x,y,u). given clause #133: (wt=-993) 4451 [para_into,3667.1.1,2273.1.1,demod,13] f(x,f(y,z,f(z,x,u)),f(z,x,u))=f(z,x,u) # label("Hint 117(8889)"). given clause #134: (wt=-993) 8886 (heat=1) [para_into,8740.1.1.3,1.1.2,demod,10,10,15,14] f(x,f(y,x,z),f(y,u,f(y,z,w)))=f(y,x,z) # label("Hint 131(12497)"). given clause #135: (wt=-993) 9215 (heat=1) [para_into,9210.1.2.3,1.1.2,demod,14,6645,14,13,flip.1] f(x,y,f(z,f(x,z,y),f(y,u,w)))=f(x,z,y) # label("Hint 108(7501)"). given clause #136: (wt=49) 1109 (heat=1) [para_into,1080.1.2.3.3,1.1.2,demod,13,13,14,15,13,13] f(x,f(x,y,z),f(x,u,f(z,w,w5)))=f(x,u,f(x,y,f(z,w5,f(x,z,w)))). given clause #137: (wt=-993) 9258 (heat=1) [para_into,9231.1.2,1.1.2,demod,12,11] f(x,y,f(z,f(x,z,u),f(y,z,w)))=f(x,y,z) # label("Hint 95(5568)"). given clause #138: (wt=-993) 22861 [para_into,8049.1.1.2,1748.1.2,demod,13,15,14,15] f(x,f(x,y,z),f(u,y,f(y,z,w)))=f(x,y,z). >> BACK DEMODULATING HINT 982 WITH 24066. >> BACK DEMODULATING HINT 486 WITH 24066. given clause #139: (wt=-993) 22865 [para_into,8049.1.1.2,1083.1.1,demod,15,14,14,15,14] f(x,f(x,y,z),f(y,u,f(y,w,z)))=f(x,y,z). >> BACK DEMODULATING HINT 989 WITH 24079. >> BACK DEMODULATING HINT 978 WITH 24079. >> BACK DEMODULATING HINT 807 WITH 24079. >> BACK DEMODULATING HINT 784 WITH 24079. >> BACK DEMODULATING HINT 783 WITH 24079. >> BACK DEMODULATING HINT 707 WITH 24079. >> BACK DEMODULATING HINT 703 WITH 24079. NEW HINT: 24084 [bsub_wt=2147483647, bsub_add_wt=-1024] f(y,f(x,y,u),f(y,z,w))=f(x,y,f(y,z,f(y,u,w))) # label(bd). >> BACK DEMODULATING HINT 702 WITH 24079. >> BACK DEMODULATING HINT 545 WITH 24079. given clause #140: (wt=-999) 24078 [para_into,22865.1.1,23314.1.2,demod,13,14,13,1128,14,12,13] f(x,f(y,x,z),f(y,u,z))=f(y,x,z). given clause #141: (wt=56) 1110 (heat=1) [para_into,1080.1.2.3.3,1.1.1,demod,15,14,15,13,13,13] f(f(x,y,z),f(y,u,f(x,y,z)),f(w,w5,f(x,y,z)))=f(w5,f(x,y,z),f(u,f(x,y,z),f(x,y,f(y,z,w)))). given clause #142: (wt=-993) 23118 [para_into,3218.1.1.3,1127.1.1,demod,12,14,flip.1] f(x,f(y,z,f(x,z,u)),f(x,z,u))=f(x,z,u). given clause #143: (wt=-993) 23319 [para_into,4937.1.1,1082.1.2,demod,13,13,13,13,15,13,1245,13] f(x,f(y,z,f(y,u,w)),f(y,u,x))=f(y,u,x). given clause #144: (wt=-993) 24065 [para_into,22861.1.1,5.1.2,demod,15,13,15,14,15,13] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). given clause #145: (wt=-991) 1274 (heat=1) [para_from,1244.1.1,1.1.1.1,demod,15,13,15,13,flip.1] f(x,y,f(y,z,f(u,x,y)))=f(y,z,f(u,x,y)). given clause #146: (wt=49) 1111 (heat=1) [para_into,1080.1.2.3,1.1.1,demod,13,15,13,13,13] f(x,f(x,y,f(x,z,u)),f(x,w,w5))=f(x,w5,f(x,z,f(x,u,f(x,y,w)))). given clause #147: (wt=-991) 1305 (heat=1) [para_into,1277.1.1.3,1.1.2,demod,11,14,flip.1] f(x,y,f(x,z,f(x,u,y)))=f(x,u,f(x,y,z)). >> BACK DEMODULATING HINT 1018 WITH 24201. >> BACK DEMODULATING HINT 368 WITH 24201. >> BACK DEMODULATING HINT 27 WITH 24201. given clause #148: (wt=-997) 24200 [para_into,1305.1.1.3,23155.1.1,demod,14,16877,14,flip.1] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). given clause #149: (wt=-991) 1357 (heat=1) [para_into,1321.1.1.3,1.1.2,demod,11,1128,1128,flip.1] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)) # label("Hint 41(1005)"). given clause #150: (wt=-991) 1532 (heat=1) [para_from,1501.1.2,1.1.2,demod,11,1128,flip.1] f(x,y,f(x,z,f(x,u,y)))=f(x,z,f(x,u,y)) # label("Hint 78(2705)"). given clause #151: (wt=58) 1112 (heat=1) [para_into,1080.1.2,1.1.1,demod,14,15,14,15,13,13] f(f(x,y,z),f(y,u,f(x,y,z)),f(w,w5,f(x,y,z)))=f(x,y,f(y,z,f(w,f(x,y,z),f(w5,u,f(x,y,z))))). given clause #152: (wt=-991) 2000 (heat=1) [para_into,1908.1.1,1.1.2,demod,14,1128,10,14,1128,flip.1] f(x,y,f(x,z,f(z,u,f(z,y,w))))=f(x,z,y) # label("Hint 127(11984)"). given clause #153: (wt=-991) 2724 [para_into,1748.1.1.3,1244.1.1,demod,15,14,15,14,13,flip.1] f(x,y,f(z,x,f(x,u,y)))=f(z,x,f(x,u,y)) # label("Hint 94(5348)"). given clause #154: (wt=-993) 24330 [para_from,2724.1.1,1081.1.1,demod,14,flip.1] f(x,f(y,x,z),f(x,u,z))=f(y,x,f(x,u,z)). given clause #155: (wt=-991) 3038 (heat=1) [para_into,2902.1.1.3.3,1.1.2,demod,15,13] f(x,y,f(x,z,f(z,u,f(y,z,w))))=f(x,y,z) # label(bd). given clause #156: (wt=46) 1113 (heat=1) [para_from,1080.1.1,1.1.2.3,demod,14] f(f(x,y,f(z,y,u)),f(z,y,u),f(y,w,w5))=f(x,f(z,y,u),f(y,w5,f(z,y,f(y,u,w)))). given clause #157: (wt=-991) 15805 (heat=1) [para_into,15377.1.2.3,1.1.2,demod,13,14,13,9216] f(x,y,f(z,u,f(x,z,f(y,z,w))))=f(x,y,z) # label("Hint 110(7840)"). >> BACK DEMODULATING HINT 759 WITH 24400. >> BACK DEMODULATING HINT 794 WITH 24406. given clause #158: (wt=-991) 23392 [para_into,11633.1.1,16862.1.1,demod,15,14,13,15,13] f(x,y,f(z,u,f(x,u,f(y,u,w))))=f(x,y,u) # label("Hint 119(9179)"). >> BACK DEMODULATING HINT 761 WITH 24462. >> BACK DEMODULATING HINT 798 WITH 24470. >> BACK DEMODULATING HINT 797 WITH 24470. >> BACK DEMODULATING HINT 797 WITH 24476. given clause #159: (wt=-991) 23413 [para_from,11633.1.1,16862.1.1,demod,14,13,flip.1] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). given clause #160: (wt=-991) 23606 [para_from,23380.1.1,2818.1.1.3,demod,15,13,1128,15,14,13,13,flip.1] f(x,y,f(z,u,f(y,z,f(x,z,w))))=f(x,y,z) # label("Hint 118(9165)"). given clause #161: (wt=57) 1114 (heat=1) [para_from,1080.1.1,1.1.1.1,demod,13,13,15,14,13,14,13,15,14] f(x,f(y,z,f(y,u,f(y,w,w5))),f(y,u,w))=f(y,f(y,u,w),f(x,f(y,z,w5),f(y,u,w))). given clause #162: (wt=-991) 23699 [para_into,1241.1.2,1100.1.1,demod,13,13,14384,13,13,flip.1] f(x,y,f(z,x,f(y,u,f(z,y,w))))=f(z,x,y). given clause #163: (wt=-991) 24175 [para_from,1274.1.2,23005.1.2,demod,13,13,2274,13,flip.1] f(x,y,f(z,y,f(u,x,y)))=f(z,y,f(u,x,y)). given clause #164: (wt=-991) 24399 [para_into,15805.1.1,23005.1.2,demod,13,13,13,13,2274,15,13] f(x,y,f(z,u,f(z,y,f(x,z,w))))=f(x,z,y) # label("Hint 121(10171)"). given clause #165: (wt=-991) 24461 [para_into,23392.1.1,24065.1.2,demod,13,13,13,13,13,14,4376,15,14] f(x,y,f(z,u,f(u,x,f(u,y,w))))=f(u,x,y) # label("Hint 123(11245)"). given clause #166: (wt=47) 1115 (heat=1) [para_from,1080.1.2,1.1.2.3,demod,13,13,13,15,14,14] f(x,f(y,x,z),f(z,u,f(z,w,w5)))=f(y,x,f(z,f(x,z,w5),f(z,u,w))). given clause #167: (wt=-991) 24469 [para_into,23392.1.1,23005.1.2,demod,13,13,13,13,2274,15,13] f(x,y,f(z,u,f(u,y,f(x,u,w))))=f(x,u,y) # label("Hint 160(21508)"). >> BACK DEMODULATING HINT 546 WITH 24750. given clause #168: (wt=-994) 24749 [para_into,24469.1.1,23327.1.2,demod,13,11608,13,14] f(f(x,y,z),f(x,y,u),f(w,u,f(y,u,f(x,u,w5))))=f(x,y,u). given clause #169: (wt=-990) 5983 (heat=1) [para_into,5968.1.1.3,1.1.2,demod,15,14,15,13,1128] f(f(x,y,z),f(x,y,u),f(u,w,f(x,y,z)))=f(w,f(x,y,z),f(x,y,u)) # label("Hint 83(3301)"). given clause #170: (wt=-990) 8612 (heat=1) [para_into,8539.1.1,1.1.2,demod,14,15,14,15,14,15,14,14] f(f(x,y,z),f(x,u,f(y,z,w)),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)) # label("Hint 73(2478)"). >> BACK DEMODULATING HINT 987 WITH 24807. >> BACK DEMODULATING HINT 550 WITH 24807. >> BACK DEMODULATING HINT 653 WITH 24809. >> BACK DEMODULATING HINT 373 WITH 24809. >> BACK DEMODULATING HINT 44 WITH 24809. >> BACK DEMODULATING HINT 988 WITH 24814. >> BACK DEMODULATING HINT 600 WITH 24814. given clause #171: (wt=49) 1116 (heat=1) [para_from,1080.1.2,1.1.1.1,demod,13,15,13,13,15,13] f(x,y,f(z,f(z,u,w),f(z,w5,x)))=f(z,x,f(x,y,f(z,u,f(z,w,w5)))). given clause #172: (wt=-1000) 24806 [para_into,8612.1.2,23297.1.2,demod,20442,14,10] f(f(x,y,z),f(x,u,f(y,z,u)),f(y,z,u))=f(y,z,u). >> BACK DEMODULATING HINT 552 WITH 24831. given clause #173: (wt=-1000) 24813 [para_from,8612.1.2,1274.1.2,demod,15,14,15,13,14,24079,1128,15,14,15,13,13,15,13,15,14,flip.1] f(f(x,y,z),f(x,u,z),f(y,u,f(x,y,z)))=f(x,y,z). >> BACK DEMODULATING HINT 992 WITH 24851. >> BACK DEMODULATING HINT 601 WITH 24851. given clause #174: (wt=-1000) 24830 [para_into,24806.1.1,24078.1.2,demod,15,14,15,14,15,14,13,15,14,13,14,23867,15,14] f(f(x,y,f(y,z,u)),f(x,z,u),f(y,z,u))=f(y,z,u). >> BACK DEMODULATING HINT 577 WITH 24865. given clause #175: (wt=-1000) 24850 [para_from,24813.1.1,1274.1.1.3,demod,12,13,13,15,13,flip.1] f(f(x,y,z),f(x,u,f(y,u,z)),f(y,u,z))=f(y,u,z). given clause #176: (wt=37) 1117 (heat=1) [para_into,1081.1.1.3,1.1.2,demod,13,15,13,13,15,13,14,flip.1] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). given clause #177: (wt=-994) 24864 [para_into,24830.1.1.1,1357.1.2] f(f(x,y,f(y,z,f(x,y,u))),f(x,z,u),f(y,z,u))=f(y,z,u). >> BACK DEMODULATING HINT 578 WITH 24889. given clause #178: (wt=-994) 24888 [para_into,24864.1.1.1.3,24469.1.2,demod,24470,14,14,14] f(f(x,y,f(y,z,f(x,y,u))),f(x,u,z),f(y,u,z))=f(y,u,z). given clause #179: (wt=-994) 24900 [para_into,24888.1.1.2,1246.1.1,demod,14,24079,1128] f(f(x,y,z),f(x,u,z),f(y,z,f(x,u,z)))=f(y,z,f(x,u,z)). >> BACK DEMODULATING HINT 429 WITH 24907. >> BACK DEMODULATING HINT 587 WITH 24912. >> BACK DEMODULATING HINT 588 WITH 24914. given clause #180: (wt=-1000) 24911 [para_into,24900.1.2,22913.1.1,demod,15,14,13,23867] f(f(x,y,f(z,u,y)),f(z,u,w),f(z,u,y))=f(z,u,y). given clause #181: (wt=39) 1118 (heat=1) [para_into,1081.1.1.3,1.1.1,demod,13,13,13,15,13,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,z,f(x,u,f(x,w,y))). given clause #182: (wt=-1000) 24913 [para_into,24900.1.2,22911.1.1,demod,15,14,13,23867] f(f(x,y,f(z,u,y)),f(z,w,u),f(z,u,y))=f(z,u,y). given clause #183: (wt=-993) 24804 [para_into,8612.1.1.2,1082.1.2,demod,14,16863,flip.1] f(x,f(y,z,x),f(z,x,u))=f(x,u,f(y,z,x)). >> BACK DEMODULATING HINT 800 WITH 24946. NEW HINT: 24953 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,f(y,z,u),f(z,w,f(x,z,f(z,w5,f(y,z,u)))))=f(x,z,f(y,z,u)) # label(bd). >> BACK DEMODULATING HINT 995 WITH 24948. >> BACK DEMODULATING HINT 819 WITH 24948. given clause #184: (wt=-991) 24945 [para_into,24804.1.2,23384.1.1,demod,23320,14,16863] f(x,y,f(z,u,f(z,x,f(z,w,y))))=f(z,x,y) # label("Hint 162(21517)"). >> BACK DEMODULATING HINT 24953 WITH 24975. given clause #185: (wt=-991) 24947 [para_into,24804.1.2,23380.1.1,demod,13,14,23395,14,16863,14] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,x,y) # label("Hint 181(27197)"). >> BACK DEMODULATING HINT 996 WITH 24986. >> BACK DEMODULATING HINT 816 WITH 24986. given clause #186: (wt=49) 1119 (heat=1) [para_into,1081.1.1,1.1.1,demod,14,13,15,14,13,flip.1] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(y,z,f(z,u,f(w,x,f(y,z,u)))). >> BACK DEMODULATING HINT 41 WITH 24999. given clause #187: (wt=-991) 24974 [para_into,24945.1.1,24850.1.2,demod,13,13,13,24851,13] f(x,y,f(z,u,f(x,z,f(z,w,y))))=f(x,z,y) # label(bd). given clause #188: (wt=-991) 24985 [para_into,24947.1.1,24850.1.2,demod,13,13,13,24851,13] f(x,y,f(z,u,f(x,u,f(u,w,y))))=f(x,u,y) # label("Hint 178(27103)"). given clause #189: (wt=-991) 25012 [para_into,1119.1.2.3.3,1081.1.2,demod,10,14,15,14,1128,flip.1] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)) # label("Hint 84(3324)"). >> BACK DEMODULATING HINT 1016 WITH 25073. >> BACK DEMODULATING HINT 777 WITH 25073. >> BACK DEMODULATING HINT 571 WITH 25073. given clause #190: (wt=-999) 25072 [para_into,25012.1.1.3,24813.1.1,demod,12,13,14,16069,14,flip.1] f(x,f(y,z,u),f(z,x,u))=f(z,x,u) # label("Hint 139(16799)"). given clause #191: (wt=37) 1120 (heat=1) [para_into,1081.1.2.3,1.1.2,demod,13,13,15,13,15,13] f(x,f(x,y,z),f(x,u,w))=f(x,w,f(x,z,f(x,y,u))). given clause #192: (wt=-990) 17460 (heat=1) [para_into,17386.1.1,1.1.2,demod,14,15,14,15,14,15,14,14] f(f(x,y,z),f(x,u,f(w,y,z)),f(w,y,z))=f(u,f(x,y,z),f(w,y,z)). >> BACK DEMODULATING HINT 1027 WITH 25177. >> BACK DEMODULATING HINT 613 WITH 25177. given clause #193: (wt=-990) 22872 [para_from,8049.1.1,1081.1.1.3,demod,13,15,14,flip.1] f(f(x,y,z),f(x,y,u),f(w,u,f(x,y,z)))=f(w,f(x,y,z),f(x,y,u)) # label("Hint 82(3280)"). given clause #194: (wt=-988) 10262 (heat=1) [para_into,10084.1.1.1,1.1.2,demod,15,13,2901,13,13,13] f(f(x,y,z),f(y,z,f(x,y,u)),f(y,w,f(y,u,z)))=f(x,y,f(y,u,z)). given clause #195: (wt=-988) 23299 [para_into,3661.1.1.2.3,5644.1.1,demod,12,15,14,16802,15,14,flip.1] f(f(x,f(y,z,u),f(y,u,f(y,z,w))),f(y,z,u),f(z,u,w5))=f(y,z,u) # label("Hint 90(4917)"). given clause #196: (wt=39) 1121 (heat=1) [para_into,1081.1.2.3,1.1.1,demod,13,15,13,15,13,13,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,u,f(x,y,f(x,z,w))). given clause #197: (wt=-987) 1131 (heat=1) [para_from,1082.1.1,1.1.2.3,demod,15,14,13,15,13] f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,u,f(x,z,w))) # label("Hint 46(1064)"). >> BACK DEMODULATING HINT 997 WITH 25244. >> BACK DEMODULATING HINT 828 WITH 25244. >> BACK DEMODULATING HINT 556 WITH 25244. given clause #198: (wt=-999) 25243 [para_from,1131.1.2,23297.1.2,demod,13,13,13,14,1128,12,13,15,13,7694,13,15,1128,14,flip.1] f(x,f(y,z,u),f(y,x,u))=f(y,x,u) # label("Hint 190(28269)"). given clause #199: (wt=-987) 1154 (heat=1) [para_into,1085.1.1.3,1.1.1,demod,13,13,13,15,13,flip.1] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,u,f(x,w,z))) # label("Hint 38(991)"). given clause #200: (wt=-987) 1557 (heat=1) [para_into,1549.1.1.3,1.1.2,demod,14,1128,11,14,1128] f(x,f(y,z,u),f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)) # label("Hint 106(7007)"). given clause #201: (wt=49) 1122 (heat=1) [para_into,1081.1.2,1.1.1,demod,15,14,13,15,14,13] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(y,z,f(z,u,f(x,w,f(y,z,u)))). >> BACK DEMODULATING HINT 371 WITH 25325. >> BACK DEMODULATING HINT 38 WITH 25325. given clause #202: (wt=-987) 1832 (heat=1) [para_into,1744.1.2.3,1.1.1,demod,15,13,13,15,13,14,1245,13,13] f(x,f(y,z,u),f(z,x,w))=f(x,w,f(y,z,f(z,u,x))) # label("Hint 36(980)"). >> BACK DEMODULATING HINT 541 WITH 25347. given clause #203: (wt=-994) 25346 [para_into,1832.1.2,24900.1.2,demod,15,14,13,1128,14,16877,15,14,13,15,14,15,14,15,14,4450,14,flip.1] f(f(x,y,f(x,z,u)),f(x,z,u),f(y,z,f(x,z,u)))=f(x,z,u). given clause #204: (wt=-987) 1865 (heat=1) [para_into,1747.1.2.3.3,1.1.2,demod,12,11] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). given clause #205: (wt=-987) 2559 [para_into,1086.1.2.3,1086.1.2,demod,15,13,14,13] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,w,f(x,y,u))) # label("Hint 39(992)"). given clause #206: (wt=37) 1123 (heat=1) [para_from,1081.1.1,1.1.2.3,demod,13,13,15] f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,w,f(x,z,u))). given clause #207: (wt=-987) 3963 (heat=1) [para_into,3842.1.1.3.3,1.1.2,demod,13,15,14,13,2819,13] f(x,f(x,y,f(z,u,w)),f(z,u,w))=f(x,y,f(z,u,w)) # label("Hint 125(11969)"). given clause #208: (wt=-987) 4070 [para_from,2314.1.1,2304.1.2,demod,13,13,13,3494,15,13] f(x,f(x,y,f(y,z,u)),f(z,w,f(x,y,z)))=f(x,y,z). given clause #209: (wt=-987) 4078 [para_from,2314.1.1,1080.1.2.3,demod,13,14,13] f(x,f(x,y,z),f(x,u,f(y,z,w)))=f(x,u,f(x,y,z)). >> BACK DEMODULATING HINT 998 WITH 25527. >> BACK DEMODULATING HINT 514 WITH 25527. >> BACK DEMODULATING HINT 23885 WITH 25540. >> BACK DEMODULATING HINT 604 WITH 25552. given clause #210: (wt=-989) 25526 [para_into,4078.1.2,23866.1.1,demod,15,13] f(x,f(x,y,z),f(x,f(y,z,u),f(y,z,w)))=f(x,y,z). given clause #211: (wt=39) 1124 (heat=1) [para_from,1081.1.1,1.1.1.1,demod,13,15,13,15,13,15,13] f(x,y,f(z,u,f(z,w,x)))=f(z,x,f(x,y,f(z,u,w))). >> BACK DEMODULATING HINT 1020 WITH 25588. >> BACK DEMODULATING HINT 557 WITH 25588. given clause #212: (wt=-996) 25573 [para_from,25526.1.1,23504.1.1.3.3,demod,14,15,13,8050,15,13,12] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). given clause #213: (wt=-1000) 25639 [para_into,25573.1.1,23557.1.1,demod,14,14,14,14,flip.1] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,y,f(x,z,u)). >> BACK DEMODULATING HINT 1007 WITH 25678. >> BACK DEMODULATING HINT 1006 WITH 25685. >> BACK DEMODULATING HINT 553 WITH 25685. given clause #214: (wt=-1000) 25642 [para_from,25573.1.1,23557.1.1,demod,14,14] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,z,f(x,y,u)). given clause #215: (wt=-1000) 25647 [para_into,25639.1.1.1,24947.1.2,demod,15,14,13,23393,13,13,13,13] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(x,z,f(y,z,u)). given clause #216: (wt=47) 1125 (heat=1) [para_into,1082.1.1.3,1.1.2,demod,15,15,13,13,14,flip.1] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(w,f(y,z,u),f(z,u,f(y,z,x))). >> BACK DEMODULATING HINT 1023 WITH 25734. >> BACK DEMODULATING HINT 563 WITH 25734. >> BACK DEMODULATING HINT 477 WITH 25746. given clause #217: (wt=-1000) 25656 [para_into,25639.1.1,16862.1.2,demod,14,14,14,14,15,14,23867] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,u,f(x,y,z)). >> BACK DEMODULATING HINT 1009 WITH 25756. >> BACK DEMODULATING HINT 555 WITH 25756. given clause #218: (wt=-1000) 25665 (heat=1) [para_into,25647.1.2,1.1.2,demod,14,15,13] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(z,u,f(x,y,z)). given clause #219: (wt=-996) 25636 [para_into,25573.1.1.1,24985.1.2,demod,15,14,23393,14] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(w,f(x,y,z),f(x,z,u)). given clause #220: (wt=-996) 25637 [para_into,25573.1.1.1,24947.1.1,demod,14,13,23414] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). given clause #221: (wt=37) 1126 (heat=1) [para_into,1082.1.1.3,1.1.1,demod,15,15,13,15,13,flip.1] f(x,f(x,y,z),f(u,z,w))=f(x,y,f(u,z,f(x,z,w))). given clause #222: (wt=-996) 25638 [para_into,25573.1.1,25573.1.2,demod,1128,14] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(u,f(x,y,z),f(x,y,w)) # label("Hint 198(32143)"). given clause #223: (wt=-996) 25640 [para_into,25573.1.1,16862.1.2,demod,15,14,23867] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). given clause #224: (wt=-996) 25663 [para_into,25639.1.2,1165.1.2] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,f(x,y,z),f(x,z,u)). given clause #225: (wt=-996) 25677 [para_from,25639.1.2,22865.1.1.3,demod,14,14,15,13] f(x,f(x,y,z),f(f(y,z,u),f(y,z,w),f(y,u,w)))=f(x,y,z). given clause #226: (wt=37) 1129 (heat=1) [para_into,1082.1.2.3,1.1.2,demod,13,15,14,15,13,15,13,13] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,z,f(x,y,w))). given clause #227: (wt=-996) 25684 [para_from,25639.1.2,23319.1.1.2,demod,15,14,14,15,14] f(x,f(x,y,z),f(f(y,u,z),f(y,u,w),f(y,z,w)))=f(x,y,z). given clause #228: (wt=-996) 25754 [para_into,25656.1.2,2141.1.2,demod,14,14] f(f(x,y,z),f(x,y,u),f(x,z,u))=f(x,f(x,y,u),f(x,z,u)). >> BACK DEMODULATING HINT 574 WITH 25831. given clause #229: (wt=-996) 25755 [para_from,25656.1.2,8049.1.1.2,demod,15,14,14,15,14] f(x,f(x,y,z),f(f(y,u,w),f(y,u,z),f(y,w,z)))=f(x,y,z). given clause #230: (wt=-996) 25769 [para_into,25636.1.1,24850.1.2,demod,14,14,24807] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(u,f(x,y,z),f(x,z,w)). given clause #231: (wt=39) 1130 (heat=1) [para_into,1082.1.2,1.1.1,demod,13,15,15,13,13,13,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,u,f(x,w,f(x,y,z))). given clause #232: (wt=-996) 25779 [para_into,25637.1.1,24850.1.2,demod,14,14,24807] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). given clause #233: (wt=-996) 25800 [para_into,25640.1.1.1,24985.1.2,demod,15,14,23393] f(f(x,y,z),f(x,z,u),f(x,z,w))=f(y,f(x,z,u),f(x,z,w)). given clause #234: (wt=-994) 25587 [para_into,1124.1.2.3,23305.1.2,demod,15,14,13,2315,13,13,13,flip.1] f(x,y,f(f(x,z,u),f(z,y,w),f(z,y,f(x,z,w))))=f(x,z,y). >> BACK DEMODULATING HINT 1021 WITH 25858. >> BACK DEMODULATING HINT 558 WITH 25858. given clause #235: (wt=-994) 25705 [para_into,25647.1.2,25012.1.2] f(f(x,y,z),f(x,z,u),f(y,z,u))=f(y,z,f(z,u,f(x,y,z))). >> BACK DEMODULATING HINT 582 WITH 25881. given clause #236: (wt=39) 1132 (heat=1) [para_from,1082.1.1,1.1.1.1,demod,13,15,13,14,15,13] f(x,y,f(z,u,f(u,w,x)))=f(u,x,f(x,y,f(z,u,w))). >> BACK DEMODULATING HINT 589 WITH 25895. given clause #237: (wt=-1000) 25880 [para_from,25705.1.2,1119.1.2.3,demod,1245,12,15,14,15,14,15,13,flip.1] f(x,y,f(f(z,x,u),f(z,y,u),f(x,y,u)))=f(x,y,u). >> BACK DEMODULATING HINT 603 WITH 25934. given clause #238: (wt=-996) 25933 [para_from,25880.1.1,17460.1.1.2,demod,14,16877,13,14,10,14,16877,13,14,flip.1] f(x,f(y,x,z),f(f(y,u,z),f(y,x,z),f(u,x,z)))=f(y,x,z). given clause #239: (wt=-994) 25716 [para_from,25647.1.2,1127.1.1.3,demod,14,13,13] f(x,y,f(f(x,y,z),f(x,y,u),f(y,z,u)))=f(x,y,f(y,z,u)). >> BACK DEMODULATING HINT 1012 WITH 25947. >> BACK DEMODULATING HINT 576 WITH 25947. given clause #240: (wt=-994) 25830 [para_from,25754.1.2,1119.1.2.3.3,demod,14,14,13,1247,12,14,13,13,flip.1] f(x,y,f(z,y,f(f(x,u,z),f(x,u,y),f(x,z,y))))=f(x,z,y). given clause #241: (wt=-975) 1133 (heat=1) [para_from,1082.1.1,1.1.1,demod,15,14,13,flip.1] f(x,y,f(y,z,f(u,w,f(x,y,z))))=f(u,f(x,y,z),f(y,w,f(x,y,z))). given clause #242: (wt=-994) 25857 [para_from,25587.1.2,25243.1.2,demod,13,14,16069,13,13,flip.1] f(x,y,f(f(z,x,u),f(z,y,w),f(z,y,f(z,x,w))))=f(z,x,y). given clause #243: (wt=-994) 25894 [para_into,1132.1.2.3,24900.1.2,demod,15,2901,15,13,15,14,15,14,14,13,flip.1] f(x,y,f(f(x,z,u),f(x,z,f(z,u,y)),f(z,u,y)))=f(x,z,y). given clause #244: (wt=-994) 25946 [para_from,25716.1.2,23005.1.1.3,demod,15,14,15,14,15,13,15,14,15,13] f(x,y,f(z,u,f(f(x,y,u),f(x,z,u),f(y,z,u))))=f(x,y,u). >> BACK DEMODULATING HINT 590 WITH 25976. >> BACK DEMODULATING HINT 1013 WITH 25978. >> BACK DEMODULATING HINT 591 WITH 25978. given clause #245: (wt=-994) 25975 [para_into,25946.1.1,25894.1.2,demod,14,15,13,13,14,15,13,13,14,15,13,13,25895,14] f(x,y,f(z,u,f(f(x,z,u),f(x,u,y),f(z,u,y))))=f(x,u,y). given clause #246: (wt=39) 1134 (heat=1) [para_into,1083.1.1.3,1.1.2,demod,15,13,13,14,flip.1] f(x,y,f(x,z,f(y,u,w)))=f(x,z,f(y,w,f(x,y,u))). given clause #247: (wt=-994) 25977 [para_into,25946.1.1,24913.1.2,demod,15,14,15,13,15,13,15,13,15,14,15,13,15,13,15,13,14,15,14,15,13,15,13,15,13,24912,15,14] f(x,y,f(z,u,f(f(z,u,x),f(z,u,y),f(u,x,y))))=f(u,x,y). given clause #248: (wt=-993) 25745 [para_from,1125.1.2,23319.1.1.2,demod,10,14,15,14,14,15,14] f(x,f(x,y,z),f(u,y,f(w,y,z)))=f(x,y,z). given clause #249: (wt=-993) 25772 [para_into,25636.1.2,23314.1.2,demod,12,15,14,1247,12] f(x,f(y,z,x),f(y,x,u))=f(x,u,f(y,z,x)). >> BACK DEMODULATING HINT 1015 WITH 26020. >> BACK DEMODULATING HINT 544 WITH 26020. given clause #250: (wt=-993) 26019 [para_from,25772.1.2,25769.1.2,demod,12,flip.1] f(x,f(y,z,x),f(y,x,f(y,u,z)))=f(y,z,x). given clause #251: (wt=47) 1135 (heat=1) [para_into,1083.1.1.3,1.1.1,demod,13,13,15,13] f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(z,f(y,z,u),f(x,w,f(y,z,u))). given clause #252: (wt=-989) 25551 [para_from,4078.1.2,17460.1.2,demod,15,13,15,13,24807,15,13,flip.1] f(x,f(y,z,x),f(x,f(u,y,z),f(y,z,w)))=f(y,z,x). >> BACK DEMODULATING HINT 605 WITH 26045. given clause #253: (wt=-989) 26044 [para_into,25551.1.1,25975.1.2,demod,15,14,15,14,15,14,15,14,25976,15,14] f(x,f(x,y,z),f(x,f(u,y,z),f(y,z,w)))=f(x,y,z). given clause #254: (wt=-987) 6344 (heat=1) [para_into,6040.1.2.3,1.1.2,demod,14,14,13,5140] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). >> BACK DEMODULATING HINT 610 WITH 26066. >> BACK DEMODULATING HINT 605 WITH 26066. >> BACK DEMODULATING HINT 998 WITH 26068. >> BACK DEMODULATING HINT 514 WITH 26068. given clause #255: (wt=-989) 26065 [para_into,6344.1.2,26044.1.1,demod,3502,14,16877,15,14] f(x,f(x,y,z),f(u,f(w,y,z),f(y,z,w5)))=f(x,y,z). given clause #256: (wt=37) 1136 (heat=1) [para_into,1083.1.2.3,1.1.2,demod,14,14,14,15,13] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(x,u,y))). given clause #257: (wt=-989) 26067 [para_into,6344.1.2,25526.1.1,demod,3502,14,3502,15,14] f(x,f(x,y,z),f(u,f(y,z,w),f(y,z,w5)))=f(x,y,z). given clause #258: (wt=-987) 22842 (heat=1) [para_into,22840.1.1.3,1.1.2,demod,12,10,15,14] f(x,f(y,z,u),f(z,x,f(y,u,w)))=f(z,x,f(y,u,w)) # label("Hint 187(27539)"). >> BACK DEMODULATING HINT 1024 WITH 26168. given clause #259: (wt=-994) 26167 [para_into,22842.1.1.3,25977.1.1,demod,15,14,16877,14,15,14,15,15,13,13,flip.1] f(x,y,f(z,u,f(f(x,z,u),f(x,y,u),f(z,y,u))))=f(x,y,u). given clause #260: (wt=-991) 26178 [para_into,22842.1.1.3,1081.1.2,demod,12,15,14,13] f(x,y,f(y,z,f(x,u,y)))=f(x,y,f(u,y,z)) # label("Hint 114(8432)"). given clause #261: (wt=47) 1137 (heat=1) [para_into,1083.1.2.3,1.1.1,demod,15,13,13,13,flip.1] f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(w,f(y,z,u),f(z,x,f(y,z,u))). given clause #262: (wt=-987) 22867 (heat=1) [para_into,22861.1.1.3.3,1.1.2,demod,15,13,13] f(x,f(x,y,z),f(y,u,f(z,w,f(y,z,w5))))=f(x,y,z) # label("Hint 60(1299)"). given clause #263: (wt=-987) 22889 [para_from,16054.1.1,5139.1.1.3,demod,15,14,15,14,15,14] f(x,f(x,y,f(z,u,w)),f(y,z,w))=f(x,y,f(z,u,w)). >> BACK DEMODULATING HINT 496 WITH 26322. given clause #264: (wt=-993) 26321 [para_into,22889.1.2,23866.1.1,demod,14,16877,15,13] f(x,f(x,y,z),f(x,z,f(u,y,z)))=f(x,y,z). given clause #265: (wt=-987) 22921 [para_from,16862.1.1,5139.1.1.3,demod,15,14,15,14,15,14] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)) # label("Hint 143(18121)"). given clause #266: (wt=-985) 1138 (heat=1) [para_from,1083.1.2,1.1.1.1,demod,15,13,14,15,13] f(x,y,f(z,u,f(z,x,w)))=f(z,x,f(x,y,f(z,u,w))) # label("Hint 48(1067)"). given clause #267: (wt=-987) 22922 [para_from,16862.1.1,1085.1.2.3,demod,15,14,13,14,15,14,13] f(x,f(x,y,f(x,z,u)),f(w,z,u))=f(x,y,f(x,z,u)) # label("Hint 77(2670)"). given clause #268: (wt=-987) 23009 [para_into,2900.1.1,2273.1.2,demod,14,14,23008,14] f(x,f(y,z,f(x,z,u)),f(u,w,f(x,z,u)))=f(x,z,u). >> BACK DEMODULATING HINT 503 WITH 26471. >> BACK DEMODULATING HINT 504 WITH 26479. >> BACK DEMODULATING HINT 505 WITH 26488. >> BACK DEMODULATING HINT 4371 WITH 26497. given clause #269: (wt=-987) 23152 [para_into,20441.1.1,2304.1.2,demod,13,13,13,13,13,23149,15,14] f(x,f(x,y,f(y,z,u)),f(u,w,f(x,y,u)))=f(x,y,u). given clause #270: (wt=-987) 23236 [para_into,23148.1.1.3.3,5139.1.1,demod,14] f(x,f(x,y,f(z,u,y)),f(z,u,w))=f(x,y,f(z,u,w)). given clause #271: (wt=49) 1139 (heat=1) [para_into,1084.1.1.3.3,1.1.2,demod,13,15,13,13,14,14,13,flip.1] f(x,y,f(x,f(x,z,u),f(x,w,w5)))=f(x,z,f(x,u,f(x,w5,f(x,y,w)))). given clause #272: (wt=-987) 23394 [para_into,11633.1.1,2818.1.1,demod,15,14] f(x,f(y,z,f(z,x,f(z,u,w))),f(z,x,w))=f(z,x,w). given clause #273: (wt=-987) 23509 [para_into,23297.1.1,23007.1.1,demod,13] f(x,f(y,z,u),f(z,u,f(y,u,x)))=f(u,x,f(y,z,u)). given clause #274: (wt=-994) 26614 [para_into,23509.1.1,25779.1.2] f(f(x,y,z),f(y,z,u),f(y,z,f(x,z,u)))=f(z,u,f(x,y,z)). given clause #275: (wt=-994) 26648 [para_from,26614.1.2,24947.1.2,demod,13,13,24975,15,14,15,14,13,flip.1] f(f(x,y,z),f(u,y,z),f(y,z,f(x,u,z)))=f(x,z,f(u,y,z)). given clause #276: (wt=49) 1140 (heat=1) [para_into,1084.1.1.3.3,1.1.1,demod,13,13,13,14,13,flip.1] f(x,f(x,y,z),f(x,u,f(x,w,w5)))=f(x,w,f(x,w5,f(x,y,f(x,z,u)))). given clause #277: (wt=-987) 23640 [para_from,23528.1.1,23007.1.1,demod,13,flip.1] f(x,f(y,z,u),f(y,z,f(z,x,u)))=f(y,z,f(z,x,u)) # label("Hint 142(17742)"). given clause #278: (wt=-987) 23668 [para_into,1165.1.1.3,16862.1.1,demod,15,14,15,14,14,16877] f(x,f(x,y,f(z,u,w)),f(x,u,w))=f(x,y,f(x,u,w)) # label("Hint 77(2670)"). given clause #279: (wt=-987) 23880 [para_into,23866.1.1,2141.1.2,demod,14,14] f(x,f(x,y,f(z,y,u)),f(x,u,f(z,y,u)))=f(x,y,u). given clause #280: (wt=-987) 25176 [para_into,17460.1.1.2,20441.1.1,demod,15,14,15,13,15,14,13,13,4420,15,14,15,14,13,flip.1] f(x,f(y,x,f(y,z,u)),f(x,u,f(y,z,u)))=f(y,x,u). given clause #281: (wt=69) 1141 (heat=1) [para_into,1084.1.1.3,1.1.1,demod,14,13,13,15,13,13,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(z,w5,f(y,z,u))))=f(w5,f(y,z,u),f(y,z,f(z,u,f(x,w,f(y,z,u))))). given clause #282: (wt=-987) 25295 [para_into,1557.1.1,25243.1.2,demod,15,13,15,13,25244,13] f(x,f(y,z,u),f(y,z,f(y,u,x)))=f(y,x,f(y,z,u)) # label("Hint 137(15872)"). given clause #283: (wt=-987) 25320 (heat=1) [para_into,25302.1.2,1.1.1,demod,13,14,13,23156,13] f(x,f(y,x,z),f(u,w,w5))=f(y,x,f(x,z,f(u,w,w5))) # label("Hint 70(2227)"). >> BACK DEMODULATING HINT 805 WITH 26816. >> BACK DEMODULATING HINT 1036 WITH 26818. >> BACK DEMODULATING HINT 804 WITH 26818. >> BACK DEMODULATING HINT 811 WITH 26820. >> BACK DEMODULATING HINT 802 WITH 26822. >> BACK DEMODULATING HINT 746 WITH 26838. >> BACK DEMODULATING HINT 742 WITH 26838. >> BACK DEMODULATING HINT 808 WITH 26840. NEW HINT: 26853 [bsub_wt=2147483647, bsub_add_wt=-1024] f(f(x,y,f(y,z,u)),f(y,z,u),f(f(y,z,u),f(z,u,w),f(w5,w6,w7)))=f(y,z,u) # label(bd). >> BACK DEMODULATING HINT 788 WITH 26887. >> BACK DEMODULATING HINT 786 WITH 26900. >> BACK DEMODULATING HINT 783 WITH 26900. >> BACK DEMODULATING HINT 567 WITH 26923. given clause #284: (wt=-996) 26815 [para_into,25320.1.1.2,24078.1.1,demod,10,14,flip.1] f(x,f(y,x,z),f(f(y,x,z),f(y,z,u),f(w,w5,w6)))=f(y,x,z) # label("Hint 167(24453)"). given clause #285: (wt=-996) 26817 [para_into,25320.1.1.2,16876.1.1,demod,10,15,13,flip.1] f(x,f(x,y,z),f(f(x,y,z),f(y,z,u),f(w,w5,w6)))=f(x,y,z) # label("Hint 166(24325)"). >> BACK DEMODULATING HINT 565 WITH 26944. >> BACK DEMODULATING HINT 519 WITH 26944. >> BACK DEMODULATING HINT 26853 WITH 26946. given clause #286: (wt=27) 1142 (heat=1) [para_into,1084.1.1,1.1.2,demod,11,13,12,14,13,flip.1] f(x,y,f(x,z,u))=f(x,z,f(x,y,u)). given clause #287: (wt=-996) 26819 [para_into,25320.1.1.2,5139.1.1,demod,10,flip.1] f(x,f(y,z,x),f(f(y,z,x),f(y,z,u),f(w,w5,w6)))=f(y,z,x) # label("Hint 173(26393)"). given clause #288: (wt=-994) 26886 [para_from,25320.1.2,5959.1.1.2,demod,14] f(f(x,y,z),f(x,z,u),f(y,f(x,y,z),f(w,w5,w6)))=f(x,y,z) # label("Hint 150(18832)"). >> BACK DEMODULATING HINT 803 WITH 26950. given clause #289: (wt=-994) 26943 [para_into,26817.1.1,1085.1.2,demod,14] f(f(x,y,z),f(x,f(x,y,z),f(u,w,w5)),f(y,z,w6))=f(x,y,z). >> BACK DEMODULATING HINT 568 WITH 26961. NEW HINT: 26964 [bsub_wt=2147483647, bsub_add_wt=-1024] f(x,y,f(f(x,y,z),f(z,u,f(x,y,z)),f(w,w5,w6)))=f(x,y,z). given clause #290: (wt=-994) 26949 [para_into,26886.1.1,25243.1.2,demod,14,14,13,14,14,13,23867,14] f(f(x,y,z),f(x,y,u),f(u,f(x,y,u),f(w,w5,w6)))=f(x,y,u) # label("Hint 165(24313)"). >> BACK DEMODULATING HINT 990 WITH 26966. >> BACK DEMODULATING HINT 564 WITH 26966. >> BACK DEMODULATING HINT 512 WITH 26966. given clause #291: (wt=69) 1143 (heat=1) [para_into,1084.1.1,1.1.1,demod,14,13,13,15,13,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(z,w5,f(y,z,u))))=f(y,z,f(z,u,f(w5,f(y,z,u),f(x,w,f(y,z,u))))). given clause #292: (wt=-994) 26960 (heat=1) [para_into,26955.1.1.3,1.1.2,demod,15,13,14,15,13,13,15,13] f(x,y,f(f(x,y,z),f(u,z,f(x,y,z)),f(w,w5,w6)))=f(x,y,z). >> BACK DEMODULATING HINT 26964 WITH 26976. >> BACK DEMODULATING HINT 569 WITH 26978. given clause #293: (wt=-994) 26965 [para_into,26949.1.1.1,26819.1.2,demod,15,14,15,14,26818] f(f(x,y,z),f(y,z,u),f(u,f(y,z,u),f(w,w5,w6)))=f(y,z,u). >> BACK DEMODULATING HINT 566 WITH 26997. given clause #294: (wt=-994) 26975 [para_into,26960.1.1.3.1,26949.1.2,demod,26950,13] f(x,y,f(f(x,y,z),f(z,u,f(x,y,z)),f(w,w5,w6)))=f(x,y,z). given clause #295: (wt=-994) 26977 [para_into,26960.1.1.3.2,3218.1.2,demod,15,13] f(x,y,f(f(x,y,z),f(x,z,f(y,z,u)),f(w,w5,w6)))=f(x,y,z). >> BACK DEMODULATING HINT 583 WITH 27008. given clause #296: (wt=49) 1144 (heat=1) [para_into,1084.1.2.3.3,1.1.2,demod,13,14,14,15,13,13] f(x,f(x,y,f(x,z,u)),f(w,y,w5))=f(x,z,f(x,u,f(y,w5,f(x,w,y)))). given clause #297: (wt=-1000) 27007 [para_into,26977.1.1.3,25769.1.1,demod,15,13] f(x,y,f(f(x,y,z),f(x,z,u),f(y,z,w)))=f(x,y,z). >> BACK DEMODULATING HINT 584 WITH 27065. given clause #298: (wt=-1000) 27064 [para_from,27007.1.2,26819.1.2,demod,15,14,15,14,26818,15,14,13,13,flip.1] f(x,y,f(f(z,x,y),f(z,x,u),f(z,y,w)))=f(z,x,y). given clause #299: (wt=-993) 26837 [para_into,25320.1.2,1136.1.1,demod,14,1128,10,14,1128,14,flip.1] f(x,y,f(z,f(x,z,y),f(u,w,w5)))=f(x,z,y) # label("Hint 108(7501)"). given clause #300: (wt=-993) 26922 (heat=1) [para_into,26894.1.1,1.1.2,demod,11,1128] f(x,y,f(z,f(x,y,z),f(u,w,w5)))=f(x,y,z). given clause #301: (wt=67) 1145 (heat=1) [para_into,1084.1.2.3.3,1.1.1,demod,14,13,13,13,13,flip.1] f(x,f(y,z,u),f(w,f(y,z,u),f(y,z,f(z,u,w5))))=f(w5,f(y,z,u),f(z,f(y,z,u),f(x,w,f(y,z,u)))). given clause #302: (wt=-990) 26899 [para_from,25320.1.2,5959.1.1.2.3] f(f(x,y,z),f(x,y,f(z,f(y,z,u),f(w,w5,w6))),f(x,z,w7))=f(x,y,z) # label("Hint 148(18782)"). given clause #303: (wt=-989) 26996 [para_into,26965.1.1.1,2.1.1] f(x,f(x,y,z),f(z,f(x,y,z),f(u,w,w5)))=f(x,y,z). given clause #304: (wt=-987) 25539 (heat=1) [para_into,25524.1.1.3.3,1.1.2,demod,11] f(x,f(x,y,f(y,z,u)),f(x,u,f(y,z,u)))=f(x,y,u). given clause #305: (wt=-987) 25731 [para_into,1125.1.2.3,1122.1.2,demod,11,11,11,14,13,11,11,11,15,13,13] f(x,f(y,z,u),f(u,x,w))=f(x,w,f(y,u,f(z,u,x))). given clause #306: (wt=69) 1146 (heat=1) [para_into,1084.1.2.3,1.1.1,demod,15,14,13,13,15,13,flip.1] f(x,f(y,z,u),f(y,z,f(z,u,f(w,w5,f(y,z,u)))))=f(w,f(y,z,u),f(w5,f(y,z,u),f(z,x,f(y,z,u)))). given clause #307: (wt=-987) 26180 [para_into,22842.1.1,1832.1.1,demod,15,13] f(x,f(y,z,u),f(y,w,f(x,z,w)))=f(x,w,f(y,z,u)) # label("Hint 191(28987)"). given clause #308: (wt=-987) 26204 [para_from,22842.1.2,26019.1.2,demod,14,4376,14,flip.1] f(x,f(y,z,u),f(u,x,f(y,z,w)))=f(u,x,f(y,z,w)) # label("Hint 185(27403)"). given clause #309: (wt=-987) 26317 [para_into,22889.1.1,2559.1.1,demod,14,13] f(x,f(y,z,u),f(u,w,f(x,y,w)))=f(x,w,f(y,z,u)). given clause #310: (wt=-987) 26395 [para_from,22921.1.2,26019.1.2,demod,14,4376,15,13,14,flip.1] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)) # label("Hint 183(27303)"). >> BACK DEMODULATING HINT 592 WITH 27364. >> BACK DEMODULATING HINT 1028 WITH 27368. >> BACK DEMODULATING HINT 595 WITH 27368. given clause #311: (wt=51) 1147 (heat=1) [para_into,1084.1.2,1.1.1,demod,13,15,13,14,13,13,flip.1] f(x,y,f(x,z,f(x,u,f(x,w,w5))))=f(x,w,f(x,w5,f(x,u,f(x,y,z)))). given clause #312: (wt=-996) 27367 [para_into,26395.1.1.3,25684.1.1,demod,14,15,14,14,14,13,25756] f(x,f(x,y,z),f(f(x,y,z),f(y,u,w),f(y,w,z)))=f(x,y,z). >> BACK DEMODULATING HINT 1031 WITH 27413. >> BACK DEMODULATING HINT 596 WITH 27413. given clause #313: (wt=-996) 27412 [para_from,27367.1.1,23640.1.1.3,demod,13,14,25244,13,12,13,13,15,13,flip.1] f(x,f(y,x,z),f(f(y,u,w),f(y,w,z),f(y,x,z)))=f(y,x,z). >> BACK DEMODULATING HINT 1032 WITH 27417. >> BACK DEMODULATING HINT 597 WITH 27417. given clause #314: (wt=-996) 27416 [para_from,27412.1.1,24175.1.1.3,demod,14,14,12,14,14,14,13,flip.1] f(x,f(y,z,x),f(f(y,u,z),f(y,u,w),f(y,z,x)))=f(y,z,x). >> BACK DEMODULATING HINT 598 WITH 27419. given clause #315: (wt=-996) 27418 [para_into,27416.1.1,26395.1.2,demod,15,14,15,14,12,15,14,15,14,15,1128,15,14] f(x,f(x,y,z),f(f(x,y,z),f(y,u,w),f(y,u,z)))=f(x,y,z). >> BACK DEMODULATING HINT 599 WITH 27421. given clause #316: (wt=49) 1148 (heat=1) [para_from,1084.1.1,1.1.2.3,demod,13,13,15,14,13] f(x,f(y,x,z),f(z,u,f(z,w,w5)))=f(y,x,f(z,w,f(z,w5,f(x,z,u)))). given clause #317: (wt=-996) 27420 [para_from,27418.1.1,23640.1.1.3,demod,13,14,25244,13,12,13,13,15,13,flip.1] f(x,f(y,x,z),f(f(y,u,w),f(y,u,z),f(y,x,z)))=f(y,x,z). given clause #318: (wt=-994) 27363 [para_into,26395.1.1.3,26167.1.1,demod,14,14,15,14,14,14,14,3502,14,14,15,14,13,flip.1] f(x,y,f(z,u,f(f(x,z,u),f(x,z,y),f(z,u,y))))=f(x,z,y). given clause #319: (wt=-987) 26411 [para_from,22921.1.2,5.1.2,demod,15,13,13,15,13,14,flip.1] f(x,f(y,z,u),f(u,x,f(w,y,z)))=f(u,x,f(w,y,z)) # label("Hint 184(27312)"). given clause #320: (wt=-987) 26470 [para_into,23009.1.1.3,22921.1.1,demod,15,13,13,14] f(x,f(x,y,f(z,y,u)),f(w,z,f(x,z,y)))=f(x,z,y). given clause #321: (wt=51) 1149 (heat=1) [para_from,1084.1.1,1.1.1.1,demod,15,13,15,13] f(x,y,f(z,u,f(u,w,f(u,w5,x))))=f(u,x,f(x,y,f(u,w5,f(z,u,w)))). given clause #322: (wt=-987) 26478 [para_into,23009.1.1,16862.1.2,demod,15,14,15,14,13,13,15,14,13,15,14,14,25244,15,14] f(x,f(y,z,f(y,x,u)),f(u,w,f(y,x,u)))=f(y,x,u). given clause #323: (wt=-987) 26487 (heat=1) [para_into,26470.1.1.3,1.1.2,demod,13,15,15,14] f(x,f(x,y,f(y,z,u)),f(y,z,f(x,z,w)))=f(x,y,z). given clause #324: (wt=-987) 26515 [para_into,23236.1.1.2,3218.1.2,demod,14] f(x,f(y,z,f(x,z,u)),f(y,u,w))=f(x,z,f(y,u,w)). >> BACK DEMODULATING HINT 614 WITH 27566. given clause #325: (wt=-994) 27565 [para_into,26515.1.1,25977.1.1,demod,15,14,2901,15,13,15,14,13,23019,15,14,2901,14,13,flip.1] f(x,y,f(z,u,f(f(z,x,u),f(z,x,y),f(z,u,y))))=f(z,x,y). given clause #326: (wt=69) 1150 (heat=1) [para_from,1084.1.1,1.1.1,demod,15,13,14,15,13,13,flip.1] f(x,y,f(y,z,f(u,f(w,w5,f(x,y,z)),f(x,y,z))))=f(w,f(x,y,z),f(w5,f(x,y,z),f(y,u,f(x,y,z)))). given clause #327: (wt=-987) 27322 [para_from,26317.1.2,25977.1.2,demod,15,14,13,14,25976,15,13,14,flip.1] f(x,f(y,z,f(y,u,x)),f(u,w,z))=f(y,x,f(u,w,z)). given clause #328: (wt=-987) 27362 [para_into,26395.1.1.3,26180.1.1,demod,14,13,13,14,16069,13,14,13,14,flip.1] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)) # label("Hint 188(27551)"). given clause #329: (wt=-987) 27402 [para_from,26395.1.1,1096.1.1.3,demod,1128,15,14,14,flip.1] f(x,f(x,y,f(y,z,u)),f(w,z,u))=f(x,y,f(w,z,u)) # label("Hint 56(1174)"). given clause #330: (wt=-987) 27403 [para_from,26395.1.2,23236.1.1.2,demod,12,15,13,1128,13,13] f(x,f(x,y,f(z,y,u)),f(z,u,w))=f(x,y,f(z,u,w)). given clause #331: (wt=49) 1151 (heat=1) [para_from,1084.1.2,1.1.2.3,demod,13,13] f(x,f(y,x,z),f(x,u,f(x,w,w5)))=f(y,x,f(x,w5,f(x,w,f(x,z,u)))). given clause #332: (wt=-987) 27685 [para_into,27362.1.1,5.1.2,demod,15,13,15,14,13] f(x,f(y,z,u),f(z,w,f(y,w,x)))=f(w,x,f(y,z,u)). given clause #333: (wt=-985) 1719 (heat=1) [para_into,1703.1.1.3,1.1.2,demod,11,1128,flip.1] f(x,y,f(z,u,f(x,z,w)))=f(x,z,f(x,y,f(z,u,w))). given clause #334: (wt=-985) 1902 (heat=1) [para_from,1875.1.2,1.1.2,demod,11,1128,flip.1] f(x,y,f(x,z,f(u,y,w)))=f(x,z,f(u,y,f(x,y,w))) # label("Hint 37(989)"). given clause #335: (wt=-985) 25885 [para_into,1132.1.1,24985.1.2,demod,15,14,15,14,24986,13] f(x,y,f(z,u,f(x,u,w)))=f(x,u,f(x,y,f(z,u,w))) # label("Hint 37(989)"). given clause #336: (wt=51) 1152 (heat=1) [para_from,1084.1.2,1.1.1.1,demod,13,15,13,14,15,13,13] f(x,y,f(x,z,f(x,u,f(x,w,w5))))=f(x,w,f(x,y,f(x,w5,f(x,z,u)))). given clause #337: (wt=-985) 26974 [para_from,1143.1.2,1081.1.2,demod,11,11,15,14,13,11,14,11,11,11,15,13,13,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,w,f(x,u,f(x,y,z))). given clause #338: (wt=-984) 25723 [para_into,1125.1.1.3,8612.1.2,demod,15,13,13,15,14,16863,15,13,15,14,13,flip.1] f(f(x,y,z),f(x,y,u),f(y,z,f(w,x,y)))=f(w,f(x,y,z),f(y,u,f(x,y,z))) # label("Hint 133(13466)"). given clause #339: (wt=-983) 24872 [para_into,24850.1.1.2,5287.1.1,demod,13,14,13,3659,14,flip.1] f(x,f(y,x,z),f(u,w,f(y,u,x)))=f(x,f(y,u,x),f(y,x,z)). given clause #340: (wt=-987) 27826 [para_from,24872.1.2,27322.1.2,demod,13,1247,14,16863,flip.1] f(x,f(y,x,z),f(u,w,f(y,u,x)))=f(x,z,f(y,u,x)). given clause #341: (wt=39) 1153 (heat=1) [para_into,1085.1.1.3,1.1.2,demod,