YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(a(b(a(a(x1))))) -> a(a(a(b(a(b(a(b(x1))))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match-rt
   automaton:
    final states: {2,1}
    transitions:
     b3(172) -> 173*
     b3(152) -> 153*
     b3(147) -> 148*
     b3(127) -> 128*
     b3(87) -> 88*
     b3(129) -> 130*
     b3(96) -> 97*
     b3(143) -> 144*
     b3(98) -> 99*
     b3(83) -> 84*
     b3(145) -> 146*
     b3(125) -> 126*
     b3(100) -> 101*
     b3(85) -> 86*
     a4(247) -> 248*
     a4(242) -> 243*
     a4(217) -> 218*
     a4(212) -> 213*
     a4(192) -> 193*
     a4(177) -> 178*
     a4(244) -> 245*
     a4(219) -> 220*
     a4(179) -> 180*
     a4(246) -> 247*
     a4(221) -> 222*
     a4(211) -> 212*
     a4(206) -> 207*
     a4(191) -> 192*
     a4(186) -> 187*
     a4(181) -> 182*
     a4(248) -> 249*
     a4(208) -> 209*
     a4(188) -> 189*
     a4(220) -> 221*
     a4(215) -> 216*
     a4(210) -> 211*
     a4(190) -> 191*
     a4(180) -> 181*
     a4(175) -> 176*
     b4(207) -> 208*
     b4(187) -> 188*
     b4(214) -> 215*
     b4(209) -> 210*
     b4(189) -> 190*
     b4(174) -> 175*
     b4(241) -> 242*
     b4(216) -> 217*
     b4(176) -> 177*
     b4(243) -> 244*
     b4(218) -> 219*
     b4(178) -> 179*
     b4(245) -> 246*
     b4(205) -> 206*
     b4(185) -> 186*
     b0(2) -> 1*
     b0(1) -> 1*
     a5(257) -> 258*
     a5(259) -> 260*
     a5(229) -> 230*
     a5(224) -> 225*
     a5(226) -> 227*
     a5(258) -> 259*
     a5(253) -> 254*
     a5(228) -> 229*
     a5(255) -> 256*
     a5(230) -> 231*
     a0(2) -> 2*
     a0(1) -> 2*
     b5(252) -> 253*
     b5(227) -> 228*
     b5(254) -> 255*
     b5(256) -> 257*
     b5(223) -> 224*
     b5(225) -> 226*
     a1(10) -> 11*
     a1(5) -> 6*
     a1(7) -> 8*
     a1(9) -> 10*
     a1(11) -> 12*
     b1(35) -> 36*
     b1(4) -> 5*
     b1(46) -> 47*
     b1(31) -> 32*
     b1(6) -> 7*
     b1(8) -> 9*
     a2(60) -> 61*
     a2(40) -> 41*
     a2(62) -> 63*
     a2(42) -> 43*
     a2(64) -> 65*
     a2(44) -> 45*
     a2(63) -> 64*
     a2(58) -> 59*
     a2(43) -> 44*
     a2(38) -> 39*
     b2(70) -> 71*
     b2(57) -> 58*
     b2(37) -> 38*
     b2(59) -> 60*
     b2(39) -> 40*
     b2(66) -> 67*
     b2(61) -> 62*
     b2(41) -> 42*
     b2(123) -> 124*
     a3(132) -> 133*
     a3(102) -> 103*
     a3(97) -> 98*
     a3(149) -> 150*
     a3(144) -> 145*
     a3(99) -> 100*
     a3(89) -> 90*
     a3(84) -> 85*
     a3(146) -> 147*
     a3(131) -> 132*
     a3(126) -> 127*
     a3(101) -> 102*
     a3(86) -> 87*
     a3(148) -> 149*
     a3(128) -> 129*
     a3(103) -> 104*
     a3(88) -> 89*
     a3(150) -> 151*
     a3(130) -> 131*
     a3(90) -> 91*
     1 -> 31*
     2 -> 4*
     9 -> 70*
     10 -> 46,37
     11 -> 66,35
     12 -> 5,7,1
     32 -> 5*
     36 -> 5*
     42 -> 83*
     44 -> 152,57
     45 -> 60,7
     47 -> 5*
     62 -> 172*
     63 -> 125*
     64 -> 123,96
     65 -> 40,7,38,9,47
     67 -> 58*
     71 -> 38*
     88 -> 205*
     90 -> 214,143
     91 -> 146,99,60
     102 -> 174*
     104 -> 42*
     124 -> 58*
     133 -> 40*
     148 -> 241*
     150 -> 185*
     151 -> 126*
     153 -> 144*
     173 -> 84*
     182 -> 86*
     193 -> 130*
     213 -> 217,146
     219 -> 252*
     221 -> 223*
     222 -> 175*
     231 -> 179*
     249 -> 188*
     260 -> 226*
   problem:
    strict:
     
    weak:
     b(a(b(a(a(x1))))) -> a(a(a(b(a(b(a(b(x1))))))))
   Qed