YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0 2]  
   [a](x0) = [0 0]x0,
   
             [2 2]  
   [b](x0) = [0 0]x0
  orientation:
              [4 4]      [2 4]                
   b(b(x1)) = [2 2]x1 >= [2 2]x1 = a(a(a(x1)))
   
                 [4 4]      [0 2]          
   b(a(b(x1))) = [2 2]x1 >= [0 0]x1 = a(x1)
   
                 [4 4]      [4 4]                
   b(a(a(x1))) = [2 2]x1 >= [2 2]x1 = b(a(b(x1)))
  problem:
   b(b(x1)) -> a(a(a(x1)))
   b(a(a(x1))) -> b(a(b(x1)))
  String Reversal Processor:
   b(b(x1)) -> a(a(a(x1)))
   a(a(b(x1))) -> b(a(b(x1)))
   Bounds Processor:
    bound: 3
    enrichment: match
    automaton:
     final states: {5,1}
     transitions:
      b1(10) -> 11*
      b1(8) -> 9*
      a1(20) -> 21*
      a1(22) -> 23*
      a1(9) -> 10*
      a1(21) -> 22*
      a2(25) -> 26*
      a2(37) -> 38*
      a2(24) -> 25*
      a2(26) -> 27*
      b2(36) -> 37*
      b2(38) -> 39*
      f20() -> 2*
      b3(40) -> 41*
      b3(42) -> 43*
      a0(2) -> 3*
      a0(4) -> 1*
      a0(6) -> 7*
      a0(3) -> 4*
      a3(41) -> 42*
      b0(7) -> 5*
      b0(2) -> 6*
      1 -> 6*
      5 -> 3,4
      7 -> 8*
      8 -> 36*
      10 -> 24,20
      11 -> 1,7
      23 -> 5*
      27 -> 37,9
      38 -> 40*
      39 -> 25,21
      43 -> 23,5,4,27
    problem:
     
    Qed