include("ortholattice-header").

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

op(400, infix, ^).
op(400, infix, v).

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

% Axiom ONE allows us to name the constant; also name its complement.
% This gives enormous help to Mace2.

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

% 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
  A v (B ^ (A v C)) != A v (C ^ (A v B)).  % denial of MOD

end_of_list.
