Input TRS: 1: +(x,0()) -> x 2: +(x,s(y)) -> s(+(x,y)) 3: +(0(),s(y)) -> s(y) 4: s(+(0(),y)) -> s(y) Number of Rules: 4 Direct QTKBOS ... orients all. I(+) = 3 * x1 + 3 * x2 + 1 sigma(+) = [2,1] I(0) = 3 I(s) = x1 + 2 sigma(s) = [1] PREC: + > 0 = s Number of Rules: 0