YES

Problem:
 f(s(X),X) -> f(X,a(X))
 f(X,c(X)) -> f(s(X),X)
 f(X,X) -> c(X)

Proof:
 DP Processor:
  DPs:
   f#(s(X),X) -> f#(X,a(X))
   f#(X,c(X)) -> f#(s(X),X)
  TRS:
   f(s(X),X) -> f(X,a(X))
   f(X,c(X)) -> f(s(X),X)
   f(X,X) -> c(X)
  Usable Rule Processor:
   DPs:
    f#(s(X),X) -> f#(X,a(X))
    f#(X,c(X)) -> f#(s(X),X)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [f#](x0, x1) = -8x0 + x1 + 0,
     
     [c](x0) = 5x0 + 3,
     
     [a](x0) = -8x0 + 0,
     
     [s](x0) = x0 + 10
    orientation:
     f#(s(X),X) = X + 2 >= -8X + 0 = f#(X,a(X))
     
     f#(X,c(X)) = 5X + 3 >= X + 2 = f#(s(X),X)
    problem:
     DPs:
      
     TRS:
      
    Qed