YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0  -&]  
   [b](x0) = [2  1 ]x0,
   
             [2  -&]  
   [a](x0) = [2  2 ]x0
  orientation:
             [4  -&]     [0  -&]           
   a(a(x)) = [4  4 ]x >= [3  2 ]x = b(b(x))
   
                [2  -&]     [2  -&]              
   b(b(a(x))) = [5  4 ]x >= [5  4 ]x = a(b(b(x)))
  problem:
   b(b(a(x))) -> a(b(b(x)))
  KBO Processor:
   weight function:
    w0 = 1
    w(b) = w(a) = 1
   precedence:
    b > a
   problem:
    
   Qed