YES(?,O(n^1))
TRS:
 {
  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)))))))))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    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)))))))))
   }
  BOUND:
   Bound: match(-raise)-bounded by 3
   Automaton:
    {
           b_3() -> 39*
           b_2() -> 13*
           b_1() -> 3*
           b_0() -> 1*
           a_3() -> 38*
           a_2() -> 12*
           a_1() -> 2*
           a_0() -> 1*
     f_3(39, 54) -> 55*
     f_3(39, 51) -> 52*
     f_3(39, 46) -> 47*
     f_3(39, 43) -> 44*
     f_3(39, 19) -> 48*
     f_3(39, 16) -> 40*
     f_3(38, 55) -> 46 | 28
     f_3(38, 53) -> 54*
     f_3(38, 52) -> 53*
     f_3(38, 50) -> 51*
     f_3(38, 49) -> 50*
     f_3(38, 48) -> 49*
     f_3(38, 47) -> 43 | 25
     f_3(38, 45) -> 46*
     f_3(38, 44) -> 45*
     f_3(38, 42) -> 43*
     f_3(38, 41) -> 42*
     f_3(38, 40) -> 41*
     f_2(13, 37) -> 30*
     f_2(13, 36) -> 37*
     f_2(13, 33) -> 34*
     f_2(13, 29) -> 22*
     f_2(13, 28) -> 29*
     f_2(13, 25) -> 26*
     f_2(13, 21) -> 14*
     f_2(13, 20) -> 21*
     f_2(13, 19) -> 30*
     f_2(13, 17) -> 18*
     f_2(13, 16) -> 22*
     f_2(13, 11) -> 14*
      f_2(13, 9) -> 30*
      f_2(13, 8) -> 14*
      f_2(13, 6) -> 22*
      f_2(13, 5) -> 14*
      f_2(13, 4) -> 14*
     f_2(12, 37) -> 28 | 10
     f_2(12, 35) -> 36*
     f_2(12, 34) -> 35*
     f_2(12, 32) -> 33*
     f_2(12, 31) -> 32*
     f_2(12, 30) -> 31*
     f_2(12, 29) -> 25 | 7
     f_2(12, 27) -> 28*
     f_2(12, 26) -> 27*
     f_2(12, 24) -> 25*
     f_2(12, 23) -> 24*
     f_2(12, 22) -> 23*
     f_2(12, 21) -> 42 | 24 | 6
     f_2(12, 19) -> 20*
     f_2(12, 18) -> 19*
     f_2(12, 16) -> 17*
     f_2(12, 15) -> 16*
     f_2(12, 14) -> 15*
      f_1(3, 37) -> 4*
      f_1(3, 29) -> 4*
      f_1(3, 11) -> 4*
      f_1(3, 10) -> 11*
       f_1(3, 9) -> 4*
       f_1(3, 7) -> 8*
       f_1(3, 6) -> 4*
       f_1(3, 1) -> 4*
      f_1(2, 11) -> 24 | 6 | 1
       f_1(2, 9) -> 10*
       f_1(2, 8) -> 9*
       f_1(2, 6) -> 7*
       f_1(2, 5) -> 6*
       f_1(2, 4) -> 5*
       f_0(1, 1) -> 1*
    }
   Strict:
    {}
   Qed