%%%%%%%%%%%%%%%%%%%%%  Basic options

op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator

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

assign(pick_given_ratio, 4).
assign(max_mem, 20000).

%%%%%%%%%%%%%%%%%%%%%  Standard for equational problems

set(knuth_bendix).
set(build_proof_object).

%%%%%%%%%%%%%%%%%%%%%  Modifications to strategy

assign(max_weight, 35).
assign(max_mem, 25000).
set(control_memory).

%%%%%%%%%%%%%%%%%%%%%  Clauses

list(usable).
x = x.
end_of_list.

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

list(sos).
A ^ ((B v C) ^ (B v D)) != (A ^ ((B v C) ^ (B v D))) ^ ((A ^ (B v (C^D))) v ((A^C) v  (A^D))).
end_of_list.