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