YES(?,O(n^3))

Problem:
 3(1(x1)) -> 4(1(x1))
 5(9(x1)) -> 2(6(5(x1)))
 3(5(x1)) -> 8(9(7(x1)))
 9(x1) -> 3(2(3(x1)))
 8(4(x1)) -> 6(x1)
 2(6(x1)) -> 4(3(x1))
 3(8(x1)) -> 3(2(7(x1)))
 9(x1) -> 5(0(2(x1)))
 8(8(4(x1))) -> 1(9(x1))
 7(1(x1)) -> 6(9(x1))
 3(9(x1)) -> 9(3(x1))
 7(5(x1)) -> 1(0(x1))

Proof:
 RT Transformation Processor:
  strict:
   3(1(x1)) -> 4(1(x1))
   5(9(x1)) -> 2(6(5(x1)))
   3(5(x1)) -> 8(9(7(x1)))
   9(x1) -> 3(2(3(x1)))
   8(4(x1)) -> 6(x1)
   2(6(x1)) -> 4(3(x1))
   3(8(x1)) -> 3(2(7(x1)))
   9(x1) -> 5(0(2(x1)))
   8(8(4(x1))) -> 1(9(x1))
   7(1(x1)) -> 6(9(x1))
   3(9(x1)) -> 9(3(x1))
   7(5(x1)) -> 1(0(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0](x0) = x0 + 2,
    
    [8](x0) = x0 + 2,
    
    [7](x0) = x0 + 27,
    
    [2](x0) = x0 + 12,
    
    [6](x0) = x0 + 1,
    
    [5](x0) = x0 + 20,
    
    [9](x0) = x0 + 22,
    
    [4](x0) = x0 + 6,
    
    [3](x0) = x0 + 4,
    
    [1](x0) = x0 + 12
   orientation:
    3(1(x1)) = x1 + 16 >= x1 + 18 = 4(1(x1))
    
    5(9(x1)) = x1 + 42 >= x1 + 33 = 2(6(5(x1)))
    
    3(5(x1)) = x1 + 24 >= x1 + 51 = 8(9(7(x1)))
    
    9(x1) = x1 + 22 >= x1 + 20 = 3(2(3(x1)))
    
    8(4(x1)) = x1 + 8 >= x1 + 1 = 6(x1)
    
    2(6(x1)) = x1 + 13 >= x1 + 10 = 4(3(x1))
    
    3(8(x1)) = x1 + 6 >= x1 + 43 = 3(2(7(x1)))
    
    9(x1) = x1 + 22 >= x1 + 34 = 5(0(2(x1)))
    
    8(8(4(x1))) = x1 + 10 >= x1 + 34 = 1(9(x1))
    
    7(1(x1)) = x1 + 39 >= x1 + 23 = 6(9(x1))
    
    3(9(x1)) = x1 + 26 >= x1 + 26 = 9(3(x1))
    
    7(5(x1)) = x1 + 47 >= x1 + 14 = 1(0(x1))
   problem:
    strict:
     3(1(x1)) -> 4(1(x1))
     3(5(x1)) -> 8(9(7(x1)))
     3(8(x1)) -> 3(2(7(x1)))
     9(x1) -> 5(0(2(x1)))
     8(8(4(x1))) -> 1(9(x1))
     3(9(x1)) -> 9(3(x1))
    weak:
     5(9(x1)) -> 2(6(5(x1)))
     9(x1) -> 3(2(3(x1)))
     8(4(x1)) -> 6(x1)
     2(6(x1)) -> 4(3(x1))
     7(1(x1)) -> 6(9(x1))
     7(5(x1)) -> 1(0(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [0](x0) = x0 + 2,
     
     [8](x0) = x0 + 18,
     
     [7](x0) = x0 + 12,
     
     [2](x0) = x0,
     
     [6](x0) = x0 + 1,
     
     [5](x0) = x0,
     
     [9](x0) = x0 + 16,
     
     [4](x0) = x0,
     
     [3](x0) = x0,
     
     [1](x0) = x0 + 10
    orientation:
     3(1(x1)) = x1 + 10 >= x1 + 10 = 4(1(x1))
     
     3(5(x1)) = x1 >= x1 + 46 = 8(9(7(x1)))
     
     3(8(x1)) = x1 + 18 >= x1 + 12 = 3(2(7(x1)))
     
     9(x1) = x1 + 16 >= x1 + 2 = 5(0(2(x1)))
     
     8(8(4(x1))) = x1 + 36 >= x1 + 26 = 1(9(x1))
     
     3(9(x1)) = x1 + 16 >= x1 + 16 = 9(3(x1))
     
     5(9(x1)) = x1 + 16 >= x1 + 1 = 2(6(5(x1)))
     
     9(x1) = x1 + 16 >= x1 = 3(2(3(x1)))
     
     8(4(x1)) = x1 + 18 >= x1 + 1 = 6(x1)
     
     2(6(x1)) = x1 + 1 >= x1 = 4(3(x1))
     
     7(1(x1)) = x1 + 22 >= x1 + 17 = 6(9(x1))
     
     7(5(x1)) = x1 + 12 >= x1 + 12 = 1(0(x1))
    problem:
     strict:
      3(1(x1)) -> 4(1(x1))
      3(5(x1)) -> 8(9(7(x1)))
      3(9(x1)) -> 9(3(x1))
     weak:
      3(8(x1)) -> 3(2(7(x1)))
      9(x1) -> 5(0(2(x1)))
      8(8(4(x1))) -> 1(9(x1))
      5(9(x1)) -> 2(6(5(x1)))
      9(x1) -> 3(2(3(x1)))
      8(4(x1)) -> 6(x1)
      2(6(x1)) -> 4(3(x1))
      7(1(x1)) -> 6(9(x1))
      7(5(x1)) -> 1(0(x1))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [0](x0) = x0,
      
      [8](x0) = x0 + 2,
      
      [7](x0) = x0 + 1,
      
      [2](x0) = x0,
      
      [6](x0) = x0 + 1,
      
      [5](x0) = x0 + 2,
      
      [9](x0) = x0 + 2,
      
      [4](x0) = x0,
      
      [3](x0) = x0 + 1,
      
      [1](x0) = x0 + 2
     orientation:
      3(1(x1)) = x1 + 3 >= x1 + 2 = 4(1(x1))
      
      3(5(x1)) = x1 + 3 >= x1 + 5 = 8(9(7(x1)))
      
      3(9(x1)) = x1 + 3 >= x1 + 3 = 9(3(x1))
      
      3(8(x1)) = x1 + 3 >= x1 + 2 = 3(2(7(x1)))
      
      9(x1) = x1 + 2 >= x1 + 2 = 5(0(2(x1)))
      
      8(8(4(x1))) = x1 + 4 >= x1 + 4 = 1(9(x1))
      
      5(9(x1)) = x1 + 4 >= x1 + 3 = 2(6(5(x1)))
      
      9(x1) = x1 + 2 >= x1 + 2 = 3(2(3(x1)))
      
      8(4(x1)) = x1 + 2 >= x1 + 1 = 6(x1)
      
      2(6(x1)) = x1 + 1 >= x1 + 1 = 4(3(x1))
      
      7(1(x1)) = x1 + 3 >= x1 + 3 = 6(9(x1))
      
      7(5(x1)) = x1 + 3 >= x1 + 2 = 1(0(x1))
     problem:
      strict:
       3(5(x1)) -> 8(9(7(x1)))
       3(9(x1)) -> 9(3(x1))
      weak:
       3(1(x1)) -> 4(1(x1))
       3(8(x1)) -> 3(2(7(x1)))
       9(x1) -> 5(0(2(x1)))
       8(8(4(x1))) -> 1(9(x1))
       5(9(x1)) -> 2(6(5(x1)))
       9(x1) -> 3(2(3(x1)))
       8(4(x1)) -> 6(x1)
       2(6(x1)) -> 4(3(x1))
       7(1(x1)) -> 6(9(x1))
       7(5(x1)) -> 1(0(x1))
     Matrix Interpretation Processor:
      dimension: 3
      interpretation:
                 [1 0 0]  
       [0](x0) = [0 0 1]x0
                 [0 0 0]  ,
       
                 [1 5 0]     [0]
       [8](x0) = [0 1 0]x0 + [2]
                 [0 0 0]     [1],
       
                 [1 0 0]     [1]
       [7](x0) = [0 1 2]x0 + [4]
                 [0 0 0]     [0],
       
                 [1 0 0]     [0]
       [2](x0) = [0 1 0]x0 + [6]
                 [0 0 0]     [0],
       
                 [1 0 1]     [0]
       [6](x0) = [0 0 1]x0 + [2]
                 [0 0 0]     [0],
       
                 [1 0 2]     [0]
       [5](x0) = [0 0 5]x0 + [0]
                 [0 0 0]     [2],
       
                 [1 0 2]     [0]
       [9](x0) = [0 0 1]x0 + [0]
                 [0 0 1]     [2],
       
                 [1 0 0]  
       [4](x0) = [0 0 1]x0
                 [0 0 0]  ,
       
                 [1 0 1]     [0]
       [3](x0) = [0 0 2]x0 + [0]
                 [0 0 1]     [1],
       
                 [1 2 3]     [1]
       [1](x0) = [0 0 1]x0 + [0]
                 [0 0 0]     [0]
      orientation:
                  [1 0 2]     [2]    [1 0 0]     [1]              
       3(5(x1)) = [0 0 0]x1 + [4] >= [0 0 0]x1 + [2] = 8(9(7(x1)))
                  [0 0 0]     [3]    [0 0 0]     [1]              
       
                  [1 0 3]     [2]    [1 0 3]     [2]           
       3(9(x1)) = [0 0 2]x1 + [4] >= [0 0 1]x1 + [1] = 9(3(x1))
                  [0 0 1]     [3]    [0 0 1]     [3]           
       
                  [1 2 3]     [1]    [1 2 3]     [1]           
       3(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(1(x1))
                  [0 0 0]     [1]    [0 0 0]     [0]           
       
                  [1 5 0]     [1]    [1 0 0]     [1]              
       3(8(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 3(2(7(x1)))
                  [0 0 0]     [2]    [0 0 0]     [1]              
       
               [1 0 2]     [0]    [1 0 0]     [0]              
       9(x1) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(x1)))
               [0 0 1]     [2]    [0 0 0]     [2]              
       
                     [1  0  10]     [10]    [1 0 7]     [7]           
       8(8(4(x1))) = [0  0  1 ]x1 + [4 ] >= [0 0 1]x1 + [2] = 1(9(x1))
                     [0  0  0 ]     [1 ]    [0 0 0]     [0]           
       
                  [1 0 4]     [4 ]    [1 0 2]     [2 ]              
       5(9(x1)) = [0 0 5]x1 + [10] >= [0 0 0]x1 + [10] = 2(6(5(x1)))
                  [0 0 0]     [2 ]    [0 0 0]     [0 ]              
       
               [1 0 2]     [0]    [1 0 1]     [0]              
       9(x1) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 3(2(3(x1)))
               [0 0 1]     [2]    [0 0 0]     [1]              
       
                  [1 0 5]     [0]    [1 0 1]     [0]        
       8(4(x1)) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [2] = 6(x1)
                  [0 0 0]     [1]    [0 0 0]     [0]        
       
                  [1 0 1]     [0]    [1 0 1]     [0]           
       2(6(x1)) = [0 0 1]x1 + [8] >= [0 0 1]x1 + [1] = 4(3(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]           
       
                  [1 2 3]     [2]    [1 0 3]     [2]           
       7(1(x1)) = [0 0 1]x1 + [4] >= [0 0 1]x1 + [4] = 6(9(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]           
       
                  [1 0 2]     [1]    [1 0 2]     [1]           
       7(5(x1)) = [0 0 5]x1 + [8] >= [0 0 0]x1 + [0] = 1(0(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]           
      problem:
       strict:
        3(9(x1)) -> 9(3(x1))
       weak:
        3(5(x1)) -> 8(9(7(x1)))
        3(1(x1)) -> 4(1(x1))
        3(8(x1)) -> 3(2(7(x1)))
        9(x1) -> 5(0(2(x1)))
        8(8(4(x1))) -> 1(9(x1))
        5(9(x1)) -> 2(6(5(x1)))
        9(x1) -> 3(2(3(x1)))
        8(4(x1)) -> 6(x1)
        2(6(x1)) -> 4(3(x1))
        7(1(x1)) -> 6(9(x1))
        7(5(x1)) -> 1(0(x1))
      Matrix Interpretation Processor:
       dimension: 3
       interpretation:
                  [1 0 0]     [0]
        [0](x0) = [0 0 0]x0 + [1]
                  [0 0 0]     [0],
        
                  [1 7 0]     [1]
        [8](x0) = [0 1 0]x0 + [1]
                  [0 0 0]     [0],
        
                  [1 0 0]     [1]
        [7](x0) = [0 1 2]x0 + [1]
                  [0 0 0]     [0],
        
                  [1 0 0]     [0]
        [2](x0) = [0 1 0]x0 + [1]
                  [0 0 0]     [0],
        
                  [1 0 2]  
        [6](x0) = [0 0 1]x0
                  [0 0 0]  ,
        
                  [1 0 6]     [0]
        [5](x0) = [0 0 3]x0 + [0]
                  [0 0 0]     [1],
        
                  [1 0 2]     [0]
        [9](x0) = [0 0 0]x0 + [0]
                  [0 0 1]     [1],
        
                  [1 0 0]  
        [4](x0) = [0 0 1]x0
                  [0 0 0]  ,
        
                  [1 0 2]  
        [3](x0) = [0 0 1]x0
                  [0 0 1]  ,
        
                  [1 0 6]     [1]
        [1](x0) = [0 0 1]x0 + [0]
                  [0 0 0]     [0]
       orientation:
                   [1 0 4]     [2]    [1 0 4]     [0]           
        3(9(x1)) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = 9(3(x1))
                   [0 0 1]     [1]    [0 0 1]     [1]           
        
                   [1 0 6]     [2]    [1 0 0]     [2]              
        3(5(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 8(9(7(x1)))
                   [0 0 0]     [1]    [0 0 0]     [0]              
        
                   [1 0 6]     [1]    [1 0 6]     [1]           
        3(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(1(x1))
                   [0 0 0]     [0]    [0 0 0]     [0]           
        
                   [1 7 0]     [1]    [1 0 0]     [1]              
        3(8(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 3(2(7(x1)))
                   [0 0 0]     [0]    [0 0 0]     [0]              
        
                [1 0 2]     [0]    [1 0 0]     [0]              
        9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(x1)))
                [0 0 1]     [1]    [0 0 0]     [1]              
        
                      [1  0  14]     [9]    [1 0 8]     [7]           
        8(8(4(x1))) = [0  0  1 ]x1 + [2] >= [0 0 1]x1 + [1] = 1(9(x1))
                      [0  0  0 ]     [0]    [0 0 0]     [0]           
        
                   [1 0 8]     [6]    [1 0 6]     [2]              
        5(9(x1)) = [0 0 3]x1 + [3] >= [0 0 0]x1 + [2] = 2(6(5(x1)))
                   [0 0 0]     [1]    [0 0 0]     [0]              
        
                [1 0 2]     [0]    [1 0 2]                
        9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(2(3(x1)))
                [0 0 1]     [1]    [0 0 0]                
        
                   [1 0 7]     [1]    [1 0 2]          
        8(4(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 = 6(x1)
                   [0 0 0]     [0]    [0 0 0]          
        
                   [1 0 2]     [0]    [1 0 2]             
        2(6(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 = 4(3(x1))
                   [0 0 0]     [0]    [0 0 0]             
        
                   [1 0 6]     [2]    [1 0 4]     [2]           
        7(1(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 + [1] = 6(9(x1))
                   [0 0 0]     [0]    [0 0 0]     [0]           
        
                   [1 0 6]     [1]    [1 0 0]     [1]           
        7(5(x1)) = [0 0 3]x1 + [3] >= [0 0 0]x1 + [0] = 1(0(x1))
                   [0 0 0]     [0]    [0 0 0]     [0]           
       problem:
        strict:
         
        weak:
         3(9(x1)) -> 9(3(x1))
         3(5(x1)) -> 8(9(7(x1)))
         3(1(x1)) -> 4(1(x1))
         3(8(x1)) -> 3(2(7(x1)))
         9(x1) -> 5(0(2(x1)))
         8(8(4(x1))) -> 1(9(x1))
         5(9(x1)) -> 2(6(5(x1)))
         9(x1) -> 3(2(3(x1)))
         8(4(x1)) -> 6(x1)
         2(6(x1)) -> 4(3(x1))
         7(1(x1)) -> 6(9(x1))
         7(5(x1)) -> 1(0(x1))
       Qed