Input TRS: 1: f(s(X),Y) -> h(s(f(h(Y),X))) Number of Rules: 1 Direct QWPOS(mSum) ... orients all. I(f) = x1 + x2 sigma(f) = [1,2] I(h) = x1 sigma(h) = [1] I(s) = x1 + 1 sigma(s) = [1] PREC: f > h = s Number of Rules: 0