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: {25,24,19,18,15,14,9,8,5}
   transitions:
    f0(18,5) -> 5*
    f0(8,5) -> 5*
    f0(18,9) -> 5*
    f0(8,9) -> 5*
    f0(18,15) -> 5*
    f0(8,15) -> 5*
    f0(18,19) -> 5*
    f0(8,19) -> 5*
    f0(18,25) -> 5*
    f0(24,8) -> 5*
    f0(8,25) -> 5*
    f0(19,8) -> 5*
    f0(14,8) -> 5*
    f0(9,8) -> 5*
    f0(24,14) -> 5*
    f0(19,14) -> 5*
    f0(14,14) -> 5*
    f0(9,14) -> 5*
    f0(24,18) -> 5*
    f0(19,18) -> 5*
    f0(14,18) -> 5*
    f0(9,18) -> 5*
    f0(24,24) -> 5*
    f0(25,5) -> 5*
    f0(19,24) -> 5*
    f0(14,24) -> 5*
    f0(15,5) -> 5*
    f0(9,24) -> 5*
    f0(25,9) -> 5*
    f0(5,5) -> 5*
    f0(15,9) -> 5*
    f0(5,9) -> 5*
    f0(25,15) -> 5*
    f0(15,15) -> 5*
    f0(25,19) -> 5*
    f0(5,15) -> 5*
    f0(15,19) -> 5*
    f0(5,19) -> 5*
    f0(25,25) -> 5*
    f0(15,25) -> 5*
    f0(5,25) -> 5*
    f0(18,8) -> 5*
    f0(8,8) -> 5*
    f0(18,14) -> 5*
    f0(8,14) -> 5*
    f0(18,18) -> 5*
    f0(8,18) -> 5*
    f0(24,5) -> 5*
    f0(18,24) -> 5*
    f0(19,5) -> 5*
    f0(14,5) -> 5*
    f0(8,24) -> 5*
    f0(9,5) -> 5*
    f0(24,9) -> 5*
    f0(19,9) -> 5*
    f0(14,9) -> 5*
    f0(9,9) -> 5*
    f0(24,15) -> 5*
    f0(19,15) -> 5*
    f0(14,15) -> 5*
    f0(9,15) -> 5*
    f0(24,19) -> 5*
    f0(19,19) -> 5*
    f0(14,19) -> 5*
    f0(9,19) -> 5*
    f0(24,25) -> 5*
    f0(19,25) -> 5*
    f0(14,25) -> 5*
    f0(25,8) -> 5*
    f0(9,25) -> 5*
    f0(15,8) -> 5*
    f0(5,8) -> 5*
    f0(25,14) -> 5*
    f0(15,14) -> 5*
    f0(25,18) -> 5*
    f0(5,14) -> 5*
    f0(15,18) -> 5*
    f0(5,18) -> 5*
    f0(25,24) -> 5*
    f0(15,24) -> 5*
    f0(5,24) -> 5*
    s0(25) -> 5*
    s0(15) -> 5*
    s0(5) -> 5*
    s0(24) -> 5*
    s0(19) -> 5*
    s0(14) -> 5*
    s0(9) -> 5*
    s0(18) -> 5*
    s0(8) -> 5*
    a0(25) -> 5*
    a0(15) -> 5*
    a0(5) -> 5*
    a0(24) -> 5*
    a0(19) -> 5*
    a0(14) -> 5*
    a0(9) -> 5*
    a0(18) -> 5*
    a0(8) -> 5*
    c0(25) -> 5*
    c0(15) -> 5*
    c0(5) -> 5*
    c0(24) -> 5*
    c0(19) -> 5*
    c0(14) -> 5*
    c0(9) -> 5*
    c0(18) -> 5*
    c0(8) -> 5*
    c1(25) -> 5*
    c1(15) -> 5*
    c1(5) -> 5*
    c1(24) -> 5*
    c1(19) -> 5*
    c1(14) -> 5*
    c1(9) -> 5*
    c1(18) -> 5*
    c1(8) -> 5*
    f1(7,14) -> 5*
    f1(7,18) -> 5*
    f1(7,24) -> 5*
    f1(8,5) -> 5*
    f1(18,9) -> 5*
    f1(8,9) -> 5*
    f1(18,15) -> 5*
    f1(8,15) -> 5*
    f1(18,19) -> 5*
    f1(8,19) -> 5*
    f1(24,6) -> 5*
    f1(18,25) -> 5*
    f1(19,6) -> 5*
    f1(14,6) -> 5*
    f1(8,25) -> 5*
    f1(9,6) -> 5*
    f1(14,8) -> 5*
    f1(14,14) -> 5*
    f1(24,18) -> 5*
    f1(19,18) -> 5*
    f1(14,18) -> 5*
    f1(9,18) -> 5*
    f1(24,24) -> 5*
    f1(19,24) -> 5*
    f1(14,24) -> 5*
    f1(9,24) -> 5*
    f1(25,9) -> 5*
    f1(15,9) -> 5*
    f1(5,9) -> 5*
    f1(25,15) -> 5*
    f1(15,15) -> 5*
    f1(25,19) -> 5*
    f1(5,15) -> 5*
    f1(15,19) -> 5*
    f1(5,19) -> 5*
    f1(25,25) -> 5*
    f1(15,25) -> 5*
    f1(5,25) -> 5*
    f1(7,5) -> 5*
    f1(7,9) -> 5*
    f1(7,15) -> 5*
    f1(7,19) -> 5*
    f1(18,6) -> 5*
    f1(7,25) -> 5*
    f1(8,6) -> 5*
    f1(8,8) -> 5*
    f1(8,14) -> 5*
    f1(18,18) -> 5*
    f1(8,18) -> 5*
    f1(18,24) -> 5*
    f1(14,5) -> 5*
    f1(8,24) -> 5*
    f1(24,9) -> 5*
    f1(19,9) -> 5*
    f1(14,9) -> 5*
    f1(9,9) -> 5*
    f1(24,15) -> 5*
    f1(19,15) -> 5*
    f1(14,15) -> 5*
    f1(9,15) -> 5*
    f1(24,19) -> 5*
    f1(19,19) -> 5*
    f1(14,19) -> 5*
    f1(9,19) -> 5*
    f1(24,25) -> 5*
    f1(25,6) -> 5*
    f1(19,25) -> 5*
    f1(14,25) -> 5*
    f1(15,6) -> 5*
    f1(9,25) -> 5*
    f1(5,6) -> 5*
    f1(25,18) -> 5*
    f1(15,18) -> 5*
    f1(5,18) -> 5*
    f1(25,24) -> 5*
    f1(15,24) -> 5*
    f1(5,24) -> 5*
    f1(7,8) -> 5*
    s1(25) -> 5,8*
    s1(15) -> 5,8*
    s1(5) -> 8*,5,7
    s1(24) -> 5,8*
    s1(19) -> 5,8*
    s1(14) -> 5,8*
    s1(9) -> 5,8*
    s1(18) -> 5,8*
    s1(8) -> 5,8*
    a1(25) -> 5,9*
    a1(15) -> 5,9*
    a1(5) -> 9*,5,6
    a1(24) -> 5,9*
    a1(19) -> 5,9*
    a1(14) -> 5,9*
    a1(9) -> 5,9*
    a1(18) -> 5,9*
    a1(8) -> 5,9*
    c2(25) -> 5*
    c2(15) -> 5*
    c2(24) -> 5*
    c2(19) -> 5*
    c2(14) -> 5*
    c2(9) -> 5*
    c2(18) -> 5*
    c2(8) -> 5*
    f2(18,11) -> 5*
    f2(18,15) -> 5*
    f2(8,15) -> 5*
    f2(18,19) -> 5*
    f2(8,19) -> 5*
    f2(18,25) -> 5*
    f2(8,25) -> 5*
    f2(14,8) -> 5*
    f2(24,12) -> 5*
    f2(14,10) -> 5*
    f2(19,12) -> 5*
    f2(14,12) -> 5*
    f2(9,12) -> 5*
    f2(14,14) -> 5*
    f2(24,18) -> 5*
    f2(19,18) -> 5*
    f2(14,18) -> 5*
    f2(9,18) -> 5*
    f2(24,24) -> 5*
    f2(19,24) -> 5*
    f2(14,24) -> 5*
    f2(9,24) -> 5*
    f2(25,11) -> 5*
    f2(15,11) -> 5*
    f2(25,15) -> 5*
    f2(15,15) -> 5*
    f2(25,19) -> 5*
    f2(5,15) -> 5*
    f2(15,19) -> 5*
    f2(5,19) -> 5*
    f2(25,25) -> 5*
    f2(15,25) -> 5*
    f2(5,25) -> 5*
    f2(13,8) -> 5*
    f2(8,10) -> 5*
    f2(18,12) -> 5*
    f2(8,12) -> 5*
    f2(13,14) -> 5*
    f2(18,18) -> 5*
    f2(8,18) -> 5*
    f2(18,24) -> 5*
    f2(8,24) -> 5*
    f2(24,11) -> 5*
    f2(19,11) -> 5*
    f2(9,11) -> 5*
    f2(24,15) -> 5*
    f2(19,15) -> 5*
    f2(14,15) -> 5*
    f2(9,15) -> 5*
    f2(24,19) -> 5*
    f2(19,19) -> 5*
    f2(14,19) -> 5*
    f2(9,19) -> 5*
    f2(24,25) -> 5*
    f2(19,25) -> 5*
    f2(14,25) -> 5*
    f2(9,25) -> 5*
    f2(25,12) -> 5*
    f2(15,12) -> 5*
    f2(5,12) -> 5*
    f2(25,18) -> 5*
    f2(15,18) -> 5*
    f2(5,18) -> 5*
    f2(25,24) -> 5*
    f2(15,24) -> 5*
    f2(5,24) -> 5*
    s2(14) -> 8,5,14*
    s2(8) -> 8,14*,5,13
    a2(25) -> 9,5,18*
    a2(15) -> 9,5,18*
    a2(5) -> 9,15*,6,5,12
    a2(24) -> 9,5,18*
    a2(19) -> 9,5,18*
    a2(14) -> 9,5,19*
    a2(9) -> 9,18*,5,11
    a2(18) -> 9,5,18*
    a2(8) -> 9,19*,5,10
    c3(25) -> 5*
    c3(15) -> 5*
    c3(24) -> 5*
    c3(19) -> 5*
    c3(14) -> 5*
    c3(18) -> 5*
    f3(8,25) -> 5*
    f3(14,24) -> 5*
    f3(8,20) -> 5*
    f3(14,21) -> 5*
    a3(14) -> 9,19,24*,5,21
    a3(8) -> 9,19,25*,10,5,20
  problem:
   
  Qed