YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 6
  enrichment: match
  automaton:
   final states: {4}
   transitions:
    b3(182) -> 183*
    b3(122) -> 123*
    b3(214) -> 215*
    b3(184) -> 185*
    b3(124) -> 125*
    b3(216) -> 217*
    b3(136) -> 137*
    b3(218) -> 219*
    b3(138) -> 139*
    b3(180) -> 181*
    b3(140) -> 141*
    b3(120) -> 121*
    c3(257) -> 258*
    c3(217) -> 218*
    c3(551) -> 552*
    c3(137) -> 138*
    c3(299) -> 300*
    c3(461) -> 462*
    c3(179) -> 180*
    c3(139) -> 140*
    c3(119) -> 120*
    c3(483) -> 484*
    c3(271) -> 272*
    c3(181) -> 182*
    c3(161) -> 162*
    c3(131) -> 132*
    c3(121) -> 122*
    c3(505) -> 506*
    c3(243) -> 244*
    c3(213) -> 214*
    c3(183) -> 184*
    c3(123) -> 124*
    c3(215) -> 216*
    c3(165) -> 166*
    c3(559) -> 560*
    c3(135) -> 136*
    a4(349) -> 350*
    a4(339) -> 340*
    a4(319) -> 320*
    a4(239) -> 240*
    a4(241) -> 242*
    a4(348) -> 349*
    a4(338) -> 339*
    a4(318) -> 319*
    a4(240) -> 241*
    a4(347) -> 348*
    a4(337) -> 338*
    a4(317) -> 318*
    b4(344) -> 345*
    b4(334) -> 335*
    b4(314) -> 315*
    b4(234) -> 235*
    b4(346) -> 347*
    b4(336) -> 337*
    b4(316) -> 317*
    b4(236) -> 237*
    b4(238) -> 239*
    b4(342) -> 343*
    b4(332) -> 333*
    b4(312) -> 313*
    b0(4) -> 4*
    c4(237) -> 238*
    c4(379) -> 380*
    c4(541) -> 542*
    c4(381) -> 382*
    c4(351) -> 352*
    c4(341) -> 342*
    c4(331) -> 332*
    c4(311) -> 312*
    c4(565) -> 566*
    c4(555) -> 556*
    c4(353) -> 354*
    c4(343) -> 344*
    c4(333) -> 334*
    c4(313) -> 314*
    c4(233) -> 234*
    c4(567) -> 568*
    c4(345) -> 346*
    c4(335) -> 336*
    c4(315) -> 316*
    c4(507) -> 508*
    c4(235) -> 236*
    c4(367) -> 368*
    c0(4) -> 4*
    a5(454) -> 455*
    a5(444) -> 445*
    a5(516) -> 517*
    a5(376) -> 377*
    a5(538) -> 539*
    a5(453) -> 454*
    a5(443) -> 444*
    a5(515) -> 516*
    a5(455) -> 456*
    a5(445) -> 446*
    a5(375) -> 376*
    a5(537) -> 538*
    a5(517) -> 518*
    a5(377) -> 378*
    a5(539) -> 540*
    a0(4) -> 4*
    b5(374) -> 375*
    b5(536) -> 537*
    b5(448) -> 449*
    b5(438) -> 439*
    b5(510) -> 511*
    b5(450) -> 451*
    b5(440) -> 441*
    b5(370) -> 371*
    b5(532) -> 533*
    b5(512) -> 513*
    b5(452) -> 453*
    b5(442) -> 443*
    b5(372) -> 373*
    b5(534) -> 535*
    b5(514) -> 515*
    a1(22) -> 23*
    a1(21) -> 22*
    a1(23) -> 24*
    c5(489) -> 490*
    c5(449) -> 450*
    c5(439) -> 440*
    c5(369) -> 370*
    c5(561) -> 562*
    c5(531) -> 532*
    c5(511) -> 512*
    c5(451) -> 452*
    c5(441) -> 442*
    c5(573) -> 574*
    c5(371) -> 372*
    c5(533) -> 534*
    c5(513) -> 514*
    c5(373) -> 374*
    c5(535) -> 536*
    c5(577) -> 578*
    c5(557) -> 558*
    c5(447) -> 448*
    c5(437) -> 438*
    c5(509) -> 510*
    b1(20) -> 21*
    b1(16) -> 17*
    b1(18) -> 19*
    a6(526) -> 527*
    a6(525) -> 526*
    a6(527) -> 528*
    c1(429) -> 430*
    c1(15) -> 16*
    c1(147) -> 148*
    c1(17) -> 18*
    c1(39) -> 40*
    c1(19) -> 20*
    c1(203) -> 204*
    c1(497) -> 498*
    c1(73) -> 74*
    c1(357) -> 358*
    c1(499) -> 500*
    b6(520) -> 521*
    b6(522) -> 523*
    b6(524) -> 525*
    a2(60) -> 61*
    a2(32) -> 33*
    a2(84) -> 85*
    a2(59) -> 60*
    a2(61) -> 62*
    a2(31) -> 32*
    a2(83) -> 84*
    a2(33) -> 34*
    a2(85) -> 86*
    c6(581) -> 582*
    c6(521) -> 522*
    c6(523) -> 524*
    c6(519) -> 520*
    b2(30) -> 31*
    b2(82) -> 83*
    b2(54) -> 55*
    b2(56) -> 57*
    b2(26) -> 27*
    b2(78) -> 79*
    b2(58) -> 59*
    b2(28) -> 29*
    b2(80) -> 81*
    c2(55) -> 56*
    c2(25) -> 26*
    c2(117) -> 118*
    c2(87) -> 88*
    c2(481) -> 482*
    c2(77) -> 78*
    c2(57) -> 58*
    c2(431) -> 432*
    c2(27) -> 28*
    c2(209) -> 210*
    c2(503) -> 504*
    c2(89) -> 90*
    c2(79) -> 80*
    c2(433) -> 434*
    c2(29) -> 30*
    c2(545) -> 546*
    c2(111) -> 112*
    c2(81) -> 82*
    c2(53) -> 54*
    c2(205) -> 206*
    c2(549) -> 550*
    c2(297) -> 298*
    a3(187) -> 188*
    a3(142) -> 143*
    a3(127) -> 128*
    a3(219) -> 220*
    a3(221) -> 222*
    a3(186) -> 187*
    a3(141) -> 142*
    a3(126) -> 127*
    a3(143) -> 144*
    a3(220) -> 221*
    a3(185) -> 186*
    a3(125) -> 126*
    4 -> 15*
    21 -> 77*
    22 -> 25*
    23 -> 39*
    24 -> 17,19,4
    31 -> 165,117
    32 -> 131,53
    33 -> 89,73
    34 -> 79,21,17,4,15,19
    40 -> 26*
    59 -> 161*
    60 -> 119,111
    61 -> 87*
    62 -> 79,17,4,15,19,21
    74 -> 16*
    83 -> 205*
    84 -> 135*
    85 -> 147*
    86 -> 19,4,17,29
    88 -> 78*
    90 -> 78*
    112 -> 26*
    118 -> 26*
    125 -> 311*
    126 -> 381,271
    127 -> 213*
    128 -> 31,117,165,121,79,19,4,17,21,29,27,83,81
    132 -> 120*
    141 -> 299,297
    142 -> 233,179
    143 -> 209,203
    144 -> 121,79,19,4,17,21,27
    148 -> 16*
    162 -> 120*
    166 -> 120*
    185 -> 353*
    186 -> 331,257
    187 -> 243*
    188 -> 31,117,21,17,4,15,19,77,81,79,83,165
    204 -> 16*
    206 -> 26*
    210 -> 78*
    219 -> 431*
    220 -> 351*
    221 -> 357*
    222 -> 123,57,19,4,17,29,139
    239 -> 447*
    240 -> 369*
    241 -> 367*
    242 -> 237,121,57,29,27,139,123,31,117,21,17,4,15,19,77,81,79,83,165,125
    244 -> 214*
    258 -> 120*
    272 -> 120*
    298 -> 26*
    300 -> 120*
    318 -> 461*
    320 -> 217*
    337 -> 549*
    338 -> 509,341
    339 -> 499*
    340 -> 57,19,4,17,29,139,237,123
    347 -> 483,481
    348 -> 437,379
    349 -> 433,429
    350 -> 27,21,17,4,15,19,77,79,121,313
    352 -> 342*
    354 -> 312*
    358 -> 16*
    368 -> 332*
    375 -> 577,555,551,545
    376 -> 581,489
    377 -> 565,505,503,497
    378 -> 449,125,121,31,311,313,83,79,81,19,4,17,21,29,27,205,123,315
    380 -> 234*
    382 -> 234*
    430 -> 16*
    432 -> 26*
    434 -> 78*
    443 -> 531*
    444 -> 557,541
    445 -> 507*
    446 -> 125,311,123,315,31,117,27,29,21,17,4,15,19,77,81,79,83,165,121,313,317
    454 -> 559*
    456 -> 335*
    462 -> 120*
    482 -> 26*
    484 -> 120*
    490 -> 438*
    498 -> 16*
    500 -> 16*
    504 -> 78*
    506 -> 214*
    508 -> 234*
    516 -> 519*
    518 -> 449*
    525 -> 573*
    527 -> 567*
    528 -> 453*
    538 -> 561*
    540 -> 237*
    542 -> 234*
    546 -> 26*
    550 -> 26*
    552 -> 120*
    556 -> 312*
    558 -> 438*
    560 -> 120*
    562 -> 510*
    566 -> 332*
    568 -> 234*
    574 -> 532*
    578 -> 448*
    582 -> 520*
  problem:
   
  Qed