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, 100).
assign(change_limit_after, 15).
assign(new_max_weight, 19).

assign(neg_weight, -3).

list(usable).
x = x.
end_of_list.

list(sos).

% Single axiom for BA in terms of Sheffer stroke (weight 105, 6 variables)

(((((x # (((y # z) # (y # (u # z))) # y)) # y) # (((y # z) # (y # (u #
z))) # (x # (y # y)))) # ((((v # (v # w)) # w) # (v # (v # (w # w))))
# y)) # y) # ((((v # (v # w)) # w) # (v # (v # (w # w)))) # ((((x #
(((y # z) # (y # (u # z))) # y)) # y) # (((y # z) # (y # (u # z))) #
(x # (y # y)))) # (y # y))) = w.

% Denials of Veroff's Sheffer BA 2-basis.

(A # C) # (A # (B # C)) != A | (B # A) != (A # B) | $Ans(Veroff).

end_of_list.
