YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(b(b(x1)))) -> b(b(b(a(a(a(x1))))))
  weak:
   
  Bounds Processor:
   bound: 5
   enrichment: match-rt
   automaton:
    final states: {3}
    transitions:
     a3(162) -> 163*
     a3(152) -> 153*
     a3(117) -> 118*
     a3(87) -> 88*
     a3(199) -> 200*
     a3(169) -> 170*
     a3(149) -> 150*
     a3(119) -> 120*
     a3(89) -> 90*
     a3(201) -> 202*
     a3(171) -> 172*
     a3(161) -> 162*
     a3(151) -> 152*
     a3(153) -> 154*
     a3(118) -> 119*
     a3(88) -> 89*
     a3(200) -> 201*
     a3(170) -> 171*
     a3(160) -> 161*
     b4(232) -> 233*
     b4(197) -> 198*
     b4(239) -> 240*
     b4(234) -> 235*
     b4(224) -> 225*
     b4(179) -> 180*
     b4(241) -> 242*
     b4(196) -> 197*
     b4(181) -> 182*
     b4(233) -> 234*
     b4(223) -> 224*
     b4(240) -> 241*
     b4(225) -> 226*
     b4(195) -> 196*
     b4(180) -> 181*
     a4(237) -> 238*
     a4(222) -> 223*
     a4(192) -> 193*
     a4(177) -> 178*
     a4(229) -> 230*
     a4(194) -> 195*
     a4(236) -> 237*
     a4(231) -> 232*
     a4(221) -> 222*
     a4(176) -> 177*
     a4(238) -> 239*
     a4(193) -> 194*
     a4(178) -> 179*
     a4(230) -> 231*
     a4(220) -> 221*
     a0(3) -> 3*
     b5(254) -> 255*
     b5(253) -> 254*
     b5(255) -> 256*
     b0(3) -> 3*
     a5(252) -> 253*
     a5(251) -> 252*
     a5(250) -> 251*
     b1(15) -> 16*
     b1(22) -> 23*
     b1(14) -> 15*
     b1(21) -> 22*
     b1(16) -> 17*
     b1(23) -> 24*
     a1(20) -> 21*
     a1(67) -> 68*
     a1(27) -> 28*
     a1(12) -> 13*
     a1(69) -> 70*
     a1(19) -> 20*
     a1(11) -> 12*
     a1(18) -> 19*
     a1(13) -> 14*
     b2(50) -> 51*
     b2(45) -> 46*
     b2(127) -> 128*
     b2(107) -> 108*
     b2(82) -> 83*
     b2(52) -> 53*
     b2(129) -> 130*
     b2(44) -> 45*
     b2(106) -> 107*
     b2(81) -> 82*
     b2(51) -> 52*
     b2(128) -> 129*
     b2(108) -> 109*
     b2(83) -> 84*
     b2(43) -> 44*
     a2(40) -> 41*
     a2(47) -> 48*
     a2(42) -> 43*
     a2(124) -> 125*
     a2(104) -> 105*
     a2(79) -> 80*
     a2(49) -> 50*
     a2(126) -> 127*
     a2(41) -> 42*
     a2(138) -> 139*
     a2(103) -> 104*
     a2(78) -> 79*
     a2(63) -> 64*
     a2(48) -> 49*
     a2(125) -> 126*
     a2(105) -> 106*
     a2(85) -> 86*
     a2(80) -> 81*
     b3(202) -> 203*
     b3(172) -> 173*
     b3(122) -> 123*
     b3(92) -> 93*
     b3(204) -> 205*
     b3(174) -> 175*
     b3(164) -> 165*
     b3(154) -> 155*
     b3(156) -> 157*
     b3(121) -> 122*
     b3(91) -> 92*
     b3(203) -> 204*
     b3(173) -> 174*
     b3(163) -> 164*
     b3(165) -> 166*
     b3(155) -> 156*
     b3(120) -> 121*
     b3(90) -> 91*
     3 -> 11*
     14 -> 47*
     15 -> 40,18
     16 -> 27*
     17 -> 13,12,3
     21 -> 85*
     22 -> 67,63
     23 -> 69*
     24 -> 13,3,11,12
     28 -> 19*
     43 -> 117*
     44 -> 103,87
     45 -> 78*
     46 -> 48,14,13
     51 -> 124*
     53 -> 20*
     64 -> 41*
     68 -> 12*
     70 -> 12*
     82 -> 169,138
     84 -> 20,42
     86 -> 41*
     90 -> 220*
     92 -> 160*
     93 -> 50,49
     107 -> 149*
     109 -> 48*
     123 -> 80*
     128 -> 151*
     130 -> 86*
     139 -> 125*
     150 -> 88*
     154 -> 229*
     155 -> 192*
     156 -> 199*
     157 -> 43,117
     166 -> 126*
     173 -> 176*
     175 -> 118*
     182 -> 120*
     198 -> 119*
     203 -> 236*
     205 -> 89,105
     226 -> 162*
     235 -> 201*
     240 -> 250*
     242 -> 221*
     256 -> 223*
   problem:
    strict:
     
    weak:
     a(a(b(b(x1)))) -> b(b(b(a(a(a(x1))))))
   Qed