Input TRS:
    1: terms(N) -> cons(recip(sqr(N)))
    2: sqr(0()) -> 0()
    3: sqr(s()) -> s()
    4: dbl(0()) -> 0()
    5: dbl(s()) -> s()
    6: add(0(),X) -> X
    7: add(s(),Y) -> s()
    8: first(0(),X) -> nil()
    9: first(s(),cons(Y)) -> cons(Y)
Number of Rules: 9
Direct QWPOS(mSum) ... orients all.
	I(sqr) = x1	sigma(sqr) = [1]
	I(terms) = x1 + 1	sigma(terms) = [1]
	I(0) = 1
	I(nil) = 0
	I(s) = 0
	I(recip) = x1	sigma(recip) = [1]
	I(add) = x1 + x2	sigma(add) = [2,1]
	I(cons) = x1	sigma(cons) = [1]
	I(dbl) = x1	sigma(dbl) = [1]
	I(first) = x1 + x2	sigma(first) = [1,2]
    PREC: 0 > terms = nil = s = add = dbl > sqr = recip = cons = first
Number of Rules: 0