YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a3(262) -> 263*
    a3(252) -> 253*
    a3(217) -> 218*
    a3(177) -> 178*
    a3(359) -> 360*
    a3(157) -> 158*
    a3(334) -> 335*
    a3(324) -> 325*
    a3(309) -> 310*
    a3(299) -> 300*
    a3(284) -> 285*
    a3(264) -> 265*
    a3(249) -> 250*
    a3(214) -> 215*
    a3(179) -> 180*
    a3(356) -> 357*
    a3(154) -> 155*
    a3(336) -> 337*
    a3(321) -> 322*
    a3(311) -> 312*
    a3(301) -> 302*
    a3(286) -> 287*
    a3(261) -> 262*
    a3(251) -> 252*
    a3(216) -> 217*
    a3(181) -> 182*
    a3(358) -> 359*
    a3(156) -> 157*
    a3(333) -> 334*
    a3(323) -> 324*
    a3(308) -> 309*
    a3(298) -> 299*
    a3(283) -> 284*
    a3(263) -> 264*
    a3(253) -> 254*
    a3(218) -> 219*
    a3(178) -> 179*
    a3(360) -> 361*
    a3(153) -> 154*
    a3(335) -> 336*
    a3(325) -> 326*
    a3(310) -> 311*
    a3(300) -> 301*
    a3(285) -> 286*
    a3(260) -> 261*
    a3(250) -> 251*
    a3(215) -> 216*
    a3(180) -> 181*
    a3(357) -> 358*
    a3(155) -> 156*
    a3(332) -> 333*
    a3(322) -> 323*
    a3(312) -> 313*
    a3(297) -> 298*
    a3(282) -> 283*
    b4(479) -> 480*
    b4(444) -> 445*
    b4(434) -> 435*
    b4(409) -> 410*
    b4(374) -> 375*
    b4(349) -> 350*
    b4(481) -> 482*
    b4(446) -> 447*
    b4(431) -> 432*
    b4(411) -> 412*
    b4(376) -> 377*
    b4(351) -> 352*
    b4(478) -> 479*
    b4(443) -> 444*
    b4(433) -> 434*
    b4(408) -> 409*
    b4(373) -> 374*
    b4(348) -> 349*
    b4(480) -> 481*
    b4(445) -> 446*
    b4(435) -> 436*
    b4(410) -> 411*
    b4(375) -> 376*
    b4(350) -> 351*
    b4(477) -> 478*
    b4(442) -> 443*
    b4(432) -> 433*
    b4(407) -> 408*
    b4(372) -> 373*
    b4(352) -> 353*
    a4(474) -> 475*
    a4(439) -> 440*
    a4(429) -> 430*
    a4(404) -> 405*
    a4(369) -> 370*
    a4(344) -> 345*
    a4(476) -> 477*
    a4(441) -> 442*
    a4(426) -> 427*
    a4(406) -> 407*
    a4(371) -> 372*
    a4(346) -> 347*
    a4(473) -> 474*
    a4(438) -> 439*
    a4(428) -> 429*
    a4(403) -> 404*
    a4(368) -> 369*
    a4(343) -> 344*
    a4(475) -> 476*
    a4(470) -> 471*
    a4(440) -> 441*
    a4(430) -> 431*
    a4(405) -> 406*
    a4(400) -> 401*
    a4(370) -> 371*
    a4(345) -> 346*
    a4(472) -> 473*
    a4(437) -> 438*
    a4(427) -> 428*
    a4(402) -> 403*
    a4(367) -> 368*
    a4(347) -> 348*
    a0(3) -> 3*
    b0(3) -> 3*
    b1(55) -> 56*
    b1(20) -> 21*
    b1(57) -> 58*
    b1(22) -> 23*
    b1(59) -> 60*
    b1(24) -> 25*
    b1(56) -> 57*
    b1(21) -> 22*
    b1(58) -> 59*
    b1(23) -> 24*
    a1(50) -> 51*
    a1(15) -> 16*
    a1(52) -> 53*
    a1(17) -> 18*
    a1(54) -> 55*
    a1(19) -> 20*
    a1(76) -> 77*
    a1(51) -> 52*
    a1(16) -> 17*
    a1(78) -> 79*
    a1(63) -> 64*
    a1(53) -> 54*
    a1(18) -> 19*
    b2(35) -> 36*
    b2(232) -> 233*
    b2(172) -> 173*
    b2(137) -> 138*
    b2(117) -> 118*
    b2(234) -> 235*
    b2(32) -> 33*
    b2(174) -> 175*
    b2(134) -> 135*
    b2(119) -> 120*
    b2(34) -> 35*
    b2(231) -> 232*
    b2(171) -> 172*
    b2(136) -> 137*
    b2(121) -> 122*
    b2(233) -> 234*
    b2(31) -> 32*
    b2(173) -> 174*
    b2(138) -> 139*
    b2(118) -> 119*
    b2(33) -> 34*
    b2(230) -> 231*
    b2(175) -> 176*
    b2(135) -> 136*
    b2(120) -> 121*
    a2(30) -> 31*
    a2(227) -> 228*
    a2(167) -> 168*
    a2(132) -> 133*
    a2(127) -> 128*
    a2(112) -> 113*
    a2(82) -> 83*
    a2(229) -> 230*
    a2(27) -> 28*
    a2(169) -> 170*
    a2(129) -> 130*
    a2(114) -> 115*
    a2(84) -> 85*
    a2(29) -> 30*
    a2(226) -> 227*
    a2(166) -> 167*
    a2(151) -> 152*
    a2(131) -> 132*
    a2(116) -> 117*
    a2(228) -> 229*
    a2(26) -> 27*
    a2(168) -> 169*
    a2(133) -> 134*
    a2(123) -> 124*
    a2(113) -> 114*
    a2(28) -> 29*
    a2(225) -> 226*
    a2(170) -> 171*
    a2(130) -> 131*
    a2(125) -> 126*
    a2(115) -> 116*
    b3(267) -> 268*
    b3(257) -> 258*
    b3(222) -> 223*
    b3(182) -> 183*
    b3(364) -> 365*
    b3(162) -> 163*
    b3(339) -> 340*
    b3(329) -> 330*
    b3(314) -> 315*
    b3(304) -> 305*
    b3(289) -> 290*
    b3(269) -> 270*
    b3(254) -> 255*
    b3(219) -> 220*
    b3(184) -> 185*
    b3(361) -> 362*
    b3(159) -> 160*
    b3(341) -> 342*
    b3(326) -> 327*
    b3(316) -> 317*
    b3(306) -> 307*
    b3(291) -> 292*
    b3(266) -> 267*
    b3(256) -> 257*
    b3(221) -> 222*
    b3(186) -> 187*
    b3(363) -> 364*
    b3(161) -> 162*
    b3(338) -> 339*
    b3(328) -> 329*
    b3(313) -> 314*
    b3(303) -> 304*
    b3(288) -> 289*
    b3(268) -> 269*
    b3(258) -> 259*
    b3(223) -> 224*
    b3(183) -> 184*
    b3(365) -> 366*
    b3(158) -> 159*
    b3(340) -> 341*
    b3(330) -> 331*
    b3(315) -> 316*
    b3(305) -> 306*
    b3(290) -> 291*
    b3(265) -> 266*
    b3(255) -> 256*
    b3(220) -> 221*
    b3(185) -> 186*
    b3(362) -> 363*
    b3(160) -> 161*
    b3(337) -> 338*
    b3(327) -> 328*
    b3(317) -> 318*
    b3(302) -> 303*
    b3(287) -> 288*
    3 -> 15*
    20 -> 129*
    21 -> 84*
    22 -> 112*
    23 -> 63,26
    24 -> 50*
    25 -> 16,17,18,3
    31 -> 214*
    32 -> 260*
    33 -> 153*
    34 -> 177,166
    35 -> 125*
    36 -> 130,29,20,19,18
    55 -> 151*
    56 -> 123*
    57 -> 127*
    58 -> 82,76
    59 -> 78*
    60 -> 16,17,3,18
    64 -> 16*
    77 -> 16*
    79 -> 16*
    83 -> 27*
    85 -> 27*
    118 -> 297*
    120 -> 225*
    122 -> 53*
    124 -> 27*
    126 -> 27*
    128 -> 27*
    139 -> 115*
    152 -> 27*
    159 -> 343*
    161 -> 321*
    163 -> 29*
    172 -> 308*
    174 -> 249*
    176 -> 130,131
    183 -> 470*
    185 -> 367*
    187 -> 215,133,132
    224 -> 156*
    231 -> 332*
    233 -> 282*
    235 -> 152*
    259 -> 133,134
    270 -> 180,169
    288 -> 426*
    290 -> 356*
    292 -> 30*
    307 -> 228*
    318 -> 252*
    327 -> 437*
    329 -> 400*
    331 -> 215*
    342 -> 285*
    353 -> 324*
    362 -> 472*
    364 -> 402*
    366 -> 216*
    377 -> 218*
    401 -> 368*
    412 -> 219*
    436 -> 359*
    447 -> 370*
    471 -> 438*
    482 -> 405*
  problem:
   
  Qed