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