YES
TRS:
 {   f(c(s(x), y)) -> f(c(x, s(y))),
  f(c(s(x), s(y))) -> g(c(x, y)),
     g(c(x, s(y))) -> g(c(s(x), y)),
  g(c(s(x), s(y))) -> f(c(x, y))}
 DP:
  Strict:
   {   f#(c(s(x), y)) -> f#(c(x, s(y))),
    f#(c(s(x), s(y))) -> g#(c(x, y)),
       g#(c(x, s(y))) -> g#(c(s(x), y)),
    g#(c(s(x), s(y))) -> f#(c(x, y))}
  Weak:
  {   f(c(s(x), y)) -> f(c(x, s(y))),
   f(c(s(x), s(y))) -> g(c(x, y)),
      g(c(x, s(y))) -> g(c(s(x), y)),
   g(c(s(x), s(y))) -> f(c(x, y))}
  EDG:
   {(f#(c(s(x), s(y))) -> g#(c(x, y)), g#(c(s(x), s(y))) -> f#(c(x, y)))
    (f#(c(s(x), s(y))) -> g#(c(x, y)), g#(c(x, s(y))) -> g#(c(s(x), y)))
    (g#(c(s(x), s(y))) -> f#(c(x, y)), f#(c(s(x), s(y))) -> g#(c(x, y)))
    (g#(c(s(x), s(y))) -> f#(c(x, y)), f#(c(s(x), y)) -> f#(c(x, s(y))))
    (g#(c(x, s(y))) -> g#(c(s(x), y)), g#(c(x, s(y))) -> g#(c(s(x), y)))
    (g#(c(x, s(y))) -> g#(c(s(x), y)), g#(c(s(x), s(y))) -> f#(c(x, y)))
    (f#(c(s(x), y)) -> f#(c(x, s(y))), f#(c(s(x), y)) -> f#(c(x, s(y))))
    (f#(c(s(x), y)) -> f#(c(x, s(y))), f#(c(s(x), s(y))) -> g#(c(x, y)))}
   SCCS:
    Scc:
     {   f#(c(s(x), y)) -> f#(c(x, s(y))),
      f#(c(s(x), s(y))) -> g#(c(x, y)),
         g#(c(x, s(y))) -> g#(c(s(x), y)),
      g#(c(s(x), s(y))) -> f#(c(x, y))}
    SCC:
     Strict:
      {   f#(c(s(x), y)) -> f#(c(x, s(y))),
       f#(c(s(x), s(y))) -> g#(c(x, y)),
          g#(c(x, s(y))) -> g#(c(s(x), y)),
       g#(c(s(x), s(y))) -> f#(c(x, y))}
     Weak:
     {   f(c(s(x), y)) -> f(c(x, s(y))),
      f(c(s(x), s(y))) -> g(c(x, y)),
         g(c(x, s(y))) -> g(c(s(x), y)),
      g(c(s(x), s(y))) -> f(c(x, y))}
     POLY:
      Argument Filtering:
       pi(g#) = 0, pi(g) = [], pi(s) = [0], pi(c) = [0,1], pi(f#) = 0, pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [c](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {f#(c(s(x), y)) -> f#(c(x, s(y))),
        g#(c(x, s(y))) -> g#(c(s(x), y))}
      Weak:
       {   f(c(s(x), y)) -> f(c(x, s(y))),
        f(c(s(x), s(y))) -> g(c(x, y)),
           g(c(x, s(y))) -> g(c(s(x), y)),
        g(c(s(x), s(y))) -> f(c(x, y))}
      EDG:
       {(g#(c(x, s(y))) -> g#(c(s(x), y)), g#(c(x, s(y))) -> g#(c(s(x), y)))
        (f#(c(s(x), y)) -> f#(c(x, s(y))), f#(c(s(x), y)) -> f#(c(x, s(y))))}
       SCCS:
        Scc:
         {g#(c(x, s(y))) -> g#(c(s(x), y))}
        Scc:
         {f#(c(s(x), y)) -> f#(c(x, s(y)))}
        SCC:
         Strict:
          {g#(c(x, s(y))) -> g#(c(s(x), y))}
         Weak:
         {   f(c(s(x), y)) -> f(c(x, s(y))),
          f(c(s(x), s(y))) -> g(c(x, y)),
             g(c(x, s(y))) -> g(c(s(x), y)),
          g(c(s(x), s(y))) -> f(c(x, y))}
         POLY:
          Argument Filtering:
           pi(g#) = 0, pi(g) = [], pi(s) = [0], pi(c) = 1, pi(f) = []
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {   f(c(s(x), y)) -> f(c(x, s(y))),
            f(c(s(x), s(y))) -> g(c(x, y)),
               g(c(x, s(y))) -> g(c(s(x), y)),
            g(c(s(x), s(y))) -> f(c(x, y))}
          Qed
        SCC:
         Strict:
          {f#(c(s(x), y)) -> f#(c(x, s(y)))}
         Weak:
         {   f(c(s(x), y)) -> f(c(x, s(y))),
          f(c(s(x), s(y))) -> g(c(x, y)),
             g(c(x, s(y))) -> g(c(s(x), y)),
          g(c(s(x), s(y))) -> f(c(x, y))}
         POLY:
          Argument Filtering:
           pi(g) = [], pi(s) = [0], pi(c) = 0, pi(f#) = 0, pi(f) = []
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {   f(c(s(x), y)) -> f(c(x, s(y))),
            f(c(s(x), s(y))) -> g(c(x, y)),
               g(c(x, s(y))) -> g(c(s(x), y)),
            g(c(s(x), s(y))) -> f(c(x, y))}
          Qed