YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 3
  interpretation:
             [0  0  1 ]  
   [b](x0) = [-& -& 0 ]x0
             [-& -& 0 ]  ,
   
             [0  1  -&]  
   [a](x0) = [-& 0  0 ]x0
             [1  0  0 ]  
  orientation:
                 [2 1 1]      [0  0  1 ]                
   a(a(a(x1))) = [1 2 0]x1 >= [-& -& 0 ]x1 = b(b(b(x1)))
                 [1 2 2]      [-& -& 0 ]                
   
                    [2 2 3]             
   b(a(a(b(x1)))) = [1 1 2]x1 >= x1 = x1
                    [1 1 2]             
   
                    [2 2 3]      [2 2 3]                      
   b(a(a(b(x1)))) = [1 1 2]x1 >= [1 1 2]x1 = b(a(a(a(b(x1)))))
                    [1 1 2]      [1 1 2]                      
  problem:
   a(a(a(x1))) -> b(b(b(x1)))
   b(a(a(b(x1)))) -> b(a(a(a(b(x1)))))
  Bounds Processor:
   bound: 2
   enrichment: match
   automaton:
    final states: {3}
    transitions:
     b1(10) -> 11*
     b1(9) -> 10*
     b1(8) -> 9*
     a1(35) -> 36*
     a1(37) -> 38*
     a1(12) -> 13*
     a1(14) -> 15*
     a1(36) -> 37*
     a1(13) -> 14*
     b2(25) -> 26*
     b2(42) -> 43*
     b2(24) -> 25*
     b2(41) -> 42*
     b2(43) -> 44*
     b2(23) -> 24*
     a0(3) -> 3*
     b0(3) -> 3*
     3 -> 8*
     9 -> 12*
     11 -> 9,12,35,3
     12 -> 23*
     15 -> 10*
     26 -> 15,10
     35 -> 41*
     38 -> 8*
     44 -> 38,8
   problem:
    
   Qed