include("ortholattice-header").

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

assign(max_proofs, 2).

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

end_of_list.

list(passive).

c(c(A)) != A | $Ans(CC).            % denial of CC
A v c(A) != B v c(B) | $Ans(ONE).    % denial of ONE

end_of_list.