set(hyper_res).
set(prolog_style_variables).
clear(print_kept).  
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
clear(print_given).
%set(ancestor_subsume).
assign(max_weight, 0).
%assign(max_distinct_vars, 4).
%assign(pick_given_ratio, 1).
%assign(max_mem, 28000).
set(order_history).
set(input_sos_first).
assign(bsub_hint_wt, 1).
set(keep_hint_subsumers).

list(hints).
% 74/24/4 proof
p(i(f(i(A,B),i(B,C)),i(A,C))).
p(i(i(i(i(A,B),i(C,B)),D),i(i(C,A),D))).
p(i(i(i(i(A,B),B),C),i(i(i(B,A),A),C))).
p(i(i(i(A,B),C),i(i(i(B,A),i(A,B)),C))).
p(i(i(i(A,B),C),i(f(i(A,D),i(D,B)),C))).
p(i(i(A,i(B,C)),i(i(D,B),i(A,i(D,C))))).
p(i(i(A,A),i(A,A))).
p(i(i(A,i(B,C)),i(i(i(C,B),B),i(A,C)))).
p(i(i(i(i(i(A,B),B),C),D),i(i(i(i(B,A),A),C),D))).
p(i(i(i(i(A,B),i(C,B)),i(C,B)),i(i(A,C),i(A,B)))).
p(i(f(i(i(A,B),C),i(C,i(B,A))),i(B,A))).
p(i(f(i(i(A,B),C),i(C,B)),i(i(B,A),A))).
p(i(i(A,i(i(B,C),C)),i(i(i(i(C,B),B),D),i(A,D)))).
p(i(i(A,B),i(i(i(C,B),i(B,C)),i(A,C)))).
p(i(i(A,i(i(B,C),i(C,B))),i(i(i(C,B),D),i(A,D)))).
p(i(A,A)).
p(i(i(A,i(i(B,C),C)),i(i(D,i(C,B)),i(A,i(D,B))))).
p(i(i(i(i(i(A,B),B),i(C,A)),D),i(i(C,i(B,A)),D))).
p(i(i(i(i(A,i(B,C)),i(B,D)),i(B,D)),i(i(A,i(D,C)),i(A,i(B,C))))).
p(i(i(i(A,B),C),i(i(C,i(B,A)),i(B,A)))).
p(i(i(i(A,B),C),i(i(C,B),i(i(B,A),A)))).
p(i(i(A,i(i(B,C),i(C,B))),i(i(D,C),i(A,i(D,B))))).
p(i(i(i(i(i(A,B),i(B,A)),i(C,A)),D),i(i(C,B),D))).
p(i(A,i(B,f(A,B)))).
p(i(i(i(i(i(A,B),B),C),i(C,i(i(A,B),B))),i(i(D,i(B,A)),i(C,i(D,A))))).
p(i(i(i(i(i(A,B),C),C),D),i(i(i(B,A),C),D))).
p(i(i(i(A,B),B),i(i(A,i(A,B)),i(A,B)))).
p(i(i(A,B),i(i(i(A,C),i(C,B)),i(C,B)))).
p(i(i(i(i(A,B),i(C,B)),A),i(i(A,C),C))).
p(i(i(i(A,f(B,A)),C),i(B,C))).
p(i(i(i(i(A,B),i(B,A)),i(C,B)),i(i(C,A),i(C,B)))).
p(i(i(i(A,B),i(C,A)),i(i(B,C),i(B,A)))).
p(i(i(i(i(i(A,B),A),A),C),i(i(i(A,B),B),C))).
p(i(i(i(i(i(A,B),i(C,A)),i(C,A)),D),i(i(C,B),D))).
p(i(i(A,i(i(A,B),B)),i(i(B,i(B,B)),i(B,i(A,B))))).
p(i(A,i(i(f(A,B),C),i(B,C)))).
p(i(i(A,B),i(i(A,B),i(A,B)))).
p(i(i(A,B),i(i(B,A),i(B,B)))).
p(i(i(A,i(A,i(B,B))),i(A,i(B,B)))).
p(i(i(i(i(A,B),B),B),i(i(i(A,B),A),A))).
p(i(i(A,i(B,C)),i(i(B,C),i(A,i(B,C))))).
p(i(i(i(A,B),B),i(i(A,i(B,A)),i(A,A)))).
p(i(i(A,i(A,B)),i(i(i(B,i(A,B)),B),B))).
p(i(i(A,i(i(A,B),B)),i(i(i(B,i(A,B)),B),B))).
p(i(i(i(i(A,B),B),A),i(i(i(B,A),B),B))).
p(i(i(A,B),i(i(A,C),i(i(B,C),i(A,C))))).
p(i(i(A,i(i(A,i(B,B)),A)),i(A,A))).
p(i(i(i(A,i(i(A,i(A,A)),A)),A),A)).
p(i(i(A,i(i(B,C),B)),i(i(i(i(C,B),B),C),i(A,B)))).
p(i(A,i(i(B,C),i(i(f(A,B),C),i(B,C))))).
p(i(i(f(i(i(A,i(i(A,i(B,B)),A)),i(A,A)),C),D),i(C,D))).
p(i(f(i(i(A,i(i(A,i(A,A)),A)),B),i(B,A)),A)).
p(i(i(i(i(A,B),B),A),i(f(i(i(B,A),C),i(C,B)),B))).
p(i(i(i(i(A,B),i(i(f(C,A),B),i(A,B))),D),i(C,D))).
p(i(i(i(A,A),A),A)).
p(i(f(i(i(A,A),B),i(B,A)),A)).
p(i(i(i(A,A),B),i(i(B,A),A))).
p(i(i(A,i(B,C)),i(i(i(C,C),B),i(A,C)))).
p(i(i(A,B),i(i(i(A,B),B),B))).
p(i(i(A,i(i(B,B),C)),i(i(D,i(C,B)),i(A,i(D,B))))).
p(i(i(i(A,A),i(i(B,A),A)),i(i(B,A),A))).
p(i(i(A,i(B,A)),i(A,A))).
p(i(A,i(i(B,C),i(B,C)))).
p(i(i(A,B),i(C,i(A,B)))).
p(i(i(i(A,A),B),i(C,B))).
p(i(i(A,i(i(B,C),D)),i(i(B,C),i(A,D)))).
p(i(i(i(A,i(B,C)),D),i(i(B,C),D))).
p(i(A,i(B,i(C,C)))).
p(i(i(i(A,B),B),i(i(C,i(B,A)),i(C,A)))).
p(i(i(A,i(i(B,i(C,C)),D)),i(A,D))).
p(i(i(A,i(i(A,B),B)),i(B,i(A,B)))).
p(i(i(i(A,B),B),i(B,i(A,B)))).
p(i(i(A,i(B,C)),i(B,i(A,C)))).
p(i(A,i(B,A))).
end_of_list.

