include("ortholattice-header").

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

% As a simple check, we prove commutativity and idempotence.

assign(max_proofs, 2).   % We're looking for two proofs

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

end_of_list.

list(passive).

A v B != B v A | $Ans(CJ).   % denial of CJ
A v A != A | $Ans(IJ).   % denial of IJ

end_of_list.