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