----- Otter 3.3f (UNM), August 2004 (mod 2005-apr-14, parse) ----- The process was started by veroff on pacaderm, Sat Jul 23 00:34:18 2005 The command was "otter -f median_df.in". The process ID is 24611. % Reading file median_df.in. lex([A,B,C,D,E,f(x,x,x)]). set(para_from). set(para_into). set(lex_order_vars). set(order_eq). assign(bsub_hint_add_wt,-1024). set(keep_hint_subsumers). set(degrade_hints2). set(input_sos_first). set(ancestor_subsume). assign(max_weight,10). assign(max_mem,750000). set(print_proof_as_hints). dependent: set(build_proof_object_1). dependent: set(order_history). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). 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(sos). 1 [] f(x,x,y)=x. 2 [] f(x,y,x)=x. 3 [] f(y,x,x)=x. 4 [] f(x,y,z)=f(y,x,z). 5 [] f(x,y,z)=f(x,z,y). 6 [] f(x,y,z)=f(z,y,x). 7 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). end_of_list. list(passive). 8 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C))|$ANS("distributivity"). end_of_list. list(hints2). 9 [] f(y,z,x)=f(x,y,z). 10 [] f(z,x,y)=f(x,y,z). 11 [] f(f(x,y,z),y,u)=f(z,y,f(x,y,u)). 12 [] f(f(x,y,z),z,u)=f(x,z,f(y,z,u)). 13 [] f(f(x,y,z),x,u)=f(y,x,f(z,x,u)). 14 [] f(x,y,f(x,y,z))=f(x,y,z). 15 [] f(z,y,f(u,y,x))=f(x,y,f(z,y,u)). 16 [] f(y,x,f(z,x,u))=f(x,f(y,x,z),u). 17 [] f(f(x,y,z),y,z)=f(x,y,z). 18 [] f(y,f(x,y,z),u)=f(x,y,f(z,y,u)). 19 [] f(z,x,f(u,x,y))=f(x,y,f(z,x,u)). 20 [] f(y,u,f(x,y,z))=f(x,y,f(z,y,u)). 21 [] f(x,y,f(z,x,y))=f(x,y,z). 22 [] f(x,x,y)=f(x,x,x). 23 [] f(f(x,y,z),y,x)=f(x,y,z). 24 [] f(x,f(x,y,z),y)=f(x,y,z). 25 [] f(x,y,f(y,x,z))=f(y,x,z). 26 [] f(x,y,f(x,y,z))=f(y,x,z). 27 [] f(x,x,y)=f(x,x,x). 28 [] f(x,x,z)=f(x,x,y). 29 [] f(x,y,f(z,x,y))=f(z,x,y). 30 [] f(f(x,y,z),y,x)=f(z,x,y). 31 [] f(x,y,f(y,x,f(x,y,z)))=f(x,y,z). 32 [] f(f(x,y,z),y,f(x,f(x,y,z),y))=f(z,x,y). 33 [] f(y,u,f(z,y,x))=f(x,y,f(z,y,u)). 34 [] f(u,x,f(z,x,y))=f(x,y,f(z,x,u)). 35 [] f(z,y,f(x,y,u))=f(x,y,f(z,y,u)). 36 [] f(z,x,f(u,x,y))=f(x,y,f(z,u,x)). 37 [] f(z,y,f(u,y,x))=f(x,y,f(z,u,y)). 38 [] f(y,u,f(x,z,y))=f(x,y,f(z,y,u)). 39 [] f(y,u,f(y,x,z))=f(x,y,f(z,y,u)). 40 [] f(z,x,f(u,x,y))=f(x,y,f(x,z,u)). 41 [] f(u,y,f(z,y,x))=f(x,y,f(z,u,y)). 42 [] f(u,y,f(z,x,y))=f(x,y,f(z,y,u)). 43 [] f(y,x,f(x,z,u))=f(x,f(y,x,z),u). 44 [] f(y,f(x,y,z),u)=f(x,y,f(y,z,u)). 45 [] f(y,u,f(z,x,y))=f(x,y,f(z,y,u)). 46 [] f(u,x,f(z,x,y))=f(x,y,f(z,u,x)). 47 [] f(y,z,f(x,y,u))=f(x,y,f(y,z,u)). 48 [] f(z,x,f(x,y,u))=f(x,y,f(z,x,u)). 49 [] f(y,u,f(x,y,z))=f(x,y,f(y,z,u)). 50 [] f(z,x,f(x,u,y))=f(x,y,f(z,x,u)). 51 [] f(x,f(y,x,z),u)=f(x,z,f(y,x,u)). 52 [] f(x,u,f(z,x,y))=f(x,y,f(z,x,u)). 53 [] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(u,f(x,y,z),f(x,y,z)). 54 [] f(z,x,f(u,y,x))=f(x,y,f(z,u,x)). 55 [] f(y,u,f(x,z,y))=f(x,y,f(z,u,y)). 56 [] f(z,y,f(x,u,y))=f(x,y,f(z,u,y)). 57 [] f(z,x,f(x,u,y))=f(x,y,f(x,z,u)). 58 [] f(y,u,f(y,x,z))=f(x,y,f(y,z,u)). 59 [] f(u,y,f(z,x,y))=f(x,y,f(z,u,y)). 60 [] f(y,f(x,z,y),u)=f(x,y,f(y,z,u)). 61 [] f(y,x,f(x,z,u))=f(x,f(y,z,x),u). 62 [] f(y,f(y,x,z),u)=f(x,y,f(y,z,u)). 63 [] f(y,x,f(x,z,u))=f(x,f(x,y,z),u). 64 [] f(y,f(x,y,z),f(z,u,w))=f(x,y,f(z,u,f(y,z,w))). 65 [] f(y,x,f(z,u,f(x,z,w)))=f(x,f(y,x,z),f(z,u,w)). 66 [] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). 67 [] f(x,z,f(y,x,u))=f(x,y,f(x,z,u)). 68 [] f(x,z,f(x,y,u))=f(x,y,f(z,x,u)). 69 [] f(w,x,f(y,u,f(x,y,z)))=f(x,f(y,z,u),f(w,x,y)). 70 [] f(y,f(z,w,u),f(x,y,z))=f(x,y,f(z,u,f(y,z,w))). 71 [] f(u,x,f(x,y,f(x,w,z)))=f(x,y,f(x,z,f(u,x,w))). 72 [] f(y,z,f(y,w,f(x,y,u)))=f(x,y,f(y,z,f(y,u,w))). 73 [] f(x,f(x,y,z),u)=f(x,z,f(y,x,u)). 74 [] f(x,u,f(x,z,y))=f(x,y,f(z,x,u)). 75 [] f(x,u,f(z,x,y))=f(x,y,f(x,z,u)). 76 [] 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))). 77 [] f(u,f(x,y,z),f(y,w,f(x,y,z)))=f(x,y,f(y,z,f(u,w,f(x,y,z)))). 78 [] f(x,u,f(x,y,z))=f(x,y,f(x,z,u)). 79 [] f(x,z,f(x,u,y))=f(x,y,f(x,z,u)). 80 [] f(x,f(y,z,x),f(z,x,u))=f(y,x,f(z,x,u)). 81 [] f(x,f(x,y,z),u)=f(x,y,f(x,z,u)). 82 [] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(u,y,x))). 83 [] f(x,u,f(x,z,y))=f(x,y,f(x,z,u)). 84 [] f(y,x,f(z,w,f(u,z,x)))=f(x,f(y,x,z),f(z,u,w)). 85 [] f(y,f(x,y,z),f(z,w,u))=f(x,y,f(z,u,f(w,z,y))). 86 [] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). 87 [] f(x,w,f(y,z,f(x,y,u)))=f(x,y,f(x,f(y,z,u),w)). 88 [] f(x,z,f(x,f(z,u,w),y))=f(x,y,f(z,u,f(x,z,w))). 89 [] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). 90 [] f(x,f(x,y,z),f(z,u,w))=f(x,y,f(z,u,f(x,z,w))). 91 [] f(x,f(x,y,z),f(u,z,w))=f(x,y,f(u,z,f(x,z,w))). 92 [] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)). 93 [] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)). 94 [] f(z,x,f(y,u,f(x,y,w)))=f(x,f(x,y,z),f(y,u,w)). 95 [] f(y,f(y,z,x),f(z,u,w))=f(x,y,f(z,u,f(y,z,w))). 96 [] f(w5,x,f(x,y,f(z,w,f(x,z,u))))=f(x,y,f(x,f(z,u,w),f(w5,x,z))). 97 [] f(y,z,f(y,f(u,w5,w),f(x,y,u)))=f(x,y,f(y,z,f(u,w,f(y,u,w5)))). 98 [] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(x,y,u))). 99 [] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,u,f(x,w,z))). 100 [] f(x,z,f(x,w,f(x,u,y)))=f(x,y,f(x,z,f(x,u,w))). 101 [] f(y,f(y,z,x),f(z,u,w))=f(x,y,f(z,u,f(z,w,y))). 102 [] f(z,x,f(y,u,f(y,w,x)))=f(x,f(x,y,z),f(y,u,w)). 103 [] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,u,f(x,y,w))). 104 [] f(w5,f(y,z,f(y,u,w)),f(y,x,f(y,z,f(y,u,w))))=f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5)))). 105 [] f(w5,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,x))))=f(x,f(y,z,f(y,u,w)),f(y,w5,f(y,z,f(y,u,w)))). 106 [] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(x,y,z). 107 [] f(x,f(x,y,z),f(y,u,f(x,y,z)))=f(x,y,z). 108 [] f(x,f(x,f(x,y,z),y),f(y,u,z))=f(x,y,z). 109 [] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). 110 [] f(x,f(x,y,z),f(y,z,u))=f(x,y,z). 111 [] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). 112 [] f(x,f(x,y,z),f(y,u,z))=f(y,z,x). 113 [] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). 114 [] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). 115 [] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). 116 [] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)). 117 [] f(x,f(y,x,z),f(z,u,y))=f(z,y,x). 118 [] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). 119 [] f(x,f(x,y,f(z,u,w)),f(z,w,y))=f(x,y,f(z,u,w)). 120 [] f(x,f(y,z,f(u,z,w)),f(x,z,w))=f(x,z,w). 121 [] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). 122 [] f(x,f(y,z,u),f(x,z,u))=f(z,u,x). 123 [] f(x,y,f(z,x,f(u,z,y)))=f(z,x,y). 124 [] f(x,f(y,z,u),f(z,u,x))=f(z,u,x). 125 [] f(x,f(y,z,u),f(y,z,x))=f(y,z,x). 126 [] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). 127 [] f(x,f(y,z,u),f(u,f(y,z,w),x))=f(u,f(y,z,w),x). 128 [] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). 129 [] 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)). 130 [] f(x,y,f(y,z,f(z,u,f(x,z,w))))=f(x,y,z). 131 [] f(x,f(y,z,u),f(y,x,z))=f(y,x,z). 132 [] f(x,f(y,z,u),f(u,x,f(w,y,z)))=f(u,x,f(w,y,z)). 133 [] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(w,f(x,y,z),f(x,y,z)). 134 [] f(x,f(x,y,f(z,u,w)),f(z,y,u))=f(x,y,f(z,u,w)). 135 [] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). 136 [] f(x,f(y,z,u),f(x,w,f(y,u,f(y,z,w))))=f(x,w,f(y,z,u)). 137 [] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(x,y,z). 138 [] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u). 139 [] f(f(x,y,f(z,y,u)),f(y,z,u),f(z,u,w))=f(z,y,u). 140 [] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(z,y,u). 141 [] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). 142 [] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). 143 [] f(x,f(y,z,u),f(x,u,f(y,w,z)))=f(x,u,f(y,w,z)). 144 [] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). 145 [] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). 146 [] f(u,f(y,z,w),f(y,z,x))=f(x,f(y,z,u),f(y,z,w)). 147 [] f(x,f(y,z,u),f(x,z,f(u,w,y)))=f(x,z,f(u,w,y)). 148 [] f(w,f(y,z,u),f(x,f(y,z,u),f(z,w5,f(y,z,u))))=f(x,f(y,z,u),f(y,z,f(z,u,f(w,w5,f(y,z,u))))). 149 [] f(w,f(y,z,u),f(y,z,f(z,u,f(x,w5,f(y,z,u)))))=f(x,f(y,z,u),f(w,f(y,z,u),f(z,w5,f(y,z,u)))). 150 [] f(x,f(y,z,u),f(x,w,f(y,z,w)))=f(x,f(y,z,u),w). 151 [] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)). 152 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(y,z,f(x,y,z)),f(y,z,u)). 153 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). 154 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 155 [] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 156 [] f(w,f(y,z,u),f(z,u,x))=f(x,f(y,z,u),f(z,u,w)). 157 [] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). 158 [] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). 159 [] f(y,f(w,z,u),f(z,u,x))=f(x,f(y,z,u),f(z,u,w)). 160 [] f(w,f(x,z,u),f(z,u,y))=f(x,f(y,z,u),f(z,u,w)). 161 [] f(w,f(u,y,z),f(z,u,x))=f(x,f(y,z,u),f(z,u,w)). 162 [] f(w,f(z,u,y),f(u,y,x))=f(x,f(y,z,u),f(u,y,w)). 163 [] f(w,f(x,z,u),f(y,z,u))=f(x,f(y,z,u),f(z,u,w)). 164 [] f(y,f(w,z,u),f(z,u,x))=f(x,f(y,z,u),f(w,z,u)). 165 [] f(w,f(z,u,y),f(u,y,x))=f(x,f(y,z,u),f(y,u,w)). 166 [] f(w,f(u,y,z),f(u,z,x))=f(x,f(y,z,u),f(z,u,w)). 167 [] f(w,f(y,z,u),f(y,u,x))=f(x,f(y,z,u),f(u,y,w)). 168 [] f(w,f(y,z,u),f(u,y,x))=f(x,f(y,z,u),f(y,u,w)). 169 [] f(w,f(y,z,u),f(x,y,u))=f(x,f(y,z,u),f(y,u,w)). 170 [] f(w,f(y,z,u),f(y,u,x))=f(x,f(y,z,u),f(w,y,u)). 171 [] f(y,f(z,w,u),f(z,u,x))=f(x,f(y,z,u),f(z,w,u)). 172 [] f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,f(x,w,f(y,z,u)),f(y,w,z)). 173 [] f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,w,f(y,z,u)). 174 [] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)). 175 [] f(x,f(y,f(z,u,w),f(x,y,w5)),f(w5,u,w))=f(x,y,f(w5,f(z,u,w),f(w5,u,w))). 176 [] f(x,f(y,f(x,y,z),f(u,w,w5)),f(z,w,w5))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). 177 [] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). 178 [] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(w,w5,z)). 179 [] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(x,z,y))). 180 [] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(z,y,x))). 181 [] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,x)). 182 [] f(x,y,f(z,y,f(u,y,f(w,x,z))))=f(z,y,f(y,u,x)). 183 [] f(x,y,f(z,y,f(u,y,f(z,x,w))))=f(z,y,f(y,u,x)). 184 [] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). 185 [] f(x,y,f(z,u,f(u,x,f(u,y,w))))=f(u,x,y). 186 [] f(x,f(y,z,u),f(w,z,f(x,w,u)))=f(x,w,f(y,z,u)). 187 [] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). 188 [] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). 189 [] f(x,y,f(x,f(y,z,u),f(w,z,u)))=f(x,y,f(w,z,u)). 190 [] f(x,f(x,y,z),f(u,z,f(x,u,w)))=f(x,y,f(x,u,z)). 191 [] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). 192 [] f(y,f(x,y,u),f(y,z,w))=f(x,y,f(y,z,f(y,u,w))). 193 [] f(y,x,f(x,u,f(x,z,w)))=f(x,f(y,x,z),f(x,u,w)). 194 [] f(x,y,f(x,z,f(u,x,y)))=f(u,x,f(x,y,z)). 195 [] f(x,y,f(x,z,f(x,y,u)))=f(u,x,f(x,y,z)). 196 [] f(x,y,f(x,f(x,y,z),u))=f(z,x,f(x,y,u)). 197 [] f(x,y,f(x,f(x,y,z),u))=f(x,z,f(x,y,u)). 198 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w). 199 [] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,w,z). 200 [] f(x,f(y,z,u),f(z,u,f(w,y,f(y,z,f(y,w5,u)))))=f(y,u,z). 201 [] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,y,x). 202 [] f(x,y,f(z,z,u))=f(z,y,x). 203 [] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). 204 [] f(x,f(y,z,u),w)=f(x,w,f(y,u,z)). 205 [] f(x,y,f(z,y,f(y,u,f(z,x,w))))=f(z,y,f(y,u,x)). 206 [] f(x,y,f(z,x,f(x,u,f(z,y,w))))=f(z,x,f(x,u,y)). 207 [] f(y,z,f(y,f(u,w5,w),f(y,u,x)))=f(x,y,f(y,z,f(u,w,f(y,u,w5)))). 208 [] f(w5,x,f(x,y,f(z,w,f(x,z,u))))=f(x,y,f(x,f(z,u,w),f(x,z,w5))). 209 [] f(u,x,f(x,y,f(z,w5,f(x,z,w))))=f(x,y,f(x,f(x,z,u),f(z,w,w5))). 210 [] f(y,z,f(y,f(y,u,x),f(u,w5,w)))=f(x,y,f(y,z,f(u,w,f(y,u,w5)))). 211 [] f(x,z,f(x,f(x,u,y),f(u,w5,w)))=f(x,y,f(x,z,f(u,w,f(x,u,w5)))). 212 [] f(x,u,f(x,y,f(z,w5,f(x,z,w))))=f(x,y,f(x,f(x,z,u),f(z,w,w5))). 213 [] f(x,y,f(x,f(z,u,f(x,w,y)),f(w,u,f(x,w,z))))=f(x,f(x,w,y),f(w,z,u)). 214 [] f(z,f(y,z,f(z,y,u)),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u))))))=f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z)))). 215 [] f(u,f(y,x,f(x,y,z)),f(x,w,f(x,f(x,y,f(y,x,f(x,y,z))),f(y,z,x))))=f(x,f(y,x,f(x,y,z)),f(y,x,f(x,f(x,y,z),f(u,w,f(y,x,f(x,y,z)))))). 216 [] f(x,y,f(x,z,f(u,w,f(x,z,y))))=f(x,f(x,z,y),f(z,u,w)). 217 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). 218 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(z,y,u))))). 219 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,y,f(z,f(z,y,u),f(x,w,f(z,y,u))))). 220 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,u,f(z,y,f(x,w,f(z,y,u))))). 221 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,f(z,y,u),f(y,x,w))). 222 [] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,x,w)). 223 [] f(x,f(y,z,u),f(y,w,f(y,f(y,z,f(z,y,f(y,z,u))),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). 224 [] f(x,f(y,z,u),f(y,w,f(y,f(y,z,u),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). 225 [] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(z,x,w)). 226 [] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(w,z,x)). 227 [] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(w,z,x),f(y,z,u)). 228 [] f(x,f(y,z,u),f(y,z,f(w,y,u)))=f(y,f(w,z,x),f(y,z,u)). 229 [] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(y,f(x,z,w5),f(y,z,f(y,u,w))). 230 [] f(x,f(y,z,f(x,u,w)),f(y,z,f(w,y,f(x,u,w))))=f(y,z,f(x,u,w)). 231 [] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(z,y,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). 232 [] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(y,z,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). 233 [] f(x,f(y,z,u),f(z,u,f(z,f(y,z,w),f(y,z,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5))))). 234 [] f(y,f(w,x,z),f(x,z,f(w,x,f(x,u,f(w,z,w5)))))=f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5))))). 235 [] f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5)))))=f(x,f(y,z,u),f(z,u,f(y,z,f(z,w,f(y,u,w5))))). 236 [] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,u,z))). 237 [] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,z,u))). 238 [] f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(z,f(x,u,w),f(y,z,u)). 239 [] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,u,w),f(y,z,u)). 240 [] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(x,u,w),f(y,z,u)). 241 [] f(f(x,y,z),f(x,y,u),f(y,u,w))=f(y,f(w,u,z),f(x,y,u)). 242 [] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(w,u,x),f(y,z,u)). 243 [] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(z,u,y)). 244 [] f(x,f(y,z,u),f(z,u,f(w,y,z)))=f(z,f(w,u,x),f(y,z,u)). 245 [] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(y,z,u)). 246 [] f(f(x,y,z),f(y,z,u),f(z,u,w))=f(z,f(x,u,w),f(y,z,u)). 247 [] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,z,u)). 248 [] f(f(x,y,z),f(u,w,y),f(w,x,y))=f(y,f(u,w,z),f(w,x,y)). 249 [] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(y,u,z)). 250 [] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(u,z,y)). 251 [] f(f(x,u,z),f(u,y,z),f(y,z,w))=f(f(x,y,z),f(y,z,u),f(z,u,w)). 252 [] f(f(x,u,z),f(u,z,y),f(z,y,w))=f(f(x,y,z),f(y,u,z),f(u,z,w)). 253 [] f(f(x,u,z),f(u,z,y),f(y,z,w))=f(f(x,y,z),f(y,u,z),f(u,z,w)). 254 [] f(f(x,u,z),f(u,y,z),f(y,z,w))=f(f(x,y,z),f(y,z,u),f(u,z,w)). 255 [] f(f(x,u,z),f(u,y,z),f(y,z,w))=f(f(x,y,z),f(u,y,z),f(u,z,w)). 256 [] f(f(x,u,z),f(y,u,z),f(y,z,w))=f(f(x,y,z),f(y,u,z),f(u,z,w)). 257 [] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,y,z)). 258 [] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,z,y)). 259 [] f(f(x,y,z),f(u,z,y),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). 260 [] f(f(x,y,z),f(u,y,z),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). 261 [] f(f(x,y,z),f(u,w,y),f(u,y,z))=f(y,f(x,u,w),f(u,y,z)). 262 [] f(f(x,y,f(z,y,f(z,f(x,z,u),w))),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 263 [] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,u,z)). 264 [] f(x,f(y,z,u),f(z,w,f(y,u,z)))=f(z,f(x,y,w),f(y,z,u)). 265 [] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). 266 [] f(x,f(y,z,u),f(w,z,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). 267 [] f(f(x,y,f(z,y,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). 268 [] f(f(x,y,f(y,z,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). 269 [] f(f(x,y,z),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 270 [] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 271 [] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,w,f(x,z,u)))))=f(z,y,f(x,z,u)). 272 [] f(f(x,y,z),f(y,z,u),f(y,z,f(z,w,f(x,z,u))))=f(z,y,f(x,z,u)). 273 [] f(f(x,y,f(z,x,u)),f(z,w,x),f(w,x,u))=f(x,w,f(z,x,u)). 274 [] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(z,y,f(x,z,u)). 275 [] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(y,z,f(x,z,u)). 276 [] f(f(x,y,f(z,x,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 277 [] f(f(x,y,f(x,z,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 278 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 279 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 280 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(x,u,w5),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 281 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 282 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 283 [] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(x,u,w5),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 284 [] f(f(x,y,f(x,z,u)),f(x,z,w),f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w)))=f(w,x,f(z,x,u)). 285 [] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(z,x,u)). 286 [] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(x,z,u)). 287 [] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(x,w,f(x,z,u)). 288 [] f(f(x,f(y,z,u),f(u,x,f(u,y,z))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). 289 [] f(f(x,f(y,z,u),f(u,x,f(y,z,u))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). 290 [] f(f(x,y,f(z,u,y)),f(y,z,w),f(y,u,w))=f(y,w,f(y,z,u)). 291 [] f(f(x,y,f(z,u,y)),f(z,y,w),f(y,u,w))=f(y,w,f(y,z,u)). 292 [] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(y,z,u)). 293 [] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). 294 [] f(f(x,y,f(z,y,u)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). 295 [] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,u,y)). 296 [] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,y,u)). 297 [] f(f(x,f(x,y,z),f(u,y,z)),f(y,z,w),f(z,f(u,y,x),w))=f(z,w,f(y,z,f(u,y,x))). 298 [] f(f(x,y,z),f(y,z,u),f(z,f(w,y,x),u))=f(z,u,f(y,z,f(w,y,x))). 299 [] f(f(x,y,z),f(y,z,u),f(z,f(x,w,y),u))=f(z,u,f(y,z,f(w,y,x))). 300 [] f(f(x,y,z),f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(y,z,f(w,y,x))). 301 [] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(u,w,y))). 302 [] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(y,u,w))). 303 [] f(x,f(y,z,f(x,u,w)),f(y,f(x,z,f(x,u,w)),f(w,y,z)))=f(y,z,f(x,u,w)). 304 [] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(w,y,z))))=f(y,z,f(x,u,w)). 305 [] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(y,z,f(w,y,z)))))=f(y,z,f(x,u,w)). 306 [] f(x,f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(x,w,y)). 307 [] f(x,f(y,z,u),f(u,f(x,w,y),f(z,u,f(w5,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 308 [] f(x,f(y,z,u),f(u,f(x,y,f(w,w5,f(x,w,y))),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 309 [] f(x,f(y,z,u),f(u,f(y,f(w,w5,f(x,w,y)),x),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 310 [] f(x,f(y,z,u),f(x,f(z,u,f(w,z,f(x,w,y))),f(u,f(w,z,f(x,w,y)),f(y,z,u))))=f(z,u,f(x,w,y)). 311 [] f(x,f(y,z,u),f(x,f(u,f(w,z,f(x,w,y)),f(y,z,u)),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 312 [] f(x,f(y,z,u),f(x,f(f(y,z,u),u,f(w,z,f(x,w,y))),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 313 [] f(x,f(y,z,u),f(z,u,f(w,z,f(x,w,y))))=f(z,u,f(x,w,y)). 314 [] f(x,f(y,z,u),f(z,f(x,w,y),f(w,z,u)))=f(z,u,f(x,w,y)). 315 [] f(x,f(y,z,u),f(x,f(w,z,u),f(y,z,f(w,z,u))))=f(z,u,f(x,w,y)). 316 [] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(x,w,y)). 317 [] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(w,x,y)). 318 [] f(x,f(y,z,u),f(z,u,f(w,w5,f(w,z,u))))=f(z,u,f(w,x,y)). 319 [] f(f(x,y,f(x,z,u)),f(w,z,u),f(w5,z,u))=f(z,u,f(x,w,w5)). 320 [] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(y,z,f(x,u,w)). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=-2147483647) 1 [] f(x,x,y)=x. given clause #2: (wt=-2147483647) 2 [] f(x,y,x)=x. given clause #3: (wt=-2147483647) 3 [] f(y,x,x)=x. given clause #4: (wt=-2147483647) 4 [] f(x,y,z)=f(y,x,z). given clause #5: (wt=-2147483647) 5 [] f(x,y,z)=f(x,z,y). +++ bsub adjust, cl 9, new wt -512 +++ bsub adjust, cl 10, new wt -512 given clause #6: (wt=-2147483647) 6 [] f(x,y,z)=f(z,y,x). given clause #7: (wt=-2147483647) 7 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). +++ bsub adjust, cl 11, new wt -512 +++ bsub adjust, cl 12, new wt -512 +++ bsub adjust, cl 13, new wt -512 +++ bsub adjust, cl 14, new wt -512 +++ bsub adjust, cl 15, new wt -512 +++ bsub adjust, cl 16, new wt -512 +++ bsub adjust, cl 17, new wt -512 +++ bsub adjust, cl 18, new wt -512 given clause #8: (wt=-1009) 322 [para_into,5.1.1,4.1.2,flip.1] f(x,y,z)=f(z,x,y). +++ bsub adjust, cl 19, new wt -512 given clause #9: (wt=-1009) 323 [para_into,5.1.2,4.1.2,flip.1] f(x,y,z)=f(y,z,x). +++ bsub adjust, cl 20, new wt -512 given clause #10: (wt=-1003) 327 [para_into,7.1.1.1,2.1.1,flip.1] f(x,y,f(x,y,z))=f(x,y,z). +++ bsub adjust, cl 21, new wt -512 +++ bsub adjust, cl 27, new wt -512 +++ bsub adjust, cl 23, new wt -512 +++ bsub adjust, cl 24, new wt -512 +++ bsub adjust, cl 25, new wt -512 +++ bsub adjust, cl 26, new wt -512 given clause #11: (wt=-1009) 337 [para_into,327.1.1.3,1.1.1,flip.1] f(x,x,y)=f(x,x,x). +++ bsub adjust, cl 28, new wt -512 given clause #12: (wt=-1009) 347 [para_into,337.1.2,337.1.2,flip.1] f(x,x,y)=f(x,x,z). +++ bsub adjust, cl 27, new wt -256 +++ bsub adjust, cl 27, new wt -128 given clause #13: (wt=-1003) 331 [para_into,7.1.2.3,2.1.1] f(f(x,y,z),y,z)=f(x,y,z). +++ bsub adjust, cl 29, new wt -512 given clause #14: (wt=-1003) 336 [para_into,327.1.1.3,323.1.2] f(x,y,f(z,x,y))=f(x,y,z). given clause #15: (wt=-1003) 338 [para_into,327.1.1,6.1.2] f(f(x,y,z),y,x)=f(x,y,z). +++ bsub adjust, cl 30, new wt -512 given clause #16: (wt=-1003) 339 [para_into,327.1.1,5.1.2] f(x,f(x,y,z),y)=f(x,y,z). given clause #17: (wt=-1003) 340 [para_into,327.1.1,4.1.2] f(x,y,f(y,x,z))=f(y,x,z). +++ bsub adjust, cl 31, new wt -512 given clause #18: (wt=-1003) 341 [para_into,327.1.2,4.1.2] f(x,y,f(x,y,z))=f(y,x,z). given clause #19: (wt=-1003) 354 [para_into,331.1.1,323.1.1] f(x,y,f(z,x,y))=f(z,x,y). given clause #20: (wt=-1003) 358 [para_into,338.1.2,323.1.2] f(f(x,y,z),y,x)=f(z,x,y). +++ bsub adjust, cl 32, new wt -512 given clause #21: (wt=-997) 324 [para_into,7.1.1.1,6.1.2] f(f(x,y,z),y,u)=f(z,y,f(x,y,u)). +++ bsub adjust, cl 34, new wt -512 +++ bsub adjust, cl 35, new wt -512 +++ bsub adjust, cl 33, new wt -512 given clause #22: (wt=-997) 325 [para_into,7.1.1.1,5.1.2] f(f(x,y,z),z,u)=f(x,z,f(y,z,u)). +++ bsub adjust, cl 36, new wt -512 +++ bsub adjust, cl 37, new wt -512 +++ bsub adjust, cl 38, new wt -512 given clause #23: (wt=-997) 326 [para_into,7.1.1.1,4.1.2] f(f(x,y,z),x,u)=f(y,x,f(z,x,u)). +++ bsub adjust, cl 40, new wt -512 +++ bsub adjust, cl 39, new wt -512 given clause #24: (wt=-997) 328 [para_into,7.1.1,6.1.2,flip.1] f(x,y,f(z,y,u))=f(u,y,f(x,y,z)). +++ bsub adjust, cl 42, new wt -512 given clause #25: (wt=-997) 329 [para_into,7.1.1,4.1.2,flip.1] f(x,y,f(z,y,u))=f(y,f(x,y,z),u). +++ bsub adjust, cl 44, new wt -512 given clause #26: (wt=-997) 333 [para_from,7.1.1,4.1.1,flip.1] f(x,f(y,x,z),u)=f(y,x,f(z,x,u)). +++ bsub adjust, cl 43, new wt -512 given clause #27: (wt=-997) 334 [para_into,322.1.2,7.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(x,y,z)). +++ bsub adjust, cl 47, new wt -512 +++ bsub adjust, cl 47, new wt -256 +++ bsub adjust, cl 49, new wt -512 +++ bsub adjust, cl 45, new wt -512 +++ bsub adjust, cl 45, new wt -256 given clause #28: (wt=-997) 335 [para_into,323.1.1,7.1.1,flip.1] f(x,y,f(z,x,u))=f(z,x,f(u,x,y)). +++ bsub adjust, cl 46, new wt -512 +++ bsub adjust, cl 48, new wt -512 +++ bsub adjust, cl 50, new wt -512 given clause #29: (wt=-997) 362 [para_into,340.1.1,340.1.2] f(x,y,f(y,x,f(x,y,z)))=f(x,y,z). given clause #30: (wt=-997) 366 [para_into,324.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(z,y,x)). +++ bsub adjust, cl 51, new wt -512 +++ bsub adjust, cl 52, new wt -512 given clause #31: (wt=-997) 367 [para_into,324.1.1,7.1.1,flip.1] f(x,y,f(z,y,u))=f(z,y,f(x,y,u)). +++ bsub adjust, cl 53, new wt -512 given clause #32: (wt=-997) 369 [para_from,324.1.1,323.1.1,flip.1] f(x,y,f(z,x,u))=f(u,x,f(z,x,y)). given clause #33: (wt=-997) 370 [para_into,325.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(x,z,y)). +++ bsub adjust, cl 55, new wt -512 given clause #34: (wt=-997) 371 [para_into,325.1.1,6.1.2,flip.1] f(x,y,f(z,y,u))=f(u,y,f(x,z,y)). +++ bsub adjust, cl 56, new wt -512 +++ bsub adjust, cl 41, new wt -512 given clause #35: (wt=-997) 373 [para_from,325.1.1,323.1.1,flip.1] f(x,y,f(z,u,x))=f(z,x,f(u,x,y)). +++ bsub adjust, cl 54, new wt -512 given clause #36: (wt=-997) 374 [para_into,326.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(y,x,z)). +++ bsub adjust, cl 58, new wt -512 given clause #37: (wt=-997) 375 [para_from,326.1.1,323.1.1,flip.1] f(x,y,f(x,z,u))=f(z,x,f(u,x,y)). +++ bsub adjust, cl 57, new wt -512 given clause #38: (wt=-997) 377 [para_into,328.1.2.3,323.1.2,flip.1] f(x,y,f(z,u,y))=f(u,y,f(z,y,x)). +++ bsub adjust, cl 59, new wt -512 given clause #39: (wt=-997) 378 [para_into,329.1.1.3,4.1.2,flip.1] f(x,f(y,x,z),u)=f(y,x,f(x,z,u)). +++ bsub adjust, cl 61, new wt -512 +++ bsub adjust, cl 63, new wt -512 given clause #40: (wt=-997) 380 [para_into,333.1.2.3,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(x,y,z),u). +++ bsub adjust, cl 60, new wt -512 +++ bsub adjust, cl 62, new wt -512 given clause #41: (wt=-997) 383 [para_into,334.1.1.3,4.1.2,flip.1] f(x,y,f(z,x,u))=f(z,x,f(x,u,y)). +++ bsub adjust, cl 69, new wt -512 given clause #42: (wt=-997) 387 [para_into,335.1.1.3,323.1.2,flip.1] f(x,y,f(z,y,u))=f(y,u,f(z,x,y)). +++ bsub adjust, cl 41, new wt -256 given clause #43: (wt=-997) 388 [para_into,335.1.2.3,323.1.1,flip.1] f(x,y,f(y,z,u))=f(y,z,f(x,y,u)). +++ bsub adjust, cl 67, new wt -512 +++ bsub adjust, cl 72, new wt -512 +++ bsub adjust, cl 65, new wt -512 +++ bsub adjust, cl 64, new wt -512 +++ bsub adjust, cl 66, new wt -512 +++ bsub adjust, cl 68, new wt -512 given clause #44: (wt=-997) 389 [para_into,335.1.2.3,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,u,f(x,y,z)). +++ bsub adjust, cl 70, new wt -512 +++ bsub adjust, cl 72, new wt -256 given clause #45: (wt=-997) 390 [para_into,366.1.1,323.1.1] f(x,f(y,x,z),u)=f(x,z,f(y,x,u)). +++ bsub adjust, cl 73, new wt -512 given clause #46: (wt=-997) 391 [para_into,366.1.1,4.1.2,flip.1] f(x,y,f(z,x,u))=f(x,u,f(z,x,y)). +++ bsub adjust, cl 75, new wt -512 +++ bsub adjust, cl 74, new wt -512 given clause #47: (wt=-997) 394 [para_into,370.1.1.3,5.1.2,flip.1] f(x,y,f(z,u,x))=f(z,x,f(u,y,x)). given clause #48: (wt=-997) 396 [para_into,371.1.1.3,323.1.2,flip.1] f(x,y,f(z,u,y))=f(z,y,f(x,u,y)). +++ bsub adjust, cl 77, new wt -512 +++ bsub adjust, cl 76, new wt -512 given clause #49: (wt=-997) 399 [para_into,373.1.2.3,5.1.2,flip.1] f(x,y,f(z,u,y))=f(y,u,f(x,z,y)). given clause #50: (wt=-997) 400 [para_into,374.1.1.3,4.1.2,flip.1] f(x,y,f(x,z,u))=f(z,x,f(x,u,y)). +++ bsub adjust, cl 79, new wt -512 +++ bsub adjust, cl 78, new wt -512 given clause #51: (wt=-997) 401 [para_into,375.1.2.3,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,u,f(y,x,z)). given clause #52: (wt=-997) 402 [para_into,377.1.2.3,5.1.2,flip.1] f(x,y,f(z,u,y))=f(u,y,f(z,x,y)). given clause #53: (wt=-997) 403 [para_into,378.1.1.2,5.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(x,z,y),u). +++ bsub adjust, cl 80, new wt -512 given clause #54: (wt=-997) 404 [para_into,378.1.1.2,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(y,x,z),u). +++ bsub adjust, cl 81, new wt -512 given clause #55: (wt=-997) 405 [para_into,380.1.2.2,5.1.2,flip.1] f(x,f(y,z,x),u)=f(y,x,f(x,z,u)). given clause #56: (wt=-997) 406 [para_into,380.1.2.2,4.1.2,flip.1] f(x,f(x,y,z),u)=f(y,x,f(x,z,u)). given clause #57: (wt=-997) 409 [para_into,388.1.1,4.1.2,flip.1] f(x,y,f(z,x,u))=f(x,z,f(x,y,u)). given clause #58: (wt=-997) 414 [para_from,388.1.1,4.1.1,flip.1] f(x,y,f(x,z,u))=f(x,z,f(y,x,u)). given clause #59: (wt=-997) 417 [para_into,390.1.1.2,4.1.2] f(x,f(x,y,z),u)=f(x,z,f(y,x,u)). +++ bsub adjust, cl 103, new wt -512 +++ bsub adjust, cl 82, new wt -512 given clause #60: (wt=-997) 419 [para_into,391.1.1.3,4.1.2,flip.1] f(x,y,f(z,x,u))=f(x,u,f(x,z,y)). +++ bsub adjust, cl 83, new wt -512 +++ bsub adjust, cl 85, new wt -512 +++ bsub adjust, cl 84, new wt -512 given clause #61: (wt=-997) 420 [para_into,391.1.2.3,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,u,f(z,x,y)). given clause #62: (wt=-997) 423 [para_into,400.1.2,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,u,f(x,y,z)). +++ bsub adjust, cl 86, new wt -512 +++ bsub adjust, cl 87, new wt -512 given clause #63: (wt=-997) 424 [para_from,400.1.2,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,z,f(x,u,y)). +++ bsub adjust, cl 88, new wt -512 given clause #64: (wt=-997) 427 [para_into,404.1.1,4.1.2,flip.1] f(x,f(x,y,z),u)=f(x,y,f(x,z,u)). +++ bsub adjust, cl 89, new wt -512 +++ bsub adjust, cl 99, new wt -512 +++ bsub adjust, cl 90, new wt -512 +++ bsub adjust, cl 91, new wt -512 given clause #65: (wt=-997) 430 [para_into,419.1.1.3,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,u,f(x,z,y)). given clause #66: (wt=-993) 365 [para_into,358.1.1,336.1.2] f(f(x,y,z),y,f(x,f(x,y,z),y))=f(z,x,y). given clause #67: (wt=-993) 425 [para_into,403.1.1.3,340.1.1,flip.1] f(x,f(y,z,x),f(z,x,u))=f(y,x,f(z,x,u)). +++ bsub adjust, cl 92, new wt -512 given clause #68: (wt=-991) 413 [para_from,388.1.1,327.1.1.3] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). +++ bsub adjust, cl 93, new wt -512 given clause #69: (wt=-993) 441 [para_into,413.1.1,380.1.1] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)). given clause #70: (wt=-991) 440 [para_into,425.1.1,389.1.2] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)). given clause #71: (wt=-987) 407 [para_into,383.1.2.3,383.1.2,flip.1] f(x,y,f(z,u,f(y,z,w)))=f(y,f(z,w,u),f(x,y,z)). +++ bsub adjust, cl 97, new wt -512 given clause #72: (wt=-987) 411 [para_from,388.1.1,378.1.2.3,flip.1] f(x,y,f(z,u,f(y,z,w)))=f(y,f(x,y,z),f(z,u,w)). +++ bsub adjust, cl 95, new wt -512 given clause #73: (wt=-987) 412 [para_from,388.1.1,380.1.1.3,flip.1] f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,u,f(x,z,w))). +++ bsub adjust, cl 94, new wt -512 given clause #74: (wt=-987) 415 [para_into,389.1.1.3,389.1.1,flip.1] f(x,f(y,z,u),f(w,x,y))=f(w,x,f(y,u,f(x,y,z))). +++ bsub adjust, cl 97, new wt -256 given clause #75: (wt=-987) 428 [para_into,417.1.2.3,414.1.1] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,u,f(x,y,w))). +++ bsub adjust, cl 98, new wt -512 given clause #76: (wt=-987) 429 [para_into,417.1.2.3,391.1.2] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(u,y,x))). +++ bsub adjust, cl 98, new wt -256 given clause #77: (wt=-987) 431 [para_from,419.1.2,329.1.1.3,flip.1] f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,w,f(u,z,x))). given clause #78: (wt=-987) 432 [para_from,419.1.2,333.1.2.3,flip.1] f(x,y,f(z,u,f(w,z,y)))=f(y,f(x,y,z),f(z,w,u)). given clause #79: (wt=-987) 433 [para_into,423.1.1.3,423.1.2,flip.1] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). +++ bsub adjust, cl 99, new wt -256 given clause #80: (wt=-987) 436 [para_into,427.1.2.3,424.1.2] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). +++ bsub adjust, cl 100, new wt -512 given clause #81: (wt=-987) 438 [para_into,427.1.2.3,388.1.1] f(x,f(x,y,z),f(z,u,w))=f(x,y,f(z,u,f(x,z,w))). given clause #82: (wt=-987) 439 [para_into,427.1.2.3,367.1.2] f(x,f(x,y,z),f(u,z,w))=f(x,y,f(u,z,f(x,z,w))). given clause #83: (wt=-987) 443 [para_into,411.1.2.2,323.1.1,flip.1] f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(x,y,w))). +++ bsub adjust, cl 102, new wt -512 +++ bsub adjust, cl 103, new wt -256 given clause #84: (wt=-987) 444 [para_into,412.1.1.2,323.1.1,flip.1] f(x,y,f(z,u,f(y,z,w)))=f(y,f(y,z,x),f(z,u,w)). +++ bsub adjust, cl 101, new wt -512 given clause #85: (wt=-987) 450 [para_into,443.1.2.3.3,323.1.1,flip.1] f(x,y,f(z,u,f(z,w,y)))=f(y,f(y,z,x),f(z,u,w)). given clause #86: (wt=-987) 452 [para_into,444.1.1.3.3,323.1.1,flip.1] f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(y,w,x))). given clause #87: (wt=-985) 434 [para_into,423.1.2.3,388.1.1,flip.1] f(x,y,f(z,u,f(x,z,w)))=f(x,z,f(x,f(z,u,w),y)). given clause #88: (wt=-985) 435 [para_into,424.1.1.3,388.1.1,flip.1] f(x,y,f(x,f(y,z,u),w))=f(x,w,f(y,z,f(x,y,u))). given clause #89: (wt=-985) 449 [para_into,436.1.1,433.1.1,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,w,f(x,y,f(x,u,z))). +++ bsub adjust, cl 104, new wt -512 +++ bsub adjust, cl 105, new wt -512 given clause #90: (wt=-983) 393 [para_into,367.1.1.3,339.1.1,flip.1] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(u,f(x,y,z),f(x,y,z)). +++ bsub adjust, cl 106, new wt -512 given clause #91: (wt=-993) 455 [para_into,393.1.2,3.1.1] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(x,y,z). +++ bsub adjust, cl 107, new wt -512 given clause #92: (wt=-993) 456 [para_into,455.1.1.3,323.1.2] f(x,f(x,y,z),f(y,u,f(x,y,z)))=f(x,y,z). +++ bsub adjust, cl 108, new wt -512 given clause #93: (wt=-993) 457 [para_into,456.1.1,438.1.2] f(x,f(x,f(x,y,z),y),f(y,u,z))=f(x,y,z). +++ bsub adjust, cl 109, new wt -512 given clause #94: (wt=-999) 458 [para_into,457.1.1.2,339.1.1] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). +++ bsub adjust, cl 107, new wt -256 +++ bsub adjust, cl 107, new wt -128 +++ bsub adjust, cl 110, new wt -512 +++ bsub adjust, cl 111, new wt -512 +++ bsub adjust, cl 112, new wt -512 given clause #95: (wt=-999) 461 [para_into,458.1.1.3,339.1.1] f(x,f(x,y,z),f(y,z,u))=f(x,y,z). +++ bsub adjust, cl 113, new wt -512 given clause #96: (wt=-999) 462 [para_into,458.1.1.3,4.1.2] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). +++ bsub adjust, cl 114, new wt -512 +++ bsub adjust, cl 115, new wt -512 +++ bsub adjust, cl 116, new wt -512 given clause #97: (wt=-999) 463 [para_into,458.1.2,323.1.1] f(x,f(x,y,z),f(y,u,z))=f(y,z,x). +++ bsub adjust, cl 117, new wt -512 +++ bsub adjust, cl 118, new wt -512 +++ bsub adjust, cl 118, new wt -256 +++ bsub adjust, cl 119, new wt -512 given clause #98: (wt=-999) 466 [para_into,462.1.1,5.1.2] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). +++ bsub adjust, cl 120, new wt -512 +++ bsub adjust, cl 120, new wt -256 +++ bsub adjust, cl 121, new wt -512 +++ bsub adjust, cl 122, new wt -512 given clause #99: (wt=-999) 468 [para_into,463.1.1.2,323.1.2] f(x,f(y,x,z),f(z,u,y))=f(z,y,x). +++ bsub adjust, cl 123, new wt -512 +++ bsub adjust, cl 123, new wt -256 given clause #100: (wt=-999) 475 [para_into,466.1.2,323.1.1] f(x,f(y,z,u),f(x,z,u))=f(z,u,x). +++ bsub adjust, cl 124, new wt -512 given clause #101: (wt=-999) 478 [para_into,475.1.1.3,323.1.1] f(x,f(y,z,u),f(z,u,x))=f(z,u,x). +++ bsub adjust, cl 125, new wt -512 +++ bsub adjust, cl 126, new wt -512 given clause #102: (wt=-999) 479 [para_into,478.1.1.2,323.1.1] f(x,f(y,z,u),f(y,z,x))=f(y,z,x). +++ bsub adjust, cl 127, new wt -512 +++ bsub adjust, cl 128, new wt -512 +++ bsub adjust, cl 187, new wt -512 +++ bsub adjust, cl 129, new wt -512 given clause #103: (wt=-997) 464 [para_into,461.1.1,439.1.1] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). +++ bsub adjust, cl 130, new wt -512 +++ bsub adjust, cl 130, new wt -256 +++ bsub adjust, cl 131, new wt -512 given clause #104: (wt=-999) 487 [para_into,464.1.1,389.1.1] f(x,f(y,z,u),f(y,x,z))=f(y,x,z). +++ bsub adjust, cl 132, new wt -512 +++ bsub adjust, cl 132, new wt -256 +++ bsub adjust, cl 133, new wt -512 +++ bsub adjust, cl 134, new wt -512 given clause #105: (wt=-997) 465 [para_into,462.1.1,427.1.1] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). +++ bsub adjust, cl 135, new wt -512 +++ bsub adjust, cl 135, new wt -256 given clause #106: (wt=-997) 474 [para_into,466.1.1,430.1.2] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). +++ bsub adjust, cl 136, new wt -512 given clause #107: (wt=-997) 480 [para_into,478.1.1,387.1.2] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). given clause #108: (wt=-997) 483 [para_into,479.1.1,373.1.1] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). +++ bsub adjust, cl 188, new wt -512 +++ bsub adjust, cl 190, new wt -512 given clause #109: (wt=-997) 495 [para_into,483.1.1.3,391.1.2] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). given clause #110: (wt=-993) 482 [para_into,479.1.1.2,388.1.2] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). given clause #111: (wt=-990) 484 [para_from,479.1.1,387.1.1.3,flip.1] 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)). given clause #112: (wt=-990) 490 [para_from,487.1.1,394.1.2.3] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(w,f(x,y,z),f(x,y,z)). +++ bsub adjust, cl 137, new wt -512 given clause #113: (wt=-1000) 497 [para_into,490.1.2,3.1.1] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(x,y,z). +++ bsub adjust, cl 138, new wt -512 given clause #114: (wt=-1000) 498 [para_into,497.1.1,323.1.2] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u). +++ bsub adjust, cl 139, new wt -512 given clause #115: (wt=-1000) 499 [para_into,498.1.1.2,4.1.2] f(f(x,y,f(z,y,u)),f(y,z,u),f(z,u,w))=f(z,y,u). +++ bsub adjust, cl 140, new wt -512 given clause #116: (wt=-1000) 500 [para_into,499.1.1.1.3,4.1.2] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(z,y,u). +++ bsub adjust, cl 141, new wt -512 given clause #117: (wt=-1000) 501 [para_into,500.1.2,4.1.2] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). +++ bsub adjust, cl 142, new wt -512 given clause #118: (wt=-1000) 502 [para_into,501.1.1.1,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). given clause #119: (wt=-987) 467 [para_from,462.1.1,458.1.1.3] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)). given clause #120: (wt=-987) 471 [para_from,463.1.1,458.1.1.3] f(x,f(x,y,f(z,u,w)),f(z,w,y))=f(x,y,f(z,u,w)). +++ bsub adjust, cl 143, new wt -512 given clause #121: (wt=-987) 481 [para_into,479.1.1.2,479.1.1] f(x,f(y,z,u),f(u,f(y,z,w),x))=f(u,f(y,z,w),x). +++ bsub adjust, cl 144, new wt -512 given clause #122: (wt=-996) 504 [para_into,481.1.1,484.1.1] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). +++ bsub adjust, cl 152, new wt -512 +++ bsub adjust, cl 145, new wt -512 given clause #123: (wt=-996) 506 [para_into,504.1.1,323.1.2] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). +++ bsub adjust, cl 152, new wt -256 given clause #124: (wt=-987) 491 [para_from,487.1.1,461.1.1.3] f(x,f(x,y,f(z,u,w)),f(z,y,u))=f(x,y,f(z,u,w)). given clause #125: (wt=-987) 496 [para_from,483.1.1,427.1.2.3] f(x,f(x,y,z),f(u,z,f(x,u,w)))=f(x,y,f(x,u,z)). given clause #126: (wt=-987) 503 [para_into,471.1.1,5.1.2] f(x,f(y,z,u),f(x,u,f(y,w,z)))=f(x,u,f(y,w,z)). +++ bsub adjust, cl 147, new wt -512 given clause #127: (wt=-987) 508 [para_into,503.1.1.2,323.1.1] f(x,f(y,z,u),f(x,z,f(u,w,y)))=f(x,z,f(u,w,y)). given clause #128: (wt=-981) 494 [para_into,474.1.1.3.3,430.1.2] f(x,f(y,z,u),f(x,w,f(y,u,f(y,z,w))))=f(x,w,f(y,z,u)). given clause #129: (wt=-975) 421 [para_into,396.1.1,380.1.2,flip.1] 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)))). +++ bsub adjust, cl 148, new wt -512 +++ bsub adjust, cl 149, new wt -512 given clause #130: (wt=-975) 422 [para_into,396.1.2,380.1.2,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 #131: (wt=-955) 509 [para_from,421.1.1,367.1.1.3,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 #132: (wt=-955) 510 [para_from,421.1.1,367.1.2.3,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(x,f(y,z,u),f(z,w5,f(y,z,u)))). given clause #133: (wt=-953) 453 [para_from,449.1.2,402.1.1.3,flip.1] f(x,f(y,z,f(y,u,w)),f(y,w5,f(y,z,f(y,u,w))))=f(w5,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,x)))). given clause #134: (wt=-953) 454 [para_from,449.1.2,402.1.2.3,flip.1] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(w5,f(y,z,f(y,u,w)),f(y,x,f(y,z,f(y,u,w)))). given clause #135: (wt=-485) 382 [para_into,334.1.1.3,322.1.2,flip.1] f(x,y,f(z,x,u))=f(z,x,f(x,y,u)). +++ bsub adjust, cl 96, new wt -512 +++ bsub adjust, cl 96, new wt -256 +++ bsub adjust, cl 71, new wt -512 +++ bsub adjust, cl 71, new wt -256 given clause #136: (wt=-485) 386 [para_into,334.1.2.3,322.1.1,flip.1] f(x,y,f(z,u,x))=f(u,x,f(z,x,y)). given clause #137: (wt=-485) 408 [para_from,387.1.2,4.1.2,flip.1] f(x,y,f(z,y,u))=f(u,y,f(z,x,y)). given clause #138: (wt=-485) 470 [para_into,463.1.1,450.1.2] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). given clause #139: (wt=-485) 477 [para_into,468.1.1,431.1.1] f(x,y,f(z,x,f(u,z,y)))=f(z,x,y). given clause #140: (wt=-485) 493 [para_into,465.1.1.3.3,6.1.2] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). +++ bsub adjust, cl 150, new wt -512 given clause #141: (wt=-987) 515 [para_into,493.1.1.3.3,479.1.1] f(x,f(y,z,u),f(x,w,f(y,z,w)))=f(x,f(y,z,u),w). given clause #142: (wt=-481) 473 [para_into,466.1.1.2,324.1.1] f(x,f(y,z,f(u,z,w)),f(x,z,w))=f(x,z,w). +++ bsub adjust, cl 151, new wt -512 given clause #143: (wt=-987) 516 [para_into,473.1.1.2,480.1.1] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)). given clause #144: (wt=-479) 486 [para_into,464.1.1.3.3,388.1.1] f(x,y,f(y,z,f(z,u,f(x,z,w))))=f(x,y,z). given clause #145: (wt=-477) 507 [para_into,506.1.1,504.1.1,flip.1] f(x,f(y,z,u),f(y,z,w))=f(w,f(y,z,x),f(y,z,u)). +++ bsub adjust, cl 152, new wt -128 +++ bsub adjust, cl 152, new wt -64 +++ bsub adjust, cl 153, new wt -512 given clause #146: (wt=-996) 519 [para_into,507.1.2.2,354.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). +++ bsub adjust, cl 154, new wt -512 given clause #147: (wt=-996) 520 [para_into,519.1.1,5.1.2] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). +++ bsub adjust, cl 155, new wt -512 +++ bsub adjust, cl 156, new wt -512 given clause #148: (wt=-996) 521 [para_into,520.1.1.2,323.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). +++ bsub adjust, cl 157, new wt -512 given clause #149: (wt=-996) 523 [para_into,521.1.1,4.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). +++ bsub adjust, cl 158, new wt -512 given clause #150: (wt=-996) 524 [para_into,523.1.1.2,323.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). +++ bsub adjust, cl 159, new wt -512 +++ bsub adjust, cl 160, new wt -512 given clause #151: (wt=-989) 522 [para_into,520.1.1,519.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(y,z,u),f(z,u,x)). +++ bsub adjust, cl 162, new wt -512 +++ bsub adjust, cl 161, new wt -512 given clause #152: (wt=-989) 525 [para_into,524.1.1,519.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(z,u,y)). +++ bsub adjust, cl 163, new wt -512 given clause #153: (wt=-989) 526 [para_from,524.1.1,519.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(y,f(w,z,u),f(z,u,x)). +++ bsub adjust, cl 164, new wt -512 given clause #154: (wt=-989) 527 [para_into,522.1.1.2,323.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(z,u,x)). +++ bsub adjust, cl 166, new wt -512 given clause #155: (wt=-989) 528 [para_into,522.1.2.2,323.1.2,flip.1] f(x,f(y,z,u),f(u,y,w))=f(w,f(z,u,y),f(u,y,x)). +++ bsub adjust, cl 165, new wt -512 given clause #156: (wt=-989) 529 [para_into,525.1.2.3,323.1.2,flip.1] f(x,f(y,z,u),f(w,z,u))=f(y,f(w,z,u),f(z,u,x)). given clause #157: (wt=-989) 530 [para_into,526.1.1.3,323.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(y,z,u)). given clause #158: (wt=-989) 531 [para_into,527.1.2.3,4.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(z,u,y),f(u,y,x)). +++ bsub adjust, cl 168, new wt -512 given clause #159: (wt=-989) 532 [para_into,528.1.1.3,4.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(u,z,x)). +++ bsub adjust, cl 167, new wt -512 given clause #160: (wt=-989) 533 [para_into,531.1.2.2,323.1.2,flip.1] f(x,f(y,z,u),f(u,y,w))=f(w,f(y,z,u),f(y,u,x)). +++ bsub adjust, cl 170, new wt -512 given clause #161: (wt=-989) 534 [para_into,532.1.1.2,323.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(y,z,u),f(u,y,x)). +++ bsub adjust, cl 169, new wt -512 given clause #162: (wt=-989) 535 [para_into,533.1.1.3,6.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(y,z,u),f(x,y,u)). +++ bsub adjust, cl 171, new wt -512 given clause #163: (wt=-989) 536 [para_into,534.1.2.3,6.1.2,flip.1] f(x,f(y,z,u),f(w,y,u))=f(w,f(y,z,u),f(y,u,x)). given clause #164: (wt=-989) 537 [para_from,535.1.2,5.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(x,y,u),f(y,z,u)). given clause #165: (wt=-475) 447 [para_into,429.1.2.3.3,6.1.2] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(x,y,u))). +++ bsub adjust, cl 173, new wt -512 given clause #166: (wt=-987) 538 [para_into,447.1.1,491.1.1,flip.1] f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,w,f(y,z,u)). +++ bsub adjust, cl 174, new wt -512 +++ bsub adjust, cl 172, new wt -512 given clause #167: (wt=-987) 539 [para_into,538.1.1,5.1.2] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)). +++ bsub adjust, cl 175, new wt -512 given clause #168: (wt=-977) 540 [para_into,538.1.2,491.1.2] f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,f(x,w,f(y,z,u)),f(y,w,z)). given clause #169: (wt=-973) 541 [para_into,539.1.1.3,466.1.1] f(x,f(y,f(z,u,w),f(x,y,w5)),f(w5,u,w))=f(x,y,f(w5,f(z,u,w),f(w5,u,w))). +++ bsub adjust, cl 176, new wt -512 given clause #170: (wt=-973) 542 [para_into,541.1.1.2,5.1.2] f(x,f(y,f(x,y,z),f(u,w,w5)),f(z,w,w5))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). +++ bsub adjust, cl 177, new wt -512 given clause #171: (wt=-973) 543 [para_into,542.1.1.3,323.1.1] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). +++ bsub adjust, cl 178, new wt -512 given clause #172: (wt=-983) 544 [para_into,543.1.2.3,475.1.1] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(w,w5,z)). +++ bsub adjust, cl 177, new wt -256 +++ bsub adjust, cl 179, new wt -512 given clause #173: (wt=-975) 546 [para_from,544.1.1,440.1.1.3,flip.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(x,z,y))). +++ bsub adjust, cl 180, new wt -512 given clause #174: (wt=-975) 547 [para_into,546.1.2.3.3,323.1.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(z,y,x))). +++ bsub adjust, cl 181, new wt -512 given clause #175: (wt=-981) 548 [para_into,547.1.2,413.1.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,x)). +++ bsub adjust, cl 182, new wt -512 given clause #176: (wt=-985) 549 [para_into,548.1.1.3.3.2,2.1.1] f(x,y,f(z,y,f(u,y,f(w,x,z))))=f(z,y,f(y,u,x)). +++ bsub adjust, cl 183, new wt -512 +++ bsub adjust, cl 183, new wt -256 given clause #177: (wt=-475) 448 [para_into,433.1.1,5.1.2] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,u,f(x,w,z))). +++ bsub adjust, cl 89, new wt -256 +++ bsub adjust, cl 89, new wt -128 +++ bsub adjust, cl 184, new wt -512 given clause #178: (wt=-991) 554 [para_from,448.1.1,470.1.1.3] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). +++ bsub adjust, cl 185, new wt -512 given clause #179: (wt=-991) 555 [para_into,554.1.1.3,4.1.2] f(x,y,f(z,u,f(u,x,f(u,y,w))))=f(u,x,y). given clause #180: (wt=-475) 451 [para_into,443.1.2,4.1.2] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,u,f(x,y,w))). +++ bsub adjust, cl 186, new wt -512 +++ bsub adjust, cl 187, new wt -256 +++ bsub adjust, cl 188, new wt -256 +++ bsub adjust, cl 191, new wt -512 given clause #181: (wt=-987) 556 [para_into,451.1.1,467.1.1,flip.1] f(x,f(y,z,u),f(w,z,f(x,w,u)))=f(x,w,f(y,z,u)). +++ bsub adjust, cl 189, new wt -512 given clause #182: (wt=-987) 559 [para_into,451.1.2,496.1.1] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). given clause #183: (wt=-987) 560 [para_into,556.1.1,435.1.2] f(x,y,f(x,f(y,z,u),f(w,z,u)))=f(x,y,f(w,z,u)). given clause #184: (wt=-485) 557 [para_into,451.1.1,461.1.1,flip.1] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). +++ bsub adjust, cl 121, new wt -256 +++ bsub adjust, cl 190, new wt -256 given clause #185: (wt=-485) 558 [para_into,451.1.1,458.1.1,flip.1] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). given clause #186: (wt=-485) 561 [para_into,557.1.1.3,335.1.1] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). given clause #187: (wt=-475) 489 [para_into,487.1.1.2,475.1.1] f(x,f(y,z,u),f(u,x,f(w,y,z)))=f(u,x,f(w,y,z)). given clause #188: (wt=-475) 562 [para_from,557.1.1,427.1.2.3] f(x,f(x,y,z),f(u,z,f(x,u,w)))=f(x,y,f(x,u,z)). +++ bsub adjust, cl 191, new wt -256 given clause #189: (wt=-475) 563 [para_into,562.1.1,451.1.2] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). given clause #190: (wt=-473) 416 [para_from,389.1.1,388.1.2.3,flip.1] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,y,f(x,w,z))). +++ bsub adjust, cl 193, new wt -512 +++ bsub adjust, cl 194, new wt -512 +++ bsub adjust, cl 192, new wt -512 given clause #191: (wt=-991) 565 [para_into,416.1.2.3,327.1.1] f(x,y,f(x,z,f(u,x,y)))=f(u,x,f(x,y,z)). +++ bsub adjust, cl 195, new wt -512 given clause #192: (wt=-991) 567 [para_into,565.1.1.3.3,323.1.1] f(x,y,f(x,z,f(x,y,u)))=f(u,x,f(x,y,z)). +++ bsub adjust, cl 196, new wt -512 given clause #193: (wt=-991) 568 [para_into,567.1.1.3,5.1.2] f(x,y,f(x,f(x,y,z),u))=f(z,x,f(x,y,u)). +++ bsub adjust, cl 197, new wt -512 given clause #194: (wt=-991) 569 [para_into,568.1.2,4.1.2] f(x,y,f(x,f(x,y,z),u))=f(x,z,f(x,y,u)). given clause #195: (wt=-987) 564 [para_into,416.1.1,424.1.2,flip.1] f(x,y,f(y,z,f(y,u,w)))=f(y,f(x,y,u),f(y,z,w)). +++ bsub adjust, cl 198, new wt -512 given clause #196: (wt=-994) 570 [para_from,564.1.2,502.1.1.1] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w). +++ bsub adjust, cl 199, new wt -512 given clause #197: (wt=-994) 571 [para_into,570.1.2,5.1.2] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,w,z). +++ bsub adjust, cl 200, new wt -512 +++ bsub adjust, cl 201, new wt -512 given clause #198: (wt=-991) 573 [para_into,571.1.1,478.1.1] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,y,x). +++ bsub adjust, cl 202, new wt -512 given clause #199: (wt=-1003) 574 [para_into,573.1.1.3,347.1.2] f(x,y,f(z,z,u))=f(z,y,x). given clause #200: (wt=-987) 566 [para_from,416.1.1,423.1.1,flip.1] f(x,f(y,x,z),f(x,u,w))=f(y,x,f(x,u,f(x,z,w))). given clause #201: (wt=-981) 572 [para_into,571.1.1,522.1.2] f(x,f(y,z,u),f(z,u,f(w,y,f(y,z,f(y,w5,u)))))=f(y,u,z). +++ bsub adjust, cl 203, new wt -512 given clause #202: (wt=-997) 575 [para_from,572.1.1,574.1.1.3,flip.1] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). +++ bsub adjust, cl 204, new wt -512 given clause #203: (wt=-997) 576 [para_into,575.1.1,323.1.2] f(x,f(y,z,u),w)=f(x,w,f(y,u,z)). +++ bsub adjust, cl 106, new wt -256 given clause #204: (wt=-481) 577 [para_into,576.1.1,473.1.1,flip.1] f(x,f(x,y,z),f(u,f(w,y,z),y))=f(x,y,z). given clause #205: (wt=-473) 514 [para_into,382.1.1.3,383.1.2,flip.1] f(x,y,f(y,z,f(y,u,w)))=f(y,z,f(y,w,f(x,y,u))). given clause #206: (wt=-473) 551 [para_into,549.1.1.3.3.3,6.1.2] f(x,y,f(z,y,f(u,y,f(z,x,w))))=f(z,y,f(y,u,x)). +++ bsub adjust, cl 205, new wt -512 given clause #207: (wt=-985) 578 [para_into,551.1.1.3.3,4.1.2] f(x,y,f(z,y,f(y,u,f(z,x,w))))=f(z,y,f(y,u,x)). +++ bsub adjust, cl 206, new wt -512 given clause #208: (wt=-985) 579 [para_into,578.1.1,4.1.2] f(x,y,f(z,x,f(x,u,f(z,y,w))))=f(z,x,f(x,u,y)). given clause #209: (wt=-463) 445 [para_from,415.1.2,388.1.2.3,flip.1] f(x,y,f(x,f(z,u,w),f(w5,x,z)))=f(w5,x,f(x,y,f(z,w,f(x,z,u)))). +++ bsub adjust, cl 208, new wt -512 given clause #210: (wt=-975) 580 [para_into,445.1.1.3.3,323.1.1,flip.1] f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(u,w5,w),f(y,u,x))). +++ bsub adjust, cl 210, new wt -512 given clause #211: (wt=-975) 581 [para_into,580.1.2.3,5.1.2,flip.1] f(x,y,f(x,f(x,z,u),f(z,w,w5)))=f(u,x,f(x,y,f(z,w5,f(x,z,w)))). +++ bsub adjust, cl 212, new wt -512 +++ bsub adjust, cl 211, new wt -512 given clause #212: (wt=-975) 582 [para_into,581.1.2,4.1.2,flip.1] f(x,y,f(x,z,f(u,w,f(x,u,w5))))=f(x,z,f(x,f(x,u,y),f(u,w5,w))). +++ bsub adjust, cl 213, new wt -512 +++ bsub adjust, cl 215, new wt -512 +++ bsub adjust, cl 214, new wt -512 +++ bsub adjust, cl 209, new wt -512 given clause #213: (wt=-975) 583 [para_from,581.1.2,4.1.2,flip.1] f(x,y,f(x,f(x,z,u),f(z,w,w5)))=f(x,u,f(x,y,f(z,w5,f(x,z,w)))). given clause #214: (wt=-975) 587 [para_from,582.1.1,4.1.1,flip.1] f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(y,u,x),f(u,w5,w))). +++ bsub adjust, cl 207, new wt -512 given clause #215: (wt=-975) 588 [para_into,587.1.2.3,5.1.2,flip.1] f(x,y,f(x,f(z,u,w),f(x,z,w5)))=f(w5,x,f(x,y,f(z,w,f(x,z,u)))). given clause #216: (wt=-971) 584 [para_into,582.1.2,516.1.1] f(x,y,f(x,f(z,u,f(x,w,y)),f(w,u,f(x,w,z))))=f(x,f(x,w,y),f(w,z,u)). +++ bsub adjust, cl 216, new wt -512 given clause #217: (wt=-981) 589 [para_into,584.1.1.3,538.1.1] f(x,y,f(x,z,f(u,w,f(x,z,y))))=f(x,f(x,z,y),f(z,u,w)). given clause #218: (wt=-921) 585 [para_from,582.1.1,510.1.2.3,flip.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(y,z,f(z,y,u)),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). +++ bsub adjust, cl 217, new wt -512 given clause #219: (wt=-927) 590 [para_into,585.1.2.2,340.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). +++ bsub adjust, cl 218, new wt -512 given clause #220: (wt=-933) 591 [para_into,590.1.2.3.3.3.3,340.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(z,y,u))))). +++ bsub adjust, cl 219, new wt -512 given clause #221: (wt=-933) 592 [para_into,591.1.2.3,4.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,y,f(z,f(z,y,u),f(x,w,f(z,y,u))))). +++ bsub adjust, cl 220, new wt -512 given clause #222: (wt=-937) 593 [para_into,592.1.2.3,569.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,u,f(z,y,f(x,w,f(z,y,u))))). +++ bsub adjust, cl 221, new wt -512 given clause #223: (wt=-945) 594 [para_into,593.1.2.3,589.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,f(z,y,u),f(y,x,w))). +++ bsub adjust, cl 222, new wt -512 given clause #224: (wt=-955) 595 [para_into,594.1.2,327.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,x,w)). +++ bsub adjust, cl 223, new wt -512 given clause #225: (wt=-961) 596 [para_into,595.1.1.2,340.1.1] f(x,f(y,z,u),f(y,w,f(y,f(y,z,f(z,y,f(y,z,u))),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). +++ bsub adjust, cl 224, new wt -512 given clause #226: (wt=-973) 597 [para_into,596.1.1.3.3.2,362.1.1] f(x,f(y,z,u),f(y,w,f(y,f(y,z,u),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). +++ bsub adjust, cl 225, new wt -512 given clause #227: (wt=-983) 598 [para_into,597.1.1.3.3,461.1.1] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(z,x,w)). +++ bsub adjust, cl 224, new wt -256 +++ bsub adjust, cl 226, new wt -512 given clause #228: (wt=-983) 600 [para_into,598.1.2.3,323.1.2] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(w,z,x)). +++ bsub adjust, cl 227, new wt -512 given clause #229: (wt=-983) 601 [para_into,600.1.2,5.1.2] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(w,z,x),f(y,z,u)). +++ bsub adjust, cl 228, new wt -512 +++ bsub adjust, cl 229, new wt -512 given clause #230: (wt=-983) 602 [para_into,601.1.1.3,414.1.1] f(x,f(y,z,u),f(y,z,f(w,y,u)))=f(y,f(w,z,x),f(y,z,u)). +++ bsub adjust, cl 230, new wt -512 given clause #231: (wt=-975) 604 [para_into,602.1.2,508.1.1] f(x,f(y,z,f(x,u,w)),f(y,z,f(w,y,f(x,u,w))))=f(y,z,f(x,u,w)). given clause #232: (wt=-965) 603 [para_into,601.1.1,454.1.2] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(y,f(x,z,w5),f(y,z,f(y,u,w))). +++ bsub adjust, cl 231, new wt -512 given clause #233: (wt=-949) 605 [para_into,603.1.1.2,555.1.1] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(z,y,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). +++ bsub adjust, cl 232, new wt -512 given clause #234: (wt=-949) 606 [para_into,605.1.1.3.3.3,4.1.2] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(y,z,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). +++ bsub adjust, cl 233, new wt -512 given clause #235: (wt=-949) 607 [para_into,606.1.1.3.3,5.1.2] f(x,f(y,z,u),f(z,u,f(z,f(y,z,w),f(y,z,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5))))). +++ bsub adjust, cl 235, new wt -512 given clause #236: (wt=-953) 608 [para_into,607.1.1.3.3,441.1.1,flip.1] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(x,z,f(w,x,f(x,u,f(w,z,w5))))). +++ bsub adjust, cl 236, new wt -512 given clause #237: (wt=-965) 609 [para_into,608.1.2.3,579.1.1] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,u,z))). +++ bsub adjust, cl 237, new wt -512 +++ bsub adjust, cl 234, new wt -512 given clause #238: (wt=-965) 610 [para_into,609.1.2.3.3,5.1.2] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,z,u))). +++ bsub adjust, cl 238, new wt -512 given clause #239: (wt=-983) 612 [para_into,610.1.1.3,555.1.1,flip.1] f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(z,f(x,u,w),f(y,z,u)). +++ bsub adjust, cl 240, new wt -512 +++ bsub adjust, cl 239, new wt -512 +++ bsub adjust, cl 240, new wt -256 +++ bsub adjust, cl 237, new wt -256 given clause #240: (wt=-983) 614 [para_into,612.1.1.3,389.1.1] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,u,w),f(y,z,u)). given clause #241: (wt=-953) 611 [para_into,609.1.2.3,579.1.2,flip.1] f(x,f(y,z,u),f(z,u,f(y,z,f(z,w,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w6))))). +++ bsub adjust, cl 235, new wt -256 +++ bsub adjust, cl 235, new wt -128 +++ bsub adjust, cl 233, new wt -256 given clause #242: (wt=-921) 586 [para_from,582.1.1,509.1.1.3,flip.1] f(x,f(y,x,f(x,y,z)),f(y,x,f(x,f(x,y,z),f(u,w,f(y,x,f(x,y,z))))))=f(u,f(y,x,f(x,y,z)),f(x,w,f(x,f(x,y,f(y,x,f(x,y,z))),f(y,z,x)))). given clause #243: (wt=-471) 615 [para_into,612.1.1.3,388.1.1] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(x,u,w),f(y,z,u)). +++ bsub adjust, cl 241, new wt -512 +++ bsub adjust, cl 242, new wt -512 given clause #244: (wt=-996) 620 [para_into,615.1.1,522.1.2] f(f(x,y,z),f(x,y,u),f(y,u,w))=f(y,f(w,u,z),f(x,y,u)). +++ bsub adjust, cl 243, new wt -512 given clause #245: (wt=-983) 621 [para_into,615.1.2.2,6.1.2] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(w,u,x),f(y,z,u)). +++ bsub adjust, cl 244, new wt -512 given clause #246: (wt=-983) 622 [para_into,620.1.1,532.1.1] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(z,u,y)). +++ bsub adjust, cl 245, new wt -512 given clause #247: (wt=-983) 623 [para_into,621.1.1.3.3,323.1.2] f(x,f(y,z,u),f(z,u,f(w,y,z)))=f(z,f(w,u,x),f(y,z,u)). +++ bsub adjust, cl 246, new wt -512 given clause #248: (wt=-996) 625 [para_into,623.1.1,522.1.2] f(f(x,y,z),f(y,z,u),f(z,u,w))=f(z,f(x,u,w),f(y,z,u)). given clause #249: (wt=-983) 624 [para_into,622.1.2.3,323.1.2] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(y,z,u)). +++ bsub adjust, cl 247, new wt -512 +++ bsub adjust, cl 248, new wt -512 given clause #250: (wt=-996) 627 [para_into,624.1.1,537.1.1] f(f(x,y,z),f(u,w,y),f(w,x,y))=f(y,f(u,w,z),f(w,x,y)). +++ bsub adjust, cl 249, new wt -512 given clause #251: (wt=-996) 628 [para_into,627.1.1,323.1.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(y,u,z)). +++ bsub adjust, cl 250, new wt -512 given clause #252: (wt=-996) 629 [para_into,628.1.2.3,323.1.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(u,z,y)). +++ bsub adjust, cl 252, new wt -512 +++ bsub adjust, cl 251, new wt -512 given clause #253: (wt=-1003) 630 [para_into,629.1.2,625.1.2,flip.1] f(f(x,y,z),f(y,z,u),f(z,u,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). +++ bsub adjust, cl 254, new wt -512 given clause #254: (wt=-1003) 631 [para_from,629.1.2,625.1.2,flip.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(u,z,y),f(z,y,w)). +++ bsub adjust, cl 253, new wt -512 given clause #255: (wt=-1003) 632 [para_into,630.1.1.3,4.1.2,flip.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(u,z,y),f(y,z,w)). +++ bsub adjust, cl 256, new wt -512 given clause #256: (wt=-1003) 633 [para_into,631.1.2.3,4.1.2,flip.1] f(f(x,y,z),f(y,z,u),f(u,z,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). +++ bsub adjust, cl 255, new wt -512 given clause #257: (wt=-1003) 634 [para_into,632.1.2.2,323.1.2,flip.1] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). +++ bsub adjust, cl 257, new wt -512 given clause #258: (wt=-1003) 635 [para_into,633.1.1.2,323.1.2,flip.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(y,u,z),f(y,z,w)). given clause #259: (wt=-996) 636 [para_into,634.1.2,628.1.1] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,y,z)). +++ bsub adjust, cl 258, new wt -512 given clause #260: (wt=-996) 637 [para_into,636.1.2.3,5.1.2] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,z,y)). +++ bsub adjust, cl 259, new wt -512 given clause #261: (wt=-996) 638 [para_into,637.1.1.1,5.1.2] f(f(x,y,z),f(u,z,y),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). +++ bsub adjust, cl 260, new wt -512 given clause #262: (wt=-996) 639 [para_into,638.1.1.2,5.1.2] f(f(x,y,z),f(u,y,z),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). +++ bsub adjust, cl 261, new wt -512 given clause #263: (wt=-996) 640 [para_into,639.1.1,576.1.2] f(f(x,y,z),f(u,w,y),f(u,y,z))=f(y,f(x,u,w),f(u,y,z)). +++ bsub adjust, cl 262, new wt -512 given clause #264: (wt=-983) 626 [para_into,624.1.1.3,373.1.2] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,z,u)). +++ bsub adjust, cl 263, new wt -512 given clause #265: (wt=-983) 642 [para_into,626.1.2.3,5.1.2] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,u,z)). +++ bsub adjust, cl 264, new wt -512 given clause #266: (wt=-983) 643 [para_into,642.1.1.2,5.1.2] f(x,f(y,z,u),f(z,w,f(y,u,z)))=f(z,f(x,y,w),f(y,z,u)). +++ bsub adjust, cl 265, new wt -512 given clause #267: (wt=-983) 644 [para_into,643.1.1.3.3,5.1.2] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). +++ bsub adjust, cl 266, new wt -512 given clause #268: (wt=-983) 645 [para_into,644.1.1.3,4.1.2] f(x,f(y,z,u),f(w,z,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). given clause #269: (wt=-964) 641 [para_into,640.1.2,554.1.1] f(f(x,y,f(z,y,f(z,f(x,z,u),w))),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 267, new wt -512 given clause #270: (wt=-964) 646 [para_into,641.1.1.1.3.3,5.1.2] f(f(x,y,f(z,y,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). +++ bsub adjust, cl 268, new wt -512 given clause #271: (wt=-964) 647 [para_into,646.1.1.1.3,4.1.2] f(f(x,y,f(y,z,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). +++ bsub adjust, cl 269, new wt -512 given clause #272: (wt=-982) 648 [para_into,647.1.1.1,486.1.1] f(f(x,y,z),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 268, new wt -256 +++ bsub adjust, cl 270, new wt -512 given clause #273: (wt=-982) 650 [para_into,648.1.1.2,323.1.2] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 271, new wt -512 +++ bsub adjust, cl 271, new wt -256 +++ bsub adjust, cl 271, new wt -128 given clause #274: (wt=-463) 512 [para_into,382.1.1.3,407.1.1,flip.1] f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(u,w5,w),f(x,y,u))). +++ bsub adjust, cl 207, new wt -256 +++ bsub adjust, cl 207, new wt -128 given clause #275: (wt=-461) 545 [para_into,544.1.2.3,475.1.2] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(z,f(w6,w,w5),f(z,w,w5))). +++ bsub adjust, cl 176, new wt -256 given clause #276: (wt=-461) 599 [para_into,598.1.1.3.3,461.1.2] f(x,f(y,z,u),f(y,w,f(y,f(y,z,u),f(z,u,w5))))=f(y,f(y,z,u),f(z,x,w)). +++ bsub adjust, cl 223, new wt -256 +++ bsub adjust, cl 224, new wt -128 +++ bsub adjust, cl 224, new wt -64 +++ bsub adjust, cl 224, new wt -32 given clause #277: (wt=-461) 656 [para_into,545.1.1.3,323.1.2] f(x,f(y,f(x,y,z),f(u,w,w5)),f(z,w,w5))=f(x,y,f(z,f(w6,w,w5),f(z,w,w5))). +++ bsub adjust, cl 175, new wt -256 given clause #278: (wt=-461) 661 [para_into,656.1.1.2,5.1.2] f(x,f(y,f(z,u,w),f(x,y,w5)),f(w5,u,w))=f(x,y,f(w5,f(w6,u,w),f(w5,u,w))). given clause #279: (wt=-453) 616 [para_into,612.1.2.3,555.1.2,flip.1] f(x,f(y,z,u),f(x,z,f(w,w5,f(w5,x,f(w5,z,w6)))))=f(y,f(w5,x,z),f(w5,x,f(x,z,u))). +++ bsub adjust, cl 236, new wt -256 given clause #280: (wt=-453) 662 [para_into,616.1.2.3.3,5.1.2] f(x,f(y,z,u),f(x,z,f(w,w5,f(w5,x,f(w5,z,w6)))))=f(y,f(w5,x,z),f(w5,x,f(x,u,z))). +++ bsub adjust, cl 234, new wt -256 given clause #281: (wt=-452) 649 [para_into,648.1.1.1,486.1.2] f(f(x,y,f(y,z,f(z,u,f(x,z,w)))),f(z,w5,y),f(z,y,f(z,y,f(z,f(x,z,w5),w6))))=f(z,y,f(x,z,w5)). +++ bsub adjust, cl 267, new wt -256 given clause #282: (wt=-452) 664 [para_into,649.1.1.1.3,4.1.2] f(f(x,y,f(z,y,f(z,u,f(x,z,w)))),f(z,w5,y),f(z,y,f(z,y,f(z,f(x,z,w5),w6))))=f(z,y,f(x,z,w5)). +++ bsub adjust, cl 262, new wt -256 given clause #283: (wt=-452) 665 [para_into,664.1.1.1.3.3,390.1.2] f(f(x,y,f(z,y,f(z,f(x,z,u),w))),f(z,w5,y),f(z,y,f(z,y,f(z,f(x,z,w5),w6))))=f(z,y,f(x,z,w5)). given clause #284: (wt=-449) 657 [para_into,599.1.1.3.3.2,362.1.2] f(x,f(y,z,u),f(y,w,f(y,f(y,z,f(z,y,f(y,z,u))),f(z,u,w5))))=f(y,f(y,z,u),f(z,x,w)). +++ bsub adjust, cl 222, new wt -256 given clause #285: (wt=-443) 666 [para_into,657.1.1.2,340.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(y,x,w)). +++ bsub adjust, cl 221, new wt -256 given clause #286: (wt=-441) 663 [para_into,662.1.2.3,579.1.2,flip.1] f(x,f(y,z,u),f(z,u,f(y,z,f(z,w,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(w6,y,f(y,z,f(y,u,w7))))). +++ bsub adjust, cl 235, new wt -64 +++ bsub adjust, cl 235, new wt -32 +++ bsub adjust, cl 233, new wt -128 given clause #287: (wt=-433) 667 [para_into,666.1.2,327.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(z,f(z,y,u),f(y,x,w))). +++ bsub adjust, cl 220, new wt -256 given clause #288: (wt=-425) 671 [para_into,667.1.2.3,589.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(z,u,f(z,y,f(x,w,f(z,y,u))))). +++ bsub adjust, cl 219, new wt -256 given clause #289: (wt=-421) 672 [para_into,671.1.2.3,569.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(z,y,f(z,f(z,y,u),f(x,w,f(z,y,u))))). +++ bsub adjust, cl 218, new wt -256 given clause #290: (wt=-421) 673 [para_into,672.1.2.3,4.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(z,y,u))))). +++ bsub adjust, cl 217, new wt -256 given clause #291: (wt=-415) 674 [para_into,673.1.2.3.3.3.3,340.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,w5))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). +++ bsub adjust, cl 214, new wt -256 given clause #292: (wt=-409) 675 [para_into,674.1.2.2,340.1.2,flip.1] f(x,f(y,x,f(x,y,z)),f(y,x,f(x,f(x,y,z),f(u,w,f(y,x,f(x,y,z))))))=f(u,f(y,x,f(x,y,z)),f(x,w,f(x,f(x,y,f(y,x,f(x,y,z))),f(y,z,w5)))). +++ bsub adjust, cl 215, new wt -256 +++ bsub adjust, cl 215, new wt -128 given clause #293: (wt=-241) 350 [para_into,347.1.1,6.1.2,flip.1] f(x,x,y)=f(z,x,x). given clause #294: (wt=-225) 460 [para_into,458.1.1.3,390.1.1] f(x,f(x,y,z),f(y,u,f(w,y,z)))=f(x,y,z). +++ bsub adjust, cl 106, new wt -128 given clause #295: (wt=-225) 687 [para_into,460.1.1.3,323.1.1] f(x,f(x,y,z),f(u,f(w,y,z),y))=f(x,y,z). given clause #296: (wt=-222) 517 [para_into,507.1.2.2,402.1.2] f(f(x,y,z),f(u,z,w),f(u,z,w5))=f(w5,f(y,z,f(x,u,z)),f(u,z,w)). given clause #297: (wt=-219) 553 [para_into,448.1.2.3,423.1.2] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). +++ bsub adjust, cl 100, new wt -256 given clause #298: (wt=-473) 688 [para_into,553.1.1,433.1.1,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,w,f(x,y,f(x,u,z))). +++ bsub adjust, cl 104, new wt -256 +++ bsub adjust, cl 105, new wt -256 given clause #299: (wt=-441) 689 [para_from,688.1.2,402.1.1.3,flip.1] f(x,f(y,z,f(y,u,w)),f(y,w5,f(y,z,f(y,u,w))))=f(w5,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,x)))). given clause #300: (wt=-441) 690 [para_from,688.1.2,402.1.2.3,flip.1] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(w5,f(y,z,f(y,u,w)),f(y,x,f(y,z,f(y,u,w)))). given clause #301: (wt=-214) 653 [para_into,650.1.1.3.3.3,538.1.1] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,w,f(x,z,u)))))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 272, new wt -512 given clause #302: (wt=-988) 691 [para_into,653.1.1.3,341.1.1] f(f(x,y,z),f(y,z,u),f(y,z,f(z,w,f(x,z,u))))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 273, new wt -512 given clause #303: (wt=-994) 692 [para_into,691.1.1,519.1.1] f(f(x,y,f(z,x,u)),f(z,w,x),f(w,x,u))=f(x,w,f(z,x,u)). +++ bsub adjust, cl 274, new wt -512 given clause #304: (wt=-994) 693 [para_into,692.1.1,323.1.1] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(z,y,f(x,z,u)). +++ bsub adjust, cl 272, new wt -256 +++ bsub adjust, cl 272, new wt -128 +++ bsub adjust, cl 275, new wt -512 given clause #305: (wt=-994) 696 [para_into,693.1.2,4.1.2] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(y,z,f(x,z,u)). +++ bsub adjust, cl 276, new wt -512 given clause #306: (wt=-948) 697 [para_into,696.1.1,482.1.2] f(f(x,y,f(z,x,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 277, new wt -512 given clause #307: (wt=-948) 698 [para_into,697.1.1.1.3,4.1.2] f(f(x,y,f(x,z,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 278, new wt -512 given clause #308: (wt=-948) 699 [para_into,698.1.1.2.2,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 279, new wt -512 given clause #309: (wt=-948) 700 [para_into,699.1.1.2.3.1,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 280, new wt -512 given clause #310: (wt=-948) 701 [para_into,700.1.1.2.3.2,323.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(x,u,w5),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 281, new wt -512 given clause #311: (wt=-948) 702 [para_into,701.1.1.2.3,555.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 282, new wt -512 given clause #312: (wt=-948) 703 [para_into,702.1.1.3.1,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 283, new wt -512 given clause #313: (wt=-948) 704 [para_into,703.1.1.3.2,323.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(x,u,w5),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). +++ bsub adjust, cl 284, new wt -512 given clause #314: (wt=-970) 705 [para_into,704.1.1,563.1.1] f(f(x,y,f(x,z,u)),f(x,z,w),f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w)))=f(w,x,f(z,x,u)). +++ bsub adjust, cl 285, new wt -512 given clause #315: (wt=-994) 706 [para_into,705.1.1,327.1.1] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(z,x,u)). +++ bsub adjust, cl 286, new wt -512 given clause #316: (wt=-994) 707 [para_into,706.1.2.3,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(x,z,u)). +++ bsub adjust, cl 287, new wt -512 given clause #317: (wt=-994) 708 [para_into,707.1.2,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(x,w,f(x,z,u)). +++ bsub adjust, cl 288, new wt -512 given clause #318: (wt=-982) 709 [para_into,708.1.1.1,489.1.2] f(f(x,f(y,z,u),f(u,x,f(u,y,z))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). +++ bsub adjust, cl 289, new wt -512 given clause #319: (wt=-982) 710 [para_into,709.1.1.1.3.3,323.1.1] f(f(x,f(y,z,u),f(u,x,f(y,z,u))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). +++ bsub adjust, cl 290, new wt -512 given clause #320: (wt=-994) 711 [para_into,710.1.1.1,365.1.1] f(f(x,y,f(z,u,y)),f(y,z,w),f(y,u,w))=f(y,w,f(y,z,u)). +++ bsub adjust, cl 291, new wt -512 given clause #321: (wt=-994) 712 [para_into,711.1.1.2,4.1.2] f(f(x,y,f(z,u,y)),f(z,y,w),f(y,u,w))=f(y,w,f(y,z,u)). +++ bsub adjust, cl 292, new wt -512 given clause #322: (wt=-994) 713 [para_into,712.1.1.3,4.1.2] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(y,z,u)). +++ bsub adjust, cl 293, new wt -512 given clause #323: (wt=-994) 714 [para_into,713.1.2.3,323.1.1] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). +++ bsub adjust, cl 294, new wt -512 given clause #324: (wt=-994) 715 [para_into,714.1.1.1.3,5.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). +++ bsub adjust, cl 295, new wt -512 given clause #325: (wt=-994) 716 [para_into,715.1.1.3,4.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,u,y)). +++ bsub adjust, cl 296, new wt -512 given clause #326: (wt=-994) 717 [para_into,716.1.2.3,5.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,y,u)). +++ bsub adjust, cl 297, new wt -512 given clause #327: (wt=-976) 718 [para_into,717.1.1.1,429.1.2] f(f(x,f(x,y,z),f(u,y,z)),f(y,z,w),f(z,f(u,y,x),w))=f(z,w,f(y,z,f(u,y,x))). +++ bsub adjust, cl 298, new wt -512 given clause #328: (wt=-988) 719 [para_into,718.1.1.1,462.1.1] f(f(x,y,z),f(y,z,u),f(z,f(w,y,x),u))=f(z,u,f(y,z,f(w,y,x))). +++ bsub adjust, cl 297, new wt -256 +++ bsub adjust, cl 299, new wt -512 given clause #329: (wt=-988) 721 [para_into,719.1.1.3.2,323.1.2] f(f(x,y,z),f(y,z,u),f(z,f(x,w,y),u))=f(z,u,f(y,z,f(w,y,x))). +++ bsub adjust, cl 300, new wt -512 given clause #330: (wt=-988) 722 [para_into,721.1.1.3,5.1.2] f(f(x,y,z),f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(y,z,f(w,y,x))). +++ bsub adjust, cl 301, new wt -512 given clause #331: (wt=-981) 723 [para_into,722.1.1,625.1.1] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(u,w,y))). +++ bsub adjust, cl 302, new wt -512 given clause #332: (wt=-981) 724 [para_into,723.1.2.3.3,323.1.2] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(y,u,w))). +++ bsub adjust, cl 303, new wt -512 given clause #333: (wt=-971) 725 [para_from,724.1.2,604.1.1.3] f(x,f(y,z,f(x,u,w)),f(y,f(x,z,f(x,u,w)),f(w,y,z)))=f(y,z,f(x,u,w)). +++ bsub adjust, cl 304, new wt -512 given clause #334: (wt=-967) 726 [para_into,725.1.1.3,614.1.2] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(w,y,z))))=f(y,z,f(x,u,w)). +++ bsub adjust, cl 305, new wt -512 given clause #335: (wt=-961) 727 [para_into,726.1.1.3.3.3,354.1.2] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(y,z,f(w,y,z)))))=f(y,z,f(x,u,w)). +++ bsub adjust, cl 306, new wt -512 given clause #336: (wt=-987) 728 [para_into,727.1.1,494.1.1] f(x,f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 307, new wt -512 given clause #337: (wt=-971) 729 [para_into,728.1.1.3,477.1.2] f(x,f(y,z,u),f(u,f(x,w,y),f(z,u,f(w5,z,f(x,w,y)))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 308, new wt -512 given clause #338: (wt=-959) 730 [para_into,729.1.1.3.2,558.1.2] f(x,f(y,z,u),f(u,f(x,y,f(w,w5,f(x,w,y))),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 309, new wt -512 given clause #339: (wt=-959) 731 [para_into,730.1.1.3.2,323.1.1] f(x,f(y,z,u),f(u,f(y,f(w,w5,f(x,w,y)),x),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 310, new wt -512 given clause #340: (wt=-955) 732 [para_into,731.1.1.3,623.1.2] f(x,f(y,z,u),f(x,f(z,u,f(w,z,f(x,w,y))),f(u,f(w,z,f(x,w,y)),f(y,z,u))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 311, new wt -512 given clause #341: (wt=-955) 733 [para_into,732.1.1.3,5.1.2] f(x,f(y,z,u),f(x,f(u,f(w,z,f(x,w,y)),f(y,z,u)),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 312, new wt -512 given clause #342: (wt=-955) 734 [para_into,733.1.1.3.2,323.1.2] f(x,f(y,z,u),f(x,f(f(y,z,u),u,f(w,z,f(x,w,y))),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 313, new wt -512 given clause #343: (wt=-981) 735 [para_into,734.1.1,560.1.1] f(x,f(y,z,u),f(z,u,f(w,z,f(x,w,y))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 314, new wt -512 given clause #344: (wt=-983) 736 [para_into,735.1.1.3,391.1.2] f(x,f(y,z,u),f(z,f(x,w,y),f(w,z,u)))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 315, new wt -512 given clause #345: (wt=-977) 737 [para_into,736.1.1.3,645.1.2] f(x,f(y,z,u),f(x,f(w,z,u),f(y,z,f(w,z,u))))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 316, new wt -512 given clause #346: (wt=-993) 738 [para_into,737.1.1,515.1.1] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(x,w,y)). +++ bsub adjust, cl 317, new wt -512 given clause #347: (wt=-993) 739 [para_into,738.1.2.3,4.1.2] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(w,x,y)). +++ bsub adjust, cl 318, new wt -512 given clause #348: (wt=-981) 740 [para_into,739.1.1.3,470.1.2] f(x,f(y,z,u),f(z,u,f(w,w5,f(w,z,u))))=f(z,u,f(w,x,y)). +++ bsub adjust, cl 319, new wt -512 given clause #349: (wt=-994) 741 [para_into,740.1.1,530.1.1] f(f(x,y,f(x,z,u)),f(w,z,u),f(w5,z,u))=f(z,u,f(x,w,w5)). +++ bsub adjust, cl 320, new wt -512 ----> UNIT CONFLICT at 21.81 sec ----> 743 [binary,742.1,8.1] $ANS("distributivity"). Length of proof is 271. Level of proof is 100. ---------------- PROOF ---------------- 1 [] f(x,x,y)=x. 2 [] f(x,y,x)=x. 3 [] f(y,x,x)=x. 4 [] f(x,y,z)=f(y,x,z). 5 [] f(x,y,z)=f(x,z,y). 6 [] f(x,y,z)=f(z,y,x). 7 [] f(f(x,w,y),w,z)=f(x,w,f(y,w,z)). 8 [] f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C))|$ANS("distributivity"). 323 [para_into,5.1.2,4.1.2,flip.1] f(x,y,z)=f(y,z,x). 324 [para_into,7.1.1.1,6.1.2] f(f(x,y,z),y,u)=f(z,y,f(x,y,u)). 325 [para_into,7.1.1.1,5.1.2] f(f(x,y,z),z,u)=f(x,z,f(y,z,u)). 326 [para_into,7.1.1.1,4.1.2] f(f(x,y,z),x,u)=f(y,x,f(z,x,u)). 327 [para_into,7.1.1.1,2.1.1,flip.1] f(x,y,f(x,y,z))=f(x,y,z). 328 [para_into,7.1.1,6.1.2,flip.1] f(x,y,f(z,y,u))=f(u,y,f(x,y,z)). 329 [para_into,7.1.1,4.1.2,flip.1] f(x,y,f(z,y,u))=f(y,f(x,y,z),u). 331 [para_into,7.1.2.3,2.1.1] f(f(x,y,z),y,z)=f(x,y,z). 333 [para_from,7.1.1,4.1.1,flip.1] f(x,f(y,x,z),u)=f(y,x,f(z,x,u)). 335 [para_into,323.1.1,7.1.1,flip.1] f(x,y,f(z,x,u))=f(z,x,f(u,x,y)). 336 [para_into,327.1.1.3,323.1.2] f(x,y,f(z,x,y))=f(x,y,z). 337 [para_into,327.1.1.3,1.1.1,flip.1] f(x,x,y)=f(x,x,x). 338 [para_into,327.1.1,6.1.2] f(f(x,y,z),y,x)=f(x,y,z). 339 [para_into,327.1.1,5.1.2] f(x,f(x,y,z),y)=f(x,y,z). 340 [para_into,327.1.1,4.1.2] f(x,y,f(y,x,z))=f(y,x,z). 341 [para_into,327.1.2,4.1.2] f(x,y,f(x,y,z))=f(y,x,z). 347 [para_into,337.1.2,337.1.2,flip.1] f(x,x,y)=f(x,x,z). 354 [para_into,331.1.1,323.1.1] f(x,y,f(z,x,y))=f(z,x,y). 358 [para_into,338.1.2,323.1.2] f(f(x,y,z),y,x)=f(z,x,y). 362 [para_into,340.1.1,340.1.2] f(x,y,f(y,x,f(x,y,z)))=f(x,y,z). 365 [para_into,358.1.1,336.1.2] f(f(x,y,z),y,f(x,f(x,y,z),y))=f(z,x,y). 366 [para_into,324.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(z,y,x)). 367 [para_into,324.1.1,7.1.1,flip.1] f(x,y,f(z,y,u))=f(z,y,f(x,y,u)). 370 [para_into,325.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(x,z,y)). 371 [para_into,325.1.1,6.1.2,flip.1] f(x,y,f(z,y,u))=f(u,y,f(x,z,y)). 373 [para_from,325.1.1,323.1.1,flip.1] f(x,y,f(z,u,x))=f(z,x,f(u,x,y)). 374 [para_into,326.1.1,323.1.1,flip.1] f(x,y,f(z,y,u))=f(y,u,f(y,x,z)). 377 [para_into,328.1.2.3,323.1.2,flip.1] f(x,y,f(z,u,y))=f(u,y,f(z,y,x)). 378 [para_into,329.1.1.3,4.1.2,flip.1] f(x,f(y,x,z),u)=f(y,x,f(x,z,u)). 380 [para_into,333.1.2.3,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(x,y,z),u). 387 [para_into,335.1.1.3,323.1.2,flip.1] f(x,y,f(z,y,u))=f(y,u,f(z,x,y)). 388 [para_into,335.1.2.3,323.1.1,flip.1] f(x,y,f(y,z,u))=f(y,z,f(x,y,u)). 389 [para_into,335.1.2.3,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,u,f(x,y,z)). 390 [para_into,366.1.1,323.1.1] f(x,f(y,x,z),u)=f(x,z,f(y,x,u)). 391 [para_into,366.1.1,4.1.2,flip.1] f(x,y,f(z,x,u))=f(x,u,f(z,x,y)). 393 [para_into,367.1.1.3,339.1.1,flip.1] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(u,f(x,y,z),f(x,y,z)). 394 [para_into,370.1.1.3,5.1.2,flip.1] f(x,y,f(z,u,x))=f(z,x,f(u,y,x)). 396 [para_into,371.1.1.3,323.1.2,flip.1] f(x,y,f(z,u,y))=f(z,y,f(x,u,y)). 400 [para_into,374.1.1.3,4.1.2,flip.1] f(x,y,f(x,z,u))=f(z,x,f(x,u,y)). 402 [para_into,377.1.2.3,5.1.2,flip.1] f(x,y,f(z,u,y))=f(u,y,f(z,x,y)). 403 [para_into,378.1.1.2,5.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(x,z,y),u). 404 [para_into,378.1.1.2,4.1.2,flip.1] f(x,y,f(y,z,u))=f(y,f(y,x,z),u). 411 [para_from,388.1.1,378.1.2.3,flip.1] f(x,y,f(z,u,f(y,z,w)))=f(y,f(x,y,z),f(z,u,w)). 413 [para_from,388.1.1,327.1.1.3] f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). 414 [para_from,388.1.1,4.1.1,flip.1] f(x,y,f(x,z,u))=f(x,z,f(y,x,u)). 415 [para_into,389.1.1.3,389.1.1,flip.1] f(x,f(y,z,u),f(w,x,y))=f(w,x,f(y,u,f(x,y,z))). 416 [para_from,389.1.1,388.1.2.3,flip.1] f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,y,f(x,w,z))). 417 [para_into,390.1.1.2,4.1.2] f(x,f(x,y,z),u)=f(x,z,f(y,x,u)). 419 [para_into,391.1.1.3,4.1.2,flip.1] f(x,y,f(z,x,u))=f(x,u,f(x,z,y)). 421 [para_into,396.1.1,380.1.2,flip.1] 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)))). 423 [para_into,400.1.2,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,u,f(x,y,z)). 424 [para_from,400.1.2,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,z,f(x,u,y)). 425 [para_into,403.1.1.3,340.1.1,flip.1] f(x,f(y,z,x),f(z,x,u))=f(y,x,f(z,x,u)). 427 [para_into,404.1.1,4.1.2,flip.1] f(x,f(x,y,z),u)=f(x,y,f(x,z,u)). 429 [para_into,417.1.2.3,391.1.2] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(u,y,x))). 430 [para_into,419.1.1.3,4.1.2,flip.1] f(x,y,f(x,z,u))=f(x,u,f(x,z,y)). 431 [para_from,419.1.2,329.1.1.3,flip.1] f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,w,f(u,z,x))). 433 [para_into,423.1.1.3,423.1.2,flip.1] f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). 435 [para_into,424.1.1.3,388.1.1,flip.1] f(x,y,f(x,f(y,z,u),w))=f(x,w,f(y,z,f(x,y,u))). 436 [para_into,427.1.2.3,424.1.2] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). 438 [para_into,427.1.2.3,388.1.1] f(x,f(x,y,z),f(z,u,w))=f(x,y,f(z,u,f(x,z,w))). 439 [para_into,427.1.2.3,367.1.2] f(x,f(x,y,z),f(u,z,w))=f(x,y,f(u,z,f(x,z,w))). 440 [para_into,425.1.1,389.1.2] f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)). 441 [para_into,413.1.1,380.1.1] f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)). 443 [para_into,411.1.2.2,323.1.1,flip.1] f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(x,y,w))). 445 [para_from,415.1.2,388.1.2.3,flip.1] f(x,y,f(x,f(z,u,w),f(w5,x,z)))=f(w5,x,f(x,y,f(z,w,f(x,z,u)))). 447 [para_into,429.1.2.3.3,6.1.2] f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(x,y,u))). 448 [para_into,433.1.1,5.1.2] f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,u,f(x,w,z))). 449 [para_into,436.1.1,433.1.1,flip.1] f(x,y,f(x,z,f(x,u,w)))=f(x,w,f(x,y,f(x,u,z))). 450 [para_into,443.1.2.3.3,323.1.1,flip.1] f(x,y,f(z,u,f(z,w,y)))=f(y,f(y,z,x),f(z,u,w)). 451 [para_into,443.1.2,4.1.2] f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,u,f(x,y,w))). 454 [para_from,449.1.2,402.1.2.3,flip.1] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(w5,f(y,z,f(y,u,w)),f(y,x,f(y,z,f(y,u,w)))). 455 [para_into,393.1.2,3.1.1] f(x,f(x,y,z),f(u,f(x,y,z),y))=f(x,y,z). 456 [para_into,455.1.1.3,323.1.2] f(x,f(x,y,z),f(y,u,f(x,y,z)))=f(x,y,z). 457 [para_into,456.1.1,438.1.2] f(x,f(x,f(x,y,z),y),f(y,u,z))=f(x,y,z). 458 [para_into,457.1.1.2,339.1.1] f(x,f(x,y,z),f(y,u,z))=f(x,y,z). 461 [para_into,458.1.1.3,339.1.1] f(x,f(x,y,z),f(y,z,u))=f(x,y,z). 462 [para_into,458.1.1.3,4.1.2] f(x,f(x,y,z),f(u,y,z))=f(x,y,z). 463 [para_into,458.1.2,323.1.1] f(x,f(x,y,z),f(y,u,z))=f(y,z,x). 464 [para_into,461.1.1,439.1.1] f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). 465 [para_into,462.1.1,427.1.1] f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). 466 [para_into,462.1.1,5.1.2] f(x,f(y,z,u),f(x,z,u))=f(x,z,u). 467 [para_from,462.1.1,458.1.1.3] f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)). 468 [para_into,463.1.1.2,323.1.2] f(x,f(y,x,z),f(z,u,y))=f(z,y,x). 470 [para_into,463.1.1,450.1.2] f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). 471 [para_from,463.1.1,458.1.1.3] f(x,f(x,y,f(z,u,w)),f(z,w,y))=f(x,y,f(z,u,w)). 473 [para_into,466.1.1.2,324.1.1] f(x,f(y,z,f(u,z,w)),f(x,z,w))=f(x,z,w). 474 [para_into,466.1.1,430.1.2] f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). 475 [para_into,466.1.2,323.1.1] f(x,f(y,z,u),f(x,z,u))=f(z,u,x). 477 [para_into,468.1.1,431.1.1] f(x,y,f(z,x,f(u,z,y)))=f(z,x,y). 478 [para_into,475.1.1.3,323.1.1] f(x,f(y,z,u),f(z,u,x))=f(z,u,x). 479 [para_into,478.1.1.2,323.1.1] f(x,f(y,z,u),f(y,z,x))=f(y,z,x). 480 [para_into,478.1.1,387.1.2] f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). 481 [para_into,479.1.1.2,479.1.1] f(x,f(y,z,u),f(u,f(y,z,w),x))=f(u,f(y,z,w),x). 482 [para_into,479.1.1.2,388.1.2] f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). 484 [para_from,479.1.1,387.1.1.3,flip.1] 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)). 486 [para_into,464.1.1.3.3,388.1.1] f(x,y,f(y,z,f(z,u,f(x,z,w))))=f(x,y,z). 487 [para_into,464.1.1,389.1.1] f(x,f(y,z,u),f(y,x,z))=f(y,x,z). 489 [para_into,487.1.1.2,475.1.1] f(x,f(y,z,u),f(u,x,f(w,y,z)))=f(u,x,f(w,y,z)). 490 [para_from,487.1.1,394.1.2.3] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(w,f(x,y,z),f(x,y,z)). 491 [para_from,487.1.1,461.1.1.3] f(x,f(x,y,f(z,u,w)),f(z,y,u))=f(x,y,f(z,u,w)). 493 [para_into,465.1.1.3.3,6.1.2] f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). 494 [para_into,474.1.1.3.3,430.1.2] f(x,f(y,z,u),f(x,w,f(y,u,f(y,z,w))))=f(x,w,f(y,z,u)). 497 [para_into,490.1.2,3.1.1] f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(x,y,z). 498 [para_into,497.1.1,323.1.2] f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u). 499 [para_into,498.1.1.2,4.1.2] f(f(x,y,f(z,y,u)),f(y,z,u),f(z,u,w))=f(z,y,u). 500 [para_into,499.1.1.1.3,4.1.2] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(z,y,u). 501 [para_into,500.1.2,4.1.2] f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). 502 [para_into,501.1.1.1,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). 503 [para_into,471.1.1,5.1.2] f(x,f(y,z,u),f(x,u,f(y,w,z)))=f(x,u,f(y,w,z)). 504 [para_into,481.1.1,484.1.1] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). 506 [para_into,504.1.1,323.1.2] f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). 507 [para_into,506.1.1,504.1.1,flip.1] f(x,f(y,z,u),f(y,z,w))=f(w,f(y,z,x),f(y,z,u)). 508 [para_into,503.1.1.2,323.1.1] f(x,f(y,z,u),f(x,z,f(u,w,y)))=f(x,z,f(u,w,y)). 510 [para_from,421.1.1,367.1.2.3,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(x,f(y,z,u),f(z,w5,f(y,z,u)))). 515 [para_into,493.1.1.3.3,479.1.1] f(x,f(y,z,u),f(x,w,f(y,z,w)))=f(x,f(y,z,u),w). 516 [para_into,473.1.1.2,480.1.1] f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)). 519 [para_into,507.1.2.2,354.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). 520 [para_into,519.1.1,5.1.2] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 521 [para_into,520.1.1.2,323.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). 522 [para_into,520.1.1,519.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(y,z,u),f(z,u,x)). 523 [para_into,521.1.1,4.1.2] f(f(x,y,z),f(u,y,z),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). 524 [para_into,523.1.1.2,323.1.1] f(f(x,y,z),f(y,z,u),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). 526 [para_from,524.1.1,519.1.1,flip.1] f(x,f(y,z,u),f(z,u,w))=f(y,f(w,z,u),f(z,u,x)). 527 [para_into,522.1.1.2,323.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(z,u,x)). 528 [para_into,522.1.2.2,323.1.2,flip.1] f(x,f(y,z,u),f(u,y,w))=f(w,f(z,u,y),f(u,y,x)). 530 [para_into,526.1.1.3,323.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(y,z,u)). 531 [para_into,527.1.2.3,4.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(z,u,y),f(u,y,x)). 532 [para_into,528.1.1.3,4.1.2,flip.1] f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(u,z,x)). 533 [para_into,531.1.2.2,323.1.2,flip.1] f(x,f(y,z,u),f(u,y,w))=f(w,f(y,z,u),f(y,u,x)). 535 [para_into,533.1.1.3,6.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(y,z,u),f(x,y,u)). 537 [para_from,535.1.2,5.1.2,flip.1] f(x,f(y,z,u),f(y,u,w))=f(w,f(x,y,u),f(y,z,u)). 538 [para_into,447.1.1,491.1.1,flip.1] f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,w,f(y,z,u)). 539 [para_into,538.1.1,5.1.2] f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)). 541 [para_into,539.1.1.3,466.1.1] f(x,f(y,f(z,u,w),f(x,y,w5)),f(w5,u,w))=f(x,y,f(w5,f(z,u,w),f(w5,u,w))). 542 [para_into,541.1.1.2,5.1.2] f(x,f(y,f(x,y,z),f(u,w,w5)),f(z,w,w5))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). 543 [para_into,542.1.1.3,323.1.1] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). 544 [para_into,543.1.2.3,475.1.1] f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(w,w5,z)). 546 [para_from,544.1.1,440.1.1.3,flip.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(x,z,y))). 547 [para_into,546.1.2.3.3,323.1.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(z,y,x))). 548 [para_into,547.1.2,413.1.1] f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,x)). 549 [para_into,548.1.1.3.3.2,2.1.1] f(x,y,f(z,y,f(u,y,f(w,x,z))))=f(z,y,f(y,u,x)). 551 [para_into,549.1.1.3.3.3,6.1.2] f(x,y,f(z,y,f(u,y,f(z,x,w))))=f(z,y,f(y,u,x)). 554 [para_from,448.1.1,470.1.1.3] f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). 555 [para_into,554.1.1.3,4.1.2] f(x,y,f(z,u,f(u,x,f(u,y,w))))=f(u,x,y). 556 [para_into,451.1.1,467.1.1,flip.1] f(x,f(y,z,u),f(w,z,f(x,w,u)))=f(x,w,f(y,z,u)). 557 [para_into,451.1.1,461.1.1,flip.1] f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). 558 [para_into,451.1.1,458.1.1,flip.1] f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). 560 [para_into,556.1.1,435.1.2] f(x,y,f(x,f(y,z,u),f(w,z,u)))=f(x,y,f(w,z,u)). 562 [para_from,557.1.1,427.1.2.3] f(x,f(x,y,z),f(u,z,f(x,u,w)))=f(x,y,f(x,u,z)). 563 [para_into,562.1.1,451.1.2] f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). 564 [para_into,416.1.1,424.1.2,flip.1] f(x,y,f(y,z,f(y,u,w)))=f(y,f(x,y,u),f(y,z,w)). 565 [para_into,416.1.2.3,327.1.1] f(x,y,f(x,z,f(u,x,y)))=f(u,x,f(x,y,z)). 567 [para_into,565.1.1.3.3,323.1.1] f(x,y,f(x,z,f(x,y,u)))=f(u,x,f(x,y,z)). 568 [para_into,567.1.1.3,5.1.2] f(x,y,f(x,f(x,y,z),u))=f(z,x,f(x,y,u)). 569 [para_into,568.1.2,4.1.2] f(x,y,f(x,f(x,y,z),u))=f(x,z,f(x,y,u)). 570 [para_from,564.1.2,502.1.1.1] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w). 571 [para_into,570.1.2,5.1.2] f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,w,z). 572 [para_into,571.1.1,522.1.2] f(x,f(y,z,u),f(z,u,f(w,y,f(y,z,f(y,w5,u)))))=f(y,u,z). 573 [para_into,571.1.1,478.1.1] f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,y,x). 574 [para_into,573.1.1.3,347.1.2] f(x,y,f(z,z,u))=f(z,y,x). 575 [para_from,572.1.1,574.1.1.3,flip.1] f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). 576 [para_into,575.1.1,323.1.2] f(x,f(y,z,u),w)=f(x,w,f(y,u,z)). 578 [para_into,551.1.1.3.3,4.1.2] f(x,y,f(z,y,f(y,u,f(z,x,w))))=f(z,y,f(y,u,x)). 579 [para_into,578.1.1,4.1.2] f(x,y,f(z,x,f(x,u,f(z,y,w))))=f(z,x,f(x,u,y)). 580 [para_into,445.1.1.3.3,323.1.1,flip.1] f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(u,w5,w),f(y,u,x))). 581 [para_into,580.1.2.3,5.1.2,flip.1] f(x,y,f(x,f(x,z,u),f(z,w,w5)))=f(u,x,f(x,y,f(z,w5,f(x,z,w)))). 582 [para_into,581.1.2,4.1.2,flip.1] f(x,y,f(x,z,f(u,w,f(x,u,w5))))=f(x,z,f(x,f(x,u,y),f(u,w5,w))). 584 [para_into,582.1.2,516.1.1] f(x,y,f(x,f(z,u,f(x,w,y)),f(w,u,f(x,w,z))))=f(x,f(x,w,y),f(w,z,u)). 585 [para_from,582.1.1,510.1.2.3,flip.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(y,z,f(z,y,u)),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). 589 [para_into,584.1.1.3,538.1.1] f(x,y,f(x,z,f(u,w,f(x,z,y))))=f(x,f(x,z,y),f(z,u,w)). 590 [para_into,585.1.2.2,340.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). 591 [para_into,590.1.2.3.3.3.3,340.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(z,y,u))))). 592 [para_into,591.1.2.3,4.1.2] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,y,f(z,f(z,y,u),f(x,w,f(z,y,u))))). 593 [para_into,592.1.2.3,569.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,u,f(z,y,f(x,w,f(z,y,u))))). 594 [para_into,593.1.2.3,589.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,f(z,y,u),f(y,x,w))). 595 [para_into,594.1.2,327.1.1] f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,x,w)). 596 [para_into,595.1.1.2,340.1.1] f(x,f(y,z,u),f(y,w,f(y,f(y,z,f(z,y,f(y,z,u))),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). 597 [para_into,596.1.1.3.3.2,362.1.1] f(x,f(y,z,u),f(y,w,f(y,f(y,z,u),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). 598 [para_into,597.1.1.3.3,461.1.1] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(z,x,w)). 600 [para_into,598.1.2.3,323.1.2] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(w,z,x)). 601 [para_into,600.1.2,5.1.2] f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(w,z,x),f(y,z,u)). 602 [para_into,601.1.1.3,414.1.1] f(x,f(y,z,u),f(y,z,f(w,y,u)))=f(y,f(w,z,x),f(y,z,u)). 603 [para_into,601.1.1,454.1.2] f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(y,f(x,z,w5),f(y,z,f(y,u,w))). 604 [para_into,602.1.2,508.1.1] f(x,f(y,z,f(x,u,w)),f(y,z,f(w,y,f(x,u,w))))=f(y,z,f(x,u,w)). 605 [para_into,603.1.1.2,555.1.1] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(z,y,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). 606 [para_into,605.1.1.3.3.3,4.1.2] f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(y,z,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). 607 [para_into,606.1.1.3.3,5.1.2] f(x,f(y,z,u),f(z,u,f(z,f(y,z,w),f(y,z,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5))))). 608 [para_into,607.1.1.3.3,441.1.1,flip.1] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(x,z,f(w,x,f(x,u,f(w,z,w5))))). 609 [para_into,608.1.2.3,579.1.1] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,u,z))). 610 [para_into,609.1.2.3.3,5.1.2] f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,z,u))). 612 [para_into,610.1.1.3,555.1.1,flip.1] f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(z,f(x,u,w),f(y,z,u)). 614 [para_into,612.1.1.3,389.1.1] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,u,w),f(y,z,u)). 615 [para_into,612.1.1.3,388.1.1] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(x,u,w),f(y,z,u)). 620 [para_into,615.1.1,522.1.2] f(f(x,y,z),f(x,y,u),f(y,u,w))=f(y,f(w,u,z),f(x,y,u)). 621 [para_into,615.1.2.2,6.1.2] f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(w,u,x),f(y,z,u)). 622 [para_into,620.1.1,532.1.1] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(z,u,y)). 623 [para_into,621.1.1.3.3,323.1.2] f(x,f(y,z,u),f(z,u,f(w,y,z)))=f(z,f(w,u,x),f(y,z,u)). 624 [para_into,622.1.2.3,323.1.2] f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(y,z,u)). 625 [para_into,623.1.1,522.1.2] f(f(x,y,z),f(y,z,u),f(z,u,w))=f(z,f(x,u,w),f(y,z,u)). 626 [para_into,624.1.1.3,373.1.2] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,z,u)). 627 [para_into,624.1.1,537.1.1] f(f(x,y,z),f(u,w,y),f(w,x,y))=f(y,f(u,w,z),f(w,x,y)). 628 [para_into,627.1.1,323.1.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(y,u,z)). 629 [para_into,628.1.2.3,323.1.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(u,z,y)). 630 [para_into,629.1.2,625.1.2,flip.1] f(f(x,y,z),f(y,z,u),f(z,u,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). 632 [para_into,630.1.1.3,4.1.2,flip.1] f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(u,z,y),f(y,z,w)). 634 [para_into,632.1.2.2,323.1.2,flip.1] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). 636 [para_into,634.1.2,628.1.1] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,y,z)). 637 [para_into,636.1.2.3,5.1.2] f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,z,y)). 638 [para_into,637.1.1.1,5.1.2] f(f(x,y,z),f(u,z,y),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). 639 [para_into,638.1.1.2,5.1.2] f(f(x,y,z),f(u,y,z),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). 640 [para_into,639.1.1,576.1.2] f(f(x,y,z),f(u,w,y),f(u,y,z))=f(y,f(x,u,w),f(u,y,z)). 641 [para_into,640.1.2,554.1.1] f(f(x,y,f(z,y,f(z,f(x,z,u),w))),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 642 [para_into,626.1.2.3,5.1.2] f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,u,z)). 643 [para_into,642.1.1.2,5.1.2] f(x,f(y,z,u),f(z,w,f(y,u,z)))=f(z,f(x,y,w),f(y,z,u)). 644 [para_into,643.1.1.3.3,5.1.2] f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). 645 [para_into,644.1.1.3,4.1.2] f(x,f(y,z,u),f(w,z,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). 646 [para_into,641.1.1.1.3.3,5.1.2] f(f(x,y,f(z,y,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). 647 [para_into,646.1.1.1.3,4.1.2] f(f(x,y,f(y,z,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). 648 [para_into,647.1.1.1,486.1.1] f(f(x,y,z),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 650 [para_into,648.1.1.2,323.1.2] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). 653 [para_into,650.1.1.3.3.3,538.1.1] f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,w,f(x,z,u)))))=f(z,y,f(x,z,u)). 691 [para_into,653.1.1.3,341.1.1] f(f(x,y,z),f(y,z,u),f(y,z,f(z,w,f(x,z,u))))=f(z,y,f(x,z,u)). 692 [para_into,691.1.1,519.1.1] f(f(x,y,f(z,x,u)),f(z,w,x),f(w,x,u))=f(x,w,f(z,x,u)). 693 [para_into,692.1.1,323.1.1] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(z,y,f(x,z,u)). 696 [para_into,693.1.2,4.1.2] f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(y,z,f(x,z,u)). 697 [para_into,696.1.1,482.1.2] f(f(x,y,f(z,x,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 698 [para_into,697.1.1.1.3,4.1.2] f(f(x,y,f(x,z,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 699 [para_into,698.1.1.2.2,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 700 [para_into,699.1.1.2.3.1,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 701 [para_into,700.1.1.2.3.2,323.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(x,u,w5),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 702 [para_into,701.1.1.2.3,555.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 703 [para_into,702.1.1.3.1,323.1.2] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 704 [para_into,703.1.1.3.2,323.1.1] f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(x,u,w5),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). 705 [para_into,704.1.1,563.1.1] f(f(x,y,f(x,z,u)),f(x,z,w),f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w)))=f(w,x,f(z,x,u)). 706 [para_into,705.1.1,327.1.1] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(z,x,u)). 707 [para_into,706.1.2.3,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(x,z,u)). 708 [para_into,707.1.2,4.1.2] f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(x,w,f(x,z,u)). 709 [para_into,708.1.1.1,489.1.2] f(f(x,f(y,z,u),f(u,x,f(u,y,z))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). 710 [para_into,709.1.1.1.3.3,323.1.1] f(f(x,f(y,z,u),f(u,x,f(y,z,u))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). 711 [para_into,710.1.1.1,365.1.1] f(f(x,y,f(z,u,y)),f(y,z,w),f(y,u,w))=f(y,w,f(y,z,u)). 712 [para_into,711.1.1.2,4.1.2] f(f(x,y,f(z,u,y)),f(z,y,w),f(y,u,w))=f(y,w,f(y,z,u)). 713 [para_into,712.1.1.3,4.1.2] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(y,z,u)). 714 [para_into,713.1.2.3,323.1.1] f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). 715 [para_into,714.1.1.1.3,5.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). 716 [para_into,715.1.1.3,4.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,u,y)). 717 [para_into,716.1.2.3,5.1.2] f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,y,u)). 718 [para_into,717.1.1.1,429.1.2] f(f(x,f(x,y,z),f(u,y,z)),f(y,z,w),f(z,f(u,y,x),w))=f(z,w,f(y,z,f(u,y,x))). 719 [para_into,718.1.1.1,462.1.1] f(f(x,y,z),f(y,z,u),f(z,f(w,y,x),u))=f(z,u,f(y,z,f(w,y,x))). 721 [para_into,719.1.1.3.2,323.1.2] f(f(x,y,z),f(y,z,u),f(z,f(x,w,y),u))=f(z,u,f(y,z,f(w,y,x))). 722 [para_into,721.1.1.3,5.1.2] f(f(x,y,z),f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(y,z,f(w,y,x))). 723 [para_into,722.1.1,625.1.1] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(u,w,y))). 724 [para_into,723.1.2.3.3,323.1.2] f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(y,u,w))). 725 [para_from,724.1.2,604.1.1.3] f(x,f(y,z,f(x,u,w)),f(y,f(x,z,f(x,u,w)),f(w,y,z)))=f(y,z,f(x,u,w)). 726 [para_into,725.1.1.3,614.1.2] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(w,y,z))))=f(y,z,f(x,u,w)). 727 [para_into,726.1.1.3.3.3,354.1.2] f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(y,z,f(w,y,z)))))=f(y,z,f(x,u,w)). 728 [para_into,727.1.1,494.1.1] f(x,f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(x,w,y)). 729 [para_into,728.1.1.3,477.1.2] f(x,f(y,z,u),f(u,f(x,w,y),f(z,u,f(w5,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 730 [para_into,729.1.1.3.2,558.1.2] f(x,f(y,z,u),f(u,f(x,y,f(w,w5,f(x,w,y))),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 731 [para_into,730.1.1.3.2,323.1.1] f(x,f(y,z,u),f(u,f(y,f(w,w5,f(x,w,y)),x),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 732 [para_into,731.1.1.3,623.1.2] f(x,f(y,z,u),f(x,f(z,u,f(w,z,f(x,w,y))),f(u,f(w,z,f(x,w,y)),f(y,z,u))))=f(z,u,f(x,w,y)). 733 [para_into,732.1.1.3,5.1.2] f(x,f(y,z,u),f(x,f(u,f(w,z,f(x,w,y)),f(y,z,u)),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 734 [para_into,733.1.1.3.2,323.1.2] f(x,f(y,z,u),f(x,f(f(y,z,u),u,f(w,z,f(x,w,y))),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). 735 [para_into,734.1.1,560.1.1] f(x,f(y,z,u),f(z,u,f(w,z,f(x,w,y))))=f(z,u,f(x,w,y)). 736 [para_into,735.1.1.3,391.1.2] f(x,f(y,z,u),f(z,f(x,w,y),f(w,z,u)))=f(z,u,f(x,w,y)). 737 [para_into,736.1.1.3,645.1.2] f(x,f(y,z,u),f(x,f(w,z,u),f(y,z,f(w,z,u))))=f(z,u,f(x,w,y)). 738 [para_into,737.1.1,515.1.1] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(x,w,y)). 739 [para_into,738.1.2.3,4.1.2] f(x,f(y,z,u),f(w,z,u))=f(z,u,f(w,x,y)). 740 [para_into,739.1.1.3,470.1.2] f(x,f(y,z,u),f(z,u,f(w,w5,f(w,z,u))))=f(z,u,f(w,x,y)). 741 [para_into,740.1.1,530.1.1] f(f(x,y,f(x,z,u)),f(w,z,u),f(w5,z,u))=f(z,u,f(x,w,w5)). 742 [para_into,741.1.1.1,473.1.1] f(f(x,y,z),f(u,y,z),f(w,y,z))=f(y,z,f(x,u,w)). 743 [binary,742.1,8.1] $ANS("distributivity"). ------------ end of proof ------------- list(hints2). % Hints from process 24611, Sat Jul 23 00:35:02 2005 f(x,x,y)=x. f(x,y,x)=x. f(x,y,y)=y. f(x,y,z)=f(y,x,z). f(x,y,z)=f(x,z,y). f(x,y,z)=f(z,y,x). f(f(x,y,z),y,u)=f(x,y,f(z,y,u)). f(f(A,D,E),f(B,D,E),f(C,D,E))!=f(D,E,f(A,B,C)). f(x,y,z)=f(y,z,x). f(x,y,z)=f(z,x,y). f(f(x,y,z),y,u)=f(z,y,f(x,y,u)). f(f(x,y,z),z,u)=f(x,z,f(y,z,u)). f(f(x,y,z),x,u)=f(y,x,f(z,x,u)). f(x,y,f(x,y,z))=f(x,y,z). f(x,y,f(z,y,u))=f(z,y,f(u,y,x)). f(x,f(y,x,z),u)=f(y,x,f(z,x,u)). f(f(x,y,z),y,z)=f(x,y,z). f(x,y,f(z,y,u))=f(y,f(x,y,z),u). f(x,y,f(z,x,u))=f(z,x,f(u,x,y)). f(x,y,f(z,y,u))=f(y,u,f(x,y,z)). f(x,y,f(z,x,y))=f(x,y,z). f(x,x,y)=f(x,x,x). f(f(x,y,z),y,x)=f(x,y,z). f(x,f(x,y,z),y)=f(x,y,z). f(x,y,f(y,x,z))=f(y,x,z). f(x,y,f(x,y,z))=f(y,x,z). f(x,x,x)=f(x,x,y). f(x,x,y)=f(x,x,z). f(x,y,f(z,x,y))=f(z,x,y). f(f(x,y,z),y,x)=f(z,x,y). f(x,y,f(y,x,f(x,y,z)))=f(x,y,z). f(f(x,y,z),y,f(x,f(x,y,z),y))=f(z,x,y). f(x,y,f(z,y,u))=f(y,u,f(z,y,x)). f(x,y,f(z,x,u))=f(u,x,f(z,x,y)). f(x,y,f(z,y,u))=f(z,y,f(x,y,u)). f(x,y,f(z,u,x))=f(z,x,f(u,x,y)). f(x,y,f(z,u,y))=f(z,y,f(u,y,x)). f(x,y,f(z,y,u))=f(y,u,f(x,z,y)). f(x,y,f(z,y,u))=f(y,u,f(y,x,z)). f(x,y,f(x,z,u))=f(z,x,f(u,x,y)). f(x,y,f(z,u,y))=f(u,y,f(z,y,x)). f(x,y,f(z,y,u))=f(u,y,f(z,x,y)). f(x,f(y,x,z),u)=f(y,x,f(x,z,u)). f(x,y,f(y,z,u))=f(y,f(x,y,z),u). f(x,y,f(z,y,u))=f(y,u,f(z,x,y)). f(x,y,f(z,u,x))=f(u,x,f(z,x,y)). f(x,y,f(y,z,u))=f(y,z,f(x,y,u)). f(x,y,f(z,x,u))=f(z,x,f(x,y,u)). f(x,y,f(y,z,u))=f(y,u,f(x,y,z)). f(x,y,f(z,x,u))=f(z,x,f(x,u,y)). f(x,f(y,x,z),u)=f(x,z,f(y,x,u)). f(x,y,f(z,x,u))=f(x,u,f(z,x,y)). f(x,f(x,y,z),f(u,f(x,y,z),y))=f(u,f(x,y,z),f(x,y,z)). f(x,y,f(z,u,x))=f(z,x,f(u,y,x)). f(x,y,f(z,u,y))=f(y,u,f(x,z,y)). f(x,y,f(z,u,y))=f(z,y,f(x,u,y)). f(x,y,f(x,z,u))=f(z,x,f(x,u,y)). f(x,y,f(y,z,u))=f(y,u,f(y,x,z)). f(x,y,f(z,u,y))=f(u,y,f(z,x,y)). f(x,y,f(y,z,u))=f(y,f(x,z,y),u). f(x,f(y,z,x),u)=f(y,x,f(x,z,u)). f(x,y,f(y,z,u))=f(y,f(y,x,z),u). f(x,f(x,y,z),u)=f(y,x,f(x,z,u)). f(x,y,f(z,u,f(y,z,w)))=f(y,f(x,y,z),f(z,u,w)). f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,u,f(x,z,w))). f(x,y,f(y,z,f(x,y,u)))=f(x,y,f(y,z,u)). f(x,y,f(x,z,u))=f(x,z,f(y,x,u)). f(x,y,f(z,x,u))=f(x,z,f(x,y,u)). f(x,f(y,z,u),f(w,x,y))=f(w,x,f(y,u,f(x,y,z))). f(x,y,f(z,u,f(y,z,w)))=f(y,f(z,w,u),f(x,y,z)). f(x,y,f(x,z,f(u,x,w)))=f(u,x,f(x,y,f(x,w,z))). f(x,y,f(y,z,f(y,u,w)))=f(y,z,f(y,w,f(x,y,u))). f(x,f(x,y,z),u)=f(x,z,f(y,x,u)). f(x,y,f(z,x,u))=f(x,u,f(x,z,y)). f(x,y,f(x,z,u))=f(x,u,f(z,x,y)). 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)))). 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))). f(x,y,f(x,z,u))=f(x,u,f(x,y,z)). f(x,y,f(x,z,u))=f(x,z,f(x,u,y)). f(x,f(y,z,x),f(z,x,u))=f(y,x,f(z,x,u)). f(x,f(x,y,z),u)=f(x,y,f(x,z,u)). f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(u,y,x))). f(x,y,f(x,z,u))=f(x,u,f(x,z,y)). f(x,f(y,x,z),f(z,u,w))=f(y,x,f(z,w,f(u,z,x))). f(x,y,f(z,u,f(w,z,y)))=f(y,f(x,y,z),f(z,w,u)). f(x,f(x,y,z),f(x,u,w))=f(x,u,f(x,y,f(x,z,w))). f(x,y,f(x,f(y,z,u),w))=f(x,w,f(y,z,f(x,y,u))). f(x,y,f(z,u,f(x,z,w)))=f(x,z,f(x,f(z,u,w),y)). f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,w,f(x,z,u))). f(x,f(x,y,z),f(z,u,w))=f(x,y,f(z,u,f(x,z,w))). f(x,f(x,y,z),f(u,z,w))=f(x,y,f(u,z,f(x,z,w))). f(x,y,f(y,z,f(u,x,y)))=f(u,y,f(x,y,z)). f(x,f(y,x,z),f(y,x,u))=f(y,x,f(x,z,u)). f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(x,y,w))). f(x,y,f(z,u,f(y,z,w)))=f(y,f(y,z,x),f(z,u,w)). f(x,y,f(x,f(z,u,w),f(w5,x,z)))=f(w5,x,f(x,y,f(z,w,f(x,z,u)))). f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(u,w5,w),f(x,y,u))). f(x,f(x,y,z),f(u,y,w))=f(x,z,f(y,w,f(x,y,u))). f(x,f(x,y,z),f(x,u,w))=f(x,y,f(x,u,f(x,w,z))). f(x,y,f(x,z,f(x,u,w)))=f(x,z,f(x,w,f(x,u,y))). f(x,y,f(z,u,f(z,w,y)))=f(y,f(y,z,x),f(z,u,w)). f(x,f(x,y,z),f(y,u,w))=f(z,x,f(y,u,f(y,w,x))). f(x,f(x,y,z),f(y,u,w))=f(x,z,f(y,u,f(x,y,w))). f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(w5,f(y,z,f(y,u,w)),f(y,x,f(y,z,f(y,u,w)))). f(x,f(y,z,f(y,u,w)),f(y,w5,f(y,z,f(y,u,w))))=f(w5,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,x)))). f(x,f(x,y,z),f(u,f(x,y,z),y))=f(x,y,z). f(x,f(x,y,z),f(y,u,f(x,y,z)))=f(x,y,z). f(x,f(x,f(x,y,z),y),f(y,u,z))=f(x,y,z). f(x,f(x,y,z),f(y,u,z))=f(x,y,z). f(x,f(x,y,z),f(y,z,u))=f(x,y,z). f(x,f(x,y,z),f(u,y,z))=f(x,y,z). f(x,f(x,y,z),f(y,u,z))=f(y,z,x). f(x,y,f(y,z,f(x,z,u)))=f(x,y,z). f(x,y,f(x,z,f(u,y,z)))=f(x,y,z). f(x,f(y,z,u),f(x,z,u))=f(x,z,u). f(x,f(x,y,f(z,u,w)),f(y,u,w))=f(x,y,f(z,u,w)). f(x,f(y,x,z),f(z,u,y))=f(z,y,x). f(x,y,f(z,u,f(z,x,y)))=f(z,x,y). f(x,f(x,y,f(z,u,w)),f(z,w,y))=f(x,y,f(z,u,w)). f(x,f(y,z,f(u,z,w)),f(x,z,w))=f(x,z,w). f(x,y,f(x,z,f(u,z,y)))=f(x,z,y). f(x,f(y,z,u),f(x,z,u))=f(z,u,x). f(x,y,f(z,x,f(u,z,y)))=f(z,x,y). f(x,f(y,z,u),f(z,u,x))=f(z,u,x). f(x,f(y,z,u),f(y,z,x))=f(y,z,x). f(x,y,f(z,y,f(u,z,x)))=f(z,x,y). f(x,f(y,z,u),f(u,f(y,z,w),x))=f(u,f(y,z,w),x). f(x,f(y,z,f(z,u,w)),f(z,u,x))=f(z,u,x). 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)). f(x,y,f(y,z,f(z,u,f(x,z,w))))=f(x,y,z). f(x,f(y,z,u),f(y,x,z))=f(y,x,z). f(x,f(y,z,u),f(u,x,f(w,y,z)))=f(u,x,f(w,y,z)). f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(w,f(x,y,z),f(x,y,z)). f(x,f(x,y,f(z,u,w)),f(z,y,u))=f(x,y,f(z,u,w)). f(x,y,f(x,z,f(z,y,u)))=f(x,y,z). f(x,f(y,z,u),f(x,w,f(y,u,f(y,z,w))))=f(x,w,f(y,z,u)). f(f(x,y,z),f(x,z,u),f(w,y,f(x,y,z)))=f(x,y,z). f(f(x,y,f(z,y,u)),f(z,y,u),f(z,u,w))=f(z,y,u). f(f(x,y,f(z,y,u)),f(y,z,u),f(z,u,w))=f(z,y,u). f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(z,y,u). f(f(x,y,f(y,z,u)),f(y,z,u),f(z,u,w))=f(y,z,u). f(f(x,y,f(x,z,u)),f(x,z,u),f(z,u,w))=f(x,z,u). f(x,f(y,z,u),f(x,u,f(y,w,z)))=f(x,u,f(y,w,z)). f(f(x,y,z),f(x,y,u),f(x,y,w))=f(w,f(x,y,z),f(x,y,u)). f(f(x,y,z),f(x,y,u),f(x,y,w))=f(z,f(x,y,u),f(x,y,w)). f(x,f(y,z,u),f(y,z,w))=f(u,f(y,z,w),f(y,z,x)). f(x,f(y,z,u),f(x,z,f(u,w,y)))=f(x,z,f(u,w,y)). 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(x,f(y,z,u),f(z,w5,f(y,z,u)))). 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))))). f(x,f(y,z,u),f(x,w,f(y,z,w)))=f(x,f(y,z,u),w). f(x,f(y,z,u),f(x,u,f(w,y,z)))=f(x,u,f(w,y,z)). f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(y,z,f(x,y,z)),f(y,z,u)). f(f(x,y,z),f(y,z,u),f(y,z,w))=f(w,f(x,y,z),f(y,z,u)). f(f(x,y,z),f(y,z,u),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). f(f(x,y,z),f(u,y,z),f(y,z,w))=f(u,f(x,y,z),f(y,z,w)). f(x,f(y,z,u),f(z,u,w))=f(w,f(y,z,u),f(z,u,x)). f(f(x,y,z),f(u,y,z),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). f(f(x,y,z),f(y,z,u),f(y,z,w))=f(x,f(u,y,z),f(y,z,w)). f(x,f(y,z,u),f(z,u,w))=f(y,f(w,z,u),f(z,u,x)). f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(z,u,y)). f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(z,u,x)). f(x,f(y,z,u),f(u,y,w))=f(w,f(z,u,y),f(u,y,x)). f(x,f(y,z,u),f(z,u,w))=f(w,f(x,z,u),f(y,z,u)). f(x,f(y,z,u),f(w,z,u))=f(y,f(w,z,u),f(z,u,x)). f(x,f(y,z,u),f(y,u,w))=f(w,f(z,u,y),f(u,y,x)). f(x,f(y,z,u),f(z,u,w))=f(w,f(u,y,z),f(u,z,x)). f(x,f(y,z,u),f(u,y,w))=f(w,f(y,z,u),f(y,u,x)). f(x,f(y,z,u),f(y,u,w))=f(w,f(y,z,u),f(u,y,x)). f(x,f(y,z,u),f(y,u,w))=f(w,f(y,z,u),f(x,y,u)). f(x,f(y,z,u),f(w,y,u))=f(w,f(y,z,u),f(y,u,x)). f(x,f(y,z,u),f(z,w,u))=f(y,f(z,w,u),f(z,u,x)). f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,f(x,w,f(y,z,u)),f(y,w,z)). f(x,f(y,z,u),f(w,z,f(x,w,y)))=f(x,w,f(y,z,u)). f(x,f(y,z,f(x,y,u)),f(u,z,w))=f(x,y,f(u,z,w)). f(x,f(y,f(z,u,w),f(x,y,w5)),f(w5,u,w))=f(x,y,f(w5,f(z,u,w),f(w5,u,w))). f(x,f(y,f(x,y,z),f(u,w,w5)),f(z,w,w5))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(z,f(u,w,w5),f(z,w,w5))). f(x,f(y,f(x,y,z),f(u,w,w5)),f(w,w5,z))=f(x,y,f(w,w5,z)). f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(x,z,y))). f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,f(z,y,x))). f(x,y,f(z,y,f(u,f(y,u,y),f(w,x,z))))=f(z,y,f(y,u,x)). f(x,y,f(z,y,f(u,y,f(w,x,z))))=f(z,y,f(y,u,x)). f(x,y,f(z,y,f(u,y,f(z,x,w))))=f(z,y,f(y,u,x)). f(x,y,f(z,u,f(z,x,f(z,y,w))))=f(z,x,y). f(x,y,f(z,u,f(u,x,f(u,y,w))))=f(u,x,y). f(x,f(y,z,u),f(w,z,f(x,w,u)))=f(x,w,f(y,z,u)). f(x,y,f(z,y,f(x,z,u)))=f(x,z,y). f(x,y,f(z,u,f(x,z,y)))=f(x,z,y). f(x,y,f(x,f(y,z,u),f(w,z,u)))=f(x,y,f(w,z,u)). f(x,f(x,y,z),f(u,z,f(x,u,w)))=f(x,y,f(x,u,z)). f(x,f(x,y,f(x,z,u)),f(y,u,w))=f(x,z,f(x,y,u)). f(x,y,f(y,z,f(y,u,w)))=f(y,f(x,y,u),f(y,z,w)). f(x,f(y,x,z),f(x,u,w))=f(y,x,f(x,u,f(x,z,w))). f(x,y,f(x,z,f(u,x,y)))=f(u,x,f(x,y,z)). f(x,y,f(x,z,f(x,y,u)))=f(u,x,f(x,y,z)). f(x,y,f(x,f(x,y,z),u))=f(z,x,f(x,y,u)). f(x,y,f(x,f(x,y,z),u))=f(x,z,f(x,y,u)). f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,z,w). f(f(x,y,f(y,z,f(y,u,w))),f(y,z,w),f(z,w,w5))=f(y,w,z). f(x,f(y,z,u),f(z,u,f(w,y,f(y,z,f(y,w5,u)))))=f(y,u,z). f(x,y,f(z,u,f(u,x,f(u,w,y))))=f(u,y,x). f(x,y,f(z,z,u))=f(z,y,x). f(f(x,y,z),u,w)=f(w,u,f(x,z,y)). f(x,f(y,z,u),w)=f(x,w,f(y,u,z)). f(x,y,f(z,y,f(y,u,f(z,x,w))))=f(z,y,f(y,u,x)). f(x,y,f(z,x,f(x,u,f(z,y,w))))=f(z,x,f(x,u,y)). f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(u,w5,w),f(y,u,x))). f(x,y,f(x,f(z,u,w),f(x,z,w5)))=f(w5,x,f(x,y,f(z,w,f(x,z,u)))). f(x,y,f(x,f(x,z,u),f(z,w,w5)))=f(u,x,f(x,y,f(z,w5,f(x,z,w)))). f(x,y,f(y,z,f(u,w,f(y,u,w5))))=f(y,z,f(y,f(y,u,x),f(u,w5,w))). f(x,y,f(x,z,f(u,w,f(x,u,w5))))=f(x,z,f(x,f(x,u,y),f(u,w5,w))). f(x,y,f(x,f(x,z,u),f(z,w,w5)))=f(x,u,f(x,y,f(z,w5,f(x,z,w)))). f(x,y,f(x,f(z,u,f(x,w,y)),f(w,u,f(x,w,z))))=f(x,f(x,w,y),f(w,z,u)). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(y,z,f(z,y,u)),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). f(x,f(y,x,f(x,y,z)),f(y,x,f(x,f(x,y,z),f(u,w,f(y,x,f(x,y,z))))))=f(u,f(y,x,f(x,y,z)),f(x,w,f(x,f(x,y,f(y,x,f(x,y,z))),f(y,z,x)))). f(x,y,f(x,z,f(u,w,f(x,z,y))))=f(x,f(x,z,y),f(z,u,w)). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(y,z,f(z,y,u)))))). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,z,f(z,f(z,y,u),f(x,w,f(z,y,u))))). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,y,f(z,f(z,y,u),f(x,w,f(z,y,u))))). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,u,f(z,y,f(x,w,f(z,y,u))))). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(z,f(z,y,u),f(y,x,w))). f(x,f(y,z,f(z,y,u)),f(z,w,f(z,f(z,y,f(y,z,f(z,y,u))),f(y,u,z))))=f(z,f(z,y,u),f(y,x,w)). f(x,f(y,z,u),f(y,w,f(y,f(y,z,f(z,y,f(y,z,u))),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). f(x,f(y,z,u),f(y,w,f(y,f(y,z,u),f(z,u,y))))=f(y,f(y,z,u),f(z,x,w)). f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(z,x,w)). f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(y,z,u),f(w,z,x)). f(x,f(y,z,u),f(y,w,f(y,z,u)))=f(y,f(w,z,x),f(y,z,u)). f(x,f(y,z,u),f(y,z,f(w,y,u)))=f(y,f(w,z,x),f(y,z,u)). f(x,f(y,z,f(y,u,w)),f(y,z,f(y,w,f(y,u,w5))))=f(y,f(x,z,w5),f(y,z,f(y,u,w))). f(x,f(y,z,f(x,u,w)),f(y,z,f(w,y,f(x,u,w))))=f(y,z,f(x,u,w)). f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(z,y,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). f(x,f(y,z,u),f(z,u,f(z,f(y,z,f(y,u,w)),f(y,z,w5))))=f(z,f(x,u,w5),f(z,u,f(z,y,f(y,z,f(y,u,w))))). f(x,f(y,z,u),f(z,u,f(z,f(y,z,w),f(y,z,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5))))). f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(x,z,f(w,x,f(x,u,f(w,z,w5))))). f(x,f(y,z,u),f(z,u,f(y,z,f(z,w,f(y,u,w5)))))=f(z,f(x,u,w),f(z,u,f(z,y,f(y,z,f(y,u,w5))))). f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,u,z))). f(x,f(y,z,u),f(x,z,f(x,w,f(w,x,f(w,z,w5)))))=f(y,f(w,x,z),f(w,x,f(x,z,u))). f(x,f(y,z,u),f(y,z,f(z,u,w)))=f(z,f(x,u,w),f(y,z,u)). f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,u,w),f(y,z,u)). f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(x,u,w),f(y,z,u)). f(f(x,y,z),f(x,y,u),f(y,u,w))=f(y,f(w,u,z),f(x,y,u)). f(x,f(y,z,u),f(z,u,f(y,z,w)))=f(z,f(w,u,x),f(y,z,u)). f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(z,u,y)). f(x,f(y,z,u),f(z,u,f(w,y,z)))=f(z,f(w,u,x),f(y,z,u)). f(x,f(y,z,u),f(y,u,f(z,u,w)))=f(u,f(x,y,w),f(y,z,u)). f(f(x,y,z),f(y,z,u),f(z,u,w))=f(z,f(x,u,w),f(y,z,u)). f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,z,u)). f(f(x,y,z),f(u,w,y),f(w,x,y))=f(y,f(u,w,z),f(w,x,y)). f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(y,u,z)). f(f(x,y,z),f(y,u,z),f(u,z,w))=f(z,f(x,y,w),f(u,z,y)). f(f(x,y,z),f(y,z,u),f(z,u,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(u,z,y),f(z,y,w)). f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(u,z,y),f(y,z,w)). f(f(x,y,z),f(y,z,u),f(u,z,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). f(f(x,y,z),f(u,y,z),f(u,z,w))=f(f(x,u,z),f(u,y,z),f(y,z,w)). f(f(x,y,z),f(y,u,z),f(u,z,w))=f(f(x,u,z),f(y,u,z),f(y,z,w)). f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,y,z)). f(f(x,y,z),f(u,y,z),f(u,z,w))=f(z,f(x,u,w),f(u,z,y)). f(f(x,y,z),f(u,z,y),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). f(f(x,y,z),f(u,y,z),f(u,y,w))=f(y,f(x,u,w),f(u,y,z)). f(f(x,y,z),f(u,w,y),f(u,y,z))=f(y,f(x,u,w),f(u,y,z)). f(f(x,y,f(z,y,f(z,f(x,z,u),w))),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). f(x,f(y,z,u),f(u,w,f(y,z,u)))=f(u,f(x,y,w),f(y,u,z)). f(x,f(y,z,u),f(z,w,f(y,u,z)))=f(z,f(x,y,w),f(y,z,u)). f(x,f(y,z,u),f(z,w,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). f(x,f(y,z,u),f(w,z,f(y,z,u)))=f(z,f(x,y,w),f(y,z,u)). f(f(x,y,f(z,y,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). f(f(x,y,f(y,z,f(z,u,f(x,z,w)))),f(z,w,y),f(z,y,f(z,y,f(z,f(x,z,w),u))))=f(z,y,f(x,z,w)). f(f(x,y,z),f(z,u,y),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,f(x,z,u),w))))=f(z,y,f(x,z,u)). f(f(x,y,z),f(y,z,u),f(z,y,f(z,y,f(z,w,f(x,z,u)))))=f(z,y,f(x,z,u)). f(f(x,y,z),f(y,z,u),f(y,z,f(z,w,f(x,z,u))))=f(z,y,f(x,z,u)). f(f(x,y,f(z,x,u)),f(z,w,x),f(w,x,u))=f(x,w,f(z,x,u)). f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(z,y,f(x,z,u)). f(f(x,y,z),f(y,z,u),f(z,w,f(x,z,u)))=f(y,z,f(x,z,u)). f(f(x,y,f(z,x,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(z,w5,x),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(z,w5,x),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(w5,x,u),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(f(x,z,w5),f(x,u,w5),w6)),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(z,w5,x),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(w5,x,u),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(w,f(x,z,w5),f(w6,f(x,z,w5),f(x,u,w5))),f(f(x,z,w5),f(x,u,w5),f(x,y,f(z,x,u))))=f(w5,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(x,z,w),f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w)))=f(w,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(z,x,u)). f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(w,x,f(x,z,u)). f(f(x,y,f(x,z,u)),f(x,z,w),f(x,u,w))=f(x,w,f(x,z,u)). f(f(x,f(y,z,u),f(u,x,f(u,y,z))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). f(f(x,f(y,z,u),f(u,x,f(y,z,u))),f(u,y,w),f(u,z,w))=f(u,w,f(u,y,z)). f(f(x,y,f(z,u,y)),f(y,z,w),f(y,u,w))=f(y,w,f(y,z,u)). f(f(x,y,f(z,u,y)),f(z,y,w),f(y,u,w))=f(y,w,f(y,z,u)). f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(y,z,u)). f(f(x,y,f(z,u,y)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). f(f(x,y,f(z,y,u)),f(z,y,w),f(u,y,w))=f(y,w,f(z,u,y)). f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,u,y)). f(f(x,y,f(z,y,u)),f(z,y,w),f(y,u,w))=f(y,w,f(z,y,u)). f(f(x,f(x,y,z),f(u,y,z)),f(y,z,w),f(z,f(u,y,x),w))=f(z,w,f(y,z,f(u,y,x))). f(f(x,y,z),f(y,z,u),f(z,f(w,y,x),u))=f(z,u,f(y,z,f(w,y,x))). f(f(x,y,z),f(y,z,u),f(z,f(x,w,y),u))=f(z,u,f(y,z,f(w,y,x))). f(f(x,y,z),f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(y,z,f(w,y,x))). f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(u,w,y))). f(x,f(y,z,f(y,u,w)),f(w,x,z))=f(x,z,f(w,x,f(y,u,w))). f(x,f(y,z,f(x,u,w)),f(y,f(x,z,f(x,u,w)),f(w,y,z)))=f(y,z,f(x,u,w)). f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(w,y,z))))=f(y,z,f(x,u,w)). f(x,f(y,z,f(x,u,w)),f(x,f(w,y,z),f(y,f(x,u,w),f(y,z,f(w,y,z)))))=f(y,z,f(x,u,w)). f(x,f(y,z,u),f(z,u,f(x,w,y)))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(u,f(x,w,y),f(z,u,f(w5,z,f(x,w,y)))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(u,f(x,y,f(w,w5,f(x,w,y))),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(u,f(y,f(w,w5,f(x,w,y)),x),f(z,u,f(w6,z,f(x,w,y)))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(x,f(z,u,f(w,z,f(x,w,y))),f(u,f(w,z,f(x,w,y)),f(y,z,u))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(x,f(u,f(w,z,f(x,w,y)),f(y,z,u)),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(x,f(f(y,z,u),u,f(w,z,f(x,w,y))),f(z,u,f(w,z,f(x,w,y)))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(z,u,f(w,z,f(x,w,y))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(z,f(x,w,y),f(w,z,u)))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(x,f(w,z,u),f(y,z,f(w,z,u))))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(w,z,u))=f(z,u,f(x,w,y)). f(x,f(y,z,u),f(w,z,u))=f(z,u,f(w,x,y)). f(x,f(y,z,u),f(z,u,f(w,w5,f(w,z,u))))=f(z,u,f(w,x,y)). f(f(x,y,f(x,z,u)),f(w,z,u),f(w5,z,u))=f(z,u,f(x,w,w5)). f(f(x,y,z),f(u,y,z),f(w,y,z))=f(y,z,f(x,u,w)). $F. end_of_list. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 349 clauses generated 1316511 para_from generated 526491 para_into generated 790020 demod & eval rewrites 0 clauses wt,lit,sk delete 1312122 tautologies deleted 0 clauses forward subsumed 3967 cl not subsumed due to ancestor_subsume 60 (subsumed by sos) 1639 unit deletions 0 factor simplifications 0 clauses kept 422 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 88 usable size 311 sos size 30 demodulators size 0 passive size 1 hot size 0 Kbytes malloced 3906 ----------- times (seconds) ----------- user CPU time 21.91 (0 hr, 0 min, 21 sec) system CPU time 0.01 (0 hr, 0 min, 0 sec) wall-clock time 44 (0 hr, 0 min, 44 sec) That finishes the proof of the theorem. Process 24611 finished Sat Jul 23 00:35:02 2005