YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(a(a(a(b(a(a(x1))))))) -> a(a(a(b(b(a(a(a(b(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     b3(656) -> 657*
     b3(434) -> 435*
     b3(404) -> 405*
     b3(344) -> 345*
     b3(319) -> 320*
     b3(516) -> 517*
     b3(314) -> 315*
     b3(486) -> 487*
     b3(254) -> 255*
     b3(234) -> 235*
     b3(224) -> 225*
     b3(386) -> 387*
     b3(376) -> 377*
     b3(568) -> 569*
     b3(154) -> 155*
     b3(351) -> 352*
     b3(346) -> 347*
     b3(523) -> 524*
     b3(518) -> 519*
     b3(296) -> 297*
     b3(615) -> 616*
     b3(610) -> 611*
     b3(176) -> 177*
     b3(171) -> 172*
     b3(166) -> 167*
     b3(318) -> 319*
     b3(440) -> 441*
     b3(435) -> 436*
     b3(430) -> 431*
     b3(400) -> 401*
     b3(350) -> 351*
     b3(522) -> 523*
     b3(290) -> 291*
     b3(462) -> 463*
     b3(255) -> 256*
     b3(654) -> 655*
     b3(250) -> 251*
     b3(235) -> 236*
     b3(230) -> 231*
     b3(225) -> 226*
     b3(220) -> 221*
     b3(614) -> 615*
     b3(387) -> 388*
     b3(382) -> 383*
     b3(170) -> 171*
     b3(569) -> 570*
     b3(564) -> 565*
     b3(160) -> 161*
     b3(155) -> 156*
     b3(150) -> 151*
     a4(676) -> 677*
     a4(671) -> 672*
     a4(636) -> 637*
     a4(631) -> 632*
     a4(414) -> 415*
     a4(409) -> 410*
     a4(606) -> 607*
     a4(601) -> 602*
     a4(561) -> 562*
     a4(556) -> 557*
     a4(511) -> 512*
     a4(506) -> 507*
     a4(496) -> 497*
     a4(491) -> 492*
     a4(678) -> 679*
     a4(673) -> 674*
     a4(638) -> 639*
     a4(633) -> 634*
     a4(416) -> 417*
     a4(411) -> 412*
     a4(608) -> 609*
     a4(603) -> 604*
     a4(341) -> 342*
     a4(336) -> 337*
     a4(286) -> 287*
     a4(281) -> 282*
     a4(560) -> 561*
     a4(555) -> 556*
     a4(510) -> 511*
     a4(505) -> 506*
     a4(495) -> 496*
     a4(490) -> 491*
     a4(288) -> 289*
     a4(283) -> 284*
     a4(677) -> 678*
     a4(672) -> 673*
     a4(637) -> 638*
     a4(632) -> 633*
     a4(415) -> 416*
     a4(410) -> 411*
     a4(607) -> 608*
     a4(602) -> 603*
     a4(562) -> 563*
     a4(557) -> 558*
     a4(340) -> 341*
     a4(335) -> 336*
     a4(512) -> 513*
     a4(507) -> 508*
     a4(342) -> 343*
     a4(337) -> 338*
     a4(494) -> 495*
     a4(489) -> 490*
     a4(287) -> 288*
     a4(282) -> 283*
     b4(464) -> 465*
     b4(339) -> 340*
     b4(334) -> 335*
     b4(284) -> 285*
     b4(578) -> 579*
     b4(558) -> 559*
     b4(710) -> 711*
     b4(508) -> 509*
     b4(493) -> 494*
     b4(488) -> 489*
     b4(675) -> 676*
     b4(670) -> 671*
     b4(640) -> 641*
     b4(635) -> 636*
     b4(630) -> 631*
     b4(413) -> 414*
     b4(408) -> 409*
     b4(605) -> 606*
     b4(600) -> 601*
     b4(540) -> 541*
     b4(338) -> 339*
     b4(502) -> 503*
     b4(694) -> 695*
     b4(492) -> 493*
     b4(285) -> 286*
     b4(280) -> 281*
     b4(674) -> 675*
     b4(634) -> 635*
     b4(412) -> 413*
     b4(604) -> 605*
     b4(594) -> 595*
     b4(559) -> 560*
     b4(554) -> 555*
     b4(509) -> 510*
     b4(504) -> 505*
     b4(696) -> 697*
     b0(3) -> 3*
     a5(681) -> 682*
     a5(591) -> 592*
     a5(586) -> 587*
     a5(688) -> 689*
     a5(683) -> 684*
     a5(590) -> 591*
     a5(585) -> 586*
     a5(687) -> 688*
     a5(682) -> 683*
     a5(592) -> 593*
     a5(587) -> 588*
     a5(686) -> 687*
     a0(3) -> 3*
     b5(588) -> 589*
     b5(685) -> 686*
     b5(680) -> 681*
     b5(684) -> 685*
     b5(589) -> 590*
     b5(584) -> 585*
     a1(20) -> 21*
     a1(15) -> 16*
     a1(52) -> 53*
     a1(47) -> 48*
     a1(22) -> 23*
     a1(17) -> 18*
     a1(54) -> 55*
     a1(49) -> 50*
     a1(21) -> 22*
     a1(16) -> 17*
     a1(53) -> 54*
     a1(48) -> 49*
     b1(50) -> 51*
     b1(92) -> 93*
     b1(144) -> 145*
     b1(19) -> 20*
     b1(14) -> 15*
     b1(206) -> 207*
     b1(51) -> 52*
     b1(46) -> 47*
     b1(88) -> 89*
     b1(58) -> 59*
     b1(18) -> 19*
     b1(90) -> 91*
     a2(75) -> 76*
     a2(30) -> 31*
     a2(25) -> 26*
     a2(192) -> 193*
     a2(187) -> 188*
     a2(127) -> 128*
     a2(122) -> 123*
     a2(32) -> 33*
     a2(27) -> 28*
     a2(104) -> 105*
     a2(99) -> 100*
     a2(79) -> 80*
     a2(74) -> 75*
     a2(191) -> 192*
     a2(186) -> 187*
     a2(126) -> 127*
     a2(121) -> 122*
     a2(106) -> 107*
     a2(101) -> 102*
     a2(31) -> 32*
     a2(26) -> 27*
     a2(128) -> 129*
     a2(123) -> 124*
     a2(78) -> 79*
     a2(73) -> 74*
     a2(190) -> 191*
     a2(185) -> 186*
     a2(105) -> 106*
     a2(100) -> 101*
     a2(80) -> 81*
     b2(182) -> 183*
     b2(142) -> 143*
     b2(102) -> 103*
     b2(77) -> 78*
     b2(274) -> 275*
     b2(72) -> 73*
     b2(189) -> 190*
     b2(184) -> 185*
     b2(124) -> 125*
     b2(29) -> 30*
     b2(24) -> 25*
     b2(398) -> 399*
     b2(146) -> 147*
     b2(298) -> 299*
     b2(86) -> 87*
     b2(76) -> 77*
     b2(188) -> 189*
     b2(103) -> 104*
     b2(98) -> 99*
     b2(260) -> 261*
     b2(28) -> 29*
     b2(392) -> 393*
     b2(130) -> 131*
     b2(125) -> 126*
     b2(120) -> 121*
     b2(312) -> 313*
     a3(257) -> 258*
     a3(252) -> 253*
     a3(237) -> 238*
     a3(232) -> 233*
     a3(227) -> 228*
     a3(222) -> 223*
     a3(616) -> 617*
     a3(611) -> 612*
     a3(389) -> 390*
     a3(384) -> 385*
     a3(172) -> 173*
     a3(571) -> 572*
     a3(167) -> 168*
     a3(566) -> 567*
     a3(157) -> 158*
     a3(354) -> 355*
     a3(152) -> 153*
     a3(349) -> 350*
     a3(526) -> 527*
     a3(521) -> 522*
     a3(436) -> 437*
     a3(431) -> 432*
     a3(618) -> 619*
     a3(613) -> 614*
     a3(174) -> 175*
     a3(169) -> 170*
     a3(321) -> 322*
     a3(316) -> 317*
     a3(256) -> 257*
     a3(251) -> 252*
     a3(438) -> 439*
     a3(236) -> 237*
     a3(433) -> 434*
     a3(231) -> 232*
     a3(226) -> 227*
     a3(221) -> 222*
     a3(388) -> 389*
     a3(383) -> 384*
     a3(570) -> 571*
     a3(565) -> 566*
     a3(156) -> 157*
     a3(353) -> 354*
     a3(151) -> 152*
     a3(348) -> 349*
     a3(525) -> 526*
     a3(520) -> 521*
     a3(258) -> 259*
     a3(253) -> 254*
     a3(238) -> 239*
     a3(233) -> 234*
     a3(228) -> 229*
     a3(223) -> 224*
     a3(617) -> 618*
     a3(612) -> 613*
     a3(390) -> 391*
     a3(385) -> 386*
     a3(173) -> 174*
     a3(572) -> 573*
     a3(168) -> 169*
     a3(567) -> 568*
     a3(158) -> 159*
     a3(153) -> 154*
     a3(320) -> 321*
     a3(315) -> 316*
     a3(437) -> 438*
     a3(432) -> 433*
     a3(352) -> 353*
     a3(347) -> 348*
     a3(524) -> 525*
     a3(322) -> 323*
     a3(519) -> 520*
     a3(317) -> 318*
     3 -> 14*
     20 -> 98*
     21 -> 58,24
     22 -> 46*
     23 -> 15,19,3
     30 -> 176*
     31 -> 150,90,72
     32 -> 120*
     33 -> 15,20,19
     52 -> 146*
     53 -> 92,86
     54 -> 88*
     55 -> 15,3,14,19
     59 -> 15*
     78 -> 166*
     79 -> 160*
     80 -> 130*
     81 -> 15,20
     87 -> 25*
     89 -> 15*
     91 -> 15*
     93 -> 15*
     105 -> 144,142
     107 -> 51*
     127 -> 220,206,182
     129 -> 19,29
     131 -> 121*
     143 -> 25*
     145 -> 15*
     147 -> 25*
     157 -> 184*
     159 -> 103*
     161 -> 151*
     173 -> 274,230
     175 -> 125*
     177 -> 167*
     183 -> 25*
     190 -> 290*
     191 -> 250*
     192 -> 260*
     193 -> 52,146
     207 -> 15*
     226 -> 488,462
     228 -> 404,392
     229 -> 104,99
     236 -> 376,334
     237 -> 280*
     238 -> 314,312
     239 -> 30,176
     257 -> 298,296
     259 -> 225,29
     261 -> 121*
     275 -> 25*
     287 -> 346*
     289 -> 171*
     291 -> 167*
     297 -> 221*
     299 -> 25*
     313 -> 25*
     321 -> 344*
     323 -> 155,77
     341 -> 408,382
     343 -> 319*
     345 -> 221*
     352 -> 502,440
     354 -> 400,398
     355 -> 126*
     377 -> 251*
     388 -> 540*
     389 -> 464*
     390 -> 486*
     391 -> 78,166
     393 -> 25*
     399 -> 25*
     401 -> 251*
     405 -> 251*
     414 -> 554*
     416 -> 430*
     417 -> 156*
     437 -> 518*
     439 -> 189*
     441 -> 251*
     463 -> 251*
     465 -> 281*
     487 -> 315*
     495 -> 516,504
     497 -> 255*
     503 -> 489*
     511 -> 584,578
     513 -> 226*
     517 -> 231*
     527 -> 147,25
     541 -> 335*
     561 -> 564*
     563 -> 435*
     570 -> 670*
     571 -> 594*
     572 -> 610*
     573 -> 190,290
     579 -> 489*
     591 -> 600*
     593 -> 493*
     595 -> 281*
     606 -> 694,680
     608 -> 656,630
     609 -> 256*
     617 -> 654,640
     619 -> 255*
     639 -> 225*
     641 -> 505*
     655 -> 231*
     657 -> 251*
     677 -> 696*
     679 -> 615*
     687 -> 710*
     689 -> 635*
     695 -> 489*
     697 -> 601*
     711 -> 505*
   problem:
    strict:
     
    weak:
     b(a(a(a(b(a(a(x1))))))) -> a(a(a(b(b(a(a(a(b(x1)))))))))
   Qed