set(anl_eq).

% We'll keep only clauses that subsume hints.

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

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).

clear(sigint_interact).
clear(detailed_history).

list(usable).
x = x.
end_of_list.

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

assign(max_proofs, 3).

list(passive).
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,f(A,B))) != f(A,B) | $Ans(OM_SS).
end_of_list.

list(hints2).
f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z)))=y.
f(x,f(f(x,y),f(f(z,f(f(f(x,y),f(x,y)),z)),z)))=f(x,y).
f(f(f(f(x,y),f(y,z)),u),f(y,f(f(v,f(f(y,y),v)),v)))=y.
f(f(x,y),f(x,f(f(z,f(f(x,x),z)),z)))=x.
f(f(x,y),f(x,f(f(z,f(f(x,x),z)),z)))=x.
f(f(x,y),f(y,f(f(z,f(f(y,y),z)),z)))=y.
f(f(x,y),f(y,y))=y.
f(f(x,y),f(y,y))=y.
f(f(x,y),f(y,f(f(y,y),z)))=y.
f(f(x,y),f(x,x))=x.
f(f(f(f(x,y),f(y,z)),u),f(y,y))=y.
f(x,f(f(x,y),f(x,y)))=f(x,y).
f(x,f(f(y,x),f(f(z,f(f(f(y,x),f(y,x)),z)),z)))=f(y,x).
f(x,f(f(y,f(f(x,x),y)),y))=f(x,x).
f(x,f(f(y,x),f(y,x)))=f(y,x).
f(f(f(x,x),y),x)=f(x,x).
f(f(x,f(f(x,x),y)),f(x,f(f(x,x),y)))=x.
f(x,f(f(x,x),y))=f(x,x).
f(f(x,x),f(x,y))=x.
f(f(f(x,y),f(x,y)),x)=f(x,y).
f(f(x,x),f(y,x))=x.
f(f(f(x,f(f(y,x),z)),u),f(f(y,x),f(y,x)))=f(y,x).
f(f(f(f(x,y),f(x,z)),u),f(x,x))=x.
f(f(f(x,f(f(x,y),z)),u),f(f(x,y),f(x,y)))=f(x,y).
f(f(f(f(x,y),f(z,y)),u),f(y,y))=y.
f(f(x,f(f(y,z),f(z,u))),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(x,f(f(f(y,x),x),f(y,x)))=f(x,x).
f(f(x,f(f(y,z),f(y,u))),f(y,y))=y.
f(f(x,f(f(y,z),f(u,z))),f(z,z))=z.
f(f(x,f(y,f(f(z,y),u))),f(f(z,y),f(z,y)))=f(z,y).
f(f(f(x,y),y),f(x,y))=y.
f(f(f(x,y),x),f(x,y))=x.
f(f(x,f(x,y)),x)=f(x,y).
f(f(x,y),f(x,f(x,y)))=x.
f(f(f(x,y),z),f(f(y,x),f(y,x)))=f(y,x).
f(f(x,y),f(y,x))=f(f(y,x),f(y,x)).
f(x,f(f(y,x),f(x,y)))=f(y,x).
f(x,y)=f(y,x).
f(f(f(f(x,y),f(y,x)),z),f(x,y))=f(f(y,x),f(x,y)).
f(x,f(x,f(x,y)))=f(x,y).
f(f(x,f(y,x)),f(y,x))=x.
f(f(f(x,y),z),f(f(y,x),f(x,y)))=f(y,x).
f(f(f(x,y),z),f(f(x,y),f(y,x)))=f(y,x).
f(f(x,f(x,y)),f(y,x))=x.
f(f(f(x,y),f(y,x)),f(f(y,x),z))=f(y,x).
f(f(f(x,y),z),f(f(x,f(f(y,u),f(y,v))),f(x,f(f(y,u),f(y,v)))))=f(x,f(f(y,u),f(y,v))).
f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,u),f(z,v)),y)))=f(f(f(z,u),f(z,v)),y).
f(f(x,y),f(y,f(f(x,y),f(y,z))))=f(f(x,y),f(y,z)).
f(f(x,y),f(y,f(f(x,y),f(z,y))))=f(f(x,y),f(y,z)).
f(f(x,y),f(y,z))=f(f(x,y),f(z,y)).
f(x,f(f(y,x),z))=f(x,f(z,f(y,x))).
f(x,f(y,z))=f(x,f(z,y)).
f(f(x,y),z)=f(z,f(y,x)).
f(x,f(y,z))=f(f(z,y),x).
f(x,f(f(y,z),u))=f(f(f(z,y),u),x).
f(f(x,y),f(z,u))=f(f(y,x),f(u,z)).
f(f(f(x,y),z),u)=f(u,f(f(y,x),z)).
f(f(f(f(x,y),z),u),f(f(f(y,x),z),f(f(x,y),z)))=f(z,f(x,y)).
f(f(f(f(x,y),f(z,u)),v),f(f(f(y,x),f(u,z)),f(f(z,u),f(x,y))))=f(f(z,u),f(x,y)).
f(f(f(f(x,f(y,f(f(z,y),u))),z),v),f(f(z,y),f(z,y)))=f(z,y).
f(f(x,f(f(f(y,f(f(z,y),u)),v),z)),f(f(z,y),f(z,y)))=f(z,y).
f(f(x,f(y,z)),f(f(f(f(z,u),f(z,v)),y),f(f(f(z,v),f(z,u)),y)))=f(f(f(z,v),f(z,u)),y).
f(f(f(f(f(x,y),f(x,z)),u),f(f(f(x,z),f(x,y)),u)),f(f(u,x),v))=f(f(f(x,z),f(x,y)),u).
f(f(f(x,f(f(y,x),z)),f(x,u)),y)=f(y,x).
f(f(f(x,y),f(x,z)),f(f(u,y),f(v,y)))=f(f(f(u,y),f(v,y)),x).
f(f(f(x,y),f(z,y)),f(f(u,v),f(u,y)))=f(f(f(x,y),f(z,y)),u).
f(f(f(x,y),f(z,y)),f(f(u,y),f(u,v)))=f(f(f(x,y),f(z,y)),u).
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,y)),z)=f(x,f(f(z,y),f(z,y))).
f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
end_of_list.
