YES
Time: 0.001323
TRS:
 {                  f(x, x, y) -> x,
                    f(x, y, y) -> y,
                  f(x, y, g y) -> x,
  f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)),
                  f(g x, x, y) -> y}
 RUF:
  Strict:
   {                  f(x, x, y) -> x,
                      f(x, y, y) -> y,
    f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))}
  Weak:
   {}
  DP:
   DP:
    {f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)),
     f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
   TRS:
   {                  f(x, x, y) -> x,
                      f(x, y, y) -> y,
    f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))}
   EDG:
    {(f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)), f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v))
     (f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)), f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)))
     (f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v), f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)))
     (f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v), f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v))}
    SCCS (1):
     Scc:
      {f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)),
       f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
     SCC (2):
      Strict:
       {f#(f(x, y, z), u, f(x, y, v)) -> f#(x, y, f(z, u, v)),
        f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
      Weak:
      {                  f(x, x, y) -> x,
                         f(x, y, y) -> y,
       f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))}
      SPSC:
       Simple Projection:
        pi(f#) = 0
       Strict:
        {f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
       EDG:
        {(f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v), f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v))}
        SCCS (1):
         Scc:
          {f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
         SCC (1):
          Strict:
           {f#(f(x, y, z), u, f(x, y, v)) -> f#(z, u, v)}
          Weak:
          {                  f(x, x, y) -> x,
                             f(x, y, y) -> y,
           f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))}
          SPSC:
           Simple Projection:
            pi(f#) = 2
           Strict:
            {}
           Qed