Input TRS:
    1: minus(0()) -> 0()
    2: +(x,0()) -> x
    3: +(0(),y) -> y
    4: +(minus(1()),1()) -> 0()
    5: minus(minus(x)) -> x
    6: +(x,minus(y)) -> minus(+(minus(x),y))
    7: +(x,+(y,z)) -> +(+(x,y),z)
    8: +(minus(+(x,1())),1()) -> minus(x)
Number of Rules: 8
Direct QWPOS(Sum) ... orients all.
	I(+) = x1 + x2	sigma(+) = [2,1]
	I(0) = 1
	I(1) = 1
	I(minus) = x1	sigma(minus) = [1]
    PREC: + = 0 = 1 > minus
Number of Rules: 0