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

lex([X,Y,X,U,0,1,_ ^ _,_ v _, c(_), f(_,_)]).

set(knuth_bendix).
% set(back_unit_deletion).

assign(pick_given_ratio, 3).

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

clear(sigint_interact).

list(usable).
x = x.
end_of_list.

list(sos).

% MOL 3-basis in terms of join and complement

(x v y) v z = x v (y v z).
x v c(c(x) v y) = x.
x v c(x v c(x v y)) = y v x.      % OML JC axiom (right side commuted)
x v c(c(y) v c(x v z)) = c(c(x v y) v c(x v z)).  % modularity in JC

c(x) v c(y) = f(x,y).     % definition of sheffer stroke
c(c(x) v c(y)) = x ^ y.   % definition of meet (this helps a lot)

end_of_list.

assign(max_weight, 20).
assign(neg_weight, -8).
assign(max_seconds, 600).

set(sos_arg).