YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0  -&]  
   [a](x0) = [0  -&]x0,
   
             [3 3]  
   [b](x0) = [3 0]x0,
   
             [0 0]  
   [c](x0) = [3 0]x0
  orientation:
                    [6 3]      [6  -&]                   
   a(a(b(c(x1)))) = [6 3]x1 >= [6  -&]x1 = b(b(a(a(x1))))
   
           [3 3]      [3  -&]                   
   b(x1) = [3 0]x1 >= [3  -&]x1 = c(c(a(a(x1))))
   
              [6 3]      [0  -&]          
   b(c(x1)) = [3 3]x1 >= [0  -&]x1 = a(x1)
   
                 [0 0]             
   a(a(c(x1))) = [0 0]x1 >= x1 = x1
  problem:
   a(a(b(c(x1)))) -> b(b(a(a(x1))))
   b(x1) -> c(c(a(a(x1))))
   a(a(c(x1))) -> x1
  DP Processor:
   DPs:
    a#(a(b(c(x1)))) -> a#(x1)
    a#(a(b(c(x1)))) -> a#(a(x1))
    a#(a(b(c(x1)))) -> b#(a(a(x1)))
    a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
    b#(x1) -> a#(x1)
    b#(x1) -> a#(a(x1))
   TRS:
    a(a(b(c(x1)))) -> b(b(a(a(x1))))
    b(x1) -> c(c(a(a(x1))))
    a(a(c(x1))) -> x1
   TDG Processor:
    DPs:
     a#(a(b(c(x1)))) -> a#(x1)
     a#(a(b(c(x1)))) -> a#(a(x1))
     a#(a(b(c(x1)))) -> b#(a(a(x1)))
     a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
     b#(x1) -> a#(x1)
     b#(x1) -> a#(a(x1))
    TRS:
     a(a(b(c(x1)))) -> b(b(a(a(x1))))
     b(x1) -> c(c(a(a(x1))))
     a(a(c(x1))) -> x1
    graph:
     b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
     b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(a(a(x1)))
     b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> a#(a(x1))
     b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> a#(x1)
     b#(x1) -> a#(x1) -> a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
     b#(x1) -> a#(x1) -> a#(a(b(c(x1)))) -> b#(a(a(x1)))
     b#(x1) -> a#(x1) -> a#(a(b(c(x1)))) -> a#(a(x1))
     b#(x1) -> a#(x1) -> a#(a(b(c(x1)))) -> a#(x1)
     a#(a(b(c(x1)))) -> b#(a(a(x1))) -> b#(x1) -> a#(a(x1))
     a#(a(b(c(x1)))) -> b#(a(a(x1))) -> b#(x1) -> a#(x1)
     a#(a(b(c(x1)))) -> b#(b(a(a(x1)))) -> b#(x1) -> a#(a(x1))
     a#(a(b(c(x1)))) -> b#(b(a(a(x1)))) -> b#(x1) -> a#(x1)
     a#(a(b(c(x1)))) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
     a#(a(b(c(x1)))) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(a(a(x1)))
     a#(a(b(c(x1)))) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> a#(a(x1))
     a#(a(b(c(x1)))) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> a#(x1)
     a#(a(b(c(x1)))) -> a#(x1) -> a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
     a#(a(b(c(x1)))) -> a#(x1) -> a#(a(b(c(x1)))) -> b#(a(a(x1)))
     a#(a(b(c(x1)))) -> a#(x1) -> a#(a(b(c(x1)))) -> a#(a(x1))
     a#(a(b(c(x1)))) -> a#(x1) -> a#(a(b(c(x1)))) -> a#(x1)
    Arctic Interpretation Processor:
     dimension: 2
     usable rules:
      a(a(b(c(x1)))) -> b(b(a(a(x1))))
      b(x1) -> c(c(a(a(x1))))
      a(a(c(x1))) -> x1
     interpretation:
      [b#](x0) = [1 2]x0 + [1],
      
      [a#](x0) = [0 1]x0 + [0],
      
                [-& 0 ]     [1]
      [a](x0) = [0  0 ]x0 + [0],
      
                [0 1]     [3]
      [b](x0) = [0 0]x0 + [1],
      
                [-& 0 ]     [0]
      [c](x0) = [0  0 ]x0 + [0]
     orientation:
      a#(a(b(c(x1)))) = [2 2]x1 + [4] >= [0 1]x1 + [0] = a#(x1)
      
      a#(a(b(c(x1)))) = [2 2]x1 + [4] >= [1 1]x1 + [1] = a#(a(x1))
      
      a#(a(b(c(x1)))) = [2 2]x1 + [4] >= [2 2]x1 + [3] = b#(a(a(x1)))
      
      a#(a(b(c(x1)))) = [2 2]x1 + [4] >= [2 2]x1 + [4] = b#(b(a(a(x1))))
      
      b#(x1) = [1 2]x1 + [1] >= [0 1]x1 + [0] = a#(x1)
      
      b#(x1) = [1 2]x1 + [1] >= [1 1]x1 + [1] = a#(a(x1))
      
                       [1 1]     [3]    [1 1]     [3]                 
      a(a(b(c(x1)))) = [1 1]x1 + [3] >= [1 1]x1 + [3] = b(b(a(a(x1))))
      
              [0 1]     [3]    [0 0]     [1]                 
      b(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = c(c(a(a(x1))))
      
                    [0 0]     [1]           
      a(a(c(x1))) = [0 0]x1 + [1] >= x1 = x1
     problem:
      DPs:
       a#(a(b(c(x1)))) -> b#(a(a(x1)))
       a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
       b#(x1) -> a#(a(x1))
      TRS:
       a(a(b(c(x1)))) -> b(b(a(a(x1))))
       b(x1) -> c(c(a(a(x1))))
       a(a(c(x1))) -> x1
     Restore Modifier:
      DPs:
       a#(a(b(c(x1)))) -> b#(a(a(x1)))
       a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
       b#(x1) -> a#(a(x1))
      TRS:
       a(a(b(c(x1)))) -> b(b(a(a(x1))))
       b(x1) -> c(c(a(a(x1))))
       a(a(c(x1))) -> x1
      EDG Processor:
       DPs:
        a#(a(b(c(x1)))) -> b#(a(a(x1)))
        a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
        b#(x1) -> a#(a(x1))
       TRS:
        a(a(b(c(x1)))) -> b(b(a(a(x1))))
        b(x1) -> c(c(a(a(x1))))
        a(a(c(x1))) -> x1
       graph:
        b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(a(a(x1)))
        b#(x1) -> a#(a(x1)) -> a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
        a#(a(b(c(x1)))) -> b#(a(a(x1))) -> b#(x1) -> a#(a(x1))
        a#(a(b(c(x1)))) -> b#(b(a(a(x1)))) -> b#(x1) -> a#(a(x1))
       Arctic Interpretation Processor:
        dimension: 2
        usable rules:
         a(a(b(c(x1)))) -> b(b(a(a(x1))))
         b(x1) -> c(c(a(a(x1))))
         a(a(c(x1))) -> x1
        interpretation:
         [b#](x0) = [0 0]x0 + [0],
         
         [a#](x0) = [-& 0 ]x0 + [0],
         
                   [-& 0 ]     [1]
         [a](x0) = [0  0 ]x0 + [0],
         
                   [0 0]     [1]
         [b](x0) = [1 0]x0 + [2],
         
                   [0 0]     [-&]
         [c](x0) = [0 0]x0 + [1 ]
        orientation:
         a#(a(b(c(x1)))) = [1 1]x1 + [2] >= [0 0]x1 + [1] = b#(a(a(x1)))
         
         a#(a(b(c(x1)))) = [1 1]x1 + [2] >= [1 1]x1 + [2] = b#(b(a(a(x1))))
         
         b#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = a#(a(x1))
         
                          [1 1]     [2]    [1 1]     [2]                 
         a(a(b(c(x1)))) = [1 1]x1 + [2] >= [1 1]x1 + [2] = b(b(a(a(x1))))
         
                 [0 0]     [1]    [0 0]     [1]                 
         b(x1) = [1 0]x1 + [2] >= [0 0]x1 + [1] = c(c(a(a(x1))))
         
                       [0 0]     [1]           
         a(a(c(x1))) = [0 0]x1 + [1] >= x1 = x1
        problem:
         DPs:
          a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
          b#(x1) -> a#(a(x1))
         TRS:
          a(a(b(c(x1)))) -> b(b(a(a(x1))))
          b(x1) -> c(c(a(a(x1))))
          a(a(c(x1))) -> x1
        Restore Modifier:
         DPs:
          a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
          b#(x1) -> a#(a(x1))
         TRS:
          a(a(b(c(x1)))) -> b(b(a(a(x1))))
          b(x1) -> c(c(a(a(x1))))
          a(a(c(x1))) -> x1
         EDG Processor:
          DPs:
           a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
           b#(x1) -> a#(a(x1))
          TRS:
           a(a(b(c(x1)))) -> b(b(a(a(x1))))
           b(x1) -> c(c(a(a(x1))))
           a(a(c(x1))) -> x1
          graph:
           b#(x1) -> a#(a(x1)) ->
           a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
           a#(a(b(c(x1)))) -> b#(b(a(a(x1)))) -> b#(x1) -> a#(a(x1))
          Arctic Interpretation Processor:
           dimension: 2
           usable rules:
            a(a(b(c(x1)))) -> b(b(a(a(x1))))
            b(x1) -> c(c(a(a(x1))))
            a(a(c(x1))) -> x1
           interpretation:
            [b#](x0) = [-& 1 ]x0 + [3],
            
            [a#](x0) = [-& 0 ]x0 + [2],
            
                      [-& 0 ]     [0]
            [a](x0) = [-& 0 ]x0 + [0],
            
                      [-& 1 ]     [2]
            [b](x0) = [3  1 ]x0 + [2],
            
                      [0 1]     [2]
            [c](x0) = [0 0]x0 + [1]
           orientation:
            a#(a(b(c(x1)))) = [3 4]x1 + [5] >= [-& 4 ]x1 + [4] = b#(b(a(a(x1))))
            
            b#(x1) = [-& 1 ]x1 + [3] >= [-& 0 ]x1 + [2] = a#(a(x1))
            
                             [3 4]     [5]    [-& 4 ]     [4]                 
            a(a(b(c(x1)))) = [3 4]x1 + [5] >= [-& 4 ]x1 + [5] = b(b(a(a(x1))))
            
                    [-& 1 ]     [2]    [-& 1 ]     [2]                 
            b(x1) = [3  1 ]x1 + [2] >= [-& 1 ]x1 + [2] = c(c(a(a(x1))))
            
                          [0 0]     [1]           
            a(a(c(x1))) = [0 0]x1 + [1] >= x1 = x1
           problem:
            DPs:
             a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
            TRS:
             a(a(b(c(x1)))) -> b(b(a(a(x1))))
             b(x1) -> c(c(a(a(x1))))
             a(a(c(x1))) -> x1
           Restore Modifier:
            DPs:
             a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
            TRS:
             a(a(b(c(x1)))) -> b(b(a(a(x1))))
             b(x1) -> c(c(a(a(x1))))
             a(a(c(x1))) -> x1
            EDG Processor:
             DPs:
              a#(a(b(c(x1)))) -> b#(b(a(a(x1))))
             TRS:
              a(a(b(c(x1)))) -> b(b(a(a(x1))))
              b(x1) -> c(c(a(a(x1))))
              a(a(c(x1))) -> x1
             graph:
              
             Qed