include("ortholattice-header").

% Modify the basic strategy.

lex([A, B, C, D, 0, 1, x v x, x ^ x, c(x), f(x,x)]).
assign(max_weight, 19).

% BA basis: { AJ, DM, ONE, CUT }

list(sos).

x v (y v z) = y v (x v z).  % AJ
x ^ y = c(c(x) v c(y)).     % DM
x v c(x) = y v c(y).        % ONE
(x v c(y)) ^ (x v y) = x.   % CUT

% Axiom ONE allows us to name the constant.  Also name its complement.

x v c(x) = 1.   % ONEa
c(1) = 0.

% Denial of distributivity.

A ^ (B v C) != (A ^ B) v (A ^ C) | $Ans(DIST1).   % denial of DIST1

end_of_list.