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

set(knuth_bendix).
assign(pick_given_ratio, 4).

assign(max_mem, 100000).

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

list(usable).
x = x.
end_of_list.

list(sos).
(x # z) # (x # (y # z)) = x.  % Veroff-27a
% (x # x) # (y # x) = x.  % Meredith-1
% (x # x) # (x # y) = x.  % Meredith-1a
% (x # y) # (x # x) = x.  % Meredith-1b
(y # x) # (x # x) = x.  % Meredith-1c
end_of_list.

list(passive).
A # B != B # A | $Ans(Commutativity).
end_of_list.