% This input file gets the strictly-forward demod-free proof (271 steps).

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).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).

% flatten out the f's
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).

   % majority
   f(x,x,y) = x.
   f(x,y,x) = x.
   f(y,x,x) = x.

   % commutativity
   f(x,y,z) = f(y,x,z).
   f(x,y,z) = f(x,z,y).
   f(x,y,z) = f(z,y,x).

   % associativity
   f(f(x,w,y),w,z) = f(x,w,f(y,w,z)).

end_of_list.

list(passive).

   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.

% hints from length 271 proof
list(hints2).

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)).

end_of_list.