op(400, xfx, [*,+,#]).  % infix operators
op(300, yf, @).         % postfix operator

set(knuth_bendix).
set(back_unit_deletion).

clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
assign(max_mem, 100000).
assign(pick_given_ratio, 8).

assign(max_weight, 110).
assign(change_limit_after, 7).
assign(new_max_weight, 30).

assign(neg_weight, -4).

% assign(max_proofs, -1).

list(usable).
x = x.
end_of_list.

list(sos).

% Single axiom for BA (weight 127, 6 variables)

(((x * x@ ) + ((x * y) + (x@ * y))) * ((((((z + (u + v)@ )@ + 0) * 1)
+ (z + v)@ )@ * w@ ) + ((((((z + (u + v)@ )@ + 0) * 1) + (z + v)@ )@ *
z) + (w@ * z)))@ ) + ((((x * x@ ) + ((x * y) + (x@ * y))) * z) +
(((((((z + (u + v)@ )@ + 0) * 1) + (z + v)@ )@ * w@ ) + ((((((z + (u +
v)@ )@ + 0) * 1) + (z + v)@ )@ * z) + (w@ * z)))@ * z)) = y.

% Denials: Hunting axioms and the dual.

A + B != B + A | (A + B) + C != A + (B + C) | (A + B@)@ + (A@ + B@)@ != B | (A@ +B@ )@ !=A*B | $Ans(Huntington_axioms_or).

A * B != B * A | (A * B) * C != A * (B * C) | (A * B@)@ * (A@ * B@)@ != B | (A@ *B@ )@ !=A+B | $Ans(Huntington_axioms_and).

end_of_list.

% list(passive).
% 
% A + B != B + A | $Ans(Commutativity_or).
% (A + B) + C != A + (B + C) | $Ans(Associativity_or).
% (A + B@)@ + (A@ + B@)@ != B | $Ans(Huntington_or).
% ((A + B)@ + (A + B@)@)@ != A | $Ans(Robbins_or).
% 
% A * B != B * A | $Ans(Commutativity_and).
% (A * B) * C != A * (B * C) | $Ans(Associativity_and).
% (A * B@)@ * (A@ * B@)@ != B | $Ans(Huntington_and).
% ((A * B)@ * (A * B@)@)@ != A | $Ans(Robbins_and).
% 
% A@ @ != A | $Ans(L1).
% A + A != A | $Ans(Idempotence_or).
% A * A != A | $Ans(Idempotence_and).
% 
% A + (B + A@)@ !=A | $Ans(L2_or).
% A + (B + B@)@ !=A | $Ans(L3_or).
% A + A@ != B + B@ | $Ans(One).
% 
% A * (B * A@)@ !=A | $Ans(L2_and).
% A * (B * B@)@ !=A | $Ans(L3_and).
% A * A@ != B * B@ | $Ans(Zero).
% 
% (A + B) * B != B | $Ans(A1).
% A * (B + C) != (B * A) + (C * A) | $Ans(D1).
% (B * A) + (C * A) != A * (B + C) | $Ans(D1).
% A + A@ != 1 | $Ans(1).
% 
% (A * B) + B != B | $Ans(A2).
% A + (B * C) != (B + A) * (C + A) | $Ans(D2).
% (B + A) * (C + A) != A + (B * C) | $Ans(D2).
% A * A@ != 0 | $Ans(0).
% 
% end_of_list.