assign(max_seconds, 30).

% The following op commands allow us to use an additional infix
% operation (@) and omit some parentheses (for *).
%
% * is the semigroup operation; @ is the commutator.
% x*y*z is right associated; x*y@z is (x*y)@z

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

assign(eq_defs, fold).
assign(max_weight, 25).

formulas(sos).

% GT axioms

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

% Definition of commutator

x @ y = x' * y' * x * y.

end_of_list.

