YES
Time: 0.001540
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))}
  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)))}
   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))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(x, h(y, z)) -> g#(x, y),
        g#(h(x, y), z) -> g#(x, f(y, z))}
      EDG:
       {(g#(x, h(y, z)) -> g#(x, y), g#(h(x, y), z) -> g#(x, f(y, z)))
        (g#(x, h(y, z)) -> g#(x, y), g#(x, h(y, z)) -> g#(x, y))
        (g#(h(x, y), z) -> g#(x, f(y, z)), g#(h(x, y), z) -> g#(x, f(y, z)))}
       SCCS (2):
        Scc:
         {g#(h(x, y), z) -> g#(x, f(y, z))}
        Scc:
         {g#(x, h(y, z)) -> g#(x, y)}
        SCC (1):
         Strict:
          {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))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
        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))}
         SPSC:
          Simple Projection:
           pi(g#) = 1
          Strict:
           {}
          Qed