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