YES(?,O(n^3))

Problem:
 active(f(x)) -> mark(f(f(x)))
 chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
 mat(f(x),f(y())) -> f(mat(x,y()))
 chk(no(c())) -> active(c())
 mat(f(x),c()) -> no(c())
 f(active(x)) -> active(f(x))
 f(no(x)) -> no(f(x))
 f(mark(x)) -> mark(f(x))
 tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))

Proof:
 RT Transformation Processor:
  strict:
   active(f(x)) -> mark(f(f(x)))
   chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
   mat(f(x),f(y())) -> f(mat(x,y()))
   chk(no(c())) -> active(c())
   mat(f(x),c()) -> no(c())
   f(active(x)) -> active(f(x))
   f(no(x)) -> no(f(x))
   f(mark(x)) -> mark(f(x))
   tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [tp](x0) = x0,
    
    [c] = 0,
    
    [y] = 25,
    
    [mat](x0, x1) = x0 + x1 + 19,
    
    [X] = 7,
    
    [chk](x0) = x0 + 13,
    
    [no](x0) = x0 + 1,
    
    [mark](x0) = x0 + 4,
    
    [active](x0) = x0 + 2,
    
    [f](x0) = x0 + 1
   orientation:
    active(f(x)) = x + 3 >= x + 6 = mark(f(f(x)))
    
    chk(no(f(x))) = x + 15 >= x + 50 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
    
    mat(f(x),f(y())) = x + 46 >= x + 45 = f(mat(x,y()))
    
    chk(no(c())) = 14 >= 2 = active(c())
    
    mat(f(x),c()) = x + 20 >= 1 = no(c())
    
    f(active(x)) = x + 3 >= x + 3 = active(f(x))
    
    f(no(x)) = x + 2 >= x + 2 = no(f(x))
    
    f(mark(x)) = x + 5 >= x + 5 = mark(f(x))
    
    tp(mark(x)) = x + 4 >= x + 49 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
   problem:
    strict:
     active(f(x)) -> mark(f(f(x)))
     chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
     f(active(x)) -> active(f(x))
     f(no(x)) -> no(f(x))
     f(mark(x)) -> mark(f(x))
     tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
    weak:
     mat(f(x),f(y())) -> f(mat(x,y()))
     chk(no(c())) -> active(c())
     mat(f(x),c()) -> no(c())
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [tp](x0) = x0 + 1,
     
     [c] = 16,
     
     [y] = 12,
     
     [mat](x0, x1) = x0 + x1 + 4,
     
     [X] = 5,
     
     [chk](x0) = x0 + 16,
     
     [no](x0) = x0 + 1,
     
     [mark](x0) = x0 + 26,
     
     [active](x0) = x0 + 4,
     
     [f](x0) = x0
    orientation:
     active(f(x)) = x + 4 >= x + 26 = mark(f(f(x)))
     
     chk(no(f(x))) = x + 17 >= x + 25 = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
     
     f(active(x)) = x + 4 >= x + 4 = active(f(x))
     
     f(no(x)) = x + 1 >= x + 1 = no(f(x))
     
     f(mark(x)) = x + 26 >= x + 26 = mark(f(x))
     
     tp(mark(x)) = x + 27 >= x + 26 = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
     
     mat(f(x),f(y())) = x + 16 >= x + 16 = f(mat(x,y()))
     
     chk(no(c())) = 33 >= 20 = active(c())
     
     mat(f(x),c()) = x + 20 >= 17 = no(c())
    problem:
     strict:
      active(f(x)) -> mark(f(f(x)))
      chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
      f(active(x)) -> active(f(x))
      f(no(x)) -> no(f(x))
      f(mark(x)) -> mark(f(x))
     weak:
      tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
      mat(f(x),f(y())) -> f(mat(x,y()))
      chk(no(c())) -> active(c())
      mat(f(x),c()) -> no(c())
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                 [1 0]     [1]
      [tp](x0) = [0 0]x0 + [8],
      
            [4]
      [c] = [0],
      
            [2]
      [y] = [9],
      
                      [1 7]     [1 0]     [0]
      [mat](x0, x1) = [0 0]x0 + [0 0]x1 + [9],
      
            [0]
      [X] = [0],
      
                  [1 0]  
      [chk](x0) = [0 0]x0,
      
                 [1 1]     [0]
      [no](x0) = [0 1]x0 + [4],
      
                     
      [mark](x0) = x0,
      
                     [1 2]  
      [active](x0) = [0 1]x0,
      
                [1 2]  
      [f](x0) = [0 1]x0
     orientation:
                     [1 4]     [1 4]                 
      active(f(x)) = [0 1]x >= [0 1]x = mark(f(f(x)))
      
                      [1 3]     [1 0]                                                    
      chk(no(f(x))) = [0 0]x >= [0 0]x = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
      
                     [1 4]     [1 4]                
      f(active(x)) = [0 1]x >= [0 1]x = active(f(x))
      
                 [1 3]    [8]    [1 3]    [0]           
      f(no(x)) = [0 1]x + [4] >= [0 1]x + [4] = no(f(x))
      
                   [1 2]     [1 2]              
      f(mark(x)) = [0 1]x >= [0 1]x = mark(f(x))
      
                    [1 0]    [1]    [1 0]    [1]                                                    
      tp(mark(x)) = [0 0]x + [8] >= [0 0]x + [8] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
      
                         [1 9]    [20]    [1 7]    [20]                
      mat(f(x),f(y())) = [0 0]x + [9 ] >= [0 0]x + [9 ] = f(mat(x,y()))
      
                     [4]    [4]              
      chk(no(c())) = [0] >= [0] = active(c())
      
                      [1 9]    [4]    [4]          
      mat(f(x),c()) = [0 0]x + [9] >= [4] = no(c())
     problem:
      strict:
       active(f(x)) -> mark(f(f(x)))
       chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
       f(active(x)) -> active(f(x))
       f(mark(x)) -> mark(f(x))
      weak:
       f(no(x)) -> no(f(x))
       tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
       mat(f(x),f(y())) -> f(mat(x,y()))
       chk(no(c())) -> active(c())
       mat(f(x),c()) -> no(c())
     Matrix Interpretation Processor:
      dimension: 3
      interpretation:
                  [1 0 0]  
       [tp](x0) = [0 0 4]x0
                  [0 0 0]  ,
       
             [6]
       [c] = [0]
             [1],
       
             [4]
       [y] = [0]
             [0],
       
                       [1 0 0]     [1 0 0]  
       [mat](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                       [0 0 0]     [0 0 1]  ,
       
             [0]
       [X] = [0]
             [0],
       
                   [1 1 6]     [0]
       [chk](x0) = [0 0 5]x0 + [1]
                   [0 0 0]     [0],
       
                    
       [no](x0) = x0
                    ,
       
                    [1 0 6]  
       [mark](x0) = [0 1 0]x0
                    [0 0 1]  ,
       
                      [1 0 0]     [1]
       [active](x0) = [0 0 6]x0 + [0]
                      [0 0 0]     [0],
       
                 [1 0 0]  
       [f](x0) = [0 0 6]x0
                 [0 0 0]  
      orientation:
                      [1 0 0]    [1]    [1 0 0]                 
       active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x = mark(f(f(x)))
                      [0 0 0]    [0]    [0 0 0]                 
       
                       [1 0 6]    [0]    [1 0 6]                                                    
       chk(no(f(x))) = [0 0 0]x + [1] >= [0 0 0]x = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                       [0 0 0]    [0]    [0 0 0]                                                    
       
                      [1 0 0]    [1]    [1 0 0]    [1]               
       f(active(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = active(f(x))
                      [0 0 0]    [0]    [0 0 0]    [0]               
       
                    [1 0 6]     [1 0 0]              
       f(mark(x)) = [0 0 6]x >= [0 0 6]x = mark(f(x))
                    [0 0 0]     [0 0 0]              
       
                  [1 0 0]     [1 0 0]            
       f(no(x)) = [0 0 6]x >= [0 0 6]x = no(f(x))
                  [0 0 0]     [0 0 0]            
       
                     [1 0 6]     [1 0 6]                                                     
       tp(mark(x)) = [0 0 4]x >= [0 0 0]x = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                     [0 0 0]     [0 0 0]                                                     
       
                          [1 0 0]    [4]    [1 0 0]    [4]                
       mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y()))
                          [0 0 0]    [0]    [0 0 0]    [0]                
       
                      [12]    [7]              
       chk(no(c())) = [6 ] >= [6] = active(c())
                      [0 ]    [0]              
       
                       [1 0 0]    [6]    [6]          
       mat(f(x),c()) = [0 0 0]x + [0] >= [0] = no(c())
                       [0 0 0]    [1]    [1]          
      problem:
       strict:
        chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
        f(active(x)) -> active(f(x))
        f(mark(x)) -> mark(f(x))
       weak:
        active(f(x)) -> mark(f(f(x)))
        f(no(x)) -> no(f(x))
        tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
        mat(f(x),f(y())) -> f(mat(x,y()))
        chk(no(c())) -> active(c())
        mat(f(x),c()) -> no(c())
      Matrix Interpretation Processor:
       dimension: 3
       interpretation:
                   [1 0 0]     [0]
        [tp](x0) = [0 0 0]x0 + [0]
                   [0 0 0]     [7],
        
              [0]
        [c] = [3]
              [5],
        
              [5]
        [y] = [0]
              [0],
        
                        [1 0 0]     [1 0 1]  
        [mat](x0, x1) = [0 0 0]x0 + [0 0 2]x1
                        [0 0 0]     [0 0 1]  ,
        
              [4]
        [X] = [0]
              [0],
        
                    [1 1 1]     [0]
        [chk](x0) = [0 0 1]x0 + [5]
                    [0 0 0]     [1],
        
                        [5]
        [no](x0) = x0 + [0]
                        [0],
        
                     [1 0 4]     [4]
        [mark](x0) = [0 0 0]x0 + [0]
                     [0 0 1]     [0],
        
                       [1 0 0]     [6]
        [active](x0) = [0 0 2]x0 + [0]
                       [0 0 0]     [0],
        
                  [1 0 0]  
        [f](x0) = [0 0 4]x0
                  [0 0 0]  
       orientation:
                        [1 0 4]    [5]    [1 0 4]    [4]                                                   
        chk(no(f(x))) = [0 0 0]x + [5] >= [0 0 0]x + [4] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                        [0 0 0]    [1]    [0 0 0]    [0]                                                   
        
                       [1 0 0]    [6]    [1 0 0]    [6]               
        f(active(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = active(f(x))
                       [0 0 0]    [0]    [0 0 0]    [0]               
        
                     [1 0 4]    [4]    [1 0 0]    [4]             
        f(mark(x)) = [0 0 4]x + [0] >= [0 0 0]x + [0] = mark(f(x))
                     [0 0 0]    [0]    [0 0 0]    [0]             
        
                       [1 0 0]    [6]    [1 0 0]    [4]                
        active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x)))
                       [0 0 0]    [0]    [0 0 0]    [0]                
        
                   [1 0 0]    [5]    [1 0 0]    [5]           
        f(no(x)) = [0 0 4]x + [0] >= [0 0 4]x + [0] = no(f(x))
                   [0 0 0]    [0]    [0 0 0]    [0]           
        
                      [1 0 4]    [4]    [1 0 4]    [4]                                                    
        tp(mark(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                      [0 0 0]    [7]    [0 0 0]    [7]                                                    
        
                           [1 0 0]    [5]    [1 0 0]    [5]                
        mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y()))
                           [0 0 0]    [0]    [0 0 0]    [0]                
        
                       [13]    [6 ]              
        chk(no(c())) = [10] >= [10] = active(c())
                       [1 ]    [0 ]              
        
                        [1 0 0]    [5 ]    [5]          
        mat(f(x),c()) = [0 0 0]x + [10] >= [3] = no(c())
                        [0 0 0]    [5 ]    [5]          
       problem:
        strict:
         f(active(x)) -> active(f(x))
         f(mark(x)) -> mark(f(x))
        weak:
         chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
         active(f(x)) -> mark(f(f(x)))
         f(no(x)) -> no(f(x))
         tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
         mat(f(x),f(y())) -> f(mat(x,y()))
         chk(no(c())) -> active(c())
         mat(f(x),c()) -> no(c())
       Matrix Interpretation Processor:
        dimension: 3
        interpretation:
                    [1 0 7]     [0]
         [tp](x0) = [0 0 5]x0 + [1]
                    [0 0 0]     [0],
         
               [0]
         [c] = [0]
               [1],
         
               [6]
         [y] = [0]
               [0],
         
                         [1 0 4]     [1 0 2]  
         [mat](x0, x1) = [0 0 0]x0 + [0 0 3]x1
                         [0 0 0]     [0 0 1]  ,
         
               [2]
         [X] = [0]
               [0],
         
                     [1 4 0]     [0]
         [chk](x0) = [0 0 0]x0 + [4]
                     [0 0 0]     [0],
         
                    [1 1 0]     [2]
         [no](x0) = [0 1 1]x0 + [2]
                    [0 0 1]     [0],
         
                      [1 0 7]     [2]
         [mark](x0) = [0 1 0]x0 + [0]
                      [0 0 1]     [0],
         
                        [1 2 5]     [2]
         [active](x0) = [0 1 2]x0 + [2]
                        [0 0 0]     [0],
         
                   [1 2 4]  
         [f](x0) = [0 1 2]x0
                   [0 0 0]  
        orientation:
                        [1 4 9]    [6]    [1 4 8]    [2]               
         f(active(x)) = [0 1 2]x + [2] >= [0 1 2]x + [2] = active(f(x))
                        [0 0 0]    [0]    [0 0 0]    [0]               
         
                      [1  2  11]    [2]    [1 2 4]    [2]             
         f(mark(x)) = [0  1  2 ]x + [0] >= [0 1 2]x + [0] = mark(f(x))
                      [0  0  0 ]    [0]    [0 0 0]    [0]             
         
                         [1  7  14]    [10]    [1  0  14]    [10]                                                   
         chk(no(f(x))) = [0  0  0 ]x + [4 ] >= [0  0  0 ]x + [4 ] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                         [0  0  0 ]    [0 ]    [0  0  0 ]    [0 ]                                                   
         
                        [1 4 8]    [2]    [1 4 8]    [2]                
         active(f(x)) = [0 1 2]x + [2] >= [0 1 2]x + [0] = mark(f(f(x)))
                        [0 0 0]    [0]    [0 0 0]    [0]                
         
                    [1 3 6]    [6]    [1 3 6]    [2]           
         f(no(x)) = [0 1 3]x + [2] >= [0 1 2]x + [2] = no(f(x))
                    [0 0 0]    [0]    [0 0 0]    [0]           
         
                       [1  0  14]    [2]    [1  0  14]    [2]                                                    
         tp(mark(x)) = [0  0  5 ]x + [1] >= [0  0  0 ]x + [1] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                       [0  0  0 ]    [0]    [0  0  0 ]    [0]                                                    
         
                            [1 2 4]    [6]    [1 0 4]    [6]                
         mat(f(x),f(y())) = [0 0 0]x + [0] >= [0 0 0]x + [0] = f(mat(x,y()))
                            [0 0 0]    [0]    [0 0 0]    [0]                
         
                        [14]    [7]              
         chk(no(c())) = [4 ] >= [4] = active(c())
                        [0 ]    [0]              
         
                         [1 2 4]    [2]    [2]          
         mat(f(x),c()) = [0 0 0]x + [3] >= [3] = no(c())
                         [0 0 0]    [1]    [1]          
        problem:
         strict:
          f(mark(x)) -> mark(f(x))
         weak:
          f(active(x)) -> active(f(x))
          chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
          active(f(x)) -> mark(f(f(x)))
          f(no(x)) -> no(f(x))
          tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
          mat(f(x),f(y())) -> f(mat(x,y()))
          chk(no(c())) -> active(c())
          mat(f(x),c()) -> no(c())
        Matrix Interpretation Processor:
         dimension: 3
         interpretation:
                     [1 0 1]     [0]
          [tp](x0) = [0 0 1]x0 + [0]
                     [0 0 1]     [1],
          
                [0]
          [c] = [0]
                [0],
          
                [0]
          [y] = [0]
                [1],
          
                          [1 0 0]     [1 0 0]     [0]
          [mat](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0]
                          [0 0 0]     [0 0 0]     [1],
          
                [0]
          [X] = [0]
                [0],
          
                      [1 1 0]     [6]
          [chk](x0) = [0 0 4]x0 + [1]
                      [0 0 0]     [1],
          
                       
          [no](x0) = x0
                       ,
          
                       [1 0 0]     [6]
          [mark](x0) = [0 0 0]x0 + [0]
                       [0 0 1]     [1],
          
                         [1 1 4]     [6]
          [active](x0) = [0 0 0]x0 + [0]
                         [0 0 1]     [1],
          
                    [1 0 1]     [0]
          [f](x0) = [0 0 0]x0 + [1]
                    [0 0 1]     [0]
         orientation:
                       [1 0 1]    [7]    [1 0 1]    [6]             
          f(mark(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = mark(f(x))
                       [0 0 1]    [1]    [0 0 1]    [1]             
          
                         [1 1 5]    [7]    [1 0 5]    [7]               
          f(active(x)) = [0 0 0]x + [1] >= [0 0 0]x + [0] = active(f(x))
                         [0 0 1]    [1]    [0 0 1]    [1]               
          
                          [1 0 1]    [7]    [1 0 1]    [7]                                                   
          chk(no(f(x))) = [0 0 4]x + [1] >= [0 0 0]x + [1] = f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                          [0 0 0]    [1]    [0 0 0]    [1]                                                   
          
                         [1 0 5]    [7]    [1 0 2]    [6]                
          active(f(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = mark(f(f(x)))
                         [0 0 1]    [1]    [0 0 1]    [1]                
          
                     [1 0 1]    [0]    [1 0 1]    [0]           
          f(no(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = no(f(x))
                     [0 0 1]    [0]    [0 0 1]    [0]           
          
                        [1 0 1]    [7]    [1 0 1]    [7]                                                    
          tp(mark(x)) = [0 0 1]x + [1] >= [0 0 0]x + [1] = tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
                        [0 0 1]    [2]    [0 0 0]    [2]                                                    
          
                             [1 0 1]    [1]    [1 0 0]    [1]                
          mat(f(x),f(y())) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(mat(x,y()))
                             [0 0 0]    [1]    [0 0 0]    [1]                
          
                         [6]    [6]              
          chk(no(c())) = [1] >= [0] = active(c())
                         [1]    [1]              
          
                          [1 0 1]    [0]    [0]          
          mat(f(x),c()) = [0 0 0]x + [0] >= [0] = no(c())
                          [0 0 0]    [1]    [0]          
         problem:
          strict:
           
          weak:
           f(mark(x)) -> mark(f(x))
           f(active(x)) -> active(f(x))
           chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
           active(f(x)) -> mark(f(f(x)))
           f(no(x)) -> no(f(x))
           tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
           mat(f(x),f(y())) -> f(mat(x,y()))
           chk(no(c())) -> active(c())
           mat(f(x),c()) -> no(c())
         Qed