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