set(hyper_res).
assign(max_proofs,-1).
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, 0).
set(keep_hint_subsumers).
list(hints).
% 52/26/4 proof
p(i(f(i(A,B),A),B)).
p(i(A,i(B,f(A,B)))).
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(A,B),i(f(i(C,A),C),B))).
p(i(i(i(A,f(B,A)),C),i(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(f(i(A,f(i(B,C),B)),A),C)).
p(i(f(i(A,i(i(B,C),C)),A),i(i(C,B),B))).
p(i(i(A,B),i(C,i(A,f(C,B))))).
p(i(i(A,B),i(i(C,A),i(i(B,D),i(C,D))))).
p(i(i(A,i(B,C)),i(i(i(C,B),B),i(A,C)))).
p(i(i(A,f(i(B,C),B)),i(A,C))).
p(i(i(A,i(i(B,C),C)),i(A,i(i(C,B),B)))).
p(i(i(A,i(i(B,C),C)),i(i(D,i(C,B)),i(A,i(D,B))))).
p(i(i(A,B),i(i(i(C,A),A),i(i(B,C),C)))).
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(i(A,B),i(C,B)),i(C,D)),i(C,D)),i(i(D,A),i(i(A,B),i(C,B))))).
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(A,i(i(B,f(i(C,D),C)),f(A,i(B,D))))).
p(i(i(i(A,i(i(B,C),C)),D),i(i(A,i(i(C,B),B)),D))).
p(i(A,i(i(i(B,C),C),i(i(f(A,C),B),B)))).
p(i(i(A,i(i(A,B),B)),i(i(B,i(B,B)),i(B,i(A,B))))).
p(i(i(A,i(f(i(i(B,C),C),i(B,C)),B)),i(i(i(B,C),C),i(A,B)))).
p(i(i(A,i(i(B,C),C)),i(D,i(A,i(i(f(D,C),B),B))))).
p(i(i(A,i(i(B,A),A)),i(i(B,i(B,B)),i(B,i(A,B))))).
p(i(i(i(A,A),A),i(i(i(i(A,A),A),A),A))).
p(i(i(A,i(i(B,C),C)),i(D,i(A,i(i(f(D,B),C),C))))).
p(i(i(A,i(A,A)),i(A,i(i(i(A,A),A),A)))).
p(i(A,i(i(i(B,B),B),i(i(f(A,i(i(B,B),B)),B),B)))).
p(i(i(A,A),i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A)))).
p(i(f(A,i(i(B,B),B)),i(i(f(A,i(i(B,B),B)),B),B))).
p(i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A))).
p(i(i(A,i(A,A)),i(A,i(f(B,i(i(A,A),A)),A)))).
p(i(i(i(A,A),i(i(A,A),i(A,A))),i(i(A,A),i(A,A)))).
p(i(i(A,A),i(f(B,i(i(i(A,A),i(A,A)),i(A,A))),i(A,A)))).
p(i(f(A,i(i(i(B,B),i(B,B)),i(B,B))),i(B,B))).
p(i(A,i(i(i(i(B,B),i(B,B)),i(B,B)),i(B,B)))).
p(i(i(i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A)),B),i(C,B))).
p(i(A,i(i(B,B),i(i(B,B),i(B,B))))).
p(i(i(i(i(A,A),i(i(A,A),i(A,A))),B),i(C,B))).
p(i(A,i(i(B,B),i(B,B)))).
p(i(i(A,i(B,B)),i(C,i(A,i(B,B))))).
p(i(i(A,i(A,A)),i(A,i(i(B,i(C,C)),A)))).
p(i(i(A,A),i(i(B,i(C,C)),i(A,A)))).
p(i(i(A,i(B,i(C,C))),i(i(D,D),i(A,i(D,D))))).
p(i(i(A,A),i(B,i(A,A)))).
p(i(A,i(B,B))).
p(i(A,i(i(B,i(C,C)),A))).
p(i(i(A,i(B,i(C,C))),i(D,i(A,D)))).
p(i(A,i(B,A))).
end_of_list.
weight_list(pick_and_purge).
% 52/26/4 proof
weight(p(i(f(i(A,B),A),B)),2).
weight(p(i(A,i(B,f(A,B)))),2).
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(A,B),i(f(i(C,A),C),B))),2).
weight(p(i(i(i(A,f(B,A)),C),i(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(f(i(A,f(i(B,C),B)),A),C)),2).
weight(p(i(f(i(A,i(i(B,C),C)),A),i(i(C,B),B))),2).
weight(p(i(i(A,B),i(C,i(A,f(C,B))))),2).
weight(p(i(i(A,B),i(i(C,A),i(i(B,D),i(C,D))))),2).
weight(p(i(i(A,i(B,C)),i(i(i(C,B),B),i(A,C)))),2).
weight(p(i(i(A,f(i(B,C),B)),i(A,C))),2).
weight(p(i(i(A,i(i(B,C),C)),i(A,i(i(C,B),B)))),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(A,B),i(i(i(C,A),A),i(i(B,C),C)))),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(i(A,B),i(C,B)),i(C,D)),i(C,D)),i(i(D,A),i(i(A,B),i(C,B))))),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(A,i(i(B,f(i(C,D),C)),f(A,i(B,D))))),2).
weight(p(i(i(i(A,i(i(B,C),C)),D),i(i(A,i(i(C,B),B)),D))),2).
weight(p(i(A,i(i(i(B,C),C),i(i(f(A,C),B),B)))),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(i(A,i(f(i(i(B,C),C),i(B,C)),B)),i(i(i(B,C),C),i(A,B)))),2).
weight(p(i(i(A,i(i(B,C),C)),i(D,i(A,i(i(f(D,C),B),B))))),2).
weight(p(i(i(A,i(i(B,A),A)),i(i(B,i(B,B)),i(B,i(A,B))))),2).
weight(p(i(i(i(A,A),A),i(i(i(i(A,A),A),A),A))),2).
weight(p(i(i(A,i(i(B,C),C)),i(D,i(A,i(i(f(D,B),C),C))))),2).
weight(p(i(i(A,i(A,A)),i(A,i(i(i(A,A),A),A)))),2).
weight(p(i(A,i(i(i(B,B),B),i(i(f(A,i(i(B,B),B)),B),B)))),2).
weight(p(i(i(A,A),i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A)))),2).
weight(p(i(f(A,i(i(B,B),B)),i(i(f(A,i(i(B,B),B)),B),B))),2).
weight(p(i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A))),2).
weight(p(i(i(A,i(A,A)),i(A,i(f(B,i(i(A,A),A)),A)))),2).
weight(p(i(i(i(A,A),i(i(A,A),i(A,A))),i(i(A,A),i(A,A)))),2).
weight(p(i(i(A,A),i(f(B,i(i(i(A,A),i(A,A)),i(A,A))),i(A,A)))),2).
weight(p(i(f(A,i(i(i(B,B),i(B,B)),i(B,B))),i(B,B))),2).
weight(p(i(A,i(i(i(i(B,B),i(B,B)),i(B,B)),i(B,B)))),2).
weight(p(i(i(i(i(i(i(A,A),i(A,A)),i(A,A)),i(A,A)),B),i(C,B))),2).
weight(p(i(A,i(i(B,B),i(i(B,B),i(B,B))))),2).
weight(p(i(i(i(i(A,A),i(i(A,A),i(A,A))),B),i(C,B))),2).
weight(p(i(A,i(i(B,B),i(B,B)))),2).
weight(p(i(i(A,i(B,B)),i(C,i(A,i(B,B))))),2).
weight(p(i(i(A,i(A,A)),i(A,i(i(B,i(C,C)),A)))),2).
weight(p(i(i(A,A),i(i(B,i(C,C)),i(A,A)))),2).
weight(p(i(i(A,i(B,i(C,C))),i(i(D,D),i(A,i(D,D))))),2).
weight(p(i(i(A,A),i(B,i(A,A)))),2).
weight(p(i(A,i(B,B))),2).
weight(p(i(A,i(i(B,i(C,C)),A))),2).
weight(p(i(i(A,i(B,i(C,C))),i(D,i(A,D)))),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(x,i(y,x))) # label(K_denial).
end_of_list.
list(sos).
p(i(A,A)) # label(AxI).
p(i(i(A,B),i(i(B,C),i(A,C)))) # label(AxBp).
p(i(i(i(A,B),B),i(i(B,A),A))) # label(AxL).
end_of_list.