assign(max_seconds, 30).


formulas(sos).

% McKenzie's 4-basis (self-dual, absorption) for lattice theory

  x v (y ^ (x ^ z)) = x         # label(McKenzie_1).
  x ^ (y v (x v z)) = x         # label(McKenzie_2).
  ((y ^ x) v (x ^ z)) v x = x   # label(McKenzie_3).
  ((y v x) ^ (x v z)) ^ x = x   # label(McKenzie_4).

end_of_list.

set(restrict_denials).

formulas(goals).

% A standard 6-basis for lattice theory.
% This gives six separate proofs plus a combined proof.

  x v y = y v x                # answer(commute_join).
  (x v y) v z = x v (y v z)    # answer(assoc_join).
  x ^ y = y ^ x                # answer(commute_meet).
  (x ^ y) ^ z = x^ (y ^ z)     # answer(assoc_meet).
  x ^ (x v y) = x              # answer(absorb_1).
  x v (x ^ y) = x              # answer(absorb_2).

  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          # label(all_six).

end_of_list.