op(400, xfx, [*,+,#]).  % infix operators
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:

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

% lemmas

% From Huntington axioms we can derive x + x@ = y + y@.  This allows
% us to include the following lemma, which speeds up the proof.
%
% x + x@ = 1.

list(sos).

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

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

end_of_list.
