include("ortholattice-header").

% OML basis: { AJ, B1, DM, OM }

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
  x v (c(x) ^ (x v y)) = x v y.    % OM

  A v (B v C) != B v (A v C).      % denial of AJ
% A v (A ^ B) != A.                % denial of B1
% A ^ B != c(c(A) v c(B)).         % denial of DM
% A v (c(A) ^ (A v B)) != A v B.   % denial of OM

end_of_list.