Input TRS:
    1: f(|0|()) -> s(|0|())
    2: f(s(|0|())) -> s(s(|0|()))
    3: f(s(|0|())) -> *(s(s(|0|())),f(|0|()))
    4: f(+(x,s(|0|()))) -> +(s(s(|0|())),f(x))
    5: f(+(x,y)) -> *(f(x),f(y))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 4 1 5 2
   |0|()	weight: 0
     s(x1)	weight: (/ 1 8) + x1
     f(x1)	weight: (/ 1 4) + 2 * x1
     +(x1,x2)	weight: (/ 3 16) + x1 + x2
     *(x1,x2)	weight: x1 + x2
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing f
3: f❆1_s(|0|()) -> *(s(s(|0|())),f❆1_|0|())
6: f(|0|()) ->= f❆1_|0|()
7: f(s(_1)) ->= f❆1_s(_1)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 3 7 6
   |0|()	weight: 0
     s(x1)	weight: (/ 1 8) + x1
f❆1_s(x1)	weight: (/ 3 8) + x1
     f(x1)	weight: (/ 1 4) + 2 * x1
f❆1_|0|()	weight: 0
     +(x1,x2)	weight: x1 + x2
     *(x1,x2)	weight: x1 + x2
Number of strict rules: 0
YES