YES

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

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