YES(?,O(n^1))

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

Proof:
 Complexity Transformation Processor:
  strict:
   a(b(a(x1))) -> b(a(x1))
   b(b(b(x1))) -> b(a(b(x1)))
   a(a(x1)) -> b(b(b(x1)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [b](x0) = x0 + 1,
     
     [a](x0) = x0
    orientation:
     a(b(a(x1))) = x1 + 1 >= x1 + 1 = b(a(x1))
     
     b(b(b(x1))) = x1 + 3 >= x1 + 2 = b(a(b(x1)))
     
     a(a(x1)) = x1 >= x1 + 3 = b(b(b(x1)))
    problem:
     strict:
      a(b(a(x1))) -> b(a(x1))
      a(a(x1)) -> b(b(b(x1)))
     weak:
      b(b(b(x1))) -> b(a(b(x1)))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [b](x0) = x0 + 1,
       
       [a](x0) = x0 + 1
      orientation:
       a(b(a(x1))) = x1 + 3 >= x1 + 2 = b(a(x1))
       
       a(a(x1)) = x1 + 2 >= x1 + 3 = b(b(b(x1)))
       
       b(b(b(x1))) = x1 + 3 >= x1 + 3 = b(a(b(x1)))
      problem:
       strict:
        a(a(x1)) -> b(b(b(x1)))
       weak:
        a(b(a(x1))) -> b(a(x1))
        b(b(b(x1))) -> b(a(b(x1)))
      Bounds Processor:
       bound: 2
       enrichment: match
       automaton:
        final states: {2,1}
        transitions:
         b1(5) -> 6*
         b1(137) -> 138*
         b1(14) -> 15*
         b1(4) -> 5*
         b1(121) -> 122*
         b1(6) -> 7*
         b1(123) -> 124*
         b1(80) -> 81*
         a1(42) -> 43*
         a1(22) -> 23*
         a1(34) -> 35*
         a1(24) -> 25*
         a1(46) -> 47*
         a1(48) -> 49*
         b2(70) -> 71*
         b2(60) -> 61*
         b2(40) -> 41*
         b2(30) -> 31*
         b2(62) -> 63*
         b2(32) -> 33*
         b2(91) -> 92*
         b2(31) -> 32*
         b2(133) -> 134*
         b2(135) -> 136*
         a0(2) -> 1*
         a0(1) -> 1*
         a2(82) -> 83*
         a2(109) -> 110*
         a2(99) -> 100*
         a2(54) -> 55*
         a2(131) -> 132*
         a2(86) -> 87*
         a2(113) -> 114*
         a2(103) -> 104*
         a2(93) -> 94*
         a2(90) -> 91*
         b0(2) -> 2*
         b0(1) -> 2*
         1 -> 48,14
         2 -> 46,1,4
         4 -> 70*
         5 -> 104,49,34
         6 -> 62,22
         7 -> 31,43,35,23,6,5,42,1
         14 -> 60*
         15 -> 100,94,114,110,23,47,55,35,25,2,24,5
         22 -> 93*
         23 -> 14*
         24 -> 113,30
         25 -> 6*
         30 -> 123*
         31 -> 134,138,132,92,124,122,100,114,110,71,63,7,81,33,61,83,87,23,47,94,41,86,15,32
         32 -> 80*
         33 -> 94,55,54,23
         34 -> 109,40
         35 -> 6*
         40 -> 121*
         41 -> 82,31
         42 -> 90*
         43 -> 14*
         46 -> 99*
         47 -> 14*
         48 -> 103*
         49 -> 14*
         55 -> 30*
         61 -> 54*
         63 -> 54*
         71 -> 54*
         81 -> 22*
         83 -> 32*
         87 -> 32*
         91 -> 137*
         92 -> 132,23,131,100,104,94,114,110,55
         94 -> 91*
         100 -> 91*
         104 -> 91*
         110 -> 30*
         114 -> 30*
         121 -> 133*
         122 -> 24*
         123 -> 135*
         124 -> 24*
         132 -> 30*
         134 -> 54*
         136 -> 54*
         138 -> 22*
       problem:
        strict:
         
        weak:
         a(a(x1)) -> b(b(b(x1)))
         a(b(a(x1))) -> b(a(x1))
         b(b(b(x1))) -> b(a(b(x1)))
       Qed