Input TRS: 1: a(a(x)) -> b(b(x)) 2: b(b(a(x))) -> a(b(b(x))) Number of Rules: 2 Direct QWPOS(Pol) ... orients all. I(a) = x1 + 3 sigma(a) = [1] I(b) = x1 + 1 sigma(b) = [1] PREC: a = b Number of Rules: 0