YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    a3(192) -> 193*
    a3(182) -> 183*
    a3(172) -> 173*
    a3(132) -> 133*
    a3(179) -> 180*
    a3(159) -> 160*
    a3(191) -> 192*
    a3(181) -> 182*
    a3(171) -> 172*
    a3(131) -> 132*
    a3(193) -> 194*
    a3(173) -> 174*
    a3(133) -> 134*
    a3(190) -> 191*
    a3(180) -> 181*
    a3(170) -> 171*
    a3(130) -> 131*
    b4(232) -> 233*
    b4(207) -> 208*
    b4(234) -> 235*
    b4(206) -> 207*
    b4(233) -> 234*
    b4(208) -> 209*
    b4(235) -> 236*
    b4(205) -> 206*
    a4(202) -> 203*
    a4(229) -> 230*
    a4(204) -> 205*
    a4(231) -> 232*
    a4(201) -> 202*
    a4(228) -> 229*
    a4(203) -> 204*
    a4(230) -> 231*
    a0(3) -> 3*
    b5(242) -> 243*
    b5(244) -> 245*
    b5(241) -> 242*
    b5(243) -> 244*
    b0(3) -> 3*
    a5(237) -> 238*
    a5(239) -> 240*
    a5(238) -> 239*
    a5(240) -> 241*
    b1(20) -> 21*
    b1(27) -> 28*
    b1(17) -> 18*
    b1(29) -> 30*
    b1(19) -> 20*
    b1(26) -> 27*
    b1(28) -> 29*
    b1(18) -> 19*
    a1(35) -> 36*
    a1(25) -> 26*
    a1(15) -> 16*
    a1(87) -> 88*
    a1(22) -> 23*
    a1(24) -> 25*
    a1(14) -> 15*
    a1(91) -> 92*
    a1(16) -> 17*
    a1(33) -> 34*
    a1(23) -> 24*
    a1(13) -> 14*
    a1(85) -> 86*
    b2(70) -> 71*
    b2(157) -> 158*
    b2(97) -> 98*
    b2(67) -> 68*
    b2(57) -> 58*
    b2(154) -> 155*
    b2(99) -> 100*
    b2(69) -> 70*
    b2(59) -> 60*
    b2(156) -> 157*
    b2(56) -> 57*
    b2(98) -> 99*
    b2(68) -> 69*
    b2(58) -> 59*
    b2(155) -> 156*
    b2(100) -> 101*
    a2(65) -> 66*
    a2(55) -> 56*
    a2(152) -> 153*
    a2(52) -> 53*
    a2(119) -> 120*
    a2(94) -> 95*
    a2(64) -> 65*
    a2(54) -> 55*
    a2(151) -> 152*
    a2(96) -> 97*
    a2(81) -> 82*
    a2(66) -> 67*
    a2(153) -> 154*
    a2(113) -> 114*
    a2(93) -> 94*
    a2(63) -> 64*
    a2(53) -> 54*
    a2(150) -> 151*
    a2(115) -> 116*
    a2(95) -> 96*
    b3(197) -> 198*
    b3(177) -> 178*
    b3(137) -> 138*
    b3(194) -> 195*
    b3(184) -> 185*
    b3(174) -> 175*
    b3(134) -> 135*
    b3(196) -> 197*
    b3(186) -> 187*
    b3(176) -> 177*
    b3(136) -> 137*
    b3(183) -> 184*
    b3(195) -> 196*
    b3(185) -> 186*
    b3(175) -> 176*
    b3(135) -> 136*
    3 -> 13*
    17 -> 63*
    18 -> 52,22
    19 -> 33*
    20 -> 35*
    21 -> 16,14,15,3
    26 -> 119*
    27 -> 85,81
    28 -> 87*
    29 -> 91*
    30 -> 16,14,3,15
    34 -> 23*
    36 -> 23*
    56 -> 159*
    57 -> 130,93
    58 -> 113*
    59 -> 115*
    60 -> 64,65,17,16
    68 -> 190,150
    71 -> 55,25
    82 -> 53*
    86 -> 14*
    88 -> 14*
    92 -> 14*
    101 -> 65*
    114 -> 64*
    116 -> 64*
    120 -> 53*
    136 -> 179*
    138 -> 67,66
    155 -> 170*
    158 -> 54*
    160 -> 131*
    175 -> 201*
    178 -> 160,131
    187 -> 193,153
    198 -> 132*
    205 -> 237*
    208 -> 228*
    209 -> 134*
    236 -> 182*
    245 -> 231*
  problem:
   
  Qed