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)))
  String Reversal Processor:
   c(b(x1)) -> b(b(c(x1)))
   a(b(x1)) -> b(c(a(x1)))
   DP Processor:
    DPs:
     c#(b(x1)) -> c#(x1)
     a#(b(x1)) -> a#(x1)
     a#(b(x1)) -> c#(a(x1))
    TRS:
     c(b(x1)) -> b(b(c(x1)))
     a(b(x1)) -> b(c(a(x1)))
    TDG Processor:
     DPs:
      c#(b(x1)) -> c#(x1)
      a#(b(x1)) -> a#(x1)
      a#(b(x1)) -> c#(a(x1))
     TRS:
      c(b(x1)) -> b(b(c(x1)))
      a(b(x1)) -> b(c(a(x1)))
     graph:
      a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> c#(a(x1))
      a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> a#(x1)
      a#(b(x1)) -> c#(a(x1)) -> c#(b(x1)) -> c#(x1)
      c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1)
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 4/9
      DPs:
       a#(b(x1)) -> a#(x1)
      TRS:
       c(b(x1)) -> b(b(c(x1)))
       a(b(x1)) -> b(c(a(x1)))
      Usable Rule Processor:
       DPs:
        a#(b(x1)) -> a#(x1)
       TRS:
        
       Arctic Interpretation Processor:
        dimension: 4
        usable rules:
         
        interpretation:
         [a#](x0) = [0  -& -& -&]x0,
         
                   [1 0 0 0]     [0]
                   [1 0 0 0]     [0]
         [b](x0) = [1 0 0 0]x0 + [0]
                   [0 0 0 0]     [0]
        orientation:
         a#(b(x1)) = [1 0 0 0]x1 + [0] >= [0  -& -& -&]x1 = a#(x1)
        problem:
         DPs:
          
         TRS:
          
        Qed
      
      DPs:
       c#(b(x1)) -> c#(x1)
      TRS:
       c(b(x1)) -> b(b(c(x1)))
       a(b(x1)) -> b(c(a(x1)))
      Usable Rule Processor:
       DPs:
        c#(b(x1)) -> c#(x1)
       TRS:
        
       Arctic Interpretation Processor:
        dimension: 4
        usable rules:
         
        interpretation:
         [c#](x0) = [0  -& -& -&]x0,
         
                   [1 0 0 0]     [0]
                   [1 0 0 0]     [0]
         [b](x0) = [1 0 0 0]x0 + [0]
                   [0 0 0 0]     [0]
        orientation:
         c#(b(x1)) = [1 0 0 0]x1 + [0] >= [0  -& -& -&]x1 = c#(x1)
        problem:
         DPs:
          
         TRS:
          
        Qed