op(400,xfx,^).
op(400,xfx,v).

set(knuth_bendix).

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

assign(pick_given_ratio, 4).
assign(max_weight, 15).
assign(max_mem, 12000).

%%%%%%%%%%%%%%%%%%%%%  Modifications to basic KB strategy below.

set(output_sequent).
set(hyper_res). set(order_history).
set(para_from_units_only).
set(para_into_units_only).

list(usable).
x = x.
end_of_list.

list(sos).
(x ^ y) v (x ^ (x v y)) = x.
(x ^ x) v (y ^ (x v x)) = x.
(x ^ y) v (y ^ (x v y)) = y.
end_of_list.

list(usable).
A ^ A != A | 
A ^ B != B ^ A | 
% ((A v C) ^ (B v C)) ^ C != C | 

A v A != A | 
A v B != B v A.
% ((A ^ C) v (B ^ C)) v C != C.
end_of_list.

list(sos).
((x v y) ^ (z v x)) ^ x = x.  % (5a)
((x ^ y) v (z ^ x)) v x = x.  % (5b)
end_of_list.

weight_list(pick_and_purge).
weight(A, -1).
weight(B, -1).
weight(C, -1).
end_of_list.
