include("ortholattice-header"). % LT basis: { AJ, AM, B1, B2 } list(usable). % 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 A v (B v C) != B v (A v C). % denial of AJ % A ^ (B ^ C) != B ^ (A ^ C). % denial of AM % A v (A ^ B) != A. % denial of B1 % A ^ (A v B) != A. % denial of B2 end_of_list.