YES
Time: 0.021748
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:
  DP:
   {  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)}
  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)}
  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 (1):
    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 (4):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [c](x0, x1) = x0 + x1,
       
       [f](x0) = 0,
       
       [s](x0) = x0 + 1,
       
       [g](x0) = x0 + 1,
       
       [f#](x0) = x0,
       
       [g#](x0) = x0
      Strict:
       g# c(s x, s y) -> f# c(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
       g# c(x, s y) -> g# c(s x, y)
       1 + 1x + 1y >= 1 + 1x + 1y
       f# c(s x, s y) -> g# c(x, y)
       2 + 1x + 1y >= 0 + 1x + 1y
       f# c(s x, y) -> f# c(x, s y)
       1 + 1x + 1y >= 1 + 1x + 1y
      Weak:
       
     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 (2):
       Scc:
        {g# c(x, s y) -> g# c(s x, y)}
       Scc:
        {f# c(s x, y) -> f# c(x, s y)}
       SCC (1):
        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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [c](x0, x1) = x0,
          
          [f](x0) = 0,
          
          [s](x0) = x0 + 1,
          
          [g](x0) = 0,
          
          [g#](x0) = x0
         Strict:
          g# c(x, s y) -> g# c(s x, y)
          1 + 0x + 1y >= 0 + 0x + 1y
         Weak:
          
        Qed
      SCC (1):
       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:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [c](x0, x1) = x0 + 1,
         
         [f](x0) = 0,
         
         [s](x0) = x0 + 1,
         
         [g](x0) = x0 + 1,
         
         [f#](x0) = x0
        Strict:
         f# c(s x, y) -> f# c(x, s y)
         2 + 1x + 0y >= 1 + 1x + 0y
        Weak:
         
       Qed