op(400, xfx, +).  % infix operator
op(300, yf, @).   % postfix operator

set(knuth_bendix).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
assign(max_mem, 100000).
assign(pick_given_ratio, 6).

list(usable).
x = x.
end_of_list.

list(sos).

% Huntington axioms for Boolean algebra:

x + y = y + x.
(x + y) + z = x + (y + z).
(x + y@)@ + (x@ + y@)@ = y.

% Definition of conjunction:

(x * y) = (x@ + y@)@.

end_of_list.

list(sos).

%  Denial of single axiom (weight 111, 6 variables)

(((X * X@) + ((X * Y) + (X@ * Y))) * ((((Z + (U + V)@)@ + (Z + V)@ )@
* W@) + ((((Z + (U + V)@)@ + (Z + V)@)@ * Z) + (W@ * Z)))@) + ((((X *
X@) + ((X * Y) + (X@ * Y))) * Z) + (((((Z + (U + V)@)@ + (Z + V)@)@ *
W@) + ((((Z + (U + V)@)@ + (Z + V)@)@ * Z) + (W@ * Z)))@ * Z)) != Y.

end_of_list.
