YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0  -&]  
   [c](x0) = [-& -&]x0,
   
             [0  0 ]  
   [a](x0) = [-& 2 ]x0,
   
             [0  -&]  
   [b](x0) = [2  1 ]x0
  orientation:
              [2 1]      [0 0]                
   a(b(x1)) = [4 3]x1 >= [2 2]x1 = b(c(a(x1)))
   
              [0  -&]      [0  -&]                
   b(c(x1)) = [2  -&]x1 >= [-& -&]x1 = c(b(b(x1)))
   
              [0 0]      [0  -&]                
   b(a(x1)) = [2 3]x1 >= [-& -&]x1 = a(c(b(x1)))
  problem:
   b(c(x1)) -> c(b(b(x1)))
   b(a(x1)) -> a(c(b(x1)))
  DP Processor:
   DPs:
    b#(c(x1)) -> b#(x1)
    b#(c(x1)) -> b#(b(x1))
    b#(a(x1)) -> b#(x1)
   TRS:
    b(c(x1)) -> c(b(b(x1)))
    b(a(x1)) -> a(c(b(x1)))
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [b#](x0) = 9x0 + 0,
     
     [c](x0) = x0 + -10,
     
     [a](x0) = 1x0 + 7,
     
     [b](x0) = x0 + -9
    orientation:
     b#(c(x1)) = 9x1 + 0 >= 9x1 + 0 = b#(x1)
     
     b#(c(x1)) = 9x1 + 0 >= 9x1 + 0 = b#(b(x1))
     
     b#(a(x1)) = 10x1 + 16 >= 9x1 + 0 = b#(x1)
     
     b(c(x1)) = x1 + -9 >= x1 + -9 = c(b(b(x1)))
     
     b(a(x1)) = 1x1 + 7 >= 1x1 + 7 = a(c(b(x1)))
    problem:
     DPs:
      b#(c(x1)) -> b#(x1)
      b#(c(x1)) -> b#(b(x1))
     TRS:
      b(c(x1)) -> c(b(b(x1)))
      b(a(x1)) -> a(c(b(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b#](x0) = x0,
      
      [c](x0) = 1x0,
      
      [a](x0) = 13,
      
      [b](x0) = x0
     orientation:
      b#(c(x1)) = 1x1 >= x1 = b#(x1)
      
      b#(c(x1)) = 1x1 >= x1 = b#(b(x1))
      
      b(c(x1)) = 1x1 >= 1x1 = c(b(b(x1)))
      
      b(a(x1)) = 13 >= 13 = a(c(b(x1)))
     problem:
      DPs:
       
      TRS:
       b(c(x1)) -> c(b(b(x1)))
       b(a(x1)) -> a(c(b(x1)))
     Qed