YES

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

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