YES(?,O(n^1))
TRS:
 {
  f(a(), a()) -> f(a(), b()),
  f(a(), b()) -> f(s a(), c()),
  f(s X, c()) -> f(X, c()),
  f(c(), c()) -> f(a(), a())
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    f(a(), a()) -> f(a(), b()),
    f(a(), b()) -> f(s a(), c()),
    f(s X, c()) -> f(X, c()),
    f(c(), c()) -> f(a(), a())
   }
  BOUND:
   Bound: match(-raise)-bounded by 4
   Automaton:
    {
         c_4() -> 6*
         c_3() -> 4*
         c_2() -> 3*
         c_1() -> 2*
         c_0() -> 1*
        s_3(5) -> 1*
        s_2(1) -> 1*
        s_1(1) -> 1*
        s_0(1) -> 1*
         b_2() -> 3*
         b_1() -> 2*
         b_0() -> 1*
         a_3() -> 5*
         a_2() -> 1*
         a_1() -> 2 | 1
         a_0() -> 1*
     f_4(5, 6) -> 1*
     f_3(5, 4) -> 1*
     f_3(1, 4) -> 1*
     f_2(5, 3) -> 1*
     f_2(1, 3) -> 1*
     f_1(5, 2) -> 1*
     f_1(1, 2) -> 1*
     f_0(1, 1) -> 1*
    }
   Strict:
    {}
   Qed