YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
  weak:
   
  Bounds Processor:
   bound: 6
   enrichment: match-rt
   automaton:
    final states: {2,1}
    transitions:
     a3(227) -> 228*
     a3(197) -> 198*
     a3(162) -> 163*
     a3(137) -> 138*
     a3(102) -> 103*
     a3(229) -> 230*
     a3(199) -> 200*
     a3(164) -> 165*
     a3(139) -> 140*
     a3(119) -> 120*
     a3(104) -> 105*
     a3(226) -> 227*
     a3(196) -> 197*
     a3(161) -> 162*
     a3(156) -> 157*
     a3(136) -> 137*
     a3(101) -> 102*
     a3(228) -> 229*
     a3(198) -> 199*
     a3(163) -> 164*
     a3(138) -> 139*
     a3(103) -> 104*
     a3(225) -> 226*
     a3(200) -> 201*
     a3(160) -> 161*
     a3(145) -> 146*
     a3(140) -> 141*
     a3(105) -> 106*
     b4(267) -> 268*
     b4(222) -> 223*
     b4(192) -> 193*
     b4(349) -> 350*
     b4(304) -> 305*
     b4(249) -> 250*
     b4(194) -> 195*
     b4(311) -> 312*
     b4(266) -> 267*
     b4(221) -> 222*
     b4(348) -> 349*
     b4(313) -> 314*
     b4(303) -> 304*
     b4(268) -> 269*
     b4(248) -> 249*
     b4(223) -> 224*
     b4(193) -> 194*
     b4(250) -> 251*
     b4(347) -> 348*
     b4(312) -> 313*
     b4(302) -> 303*
     a4(262) -> 263*
     a4(247) -> 248*
     a4(217) -> 218*
     a4(187) -> 188*
     a4(344) -> 345*
     a4(309) -> 310*
     a4(299) -> 300*
     a4(264) -> 265*
     a4(244) -> 245*
     a4(219) -> 220*
     a4(189) -> 190*
     a4(346) -> 347*
     a4(306) -> 307*
     a4(301) -> 302*
     a4(261) -> 262*
     a4(246) -> 247*
     a4(216) -> 217*
     a4(191) -> 192*
     a4(378) -> 379*
     a4(343) -> 344*
     a4(308) -> 309*
     a4(298) -> 299*
     a4(263) -> 264*
     a4(243) -> 244*
     a4(218) -> 219*
     a4(188) -> 189*
     a4(345) -> 346*
     a4(310) -> 311*
     a4(300) -> 301*
     a4(265) -> 266*
     a4(245) -> 246*
     a4(220) -> 221*
     a4(190) -> 191*
     a4(342) -> 343*
     a4(307) -> 308*
     a4(297) -> 298*
     a0(2) -> 1*
     a0(1) -> 1*
     b5(277) -> 278*
     b5(414) -> 415*
     b5(404) -> 405*
     b5(374) -> 375*
     b5(339) -> 340*
     b5(466) -> 467*
     b5(376) -> 377*
     b5(276) -> 277*
     b5(468) -> 469*
     b5(413) -> 414*
     b5(403) -> 404*
     b5(338) -> 339*
     b5(405) -> 406*
     b5(375) -> 376*
     b5(340) -> 341*
     b5(275) -> 276*
     b5(467) -> 468*
     b5(412) -> 413*
     b0(2) -> 2*
     b0(1) -> 2*
     a5(272) -> 273*
     a5(464) -> 465*
     a5(409) -> 410*
     a5(399) -> 400*
     a5(369) -> 370*
     a5(334) -> 335*
     a5(274) -> 275*
     a5(461) -> 462*
     a5(411) -> 412*
     a5(401) -> 402*
     a5(371) -> 372*
     a5(336) -> 337*
     a5(271) -> 272*
     a5(463) -> 464*
     a5(408) -> 409*
     a5(398) -> 399*
     a5(373) -> 374*
     a5(333) -> 334*
     a5(273) -> 274*
     a5(465) -> 466*
     a5(410) -> 411*
     a5(400) -> 401*
     a5(370) -> 371*
     a5(335) -> 336*
     a5(270) -> 271*
     a5(462) -> 463*
     a5(407) -> 408*
     a5(402) -> 403*
     a5(372) -> 373*
     a5(337) -> 338*
     b1(10) -> 11*
     b1(9) -> 10*
     b1(11) -> 12*
     b6(439) -> 440*
     b6(441) -> 442*
     b6(431) -> 432*
     b6(440) -> 441*
     b6(430) -> 431*
     b6(432) -> 433*
     a1(35) -> 36*
     a1(5) -> 6*
     a1(37) -> 38*
     a1(7) -> 8*
     a1(4) -> 5*
     a1(31) -> 32*
     a1(6) -> 7*
     a1(8) -> 9*
     a6(434) -> 435*
     a6(429) -> 430*
     a6(436) -> 437*
     a6(426) -> 427*
     a6(438) -> 439*
     a6(428) -> 429*
     a6(435) -> 436*
     a6(425) -> 426*
     a6(437) -> 438*
     a6(427) -> 428*
     b2(45) -> 46*
     b2(87) -> 88*
     b2(62) -> 63*
     b2(64) -> 65*
     b2(44) -> 45*
     b2(86) -> 87*
     b2(46) -> 47*
     b2(88) -> 89*
     b2(63) -> 64*
     a2(60) -> 61*
     a2(40) -> 41*
     a2(82) -> 83*
     a2(57) -> 58*
     a2(42) -> 43*
     a2(84) -> 85*
     a2(59) -> 60*
     a2(39) -> 40*
     a2(121) -> 122*
     a2(81) -> 82*
     a2(61) -> 62*
     a2(41) -> 42*
     a2(83) -> 84*
     a2(68) -> 69*
     a2(58) -> 59*
     a2(43) -> 44*
     a2(85) -> 86*
     b3(232) -> 233*
     b3(202) -> 203*
     b3(167) -> 168*
     b3(142) -> 143*
     b3(107) -> 108*
     b3(231) -> 232*
     b3(201) -> 202*
     b3(166) -> 167*
     b3(141) -> 142*
     b3(106) -> 107*
     b3(203) -> 204*
     b3(143) -> 144*
     b3(108) -> 109*
     b3(230) -> 231*
     b3(165) -> 166*
     1 -> 31*
     2 -> 4*
     9 -> 68*
     10 -> 39,37
     11 -> 35*
     12 -> 6,32,1
     32 -> 5*
     36 -> 5*
     38 -> 5*
     45 -> 145,57
     47 -> 41,7,8,6
     62 -> 156*
     63 -> 101,81
     64 -> 121*
     65 -> 69,9,40,8
     69 -> 40*
     87 -> 119*
     89 -> 69,40
     107 -> 136*
     109 -> 41,42
     120 -> 102*
     122 -> 40*
     141 -> 216*
     143 -> 160*
     144 -> 44,43
     146 -> 137*
     157 -> 102*
     166 -> 196,187
     168 -> 138,59
     193 -> 261*
     195 -> 140*
     202 -> 225*
     204 -> 61*
     222 -> 243*
     224 -> 162*
     231 -> 297*
     233 -> 157,102
     251 -> 164*
     267 -> 270*
     269 -> 217*
     276 -> 333*
     278 -> 219*
     303 -> 306*
     305 -> 104*
     311 -> 398*
     313 -> 342*
     314 -> 106*
     338 -> 425*
     340 -> 369*
     341 -> 221*
     348 -> 378*
     350 -> 138*
     375 -> 407*
     377 -> 245*
     379 -> 188*
     404 -> 461*
     406 -> 344*
     415 -> 247*
     431 -> 434*
     433 -> 371*
     442 -> 373*
     469 -> 346*
   problem:
    strict:
     
    weak:
     a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
   Qed