%  set(auto).
%  set(knuth_bendix).
set(para_from).
set(para_into).
set(hyper_res).
%  set(ur_res).

assign(max_weight, 60).
assign(max_distinct_vars, 12).
assign(bsub_hint_wt, 10).
assign(equiv_hint_wt, 10).
assign(pick_given_ratio, -1).
assign(heat, 2).

set(order_eq).
%  set(dynamic_demod).
set(print_proof_as_hints).
  set(print_lists_at_end). 

assign(max_proofs,5).
%assign(max_weight,60). 
assign(max_mem,4800000).
%  assign(max_seconds, 600).
%  assign(max_given,90).
%  assign(max_distinct_vars,12).

set(ancestor_subsume).
set(back_sub).
%  set(back_unit_deletion).

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

assign(demod_limit,500).
%  assign(pick_given_ratio,-1).
%  assign(bsub_hint_wt,10).
%  assign(heat,2).
set(keep_hint_subsumers).
set(input_sos_first).
%  set(sos_queue).
%  set(very_verbose).
clear(process_input).  
  
weight_list(pick_and_purge).
  weight(f(e,x)=x,0).
  weight(f(x,f(x,f(x,f(x,x))))=e,0).
  weight(f(f(x,y),z)=f(x,f(y,z)),0).
  weight(junk,1000).
end_of_list.

list(usable).
  (x = x).
%  f(x,f(x,f(x,f(x,x))))=e.
%  f(e,x)=x.
%  f(x,e)=x.
%  f(e,f(e,x))=x.
end_of_list.


list(sos).
%  (f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(z,f(z,f(z,z)))))) = y).
  (f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = y).
  (f(f(a,b),c) != f(a,f(b,c))) | (f(e,a) != a) | (f(a,f(a,f(a,f(a,a)))) != e) | $ANS(all).
end_of_list.

list(hot).
  (f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = y).
end_of_list.

list(passive).
%  (f(f(b,f(b,f(b,f(b,b)))),a) != a) | $ANS(L_ident).
%  (f(a,f(a,f(a,f(a,a)))) != f(b,f(b,f(b,f(b,b))))) | $ANS(X5).
%  (f(a,f(b,f(b,f(b,f(b,b))))) != a) | $ANS(R_ident).
    
  (f(f(a,b),c) != f(a,f(b,c))) | $ANS(assoc).
  (f(a,f(a,f(a,f(a,a)))) != e) |  $ANS(exp5).
  (f(e,a) != a) | $ANS(lid).
  (f(a,e) != a) | $ANS(rid).
%  (f(e,f(e,a)) != a) | $ANS(demod).
end_of_list.
  

list(demodulators).
  EQ(f(x,f(f(x,f(x,f(f(x,y),u))),f(e,f(u,f(u,f(u,u)))))),junk). 
  
%  EQ(f(e,f(e,f(e,e)))=f(e,e),junk).
  EQ(f(f(e,f(e,f(f(e,f(e,e)),x))),f(e,f(x,f(x,f(x,x)))))=e,junk).

  EQ(f(f(x,f(x,f(f(x,f(x,y)),z))),f(e,f(z,f(z,f(z,z)))))=f(x,f(x,f(f(x,f(x,f(y,u))),f(e,f(u,f(u,f(u,u))))))),junk).
  EQ(f(e,f(e,e))=e,junk).

end_of_list.

