clauses(theory).

  % Lattice Theory

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

  % This is for Mace4 (finite), so we can include 0 and 1.

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

end_of_list.

clauses(goals).

  % Deny follwing clauses.  (Clauses in "goals" are falsified in any
  % models that are produced.)

  (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82).
  x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2).

end_of_list.