YES

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:
 String Reversal Processor:
  1(3(x1)) -> 1(4(x1))
  9(5(x1)) -> 5(6(2(x1)))
  5(3(x1)) -> 7(9(8(x1)))
  9(x1) -> 3(2(3(x1)))
  4(8(x1)) -> 6(x1)
  6(2(x1)) -> 3(4(x1))
  8(3(x1)) -> 7(2(3(x1)))
  9(x1) -> 2(0(5(x1)))
  4(8(8(x1))) -> 9(1(x1))
  1(7(x1)) -> 9(6(x1))
  9(3(x1)) -> 3(9(x1))
  5(7(x1)) -> 0(1(x1))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 0]  
    [0](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 0 1]     [0]
    [8](x0) = [0 0 0]x0 + [0]
              [0 1 0]     [1],
    
              [1 0 0]  
    [7](x0) = [0 1 0]x0
              [0 1 0]  ,
    
              [1 0 0]  
    [2](x0) = [0 0 1]x0
              [0 0 0]  ,
    
              [1 1 0]  
    [6](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 1 0]  
    [5](x0) = [0 1 1]x0
              [0 0 1]  ,
    
              [1 1 0]  
    [9](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 0 1]  
    [4](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 1 0]  
    [3](x0) = [0 0 1]x0
              [0 0 0]  ,
    
              [1 1 0]  
    [1](x0) = [0 0 0]x0
              [0 1 0]  
   orientation:
               [1 1 1]      [1 0 1]             
    1(3(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 1(4(x1))
               [0 0 1]      [0 0 0]             
    
               [1 2 1]      [1 0 1]                
    9(5(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 5(6(2(x1)))
               [0 0 0]      [0 0 0]                
    
               [1 1 1]      [1 0 1]                
    5(3(x1)) = [0 0 1]x1 >= [0 0 0]x1 = 7(9(8(x1)))
               [0 0 0]      [0 0 0]                
    
            [1 1 0]      [1 1 0]                
    9(x1) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(3(x1)))
            [0 0 0]      [0 0 0]                
    
               [1 1 1]     [1]    [1 1 0]          
    4(8(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 6(x1)
               [0 0 0]     [0]    [0 0 0]          
    
               [1 0 1]      [1 0 1]             
    6(2(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(4(x1))
               [0 0 0]      [0 0 0]             
    
               [1 1 0]     [0]    [1 1 0]                
    8(3(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 7(2(3(x1)))
               [0 0 1]     [1]    [0 0 0]                
    
            [1 1 0]      [1 1 0]                
    9(x1) = [0 0 0]x1 >= [0 0 0]x1 = 2(0(5(x1)))
            [0 0 0]      [0 0 0]                
    
                  [1 1 1]     [2]    [1 1 0]             
    4(8(8(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 9(1(x1))
                  [0 0 0]     [0]    [0 0 0]             
    
               [1 1 0]      [1 1 0]             
    1(7(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 9(6(x1))
               [0 1 0]      [0 0 0]             
    
               [1 1 1]      [1 1 0]             
    9(3(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(9(x1))
               [0 0 0]      [0 0 0]             
    
               [1 1 0]      [1 1 0]             
    5(7(x1)) = [0 2 0]x1 >= [0 0 0]x1 = 0(1(x1))
               [0 1 0]      [0 0 0]             
   problem:
    1(3(x1)) -> 1(4(x1))
    9(5(x1)) -> 5(6(2(x1)))
    5(3(x1)) -> 7(9(8(x1)))
    9(x1) -> 3(2(3(x1)))
    6(2(x1)) -> 3(4(x1))
    8(3(x1)) -> 7(2(3(x1)))
    9(x1) -> 2(0(5(x1)))
    1(7(x1)) -> 9(6(x1))
    9(3(x1)) -> 3(9(x1))
    5(7(x1)) -> 0(1(x1))
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [0](x0) = x0,
     
     [8](x0) = x0,
     
     [7](x0) = x0,
     
     [2](x0) = x0,
     
     [6](x0) = x0,
     
     [5](x0) = 2x0,
     
     [9](x0) = 2x0,
     
     [4](x0) = x0,
     
     [3](x0) = x0,
     
     [1](x0) = 2x0
    orientation:
     1(3(x1)) = 2x1 >= 2x1 = 1(4(x1))
     
     9(5(x1)) = 4x1 >= 2x1 = 5(6(2(x1)))
     
     5(3(x1)) = 2x1 >= 2x1 = 7(9(8(x1)))
     
     9(x1) = 2x1 >= x1 = 3(2(3(x1)))
     
     6(2(x1)) = x1 >= x1 = 3(4(x1))
     
     8(3(x1)) = x1 >= x1 = 7(2(3(x1)))
     
     9(x1) = 2x1 >= 2x1 = 2(0(5(x1)))
     
     1(7(x1)) = 2x1 >= 2x1 = 9(6(x1))
     
     9(3(x1)) = 2x1 >= 2x1 = 3(9(x1))
     
     5(7(x1)) = 2x1 >= 2x1 = 0(1(x1))
    problem:
     1(3(x1)) -> 1(4(x1))
     5(3(x1)) -> 7(9(8(x1)))
     6(2(x1)) -> 3(4(x1))
     8(3(x1)) -> 7(2(3(x1)))
     9(x1) -> 2(0(5(x1)))
     1(7(x1)) -> 9(6(x1))
     9(3(x1)) -> 3(9(x1))
     5(7(x1)) -> 0(1(x1))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [0](x0) = x0,
      
      [8](x0) = 2x0,
      
      [7](x0) = 2x0,
      
      [2](x0) = x0,
      
      [6](x0) = 4x0,
      
      [5](x0) = x0,
      
      [9](x0) = x0,
      
      [4](x0) = x0,
      
      [3](x0) = 4x0,
      
      [1](x0) = 2x0
     orientation:
      1(3(x1)) = 6x1 >= 2x1 = 1(4(x1))
      
      5(3(x1)) = 4x1 >= 4x1 = 7(9(8(x1)))
      
      6(2(x1)) = 4x1 >= 4x1 = 3(4(x1))
      
      8(3(x1)) = 6x1 >= 6x1 = 7(2(3(x1)))
      
      9(x1) = x1 >= x1 = 2(0(5(x1)))
      
      1(7(x1)) = 4x1 >= 4x1 = 9(6(x1))
      
      9(3(x1)) = 4x1 >= 4x1 = 3(9(x1))
      
      5(7(x1)) = 2x1 >= 2x1 = 0(1(x1))
     problem:
      5(3(x1)) -> 7(9(8(x1)))
      6(2(x1)) -> 3(4(x1))
      8(3(x1)) -> 7(2(3(x1)))
      9(x1) -> 2(0(5(x1)))
      1(7(x1)) -> 9(6(x1))
      9(3(x1)) -> 3(9(x1))
      5(7(x1)) -> 0(1(x1))
     String Reversal Processor:
      3(5(x1)) -> 8(9(7(x1)))
      2(6(x1)) -> 4(3(x1))
      3(8(x1)) -> 3(2(7(x1)))
      9(x1) -> 5(0(2(x1)))
      7(1(x1)) -> 6(9(x1))
      3(9(x1)) -> 9(3(x1))
      7(5(x1)) -> 1(0(x1))
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                  [1 0 0]  
        [0](x0) = [0 0 1]x0
                  [0 1 0]  ,
        
                  [1 1 0]     [0]
        [8](x0) = [0 0 0]x0 + [0]
                  [0 0 1]     [1],
        
                  [1 1 0]  
        [7](x0) = [1 1 1]x0
                  [0 0 1]  ,
        
                  [1 0 0]     [0]
        [2](x0) = [0 0 0]x0 + [1]
                  [0 0 1]     [0],
        
                  [1 0 1]  
        [6](x0) = [1 0 0]x0
                  [0 1 0]  ,
        
                  [1 1 0]     [1]
        [5](x0) = [0 0 0]x0 + [0]
                  [1 0 1]     [0],
        
                  [1 0 1]     [1]
        [9](x0) = [0 0 0]x0 + [0]
                  [1 0 0]     [1],
        
                  [1 0 0]  
        [4](x0) = [0 0 0]x0
                  [0 0 0]  ,
        
                  [1 0 1]     [0]
        [3](x0) = [1 0 0]x0 + [1]
                  [1 0 0]     [1],
        
                  [1 0 1]     [1]
        [1](x0) = [1 1 1]x0 + [1]
                  [0 0 0]     [0]
       orientation:
                   [2 1 1]     [1]    [1 1 1]     [1]              
        3(5(x1)) = [1 1 0]x1 + [2] >= [0 0 0]x1 + [0] = 8(9(7(x1)))
                   [1 1 0]     [2]    [1 1 0]     [2]              
        
                   [1 0 1]     [0]    [1 0 1]             
        2(6(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 4(3(x1))
                   [0 1 0]     [0]    [0 0 0]             
        
                   [1 1 1]     [1]    [1 1 1]     [0]              
        3(8(x1)) = [1 1 0]x1 + [1] >= [1 1 0]x1 + [1] = 3(2(7(x1)))
                   [1 1 0]     [1]    [1 1 0]     [1]              
        
                [1 0 1]     [1]    [1 0 1]     [1]              
        9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(x1)))
                [1 0 0]     [1]    [1 0 0]     [1]              
        
                   [2 1 2]     [2]    [2 0 1]     [2]           
        7(1(x1)) = [2 1 2]x1 + [2] >= [1 0 1]x1 + [1] = 6(9(x1))
                   [0 0 0]     [0]    [0 0 0]     [0]           
        
                   [2 0 1]     [2]    [2 0 1]     [2]           
        3(9(x1)) = [1 0 1]x1 + [2] >= [0 0 0]x1 + [0] = 9(3(x1))
                   [1 0 1]     [2]    [1 0 1]     [1]           
        
                   [1 1 0]     [1]    [1 1 0]     [1]           
        7(5(x1)) = [2 1 1]x1 + [1] >= [1 1 1]x1 + [1] = 1(0(x1))
                   [1 0 1]     [0]    [0 0 0]     [0]           
       problem:
        3(5(x1)) -> 8(9(7(x1)))
        2(6(x1)) -> 4(3(x1))
        9(x1) -> 5(0(2(x1)))
        7(1(x1)) -> 6(9(x1))
        3(9(x1)) -> 9(3(x1))
        7(5(x1)) -> 1(0(x1))
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [0](x0) = x0,
         
         [8](x0) = x0,
         
         [7](x0) = 1x0,
         
         [2](x0) = x0,
         
         [6](x0) = 1x0,
         
         [5](x0) = 1x0,
         
         [9](x0) = 1x0,
         
         [4](x0) = x0,
         
         [3](x0) = 1x0,
         
         [1](x0) = 2x0
        orientation:
         3(5(x1)) = 2x1 >= 2x1 = 8(9(7(x1)))
         
         2(6(x1)) = 1x1 >= 1x1 = 4(3(x1))
         
         9(x1) = 1x1 >= 1x1 = 5(0(2(x1)))
         
         7(1(x1)) = 3x1 >= 2x1 = 6(9(x1))
         
         3(9(x1)) = 2x1 >= 2x1 = 9(3(x1))
         
         7(5(x1)) = 2x1 >= 2x1 = 1(0(x1))
        problem:
         3(5(x1)) -> 8(9(7(x1)))
         2(6(x1)) -> 4(3(x1))
         9(x1) -> 5(0(2(x1)))
         3(9(x1)) -> 9(3(x1))
         7(5(x1)) -> 1(0(x1))
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [0](x0) = x0,
          
          [8](x0) = 1x0,
          
          [7](x0) = 3x0,
          
          [2](x0) = 10x0,
          
          [6](x0) = 6x0,
          
          [5](x0) = 1x0,
          
          [9](x0) = 11x0,
          
          [4](x0) = 2x0,
          
          [3](x0) = 14x0,
          
          [1](x0) = x0
         orientation:
          3(5(x1)) = 15x1 >= 15x1 = 8(9(7(x1)))
          
          2(6(x1)) = 16x1 >= 16x1 = 4(3(x1))
          
          9(x1) = 11x1 >= 11x1 = 5(0(2(x1)))
          
          3(9(x1)) = 25x1 >= 25x1 = 9(3(x1))
          
          7(5(x1)) = 4x1 >= x1 = 1(0(x1))
         problem:
          3(5(x1)) -> 8(9(7(x1)))
          2(6(x1)) -> 4(3(x1))
          9(x1) -> 5(0(2(x1)))
          3(9(x1)) -> 9(3(x1))
         Arctic Interpretation Processor:
          dimension: 2
          interpretation:
                     [0  -&]  
           [0](x0) = [-& -&]x0,
           
                     [0  0 ]  
           [8](x0) = [-& 0 ]x0,
           
                     [0  -&]  
           [7](x0) = [0  3 ]x0,
           
                     [0 0]  
           [2](x0) = [3 2]x0,
           
                     [0 1]  
           [6](x0) = [2 2]x0,
           
                     [0 3]  
           [5](x0) = [0 0]x0,
           
                     [0 0]  
           [9](x0) = [0 0]x0,
           
                       
           [4](x0) = x0,
           
                     [0  -&]  
           [3](x0) = [0  0 ]x0
          orientation:
                      [0 3]      [0 3]                
           3(5(x1)) = [0 3]x1 >= [0 3]x1 = 8(9(7(x1)))
           
                      [2 2]      [0  -&]             
           2(6(x1)) = [4 4]x1 >= [0  0 ]x1 = 4(3(x1))
           
                   [0 0]      [0 0]                
           9(x1) = [0 0]x1 >= [0 0]x1 = 5(0(2(x1)))
           
                      [0 0]      [0 0]             
           3(9(x1)) = [0 0]x1 >= [0 0]x1 = 9(3(x1))
          problem:
           3(5(x1)) -> 8(9(7(x1)))
           9(x1) -> 5(0(2(x1)))
           3(9(x1)) -> 9(3(x1))
          Arctic Interpretation Processor:
           dimension: 1
           interpretation:
            [0](x0) = x0,
            
            [8](x0) = 6x0,
            
            [7](x0) = 1x0,
            
            [2](x0) = x0,
            
            [5](x0) = 1x0,
            
            [9](x0) = 1x0,
            
            [3](x0) = 8x0
           orientation:
            3(5(x1)) = 9x1 >= 8x1 = 8(9(7(x1)))
            
            9(x1) = 1x1 >= 1x1 = 5(0(2(x1)))
            
            3(9(x1)) = 9x1 >= 9x1 = 9(3(x1))
           problem:
            9(x1) -> 5(0(2(x1)))
            3(9(x1)) -> 9(3(x1))
           Arctic Interpretation Processor:
            dimension: 2
            interpretation:
                       [0  0 ]  
             [0](x0) = [0  -&]x0,
             
                       [0  -&]  
             [2](x0) = [0  -&]x0,
             
                       [0 0]  
             [5](x0) = [0 0]x0,
             
                       [1 0]  
             [9](x0) = [1 2]x0,
             
                       [0 0]  
             [3](x0) = [0 2]x0
            orientation:
                     [1 0]      [0  -&]                
             9(x1) = [1 2]x1 >= [0  -&]x1 = 5(0(2(x1)))
             
                        [1 2]      [1 2]             
             3(9(x1)) = [3 4]x1 >= [2 4]x1 = 9(3(x1))
            problem:
             3(9(x1)) -> 9(3(x1))
            KBO Processor:
             weight function:
              w0 = 1
              w(9) = w(3) = 1
             precedence:
              3 > 9
             problem:
              
             Qed