% axioms
a = b
aab = c
aa =

% ordering
ordering: lex a > c > b

% no goals