YES(?,O(n^3))

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(b(a(x1))) -> a(a(b(b(a(a(x1))))))
   b(a(a(b(x1)))) -> b(a(b(x1)))
  weak:
   
  Bounds Processor:
   bound: 4
   enrichment: match
   automaton:
    final states: {2,1}
    transitions:
     b3(272) -> 273*
     b3(284) -> 285*
     b3(214) -> 215*
     b3(271) -> 272*
     b3(161) -> 162*
     b3(218) -> 219*
     b3(163) -> 164*
     b3(153) -> 154*
     b3(155) -> 156*
     b4(364) -> 365*
     b4(290) -> 291*
     b4(362) -> 363*
     b4(292) -> 293*
     a4(291) -> 292*
     a4(363) -> 364*
     a0(2) -> 1*
     a0(1) -> 1*
     b0(2) -> 2*
     b0(1) -> 2*
     a1(55) -> 56*
     a1(102) -> 103*
     a1(234) -> 235*
     a1(124) -> 125*
     a1(19) -> 20*
     a1(36) -> 37*
     a1(118) -> 119*
     a1(58) -> 59*
     b1(20) -> 21*
     b1(57) -> 58*
     b1(174) -> 175*
     b1(101) -> 102*
     b1(56) -> 57*
     b1(103) -> 104*
     b1(28) -> 29*
     b1(18) -> 19*
     a2(324) -> 325*
     a2(139) -> 140*
     a2(69) -> 70*
     a2(226) -> 227*
     a2(201) -> 202*
     a2(96) -> 97*
     a2(138) -> 139*
     a2(260) -> 261*
     a2(135) -> 136*
     b2(70) -> 71*
     b2(147) -> 148*
     b2(137) -> 138*
     b2(97) -> 98*
     b2(89) -> 90*
     b2(136) -> 137*
     b2(268) -> 269*
     b2(68) -> 69*
     b2(195) -> 196*
     b2(95) -> 96*
     b2(85) -> 86*
     a3(162) -> 163*
     a3(274) -> 275*
     a3(154) -> 155*
     a3(303) -> 304*
     a3(273) -> 274*
     a3(320) -> 321*
     a3(270) -> 271*
     a3(307) -> 308*
     1 -> 124,28
     2 -> 118,18
     18 -> 89*
     19 -> 201*
     20 -> 68,55
     21 -> 86,29,36,2
     28 -> 85*
     29 -> 19*
     36 -> 226*
     37 -> 202,70,119,1,20
     57 -> 95*
     59 -> 36*
     71 -> 137,57
     86 -> 69*
     90 -> 69*
     95 -> 153*
     96 -> 307,234
     97 -> 218,135,101
     98 -> 21*
     101 -> 268*
     102 -> 260*
     104 -> 86*
     119 -> 55*
     125 -> 55*
     136 -> 227,202
     137 -> 174,161
     138 -> 303*
     139 -> 320,147
     140 -> 227,261,202,324,70,119,37,103
     147 -> 214*
     148 -> 21,104
     156 -> 272,71,137
     161 -> 290*
     163 -> 270*
     164 -> 71,86,69
     174 -> 195*
     175 -> 19*
     196 -> 69*
     202 -> 135*
     215 -> 154*
     219 -> 154*
     227 -> 69*
     235 -> 55*
     261 -> 69*
     269 -> 69*
     272 -> 362*
     274 -> 284*
     275 -> 155,227,202,70
     285 -> 71*
     293 -> 272*
     304 -> 270*
     308 -> 270*
     321 -> 154*
     325 -> 70*
     365 -> 156*
   problem:
    strict:
     a(b(a(x1))) -> a(a(b(b(a(a(x1))))))
    weak:
     b(a(a(b(x1)))) -> b(a(b(x1)))
   Matrix Interpretation Processor:
    dimension: 3
    max_matrix:
     [1 1 1]
     [0 0 1]
     [0 0 0]
     interpretation:
                [1 0 1]     [0]
      [b](x0) = [0 0 1]x0 + [1]
                [0 0 0]     [0],
      
                [1 1 0]     [0]
      [a](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [1]
     orientation:
                    [1 1 0]     [3]    [1 1 0]     [2]                       
      a(b(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(a(b(b(a(a(x1))))))
                    [0 0 0]     [1]    [0 0 0]     [1]                       
      
                       [1 0 2]     [2]    [1 0 2]     [2]              
      b(a(a(b(x1)))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = b(a(b(x1)))
                       [0 0 0]     [0]    [0 0 0]     [0]              
     problem:
      strict:
       
      weak:
       a(b(a(x1))) -> a(a(b(b(a(a(x1))))))
       b(a(a(b(x1)))) -> b(a(b(x1)))
     Qed