set(hyper_res).

assign(bsub_hint_wt, 0).
set(keep_hint_subsumers).
clear(print_kept).

list(hints).
% Proof of Reflexivity from XCB
P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v)).
P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),e(v6,w)),v6)).
P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v))).
P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(v,u)),v),w),v6),e(w,v6))).
P(e(e(x,e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w)),x)).
P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),v),e(w,v)),w))).
P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6)),v7),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)).
P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),v),e(w,v)),w),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)).
P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,v),e(w,v)),w)),v6),e(v7,v6))),v7)).
P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),u)).
P(e(x,x)).
end_of_list.

list(usable).
-P(e(x,y)) | -P(x) | P(y) | $Ans(clause_number=$NEXT_CL_NUM,
                                 length_major=count(e(x,y)),
        	                 length_minor=count(x),
        	                 length_conclusion=count(y)).
end_of_list.
  
list(sos).
P(e(x,e(e(e(x,y),e(z,y)),z))).  % XCB
end_of_list.
  
list(passive).
-P(e(a,a)) | $ANSWER(reflex).
end_of_list.

make_evaluable(_+_, $SUM(_,_)).
clear(demod_history).
assign(demod_limit, -1).

list(demodulators).
count(e(x,y)) = count(x) + count(y) + 1.
$VAR(x) -> count(x) = 1.
end_of_list.