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.