% See www.mcs.anl.gov/~mccune/papers/ltsax


clauses(sos).

% Single axioms for lattice theory.

% (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x # label(A1).
  (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x # label(A2).

% Denial of McKenzie 4-basis

B v (A ^ (B ^ C)) != B |
    B ^ (A v (B v C)) != B |
    ((A ^ B) v (B ^ C)) v B != B |
    ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).

end_of_list.