YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1)))))))))
  weak:
   
  Bounds Processor:
   bound: 3
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     a3(162) -> 163*
     a3(157) -> 158*
     a3(142) -> 143*
     a3(137) -> 138*
     a3(159) -> 160*
     a3(139) -> 140*
     a3(156) -> 157*
     a3(136) -> 137*
     a3(160) -> 161*
     a3(155) -> 156*
     a3(140) -> 141*
     a3(135) -> 136*
     a1(20) -> 21*
     a1(15) -> 16*
     a1(22) -> 23*
     a1(17) -> 18*
     a1(19) -> 20*
     a1(16) -> 17*
     b3(154) -> 155*
     b3(134) -> 135*
     b3(161) -> 162*
     b3(141) -> 142*
     b3(158) -> 159*
     b3(138) -> 139*
     b1(30) -> 31*
     b1(32) -> 33*
     b1(24) -> 25*
     b1(14) -> 15*
     b1(21) -> 22*
     b1(118) -> 119*
     b1(18) -> 19*
     b1(120) -> 121*
     a2(60) -> 61*
     a2(40) -> 41*
     a2(92) -> 93*
     a2(87) -> 88*
     a2(94) -> 95*
     a2(89) -> 90*
     a2(64) -> 65*
     a2(59) -> 60*
     a2(44) -> 45*
     a2(39) -> 40*
     a2(91) -> 92*
     a2(66) -> 67*
     a2(61) -> 62*
     a2(46) -> 47*
     a2(41) -> 42*
     a2(88) -> 89*
     a2(63) -> 64*
     a2(43) -> 44*
     a0(3) -> 3*
     b2(65) -> 66*
     b2(45) -> 46*
     b2(112) -> 113*
     b2(82) -> 83*
     b2(62) -> 63*
     b2(42) -> 43*
     b2(174) -> 175*
     b2(126) -> 127*
     b2(96) -> 97*
     b2(86) -> 87*
     b2(128) -> 129*
     b2(93) -> 94*
     b2(68) -> 69*
     b2(58) -> 59*
     b2(38) -> 39*
     b2(110) -> 111*
     b2(90) -> 91*
     b0(3) -> 3*
     3 -> 14*
     15 -> 174*
     16 -> 82*
     17 -> 38,24
     19 -> 58*
     20 -> 86,30
     22 -> 68,32
     23 -> 41,17,3
     25 -> 15*
     31 -> 15*
     33 -> 15*
     46 -> 128,120
     47 -> 42,18
     61 -> 154,126
     64 -> 134,96
     66 -> 112*
     67 -> 157,41,17,24
     69 -> 59*
     83 -> 59*
     94 -> 118,110
     95 -> 45,21
     97 -> 87*
     111 -> 87*
     113 -> 59*
     119 -> 15*
     121 -> 15*
     127 -> 39*
     129 -> 39*
     143 -> 161,45
     163 -> 158,42
     175 -> 59*
   problem:
    strict:
     
    weak:
     a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1)))))))))
   Qed