YES
Trs:
 {f(s(X), X) -> f(X, a(X)),
  f(X, c(X)) -> f(s(X), X),
     f(X, X) -> c(X)}
 Comment:
  We consider a non-duplicating trs.
  BOUND:
   Automaton:
    {     a_3(q13) -> q18 | q15 | q14 | q10 | q7 | q4 | q3,
           a_3(q6) -> q18 | q15 | q14 | q10 | q7 | q4 | q3,
          a_2(q18) -> q14 | q10 | q7 | q4 | q3,
          a_2(q14) -> q14 | q10 | q7 | q4 | q3,
          a_2(q13) -> q14 | q10 | q7 | q4 | q3,
           a_2(q7) -> q14 | q10 | q7 | q4 | q3,
           a_2(q6) -> q14 | q10 | q7 | q4 | q3,
           a_2(q3) -> q14 | q10 | q7 | q4 | q3,
          a_1(q18) -> q7 | q4 | q3,
          a_1(q14) -> q7 | q4 | q3,
          a_1(q13) -> q7 | q4 | q3,
           a_1(q7) -> q7 | q4 | q3,
           a_1(q6) -> q7 | q4 | q3,
           a_1(q3) -> q7 | q4 | q3,
          a_0(q18) -> q3,
          a_0(q14) -> q3,
          a_0(q13) -> q3,
           a_0(q7) -> q3,
           a_0(q6) -> q3,
           a_0(q3) -> q3,
          s_2(q13) -> q13 | q12 | q6 | q5 | q3,
           s_2(q6) -> q13 | q12 | q6 | q5 | q3,
          s_1(q18) -> q6 | q5 | q3,
          s_1(q14) -> q6 | q5 | q3,
          s_1(q13) -> q6 | q5 | q3,
           s_1(q7) -> q6 | q5 | q3,
           s_1(q6) -> q6 | q5 | q3,
           s_1(q3) -> q6 | q5 | q3,
          s_0(q18) -> q3,
          s_0(q14) -> q3,
          s_0(q13) -> q3,
           s_0(q7) -> q3,
           s_0(q6) -> q3,
           s_0(q3) -> q3,
     f_3(q13, q18) -> q3,
     f_3(q13, q15) -> q3,
      f_3(q6, q18) -> q3,
      f_3(q6, q15) -> q3,
     f_2(q18, q18) -> q3,
     f_2(q18, q14) -> q3,
     f_2(q18, q10) -> q3,
     f_2(q14, q18) -> q3,
     f_2(q14, q14) -> q3,
     f_2(q14, q10) -> q3,
     f_2(q13, q18) -> q3,
     f_2(q13, q14) -> q3,
     f_2(q13, q13) -> q3,
     f_2(q13, q10) -> q3,
      f_2(q13, q6) -> q3,
     f_2(q12, q13) -> q3,
      f_2(q12, q6) -> q3,
      f_2(q7, q18) -> q3,
      f_2(q7, q14) -> q3,
      f_2(q7, q10) -> q3,
      f_2(q6, q18) -> q3,
      f_2(q6, q14) -> q3,
      f_2(q6, q10) -> q3,
      f_2(q3, q18) -> q3,
      f_2(q3, q14) -> q3,
      f_2(q3, q10) -> q3,
     f_1(q18, q18) -> q3,
     f_1(q18, q14) -> q3,
      f_1(q18, q7) -> q3,
      f_1(q18, q4) -> q3,
     f_1(q14, q18) -> q3,
     f_1(q14, q14) -> q3,
      f_1(q14, q7) -> q3,
      f_1(q14, q4) -> q3,
     f_1(q13, q18) -> q3,
     f_1(q13, q14) -> q3,
     f_1(q13, q13) -> q3,
      f_1(q13, q7) -> q3,
      f_1(q13, q6) -> q3,
      f_1(q13, q4) -> q3,
      f_1(q13, q3) -> q3,
      f_1(q7, q18) -> q3,
      f_1(q7, q14) -> q3,
       f_1(q7, q7) -> q3,
       f_1(q7, q4) -> q3,
      f_1(q6, q18) -> q3,
      f_1(q6, q14) -> q3,
      f_1(q6, q13) -> q3,
       f_1(q6, q7) -> q3,
       f_1(q6, q6) -> q3,
       f_1(q6, q4) -> q3,
       f_1(q6, q3) -> q3,
      f_1(q5, q18) -> q3,
      f_1(q5, q14) -> q3,
      f_1(q5, q13) -> q3,
       f_1(q5, q7) -> q3,
       f_1(q5, q6) -> q3,
       f_1(q5, q3) -> q3,
      f_1(q3, q18) -> q3,
      f_1(q3, q14) -> q3,
       f_1(q3, q7) -> q3,
       f_1(q3, q4) -> q3,
     f_0(q18, q18) -> q3,
     f_0(q18, q14) -> q3,
     f_0(q18, q13) -> q3,
      f_0(q18, q7) -> q3,
      f_0(q18, q6) -> q3,
      f_0(q18, q3) -> q3,
     f_0(q14, q18) -> q3,
     f_0(q14, q14) -> q3,
     f_0(q14, q13) -> q3,
      f_0(q14, q7) -> q3,
      f_0(q14, q6) -> q3,
      f_0(q14, q3) -> q3,
     f_0(q13, q18) -> q3,
     f_0(q13, q14) -> q3,
     f_0(q13, q13) -> q3,
      f_0(q13, q7) -> q3,
      f_0(q13, q6) -> q3,
      f_0(q13, q3) -> q3,
      f_0(q7, q18) -> q3,
      f_0(q7, q14) -> q3,
      f_0(q7, q13) -> q3,
       f_0(q7, q7) -> q3,
       f_0(q7, q6) -> q3,
       f_0(q7, q3) -> q3,
      f_0(q6, q18) -> q3,
      f_0(q6, q14) -> q3,
      f_0(q6, q13) -> q3,
       f_0(q6, q7) -> q3,
       f_0(q6, q6) -> q3,
       f_0(q6, q3) -> q3,
      f_0(q3, q18) -> q3,
      f_0(q3, q14) -> q3,
      f_0(q3, q13) -> q3,
       f_0(q3, q7) -> q3,
       f_0(q3, q6) -> q3,
       f_0(q3, q3) -> q3,
          c_3(q18) -> q3,
          c_3(q14) -> q3,
          c_3(q13) -> q3,
          c_2(q18) -> q3,
          c_2(q14) -> q3,
          c_2(q13) -> q3,
           c_2(q7) -> q3,
           c_2(q6) -> q3,
          c_1(q18) -> q3,
          c_1(q14) -> q3,
          c_1(q13) -> q3,
           c_1(q7) -> q3,
           c_1(q6) -> q3,
           c_1(q3) -> q3,
          c_0(q18) -> q3,
          c_0(q14) -> q3,
          c_0(q13) -> q3,
           c_0(q7) -> q3,
           c_0(q6) -> q3,
           c_0(q3) -> q3}
   Strict:
   {}
   Qed