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
   |0|()	weight: 0
     s(x1)	weight: 39 + 2 * x1
     f(x1)	weight: 39 + 2 * x1
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 1 3
   |0|()	weight: 0
     s(x1)	weight: 39 + 2 * x1
     f(x1)	weight: 40 + x1
Number of strict rules: 0
YES