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