op(400, xfx, ^).
op(400, xfx, v).

set(knuth_bendix).
assign(pick_given_ratio, 3).
assign(max_weight, 55).
assign(neg_weight, -5).

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).

list(sos).

x = x.

% 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.  % A1
 (((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x.  % 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.

end_of_list.