YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 3
  interpretation:
             [1  0  0 ]  
   [b](x0) = [-& 0  0 ]x0
             [1  0  0 ]  ,
   
             [3 2 2]  
   [a](x0) = [2 1 1]x0
             [3 2 2]  
  orientation:
           [3 2 2]      [2 1 1]             
   a(x1) = [2 1 1]x1 >= [1 0 0]x1 = b(b(x1))
           [3 2 2]      [2 1 1]             
   
                 [3 2 2]      [3 2 2]          
   b(b(b(x1))) = [2 1 1]x1 >= [2 1 1]x1 = a(x1)
                 [3 2 2]      [3 2 2]          
  problem:
   b(b(b(x1))) -> a(x1)
  Arctic Interpretation Processor:
   dimension: 3
   interpretation:
              [1  0  -&]  
    [b](x0) = [0  1  0 ]x0
              [1  0  -&]  ,
    
              [0  -& -&]  
    [a](x0) = [-& -& -&]x0
              [-& -& -&]  
   orientation:
                  [3 2 1]      [0  -& -&]          
    b(b(b(x1))) = [2 3 2]x1 >= [-& -& -&]x1 = a(x1)
                  [3 2 1]      [-& -& -&]          
   problem:
    
   Qed