YES

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

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