% axioms
aba = ba

% ordering
ordering: lex a > b

% goals, i.e. word problems to be solved
% Note that any equation appearing after the specification of the preorder is considered a goal.
bba = abba
abbbbbbbbbba = bbbbbbbbbba