YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   b(a(b(a(a(x1))))) -> a(a(b(b(a(b(a(b(a(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 4
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     b3(142) -> 143*
     b3(112) -> 113*
     b3(102) -> 103*
     b3(114) -> 115*
     b3(104) -> 105*
     b3(84) -> 85*
     b3(79) -> 80*
     b3(171) -> 172*
     b3(166) -> 167*
     b3(81) -> 82*
     b3(168) -> 169*
     b3(143) -> 144*
     b3(138) -> 139*
     b3(83) -> 84*
     b3(170) -> 171*
     b3(140) -> 141*
     b3(115) -> 116*
     b3(110) -> 111*
     b3(105) -> 106*
     b3(100) -> 101*
     a4(212) -> 213*
     a4(202) -> 203*
     a4(204) -> 205*
     a4(194) -> 195*
     a4(164) -> 165*
     a4(211) -> 212*
     a4(206) -> 207*
     a4(201) -> 202*
     a4(196) -> 197*
     a4(156) -> 157*
     a4(208) -> 209*
     a4(198) -> 199*
     a4(163) -> 164*
     a4(158) -> 159*
     a4(160) -> 161*
     b4(207) -> 208*
     b4(197) -> 198*
     b4(162) -> 163*
     b4(157) -> 158*
     b4(209) -> 210*
     b4(199) -> 200*
     b4(159) -> 160*
     b4(161) -> 162*
     b4(210) -> 211*
     b4(205) -> 206*
     b4(200) -> 201*
     b4(195) -> 196*
     b0(3) -> 3*
     a0(3) -> 3*
     a1(22) -> 23*
     a1(14) -> 15*
     a1(21) -> 22*
     a1(16) -> 17*
     a1(18) -> 19*
     b1(50) -> 51*
     b1(20) -> 21*
     b1(15) -> 16*
     b1(17) -> 18*
     b1(19) -> 20*
     b1(46) -> 47*
     a2(65) -> 66*
     a2(32) -> 33*
     a2(64) -> 65*
     a2(59) -> 60*
     a2(54) -> 55*
     a2(24) -> 25*
     a2(61) -> 62*
     a2(31) -> 32*
     a2(26) -> 27*
     a2(28) -> 29*
     b2(60) -> 61*
     b2(30) -> 31*
     b2(25) -> 26*
     b2(62) -> 63*
     b2(27) -> 28*
     b2(29) -> 30*
     b2(76) -> 77*
     b2(63) -> 64*
     b2(58) -> 59*
     a3(172) -> 173*
     a3(167) -> 168*
     a3(117) -> 118*
     a3(107) -> 108*
     a3(82) -> 83*
     a3(169) -> 170*
     a3(144) -> 145*
     a3(139) -> 140*
     a3(109) -> 110*
     a3(141) -> 142*
     a3(116) -> 117*
     a3(111) -> 112*
     a3(106) -> 107*
     a3(101) -> 102*
     a3(86) -> 87*
     a3(173) -> 174*
     a3(113) -> 114*
     a3(103) -> 104*
     a3(78) -> 79*
     a3(145) -> 146*
     a3(85) -> 86*
     a3(80) -> 81*
     3 -> 14*
     21 -> 54*
     22 -> 46,24
     23 -> 16,50,18,3
     32 -> 58*
     33 -> 28,20,18
     47 -> 16*
     51 -> 16*
     55 -> 25*
     64 -> 109*
     65 -> 78*
     66 -> 76,26,47,16
     77 -> 26*
     86 -> 100*
     87 -> 30*
     106 -> 156*
     108 -> 138,59
     118 -> 82,28
     145 -> 166*
     146 -> 63*
     165 -> 141*
     172 -> 204*
     173 -> 194*
     174 -> 111*
     203 -> 115*
     213 -> 198*
   problem:
    strict:
     
    weak:
     b(a(b(a(a(x1))))) -> a(a(b(b(a(b(a(b(a(x1)))))))))
   Qed