% Find an orthomodular lattice that is not modular.

formulas(assumptions).

% Lattice Axioms

x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x v y = y v x.
(x v y) v z = x v (y v z).
x v (x ^ y) = x.
x ^ (x v y) = x.

% Idempotence (follows from the lattice axioms)

x ^ x = x.
x v x = x.

% The following gives us ortholattices.

c(x) ^ x = 0.
c(x) v x = 1.
c(c(x)) = x.
x ^ y = c(c(x) v c(y)).

% Ortholattice lemmas.

1 v x = 1.
1 ^ x = x.

0 ^ x = 0.
0 v x = x.

% Make it an orthomodular lattice

x v (c(x) ^ (x v y)) = x v y.  % (OML)

% Denial of Modularity:

A v (B ^ (A v C)) != (A v B) ^ (A v C).

end_of_list.