set(para_into).
set(para_from).
set(order_eq).
set(ancestor_subsume).
assign(max_weight,20).
%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,300000).
%  assign(max_seconds,30).
assign(pick_given_ratio,2).
  
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").
end_of_list.

list(passive).
f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b # label("neg SING_2").
end_of_list.

list(demodulators).
%  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(f(x,x),f(x,x))=x,junk).
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 hints from temp.ba.mirror.wos.out4ab 23-step proof.
f(x,f(f(f(y,z),f(f(y,z),f(f(y,f(y,x)),y))),f(y,z)))=f(f(y,f(y,x)),y).
f(f(f(f(x,f(x,y)),x),z),f(f(y,f(y,z)),y))=z.
f(x,f(f(y,f(y,f(f(x,f(x,x)),x))),y))=f(f(x,f(x,x)),x).
f(x,f(f(f(f(x,y),x),x),f(f(x,y),x)))=f(f(x,f(x,x)),x).
f(f(x,f(x,x)),x)=f(x,x).
f(f(f(x,y),x),f(x,x))=x.
f(f(x,x),f(f(x,f(x,x)),x))=x.
f(x,f(f(y,f(y,f(x,x))),y))=f(x,x).
f(f(x,x),f(f(x,f(x,f(f(y,f(y,f(x,x))),y))),x))=x.
f(f(x,f(x,f(f(x,y),f(x,y)))),x)=f(x,y).
f(f(x,y),f(x,x))=x.
f(x,f(f(x,y),f(x,y)))=f(x,y).
f(f(x,f(x,y)),x)=f(x,y).
f(f(f(x,y),z),f(x,z))=z.
f(f(x,y),f(f(x,z),y))=y.
f(f(x,x),f(x,y))=x.
f(f(f(f(x,x),y),f(x,z)),x)=f(x,z).
f(x,y)=f(y,x).
f(f(f(x,y),z),f(z,x))=z.
f(f(x,y),f(y,f(z,x)))=y.
f(x,f(f(x,y),x))=f(x,y).
f(x,f(f(y,x),x))=f(x,y).
f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y.
%  f(f(f(x,y),z),f(f(x,f(x,z)),x))=z   # label("SING_1").
%  f(f(a,f(f(b,a),a)),f(b,f(c,a)))!=b   # label("neg SING_2").
%  f(f(x,y),f(f(f(f(z,u),x),f(f(f(z,u),x),y)),f(f(z,u),x)))=y   # label("SING_1 => SING_2 3(91)").
%  f(x,f(f(f(y,z),f(f(y,z),f(f(y,f(y,x)),y))),f(y,z)))=f(f(y,f(y,x)),y)   # label("SING_1 => SING_2 4(92)").
%  f(f(x,y),f(f(f(z,x),f(f(z,x),y)),f(z,x)))=y   # label("SING_1 => SING_2 3(91)").
%  f(f(f(f(x,f(x,y)),x),z),f(f(y,f(y,z)),y))=z   # label("SING_1 => SING_2 6(96)").
%  f(x,f(f(y,f(y,f(f(x,f(x,x)),x))),y))=f(f(x,f(x,x)),x)   # label("SING_1 => SING_2 7(99)").
%  f(x,f(f(f(f(x,y),x),x),f(f(x,y),x)))=f(f(x,f(x,x)),x)   # label("SING_1 => SING_2 9(104)").
%  f(f(x,f(x,x)),x)=f(x,x)   # label("SING_1 => SING_2 10(113)").
%  f(f(f(x,y),x),f(x,x))=x   # label("SING_1 => SING_2 11(134)").
%  f(f(x,x),f(x,x))=x   # label("SING_1 => SING_2 12(152)").
%  f(x,f(f(y,f(y,f(x,x))),y))=f(x,x)   # label("SING_1 => SING_2 13(159)").
%  f(f(f(f(x,x),y),f(x,x)),x)=f(x,x)   # label("SING_1 => SING_2 14(166)").
%  f(f(x,x),f(f(y,f(y,x)),y))=x   # label("SING_1 => SING_2 16(220)").
%  f(f(x,x),f(f(x,f(x,f(f(y,f(y,f(x,x))),y))),x))=x.
%  f(f(x,f(x,f(f(x,y),f(x,y)))),x)=f(x,y)   # label("SING_1 => SING_2 17(286)").
%  f(f(x,y),f(x,x))=x   # label("SING_1 => SING_2 12(152)").
%  f(x,f(f(x,y),f(x,y)))=f(x,y)   # label("SING_1 => SING_2 19(379)").
%  f(f(x,f(x,y)),x)=f(x,y)   # label("SING_1 => SING_2 10(113)").
%  f(f(x,x),f(y,x))=x   # label("SING_1 => SING_2 12(152)").
%  f(f(x,y),f(f(z,x),y))=y   # label("SING_1 => SING_2 35(1742)").
%  f(f(f(x,y),z),f(x,z))=z   # label("SING_1 => SING_2 11(134)").
%  f(f(x,x),f(x,y))=x   # label("SING_1 => SING_2 12(152)").
%  f(x,f(f(y,z),f(y,x)))=f(y,x)   # label("SING_1 => SING_2 20(380)").
%  f(x,f(x,f(y,x)))=f(y,x)   # label("SING_1 => SING_2 36(1753)").
%  f(f(x,y),y)=f(y,f(x,y))   # label("SING_1 => SING_2 28(1131)").
%  f(x,f(f(y,x),x))=f(y,x)   # label("SING_1 => SING_2 39(2197)").
%  f(x,y)=f(y,x)   # label("SING_1 => SING_2 28(1131)").
%  f(f(x,y),f(y,f(z,x)))=y   # label("SING_1 => SING_2 46(4961)").
%  f(f(x,y),f(x,f(z,y)))=x   # label("SING_1 => SING_2 44(4634)").
%  f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y   # label("SING_1 => SING_2 48(5227)").
end_of_list.
