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

set(knuth_bendix).
assign(pick_given_ratio, 1).
assign(max_weight, 30).

assign(max_mem, 60000).

clear(back_sub).

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

assign(max_given, 1150).   % This should get 30 of weight -85 (length 15).

weight_list(pick_and_purge).
weight(Pixley($(1)), -100).
end_of_list.

list(usable).
x = x.
end_of_list.

list(sos).
((x # x) # (x # y)) = x.
(x # (x # y)) = (x # (y # y)).
(x # (x # (y # z))) = (y # (y # (x # z))).

% lemmas:

% (x # x) # (x # y)=x.
% x # y=y # x.
(x # y) # (x # x)=x.
(x # x) # (y # x)=x.
(x # y) # (y # y)=y.

% (x # (x # x)) = 0.  % lemma
% (0 # 0) = 1.        % definition

Pixley((((a#a)# ((b#b)# (b#b)))# ((((a#a)# (c#c))# (((b#b)# (b#b))# (c#c)))# (((a#a)# (c#c))# (((b#b)# (b#b))# (c#c)))))# (((a#a)# ((b#b)# (b#b)))# ((((a#a)# (c#c))# (((b#b)# (b#b))# (c#c)))# (((a#a)# (c#c))# (((b#b)# (b#b))# (c#c)))))).
end_of_list.