Input TRS:
    1: a__and(tt(),X) -> mark(X)
    2: a__plus(N,0()) -> mark(N)
    3: a__plus(N,s(M)) -> s(a__plus(mark(N),mark(M)))
    4: mark(and(X1,X2)) -> a__and(mark(X1),X2)
    5: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    6: mark(tt()) -> tt()
    7: mark(0()) -> 0()
    8: mark(s(X)) -> s(mark(X))
    9: a__and(X1,X2) -> and(X1,X2)
    10: a__plus(X1,X2) -> plus(X1,X2)
Number of Rules: 10
Direct QWPOS(mSum) ... orients all.
	I(tt) = 0
	I(mark) = x1	sigma(mark) = [1]
	I(0) = 0
	I(plus) = x1 + x2 + 1	sigma(plus) = [1,2]
	I(and) = x1 + x2 + 1	sigma(and) = [1,2]
	I(a__and) = x1 + x2 + 1	sigma(a__and) = [2,1]
	I(s) = x1 + 1	sigma(s) = [1]
	I(a__plus) = x1 + x2 + 1	sigma(a__plus) = [1,2]
    PREC: tt = mark = 0 = a__and > and = a__plus > plus = s
Number of Rules: 0