assign(new_constants, 1).

% assign(eq_defs, fold).  % causes DM to be oriented so that ^ is introduced

clauses(sos).

% These four equations are a basis for orthomodular lattices (OML)

x v (y v z) = y v (x v z)     # label(AJ).
x v (x ^ y) = x               # label(B1).
x ^ y = c(c(x) v c(y))        # label(DM).
x v (c(x) ^ (x v y)) = x v y  # label(OM).

end_of_list.

clauses(goals).

c(c(x)) = x         # answer(CC).
x v c(x) = y v c(y) # answer(ONE).

end_of_list.