set(para_into).
set(para_from).
set(order_eq).
%  set(ancestor_subsume).
assign(max_weight,60).
%assign(change_limit_after,50).
%assign(new_max_weight,25).
set(keep_hint_subsumers).
set(input_sos_first).
assign(bsub_hint_add_wt,-1024).
clear(print_kept).  
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
assign(max_proofs,-1).
assign(max_mem,440000).
assign(report,3600).
assign(max_seconds,240).
assign(pick_given_ratio,3).
  
weight_list(pick_and_purge).
weight(junk,1000).
end_of_list.

list(usable).
x=x.
end_of_list.

list(sos).
%  f(f(f(x,y),z),f(f(x,f(x,z)),x))=z # label("SING_1").
%  f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y.
%  f(f(f(x,y),z),f(x,f(f(x,z),x)))=z.
f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y.
end_of_list.

list(passive).
%  f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2").
%  f(f(f(a,b),c),f(a,f(f(a,c),a)))!=c | $ANS(SING_3).
%  f(f(f(a,f(b,a)),a),f(b,f(c,a)))!=b | $ANS(SING_4).
f(f(f(a,b),c),f(f(a,f(a,c)),a))!=c | $ANS(SING_1).
end_of_list.

list(demodulators).
EQ(f(f(f(x,f(y,x)),x),f(y,y))=y,junk).
EQ(f(f(x,f(f(y,f(x,y)),y)),f(x,f(z,f(f(y,f(x,y)),y))))=x,junk).
EQ(f(x,f(f(f(x,f(x,x)),x),f(y,f(x,f(x,x)))))=f(f(x,f(x,x)),x),junk).
EQ(f(f(f(x,f(y,x)),x),f(y,f(x,f(f(z,f(x,z)),z))))=y,junk).
EQ(f(f(f(f(x,f(y,z)),f(u,f(x,f(y,z)))),f(x,f(y,z))),f(u,x))=u,junk).
EQ(f(f(x,f(x,y)),x)=f(x,y),junk).
%  Following are to block various single axioms, in search of a circle of pure proofs.
%  EQ(f(f(f(x,y),z),f(f(x,f(x,z)),x))=z,junk).
EQ(f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y,junk).
EQ(f(f(f(x,y),z),f(x,f(f(x,z),x)))=z,junk).
%  EQ(f(f(f(x,f(y,x)),x),f(y,f(z,x)))=y,junk).
%  Following to shoorten the proof of the second single axiom from the first, within a pure proof.
%  EQ(f(x,f(x,f(y,x)))=f(y,x),junk).
%  Following are to shorten the proof that deduces the three Sheffer.
%  EQ(f(f(x,y),f(y,f(x,z)))=y,junk).
%  EQ(f(f(x,f(y,f(z,x))),y)=f(y,f(z,x)),junk).
%  EQ(f(f(x,f(x,x)),x)=f(x,x),junk).
%  EQ(f(f(f(x,y),y),f(x,y))=y,junk).
%  EQ(f(f(x,f(y,y)),y)=f(y,y),junk).
%  EQ(f(f(x,f(y,f(z,y))),f(x,f(y,f(z,u))))=f(f(x,f(y,f(z,y))),f(x,z)),junk).
%  EQ(f(f(f(x,y),x),f(x,f(z,y)))=f(f(x,f(z,y)),f(x,f(z,y))),junk).
%  EQ(f(f(f(x,y),z),f(z,y))=z,junk).
%  EQ(f(x,f(f(f(y,z),f(f(y,z),f(f(z,f(z,x)),z))),f(y,z)))=f(f(z,f(z,x)),z),junk).
%  EQ(f(x,f(y,f(x,f(z,y))))=f(x,f(z,y)),junk).
%  EQ(f(f(f(x,f(x,x)),x),f(f(y,f(y,x)),y))=x,junk).
%  EQ(f(f(x,y),f(f(f(f(z,f(z,x)),z),f(f(f(z,f(z,x)),z),y)),f(f(z,f(z,x)),z)))=y,junk).
%  EQ(f(x,f(f(x,y),f(z,f(x,f(u,y)))))=f(x,y),junk).
(f(x,junk) = junk).
(f(junk,x) = junk).
end_of_list.

