YES

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

Proof:
 String Reversal Processor:
  a(a(x1)) -> a(b(a(b(c(x1)))))
  b(a(b(x1))) -> b(x1)
  a(a(a(x1))) -> a(c(c(x1)))
  c(c(x1)) -> a(b(c(b(a(x1)))))
  a(c(a(x1))) -> a(c(c(x1)))
  c(a(c(x1))) -> c(a(a(x1)))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
              [1 2]     [0]
    [c](x0) = [0 0]x0 + [1],
    
              [1 1]  
    [b](x0) = [0 0]x0,
    
              [1 2]     [0]
    [a](x0) = [0 0]x0 + [1]
   orientation:
               [1 2]     [2]    [1 2]     [2]                    
    a(a(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(a(b(c(x1)))))
    
                  [1 1]     [1]    [1 1]          
    b(a(b(x1))) = [0 0]x1 + [0] >= [0 0]x1 = b(x1)
    
                  [1 2]     [4]    [1 2]     [4]              
    a(a(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(c(c(x1)))
    
               [1 2]     [2]    [1 2]     [2]                    
    c(c(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(c(b(a(x1)))))
    
                  [1 2]     [4]    [1 2]     [4]              
    a(c(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(c(c(x1)))
    
                  [1 2]     [4]    [1 2]     [4]              
    c(a(c(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = c(a(a(x1)))
   problem:
    a(a(x1)) -> a(b(a(b(c(x1)))))
    a(a(a(x1))) -> a(c(c(x1)))
    c(c(x1)) -> a(b(c(b(a(x1)))))
    a(c(a(x1))) -> a(c(c(x1)))
    c(a(c(x1))) -> c(a(a(x1)))
   String Reversal Processor:
    a(a(x1)) -> c(b(a(b(a(x1)))))
    a(a(a(x1))) -> c(c(a(x1)))
    c(c(x1)) -> a(b(c(b(a(x1)))))
    a(c(a(x1))) -> c(c(a(x1)))
    c(a(c(x1))) -> a(a(c(x1)))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                [1 0 1]     [0]
      [c](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [1],
      
                [1 0 0]  
      [b](x0) = [0 0 0]x0
                [0 0 0]  ,
      
                [1 0 1]     [0]
      [a](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [1]
     orientation:
                 [1 0 1]     [1]    [1 0 1]     [0]                    
      a(a(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(b(a(b(a(x1)))))
                 [0 0 0]     [1]    [0 0 0]     [1]                    
      
                    [1 0 1]     [2]    [1 0 1]     [2]              
      a(a(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(c(a(x1)))
                    [0 0 0]     [1]    [0 0 0]     [1]              
      
                 [1 0 1]     [1]    [1 0 1]     [0]                    
      c(c(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(b(c(b(a(x1)))))
                 [0 0 0]     [1]    [0 0 0]     [1]                    
      
                    [1 0 1]     [2]    [1 0 1]     [2]              
      a(c(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(c(a(x1)))
                    [0 0 0]     [1]    [0 0 0]     [1]              
      
                    [1 0 1]     [2]    [1 0 1]     [2]              
      c(a(c(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(a(c(x1)))
                    [0 0 0]     [1]    [0 0 0]     [1]              
     problem:
      a(a(a(x1))) -> c(c(a(x1)))
      a(c(a(x1))) -> c(c(a(x1)))
      c(a(c(x1))) -> a(a(c(x1)))
     DP Processor:
      DPs:
       a#(a(a(x1))) -> c#(a(x1))
       a#(a(a(x1))) -> c#(c(a(x1)))
       a#(c(a(x1))) -> c#(c(a(x1)))
       c#(a(c(x1))) -> a#(a(c(x1)))
      TRS:
       a(a(a(x1))) -> c(c(a(x1)))
       a(c(a(x1))) -> c(c(a(x1)))
       c(a(c(x1))) -> a(a(c(x1)))
      TDG Processor:
       DPs:
        a#(a(a(x1))) -> c#(a(x1))
        a#(a(a(x1))) -> c#(c(a(x1)))
        a#(c(a(x1))) -> c#(c(a(x1)))
        c#(a(c(x1))) -> a#(a(c(x1)))
       TRS:
        a(a(a(x1))) -> c(c(a(x1)))
        a(c(a(x1))) -> c(c(a(x1)))
        c(a(c(x1))) -> a(a(c(x1)))
       graph:
        c#(a(c(x1))) -> a#(a(c(x1))) -> a#(c(a(x1))) -> c#(c(a(x1)))
        c#(a(c(x1))) -> a#(a(c(x1))) -> a#(a(a(x1))) -> c#(c(a(x1)))
        c#(a(c(x1))) -> a#(a(c(x1))) -> a#(a(a(x1))) -> c#(a(x1))
        a#(c(a(x1))) -> c#(c(a(x1))) -> c#(a(c(x1))) -> a#(a(c(x1)))
        a#(a(a(x1))) -> c#(c(a(x1))) -> c#(a(c(x1))) -> a#(a(c(x1)))
        a#(a(a(x1))) -> c#(a(x1)) -> c#(a(c(x1))) -> a#(a(c(x1)))
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [c#](x0) = 1x0,
         
         [a#](x0) = 1x0,
         
         [c](x0) = 1x0,
         
         [a](x0) = 1x0
        orientation:
         a#(a(a(x1))) = 3x1 >= 2x1 = c#(a(x1))
         
         a#(a(a(x1))) = 3x1 >= 3x1 = c#(c(a(x1)))
         
         a#(c(a(x1))) = 3x1 >= 3x1 = c#(c(a(x1)))
         
         c#(a(c(x1))) = 3x1 >= 3x1 = a#(a(c(x1)))
         
         a(a(a(x1))) = 3x1 >= 3x1 = c(c(a(x1)))
         
         a(c(a(x1))) = 3x1 >= 3x1 = c(c(a(x1)))
         
         c(a(c(x1))) = 3x1 >= 3x1 = a(a(c(x1)))
        problem:
         DPs:
          a#(a(a(x1))) -> c#(c(a(x1)))
          a#(c(a(x1))) -> c#(c(a(x1)))
          c#(a(c(x1))) -> a#(a(c(x1)))
         TRS:
          a(a(a(x1))) -> c(c(a(x1)))
          a(c(a(x1))) -> c(c(a(x1)))
          c(a(c(x1))) -> a(a(c(x1)))
        EDG Processor:
         DPs:
          a#(a(a(x1))) -> c#(c(a(x1)))
          a#(c(a(x1))) -> c#(c(a(x1)))
          c#(a(c(x1))) -> a#(a(c(x1)))
         TRS:
          a(a(a(x1))) -> c(c(a(x1)))
          a(c(a(x1))) -> c(c(a(x1)))
          c(a(c(x1))) -> a(a(c(x1)))
         graph:
          c#(a(c(x1))) -> a#(a(c(x1))) -> a#(a(a(x1))) -> c#(c(a(x1)))
          c#(a(c(x1))) -> a#(a(c(x1))) -> a#(c(a(x1))) -> c#(c(a(x1)))
          a#(c(a(x1))) -> c#(c(a(x1))) -> c#(a(c(x1))) -> a#(a(c(x1)))
          a#(a(a(x1))) -> c#(c(a(x1))) -> c#(a(c(x1))) -> a#(a(c(x1)))
         Arctic Interpretation Processor:
          dimension: 2
          interpretation:
           [c#](x0) = [-4 0 ]x0 + [0],
           
           [a#](x0) = [-1 -&]x0 + [0],
           
                     [0  1 ]     [0]
           [c](x0) = [-& 0 ]x0 + [0],
           
                     [-& 1 ]     [0]
           [a](x0) = [0  0 ]x0 + [1]
          orientation:
           a#(a(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = c#(c(a(x1)))
           
           a#(c(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = c#(c(a(x1)))
           
           c#(a(c(x1))) = [0 1]x1 + [1] >= [-& 0 ]x1 + [0] = a#(a(c(x1)))
           
                         [1 2]     [2]    [1 1]     [2]              
           a(a(a(x1))) = [1 1]x1 + [2] >= [0 0]x1 + [1] = c(c(a(x1)))
           
                         [1 1]     [2]    [1 1]     [2]              
           a(c(a(x1))) = [1 1]x1 + [2] >= [0 0]x1 + [1] = c(c(a(x1)))
           
                         [1 2]     [2]    [1 2]     [2]              
           c(a(c(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(a(c(x1)))
          problem:
           DPs:
            a#(a(a(x1))) -> c#(c(a(x1)))
            a#(c(a(x1))) -> c#(c(a(x1)))
           TRS:
            a(a(a(x1))) -> c(c(a(x1)))
            a(c(a(x1))) -> c(c(a(x1)))
            c(a(c(x1))) -> a(a(c(x1)))
          EDG Processor:
           DPs:
            a#(a(a(x1))) -> c#(c(a(x1)))
            a#(c(a(x1))) -> c#(c(a(x1)))
           TRS:
            a(a(a(x1))) -> c(c(a(x1)))
            a(c(a(x1))) -> c(c(a(x1)))
            c(a(c(x1))) -> a(a(c(x1)))
           graph:
            
           Qed