% axioms
aba = baaa

% ordering
ordering: syl-l b > a

% goals
abbaaa = bbaaaaaaa
abbbaaaaaaa = bbbaaaaaaaaaaaaaaa