list(hints).
f(a,e)!=a.
f(a,f(a,f(a,f(a,a))))!=e.
f(e,a)!=a.
f(e,a)!=a|f(a,f(a,f(a,f(a,a))))!=e.
f(e,e)=e.
f(e,f(e,e))=e.
f(e,f(e,f(e,e)))=f(e,f(e,e)).
f(e,f(e,f(e,f(e,f(e,e)))))=e.
f(e,f(e,f(e,f(x,f(x,x)))))=f(x,f(x,x)).
f(e,f(e,f(e,x)))=x.
f(e,f(e,f(f(e,f(e,e)),e)))=e.
f(e,f(e,f(f(e,f(e,f(x,y))),f(e,f(y,f(y,f(y,y)))))))=f(e,x).
f(e,f(e,f(f(x,f(x,x)),f(x,f(x,x)))))=f(f(x,f(x,x)),f(x,f(x,x))).
f(e,f(e,f(f(x,y),f(e,f(y,f(y,f(y,y)))))))=f(e,x).
f(e,f(e,f(f(x,y),f(y,f(y,f(y,y))))))=f(e,x).
f(e,f(e,x))=x.
f(e,x)=x.
f(f(a,b),c)!=f(a,f(b,c)).
f(f(a,b),c)!=f(a,f(b,c))|f(e,a)!=a|f(a,f(a,f(a,f(a,a))))!=e.
f(f(x,f(e,f(e,f(e,f(e,f(y,f(y,f(y,y)))))))),y)=x.
f(f(x,f(x,f(f(x,f(x,f(x,y))),z))),f(e,f(z,f(z,f(z,z)))))=y.
f(f(x,f(x,f(f(x,f(x,y)),z))),f(e,f(z,f(z,f(z,z)))))=f(x,f(x,f(f(x,f(x,f(y,u))),f(e,f(u,f(u,f(u,u))))))).
f(f(x,f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(u,f(u,f(u,u)))))))),u)=f(x,f(y,z)).
f(f(x,f(x,f(x,f(f(x,f(x,y)),f(e,f(z,f(z,f(z,z)))))))),z)=y.
f(f(x,f(x,f(x,f(f(x,y),f(e,f(z,f(z,f(z,z)))))))),z)=f(x,f(x,f(f(x,f(x,f(y,u))),f(e,f(u,f(u,f(u,u))))))).
f(f(x,f(x,f(x,x))),x)=e.
f(f(x,f(x,x)),f(x,f(x,x)))=f(e,f(e,x)).
f(f(x,f(x,x)),f(x,f(x,x)))=x.
f(f(x,f(x,y)),f(x,f(x,y)))=f(x,f(x,f(y,f(x,f(x,y))))).
f(f(x,y),f(y,f(y,f(y,y))))=f(e,x).
f(f(x,y),f(y,f(y,f(y,y))))=x.
f(f(x,y),z)=f(x,f(y,z)).
f(x,e)=x.
f(x,f(e,f(e,e)))=x.
f(x,f(f(x,f(x,f(x,f(f(x,y),f(e,f(z,f(z,f(z,z)))))))),z))=y.
f(x,f(f(x,y),z))=f(x,f(x,f(y,z))).
f(x,f(f(y,f(y,f(y,y))),f(f(y,f(y,f(y,y))),f(f(y,f(y,f(y,y))),f(y,f(y,f(y,y)))))))=f(x,y).
f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z)))))))=y.
f(x,f(x,f(f(x,f(x,f(x,e))),y)))=f(z,f(z,f(f(z,f(z,z)),y))).
f(x,f(x,f(f(x,f(x,f(x,f(y,f(e,f(z,f(z,f(z,z)))))))),z)))=y.
f(x,f(x,f(f(x,f(x,f(x,y))),y)))=f(y,f(y,e)).
f(x,f(x,f(f(x,f(x,f(x,y))),y)))=f(y,y).
f(x,f(x,f(f(x,f(x,f(x,y))),z)))=f(u,f(u,f(f(u,f(u,f(u,y))),z))).
f(x,f(x,f(f(x,f(x,x)),y)))=f(e,f(e,f(e,y))).
f(x,f(x,f(x,f(f(x,f(x,f(y,z))),f(e,f(z,f(z,f(z,z))))))))=y.
f(x,f(x,f(x,f(x,f(x,e)))))=e.
f(x,f(x,f(x,f(x,f(x,f(y,e))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u))))))),f(f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u))))))),f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u)))))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u))))))),f(f(w,f(w,f(f(w,f(w,f(w,u))),f(e,f(u,f(u,f(u,u))))))),f(w,f(w,f(f(w,f(w,f(w,u))),f(e,f(u,f(u,f(u,u)))))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u))))))),f(w,f(w,f(f(w,f(w,f(w,u))),f(e,f(u,f(u,f(u,u))))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u)))))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))),f(v,f(v,f(f(v,f(v,f(v,u))),f(e,f(u,f(u,f(u,u)))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,f(y,f(e,f(z,f(z,f(f(z,f(z,f(z,u))),f(e,f(u,f(u,f(u,u))))))))))))))=y.
f(x,f(x,f(x,f(x,f(x,y)))))=y.
f(x,f(x,f(x,f(x,x))))=e.
f(x,f(x,f(y,f(e,f(f(e,f(z,f(z,f(z,z)))),f(f(e,f(z,f(z,f(z,z)))),f(f(e,f(z,f(z,f(z,z)))),f(e,f(z,f(z,f(z,z)))))))))))=f(x,f(f(x,y),z)).
f(x,f(x,f(y,f(e,f(f(z,f(z,f(z,z))),f(f(e,f(z,f(z,f(z,z)))),f(f(e,f(z,f(z,f(z,z)))),f(e,f(z,f(z,f(z,z)))))))))))=f(x,f(f(x,y),z)).
f(x,f(x,f(y,f(e,f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(f(e,f(z,f(z,f(z,z)))),f(e,f(z,f(z,f(z,z)))))))))))=f(x,f(f(x,y),z)).
f(x,f(x,f(y,f(e,f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(e,f(z,f(z,f(z,z)))))))))))=f(x,f(f(x,y),z)).
f(x,f(x,f(y,f(e,f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(z,f(z,f(z,z))))))))))=f(x,f(f(x,y),z)).
f(x,f(x,f(y,f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(f(z,f(z,f(z,z))),f(z,f(z,f(z,z)))))))))=f(x,f(f(x,y),z)).
f(x,f(y,f(y,f(f(y,f(y,f(y,z))),f(e,f(z,f(z,f(z,z))))))))=x.
end_of_list.



% end of fixed part