list(hints).
%  Following 71 hints from wos
f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z)))))=f(f(z,f(x,z)),z).
f(f(x,f(f(y,f(x,y)),y)),f(x,f(z,f(f(y,f(x,y)),y))))=x.
f(f(f(f(x,y),f(f(f(y,f(z,y)),y),f(x,y))),f(x,y)),z)=f(f(y,f(z,y)),y).
f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(z,f(f(f(y,f(x,y)),y),z)),z)))=x.
f(f(f(x,f(y,x)),x),f(y,f(f(z,f(x,z)),z)))=y.
f(x,f(f(f(x,f(x,x)),x),f(y,f(x,f(x,x)))))=f(f(x,f(x,x)),x).
f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),x))=f(f(z,f(x,z)),z).
f(x,f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x).
f(x,f(f(x,f(f(f(x,f(x,x)),x),x)),x))=f(f(x,f(x,x)),x).
f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))=x.
f(f(f(x,f(f(f(x,f(x,x)),x),x)),x),x)=f(f(x,f(x,x)),x).
f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),x)=f(f(x,f(x,x)),x).
f(f(f(f(f(x,f(x,x)),x),f(y,f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(y,x))=y.
f(f(f(f(f(x,f(x,x)),x),x),f(x,f(f(f(x,f(x,x)),x),x))),f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x).
f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x))=f(f(x,f(x,x)),x).
f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),f(z,x))=z.
f(f(x,f(f(f(y,z),f(x,f(y,z))),f(y,z))),f(x,f(f(f(x,y),x),f(x,y))))=x.
f(f(f(x,f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),x)),x),z)=f(f(f(x,y),f(z,f(x,y))),f(x,y)).
f(f(f(f(x,f(x,x)),x),f(f(f(x,y),f(f(f(x,f(x,x)),x),f(x,y))),f(x,y))),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x)))=f(f(x,f(x,x)),x).
f(f(f(x,f(x,x)),x),f(x,f(f(y,f(f(f(f(x,f(x,x)),x),x),y)),y)))=x.
f(f(f(f(x,f(x,x)),x),f(f(f(x,y),f(f(f(x,f(x,x)),x),f(x,y))),f(x,y))),x)=f(f(x,f(x,x)),x).
f(f(x,f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x))=x.
f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),x))=f(x,f(f(x,f(x,x)),x)).
f(f(f(f(x,f(x,x)),x),x),x)=f(f(x,f(x,x)),x).
f(f(f(x,f(f(x,f(x,x)),x)),x),f(f(f(f(x,f(x,x)),x),x),f(y,x)))=f(f(f(x,f(x,x)),x),x).
f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x))))=x.
f(f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),f(x,f(f(f(f(x,f(x,x)),x),x),f(f(x,f(f(x,f(x,x)),x)),x)))))),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(x,f(x,x)),x)),x)),f(f(x,f(x,x)),x))=f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x))=f(f(x,f(f(x,f(x,x)),x)),f(f(x,f(x,x)),x)).
f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x))=x.
f(f(x,f(x,x)),x)=f(x,x).
f(f(x,f(f(x,f(x,x)),x)),x)=f(x,x).
f(f(f(x,f(x,x)),x),f(x,x))=x.
f(f(x,x),f(x,f(y,x)))=x.
f(f(f(x,f(y,x)),x),f(y,f(x,f(x,x))))=y.
f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),y)=f(y,y).
f(f(x,x),f(x,x))=x.
f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),f(y,f(y,y)))=f(f(y,f(f(y,f(y,y)),y)),y).
f(f(f(x,f(x,x)),x),f(f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)),f(x,f(x,x))))=f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)).
f(f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y)),f(y,f(y,y)))=f(y,y).
f(f(x,x),f(f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)),f(x,f(x,x))))=f(f(f(y,x),f(f(x,x),f(y,x))),f(y,x)).
f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y))=f(f(y,y),f(y,y)).
f(f(f(x,y),f(f(y,y),f(x,y))),f(x,y))=y.
f(x,f(f(x,x),y))=f(x,x).
f(f(x,x),f(x,y))=f(f(x,x),f(x,x)).
f(f(f(x,f(y,x)),x),f(y,y))=y.
f(f(f(x,f(f(y,y),x)),x),y)=f(y,y).
f(f(x,x),f(x,y))=x.
f(f(f(x,f(x,x)),x),f(x,y))=x.
f(f(f(x,f(f(f(f(x,y),x),f(x,y)),x)),x),f(x,x))=f(f(f(x,y),f(f(x,x),f(x,y))),f(x,y)).
f(f(f(f(x,y),x),f(x,y)),x)=f(x,x).
f(f(f(x,f(f(f(f(x,y),x),f(x,y)),x)),x),f(x,x))=f(f(f(x,y),x),f(x,y)).
f(f(f(x,f(x,x)),x),f(x,x))=f(f(f(x,y),x),f(x,y)).
f(f(f(x,y),x),f(x,y))=x.
f(x,f(f(y,x),f(f(x,x),f(y,x))))=f(y,x).
f(f(x,x),f(y,x))=x.
f(f(f(x,y),y),f(x,y))=y.
f(f(x,f(y,x)),f(f(f(y,x),x),f(y,x)))=f(y,x).
f(f(x,f(y,x)),x)=f(y,x).
f(f(x,f(f(x,f(y,x)),x)),x)=f(y,x).
f(f(f(x,f(y,x)),x),f(y,f(x,z)))=y.
f(f(x,y),f(x,f(z,y)))=x.
f(x,f(f(f(x,y),x),f(z,f(x,y))))=f(f(x,y),x).
f(f(x,f(y,x)),x)=f(x,y).
f(f(f(x,y),z),f(z,x))=z.
f(f(x,f(x,y)),x)=f(y,x).
f(f(f(x,y),z),f(f(x,f(x,z)),x))=z.
end_of_list.