include("ortholattice-header").

% LT basis: { AJ, AM, B1, B2 }

list(sos).

x v (y v z) = y v (x v z).  % AJ
x ^ (y ^ z) = y ^ (x ^ z).  % AM
x v (x ^ y) = x.            % B1
x ^ (x v y) = x.            % B2

  x v (y ^ (x v z)) = x v (z ^ (x v y)).   % MOD
% x v (y ^ (x v z)) = (x v y) ^ (x v z).   % MOD2

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

end_of_list.