YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {28,27,19,18,15,14,9,8,5}
   transitions:
    f0(27,18) -> 5*
    f0(28,5) -> 5*
    f0(18,5) -> 5*
    f0(27,28) -> 5*
    f0(28,9) -> 5*
    f0(8,5) -> 5*
    f0(18,9) -> 5*
    f0(8,9) -> 5*
    f0(28,15) -> 5*
    f0(18,15) -> 5*
    f0(28,19) -> 5*
    f0(8,15) -> 5*
    f0(18,19) -> 5*
    f0(8,19) -> 5*
    f0(28,27) -> 5*
    f0(18,27) -> 5*
    f0(19,8) -> 5*
    f0(14,8) -> 5*
    f0(8,27) -> 5*
    f0(9,8) -> 5*
    f0(19,14) -> 5*
    f0(14,14) -> 5*
    f0(9,14) -> 5*
    f0(19,18) -> 5*
    f0(14,18) -> 5*
    f0(9,18) -> 5*
    f0(15,5) -> 5*
    f0(5,5) -> 5*
    f0(19,28) -> 5*
    f0(14,28) -> 5*
    f0(15,9) -> 5*
    f0(9,28) -> 5*
    f0(5,9) -> 5*
    f0(15,15) -> 5*
    f0(5,15) -> 5*
    f0(15,19) -> 5*
    f0(5,19) -> 5*
    f0(15,27) -> 5*
    f0(5,27) -> 5*
    f0(27,5) -> 5*
    f0(27,9) -> 5*
    f0(27,15) -> 5*
    f0(27,19) -> 5*
    f0(27,27) -> 5*
    f0(28,8) -> 5*
    f0(18,8) -> 5*
    f0(8,8) -> 5*
    f0(28,14) -> 5*
    f0(18,14) -> 5*
    f0(28,18) -> 5*
    f0(8,14) -> 5*
    f0(18,18) -> 5*
    f0(8,18) -> 5*
    f0(19,5) -> 5*
    f0(14,5) -> 5*
    f0(28,28) -> 5*
    f0(9,5) -> 5*
    f0(18,28) -> 5*
    f0(19,9) -> 5*
    f0(14,9) -> 5*
    f0(8,28) -> 5*
    f0(9,9) -> 5*
    f0(19,15) -> 5*
    f0(14,15) -> 5*
    f0(9,15) -> 5*
    f0(19,19) -> 5*
    f0(14,19) -> 5*
    f0(9,19) -> 5*
    f0(19,27) -> 5*
    f0(14,27) -> 5*
    f0(15,8) -> 5*
    f0(9,27) -> 5*
    f0(5,8) -> 5*
    f0(15,14) -> 5*
    f0(5,14) -> 5*
    f0(15,18) -> 5*
    f0(5,18) -> 5*
    f0(15,28) -> 5*
    f0(5,28) -> 5*
    f0(27,8) -> 5*
    f0(27,14) -> 5*
    c1(15) -> 5*
    c1(5) -> 5*
    c1(27) -> 5*
    c1(19) -> 5*
    c1(14) -> 5*
    c1(9) -> 5*
    c1(28) -> 5*
    c1(18) -> 5*
    c1(8) -> 5*
    f1(27,18) -> 5*
    f1(7,14) -> 5*
    f1(7,18) -> 5*
    f1(27,28) -> 5*
    f1(28,9) -> 5*
    f1(8,5) -> 5*
    f1(18,9) -> 5*
    f1(7,28) -> 5*
    f1(8,9) -> 5*
    f1(28,15) -> 5*
    f1(18,15) -> 5*
    f1(28,19) -> 5*
    f1(8,15) -> 5*
    f1(18,19) -> 5*
    f1(8,19) -> 5*
    f1(28,27) -> 5*
    f1(19,6) -> 5*
    f1(14,6) -> 5*
    f1(18,27) -> 5*
    f1(9,6) -> 5*
    f1(14,8) -> 5*
    f1(8,27) -> 5*
    f1(14,14) -> 5*
    f1(19,18) -> 5*
    f1(14,18) -> 5*
    f1(9,18) -> 5*
    f1(19,28) -> 5*
    f1(14,28) -> 5*
    f1(15,9) -> 5*
    f1(9,28) -> 5*
    f1(5,9) -> 5*
    f1(15,15) -> 5*
    f1(5,15) -> 5*
    f1(15,19) -> 5*
    f1(5,19) -> 5*
    f1(15,27) -> 5*
    f1(5,27) -> 5*
    f1(27,9) -> 5*
    f1(7,5) -> 5*
    f1(7,9) -> 5*
    f1(27,15) -> 5*
    f1(27,19) -> 5*
    f1(7,15) -> 5*
    f1(7,19) -> 5*
    f1(28,6) -> 5*
    f1(27,27) -> 5*
    f1(18,6) -> 5*
    f1(8,6) -> 5*
    f1(7,27) -> 5*
    f1(8,8) -> 5*
    f1(28,18) -> 5*
    f1(8,14) -> 5*
    f1(18,18) -> 5*
    f1(8,18) -> 5*
    f1(14,5) -> 5*
    f1(28,28) -> 5*
    f1(18,28) -> 5*
    f1(19,9) -> 5*
    f1(14,9) -> 5*
    f1(8,28) -> 5*
    f1(9,9) -> 5*
    f1(19,15) -> 5*
    f1(14,15) -> 5*
    f1(9,15) -> 5*
    f1(19,19) -> 5*
    f1(14,19) -> 5*
    f1(9,19) -> 5*
    f1(15,6) -> 5*
    f1(19,27) -> 5*
    f1(14,27) -> 5*
    f1(5,6) -> 5*
    f1(9,27) -> 5*
    f1(15,18) -> 5*
    f1(5,18) -> 5*
    f1(15,28) -> 5*
    f1(5,28) -> 5*
    f1(27,6) -> 5*
    f1(7,8) -> 5*
    s1(15) -> 8*
    s1(5) -> 8*,5,7
    s1(27) -> 8*
    s1(19) -> 8*
    s1(14) -> 8*
    s1(9) -> 8*
    s1(28) -> 8*
    s1(18) -> 8*
    s1(8) -> 8*
    c2(9) -> 5*
    c2(8) -> 5*
    f2(27,18) -> 5*
    f2(27,28) -> 5*
    f2(28,11) -> 5*
    f2(18,11) -> 5*
    f2(28,15) -> 5*
    f2(18,15) -> 5*
    f2(28,19) -> 5*
    f2(8,15) -> 5*
    f2(18,19) -> 5*
    f2(8,19) -> 5*
    f2(28,27) -> 5*
    f2(18,27) -> 5*
    f2(14,8) -> 5*
    f2(8,27) -> 5*
    f2(14,10) -> 5*
    f2(19,12) -> 5*
    f2(14,12) -> 5*
    f2(9,12) -> 5*
    f2(14,14) -> 5*
    f2(19,18) -> 5*
    f2(14,18) -> 5*
    f2(9,18) -> 5*
    f2(19,28) -> 5*
    f2(14,28) -> 5*
    f2(9,28) -> 5*
    f2(15,11) -> 5*
    f2(15,15) -> 5*
    f2(5,15) -> 5*
    f2(15,19) -> 5*
    f2(5,19) -> 5*
    f2(15,27) -> 5*
    f2(5,27) -> 5*
    f2(27,11) -> 5*
    f2(27,15) -> 5*
    f2(27,19) -> 5*
    f2(27,27) -> 5*
    f2(13,8) -> 5*
    f2(28,12) -> 5*
    f2(8,10) -> 5*
    f2(18,12) -> 5*
    f2(8,12) -> 5*
    f2(13,14) -> 5*
    f2(28,18) -> 5*
    f2(18,18) -> 5*
    f2(8,18) -> 5*
    f2(28,28) -> 5*
    f2(18,28) -> 5*
    f2(8,28) -> 5*
    f2(19,11) -> 5*
    f2(9,11) -> 5*
    f2(19,15) -> 5*
    f2(14,15) -> 5*
    f2(9,15) -> 5*
    f2(19,19) -> 5*
    f2(14,19) -> 5*
    f2(9,19) -> 5*
    f2(19,27) -> 5*
    f2(14,27) -> 5*
    f2(9,27) -> 5*
    f2(15,12) -> 5*
    f2(5,12) -> 5*
    f2(15,18) -> 5*
    f2(5,18) -> 5*
    f2(15,28) -> 5*
    f2(5,28) -> 5*
    f2(27,12) -> 5*
    s2(14) -> 8,14*
    s2(8) -> 8,14*,13
    a2(15) -> 18*
    a2(5) -> 9,15*,6,5,12
    a2(27) -> 18*
    a2(19) -> 18*
    a2(14) -> 15*
    a2(9) -> 9,18*,11
    a2(28) -> 18*
    a2(18) -> 18*
    a2(8) -> 15*
    c3(15) -> 5*
    c3(27) -> 5*
    c3(19) -> 5*
    c3(14) -> 5*
    c3(28) -> 5*
    c3(18) -> 5*
    f3(8,20) -> 5*
    f3(8,28) -> 5*
    f3(14,21) -> 5*
    f3(14,27) -> 5*
    a3(14) -> 19,15,27*,21
    a3(8) -> 19,9,15,28*,10,20
  problem:
   
  Qed