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 QTKBOS ... orients all. I(0) = 1 I(a) = x1 + 2 * x2 sigma(a) = [1,2] I(b) = x1 + 3 * x2 + 3 sigma(b) = [1,2] I(c) = 2 * x1 sigma(c) = [1] PREC: c > 0 > a = b Number of Rules: 0