YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 7
  enrichment: match
  automaton:
   final states: {2,1}
   transitions:
    b3(167) -> 168*
    b3(169) -> 170*
    b3(134) -> 135*
    b3(89) -> 90*
    b3(191) -> 192*
    b3(136) -> 137*
    b3(116) -> 117*
    b3(91) -> 92*
    b3(178) -> 179*
    b3(163) -> 164*
    b3(138) -> 139*
    b3(118) -> 119*
    b3(295) -> 296*
    b3(93) -> 94*
    b3(165) -> 166*
    b3(140) -> 141*
    b3(120) -> 121*
    a4(252) -> 253*
    a4(247) -> 248*
    a4(237) -> 238*
    a4(232) -> 233*
    a4(187) -> 188*
    a4(314) -> 315*
    a4(309) -> 310*
    a4(304) -> 305*
    a4(249) -> 250*
    a4(234) -> 235*
    a4(219) -> 220*
    a4(214) -> 215*
    a4(311) -> 312*
    a4(306) -> 307*
    a4(251) -> 252*
    a4(236) -> 237*
    a4(216) -> 217*
    a4(186) -> 187*
    a4(181) -> 182*
    a4(313) -> 314*
    a4(253) -> 254*
    a4(238) -> 239*
    a4(218) -> 219*
    a4(183) -> 184*
    a4(315) -> 316*
    a4(305) -> 306*
    a4(300) -> 301*
    a4(220) -> 221*
    a4(185) -> 186*
    a4(302) -> 303*
    b4(217) -> 218*
    b4(399) -> 400*
    b4(182) -> 183*
    b4(299) -> 300*
    b4(184) -> 185*
    b4(326) -> 327*
    b4(301) -> 302*
    b4(246) -> 247*
    b4(231) -> 232*
    b4(328) -> 329*
    b4(308) -> 309*
    b4(303) -> 304*
    b4(293) -> 294*
    b4(248) -> 249*
    b4(233) -> 234*
    b4(213) -> 214*
    b4(310) -> 311*
    b4(250) -> 251*
    b4(240) -> 241*
    b4(235) -> 236*
    b4(215) -> 216*
    b4(180) -> 181*
    b4(312) -> 313*
    b4(297) -> 298*
    b0(2) -> 1*
    b0(1) -> 1*
    a5(359) -> 360*
    a5(344) -> 345*
    a5(324) -> 325*
    a5(289) -> 290*
    a5(279) -> 280*
    a5(274) -> 275*
    a5(346) -> 347*
    a5(336) -> 337*
    a5(331) -> 332*
    a5(276) -> 277*
    a5(358) -> 359*
    a5(353) -> 354*
    a5(333) -> 334*
    a5(323) -> 324*
    a5(318) -> 319*
    a5(288) -> 289*
    a5(283) -> 284*
    a5(278) -> 279*
    a5(355) -> 356*
    a5(345) -> 346*
    a5(340) -> 341*
    a5(335) -> 336*
    a5(320) -> 321*
    a5(285) -> 286*
    a5(280) -> 281*
    a5(357) -> 358*
    a5(342) -> 343*
    a5(337) -> 338*
    a5(322) -> 323*
    a5(287) -> 288*
    a0(2) -> 2*
    a0(1) -> 2*
    b5(282) -> 283*
    b5(277) -> 278*
    b5(354) -> 355*
    b5(339) -> 340*
    b5(334) -> 335*
    b5(319) -> 320*
    b5(284) -> 285*
    b5(401) -> 402*
    b5(356) -> 357*
    b5(341) -> 342*
    b5(321) -> 322*
    b5(286) -> 287*
    b5(343) -> 344*
    b5(273) -> 274*
    b5(450) -> 451*
    b5(330) -> 331*
    b5(275) -> 276*
    b5(352) -> 353*
    b5(332) -> 333*
    b5(317) -> 318*
    a1(10) -> 11*
    a1(5) -> 6*
    a1(7) -> 8*
    a1(9) -> 10*
    a1(11) -> 12*
    a6(459) -> 460*
    a6(429) -> 430*
    a6(424) -> 425*
    a6(419) -> 420*
    a6(379) -> 380*
    a6(426) -> 427*
    a6(421) -> 422*
    a6(458) -> 459*
    a6(453) -> 454*
    a6(428) -> 429*
    a6(378) -> 379*
    a6(373) -> 374*
    a6(455) -> 456*
    a6(430) -> 431*
    a6(420) -> 421*
    a6(415) -> 416*
    a6(375) -> 376*
    a6(457) -> 458*
    a6(417) -> 418*
    a6(377) -> 378*
    b1(35) -> 36*
    b1(57) -> 58*
    b1(59) -> 60*
    b1(4) -> 5*
    b1(31) -> 32*
    b1(6) -> 7*
    b1(8) -> 9*
    b6(454) -> 455*
    b6(414) -> 415*
    b6(374) -> 375*
    b6(456) -> 457*
    b6(416) -> 417*
    b6(376) -> 377*
    b6(423) -> 424*
    b6(418) -> 419*
    b6(465) -> 466*
    b6(425) -> 426*
    b6(452) -> 453*
    b6(427) -> 428*
    b6(372) -> 373*
    a2(75) -> 76*
    a2(40) -> 41*
    a2(77) -> 78*
    a2(42) -> 43*
    a2(79) -> 80*
    a2(44) -> 45*
    a2(78) -> 79*
    a2(73) -> 74*
    a2(43) -> 44*
    a2(38) -> 39*
    a7(474) -> 475*
    a7(473) -> 474*
    a7(468) -> 469*
    a7(470) -> 471*
    a7(472) -> 473*
    b2(87) -> 88*
    b2(72) -> 73*
    b2(37) -> 38*
    b2(74) -> 75*
    b2(39) -> 40*
    b2(81) -> 82*
    b2(76) -> 77*
    b2(41) -> 42*
    b2(85) -> 86*
    b7(469) -> 470*
    b7(471) -> 472*
    b7(467) -> 468*
    a3(172) -> 173*
    a3(142) -> 143*
    a3(137) -> 138*
    a3(122) -> 123*
    a3(117) -> 118*
    a3(92) -> 93*
    a3(139) -> 140*
    a3(119) -> 120*
    a3(94) -> 95*
    a3(171) -> 172*
    a3(166) -> 167*
    a3(141) -> 142*
    a3(121) -> 122*
    a3(96) -> 97*
    a3(168) -> 169*
    a3(143) -> 144*
    a3(123) -> 124*
    a3(170) -> 171*
    a3(95) -> 96*
    a3(90) -> 91*
    1 -> 31*
    2 -> 4*
    9 -> 85*
    10 -> 37*
    11 -> 81,35
    12 -> 5,7,1
    32 -> 5*
    36 -> 5*
    42 -> 89*
    43 -> 87,59
    44 -> 163,72,57
    45 -> 75,5,1,31,7
    58 -> 5*
    60 -> 5*
    77 -> 165*
    78 -> 134*
    79 -> 116*
    80 -> 38,9
    82 -> 73*
    86 -> 38*
    88 -> 38*
    94 -> 231*
    96 -> 328,136
    97 -> 139,7,75
    121 -> 240*
    122 -> 180*
    123 -> 178*
    124 -> 40,42
    135 -> 117*
    141 -> 293*
    142 -> 297,295
    143 -> 213,191
    144 -> 9,85,42,135,88,60,7,5,40,38,117
    164 -> 137*
    170 -> 299*
    172 -> 246*
    173 -> 119*
    179 -> 137*
    188 -> 92*
    192 -> 137*
    218 -> 330*
    219 -> 282*
    220 -> 308*
    221 -> 121*
    236 -> 352*
    238 -> 339,326
    239 -> 249,216,139
    241 -> 232*
    251 -> 317*
    253 -> 273*
    254 -> 298,296,117,181
    278 -> 450*
    279 -> 401*
    280 -> 399*
    281 -> 121,240,185
    290 -> 234*
    294 -> 232*
    296 -> 117*
    298 -> 181*
    307 -> 249*
    316 -> 183*
    322 -> 452*
    324 -> 423*
    325 -> 276*
    327 -> 247*
    329 -> 247*
    338 -> 311*
    344 -> 414*
    346 -> 372*
    347 -> 283*
    360 -> 249,342
    380 -> 287*
    400 -> 309*
    402 -> 283*
    422 -> 375*
    428 -> 467*
    430 -> 465*
    431 -> 402*
    451 -> 331*
    460 -> 426*
    466 -> 373*
    475 -> 375*
  problem:
   
  Qed