YES(?,O(n^1))

Problem:
 f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) ->
 f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))))

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    f3(79,87) -> 88*
    f3(79,89) -> 90*
    f3(79,91) -> 92*
    f3(77,48) -> 78*
    f3(77,82) -> 83*
    f3(77,90) -> 91*
    f3(79,78) -> 80*
    f3(79,80) -> 81*
    f3(79,84) -> 85*
    f3(79,86) -> 93,41
    f3(79,88) -> 89*
    f3(79,92) -> 93*
    f3(79,94) -> 90,38
    f3(77,45) -> 87*
    f3(77,85) -> 86*
    f3(77,93) -> 94*
    f3(79,81) -> 82*
    f3(79,83) -> 84*
    f1(17,16) -> 18*
    f1(17,18) -> 19*
    f1(17,22) -> 23*
    f1(17,24) -> 37,19,4
    f1(15,19) -> 16*
    f1(15,23) -> 24*
    f1(17,19) -> 20*
    f1(17,21) -> 22*
    f1(15,4) -> 16*
    f1(15,20) -> 21*
    f1(15,22) -> 16*
    f1(15,24) -> 16*
    f1(15,34) -> 16*
    f1(15,42) -> 16*
    a3() -> 79*
    a1() -> 17*
    b3() -> 77*
    b1() -> 15*
    f2(27,26) -> 28*
    f2(27,28) -> 29*
    f2(27,32) -> 33*
    f2(27,34) -> 41,23
    f2(27,36) -> 37*
    f2(27,40) -> 41*
    f2(27,42) -> 38,20
    f2(27,44) -> 45*
    f2(27,48) -> 49*
    f2(27,50) -> 89,37,19
    f2(25,19) -> 35*
    f2(25,21) -> 43*
    f2(25,33) -> 34*
    f2(25,41) -> 42*
    f2(25,45) -> 35*
    f2(25,49) -> 50*
    f2(27,29) -> 30*
    f2(27,31) -> 32*
    f2(27,35) -> 36*
    f2(27,37) -> 38*
    f2(27,39) -> 40*
    f2(27,43) -> 44*
    f2(27,45) -> 46*
    f2(27,47) -> 48*
    f2(25,16) -> 43*
    f2(25,18) -> 43*
    f2(25,22) -> 26*
    f2(25,24) -> 43*
    f2(25,30) -> 31*
    f2(25,34) -> 26*
    f2(25,38) -> 39*
    f2(25,42) -> 35*
    f2(25,46) -> 47*
    f2(25,48) -> 26*
    f2(25,50) -> 43*
    f0(4,4) -> 4*
    a2() -> 27*
    a0() -> 4*
    b2() -> 25*
    b0() -> 4*
  problem:
   
  Qed