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 modularity.

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

end_of_list.