YES(?,O(n^1))

Problem:
 a(b(a(x1))) -> a(a(b(b(a(a(x1))))))
 b(a(a(b(x1)))) -> b(a(b(x1)))

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    a3(182) -> 183*
    a3(122) -> 123*
    a3(117) -> 118*
    a3(87) -> 88*
    a3(82) -> 83*
    a3(189) -> 190*
    a3(184) -> 185*
    a3(191) -> 192*
    a3(121) -> 122*
    a3(86) -> 87*
    a3(188) -> 189*
    a3(178) -> 179*
    a3(143) -> 144*
    a3(118) -> 119*
    a3(83) -> 84*
    a3(225) -> 226*
    a3(185) -> 186*
    a3(180) -> 181*
    a3(175) -> 176*
    a3(317) -> 318*
    b4(227) -> 228*
    b4(259) -> 260*
    b4(229) -> 230*
    b4(326) -> 327*
    b4(321) -> 322*
    b4(266) -> 267*
    b4(231) -> 232*
    b4(221) -> 222*
    b4(268) -> 269*
    b4(233) -> 234*
    b4(223) -> 224*
    b4(290) -> 291*
    b4(260) -> 261*
    b4(235) -> 236*
    b4(322) -> 323*
    a4(267) -> 268*
    a4(262) -> 263*
    a4(257) -> 258*
    a4(222) -> 223*
    a4(324) -> 325*
    a4(264) -> 265*
    a4(261) -> 262*
    a4(323) -> 324*
    a4(258) -> 259*
    a4(228) -> 229*
    a4(270) -> 271*
    a0(2) -> 1*
    a0(1) -> 1*
    b5(339) -> 340*
    b5(304) -> 305*
    b5(337) -> 338*
    b5(302) -> 303*
    b0(2) -> 2*
    b0(1) -> 2*
    a5(338) -> 339*
    a5(303) -> 304*
    b1(72) -> 73*
    b1(37) -> 38*
    b1(7) -> 8*
    b1(24) -> 25*
    b1(46) -> 47*
    b1(26) -> 27*
    b1(6) -> 7*
    a1(25) -> 26*
    a1(5) -> 6*
    a1(22) -> 23*
    a1(9) -> 10*
    a1(4) -> 5*
    a1(8) -> 9*
    b2(57) -> 58*
    b2(42) -> 43*
    b2(154) -> 155*
    b2(134) -> 135*
    b2(74) -> 75*
    b2(136) -> 137*
    b2(126) -> 127*
    b2(76) -> 77*
    b2(66) -> 67*
    b2(41) -> 42*
    b2(68) -> 69*
    b2(58) -> 59*
    b2(140) -> 141*
    a2(75) -> 76*
    a2(60) -> 61*
    a2(55) -> 56*
    a2(40) -> 41*
    a2(67) -> 68*
    a2(104) -> 105*
    a2(59) -> 60*
    a2(44) -> 45*
    a2(39) -> 40*
    a2(96) -> 97*
    a2(56) -> 57*
    a2(98) -> 99*
    a2(43) -> 44*
    b3(217) -> 218*
    b3(207) -> 208*
    b3(197) -> 198*
    b3(187) -> 188*
    b3(142) -> 143*
    b3(174) -> 175*
    b3(144) -> 145*
    b3(119) -> 120*
    b3(84) -> 85*
    b3(186) -> 187*
    b3(176) -> 177*
    b3(193) -> 194*
    b3(205) -> 206*
    b3(195) -> 196*
    b3(120) -> 121*
    b3(85) -> 86*
    1 -> 37,22
    2 -> 24,4
    4 -> 104*
    5 -> 72*
    7 -> 66*
    9 -> 55*
    10 -> 26,5,1
    22 -> 98*
    23 -> 46,5
    24 -> 134*
    25 -> 39*
    26 -> 74*
    27 -> 85,137,141,40,47,42,73,38,7,25,2
    37 -> 136*
    38 -> 25*
    42 -> 195*
    43 -> 191*
    44 -> 182,126
    45 -> 105,76,26,74,40,96,1,22,37,5
    47 -> 42*
    58 -> 174*
    59 -> 184*
    60 -> 154,117
    61 -> 41,105,76,5,72,40,26
    66 -> 217*
    67 -> 82*
    68 -> 142*
    69 -> 137,75,27,7,66,73,38,2,25
    72 -> 140*
    73 -> 25*
    77 -> 85,42,7
    85 -> 42,227
    86 -> 264*
    87 -> 193*
    88 -> 144,41,105,76,180,26,5,1,22,37,72,74,40
    97 -> 84*
    99 -> 83*
    105 -> 83*
    122 -> 197*
    123 -> 41,76
    126 -> 205*
    127 -> 38,2,4,24,73
    135 -> 40*
    137 -> 40*
    141 -> 40*
    145 -> 85,7,66,42
    154 -> 207*
    155 -> 27,38,7,2,4,24,66,25,39
    174 -> 221*
    176 -> 178*
    177 -> 187,141,40,77,75
    179 -> 119*
    181 -> 119*
    183 -> 118*
    187 -> 266*
    189 -> 257*
    190 -> 265,229,87,41,193,40,105
    192 -> 185*
    194 -> 187,225,85,137,141,27,47,73,2,38,39,40,77,75
    195 -> 231*
    196 -> 86*
    198 -> 77*
    205 -> 233*
    206 -> 86*
    207 -> 235*
    208 -> 86*
    218 -> 83*
    224 -> 120*
    226 -> 144*
    230 -> 260,145,85,7,42,195
    232 -> 228*
    234 -> 228*
    236 -> 228*
    260 -> 337*
    262 -> 290*
    263 -> 321,41,26,5,72,1,140,74,40,105,76,226
    265 -> 258*
    266 -> 302*
    268 -> 270*
    269 -> 230,194,225,77,27,75,187
    271 -> 259*
    291 -> 317,75,27,137,38,2,73,47,141,77,145,42,7,66,217,85,195,231
    305 -> 260*
    318 -> 84*
    324 -> 326*
    325 -> 318*
    327 -> 85,195,231
    340 -> 322*
  problem:
   
  Qed