YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(a(b(b(x1))))) -> b(b(b(b(b(a(a(a(a(a(x1))))))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match-rt
   automaton:
    final states: {2,1}
    transitions:
     a3(272) -> 273*
     a3(247) -> 248*
     a3(207) -> 208*
     a3(192) -> 193*
     a3(162) -> 163*
     a3(137) -> 138*
     a3(107) -> 108*
     a3(274) -> 275*
     a3(269) -> 270*
     a3(249) -> 250*
     a3(204) -> 205*
     a3(194) -> 195*
     a3(159) -> 160*
     a3(139) -> 140*
     a3(109) -> 110*
     a3(271) -> 272*
     a3(251) -> 252*
     a3(206) -> 207*
     a3(196) -> 197*
     a3(161) -> 162*
     a3(136) -> 137*
     a3(116) -> 117*
     a3(106) -> 107*
     a3(273) -> 274*
     a3(248) -> 249*
     a3(203) -> 204*
     a3(193) -> 194*
     a3(163) -> 164*
     a3(138) -> 139*
     a3(108) -> 109*
     a3(275) -> 276*
     a3(250) -> 251*
     a3(205) -> 206*
     a3(195) -> 196*
     a3(160) -> 161*
     a3(135) -> 136*
     a3(105) -> 106*
     b4(449) -> 450*
     b4(242) -> 243*
     b4(414) -> 415*
     b4(394) -> 395*
     b4(359) -> 360*
     b4(324) -> 325*
     b4(299) -> 300*
     b4(491) -> 492*
     b4(451) -> 452*
     b4(244) -> 245*
     b4(416) -> 417*
     b4(391) -> 392*
     b4(356) -> 357*
     b4(326) -> 327*
     b4(301) -> 302*
     b4(493) -> 494*
     b4(448) -> 449*
     b4(241) -> 242*
     b4(418) -> 419*
     b4(393) -> 394*
     b4(358) -> 359*
     b4(323) -> 324*
     b4(298) -> 299*
     b4(495) -> 496*
     b4(450) -> 451*
     b4(243) -> 244*
     b4(415) -> 416*
     b4(390) -> 391*
     b4(355) -> 356*
     b4(325) -> 326*
     b4(300) -> 301*
     b4(492) -> 493*
     b4(447) -> 448*
     b4(245) -> 246*
     b4(417) -> 418*
     b4(392) -> 393*
     b4(357) -> 358*
     b4(322) -> 323*
     b4(302) -> 303*
     b4(494) -> 495*
     a4(444) -> 445*
     a4(237) -> 238*
     a4(409) -> 410*
     a4(389) -> 390*
     a4(354) -> 355*
     a4(319) -> 320*
     a4(304) -> 305*
     a4(294) -> 295*
     a4(486) -> 487*
     a4(446) -> 447*
     a4(239) -> 240*
     a4(411) -> 412*
     a4(386) -> 387*
     a4(361) -> 362*
     a4(351) -> 352*
     a4(321) -> 322*
     a4(296) -> 297*
     a4(488) -> 489*
     a4(443) -> 444*
     a4(236) -> 237*
     a4(413) -> 414*
     a4(388) -> 389*
     a4(353) -> 354*
     a4(318) -> 319*
     a4(293) -> 294*
     a4(490) -> 491*
     a4(445) -> 446*
     a4(238) -> 239*
     a4(410) -> 411*
     a4(385) -> 386*
     a4(350) -> 351*
     a4(320) -> 321*
     a4(295) -> 296*
     a4(487) -> 488*
     a4(442) -> 443*
     a4(240) -> 241*
     a4(412) -> 413*
     a4(387) -> 388*
     a4(352) -> 353*
     a4(317) -> 318*
     a4(297) -> 298*
     a4(489) -> 490*
     a0(2) -> 1*
     a0(1) -> 1*
     b5(459) -> 460*
     b5(506) -> 507*
     b5(461) -> 462*
     b5(503) -> 504*
     b5(458) -> 459*
     b5(505) -> 506*
     b5(460) -> 461*
     b5(502) -> 503*
     b5(462) -> 463*
     b5(504) -> 505*
     b0(2) -> 2*
     b0(1) -> 2*
     a5(454) -> 455*
     a5(501) -> 502*
     a5(456) -> 457*
     a5(498) -> 499*
     a5(453) -> 454*
     a5(500) -> 501*
     a5(455) -> 456*
     a5(497) -> 498*
     a5(457) -> 458*
     a5(499) -> 500*
     b1(10) -> 11*
     b1(12) -> 13*
     b1(9) -> 10*
     b1(11) -> 12*
     b1(13) -> 14*
     a1(50) -> 51*
     a1(5) -> 6*
     a1(52) -> 53*
     a1(37) -> 38*
     a1(7) -> 8*
     a1(4) -> 5*
     a1(6) -> 7*
     a1(8) -> 9*
     b2(65) -> 66*
     b2(97) -> 98*
     b2(62) -> 63*
     b2(99) -> 100*
     b2(64) -> 65*
     b2(101) -> 102*
     b2(61) -> 62*
     b2(98) -> 99*
     b2(63) -> 64*
     b2(100) -> 101*
     a2(60) -> 61*
     a2(92) -> 93*
     a2(77) -> 78*
     a2(67) -> 68*
     a2(57) -> 58*
     a2(94) -> 95*
     a2(79) -> 80*
     a2(69) -> 70*
     a2(59) -> 60*
     a2(96) -> 97*
     a2(56) -> 57*
     a2(93) -> 94*
     a2(58) -> 59*
     a2(95) -> 96*
     b3(277) -> 278*
     b3(252) -> 253*
     b3(212) -> 213*
     b3(197) -> 198*
     b3(167) -> 168*
     b3(142) -> 143*
     b3(112) -> 113*
     b3(279) -> 280*
     b3(254) -> 255*
     b3(209) -> 210*
     b3(199) -> 200*
     b3(164) -> 165*
     b3(144) -> 145*
     b3(114) -> 115*
     b3(276) -> 277*
     b3(256) -> 257*
     b3(211) -> 212*
     b3(201) -> 202*
     b3(166) -> 167*
     b3(141) -> 142*
     b3(111) -> 112*
     b3(278) -> 279*
     b3(253) -> 254*
     b3(208) -> 209*
     b3(198) -> 199*
     b3(168) -> 169*
     b3(143) -> 144*
     b3(113) -> 114*
     b3(280) -> 281*
     b3(255) -> 256*
     b3(210) -> 211*
     b3(200) -> 201*
     b3(165) -> 166*
     b3(140) -> 141*
     b3(110) -> 111*
     1 -> 37*
     2 -> 4*
     9 -> 77*
     10 -> 69*
     11 -> 67*
     12 -> 56,52
     13 -> 50*
     14 -> 6,7,38,1
     38 -> 5*
     51 -> 5*
     53 -> 5*
     61 -> 192*
     62 -> 159*
     63 -> 116*
     64 -> 105,92
     65 -> 79*
     66 -> 78,57,59,8,9,7
     68 -> 57*
     70 -> 57*
     78 -> 57*
     80 -> 57*
     98 -> 203*
     100 -> 135*
     102 -> 78,58,57
     111 -> 361*
     113 -> 293,269
     115 -> 193,60,59
     117 -> 106*
     140 -> 409*
     141 -> 350*
     142 -> 317*
     143 -> 247,236
     144 -> 271*
     145 -> 60,61
     169 -> 108,95
     202 -> 108*
     209 -> 486*
     211 -> 442*
     213 -> 138*
     246 -> 195*
     253 -> 385*
     255 -> 304*
     257 -> 193,194
     270 -> 248*
     281 -> 162*
     303 -> 197,196
     305 -> 294*
     327 -> 274*
     360 -> 296,239,250
     362 -> 351*
     395 -> 296*
     419 -> 320*
     448 -> 497*
     450 -> 453*
     452 -> 410*
     463 -> 413*
     496 -> 445*
     507 -> 456*
   problem:
    strict:
     
    weak:
     a(a(a(b(b(x1))))) -> b(b(b(b(b(a(a(a(a(a(x1))))))))))
   Qed