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