YES
Time: 0.014574
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#(h(x, y), z) -> g#(x, f(y, z)), g#(h(x, y), z) -> g#(x, f(y, z)))
     (g#(h(x, y), z) -> g#(x, f(y, z)), g#(f(x, y), z) -> g#(y, z))
     (g#(x, h(y, z)) -> g#(x, y), g#(x, h(y, z)) -> g#(x, y))
     (g#(x, h(y, z)) -> g#(x, y), g#(f(x, y), z) -> g#(y, z))
     (g#(x, h(y, z)) -> g#(x, y), g#(h(x, y), z) -> g#(x, f(y, z)))
     (g#(f(x, y), z) -> g#(y, z), 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), g#(h(x, y), z) -> g#(x, f(y, z)))}
    STATUS:
     arrows: 0.111111
     SCCS (1):
      Scc:
       {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))}
      
      SCC (3):
       Strict:
        {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))}
       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,
         
         [g](x0, x1) = 0,
         
         [h](x0, x1) = x0 + 1,
         
         [g#](x0, x1) = x0
        Strict:
         g#(h(x, y), z) -> g#(x, f(y, z))
         1 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
         g#(f(x, y), z) -> g#(y, z)
         0 + 0x + 1y + 0z >= 0 + 1y + 0z
         g#(x, h(y, z)) -> g#(x, y)
         0 + 1x + 0y + 0z >= 0 + 1x + 0y
        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 >= 0 + 0x + 0y + 0z
         g(x, h(y, z)) -> h(g(x, y), z)
         0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
       SCCS (1):
        Scc:
         {g#(x, h(y, z)) -> g#(x, y),
          g#(f(x, y), z) -> g#(y, z)}
        
        SCC (2):
         Strict:
          {g#(x, h(y, z)) -> g#(x, y),
           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
           g#(x, h(y, z)) -> g#(x, y)
           0 + 1x + 0y + 0z >= 0 + 1x + 0y
          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
         SCCS (1):
          Scc:
           {g#(x, h(y, z)) -> g#(x, y)}
          
          SCC (1):
           Strict:
            {g#(x, h(y, z)) -> g#(x, y)}
           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) = x0 + x1 + 1,
             
             [h](x0, x1) = x0 + 1,
             
             [g#](x0, x1) = x0
            Strict:
             g#(x, h(y, z)) -> g#(x, y)
             1 + 0x + 1y + 0z >= 0 + 0x + 1y
            Weak:
             g(h(x, y), z) -> g(x, f(y, z))
             2 + 1x + 0y + 1z >= 2 + 1x + 0y + 1z
             g(f(x, y), z) -> f(x, g(y, z))
             2 + 0x + 1y + 1z >= 2 + 0x + 1y + 1z
             g(x, h(y, z)) -> h(g(x, y), z)
             2 + 1x + 1y + 0z >= 2 + 1x + 1y + 0z
           Qed