Input TRS: 1: a(b(x)) -> b(b(a(a(x)))) Number of Rules: 1 Direct POLO(mSum) ... failed.