set(para_from).
set(para_into).
set(order_eq).

% Keep clauses only if they subsume hints.

set(keep_hint_subsumers).
assign(bsub_hint_add_wt, -1000).
assign(max_weight, 0).
set(degrade_hints2).

clear(print_kept).

clear(sigint_interact).
clear(detailed_history).

list(usable).
x = x.
end_of_list.

list(sos).
f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x.  % MOL_Sh
end_of_list.

assign(max_proofs, 4).

list(passive).

% MOL 4-basis: { A_SS, B_SS, ONE_SS, MOD_SS }

f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))) | $Ans(A_SS).
f(f(A,A),f(A,B)) != A | $Ans(B_SS).
f(A,f(A,A)) != f(B,f(B,B)) | $Ans(ONE_SS).
f(A,f(B,f(A,f(C,C)))) != f(A,f(C,f(A,f(B,B)))) | $Ans(MOD_SS).

end_of_list.

list(hints2).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),f(f(f(y,y),z),f(f(f(f(f(y,y),z),z),y),f(y,u)))),y),f(y,v))))=y.
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),u),f(f(f(f(f(f(y,z),x),u),u),f(y,z)),z)))=f(y,z).
f(f(x,y),f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))))=f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))).
f(f(f(f(f(x,x),y),f(f(f(f(f(x,z),y),y),x),f(x,u))),f(z,x)),f(f(f(f(z,x),f(z,x)),v),f(f(f(f(x,v),v),f(z,x)),x)))=f(z,x).
f(f(x,y),f(y,y))=y.
f(f(x,y),f(f(f(y,y),z),y))=y.
f(f(x,f(y,y)),y)=f(y,y).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),x)))=f(y,x).
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),z)))=f(y,z).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u))))=f(y,x).
f(f(x,y),f(f(f(y,y),f(x,x)),f(f(f(x,f(x,x)),y),f(y,z))))=y.
f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x))=f(f(f(x,x),x),f(f(f(f(x,x),x),f(f(x,x),x)),x)).
f(f(x,y),f(f(z,f(y,y)),y))=y.
f(f(x,f(f(f(y,y),z),y)),y)=f(f(f(y,y),z),y).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(f(f(y,y),z),y)),f(f(f(y,y),z),y)),y),f(y,u))))=y.
f(f(x,f(y,y)),f(f(z,y),f(y,y)))=f(y,y).
f(f(f(x,x),y),x)=f(x,x).
f(f(x,y),f(x,x))=f(f(x,x),f(x,x)).
f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))))=x.
f(f(x,y),f(x,x))=x.
f(x,f(f(x,y),f(x,y)))=f(x,y).
f(x,f(f(y,x),f(y,x)))=f(y,x).
f(f(x,y),f(f(z,f(x,x)),x))=x.
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(f(f(y,z),x),f(f(y,z),x))),f(f(f(f(y,z),x),f(y,z)),z)))=f(y,z).
f(f(f(x,x),f(x,y)),f(f(f(f(x,y),f(x,y)),z),f(f(f(f(x,z),z),f(x,y)),f(f(x,y),u))))=f(x,y).
f(f(x,y),f(f(f(y,y),f(f(y,x),f(y,x))),f(f(f(y,x),y),f(y,z))))=y.
f(f(f(f(x,y),f(x,y)),x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))=x.
f(x,f(f(f(f(y,x),f(y,x)),z),f(y,x)))=f(y,x).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(u,y))))=y.
f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(y,x))))=x.
f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))),x))=f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))).
f(x,f(f(f(f(x,x),f(x,x)),f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x).
f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(x,f(f(x,x),y))))=f(x,x).
f(f(x,f(y,z)),f(f(f(f(y,z),f(y,z)),f(x,x)),f(f(f(x,f(x,x)),f(y,z)),y)))=f(y,z).
f(f(x,f(y,y)),f(f(y,z),f(f(f(f(f(f(y,y),x),z),z),f(y,y)),f(u,f(y,y)))))=f(y,y).
f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(f(x,x),y))))=f(x,x).
f(f(f(x,x),f(y,x)),f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x)))=f(y,x).
f(f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(x,f(f(x,x),y)))))=f(f(x,f(x,x)),f(x,f(f(x,x),y))).
f(f(x,f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,y),f(y,f(f(f(f(y,y),z),y),f(y,u))))=y.
f(f(x,y),f(y,f(f(y,y),f(y,z))))=y.
f(f(x,f(f(x,x),f(x,y))),f(x,f(f(x,x),f(x,y))))=x.
f(x,f(f(x,x),f(x,y)))=f(x,x).
f(f(x,x),f(x,f(f(x,x),y)))=f(f(x,x),f(x,x)).
f(f(x,y),f(f(f(x,y),f(x,y)),y))=f(f(x,y),f(x,y)).
f(f(x,y),f(f(f(x,y),f(x,y)),x))=f(f(x,y),f(x,y)).
f(f(x,x),f(x,f(f(x,x),y)))=x.
f(f(x,x),f(x,f(y,f(x,x))))=x.
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),x).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))),f(f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),y).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),f(f(x,x),f(x,x))),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))).
f(f(x,x),f(f(f(f(f(x,x),f(x,y)),f(f(x,x),f(x,y))),f(x,x)),f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x))))=f(f(x,x),f(x,y)).
f(x,f(f(x,f(x,x)),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x).
f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))))=f(x,x).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),f(f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))),f(x,x)))=f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))).
f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(x,x),x),f(f(x,x),x)),x))=f(f(f(x,x),x),f(f(x,x),x)).
f(f(f(f(x,x),x),f(f(x,x),x)),f(f(f(x,x),x),f(f(x,x),x)))=f(f(f(f(x,x),x),f(f(x,x),x)),x).
f(f(f(f(x,x),x),f(f(x,x),x)),x)=f(f(x,x),x).
f(f(f(f(x,x),f(x,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x).
f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x).
f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(f(f(x,x),f(f(x,x),x)),f(f(f(x,x),x),y))))=f(f(x,x),x).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),f(f(x,x),f(x,x))),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))).
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(f(f(f(x,x),x),f(x,f(y,f(x,x)))),x)))=f(x,f(y,f(x,x))).
f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x))=f(f(x,x),f(f(f(x,x),x),f(f(f(x,x),x),f(x,y)))).
f(f(f(f(x,x),x),f(f(f(x,x),x),f(x,y))),f(x,x))=x.
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x)=f(x,f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x))))).
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(y,f(x,x)))),x)=f(x,x).
f(f(f(x,f(x,x)),x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y))))=x.
f(f(x,x),f(f(f(x,x),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,x),f(x,y))))=x.
f(f(x,x),f(f(x,f(x,x)),f(f(x,x),f(x,y))))=x.
f(x,f(f(f(x,x),f(f(x,x),f(x,x))),f(f(f(x,x),f(x,x)),f(f(x,x),y))))=f(x,x).
f(x,f(f(f(x,x),x),f(f(f(x,x),f(x,x)),f(f(x,x),y))))=f(x,x).
f(x,f(f(f(x,x),x),f(x,f(f(x,x),y))))=f(x,x).
f(f(x,f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(f(f(f(f(x,f(x,x)),f(x,f(f(x,x),y))),f(f(x,f(x,x)),f(x,f(f(x,x),y)))),f(x,x)),x))=f(f(x,f(x,x)),f(x,f(f(x,x),y))).
f(f(x,f(x,x)),f(x,f(f(x,x),y)))=x.
f(f(x,f(x,x)),f(x,f(y,f(x,x))))=x.
f(f(f(x,x),x),f(f(x,x),f(y,f(f(x,x),f(x,x)))))=f(x,x).
f(f(f(x,x),x),f(f(x,x),f(y,x)))=f(x,x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),f(f(f(x,x),x),f(f(x,x),f(y,x))))),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),f(f(x,x),f(x,x))),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(f(f(x,x),x),f(f(x,x),x)),x),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(f(f(x,x),x),f(f(x,x),f(y,x))),f(f(x,x),x)),x)))=f(f(x,x),x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),f(f(f(x,x),x),f(f(f(x,x),f(f(x,x),x)),x)))=f(f(x,x),x).
f(f(f(f(x,x),f(y,x)),f(f(x,x),x)),x)=f(f(x,x),x).
f(f(f(x,x),f(x,x)),f(f(x,f(f(f(x,x),f(x,x)),f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x).
f(x,f(f(x,f(f(f(x,x),f(x,x)),f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x).
f(x,f(f(x,f(x,f(x,x))),f(f(f(f(x,x),f(x,x)),f(x,x)),f(y,f(x,x)))))=f(x,x).
f(x,f(f(x,f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(x,x)))))=f(x,x).
f(x,f(x,f(x,x)))=f(x,x).
f(f(x,x),f(f(x,x),x))=f(f(x,x),f(x,x)).
f(f(x,x),f(f(x,x),x))=x.
f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(f(f(x,x),x),y))))=f(f(x,x),x).
f(f(x,f(f(x,x),x)),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x).
f(f(x,y),f(f(f(y,f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),w),f(f(f(f(f(f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))),x),w),w),f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v))))))=f(f(z,y),f(f(f(y,y),u),f(f(f(f(f(y,z),u),u),y),f(y,v)))).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))),x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))))=f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w))))))=f(f(u,y),f(f(f(y,y),v),f(f(f(f(f(y,u),v),v),y),f(y,w)))).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w))))))=f(f(v,y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w)))).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(y,x),z),z),y),f(f(f(y,y),u),f(f(f(f(f(y,v),u),u),y),f(y,w))))))=y.
f(f(x,f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),f(f(x,x),f(x,f(f(x,x),y)))))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(x,x),f(f(f(f(f(f(x,x),x),f(x,f(f(x,x),y))),f(f(f(x,x),x),f(x,f(f(x,x),y)))),f(x,x)),x))=f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y))).
f(f(f(f(x,x),f(x,x)),f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x.
f(f(x,f(f(f(x,x),x),f(f(x,x),x))),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x.
f(f(f(x,x),x),f(f(f(f(x,x),x),f(x,x)),f(f(x,x),y)))=x.
f(f(f(x,x),x),f(x,f(f(x,x),y)))=x.
f(f(x,f(x,x)),f(f(x,x),f(f(f(x,x),f(x,x)),y)))=f(x,x).
f(f(f(x,x),x),f(x,f(y,f(x,x))))=x.
f(x,f(f(f(f(x,f(y,f(x,x))),f(x,f(y,f(x,x)))),x),f(x,x)))=f(x,f(y,f(x,x))).
f(f(x,f(x,x)),f(f(x,x),f(x,y)))=f(x,x).
f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),y))=f(f(x,y),f(x,y)).
f(f(f(x,y),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),x))=f(f(x,y),f(x,y)).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),y),f(f(f(x,y),f(x,y)),y)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),y).
f(f(f(x,y),f(x,y)),f(f(f(f(f(f(x,y),f(x,y)),x),f(f(f(x,y),f(x,y)),x)),f(f(x,y),f(x,y))),f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))))=f(f(f(x,y),f(x,y)),x).
f(x,f(y,f(x,x)))=f(x,x).
f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))=f(f(f(x,y),f(x,y)),y).
f(f(f(x,y),f(x,y)),y)=f(x,y).
f(f(f(x,y),f(x,y)),f(f(x,y),f(x,y)))=f(f(f(x,y),f(x,y)),x).
f(f(f(x,y),f(x,y)),x)=f(x,y).
f(f(x,x),f(f(f(x,x),f(x,y)),f(f(f(x,f(x,x)),f(f(x,x),f(x,y))),f(x,x))))=f(f(x,x),f(x,y)).
f(x,f(f(x,x),y))=f(x,x).
f(f(x,y),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u))))=x.
f(f(x,x),f(f(f(x,x),x),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x).
f(f(f(x,f(f(x,x),y)),z),x)=f(x,x).
f(f(x,x),f(f(f(x,x),f(x,y)),f(f(x,x),f(x,x))))=f(f(x,x),f(x,y)).
f(f(x,x),f(x,x))=f(f(x,x),f(x,y)).
f(f(x,x),f(x,y))=x.
f(f(x,x),f(y,x))=x.
f(f(x,y),f(y,f(f(f(f(f(y,x),f(y,z)),f(y,z)),y),f(u,y))))=y.
f(x,f(f(f(f(y,x),f(y,x)),f(x,x)),f(f(x,f(y,x)),x)))=f(y,x).
f(x,f(f(f(f(y,x),f(y,x)),z),f(f(f(f(x,z),z),f(y,x)),f(f(y,x),u))))=f(y,x).
f(f(x,y),f(y,f(f(f(f(f(y,x),f(z,y)),f(z,y)),y),f(u,y))))=y.
f(x,f(f(y,x),f(f(f(f(f(f(y,x),f(x,x)),f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(y,x).
f(f(x,y),f(f(f(f(y,x),f(y,z)),f(y,z)),y))=y.
f(x,f(f(f(f(f(y,x),f(x,x)),f(f(y,x),z)),f(f(y,x),z)),f(y,x)))=f(y,x).
f(x,f(f(f(f(f(x,y),f(x,x)),f(f(x,y),z)),f(f(x,y),z)),f(x,y)))=f(x,y).
f(f(x,y),f(f(f(f(x,f(f(x,y),f(x,y))),f(x,z)),f(x,z)),x))=x.
f(f(x,y),f(f(f(f(y,f(f(x,y),f(x,y))),f(y,z)),f(y,z)),y))=y.
f(f(x,y),f(f(f(f(y,x),f(z,y)),f(z,y)),y))=y.
f(f(x,y),f(f(f(f(x,f(f(x,y),f(x,y))),f(z,x)),f(z,x)),x))=x.
f(f(x,y),f(f(f(f(x,y),f(x,z)),f(x,z)),x))=x.
f(f(x,y),f(f(f(f(x,y),f(y,z)),f(y,z)),y))=y.
f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x))=x.
f(x,f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)))=f(y,x).
f(x,f(f(f(x,y),f(f(y,x),f(f(f(f(y,x),f(z,y)),f(z,y)),y))),f(y,x)))=f(y,x).
f(x,f(f(f(x,f(f(x,y),z)),f(f(x,y),z)),f(x,y)))=f(x,y).
f(x,f(f(f(x,x),f(f(x,y),f(f(f(f(x,y),f(z,x)),f(z,x)),x))),f(x,y)))=f(x,y).
f(x,f(f(y,x),f(f(f(f(x,y),y),f(y,x)),f(f(y,x),z))))=f(y,x).
f(x,f(f(f(x,y),y),f(y,x)))=f(y,x).
f(x,f(x,f(f(x,x),x)))=f(f(x,x),x).
f(f(x,x),x)=f(x,f(x,x)).
f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(f(x,x),x)))))=f(f(x,x),x).
f(f(f(x,f(x,x)),f(f(f(x,x),x),f(x,y))),f(x,x))=x.
f(f(x,x),f(f(x,f(x,x)),f(f(f(x,x),x),f(x,y))))=x.
f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))),f(x,x))=x.
f(f(x,x),f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,y))))=x.
f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x))))))=f(f(x,x),x).
f(f(x,x),f(f(x,f(x,x)),f(x,f(y,f(x,f(x,x))))))=f(x,f(x,x)).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(f(x,f(x,x)),x)))=f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))).
f(x,f(f(f(x,x),x),f(x,y)))=f(x,y).
f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(y,x).
f(x,f(f(y,x),f(f(f(f(x,f(f(y,x),z)),f(f(y,x),z)),f(y,x)),f(u,f(y,x)))))=f(x,f(f(f(x,x),x),f(y,x))).
f(x,f(f(f(x,x),x),f(y,x)))=f(y,x).
f(f(x,x),f(f(x,f(x,x)),f(y,f(x,x))))=f(y,f(x,x)).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))),f(x,x)))=f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x)))).
f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x))))=f(f(f(x,f(x,x)),f(x,f(x,x))),x).
f(f(x,f(x,x)),f(f(x,f(x,x)),f(x,f(x,x))))=f(x,f(x,x)).
f(f(f(x,f(x,x)),f(x,f(x,x))),f(f(x,f(x,x)),f(y,f(f(x,f(x,x)),f(x,f(x,x))))))=f(y,f(f(x,f(x,x)),f(x,f(x,x)))).
f(x,f(f(y,f(y,y)),f(y,f(y,y))))=f(y,f(y,y)).
f(f(x,f(x,x)),y)=f(y,y).
f(x,f(f(y,f(y,y)),f(z,x)))=f(z,x).
f(f(x,x),f(y,f(y,y)))=x.
f(x,f(y,f(y,y)))=f(x,x).
f(f(f(x,f(x,x)),f(y,z)),y)=f(y,z).
f(x,f(f(y,f(y,y)),f(x,z)))=f(x,z).
f(f(f(x,f(x,x)),y),f(y,z))=y.
f(x,f(y,f(f(z,f(z,z)),x)))=f(x,x).
f(f(x,y),f(f(z,f(z,z)),x))=x.
f(f(f(f(x,f(x,x)),y),z),y)=f(y,y).
f(f(x,x),f(f(x,f(x,x)),f(x,y)))=f(x,f(x,x)).
f(f(x,y),f(f(f(x,x),f(z,f(z,z))),f(f(f(f(f(x,y),f(x,y)),f(z,f(z,z))),x),f(x,u))))=x.
f(f(x,f(y,f(y,y))),f(z,f(z,z)))=x.
f(f(x,f(y,f(y,y))),f(z,x))=x.
f(f(x,f(y,f(y,y))),f(x,z))=x.
f(x,f(x,x))=f(y,f(y,y)).
f(x,f(x,x))=f(f(y,y),y).
f(f(x,y),f(f(z,f(z,z)),f(f(f(f(f(y,x),y),y),y),f(u,y))))=y.
f(x,f(x,f(x,y)))=f(x,y).
f(x,f(x,f(y,x)))=f(y,x).
f(f(x,y),f(f(x,y),y))=y.
f(f(x,y),f(f(x,y),x))=x.
f(f(x,x),f(f(x,y),f(x,y)))=f(x,f(x,x)).
f(f(x,f(y,y)),f(f(x,f(y,y)),f(x,f(y,y))))=f(f(f(x,f(y,y)),f(x,f(y,y))),y).
f(f(f(f(f(x,y),x),x),x),f(y,x))=x.
f(f(x,f(f(y,y),f(y,y))),f(f(x,f(f(y,y),f(y,y))),f(x,f(f(y,y),f(y,y)))))=f(f(f(x,y),f(x,f(f(y,y),f(y,y)))),f(y,y)).
f(f(x,y),f(x,f(f(f(f(f(x,y),f(x,y)),f(z,f(z,z))),x),f(x,u))))=x.
f(f(x,y),f(x,f(f(f(x,y),x),f(x,z))))=x.
f(f(x,f(f(y,y),f(y,y))),f(f(x,f(f(y,y),f(y,y))),f(x,f(f(y,y),f(y,y)))))=f(f(f(x,y),f(x,y)),f(y,y)).
f(f(f(x,y),f(x,y)),f(y,y))=f(z,f(z,z)).
f(x,f(f(y,f(y,y)),f(f(x,f(z,x)),x)))=f(z,x).
f(f(x,f(y,x)),x)=f(y,x).
f(f(f(x,f(x,x)),f(y,z)),y)=f(f(y,f(y,z)),y).
f(f(x,f(y,x)),f(x,f(f(y,x),f(x,z))))=x.
f(f(x,f(y,x)),f(y,x))=x.
f(f(x,f(x,y)),x)=f(x,y).
f(f(x,y),x)=f(x,f(x,y)).
f(f(x,y),y)=f(y,f(x,y)).
f(f(x,f(x,y)),f(x,y))=x.
f(f(f(x,y),x),x)=f(x,y).
f(x,f(f(y,f(x,y)),f(y,x)))=f(y,x).
f(f(x,y),f(f(f(y,y),f(f(y,x),z)),f(f(f(y,x),y),f(y,u))))=y.
f(f(f(x,y),x),f(y,x))=x.
f(f(x,y),f(f(z,f(z,z)),f(f(f(y,x),y),f(u,y))))=y.
f(f(f(x,f(x,f(x,y))),x),f(y,x))=x.
f(f(x,f(x,y)),f(y,x))=x.
f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(u,y))))=y.
f(f(x,y),f(f(z,f(z,z)),f(f(x,f(x,f(f(u,f(u,u)),f(x,y)))),f(v,x))))=x.
f(f(x,y),f(f(z,f(z,z)),f(f(y,f(y,x)),f(y,u))))=y.
f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(f(f(z,y),f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u)))),f(f(z,y),f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))))))=y.
f(f(x,x),f(f(f(x,x),y),f(f(f(x,x),x),f(x,z))))=x.
f(f(x,x),f(f(f(x,x),y),f(f(z,f(z,z)),f(x,u))))=x.
f(f(x,y),f(f(z,f(z,z)),f(f(x,f(x,y)),f(u,x))))=x.
f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,f(f(z,y),f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))))))=y.
f(f(f(x,f(x,x)),f(f(y,f(y,z)),f(y,u))),f(y,y))=y.
f(f(f(x,f(x,x)),f(f(y,z),f(z,u))),f(z,z))=z.
f(f(f(x,f(x,x)),f(f(y,z),f(u,z))),f(z,z))=z.
f(f(f(x,y),f(y,z)),f(f(x,y),f(y,z)))=f(y,f(f(x,y),f(y,z))).
f(f(f(x,f(x,x)),f(f(y,z),f(u,y))),f(y,y))=y.
f(f(f(x,y),f(z,x)),f(f(x,y),f(z,x)))=f(x,f(f(x,y),f(z,x))).
f(f(x,y),f(x,f(f(z,x),f(x,y))))=f(f(z,x),f(x,y)).
f(f(x,f(f(y,z),f(z,u))),f(z,f(f(y,z),f(z,u))))=f(f(y,z),f(z,u)).
f(x,f(f(x,y),f(f(z,f(x,y)),f(f(x,y),f(f(u,f(u,u)),f(f(x,f(x,y)),f(v,x)))))))=f(f(z,f(x,y)),f(f(x,y),f(f(u,f(u,u)),f(f(x,f(x,y)),f(v,x))))).
f(f(x,y),f(y,f(f(y,z),f(x,y))))=f(f(y,z),f(x,y)).
f(f(x,f(f(y,f(f(z,u),f(u,v))),f(u,f(f(z,u),f(u,v))))),f(u,f(f(z,u),f(u,v))))=f(f(z,u),f(u,v)).
f(f(x,f(y,z)),f(f(y,z),f(f(u,f(u,u)),f(f(y,f(y,z)),f(v,y)))))=f(y,f(f(y,z),f(f(x,f(y,z)),y))).
f(x,f(f(x,y),f(f(z,f(x,y)),x)))=f(f(z,f(x,y)),x).
f(f(f(x,f(x,y)),f(y,x)),y)=f(y,f(f(y,x),f(x,y))).
f(x,f(f(x,y),f(y,x)))=f(y,x).
f(f(x,y),f(x,y))=f(f(y,x),f(x,y)).
f(x,f(f(y,x),f(x,y)))=f(x,y).
f(f(f(x,y),f(y,x)),f(f(y,x),z))=f(y,x).
f(f(x,f(y,x)),f(x,y))=x.
f(f(f(x,y),y),f(y,x))=y.
f(x,y)=f(y,x).
f(f(x,y),f(f(f(y,y),z),f(f(f(f(f(x,y),z),z),y),f(y,u))))=y.
f(x,f(f(y,x),f(y,f(f(y,x),z))))=f(y,x).
f(f(f(x,y),f(y,x)),f(f(x,y),z))=f(y,x).
f(x,f(f(y,x),f(y,f(z,f(y,x)))))=f(y,x).
f(f(f(f(x,y),z),f(u,f(u,u))),f(y,x))=f(f(x,y),z).
f(x,f(f(y,z),f(z,x)))=f(z,x).
f(x,f(f(y,z),f(x,z)))=f(z,x).
f(x,f(y,f(x,f(z,y))))=f(f(z,y),x).
f(x,f(f(x,y),f(z,y)))=f(y,x).
f(x,f(f(x,f(y,z)),z))=f(f(y,z),x).
f(f(f(x,y),f(z,y)),x)=f(y,x).
f(f(f(x,f(y,z)),z),x)=f(f(y,z),x).
f(f(f(x,f(x,x)),y),z)=f(z,f(y,y)).
f(x,f(y,f(x,f(z,y))))=f(x,f(z,y)).
f(f(x,f(f(y,f(y,y)),f(z,u))),f(z,z))=z.
f(f(f(f(x,y),z),y),z)=f(f(x,y),z).
f(f(f(x,f(y,z)),z),x)=f(f(z,y),x).
f(f(x,f(y,f(y,y))),z)=f(z,f(x,x)).
f(f(f(x,f(x,x)),y),z)=f(f(y,y),z).
f(x,f(f(y,f(z,f(z,z))),f(y,u)))=f(x,f(f(y,u),f(x,y))).
f(f(x,f(y,f(z,x))),y)=f(y,f(z,x)).
f(f(x,f(y,f(z,x))),y)=f(f(x,z),y).
f(x,f(y,z))=f(f(z,y),x).
f(f(x,y),z)=f(z,f(y,x)).
f(x,f(y,f(z,u)))=f(f(y,f(u,z)),x).
f(f(f(f(x,f(x,x)),y),z),u)=f(u,f(z,f(y,y))).
f(x,f(y,f(z,f(u,f(u,u)))))=f(f(y,f(z,z)),x).
f(x,f(y,z))=f(x,f(z,y)).
f(x,f(f(y,x),f(y,z)))=f(y,x).
f(f(f(x,y),f(x,y)),f(z,f(y,x)))=f(x,y).
f(f(x,f(y,z)),u)=f(u,f(x,f(z,y))).
f(f(f(x,y),z),u)=f(u,f(z,f(y,x))).
f(f(x,f(y,z)),u)=f(u,f(f(z,y),x)).
f(x,f(f(f(y,z),x),f(u,f(z,y))))=f(f(y,z),x).
f(f(f(x,f(y,z)),u),v)=f(v,f(f(x,f(z,y)),u)).
f(f(x,f(f(y,z),f(z,u))),f(z,z))=z.
f(f(x,f(y,y)),f(f(z,y),f(z,y)))=f(z,y).
f(f(x,f(f(y,z),f(y,u))),f(y,y))=y.
f(f(f(f(x,y),f(z,y)),u),f(y,y))=y.
f(f(x,x),f(y,f(f(z,x),f(u,x))))=x.
f(f(f(x,f(y,z)),f(x,f(y,z))),f(u,f(f(z,y),f(v,f(x,f(y,z))))))=f(x,f(y,z)).
f(f(f(x,x),y),f(f(z,x),f(z,x)))=f(z,x).
f(x,f(f(f(f(y,y),z),x),f(u,y)))=f(f(f(y,y),z),x).
f(f(f(f(x,f(f(y,z),f(y,u))),f(y,y)),f(v,f(v,v))),f(f(f(y,z),f(y,u)),x))=y.
f(f(f(x,x),y),f(f(x,z),f(x,z)))=f(x,z).
f(x,f(f(f(y,y),z),f(f(y,u),x)))=f(f(y,u),x).
f(f(f(f(x,x),y),f(f(f(x,x),y),f(f(x,z),f(x,z)))),f(x,z))=f(f(x,x),y).
f(x,f(f(y,z),f(x,y)))=f(x,y).
f(f(f(x,y),x),f(f(f(y,x),z),x))=f(f(f(x,y),x),f(y,x)).
f(x,f(f(x,y),f(y,z)))=f(x,y).
f(f(f(x,y),f(y,z)),x)=f(x,y).
f(f(f(f(x,y),z),f(z,u)),f(y,x))=f(f(x,y),z).
f(f(f(x,y),x),f(f(f(y,x),z),x))=x.
f(f(f(f(x,x),y),f(x,z)),f(x,z))=f(f(x,x),y).
f(f(x,f(f(y,x),f(x,z))),f(u,f(f(z,x),f(v,f(f(y,x),f(x,z))))))=f(f(y,x),f(x,z)).
f(f(x,f(y,f(y,y))),f(f(f(x,z),f(x,u)),v))=x.
f(f(x,f(f(f(f(f(y,x),z),z),x),f(x,y))),f(u,x))=f(f(f(f(f(y,x),z),z),x),f(x,y)).
f(f(f(f(f(x,y),z),z),y),f(y,x))=y.
f(f(f(x,f(x,f(y,z))),z),f(z,y))=z.
f(f(x,f(y,f(y,f(z,x)))),f(x,z))=x.
f(f(f(x,f(x,f(y,z))),z),f(y,z))=z.
f(f(x,y),f(f(z,f(z,f(x,y))),y))=y.
f(f(f(x,f(f(y,z),x)),y),f(z,y))=y.
f(x,f(f(y,f(y,f(f(x,f(z,f(z,f(u,x)))),f(x,u)))),f(x,u)))=f(x,u).
f(f(x,y),f(f(z,f(f(y,x),z)),y))=y.
f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),f(f(x,y),f(f(u,f(f(y,x),u)),y))))=y.
f(x,f(f(y,f(y,x)),f(x,z)))=f(x,z).
f(f(x,y),f(f(z,f(f(u,f(f(y,x),u)),y)),y))=y.
f(f(x,f(f(y,f(f(z,f(x,x)),y)),z)),z)=f(z,z).
f(f(f(f(x,f(x,f(y,f(z,z)))),y),z),y)=f(y,y).
f(f(f(x,f(f(y,f(z,z)),x)),y),z)=f(f(y,y),z).
f(f(f(x,f(x,f(y,f(z,z)))),y),z)=f(f(y,y),z).
f(f(f(x,f(f(y,f(z,z)),x)),f(f(y,f(z,z)),x)),z)=f(f(f(f(y,f(z,z)),x),f(f(y,f(z,z)),x)),z).
f(f(x,f(x,f(y,y))),y)=f(f(x,x),y).
f(f(x,f(f(f(y,f(y,y)),z),x)),z)=f(f(x,x),z).
f(f(f(f(f(f(x,x),y),f(x,x)),f(x,x)),f(f(y,f(x,x)),z)),x)=f(f(f(f(y,f(x,x)),z),f(f(y,f(x,x)),z)),x).
f(f(f(f(x,f(y,y)),z),f(f(x,f(y,y)),z)),y)=f(z,y).
f(f(f(f(x,f(y,y)),z),f(f(x,f(y,y)),z)),y)=f(f(f(f(y,y),x),f(f(x,f(y,y)),z)),y).
f(f(f(f(x,x),y),f(f(y,f(x,x)),z)),x)=f(z,x).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x)=f(z,x).
f(f(f(f(x,x),y),f(z,f(y,f(x,x)))),x)=f(f(f(z,f(y,f(x,x))),f(z,u)),x).
f(f(f(x,f(y,f(z,z))),f(x,u)),z)=f(x,z).
f(f(f(x,f(y,z)),f(x,u)),f(z,z))=f(x,f(z,z)).
f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(x,f(f(u,y),f(v,y))).
f(f(f(x,y),f(x,f(f(z,z),u))),z)=f(x,z).
f(f(f(x,y),f(x,f(z,u))),f(z,z))=f(x,f(z,z)).
f(f(x,x),f(f(y,z),f(z,f(u,x))))=f(z,f(x,x)).
f(f(x,x),f(f(f(y,x),f(z,u)),z))=f(f(z,u),f(x,x)).
f(f(x,x),f(f(y,z),f(z,f(u,x))))=f(f(x,x),z).
f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),f(f(z,u),f(f(v,f(x,x)),u)))=f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),u).
f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(u,f(f(z,y),f(x,y))).
f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
f(f(f(x,f(y,f(y,y))),f(x,f(y,f(y,y)))),z)=f(x,f(f(u,z),f(f(v,f(x,x)),z))).
f(x,f(f(y,z),f(f(u,f(x,x)),z)))=f(x,z).
f(f(f(x,y),f(x,z)),f(f(u,v),f(x,v)))=f(f(f(x,y),f(x,z)),v).
f(f(f(x,y),f(x,f(f(x,z),u))),z)=f(x,f(f(x,z),f(x,z))).
f(f(f(x,y),f(x,f(f(x,z),u))),z)=f(z,x).
f(f(x,f(x,y)),f(y,f(f(y,x),z)))=f(f(x,x),f(y,f(f(y,x),z))).
f(x,f(f(y,y),f(x,f(f(x,y),z))))=f(x,f(f(x,y),z)).
f(x,f(f(y,y),f(f(f(x,y),z),x)))=f(x,f(f(x,y),z)).
f(x,f(f(x,y),f(z,z)))=f(x,f(f(x,z),f(x,y))).
f(x,f(f(x,f(y,y)),f(x,z)))=f(x,f(f(x,z),y)).
f(x,f(f(x,f(y,y)),f(x,z)))=f(x,f(y,f(x,z))).
f(x,f(f(f(f(y,f(y,y)),z),x),f(x,u)))=f(x,f(z,f(x,u))).
f(x,f(f(f(f(y,f(y,y)),z),x),f(x,f(u,u))))=f(x,f(u,f(x,f(z,z)))).
f(x,f(y,f(x,f(z,z))))=f(x,f(z,f(x,f(y,y)))).
end_of_list.
