Input TRS:
    1: U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
    2: U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
    3: plus(N,0()) -> N
    4: plus(N,s(M)) -> U11(tt(),M,N)
    5: activate(X) -> X
Number of Rules: 5
Direct QWPOS(Sum) ... orients all.
	I(tt) = 0
	I(0) = 0
	I(plus) = x1 + x2	sigma(plus) = [2,1]
	I(s) = x1 + 1	sigma(s) = [1]
	I(activate) = x1	sigma(activate) = [1]
	I(U11) = x1 + x2 + x3 + 1	sigma(U11) = [1,3,2]
	I(U12) = x1 + x2 + x3 + 1	sigma(U12) = [1,3,2]
    PREC: tt > plus > U11 > 0 = U12 > s = activate
Number of Rules: 0