YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0  -&]  
   [c](x0) = [0  -&]x0,
   
             [0 0]  
   [a](x0) = [1 1]x0,
   
             [0 0]  
   [b](x0) = [1 1]x0
  orientation:
              [1 1]      [1 1]             
   a(b(x1)) = [2 2]x1 >= [2 2]x1 = b(a(x1))
   
              [1 1]      [0 0]                
   b(a(x1)) = [2 2]x1 >= [1 1]x1 = 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