Input TRS:
    1: f(s(x),s(y),s(z)) -> f(g(z,s(x)),h(s(y),z),k(s(z),x,y))
    2: g(s(x),s(y)) ->= h(s(s(y)),s(s(x)))
    3: h(s(x),s(y)) ->= g(s(s(y)),s(s(x)))
    4: k(x,y,z) ->= f(|0|(),y,z)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing f g h
1: f❆1_s(x,s(y),s(z)) -> f(g(z,s(x)),h❆1_s(y,z),k(s(z),x,y))
2: g❆1_s(x,s(y)) ->= h❆1_s(s(y),s(s(x)))
3: h❆1_s(x,s(y)) ->= g❆1_s(s(y),s(s(x)))
4: k(x,y,z) ->= f❆1_|0|(y,z)
5: h(s(_1),_2) ->= h❆1_s(_1,_2)
6: g(s(_1),_2) ->= g❆1_s(_1,_2)
7: f(|0|(),_2,_3) ->= f❆1_|0|(_2,_3)
8: f(s(_1),_3,_4) ->= f❆1_s(_1,_3,_4)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #f❆1_s(x,s(y),s(z)) -> #f(g(z,s(x)),h❆1_s(y,z),k(s(z),x,y))
   #2: #f(s(_1),_3,_4) ->? #f❆1_s(_1,_3,_4)
Number of SCCs: 0, DPs: 0, edges: 0
YES