YES(?,O(n^1))

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
  weak:
   
  Bounds Processor:
   bound: 6
   enrichment: match
   automaton:
    final states: {2,1}
    transitions:
     a3(187) -> 188*
     a3(132) -> 133*
     a3(117) -> 118*
     a3(112) -> 113*
     a3(92) -> 93*
     a3(189) -> 190*
     a3(129) -> 130*
     a3(119) -> 120*
     a3(94) -> 95*
     a3(186) -> 187*
     a3(131) -> 132*
     a3(116) -> 117*
     a3(96) -> 97*
     a3(188) -> 189*
     a3(133) -> 134*
     a3(118) -> 119*
     a3(93) -> 94*
     a3(185) -> 186*
     a3(130) -> 131*
     a3(125) -> 126*
     a3(120) -> 121*
     a3(95) -> 96*
     b4(232) -> 233*
     b4(182) -> 183*
     b4(259) -> 260*
     b4(234) -> 235*
     b4(224) -> 225*
     b4(204) -> 205*
     b4(154) -> 155*
     b4(144) -> 145*
     b4(261) -> 262*
     b4(181) -> 182*
     b4(156) -> 157*
     b4(233) -> 234*
     b4(223) -> 224*
     b4(203) -> 204*
     b4(183) -> 184*
     b4(143) -> 144*
     b4(260) -> 261*
     b4(225) -> 226*
     b4(205) -> 206*
     b4(155) -> 156*
     b4(145) -> 146*
     a4(257) -> 258*
     a4(227) -> 228*
     a4(222) -> 223*
     a4(202) -> 203*
     a4(177) -> 178*
     a4(152) -> 153*
     a4(142) -> 143*
     a4(254) -> 255*
     a4(229) -> 230*
     a4(219) -> 220*
     a4(199) -> 200*
     a4(179) -> 180*
     a4(149) -> 150*
     a4(139) -> 140*
     a4(276) -> 277*
     a4(256) -> 257*
     a4(231) -> 232*
     a4(221) -> 222*
     a4(201) -> 202*
     a4(176) -> 177*
     a4(151) -> 152*
     a4(141) -> 142*
     a4(258) -> 259*
     a4(228) -> 229*
     a4(218) -> 219*
     a4(198) -> 199*
     a4(178) -> 179*
     a4(153) -> 154*
     a4(138) -> 139*
     a4(255) -> 256*
     a4(230) -> 231*
     a4(220) -> 221*
     a4(200) -> 201*
     a4(180) -> 181*
     a4(150) -> 151*
     a4(140) -> 141*
     a0(2) -> 1*
     a0(1) -> 1*
     b5(272) -> 273*
     b5(252) -> 253*
     b5(212) -> 213*
     b5(364) -> 365*
     b5(274) -> 275*
     b5(214) -> 215*
     b5(366) -> 367*
     b5(311) -> 312*
     b5(301) -> 302*
     b5(251) -> 252*
     b5(303) -> 304*
     b5(273) -> 274*
     b5(213) -> 214*
     b5(365) -> 366*
     b5(310) -> 311*
     b5(250) -> 251*
     b5(312) -> 313*
     b5(302) -> 303*
     b0(2) -> 2*
     b0(1) -> 2*
     a5(267) -> 268*
     a5(247) -> 248*
     a5(207) -> 208*
     a5(359) -> 360*
     a5(309) -> 310*
     a5(299) -> 300*
     a5(269) -> 270*
     a5(249) -> 250*
     a5(209) -> 210*
     a5(361) -> 362*
     a5(306) -> 307*
     a5(296) -> 297*
     a5(271) -> 272*
     a5(246) -> 247*
     a5(211) -> 212*
     a5(363) -> 364*
     a5(308) -> 309*
     a5(298) -> 299*
     a5(268) -> 269*
     a5(248) -> 249*
     a5(208) -> 209*
     a5(360) -> 361*
     a5(305) -> 306*
     a5(300) -> 301*
     a5(270) -> 271*
     a5(245) -> 246*
     a5(210) -> 211*
     a5(362) -> 363*
     a5(307) -> 308*
     a5(297) -> 298*
     b1(10) -> 11*
     b1(9) -> 10*
     b1(11) -> 12*
     b6(339) -> 340*
     b6(329) -> 330*
     b6(338) -> 339*
     b6(328) -> 329*
     b6(330) -> 331*
     b6(337) -> 338*
     a1(35) -> 36*
     a1(5) -> 6*
     a1(37) -> 38*
     a1(7) -> 8*
     a1(4) -> 5*
     a1(31) -> 32*
     a1(6) -> 7*
     a1(8) -> 9*
     a6(334) -> 335*
     a6(324) -> 325*
     a6(336) -> 337*
     a6(326) -> 327*
     a6(333) -> 334*
     a6(323) -> 324*
     a6(335) -> 336*
     a6(325) -> 326*
     a6(332) -> 333*
     a6(327) -> 328*
     b2(55) -> 56*
     b2(62) -> 63*
     b2(64) -> 65*
     b2(54) -> 55*
     b2(63) -> 64*
     b2(53) -> 54*
     a2(70) -> 71*
     a2(60) -> 61*
     a2(50) -> 51*
     a2(57) -> 58*
     a2(52) -> 53*
     a2(59) -> 60*
     a2(49) -> 50*
     a2(101) -> 102*
     a2(61) -> 62*
     a2(51) -> 52*
     a2(58) -> 59*
     a2(48) -> 49*
     a2(90) -> 91*
     b3(192) -> 193*
     b3(122) -> 123*
     b3(97) -> 98*
     b3(134) -> 135*
     b3(99) -> 100*
     b3(191) -> 192*
     b3(136) -> 137*
     b3(121) -> 122*
     b3(123) -> 124*
     b3(98) -> 99*
     b3(190) -> 191*
     b3(135) -> 136*
     1 -> 31*
     2 -> 4*
     9 -> 70*
     10 -> 48,37
     11 -> 35*
     12 -> 6,32,1
     32 -> 5*
     36 -> 5*
     38 -> 5*
     54 -> 125,57
     56 -> 50,7,8,6
     62 -> 112*
     63 -> 92,90
     64 -> 101*
     65 -> 71,9,8
     71 -> 49*
     91 -> 58*
     98 -> 116*
     100 -> 50,51
     102 -> 49*
     113 -> 93*
     121 -> 149*
     123 -> 129*
     124 -> 53,52
     126 -> 117*
     135 -> 138*
     137 -> 118,59
     144 -> 198,185
     146 -> 61,120
     155 -> 176*
     157 -> 131*
     184 -> 133*
     191 -> 218*
     193 -> 113*
     204 -> 207*
     206 -> 150*
     213 -> 245*
     215 -> 152*
     224 -> 227*
     226 -> 95*
     232 -> 296*
     234 -> 254*
     235 -> 97*
     250 -> 323*
     252 -> 267*
     253 -> 154*
     260 -> 276*
     262 -> 118*
     273 -> 305*
     275 -> 178*
     277 -> 139*
     302 -> 359*
     304 -> 256*
     313 -> 180*
     329 -> 332*
     331 -> 269*
     340 -> 271*
     367 -> 258*
   problem:
    strict:
     
    weak:
     a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
   Qed