Input TRS:
    1: f(0()) -> s(0())
    2: f(s(0())) -> s(0())
    3: f(s(s(x))) -> f(f(s(x)))
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 2
     s(x1)	weight: 39 + 2 * x1
     f(x1)	weight: 39 + 2 * x1
     0()	weight: 0
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 1 3
     s(x1)	weight: 39 + 2 * x1
     f(x1)	weight: 40 + x1
     0()	weight: 0
Number of strict rules: 0
YES