YES
Time: 0.004077
TRS:
 {g(x, h(y, z)) -> h(g(x, y), z),
  g(f(x, y), z) -> f(x, g(y, z)),
  g(h(x, y), z) -> g(x, f(y, z))}
 DP:
  DP:
   {g#(x, h(y, z)) -> g#(x, y),
    g#(f(x, y), z) -> g#(y, z),
    g#(h(x, y), z) -> g#(x, f(y, z))}
  TRS:
  {g(x, h(y, z)) -> h(g(x, y), z),
   g(f(x, y), z) -> f(x, g(y, z)),
   g(h(x, y), z) -> g(x, f(y, z))}
  UR:
   {}
   EDG:
    {(g#(x, h(y, z)) -> g#(x, y), g#(f(x, y), z) -> g#(y, z))
     (g#(f(x, y), z) -> g#(y, z), g#(f(x, y), z) -> g#(y, z))}
    STATUS:
     arrows: 0.777778
     SCCS (1):
      Scc:
       {g#(f(x, y), z) -> g#(y, z)}
      
      
      
      SCC (1):
       Strict:
        {g#(f(x, y), z) -> g#(y, z)}
       Weak:
       {g(x, h(y, z)) -> h(g(x, y), z),
        g(f(x, y), z) -> f(x, g(y, z)),
        g(h(x, y), z) -> g(x, f(y, z))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = x0 + 1,
         
         [g](x0, x1) = 0,
         
         [h](x0, x1) = 0,
         
         [g#](x0, x1) = x0
        Strict:
         g#(f(x, y), z) -> g#(y, z)
         1 + 0x + 1y + 0z >= 0 + 1y + 0z
        Weak:
         g(h(x, y), z) -> g(x, f(y, z))
         0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
         g(f(x, y), z) -> f(x, g(y, z))
         0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
         g(x, h(y, z)) -> h(g(x, y), z)
         0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
       Qed