set(hyper_res).
assign(max_weight,24).
assign(max_distinct_vars,5).
%assign(change_limit_after,500). 
%assign(new_max_weight,24).
set(prolog_style_variables).
assign(pick_given_ratio, 3).
assign(max_proofs, -1).
clear(print_kept).
set(ancestor_subsume).
assign(max_mem, 900000).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
clear(print_given).
clear(print_kept).
assign(heat,0).
% assign(dynamic_heat_weight, 1).
set(order_history).
set(input_sos_first).
%set(sos_queue).
% set(sos_stack).
assign(bsub_hint_wt, 1).
set(keep_hint_subsumers).

list(hints).
end_of_list.
 
weight_list(pick_and_purge).
% 24/11/5 proof
weight(t(i(i(i(i(A,B),i(C,B)),D),i(i(C,i(i(B,E),f)),D))),2).
weight(t(i(i(A,i(i(B,C),f)),i(i(i(A,B),D),i(E,D)))),2).
weight(t(i(i(i(i(i(A,B),i(i(f,C),f)),D),A),i(i(E,f),A))),2).
weight(t(i(i(i(i(i(i(A,B),i(C,B)),f),C),D),i(E,D))),2).
weight(t(i(i(i(i(A,f),B),C),i(i(i(B,D),i(i(f,E),f)),C))),2).
weight(t(i(i(A,i(i(B,C),f)),i(D,i(A,B)))),2).
weight(t(i(i(i(A,B),i(i(f,C),f)),i(D,A))),2).
weight(t(i(i(i(A,B),i(i(f,C),f)),i(i(A,D),i(E,D)))),2).
weight(t(i(i(i(A,i(i(B,i(i(C,D),f)),E)),C),i(B,C))),2).
weight(t(i(A,i(f,B))),2).
weight(t(i(i(i(A,B),C),i(B,C))),2).
weight(t(i(i(i(i(A,B),i(C,B)),D),i(A,D))),2).
weight(t(i(i(i(A,B),A),i(C,A))),2).
weight(t(i(f,A)),2).
weight(t(i(A,i(B,A))),2).
weight(t(i(A,i(i(i(i(i(B,C),D),i(E,D)),f),B))),2).
weight(t(i(i(i(i(i(A,B),C),i(D,C)),f),A)),2).
weight(t(i(i(A,B),i(i(i(A,C),f),B))),2).
weight(t(i(i(i(i(A,B),C),f),i(i(i(A,D),f),B))),2).
weight(t(i(i(i(i(i(A,B),A),C),f),i(D,A))),2).
weight(t(i(i(i(i(i(A,B),f),C),D),i(i(A,C),D))),2).
weight(t(i(A,i(i(i(B,C),B),B))),2).
weight(t(i(i(A,B),i(i(B,C),i(A,C)))),2).
weight(t(i(i(i(A,B),A),A)),2).
end_of_list.
 
list(sos).
t(i(i(i(i(A,i(i(B,C),f)),D),E),i(i(E,B),i(A,B)))) # label(A7).
end_of_list.

list(usable).
-t(A) | -t(i(A,B)) | t(B) # label(mp).

-t(i(i(x,y),i(i(y,z),i(x,z)))) |  -t(i(x,i(y,x))) | -t(i(i(i(x,y),x),x)) | -t(i(f,x)) # label(T1_T4).
end_of_list.

list(hot).
-t(A) | -t(i(A,B)) | t(B) # label(mp).
t(i(i(i(i(A,i(i(B,C),f)),D),E),i(i(E,B),i(A,B)))) # label(A7).
end_of_list.

list(demodulators).
(i(X,X) = junk).
(i(X,junk) = junk).
(i(junk,X) = junk).
(t(junk) = $T).
end_of_list.