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