YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   2(7(x1)) -> 1(8(x1))
   2(8(1(x1))) -> 8(x1)
   2(8(x1)) -> 4(x1)
   5(9(x1)) -> 0(x1)
   4(x1) -> 5(2(3(x1)))
   5(3(x1)) -> 6(0(x1))
   2(8(x1)) -> 7(x1)
   4(7(x1)) -> 1(3(x1))
   5(2(6(x1))) -> 6(2(4(x1)))
   9(7(x1)) -> 7(5(x1))
   7(2(x1)) -> 4(x1)
   7(0(x1)) -> 9(3(x1))
   6(9(x1)) -> 9(x1)
   9(5(9(x1))) -> 5(7(x1))
   4(x1) -> 9(6(6(x1)))
   9(x1) -> 6(7(x1))
   6(2(x1)) -> 7(7(x1))
   2(4(x1)) -> 0(7(x1))
   6(6(x1)) -> 3(x1)
   0(3(x1)) -> 5(3(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [6](x0) = x0,
    
    [3](x0) = x0 + 16,
    
    [0](x0) = x0 + 5,
    
    [5](x0) = x0 + 4,
    
    [9](x0) = x0,
    
    [4](x0) = x0 + 30,
    
    [1](x0) = x0 + 2,
    
    [8](x0) = x0 + 12,
    
    [2](x0) = x0 + 2,
    
    [7](x0) = x0 + 8
   orientation:
    2(7(x1)) = x1 + 10 >= x1 + 14 = 1(8(x1))
    
    2(8(1(x1))) = x1 + 16 >= x1 + 12 = 8(x1)
    
    2(8(x1)) = x1 + 14 >= x1 + 30 = 4(x1)
    
    5(9(x1)) = x1 + 4 >= x1 + 5 = 0(x1)
    
    4(x1) = x1 + 30 >= x1 + 22 = 5(2(3(x1)))
    
    5(3(x1)) = x1 + 20 >= x1 + 5 = 6(0(x1))
    
    2(8(x1)) = x1 + 14 >= x1 + 8 = 7(x1)
    
    4(7(x1)) = x1 + 38 >= x1 + 18 = 1(3(x1))
    
    5(2(6(x1))) = x1 + 6 >= x1 + 32 = 6(2(4(x1)))
    
    9(7(x1)) = x1 + 8 >= x1 + 12 = 7(5(x1))
    
    7(2(x1)) = x1 + 10 >= x1 + 30 = 4(x1)
    
    7(0(x1)) = x1 + 13 >= x1 + 16 = 9(3(x1))
    
    6(9(x1)) = x1 >= x1 = 9(x1)
    
    9(5(9(x1))) = x1 + 4 >= x1 + 12 = 5(7(x1))
    
    4(x1) = x1 + 30 >= x1 = 9(6(6(x1)))
    
    9(x1) = x1 >= x1 + 8 = 6(7(x1))
    
    6(2(x1)) = x1 + 2 >= x1 + 16 = 7(7(x1))
    
    2(4(x1)) = x1 + 32 >= x1 + 13 = 0(7(x1))
    
    6(6(x1)) = x1 >= x1 + 16 = 3(x1)
    
    0(3(x1)) = x1 + 21 >= x1 + 20 = 5(3(x1))
   problem:
    strict:
     2(7(x1)) -> 1(8(x1))
     2(8(x1)) -> 4(x1)
     5(9(x1)) -> 0(x1)
     5(2(6(x1))) -> 6(2(4(x1)))
     9(7(x1)) -> 7(5(x1))
     7(2(x1)) -> 4(x1)
     7(0(x1)) -> 9(3(x1))
     6(9(x1)) -> 9(x1)
     9(5(9(x1))) -> 5(7(x1))
     9(x1) -> 6(7(x1))
     6(2(x1)) -> 7(7(x1))
     6(6(x1)) -> 3(x1)
    weak:
     2(8(1(x1))) -> 8(x1)
     4(x1) -> 5(2(3(x1)))
     5(3(x1)) -> 6(0(x1))
     2(8(x1)) -> 7(x1)
     4(7(x1)) -> 1(3(x1))
     4(x1) -> 9(6(6(x1)))
     2(4(x1)) -> 0(7(x1))
     0(3(x1)) -> 5(3(x1))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [6](x0) = x0,
     
     [3](x0) = x0 + 1,
     
     [0](x0) = x0,
     
     [5](x0) = x0,
     
     [9](x0) = x0 + 24,
     
     [4](x0) = x0 + 24,
     
     [1](x0) = x0 + 19,
     
     [8](x0) = x0 + 14,
     
     [2](x0) = x0 + 17,
     
     [7](x0) = x0 + 8
    orientation:
     2(7(x1)) = x1 + 25 >= x1 + 33 = 1(8(x1))
     
     2(8(x1)) = x1 + 31 >= x1 + 24 = 4(x1)
     
     5(9(x1)) = x1 + 24 >= x1 = 0(x1)
     
     5(2(6(x1))) = x1 + 17 >= x1 + 41 = 6(2(4(x1)))
     
     9(7(x1)) = x1 + 32 >= x1 + 8 = 7(5(x1))
     
     7(2(x1)) = x1 + 25 >= x1 + 24 = 4(x1)
     
     7(0(x1)) = x1 + 8 >= x1 + 25 = 9(3(x1))
     
     6(9(x1)) = x1 + 24 >= x1 + 24 = 9(x1)
     
     9(5(9(x1))) = x1 + 48 >= x1 + 8 = 5(7(x1))
     
     9(x1) = x1 + 24 >= x1 + 8 = 6(7(x1))
     
     6(2(x1)) = x1 + 17 >= x1 + 16 = 7(7(x1))
     
     6(6(x1)) = x1 >= x1 + 1 = 3(x1)
     
     2(8(1(x1))) = x1 + 50 >= x1 + 14 = 8(x1)
     
     4(x1) = x1 + 24 >= x1 + 18 = 5(2(3(x1)))
     
     5(3(x1)) = x1 + 1 >= x1 = 6(0(x1))
     
     2(8(x1)) = x1 + 31 >= x1 + 8 = 7(x1)
     
     4(7(x1)) = x1 + 32 >= x1 + 20 = 1(3(x1))
     
     4(x1) = x1 + 24 >= x1 + 24 = 9(6(6(x1)))
     
     2(4(x1)) = x1 + 41 >= x1 + 8 = 0(7(x1))
     
     0(3(x1)) = x1 + 1 >= x1 + 1 = 5(3(x1))
    problem:
     strict:
      2(7(x1)) -> 1(8(x1))
      5(2(6(x1))) -> 6(2(4(x1)))
      7(0(x1)) -> 9(3(x1))
      6(9(x1)) -> 9(x1)
      6(6(x1)) -> 3(x1)
     weak:
      2(8(x1)) -> 4(x1)
      5(9(x1)) -> 0(x1)
      9(7(x1)) -> 7(5(x1))
      7(2(x1)) -> 4(x1)
      9(5(9(x1))) -> 5(7(x1))
      9(x1) -> 6(7(x1))
      6(2(x1)) -> 7(7(x1))
      2(8(1(x1))) -> 8(x1)
      4(x1) -> 5(2(3(x1)))
      5(3(x1)) -> 6(0(x1))
      2(8(x1)) -> 7(x1)
      4(7(x1)) -> 1(3(x1))
      4(x1) -> 9(6(6(x1)))
      2(4(x1)) -> 0(7(x1))
      0(3(x1)) -> 5(3(x1))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [6](x0) = x0 + 1,
      
      [3](x0) = x0 + 1,
      
      [0](x0) = x0,
      
      [5](x0) = x0,
      
      [9](x0) = x0 + 4,
      
      [4](x0) = x0 + 6,
      
      [1](x0) = x0 + 1,
      
      [8](x0) = x0 + 9,
      
      [2](x0) = x0 + 5,
      
      [7](x0) = x0 + 2
     orientation:
      2(7(x1)) = x1 + 7 >= x1 + 10 = 1(8(x1))
      
      5(2(6(x1))) = x1 + 6 >= x1 + 12 = 6(2(4(x1)))
      
      7(0(x1)) = x1 + 2 >= x1 + 5 = 9(3(x1))
      
      6(9(x1)) = x1 + 5 >= x1 + 4 = 9(x1)
      
      6(6(x1)) = x1 + 2 >= x1 + 1 = 3(x1)
      
      2(8(x1)) = x1 + 14 >= x1 + 6 = 4(x1)
      
      5(9(x1)) = x1 + 4 >= x1 = 0(x1)
      
      9(7(x1)) = x1 + 6 >= x1 + 2 = 7(5(x1))
      
      7(2(x1)) = x1 + 7 >= x1 + 6 = 4(x1)
      
      9(5(9(x1))) = x1 + 8 >= x1 + 2 = 5(7(x1))
      
      9(x1) = x1 + 4 >= x1 + 3 = 6(7(x1))
      
      6(2(x1)) = x1 + 6 >= x1 + 4 = 7(7(x1))
      
      2(8(1(x1))) = x1 + 15 >= x1 + 9 = 8(x1)
      
      4(x1) = x1 + 6 >= x1 + 6 = 5(2(3(x1)))
      
      5(3(x1)) = x1 + 1 >= x1 + 1 = 6(0(x1))
      
      2(8(x1)) = x1 + 14 >= x1 + 2 = 7(x1)
      
      4(7(x1)) = x1 + 8 >= x1 + 2 = 1(3(x1))
      
      4(x1) = x1 + 6 >= x1 + 6 = 9(6(6(x1)))
      
      2(4(x1)) = x1 + 11 >= x1 + 2 = 0(7(x1))
      
      0(3(x1)) = x1 + 1 >= x1 + 1 = 5(3(x1))
     problem:
      strict:
       2(7(x1)) -> 1(8(x1))
       5(2(6(x1))) -> 6(2(4(x1)))
       7(0(x1)) -> 9(3(x1))
      weak:
       6(9(x1)) -> 9(x1)
       6(6(x1)) -> 3(x1)
       2(8(x1)) -> 4(x1)
       5(9(x1)) -> 0(x1)
       9(7(x1)) -> 7(5(x1))
       7(2(x1)) -> 4(x1)
       9(5(9(x1))) -> 5(7(x1))
       9(x1) -> 6(7(x1))
       6(2(x1)) -> 7(7(x1))
       2(8(1(x1))) -> 8(x1)
       4(x1) -> 5(2(3(x1)))
       5(3(x1)) -> 6(0(x1))
       2(8(x1)) -> 7(x1)
       4(7(x1)) -> 1(3(x1))
       4(x1) -> 9(6(6(x1)))
       2(4(x1)) -> 0(7(x1))
       0(3(x1)) -> 5(3(x1))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [6](x0) = x0,
       
       [3](x0) = x0,
       
       [0](x0) = x0,
       
       [5](x0) = x0,
       
       [9](x0) = x0 + 15,
       
       [4](x0) = x0 + 16,
       
       [1](x0) = x0 + 3,
       
       [8](x0) = x0 + 16,
       
       [2](x0) = x0 + 16,
       
       [7](x0) = x0 + 4
      orientation:
       2(7(x1)) = x1 + 20 >= x1 + 19 = 1(8(x1))
       
       5(2(6(x1))) = x1 + 16 >= x1 + 32 = 6(2(4(x1)))
       
       7(0(x1)) = x1 + 4 >= x1 + 15 = 9(3(x1))
       
       6(9(x1)) = x1 + 15 >= x1 + 15 = 9(x1)
       
       6(6(x1)) = x1 >= x1 = 3(x1)
       
       2(8(x1)) = x1 + 32 >= x1 + 16 = 4(x1)
       
       5(9(x1)) = x1 + 15 >= x1 = 0(x1)
       
       9(7(x1)) = x1 + 19 >= x1 + 4 = 7(5(x1))
       
       7(2(x1)) = x1 + 20 >= x1 + 16 = 4(x1)
       
       9(5(9(x1))) = x1 + 30 >= x1 + 4 = 5(7(x1))
       
       9(x1) = x1 + 15 >= x1 + 4 = 6(7(x1))
       
       6(2(x1)) = x1 + 16 >= x1 + 8 = 7(7(x1))
       
       2(8(1(x1))) = x1 + 35 >= x1 + 16 = 8(x1)
       
       4(x1) = x1 + 16 >= x1 + 16 = 5(2(3(x1)))
       
       5(3(x1)) = x1 >= x1 = 6(0(x1))
       
       2(8(x1)) = x1 + 32 >= x1 + 4 = 7(x1)
       
       4(7(x1)) = x1 + 20 >= x1 + 3 = 1(3(x1))
       
       4(x1) = x1 + 16 >= x1 + 15 = 9(6(6(x1)))
       
       2(4(x1)) = x1 + 32 >= x1 + 4 = 0(7(x1))
       
       0(3(x1)) = x1 >= x1 = 5(3(x1))
      problem:
       strict:
        5(2(6(x1))) -> 6(2(4(x1)))
        7(0(x1)) -> 9(3(x1))
       weak:
        2(7(x1)) -> 1(8(x1))
        6(9(x1)) -> 9(x1)
        6(6(x1)) -> 3(x1)
        2(8(x1)) -> 4(x1)
        5(9(x1)) -> 0(x1)
        9(7(x1)) -> 7(5(x1))
        7(2(x1)) -> 4(x1)
        9(5(9(x1))) -> 5(7(x1))
        9(x1) -> 6(7(x1))
        6(2(x1)) -> 7(7(x1))
        2(8(1(x1))) -> 8(x1)
        4(x1) -> 5(2(3(x1)))
        5(3(x1)) -> 6(0(x1))
        2(8(x1)) -> 7(x1)
        4(7(x1)) -> 1(3(x1))
        4(x1) -> 9(6(6(x1)))
        2(4(x1)) -> 0(7(x1))
        0(3(x1)) -> 5(3(x1))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [6](x0) = x0,
        
        [3](x0) = x0,
        
        [0](x0) = x0 + 3,
        
        [5](x0) = x0 + 3,
        
        [9](x0) = x0 + 8,
        
        [4](x0) = x0 + 25,
        
        [1](x0) = x0 + 11,
        
        [8](x0) = x0 + 14,
        
        [2](x0) = x0 + 18,
        
        [7](x0) = x0 + 7
       orientation:
        5(2(6(x1))) = x1 + 21 >= x1 + 43 = 6(2(4(x1)))
        
        7(0(x1)) = x1 + 10 >= x1 + 8 = 9(3(x1))
        
        2(7(x1)) = x1 + 25 >= x1 + 25 = 1(8(x1))
        
        6(9(x1)) = x1 + 8 >= x1 + 8 = 9(x1)
        
        6(6(x1)) = x1 >= x1 = 3(x1)
        
        2(8(x1)) = x1 + 32 >= x1 + 25 = 4(x1)
        
        5(9(x1)) = x1 + 11 >= x1 + 3 = 0(x1)
        
        9(7(x1)) = x1 + 15 >= x1 + 10 = 7(5(x1))
        
        7(2(x1)) = x1 + 25 >= x1 + 25 = 4(x1)
        
        9(5(9(x1))) = x1 + 19 >= x1 + 10 = 5(7(x1))
        
        9(x1) = x1 + 8 >= x1 + 7 = 6(7(x1))
        
        6(2(x1)) = x1 + 18 >= x1 + 14 = 7(7(x1))
        
        2(8(1(x1))) = x1 + 43 >= x1 + 14 = 8(x1)
        
        4(x1) = x1 + 25 >= x1 + 21 = 5(2(3(x1)))
        
        5(3(x1)) = x1 + 3 >= x1 + 3 = 6(0(x1))
        
        2(8(x1)) = x1 + 32 >= x1 + 7 = 7(x1)
        
        4(7(x1)) = x1 + 32 >= x1 + 11 = 1(3(x1))
        
        4(x1) = x1 + 25 >= x1 + 8 = 9(6(6(x1)))
        
        2(4(x1)) = x1 + 43 >= x1 + 10 = 0(7(x1))
        
        0(3(x1)) = x1 + 3 >= x1 + 3 = 5(3(x1))
       problem:
        strict:
         5(2(6(x1))) -> 6(2(4(x1)))
        weak:
         7(0(x1)) -> 9(3(x1))
         2(7(x1)) -> 1(8(x1))
         6(9(x1)) -> 9(x1)
         6(6(x1)) -> 3(x1)
         2(8(x1)) -> 4(x1)
         5(9(x1)) -> 0(x1)
         9(7(x1)) -> 7(5(x1))
         7(2(x1)) -> 4(x1)
         9(5(9(x1))) -> 5(7(x1))
         9(x1) -> 6(7(x1))
         6(2(x1)) -> 7(7(x1))
         2(8(1(x1))) -> 8(x1)
         4(x1) -> 5(2(3(x1)))
         5(3(x1)) -> 6(0(x1))
         2(8(x1)) -> 7(x1)
         4(7(x1)) -> 1(3(x1))
         4(x1) -> 9(6(6(x1)))
         2(4(x1)) -> 0(7(x1))
         0(3(x1)) -> 5(3(x1))
       Arctic Interpretation Processor:
        dimension: 2
        interpretation:
                   [0  -&]  
         [6](x0) = [0  -&]x0,
         
                   [0  -&]  
         [3](x0) = [-& -&]x0,
         
                   [0  -&]  
         [0](x0) = [0  -&]x0,
         
                   [0 0]  
         [5](x0) = [0 0]x0,
         
                   [0 0]  
         [9](x0) = [0 0]x0,
         
                   [0  -&]  
         [4](x0) = [0  -&]x0,
         
                   [0 0]  
         [1](x0) = [0 1]x0,
         
                   [0 0]  
         [8](x0) = [0 0]x0,
         
                   [0 0]  
         [2](x0) = [0 1]x0,
         
                   [0  -&]  
         [7](x0) = [0  0 ]x0
        orientation:
                       [1  -&]      [0  -&]                
         5(2(6(x1))) = [1  -&]x1 >= [0  -&]x1 = 6(2(4(x1)))
         
                    [0  -&]      [0  -&]             
         7(0(x1)) = [0  -&]x1 >= [0  -&]x1 = 9(3(x1))
         
                    [0 0]      [0 0]             
         2(7(x1)) = [1 1]x1 >= [1 1]x1 = 1(8(x1))
         
                    [0 0]      [0 0]          
         6(9(x1)) = [0 0]x1 >= [0 0]x1 = 9(x1)
         
                    [0  -&]      [0  -&]          
         6(6(x1)) = [0  -&]x1 >= [-& -&]x1 = 3(x1)
         
                    [0 0]      [0  -&]          
         2(8(x1)) = [1 1]x1 >= [0  -&]x1 = 4(x1)
         
                    [0 0]      [0  -&]          
         5(9(x1)) = [0 0]x1 >= [0  -&]x1 = 0(x1)
         
                    [0 0]      [0 0]             
         9(7(x1)) = [0 0]x1 >= [0 0]x1 = 7(5(x1))
         
                    [0 0]      [0  -&]          
         7(2(x1)) = [0 1]x1 >= [0  -&]x1 = 4(x1)
         
                       [0 0]      [0 0]             
         9(5(9(x1))) = [0 0]x1 >= [0 0]x1 = 5(7(x1))
         
                 [0 0]      [0  -&]             
         9(x1) = [0 0]x1 >= [0  -&]x1 = 6(7(x1))
         
                    [0 0]      [0  -&]             
         6(2(x1)) = [0 0]x1 >= [0  0 ]x1 = 7(7(x1))
         
                       [0 1]      [0 0]          
         2(8(1(x1))) = [1 2]x1 >= [0 0]x1 = 8(x1)
         
                 [0  -&]      [0  -&]                
         4(x1) = [0  -&]x1 >= [0  -&]x1 = 5(2(3(x1)))
         
                    [0  -&]      [0  -&]             
         5(3(x1)) = [0  -&]x1 >= [0  -&]x1 = 6(0(x1))
         
                    [0 0]      [0  -&]          
         2(8(x1)) = [1 1]x1 >= [0  0 ]x1 = 7(x1)
         
                    [0  -&]      [0  -&]             
         4(7(x1)) = [0  -&]x1 >= [0  -&]x1 = 1(3(x1))
         
                 [0  -&]      [0  -&]                
         4(x1) = [0  -&]x1 >= [0  -&]x1 = 9(6(6(x1)))
         
                    [0  -&]      [0  -&]             
         2(4(x1)) = [1  -&]x1 >= [0  -&]x1 = 0(7(x1))
         
                    [0  -&]      [0  -&]             
         0(3(x1)) = [0  -&]x1 >= [0  -&]x1 = 5(3(x1))
        problem:
         strict:
          
         weak:
          5(2(6(x1))) -> 6(2(4(x1)))
          7(0(x1)) -> 9(3(x1))
          2(7(x1)) -> 1(8(x1))
          6(9(x1)) -> 9(x1)
          6(6(x1)) -> 3(x1)
          2(8(x1)) -> 4(x1)
          5(9(x1)) -> 0(x1)
          9(7(x1)) -> 7(5(x1))
          7(2(x1)) -> 4(x1)
          9(5(9(x1))) -> 5(7(x1))
          9(x1) -> 6(7(x1))
          6(2(x1)) -> 7(7(x1))
          2(8(1(x1))) -> 8(x1)
          4(x1) -> 5(2(3(x1)))
          5(3(x1)) -> 6(0(x1))
          2(8(x1)) -> 7(x1)
          4(7(x1)) -> 1(3(x1))
          4(x1) -> 9(6(6(x1)))
          2(4(x1)) -> 0(7(x1))
          0(3(x1)) -> 5(3(x1))
        Qed