op(400, xfx, #).  % infix 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).

assign(max_weight, 100).
% assign(max_proofs, -1).
assign(max_seconds, 90).

list(usable).
x = x.
end_of_list.

list(sos).
((x # (x # z)) # z) # (x # (x # (z # z))) = z.  % P1 from Pixley-8 (P-21)
((y # (x # y)) # y) # (x # (y # (y # y))) = x.  % P2 from Pixley-8 (P-21)
((y # (x # x)) # x) # (x # (y # (x # x))) = x.  % P3 from Pixley-8 (P-21)
(x # z) # (x # (y # z)) = x.  % Veroff-27a
end_of_list.

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