YES

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

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