weight_list(pick_and_purge).
% 74/24/4 proof
weight(p(i(f(i(A,B),i(B,C)),i(A,C))),2).
weight(p(i(i(i(i(A,B),i(C,B)),D),i(i(C,A),D))),2).
weight(p(i(i(i(i(A,B),B),C),i(i(i(B,A),A),C))),2).
weight(p(i(i(i(A,B),C),i(i(i(B,A),i(A,B)),C))),2).
weight(p(i(i(i(A,B),C),i(f(i(A,D),i(D,B)),C))),2).
weight(p(i(i(A,i(B,C)),i(i(D,B),i(A,i(D,C))))),2).
weight(p(i(i(A,A),i(A,A))),2).
weight(p(i(i(A,i(B,C)),i(i(i(C,B),B),i(A,C)))),2).
weight(p(i(i(i(i(i(A,B),B),C),D),i(i(i(i(B,A),A),C),D))),2).
weight(p(i(i(i(i(A,B),i(C,B)),i(C,B)),i(i(A,C),i(A,B)))),2).
weight(p(i(f(i(i(A,B),C),i(C,i(B,A))),i(B,A))),2).
weight(p(i(f(i(i(A,B),C),i(C,B)),i(i(B,A),A))),2).
weight(p(i(i(A,i(i(B,C),C)),i(i(i(i(C,B),B),D),i(A,D)))),2).
weight(p(i(i(A,B),i(i(i(C,B),i(B,C)),i(A,C)))),2).
weight(p(i(i(A,i(i(B,C),i(C,B))),i(i(i(C,B),D),i(A,D)))),2).
weight(p(i(A,A)),2).
weight(p(i(i(A,i(i(B,C),C)),i(i(D,i(C,B)),i(A,i(D,B))))),2).
weight(p(i(i(i(i(i(A,B),B),i(C,A)),D),i(i(C,i(B,A)),D))),2).
weight(p(i(i(i(i(A,i(B,C)),i(B,D)),i(B,D)),i(i(A,i(D,C)),i(A,i(B,C))))),2).
weight(p(i(i(i(A,B),C),i(i(C,i(B,A)),i(B,A)))),2).
weight(p(i(i(i(A,B),C),i(i(C,B),i(i(B,A),A)))),2).
weight(p(i(i(A,i(i(B,C),i(C,B))),i(i(D,C),i(A,i(D,B))))),2).
weight(p(i(i(i(i(i(A,B),i(B,A)),i(C,A)),D),i(i(C,B),D))),2).
weight(p(i(A,i(B,f(A,B)))),2).
weight(p(i(i(i(i(i(A,B),B),C),i(C,i(i(A,B),B))),i(i(D,i(B,A)),i(C,i(D,A))))),2).
weight(p(i(i(i(i(i(A,B),C),C),D),i(i(i(B,A),C),D))),2).
weight(p(i(i(i(A,B),B),i(i(A,i(A,B)),i(A,B)))),2).
weight(p(i(i(A,B),i(i(i(A,C),i(C,B)),i(C,B)))),2).
weight(p(i(i(i(i(A,B),i(C,B)),A),i(i(A,C),C))),2).
weight(p(i(i(i(A,f(B,A)),C),i(B,C))),2).
weight(p(i(i(i(i(A,B),i(B,A)),i(C,B)),i(i(C,A),i(C,B)))),2).
weight(p(i(i(i(A,B),i(C,A)),i(i(B,C),i(B,A)))),2).
weight(p(i(i(i(i(i(A,B),A),A),C),i(i(i(A,B),B),C))),2).
weight(p(i(i(i(i(i(A,B),i(C,A)),i(C,A)),D),i(i(C,B),D))),2).
weight(p(i(i(A,i(i(A,B),B)),i(i(B,i(B,B)),i(B,i(A,B))))),2).
weight(p(i(A,i(i(f(A,B),C),i(B,C)))),2).
weight(p(i(i(A,B),i(i(A,B),i(A,B)))),2).
weight(p(i(i(A,B),i(i(B,A),i(B,B)))),2).
weight(p(i(i(A,i(A,i(B,B))),i(A,i(B,B)))),2).
weight(p(i(i(i(i(A,B),B),B),i(i(i(A,B),A),A))),2).
weight(p(i(i(A,i(B,C)),i(i(B,C),i(A,i(B,C))))),2).
weight(p(i(i(i(A,B),B),i(i(A,i(B,A)),i(A,A)))),2).
weight(p(i(i(A,i(A,B)),i(i(i(B,i(A,B)),B),B))),2).
weight(p(i(i(A,i(i(A,B),B)),i(i(i(B,i(A,B)),B),B))),2).
weight(p(i(i(i(i(A,B),B),A),i(i(i(B,A),B),B))),2).
weight(p(i(i(A,B),i(i(A,C),i(i(B,C),i(A,C))))),2).
weight(p(i(i(A,i(i(A,i(B,B)),A)),i(A,A))),2).
weight(p(i(i(i(A,i(i(A,i(A,A)),A)),A),A)),2).
weight(p(i(i(A,i(i(B,C),B)),i(i(i(i(C,B),B),C),i(A,B)))),2).
weight(p(i(A,i(i(B,C),i(i(f(A,B),C),i(B,C))))),2).
weight(p(i(i(f(i(i(A,i(i(A,i(B,B)),A)),i(A,A)),C),D),i(C,D))),2).
weight(p(i(f(i(i(A,i(i(A,i(A,A)),A)),B),i(B,A)),A)),2).
weight(p(i(i(i(i(A,B),B),A),i(f(i(i(B,A),C),i(C,B)),B))),2).
weight(p(i(i(i(i(A,B),i(i(f(C,A),B),i(A,B))),D),i(C,D))),2).
weight(p(i(i(i(A,A),A),A)),2).
weight(p(i(f(i(i(A,A),B),i(B,A)),A)),2).
weight(p(i(i(i(A,A),B),i(i(B,A),A))),2).
weight(p(i(i(A,i(B,C)),i(i(i(C,C),B),i(A,C)))),2).
weight(p(i(i(A,B),i(i(i(A,B),B),B))),2).
weight(p(i(i(A,i(i(B,B),C)),i(i(D,i(C,B)),i(A,i(D,B))))),2).
weight(p(i(i(i(A,A),i(i(B,A),A)),i(i(B,A),A))),2).
weight(p(i(i(A,i(B,A)),i(A,A))),2).
weight(p(i(A,i(i(B,C),i(B,C)))),2).
weight(p(i(i(A,B),i(C,i(A,B)))),2).
weight(p(i(i(i(A,A),B),i(C,B))),2).
weight(p(i(i(A,i(i(B,C),D)),i(i(B,C),i(A,D)))),2).
weight(p(i(i(i(A,i(B,C)),D),i(i(B,C),D))),2).
weight(p(i(A,i(B,i(C,C)))),2).
weight(p(i(i(i(A,B),B),i(i(C,i(B,A)),i(C,A)))),2).
weight(p(i(i(A,i(i(B,i(C,C)),D)),i(A,D))),2).
weight(p(i(i(A,i(i(A,B),B)),i(B,i(A,B)))),2).
weight(p(i(i(i(A,B),B),i(B,i(A,B)))),2).
weight(p(i(i(A,i(B,C)),i(B,i(A,C)))),2).
weight(p(i(A,i(B,A))),2).
end_of_list.

list(usable).
-p(i(A,B)) | -p(A) | p(B) # label(Det).
-p(i(f(A,B),C)) | p(i(A,i(B,C))) # label(Resid1).
p(i(f(A,B),C)) | -p(i(A,i(B,C))) # label(Resid2).
-p(i(c1,i(c2,c1))) | -p(i(i(x,i(y,z)),i(y,i(x,z)))) # label(AxK_AxC_denials).
end_of_list.

list(sos).
p(i(i(A,B),i(i(B,C),i(A,C)))) # label(AxBp).
p(i(i(i(X,Y),Y),i(i(Y,X),X))) # label(AxL).
p(i(i(i(X,Y),i(Y,X)),i(Y,X))) # label(AxTO).
end_of_list.