YES
Time: 0.000981
TRS:
 {f(x, c y) -> f(x, s f(y, y)),
  f(s x, y) -> f(x, s c y)}
 DP:
  DP:
   {f#(x, c y) -> f#(x, s f(y, y)),
    f#(x, c y) -> f#(y, y),
    f#(s x, y) -> f#(x, s c y)}
  TRS:
  {f(x, c y) -> f(x, s f(y, y)),
   f(s x, y) -> f(x, s c y)}
  EDG:
   {(f#(x, c y) -> f#(y, y), f#(s x, y) -> f#(x, s c y))
    (f#(x, c y) -> f#(y, y), f#(x, c y) -> f#(y, y))
    (f#(x, c y) -> f#(y, y), f#(x, c y) -> f#(x, s f(y, y)))
    (f#(s x, y) -> f#(x, s c y), f#(s x, y) -> f#(x, s c y))
    (f#(x, c y) -> f#(x, s f(y, y)), f#(s x, y) -> f#(x, s c y))}
   SCCS (2):
    Scc:
     {f#(s x, y) -> f#(x, s c y)}
    Scc:
     {f#(x, c y) -> f#(y, y)}
    SCC (1):
     Strict:
      {f#(s x, y) -> f#(x, s c y)}
     Weak:
     {f(x, c y) -> f(x, s f(y, y)),
      f(s x, y) -> f(x, s c y)}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {f#(x, c y) -> f#(y, y)}
     Weak:
     {f(x, c y) -> f(x, s f(y, y)),
      f(s x, y) -> f(x, s c y)}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {}
      Qed