include("ortholattice-header").

% MOL basis: { AJ, B1, DM, CC, ONE, MOD }

list(sos).

x v (y v z) = y v (x v z).  % AJ
x v (x ^ y) = x.            % B1
x ^ y = c(c(x) v c(y)).     % DM
c(c(x)) = x.                % CC
x v c(x) = y v c(y).        % ONE
x v (y ^ (x v z)) = x v (z ^ (x v y)).  % MOD

A v (c(A) ^ (A v B)) != A v B | $Ans(OM).   % denial of OM

end_of_list.