include("ortholattice-header").

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

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

end_of_list.

list(sos).

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

end_of_list.