Input TRS:
    1: g(|0|(),f(x,x)) -> x
    2: g(x,s(y)) -> g(f(x,y),|0|())
    3: g(s(x),y) -> g(f(x,y),|0|())
    4: g(f(x,y),|0|()) -> f(g(x,|0|()),g(y,|0|()))
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 1 3 2
   |0|()	weight: 0
     s(x1)	weight: 30614 + 2 * x1
     f(x1,x2)	weight: 30613 + x1 + 2 * x2
     g(x1,x2)	weight: x1 + 2 * x2
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 4
   |0|()	weight: 0
     s(x1)	weight: (/ 61225 2) + 2 * x1
     f(x1,x2)	weight: (/ 1 4) + x1 + x2
     g(x1,x2)	weight: 2 * x1 + 2 * x2
Number of strict rules: 0
YES