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