YES(?,O(n^3))

Problem:
 a(b(c(x1))) -> c(b(a(x1)))
 C(B(A(x1))) -> A(B(C(x1)))
 b(a(C(x1))) -> C(a(b(x1)))
 c(A(B(x1))) -> B(A(c(x1)))
 A(c(b(x1))) -> b(c(A(x1)))
 B(C(a(x1))) -> a(C(B(x1)))
 a(A(x1)) -> x1
 A(a(x1)) -> x1
 b(B(x1)) -> x1
 B(b(x1)) -> x1
 c(C(x1)) -> x1
 C(c(x1)) -> x1

Proof:
 RT Transformation Processor:
  strict:
   a(b(c(x1))) -> c(b(a(x1)))
   C(B(A(x1))) -> A(B(C(x1)))
   b(a(C(x1))) -> C(a(b(x1)))
   c(A(B(x1))) -> B(A(c(x1)))
   A(c(b(x1))) -> b(c(A(x1)))
   B(C(a(x1))) -> a(C(B(x1)))
   a(A(x1)) -> x1
   A(a(x1)) -> x1
   b(B(x1)) -> x1
   B(b(x1)) -> x1
   c(C(x1)) -> x1
   C(c(x1)) -> x1
  weak:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {7}
    transitions:
     a0(7) -> 7*
     b0(7) -> 7*
     c0(7) -> 7*
     C0(7) -> 7*
     B0(7) -> 7*
     A0(7) -> 7*
   problem:
    strict:
     a(b(c(x1))) -> c(b(a(x1)))
     C(B(A(x1))) -> A(B(C(x1)))
     b(a(C(x1))) -> C(a(b(x1)))
     c(A(B(x1))) -> B(A(c(x1)))
     A(c(b(x1))) -> b(c(A(x1)))
     B(C(a(x1))) -> a(C(B(x1)))
     a(A(x1)) -> x1
     A(a(x1)) -> x1
     b(B(x1)) -> x1
     B(b(x1)) -> x1
     c(C(x1)) -> x1
    weak:
     C(c(x1)) -> x1
   Bounds Processor:
    bound: 0
    enrichment: match-rt
    automaton:
     final states: {7}
     transitions:
      a0(7) -> 7*
      b0(7) -> 7*
      c0(7) -> 7*
      C0(7) -> 7*
      B0(7) -> 7*
      A0(7) -> 7*
    problem:
     strict:
      a(b(c(x1))) -> c(b(a(x1)))
      C(B(A(x1))) -> A(B(C(x1)))
      b(a(C(x1))) -> C(a(b(x1)))
      c(A(B(x1))) -> B(A(c(x1)))
      A(c(b(x1))) -> b(c(A(x1)))
      B(C(a(x1))) -> a(C(B(x1)))
      a(A(x1)) -> x1
      A(a(x1)) -> x1
      b(B(x1)) -> x1
      B(b(x1)) -> x1
     weak:
      c(C(x1)) -> x1
      C(c(x1)) -> x1
    Bounds Processor:
     bound: 0
     enrichment: match-rt
     automaton:
      final states: {7}
      transitions:
       a0(7) -> 7*
       b0(7) -> 7*
       c0(7) -> 7*
       C0(7) -> 7*
       B0(7) -> 7*
       A0(7) -> 7*
     problem:
      strict:
       a(b(c(x1))) -> c(b(a(x1)))
       C(B(A(x1))) -> A(B(C(x1)))
       b(a(C(x1))) -> C(a(b(x1)))
       c(A(B(x1))) -> B(A(c(x1)))
       A(c(b(x1))) -> b(c(A(x1)))
       B(C(a(x1))) -> a(C(B(x1)))
       a(A(x1)) -> x1
       A(a(x1)) -> x1
       b(B(x1)) -> x1
      weak:
       B(b(x1)) -> x1
       c(C(x1)) -> x1
       C(c(x1)) -> x1
     Bounds Processor:
      bound: 0
      enrichment: match-rt
      automaton:
       final states: {7}
       transitions:
        a0(7) -> 7*
        b0(7) -> 7*
        c0(7) -> 7*
        C0(7) -> 7*
        B0(7) -> 7*
        A0(7) -> 7*
      problem:
       strict:
        a(b(c(x1))) -> c(b(a(x1)))
        C(B(A(x1))) -> A(B(C(x1)))
        b(a(C(x1))) -> C(a(b(x1)))
        c(A(B(x1))) -> B(A(c(x1)))
        A(c(b(x1))) -> b(c(A(x1)))
        B(C(a(x1))) -> a(C(B(x1)))
        a(A(x1)) -> x1
        A(a(x1)) -> x1
       weak:
        b(B(x1)) -> x1
        B(b(x1)) -> x1
        c(C(x1)) -> x1
        C(c(x1)) -> x1
      Bounds Processor:
       bound: 0
       enrichment: match-rt
       automaton:
        final states: {7}
        transitions:
         a0(7) -> 7*
         b0(7) -> 7*
         c0(7) -> 7*
         C0(7) -> 7*
         B0(7) -> 7*
         A0(7) -> 7*
       problem:
        strict:
         a(b(c(x1))) -> c(b(a(x1)))
         C(B(A(x1))) -> A(B(C(x1)))
         b(a(C(x1))) -> C(a(b(x1)))
         c(A(B(x1))) -> B(A(c(x1)))
         A(c(b(x1))) -> b(c(A(x1)))
         B(C(a(x1))) -> a(C(B(x1)))
         a(A(x1)) -> x1
        weak:
         A(a(x1)) -> x1
         b(B(x1)) -> x1
         B(b(x1)) -> x1
         c(C(x1)) -> x1
         C(c(x1)) -> x1
       Bounds Processor:
        bound: 0
        enrichment: match-rt
        automaton:
         final states: {7}
         transitions:
          a0(7) -> 7*
          b0(7) -> 7*
          c0(7) -> 7*
          C0(7) -> 7*
          B0(7) -> 7*
          A0(7) -> 7*
        problem:
         strict:
          a(b(c(x1))) -> c(b(a(x1)))
          C(B(A(x1))) -> A(B(C(x1)))
          b(a(C(x1))) -> C(a(b(x1)))
          c(A(B(x1))) -> B(A(c(x1)))
          A(c(b(x1))) -> b(c(A(x1)))
          B(C(a(x1))) -> a(C(B(x1)))
         weak:
          a(A(x1)) -> x1
          A(a(x1)) -> x1
          b(B(x1)) -> x1
          B(b(x1)) -> x1
          c(C(x1)) -> x1
          C(c(x1)) -> x1
        Matrix Interpretation Processor:
         dimension: 2
         interpretation:
                      
          [C](x0) = x0,
          
                         [0]
          [B](x0) = x0 + [8],
          
                      
          [A](x0) = x0,
          
                      
          [a](x0) = x0,
          
                      
          [b](x0) = x0,
          
                    [1 2]  
          [c](x0) = [0 1]x0
         orientation:
                        [1 2]      [1 2]                
          a(b(c(x1))) = [0 1]x1 >= [0 1]x1 = c(b(a(x1)))
          
                             [0]         [0]              
          C(B(A(x1))) = x1 + [8] >= x1 + [8] = A(B(C(x1)))
          
                                              
          b(a(C(x1))) = x1 >= x1 = C(a(b(x1)))
          
                        [1 2]     [16]    [1 2]     [0]              
          c(A(B(x1))) = [0 1]x1 + [8 ] >= [0 1]x1 + [8] = B(A(c(x1)))
          
                        [1 2]      [1 2]                
          A(c(b(x1))) = [0 1]x1 >= [0 1]x1 = b(c(A(x1)))
          
                             [0]         [0]              
          B(C(a(x1))) = x1 + [8] >= x1 + [8] = a(C(B(x1)))
          
                                  
          a(A(x1)) = x1 >= x1 = x1
          
                                  
          A(a(x1)) = x1 >= x1 = x1
          
                          [0]           
          b(B(x1)) = x1 + [8] >= x1 = x1
          
                          [0]           
          B(b(x1)) = x1 + [8] >= x1 = x1
          
                     [1 2]             
          c(C(x1)) = [0 1]x1 >= x1 = x1
          
                     [1 2]             
          C(c(x1)) = [0 1]x1 >= x1 = x1
         problem:
          strict:
           a(b(c(x1))) -> c(b(a(x1)))
           C(B(A(x1))) -> A(B(C(x1)))
           b(a(C(x1))) -> C(a(b(x1)))
           A(c(b(x1))) -> b(c(A(x1)))
           B(C(a(x1))) -> a(C(B(x1)))
          weak:
           c(A(B(x1))) -> B(A(c(x1)))
           a(A(x1)) -> x1
           A(a(x1)) -> x1
           b(B(x1)) -> x1
           B(b(x1)) -> x1
           c(C(x1)) -> x1
           C(c(x1)) -> x1
         Matrix Interpretation Processor:
          dimension: 2
          interpretation:
                          [0]
           [C](x0) = x0 + [1],
           
                          [0]
           [B](x0) = x0 + [1],
           
                          [8]
           [A](x0) = x0 + [0],
           
                       
           [a](x0) = x0,
           
                     [1 1]     [8]
           [b](x0) = [0 1]x0 + [1],
           
                     [1 8]     [0]
           [c](x0) = [0 1]x0 + [8]
          orientation:
                         [1 9]     [16]    [1 9]     [16]              
           a(b(c(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = c(b(a(x1)))
           
                              [8]         [8]              
           C(B(A(x1))) = x1 + [2] >= x1 + [2] = A(B(C(x1)))
           
                         [1 1]     [9]    [1 1]     [8]              
           b(a(C(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = C(a(b(x1)))
           
                         [1 9]     [24]    [1 9]     [24]              
           A(c(b(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = b(c(A(x1)))
           
                              [0]         [0]              
           B(C(a(x1))) = x1 + [2] >= x1 + [2] = a(C(B(x1)))
           
                         [1 8]     [16]    [1 8]     [8]              
           c(A(B(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9] = B(A(c(x1)))
           
                           [8]           
           a(A(x1)) = x1 + [0] >= x1 = x1
           
                           [8]           
           A(a(x1)) = x1 + [0] >= x1 = x1
           
                      [1 1]     [9]           
           b(B(x1)) = [0 1]x1 + [2] >= x1 = x1
           
                      [1 1]     [8]           
           B(b(x1)) = [0 1]x1 + [2] >= x1 = x1
           
                      [1 8]     [8]           
           c(C(x1)) = [0 1]x1 + [9] >= x1 = x1
           
                      [1 8]     [0]           
           C(c(x1)) = [0 1]x1 + [9] >= x1 = x1
          problem:
           strict:
            a(b(c(x1))) -> c(b(a(x1)))
            C(B(A(x1))) -> A(B(C(x1)))
            A(c(b(x1))) -> b(c(A(x1)))
            B(C(a(x1))) -> a(C(B(x1)))
           weak:
            b(a(C(x1))) -> C(a(b(x1)))
            c(A(B(x1))) -> B(A(c(x1)))
            a(A(x1)) -> x1
            A(a(x1)) -> x1
            b(B(x1)) -> x1
            B(b(x1)) -> x1
            c(C(x1)) -> x1
            C(c(x1)) -> x1
          Matrix Interpretation Processor:
           dimension: 2
           interpretation:
                        
            [C](x0) = x0,
            
                        
            [B](x0) = x0,
            
                      [1 4]     [8]
            [A](x0) = [0 1]x0 + [2],
            
                        
            [a](x0) = x0,
            
                      [1 4]     [0]
            [b](x0) = [0 1]x0 + [4],
            
                        
            [c](x0) = x0
           orientation:
                          [1 4]     [0]    [1 4]     [0]              
            a(b(c(x1))) = [0 1]x1 + [4] >= [0 1]x1 + [4] = c(b(a(x1)))
            
                          [1 4]     [8]    [1 4]     [8]              
            C(B(A(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = A(B(C(x1)))
            
                          [1 8]     [24]    [1 8]     [16]              
            A(c(b(x1))) = [0 1]x1 + [6 ] >= [0 1]x1 + [6 ] = b(c(A(x1)))
            
                                                
            B(C(a(x1))) = x1 >= x1 = a(C(B(x1)))
            
                          [1 4]     [0]    [1 4]     [0]              
            b(a(C(x1))) = [0 1]x1 + [4] >= [0 1]x1 + [4] = C(a(b(x1)))
            
                          [1 4]     [8]    [1 4]     [8]              
            c(A(B(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = B(A(c(x1)))
            
                       [1 4]     [8]           
            a(A(x1)) = [0 1]x1 + [2] >= x1 = x1
            
                       [1 4]     [8]           
            A(a(x1)) = [0 1]x1 + [2] >= x1 = x1
            
                       [1 4]     [0]           
            b(B(x1)) = [0 1]x1 + [4] >= x1 = x1
            
                       [1 4]     [0]           
            B(b(x1)) = [0 1]x1 + [4] >= x1 = x1
            
                                    
            c(C(x1)) = x1 >= x1 = x1
            
                                    
            C(c(x1)) = x1 >= x1 = x1
           problem:
            strict:
             a(b(c(x1))) -> c(b(a(x1)))
             C(B(A(x1))) -> A(B(C(x1)))
             B(C(a(x1))) -> a(C(B(x1)))
            weak:
             A(c(b(x1))) -> b(c(A(x1)))
             b(a(C(x1))) -> C(a(b(x1)))
             c(A(B(x1))) -> B(A(c(x1)))
             a(A(x1)) -> x1
             A(a(x1)) -> x1
             b(B(x1)) -> x1
             B(b(x1)) -> x1
             c(C(x1)) -> x1
             C(c(x1)) -> x1
           Matrix Interpretation Processor:
            dimension: 2
            interpretation:
                         
             [C](x0) = x0,
             
                         
             [B](x0) = x0,
             
                         
             [A](x0) = x0,
             
                       [1 1]  
             [a](x0) = [0 1]x0,
             
                         
             [b](x0) = x0,
             
                            [4]
             [c](x0) = x0 + [1]
            orientation:
                           [1 1]     [5]    [1 1]     [4]              
             a(b(c(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = c(b(a(x1)))
             
                                                 
             C(B(A(x1))) = x1 >= x1 = A(B(C(x1)))
             
                           [1 1]      [1 1]                
             B(C(a(x1))) = [0 1]x1 >= [0 1]x1 = a(C(B(x1)))
             
                                [4]         [4]              
             A(c(b(x1))) = x1 + [1] >= x1 + [1] = b(c(A(x1)))
             
                           [1 1]      [1 1]                
             b(a(C(x1))) = [0 1]x1 >= [0 1]x1 = C(a(b(x1)))
             
                                [4]         [4]              
             c(A(B(x1))) = x1 + [1] >= x1 + [1] = B(A(c(x1)))
             
                        [1 1]             
             a(A(x1)) = [0 1]x1 >= x1 = x1
             
                        [1 1]             
             A(a(x1)) = [0 1]x1 >= x1 = x1
             
                                     
             b(B(x1)) = x1 >= x1 = x1
             
                                     
             B(b(x1)) = x1 >= x1 = x1
             
                             [4]           
             c(C(x1)) = x1 + [1] >= x1 = x1
             
                             [4]           
             C(c(x1)) = x1 + [1] >= x1 = x1
            problem:
             strict:
              C(B(A(x1))) -> A(B(C(x1)))
              B(C(a(x1))) -> a(C(B(x1)))
             weak:
              a(b(c(x1))) -> c(b(a(x1)))
              A(c(b(x1))) -> b(c(A(x1)))
              b(a(C(x1))) -> C(a(b(x1)))
              c(A(B(x1))) -> B(A(c(x1)))
              a(A(x1)) -> x1
              A(a(x1)) -> x1
              b(B(x1)) -> x1
              B(b(x1)) -> x1
              c(C(x1)) -> x1
              C(c(x1)) -> x1
            Matrix Interpretation Processor:
             dimension: 2
             interpretation:
                          
              [C](x0) = x0,
              
                        [1 5]     [0]
              [B](x0) = [0 1]x0 + [1],
              
                          
              [A](x0) = x0,
              
                        [1 8]     [0]
              [a](x0) = [0 1]x0 + [2],
              
                        [1 8]     [0]
              [b](x0) = [0 1]x0 + [2],
              
                          
              [c](x0) = x0
             orientation:
                            [1 5]     [0]    [1 5]     [0]              
              C(B(A(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = A(B(C(x1)))
              
                            [1  13]     [10]    [1  13]     [8]              
              B(C(a(x1))) = [0  1 ]x1 + [3 ] >= [0  1 ]x1 + [3] = a(C(B(x1)))
              
                            [1  16]     [16]    [1  16]     [16]              
              a(b(c(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = c(b(a(x1)))
              
                            [1 8]     [0]    [1 8]     [0]              
              A(c(b(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = b(c(A(x1)))
              
                            [1  16]     [16]    [1  16]     [16]              
              b(a(C(x1))) = [0  1 ]x1 + [4 ] >= [0  1 ]x1 + [4 ] = C(a(b(x1)))
              
                            [1 5]     [0]    [1 5]     [0]              
              c(A(B(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = B(A(c(x1)))
              
                         [1 8]     [0]           
              a(A(x1)) = [0 1]x1 + [2] >= x1 = x1
              
                         [1 8]     [0]           
              A(a(x1)) = [0 1]x1 + [2] >= x1 = x1
              
                         [1  13]     [8]           
              b(B(x1)) = [0  1 ]x1 + [3] >= x1 = x1
              
                         [1  13]     [10]           
              B(b(x1)) = [0  1 ]x1 + [3 ] >= x1 = x1
              
                                      
              c(C(x1)) = x1 >= x1 = x1
              
                                      
              C(c(x1)) = x1 >= x1 = x1
             problem:
              strict:
               C(B(A(x1))) -> A(B(C(x1)))
              weak:
               B(C(a(x1))) -> a(C(B(x1)))
               a(b(c(x1))) -> c(b(a(x1)))
               A(c(b(x1))) -> b(c(A(x1)))
               b(a(C(x1))) -> C(a(b(x1)))
               c(A(B(x1))) -> B(A(c(x1)))
               a(A(x1)) -> x1
               A(a(x1)) -> x1
               b(B(x1)) -> x1
               B(b(x1)) -> x1
               c(C(x1)) -> x1
               C(c(x1)) -> x1
             Matrix Interpretation Processor:
              dimension: 3
              interpretation:
                         [1 0 1]     [1]
               [C](x0) = [0 1 0]x0 + [0]
                         [0 0 1]     [2],
               
                              [2]
               [B](x0) = x0 + [0]
                              [0],
               
                              [0]
               [A](x0) = x0 + [0]
                              [2],
               
                              [4]
               [a](x0) = x0 + [0]
                              [0],
               
                              [3]
               [b](x0) = x0 + [0]
                              [0],
               
                           
               [c](x0) = x0
                           
              orientation:
                             [1 0 1]     [5]    [1 0 1]     [3]              
               C(B(A(x1))) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = A(B(C(x1)))
                             [0 0 1]     [4]    [0 0 1]     [4]              
               
                             [1 0 1]     [7]    [1 0 1]     [7]              
               B(C(a(x1))) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = a(C(B(x1)))
                             [0 0 1]     [2]    [0 0 1]     [2]              
               
                                  [7]         [7]              
               a(b(c(x1))) = x1 + [0] >= x1 + [0] = c(b(a(x1)))
                                  [0]         [0]              
               
                                  [3]         [3]              
               A(c(b(x1))) = x1 + [0] >= x1 + [0] = b(c(A(x1)))
                                  [2]         [2]              
               
                             [1 0 1]     [8]    [1 0 1]     [8]              
               b(a(C(x1))) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = C(a(b(x1)))
                             [0 0 1]     [2]    [0 0 1]     [2]              
               
                                  [2]         [2]              
               c(A(B(x1))) = x1 + [0] >= x1 + [0] = B(A(c(x1)))
                                  [2]         [2]              
               
                               [4]           
               a(A(x1)) = x1 + [0] >= x1 = x1
                               [2]           
               
                               [4]           
               A(a(x1)) = x1 + [0] >= x1 = x1
                               [2]           
               
                               [5]           
               b(B(x1)) = x1 + [0] >= x1 = x1
                               [0]           
               
                               [5]           
               B(b(x1)) = x1 + [0] >= x1 = x1
                               [0]           
               
                          [1 0 1]     [1]           
               c(C(x1)) = [0 1 0]x1 + [0] >= x1 = x1
                          [0 0 1]     [2]           
               
                          [1 0 1]     [1]           
               C(c(x1)) = [0 1 0]x1 + [0] >= x1 = x1
                          [0 0 1]     [2]           
              problem:
               strict:
                
               weak:
                C(B(A(x1))) -> A(B(C(x1)))
                B(C(a(x1))) -> a(C(B(x1)))
                a(b(c(x1))) -> c(b(a(x1)))
                A(c(b(x1))) -> b(c(A(x1)))
                b(a(C(x1))) -> C(a(b(x1)))
                c(A(B(x1))) -> B(A(c(x1)))
                a(A(x1)) -> x1
                A(a(x1)) -> x1
                b(B(x1)) -> x1
                B(b(x1)) -> x1
                c(C(x1)) -> x1
                C(c(x1)) -> x1
              Qed