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: {19,4}
   transitions:
    f0(43,1) -> 4*
    f0(38,1) -> 4*
    f0(43,3) -> 4*
    f0(38,3) -> 4*
    f0(3,1) -> 4*
    f0(3,3) -> 4*
    f0(43,19) -> 4*
    f0(38,19) -> 4*
    f0(3,19) -> 4*
    f0(43,33) -> 4*
    f0(38,33) -> 4*
    f0(45,1) -> 4*
    f0(3,33) -> 4*
    f0(45,3) -> 4*
    f0(45,19) -> 4*
    f0(45,33) -> 4*
    f0(37,1) -> 4*
    f0(37,3) -> 4*
    f0(2,1) -> 4*
    f0(2,3) -> 4*
    f0(37,19) -> 4*
    f0(2,19) -> 4*
    f0(37,33) -> 4*
    f0(2,33) -> 4*
    f0(34,1) -> 4*
    f0(34,3) -> 4*
    f0(19,1) -> 4*
    f0(19,3) -> 4*
    f0(34,19) -> 4*
    f0(19,19) -> 4*
    f0(34,33) -> 4*
    f0(19,33) -> 4*
    f0(36,1) -> 4*
    f0(36,3) -> 4*
    f0(36,19) -> 4*
    f0(36,33) -> 4*
    c1(19) -> 4,19*
    c1(3) -> 19*,3,4
    f1(1,33) -> 4*
    f1(33,1) -> 4*
    f1(36,43) -> 4*
    f1(33,3) -> 4*
    f1(1,37) -> 4*
    f1(36,45) -> 4*
    f1(1,43) -> 4*
    f1(1,45) -> 4*
    f1(37,34) -> 4*
    f1(37,36) -> 4*
    f1(37,38) -> 4*
    f1(33,19) -> 4*
    f1(2,34) -> 4*
    f1(34,2) -> 4*
    f1(2,36) -> 4*
    f1(2,38) -> 4*
    f1(19,2) -> 4*
    f1(33,33) -> 4*
    f1(43,37) -> 4*
    f1(38,37) -> 4*
    f1(33,37) -> 4*
    f1(43,43) -> 4*
    f1(38,43) -> 4*
    f1(33,43) -> 4*
    f1(3,37) -> 4*
    f1(43,45) -> 4*
    f1(38,45) -> 4*
    f1(33,45) -> 4*
    f1(3,43) -> 4*
    f1(3,45) -> 4*
    f1(34,34) -> 4*
    f1(34,36) -> 4*
    f1(19,34) -> 4*
    f1(34,38) -> 4*
    f1(19,36) -> 4*
    f1(19,38) -> 4*
    f1(36,2) -> 4*
    f1(1,2) -> 4*
    f1(45,37) -> 4*
    f1(45,43) -> 4*
    f1(45,45) -> 4*
    f1(36,34) -> 4*
    f1(36,36) -> 4*
    f1(36,38) -> 4*
    f1(43,2) -> 4*
    f1(1,34) -> 4*
    f1(38,2) -> 4*
    f1(33,2) -> 4*
    f1(1,36) -> 4*
    f1(1,38) -> 4*
    f1(3,2) -> 4*
    f1(37,37) -> 4*
    f1(37,43) -> 4*
    f1(2,37) -> 4*
    f1(37,45) -> 4*
    f1(2,43) -> 4*
    f1(2,45) -> 4*
    f1(43,34) -> 4*
    f1(38,34) -> 4*
    f1(33,34) -> 4*
    f1(43,36) -> 4*
    f1(38,36) -> 4*
    f1(33,36) -> 4*
    f1(43,38) -> 4*
    f1(38,38) -> 4*
    f1(33,38) -> 4*
    f1(45,2) -> 4*
    f1(3,34) -> 4*
    f1(3,36) -> 4*
    f1(3,38) -> 4*
    f1(34,37) -> 4*
    f1(19,37) -> 4*
    f1(34,43) -> 4*
    f1(34,45) -> 4*
    f1(19,43) -> 4*
    f1(1,1) -> 4*
    f1(19,45) -> 4*
    f1(1,3) -> 4*
    f1(45,34) -> 4*
    f1(45,36) -> 4*
    f1(45,38) -> 4*
    f1(37,2) -> 4*
    f1(1,19) -> 4*
    f1(2,2) -> 4*
    f1(36,37) -> 4*
    s1(45) -> 1*
    s1(37) -> 1*
    s1(2) -> 1*
    s1(34) -> 1*
    s1(19) -> 1*
    s1(36) -> 1*
    s1(43) -> 1*
    s1(38) -> 1*
    s1(3) -> 1*
    c2(45) -> 4,19*
    c2(37) -> 4,19*
    c2(2) -> 3,19*,4
    c2(34) -> 19*
    c2(36) -> 4,19*
    c2(1) -> 3,19*,4
    c2(43) -> 4,19*
    c2(38) -> 4,19*
    c2(33) -> 19*
    f2(33,1) -> 4*
    f2(28,1) -> 4*
    f2(1,43) -> 4*
    f2(1,45) -> 4*
    f2(37,34) -> 4*
    f2(2,34) -> 4*
    f2(43,25) -> 4*
    f2(38,25) -> 4*
    f2(3,21) -> 4*
    f2(33,33) -> 4*
    f2(28,33) -> 4*
    f2(19,20) -> 4*
    f2(33,43) -> 4*
    f2(3,37) -> 4*
    f2(33,45) -> 4*
    f2(34,34) -> 4*
    f2(19,38) -> 4*
    f2(45,25) -> 4*
    f2(1,24) -> 4*
    f2(36,34) -> 4*
    f2(1,36) -> 4*
    f2(37,25) -> 4*
    f2(2,25) -> 4*
    f2(33,24) -> 4*
    f2(43,34) -> 4*
    f2(38,34) -> 4*
    f2(33,36) -> 4*
    f2(19,21) -> 4*
    f2(3,38) -> 4*
    f2(34,25) -> 4*
    f2(19,37) -> 4*
    f2(45,34) -> 4*
    f2(36,25) -> 4*
    s2(1) -> 33*,1,28
    s2(33) -> 33*
    a2(45) -> 34*
    a2(37) -> 34*
    a2(2) -> 34*,2,25
    a2(34) -> 34*
    a2(19) -> 38*,2,20
    a2(36) -> 34*
    a2(43) -> 34*
    a2(38) -> 34*
    a2(3) -> 37*,2,21
    c3(34) -> 19*,4
    c3(33) -> 19*,4
    f3(1,43) -> 4*
    f3(1,45) -> 4*
    f3(33,39) -> 4*
    f3(33,43) -> 4*
    f3(33,45) -> 4*
    f3(1,40) -> 4*
    f3(33,40) -> 4*
    a3(1) -> 36,43*,24,2,40
    a3(33) -> 36,45*,39
  problem:
   
  Qed