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))
     Arctic Interpretation Processor:
      dimension: 2
      interpretation:
                 [0  -&]  
       [0](x0) = [0  -&]x0,
       
                 [0  -&]  
       [8](x0) = [0  3 ]x0,
       
                 [0 0]  
       [7](x0) = [1 0]x0,
       
                 [0 0]  
       [2](x0) = [0 0]x0,
       
                 [0  -&]  
       [6](x0) = [3  3 ]x0,
       
                 [0  -&]  
       [5](x0) = [0  1 ]x0,
       
                 [0  -&]  
       [9](x0) = [0  -&]x0,
       
                   
       [4](x0) = x0,
       
                 [0 0]  
       [3](x0) = [0 0]x0,
       
                 [0 0]  
       [1](x0) = [0 0]x0
      orientation:
                  [0 0]      [0  -&]                
       5(3(x1)) = [1 1]x1 >= [1  -&]x1 = 7(9(8(x1)))
       
                  [0 0]      [0 0]             
       6(2(x1)) = [3 3]x1 >= [0 0]x1 = 3(4(x1))
       
                  [0 0]      [0 0]                
       8(3(x1)) = [3 3]x1 >= [1 1]x1 = 7(2(3(x1)))
       
               [0  -&]      [0  -&]                
       9(x1) = [0  -&]x1 >= [0  -&]x1 = 2(0(5(x1)))
       
                  [1 0]      [0  -&]             
       1(7(x1)) = [1 0]x1 >= [0  -&]x1 = 9(6(x1))
       
                  [0 0]      [0  -&]             
       9(3(x1)) = [0 0]x1 >= [0  -&]x1 = 3(9(x1))
       
                  [0 0]      [0 0]             
       5(7(x1)) = [2 1]x1 >= [0 0]x1 = 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)))
       9(3(x1)) -> 3(9(x1))
       5(7(x1)) -> 0(1(x1))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [0](x0) = x0,
        
        [8](x0) = 6x0,
        
        [7](x0) = 6x0,
        
        [2](x0) = x0,
        
        [6](x0) = 14x0,
        
        [5](x0) = 8x0,
        
        [9](x0) = 8x0,
        
        [4](x0) = 2x0,
        
        [3](x0) = 12x0,
        
        [1](x0) = x0
       orientation:
        5(3(x1)) = 20x1 >= 20x1 = 7(9(8(x1)))
        
        6(2(x1)) = 14x1 >= 14x1 = 3(4(x1))
        
        8(3(x1)) = 18x1 >= 18x1 = 7(2(3(x1)))
        
        9(x1) = 8x1 >= 8x1 = 2(0(5(x1)))
        
        9(3(x1)) = 20x1 >= 20x1 = 3(9(x1))
        
        5(7(x1)) = 14x1 >= x1 = 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)))
        9(3(x1)) -> 3(9(x1))
       Arctic Interpretation Processor:
        dimension: 2
        interpretation:
                   [0  0 ]  
         [0](x0) = [0  -&]x0,
         
                   [0 0]  
         [8](x0) = [0 0]x0,
         
                   [0  0 ]  
         [7](x0) = [-& 0 ]x0,
         
                     
         [2](x0) = x0,
         
                   [3  1 ]  
         [6](x0) = [2  -&]x0,
         
                   [0  -&]  
         [5](x0) = [0  0 ]x0,
         
                   [0  0 ]  
         [9](x0) = [0  -&]x0,
         
                   [2  0 ]  
         [4](x0) = [0  -&]x0,
         
                   [0  0 ]  
         [3](x0) = [-& 0 ]x0
        orientation:
                    [0 0]      [0 0]                
         5(3(x1)) = [0 0]x1 >= [0 0]x1 = 7(9(8(x1)))
         
                    [3  1 ]      [2  0 ]             
         6(2(x1)) = [2  -&]x1 >= [0  -&]x1 = 3(4(x1))
         
                    [0 0]      [0  0 ]                
         8(3(x1)) = [0 0]x1 >= [-& 0 ]x1 = 7(2(3(x1)))
         
                 [0  0 ]      [0  0 ]                
         9(x1) = [0  -&]x1 >= [0  -&]x1 = 2(0(5(x1)))
         
                    [0 0]      [0  0 ]             
         9(3(x1)) = [0 0]x1 >= [0  -&]x1 = 3(9(x1))
        problem:
         5(3(x1)) -> 7(9(8(x1)))
         8(3(x1)) -> 7(2(3(x1)))
         9(x1) -> 2(0(5(x1)))
         9(3(x1)) -> 3(9(x1))
        Arctic Interpretation Processor:
         dimension: 2
         interpretation:
                    [0  -&]  
          [0](x0) = [-& 1 ]x0,
          
                    [0  1 ]  
          [8](x0) = [-& 0 ]x0,
          
                    [0  0 ]  
          [7](x0) = [-& -&]x0,
          
                    [0 0]  
          [2](x0) = [0 0]x0,
          
                      
          [5](x0) = x0,
          
                    [0 1]  
          [9](x0) = [0 1]x0,
          
                    [0 1]  
          [3](x0) = [0 1]x0
         orientation:
                     [0 1]      [0  1 ]                
          5(3(x1)) = [0 1]x1 >= [-& -&]x1 = 7(9(8(x1)))
          
                     [1 2]      [0  1 ]                
          8(3(x1)) = [0 1]x1 >= [-& -&]x1 = 7(2(3(x1)))
          
                  [0 1]      [0 1]                
          9(x1) = [0 1]x1 >= [0 1]x1 = 2(0(5(x1)))
          
                     [1 2]      [1 2]             
          9(3(x1)) = [1 2]x1 >= [1 2]x1 = 3(9(x1))
         problem:
          5(3(x1)) -> 7(9(8(x1)))
          9(x1) -> 2(0(5(x1)))
          9(3(x1)) -> 3(9(x1))
         Arctic Interpretation Processor:
          dimension: 2
          interpretation:
                     [0  0 ]  
           [0](x0) = [-& 0 ]x0,
           
                     [0  0 ]  
           [8](x0) = [-& -&]x0,
           
                     [0 3]  
           [7](x0) = [0 3]x0,
           
                     [0  0 ]  
           [2](x0) = [-& -&]x0,
           
                     [0  -&]  
           [5](x0) = [0  2 ]x0,
           
                     [0  2 ]  
           [9](x0) = [-& 0 ]x0,
           
                     [1  3 ]  
           [3](x0) = [-& 0 ]x0
          orientation:
                      [1 3]      [0 0]                
           5(3(x1)) = [1 3]x1 >= [0 0]x1 = 7(9(8(x1)))
           
                   [0  2 ]      [0  2 ]                
           9(x1) = [-& 0 ]x1 >= [-& -&]x1 = 2(0(5(x1)))
           
                      [1  3 ]      [1  3 ]             
           9(3(x1)) = [-& 0 ]x1 >= [-& 0 ]x1 = 3(9(x1))
          problem:
           9(x1) -> 2(0(5(x1)))
           9(3(x1)) -> 3(9(x1))
          Arctic Interpretation Processor:
           dimension: 2
           interpretation:
                      [0  -&]  
            [0](x0) = [1  0 ]x0,
            
                      [0  -&]  
            [2](x0) = [0  -&]x0,
            
                      [0  -&]  
            [5](x0) = [0  3 ]x0,
            
                      [1 0]  
            [9](x0) = [1 0]x0,
            
                      [0  0 ]  
            [3](x0) = [-& 0 ]x0
           orientation:
                    [1 0]      [0  -&]                
            9(x1) = [1 0]x1 >= [0  -&]x1 = 2(0(5(x1)))
            
                       [1 1]      [1 0]             
            9(3(x1)) = [1 1]x1 >= [1 0]x1 = 3(9(x1))
           problem:
            9(3(x1)) -> 3(9(x1))
           KBO Processor:
            weight function:
             w0 = 1
             w(9) = w(3) = 1
            precedence:
             9 > 3
            problem:
             
            Qed