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 ]  
   [b](x0) = [0  -& -&]x0
             [0  0  0 ]  ,
   
             [0  0  -&]  
   [a](x0) = [0  -& 3 ]x0
             [0  -& 0 ]  
  orientation:
                 [3 0 3]      [0 0 0]                
   a(a(a(x1))) = [3 3 3]x1 >= [0 0 0]x1 = b(b(b(x1)))
                 [0 0 3]      [0 0 0]                
   
                    [3 3 3]             
   b(a(a(b(x1)))) = [3 3 3]x1 >= x1 = x1
                    [3 3 3]             
   
                    [3 3 3]      [3 3 3]                      
   b(a(a(b(x1)))) = [3 3 3]x1 >= [3 3 3]x1 = b(a(a(a(b(x1)))))
                    [3 3 3]      [3 3 3]                      
  problem:
   a(a(a(x1))) -> b(b(b(x1)))
   b(a(a(b(x1)))) -> b(a(a(a(b(x1)))))
  Bounds Processor:
   bound: 1
   enrichment: match
   automaton:
    final states: {5,1}
    transitions:
     b1(10) -> 11*
     b1(9) -> 10*
     b1(11) -> 12*
     f20() -> 2*
     b0(2) -> 3*
     b0(4) -> 1*
     b0(8) -> 5*
     b0(3) -> 4*
     a0(7) -> 8*
     a0(6) -> 7*
     a0(3) -> 6*
     3 -> 9*
     5 -> 3,9
     12 -> 8*
   problem:
    
   Qed