YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(a(b(a(a(a(x1)))))) -> a(a(a(b(a(b(a(b(a(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match-rt
   automaton:
    final states: {2,1}
    transitions:
     b3(187) -> 188*
     b3(162) -> 163*
     b3(92) -> 93*
     b3(164) -> 165*
     b3(149) -> 150*
     b3(94) -> 95*
     b3(166) -> 167*
     b3(151) -> 152*
     b3(183) -> 184*
     b3(153) -> 154*
     b3(210) -> 211*
     b3(185) -> 186*
     b3(90) -> 91*
     a4(252) -> 253*
     a4(242) -> 243*
     a4(212) -> 213*
     a4(202) -> 203*
     a4(244) -> 245*
     a4(234) -> 235*
     a4(219) -> 220*
     a4(214) -> 215*
     a4(204) -> 205*
     a4(251) -> 252*
     a4(246) -> 247*
     a4(241) -> 242*
     a4(236) -> 237*
     a4(216) -> 217*
     a4(196) -> 197*
     a4(248) -> 249*
     a4(238) -> 239*
     a4(218) -> 219*
     a4(203) -> 204*
     a4(198) -> 199*
     a4(250) -> 251*
     a4(240) -> 241*
     a4(220) -> 221*
     a4(200) -> 201*
     b4(247) -> 248*
     b4(237) -> 238*
     b4(217) -> 218*
     b4(197) -> 198*
     b4(249) -> 250*
     b4(239) -> 240*
     b4(199) -> 200*
     b4(201) -> 202*
     b4(213) -> 214*
     b4(245) -> 246*
     b4(235) -> 236*
     b4(215) -> 216*
     b0(2) -> 1*
     b0(1) -> 1*
     a5(262) -> 263*
     a5(254) -> 255*
     a5(261) -> 262*
     a5(256) -> 257*
     a5(258) -> 259*
     a5(260) -> 261*
     a0(2) -> 2*
     a0(1) -> 2*
     b5(257) -> 258*
     b5(259) -> 260*
     b5(255) -> 256*
     a1(10) -> 11*
     a1(12) -> 13*
     a1(34) -> 35*
     a1(4) -> 5*
     a1(11) -> 12*
     a1(6) -> 7*
     a1(8) -> 9*
     b1(55) -> 56*
     b1(5) -> 6*
     b1(7) -> 8*
     b1(9) -> 10*
     b1(61) -> 62*
     b1(63) -> 64*
     a2(70) -> 71*
     a2(40) -> 41*
     a2(87) -> 88*
     a2(72) -> 73*
     a2(42) -> 43*
     a2(109) -> 110*
     a2(104) -> 105*
     a2(44) -> 45*
     a2(106) -> 107*
     a2(71) -> 72*
     a2(66) -> 67*
     a2(36) -> 37*
     a2(108) -> 109*
     a2(68) -> 69*
     a2(43) -> 44*
     a2(38) -> 39*
     a2(110) -> 111*
     b2(65) -> 66*
     b2(112) -> 113*
     b2(107) -> 108*
     b2(67) -> 68*
     b2(37) -> 38*
     b2(69) -> 70*
     b2(39) -> 40*
     b2(146) -> 147*
     b2(41) -> 42*
     b2(158) -> 159*
     b2(103) -> 104*
     b2(105) -> 106*
     a3(192) -> 193*
     a3(167) -> 168*
     a3(152) -> 153*
     a3(97) -> 98*
     a3(189) -> 190*
     a3(184) -> 185*
     a3(169) -> 170*
     a3(154) -> 155*
     a3(89) -> 90*
     a3(186) -> 187*
     a3(171) -> 172*
     a3(156) -> 157*
     a3(96) -> 97*
     a3(91) -> 92*
     a3(188) -> 189*
     a3(168) -> 169*
     a3(163) -> 164*
     a3(148) -> 149*
     a3(133) -> 134*
     a3(93) -> 94*
     a3(190) -> 191*
     a3(165) -> 166*
     a3(155) -> 156*
     a3(150) -> 151*
     a3(95) -> 96*
     1 -> 34*
     2 -> 4*
     10 -> 87*
     11 -> 63,36
     12 -> 61*
     13 -> 6,55,8,1
     35 -> 5*
     42 -> 148*
     43 -> 89*
     44 -> 65*
     45 -> 38,103,64,6,10,8
     56 -> 6*
     62 -> 6*
     64 -> 6*
     70 -> 192*
     71 -> 133*
     72 -> 112*
     73 -> 146,38,8,10,64,6
     88 -> 37*
     95 -> 234*
     96 -> 196*
     97 -> 162*
     98 -> 183,42,40
     109 -> 171*
     110 -> 158*
     111 -> 8,40
     113 -> 38*
     134 -> 90*
     147 -> 104*
     157 -> 106*
     159 -> 38*
     168 -> 212*
     170 -> 150*
     172 -> 162*
     189 -> 244*
     190 -> 210*
     191 -> 93,68
     193 -> 149*
     205 -> 152*
     211 -> 163*
     221 -> 154*
     243 -> 186*
     251 -> 254*
     253 -> 236*
     263 -> 240*
   problem:
    strict:
     
    weak:
     b(a(b(a(a(a(x1)))))) -> a(a(a(b(a(b(a(b(a(x1)))))))))
   Qed