include("ortholattice-header").

% OL basis: { AJ, B1, DM, CC, ONE }

list(usable).

  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

% 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
  c(c(A)) != A.                % denial of CC
% A v c(A) != B v c(B).        % denial of ONE

end_of_list.

