clauses(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).

% The following can be used to get the subproofs together.
% (Also remove assign(maxproofs, 6).)

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

end_of_list.

set(restrict_denials).
assign(max_proofs, 6).  % prove the 6 parts separately

clauses(goals).

% A standard 6-basis for lattice theory.
% This gives six separate proofs.

    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).

end_of_list.