YES

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

Proof:
 String Reversal Processor:
  b(a(x1)) -> a(c(b(x1)))
  c(b(x1)) -> b(b(c(x1)))
  c(a(x1)) -> b(a(c(x1)))
  DP Processor:
   DPs:
    b#(a(x1)) -> b#(x1)
    b#(a(x1)) -> c#(b(x1))
    c#(b(x1)) -> c#(x1)
    c#(b(x1)) -> b#(c(x1))
    c#(b(x1)) -> b#(b(c(x1)))
    c#(a(x1)) -> c#(x1)
    c#(a(x1)) -> b#(a(c(x1)))
   TRS:
    b(a(x1)) -> a(c(b(x1)))
    c(b(x1)) -> b(b(c(x1)))
    c(a(x1)) -> b(a(c(x1)))
   TDG Processor:
    DPs:
     b#(a(x1)) -> b#(x1)
     b#(a(x1)) -> c#(b(x1))
     c#(b(x1)) -> c#(x1)
     c#(b(x1)) -> b#(c(x1))
     c#(b(x1)) -> b#(b(c(x1)))
     c#(a(x1)) -> c#(x1)
     c#(a(x1)) -> b#(a(c(x1)))
    TRS:
     b(a(x1)) -> a(c(b(x1)))
     c(b(x1)) -> b(b(c(x1)))
     c(a(x1)) -> b(a(c(x1)))
    graph:
     c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> b#(a(c(x1)))
     c#(a(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1)
     c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> b#(b(c(x1)))
     c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> b#(c(x1))
     c#(a(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1)
     c#(a(x1)) -> b#(a(c(x1))) -> b#(a(x1)) -> c#(b(x1))
     c#(a(x1)) -> b#(a(c(x1))) -> b#(a(x1)) -> b#(x1)
     c#(b(x1)) -> c#(x1) -> c#(a(x1)) -> b#(a(c(x1)))
     c#(b(x1)) -> c#(x1) -> c#(a(x1)) -> c#(x1)
     c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> b#(b(c(x1)))
     c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> b#(c(x1))
     c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1)
     c#(b(x1)) -> b#(c(x1)) -> b#(a(x1)) -> c#(b(x1))
     c#(b(x1)) -> b#(c(x1)) -> b#(a(x1)) -> b#(x1)
     c#(b(x1)) -> b#(b(c(x1))) -> b#(a(x1)) -> c#(b(x1))
     c#(b(x1)) -> b#(b(c(x1))) -> b#(a(x1)) -> b#(x1)
     b#(a(x1)) -> c#(b(x1)) -> c#(a(x1)) -> b#(a(c(x1)))
     b#(a(x1)) -> c#(b(x1)) -> c#(a(x1)) -> c#(x1)
     b#(a(x1)) -> c#(b(x1)) -> c#(b(x1)) -> b#(b(c(x1)))
     b#(a(x1)) -> c#(b(x1)) -> c#(b(x1)) -> b#(c(x1))
     b#(a(x1)) -> c#(b(x1)) -> c#(b(x1)) -> c#(x1)
     b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> c#(b(x1))
     b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = 1x0 + 5,
      
      [b#](x0) = x0 + 0,
      
      [c](x0) = x0 + 5,
      
      [a](x0) = 3x0 + 8,
      
      [b](x0) = x0
     orientation:
      b#(a(x1)) = 3x1 + 8 >= x1 + 0 = b#(x1)
      
      b#(a(x1)) = 3x1 + 8 >= 1x1 + 5 = c#(b(x1))
      
      c#(b(x1)) = 1x1 + 5 >= 1x1 + 5 = c#(x1)
      
      c#(b(x1)) = 1x1 + 5 >= x1 + 5 = b#(c(x1))
      
      c#(b(x1)) = 1x1 + 5 >= x1 + 5 = b#(b(c(x1)))
      
      c#(a(x1)) = 4x1 + 9 >= 1x1 + 5 = c#(x1)
      
      c#(a(x1)) = 4x1 + 9 >= 3x1 + 8 = b#(a(c(x1)))
      
      b(a(x1)) = 3x1 + 8 >= 3x1 + 8 = a(c(b(x1)))
      
      c(b(x1)) = x1 + 5 >= x1 + 5 = b(b(c(x1)))
      
      c(a(x1)) = 3x1 + 8 >= 3x1 + 8 = b(a(c(x1)))
     problem:
      DPs:
       c#(b(x1)) -> c#(x1)
       c#(b(x1)) -> b#(c(x1))
       c#(b(x1)) -> b#(b(c(x1)))
      TRS:
       b(a(x1)) -> a(c(b(x1)))
       c(b(x1)) -> b(b(c(x1)))
       c(a(x1)) -> b(a(c(x1)))
     EDG Processor:
      DPs:
       c#(b(x1)) -> c#(x1)
       c#(b(x1)) -> b#(c(x1))
       c#(b(x1)) -> b#(b(c(x1)))
      TRS:
       b(a(x1)) -> a(c(b(x1)))
       c(b(x1)) -> b(b(c(x1)))
       c(a(x1)) -> b(a(c(x1)))
      graph:
       c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> c#(x1)
       c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> b#(c(x1))
       c#(b(x1)) -> c#(x1) -> c#(b(x1)) -> b#(b(c(x1)))
      SCC Processor:
       #sccs: 1
       #rules: 1
       #arcs: 3/9
       DPs:
        c#(b(x1)) -> c#(x1)
       TRS:
        b(a(x1)) -> a(c(b(x1)))
        c(b(x1)) -> b(b(c(x1)))
        c(a(x1)) -> b(a(c(x1)))
       Matrix Interpretation Processor: dim=4
        
        interpretation:
         [c#](x0) = [0 0 1 1]x0,
         
                   [1 0 0 0]  
                   [0 0 0 0]  
         [c](x0) = [0 0 1 1]x0
                   [0 0 1 1]  ,
         
                   [1 0 0 0]     [1]
                   [0 0 0 0]     [0]
         [a](x0) = [0 0 0 0]x0 + [0]
                   [0 0 0 0]     [1],
         
                   [1 0 0 0]     [0]
                   [0 0 0 0]     [0]
         [b](x0) = [0 0 0 1]x0 + [0]
                   [0 0 1 0]     [1]
        orientation:
         c#(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 = c#(x1)
         
                    [1 0 0 0]     [1]    [1 0 0 0]     [1]              
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         b(a(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = a(c(b(x1)))
                    [0 0 0 0]     [1]    [0 0 0 0]     [1]              
         
                    [1 0 0 0]     [0]    [1 0 0 0]     [0]              
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         c(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = b(b(c(x1)))
                    [0 0 1 1]     [1]    [0 0 1 1]     [1]              
         
                    [1 0 0 0]     [1]    [1 0 0 0]     [1]              
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         c(a(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(a(c(x1)))
                    [0 0 0 0]     [1]    [0 0 0 0]     [1]              
        problem:
         DPs:
          
         TRS:
          b(a(x1)) -> a(c(b(x1)))
          c(b(x1)) -> b(b(c(x1)))
          c(a(x1)) -> b(a(c(x1)))
        Qed