Input TRS:
    1: f(|0|()) -> cons(|0|())
    2: f(s(|0|())) -> f(p(s(|0|())))
    3: p(s(X)) -> X
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 1 3
   |0|()	weight: 0
     s(x1)	weight: (/ 77 2) + x1
     f(x1)	weight: (/ 1 2) + 2 * x1
     p(x1)	weight: x1
  cons(x1)	weight: x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing f
2: f❆1_s(|0|()) -> f❆1_p(s(|0|()))
4: f(p(_1)) ->= f❆1_p(_1)
5: f(s(_1)) ->= f❆1_s(_1)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 4 5 2
   |0|()	weight: 0
f❆1_p(x1)	weight: 2 * x1
     s(x1)	weight: (/ 1 4) + x1
f❆1_s(x1)	weight: (/ 3 4) + x1
     f(x1)	weight: (/ 1 2) + 2 * x1
     p(x1)	weight: (/ 153 4) + x1
  cons(x1)	weight: x1
Number of strict rules: 0
YES