% With the following op commands, x*y*z is right associated; x*y@z is (x*y)@z.

op(450, infix, @).
op(400, infix_right, *).

lex([A, B, C, D, F, G, e, _@_, _*_, i(_)]).

set(anl_eq).

assign(max_weight, 19).
assign(pick_given_ratio, 4).

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

assign(max_seconds, 60).
assign(max_mem, 150000).

clear(sigint_interact).

list(usable).
x = x.
end_of_list.

list(sos).

% GT axioms

(x * y) * z = x * (y * z).
e * x = x.
i(x) * x = e.

% Definition of commutator

(x @ y) = i(x) * i(y) * x * y.

end_of_list.