YES

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:
 String Reversal Processor:
  7(2(x1)) -> 8(1(x1))
  1(8(2(x1))) -> 8(x1)
  8(2(x1)) -> 4(x1)
  9(5(x1)) -> 0(x1)
  4(x1) -> 3(2(5(x1)))
  3(5(x1)) -> 0(6(x1))
  8(2(x1)) -> 7(x1)
  7(4(x1)) -> 3(1(x1))
  6(2(5(x1))) -> 4(2(6(x1)))
  7(9(x1)) -> 5(7(x1))
  2(7(x1)) -> 4(x1)
  0(7(x1)) -> 3(9(x1))
  9(6(x1)) -> 9(x1)
  9(5(9(x1))) -> 7(5(x1))
  4(x1) -> 6(6(9(x1)))
  9(x1) -> 7(6(x1))
  2(6(x1)) -> 7(7(x1))
  4(2(x1)) -> 7(0(x1))
  6(6(x1)) -> 3(x1)
  3(0(x1)) -> 3(5(x1))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 0]  
    [6](x0) = [0 1 0]x0
              [0 0 0]  ,
    
              [1 0 0]  
    [3](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 0 0]  
    [0](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 0 0]  
    [5](x0) = [0 0 0]x0
              [0 1 0]  ,
    
              [1 1 0]  
    [9](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 1 0]  
    [4](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 1 0]     [0]
    [1](x0) = [0 1 0]x0 + [1]
              [0 0 0]     [0],
    
              [1 0 0]  
    [8](x0) = [0 0 1]x0
              [0 0 0]  ,
    
              [1 1 1]     [0]
    [2](x0) = [0 0 1]x0 + [0]
              [0 0 1]     [1],
    
              [1 1 0]  
    [7](x0) = [0 0 0]x0
              [0 0 0]  
   orientation:
               [1 1 2]      [1 1 0]             
    7(2(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 8(1(x1))
               [0 0 0]      [0 0 0]             
    
                  [1 1 2]     [1]    [1 0 0]          
    1(8(2(x1))) = [0 0 1]x1 + [2] >= [0 0 1]x1 = 8(x1)
                  [0 0 0]     [0]    [0 0 0]          
    
               [1 1 1]     [0]    [1 1 0]          
    8(2(x1)) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 4(x1)
               [0 0 0]     [0]    [0 0 0]          
    
               [1 0 0]      [1 0 0]          
    9(5(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(x1)
               [0 0 0]      [0 0 0]          
    
            [1 1 0]      [1 1 0]                
    4(x1) = [0 0 0]x1 >= [0 0 0]x1 = 3(2(5(x1)))
            [0 0 0]      [0 0 0]                
    
               [1 0 0]      [1 0 0]             
    3(5(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(6(x1))
               [0 0 0]      [0 0 0]             
    
               [1 1 1]     [0]    [1 1 0]          
    8(2(x1)) = [0 0 1]x1 + [1] >= [0 0 0]x1 = 7(x1)
               [0 0 0]     [0]    [0 0 0]          
    
               [1 1 0]      [1 1 0]             
    7(4(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(1(x1))
               [0 0 0]      [0 0 0]             
    
                  [1 1 0]      [1 1 0]                
    6(2(5(x1))) = [0 1 0]x1 >= [0 0 0]x1 = 4(2(6(x1)))
                  [0 0 0]      [0 0 0]                
    
               [1 1 0]      [1 1 0]             
    7(9(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 5(7(x1))
               [0 0 0]      [0 0 0]             
    
               [1 1 0]     [0]    [1 1 0]          
    2(7(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 4(x1)
               [0 0 0]     [1]    [0 0 0]          
    
               [1 1 0]      [1 1 0]             
    0(7(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(9(x1))
               [0 0 0]      [0 0 0]             
    
               [1 1 0]      [1 1 0]          
    9(6(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 9(x1)
               [0 0 0]      [0 0 0]          
    
                  [1 1 0]      [1 0 0]             
    9(5(9(x1))) = [0 0 0]x1 >= [0 0 0]x1 = 7(5(x1))
                  [0 0 0]      [0 0 0]             
    
            [1 1 0]      [1 1 0]                
    4(x1) = [0 0 0]x1 >= [0 0 0]x1 = 6(6(9(x1)))
            [0 0 0]      [0 0 0]                
    
            [1 1 0]      [1 1 0]             
    9(x1) = [0 0 0]x1 >= [0 0 0]x1 = 7(6(x1))
            [0 0 0]      [0 0 0]             
    
               [1 1 0]     [0]    [1 1 0]             
    2(6(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 7(7(x1))
               [0 0 0]     [1]    [0 0 0]             
    
               [1 1 2]      [1 0 0]             
    4(2(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 7(0(x1))
               [0 0 0]      [0 0 0]             
    
               [1 0 0]      [1 0 0]          
    6(6(x1)) = [0 1 0]x1 >= [0 0 0]x1 = 3(x1)
               [0 0 0]      [0 0 0]          
    
               [1 0 0]      [1 0 0]             
    3(0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(x1))
               [0 0 0]      [0 0 0]             
   problem:
    7(2(x1)) -> 8(1(x1))
    8(2(x1)) -> 4(x1)
    9(5(x1)) -> 0(x1)
    4(x1) -> 3(2(5(x1)))
    3(5(x1)) -> 0(6(x1))
    8(2(x1)) -> 7(x1)
    7(4(x1)) -> 3(1(x1))
    6(2(5(x1))) -> 4(2(6(x1)))
    7(9(x1)) -> 5(7(x1))
    2(7(x1)) -> 4(x1)
    0(7(x1)) -> 3(9(x1))
    9(6(x1)) -> 9(x1)
    9(5(9(x1))) -> 7(5(x1))
    4(x1) -> 6(6(9(x1)))
    9(x1) -> 7(6(x1))
    2(6(x1)) -> 7(7(x1))
    4(2(x1)) -> 7(0(x1))
    6(6(x1)) -> 3(x1)
    3(0(x1)) -> 3(5(x1))
   String Reversal Processor:
    2(7(x1)) -> 1(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))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                [1 0 0]     [0]
      [6](x0) = [1 0 0]x0 + [1]
                [1 0 0]     [1],
      
                [1 0 0]  
      [3](x0) = [0 0 0]x0
                [0 0 0]  ,
      
                [1 0 0]     [0]
      [0](x0) = [1 0 0]x0 + [1]
                [1 0 0]     [1],
      
                [1 0 0]     [0]
      [5](x0) = [1 0 0]x0 + [1]
                [1 0 0]     [1],
      
                [1 0 0]     [0]
      [9](x0) = [1 0 0]x0 + [1]
                [1 0 0]     [1],
      
                [1 0 0]     [0]
      [4](x0) = [1 0 0]x0 + [1]
                [1 0 0]     [1],
      
                [1 0 0]     [0]
      [1](x0) = [0 0 0]x0 + [0]
                [0 1 0]     [1],
      
                [1 0 1]     [0]
      [8](x0) = [1 0 0]x0 + [0]
                [1 1 1]     [1],
      
                [1 1 1]     [0]
      [2](x0) = [0 0 1]x0 + [0]
                [1 0 0]     [1],
      
                [1 0 0]  
      [7](x0) = [0 0 1]x0
                [0 0 1]  
     orientation:
                 [1 0 2]     [0]    [1 0 1]     [0]           
      2(7(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 1(8(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [3 1 2]     [1]    [1 0 0]     [0]        
      2(8(x1)) = [1 1 1]x1 + [1] >= [1 0 0]x1 + [1] = 4(x1)
                 [1 0 1]     [1]    [1 0 0]     [1]        
      
                 [1 0 0]     [0]    [1 0 0]     [0]        
      5(9(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 0(x1)
                 [1 0 0]     [1]    [1 0 0]     [1]        
      
              [1 0 0]     [0]    [1 0 0]     [0]              
      4(x1) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 5(2(3(x1)))
              [1 0 0]     [1]    [1 0 0]     [1]              
      
                 [1 0 0]     [0]    [1 0 0]     [0]           
      5(3(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 6(0(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [3 1 2]     [1]    [1 0 0]          
      2(8(x1)) = [1 1 1]x1 + [1] >= [0 0 1]x1 = 7(x1)
                 [1 0 1]     [1]    [0 0 1]          
      
                 [1 0 0]     [0]    [1 0 0]     [0]           
      4(7(x1)) = [1 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1(3(x1))
                 [1 0 0]     [1]    [0 0 0]     [1]           
      
                    [3 0 0]     [2]    [3 0 0]     [2]              
      5(2(6(x1))) = [3 0 0]x1 + [3] >= [3 0 0]x1 + [3] = 6(2(4(x1)))
                    [3 0 0]     [3]    [3 0 0]     [3]              
      
                 [1 0 0]     [0]    [1 0 0]     [0]           
      9(7(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 7(5(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [1 1 1]     [0]    [1 0 0]     [0]        
      7(2(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 4(x1)
                 [1 0 0]     [1]    [1 0 0]     [1]        
      
                 [1 0 0]     [0]    [1 0 0]     [0]           
      7(0(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 9(3(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [1 0 0]     [0]    [1 0 0]     [0]        
      6(9(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 9(x1)
                 [1 0 0]     [1]    [1 0 0]     [1]        
      
                    [1 0 0]     [0]    [1 0 0]     [0]           
      9(5(9(x1))) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 5(7(x1))
                    [1 0 0]     [1]    [1 0 0]     [1]           
      
              [1 0 0]     [0]    [1 0 0]     [0]              
      4(x1) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 9(6(6(x1)))
              [1 0 0]     [1]    [1 0 0]     [1]              
      
              [1 0 0]     [0]    [1 0 0]     [0]           
      9(x1) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 6(7(x1))
              [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [1 1 1]     [0]    [1 0 0]             
      6(2(x1)) = [1 1 1]x1 + [1] >= [0 0 1]x1 = 7(7(x1))
                 [1 1 1]     [1]    [0 0 1]             
      
                 [3 0 0]     [2]    [1 0 0]     [0]           
      2(4(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 0(7(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
      
                 [1 0 0]     [0]    [1 0 0]          
      6(6(x1)) = [1 0 0]x1 + [1] >= [0 0 0]x1 = 3(x1)
                 [1 0 0]     [1]    [0 0 0]          
      
                 [1 0 0]     [0]    [1 0 0]     [0]           
      0(3(x1)) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = 5(3(x1))
                 [1 0 0]     [1]    [1 0 0]     [1]           
     problem:
      2(7(x1)) -> 1(8(x1))
      5(9(x1)) -> 0(x1)
      4(x1) -> 5(2(3(x1)))
      5(3(x1)) -> 6(0(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))
      6(6(x1)) -> 3(x1)
      0(3(x1)) -> 5(3(x1))
     String Reversal Processor:
      7(2(x1)) -> 8(1(x1))
      9(5(x1)) -> 0(x1)
      4(x1) -> 3(2(5(x1)))
      3(5(x1)) -> 0(6(x1))
      7(4(x1)) -> 3(1(x1))
      6(2(5(x1))) -> 4(2(6(x1)))
      7(9(x1)) -> 5(7(x1))
      2(7(x1)) -> 4(x1)
      0(7(x1)) -> 3(9(x1))
      9(6(x1)) -> 9(x1)
      9(5(9(x1))) -> 7(5(x1))
      4(x1) -> 6(6(9(x1)))
      9(x1) -> 7(6(x1))
      2(6(x1)) -> 7(7(x1))
      6(6(x1)) -> 3(x1)
      3(0(x1)) -> 3(5(x1))
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                  [1 0 0]  
        [6](x0) = [0 0 0]x0
                  [0 0 0]  ,
        
                  [1 0 0]  
        [3](x0) = [0 0 0]x0
                  [0 0 0]  ,
        
                  [1 0 0]  
        [0](x0) = [0 0 0]x0
                  [0 0 0]  ,
        
                  [1 0 0]     [0]
        [5](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1],
        
                  [1 0 0]     [0]
        [9](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1],
        
                  [1 0 0]     [1]
        [4](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [0],
        
                  [1 0 0]     [0]
        [1](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1],
        
                  [1 0 0]  
        [8](x0) = [0 0 0]x0
                  [0 0 1]  ,
        
                  [1 0 1]     [0]
        [2](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1],
        
                  [1 0 0]     [0]
        [7](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1]
       orientation:
                   [1 0 1]     [0]    [1 0 0]     [0]           
        7(2(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 8(1(x1))
                   [0 0 0]     [1]    [0 0 0]     [1]           
        
                   [1 0 0]     [0]    [1 0 0]          
        9(5(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0(x1)
                   [0 0 0]     [1]    [0 0 0]          
        
                [1 0 0]     [1]    [1 0 0]     [1]              
        4(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 3(2(5(x1)))
                [0 0 0]     [0]    [0 0 0]     [0]              
        
                   [1 0 0]      [1 0 0]             
        3(5(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 0(6(x1))
                   [0 0 0]      [0 0 0]             
        
                   [1 0 0]     [1]    [1 0 0]             
        7(4(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 3(1(x1))
                   [0 0 0]     [1]    [0 0 0]             
        
                      [1 0 0]     [1]    [1 0 0]     [1]              
        6(2(5(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(2(6(x1)))
                      [0 0 0]     [0]    [0 0 0]     [0]              
        
                   [1 0 0]     [0]    [1 0 0]     [0]           
        7(9(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(7(x1))
                   [0 0 0]     [1]    [0 0 0]     [1]           
        
                   [1 0 0]     [1]    [1 0 0]     [1]        
        2(7(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(x1)
                   [0 0 0]     [1]    [0 0 0]     [0]        
        
                   [1 0 0]      [1 0 0]             
        0(7(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(9(x1))
                   [0 0 0]      [0 0 0]             
        
                   [1 0 0]     [0]    [1 0 0]     [0]        
        9(6(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 9(x1)
                   [0 0 0]     [1]    [0 0 0]     [1]        
        
                      [1 0 0]     [0]    [1 0 0]     [0]           
        9(5(9(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 7(5(x1))
                      [0 0 0]     [1]    [0 0 0]     [1]           
        
                [1 0 0]     [1]    [1 0 0]                
        4(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 6(6(9(x1)))
                [0 0 0]     [0]    [0 0 0]                
        
                [1 0 0]     [0]    [1 0 0]     [0]           
        9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 7(6(x1))
                [0 0 0]     [1]    [0 0 0]     [1]           
        
                   [1 0 0]     [0]    [1 0 0]     [0]           
        2(6(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 7(7(x1))
                   [0 0 0]     [1]    [0 0 0]     [1]           
        
                   [1 0 0]      [1 0 0]          
        6(6(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(x1)
                   [0 0 0]      [0 0 0]          
        
                   [1 0 0]      [1 0 0]             
        3(0(x1)) = [0 0 0]x1 >= [0 0 0]x1 = 3(5(x1))
                   [0 0 0]      [0 0 0]             
       problem:
        7(2(x1)) -> 8(1(x1))
        9(5(x1)) -> 0(x1)
        4(x1) -> 3(2(5(x1)))
        3(5(x1)) -> 0(6(x1))
        6(2(5(x1))) -> 4(2(6(x1)))
        7(9(x1)) -> 5(7(x1))
        2(7(x1)) -> 4(x1)
        0(7(x1)) -> 3(9(x1))
        9(6(x1)) -> 9(x1)
        9(5(9(x1))) -> 7(5(x1))
        9(x1) -> 7(6(x1))
        2(6(x1)) -> 7(7(x1))
        6(6(x1)) -> 3(x1)
        3(0(x1)) -> 3(5(x1))
       String Reversal Processor:
        2(7(x1)) -> 1(8(x1))
        5(9(x1)) -> 0(x1)
        4(x1) -> 5(2(3(x1)))
        5(3(x1)) -> 6(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)
        0(3(x1)) -> 5(3(x1))
        Bounds Processor:
         bound: 2
         enrichment: match
         automaton:
          final states: {20,6,19,18,16,15,14,10,12,9,8,5,4,1}
          transitions:
           f100() -> 2*
           10(3) -> 1*
           80(2) -> 3*
           00(2) -> 4*
           50(17) -> 16*
           50(7) -> 5*
           50(2) -> 13*
           50(6) -> 20*
           20(10) -> 11*
           20(6) -> 7*
           30(2) -> 6*
           60(17) -> 18*
           60(4) -> 8*
           60(11) -> 9*
           40(2) -> 10*
           70(17) -> 19*
           70(2) -> 17*
           70(13) -> 12*
           90(2) -> 15*
           90(6) -> 14*
           71(50) -> 51*
           71(51) -> 52*
           71(41) -> 42*
           71(38) -> 39*
           61(30) -> 31*
           61(42) -> 43*
           61(39) -> 40*
           01(29) -> 30*
           01(63) -> 64*
           51(27) -> 28*
           51(83) -> 84*
           21(26) -> 27*
           31(95) -> 96*
           31(25) -> 26*
           31(71) -> 72*
           91(55) -> 56*
           91(69) -> 70*
           62(89) -> 90*
           62(79) -> 80*
           62(58) -> 59*
           72(57) -> 58*
           72(78) -> 79*
           02(88) -> 89*
           32(99) -> 100*
           32(91) -> 92*
           2 -> 41,29,25
           4 -> 13*
           6 -> 69,63,38
           8 -> 13*
           9 -> 13*
           10 -> 42,17,50
           12 -> 15*
           14 -> 42,17
           16 -> 15*
           20 -> 89,30,4
           25 -> 88*
           26 -> 83,55
           28 -> 10*
           30 -> 99,95
           31 -> 20*
           39 -> 91,71
           40 -> 14*
           43 -> 15*
           52 -> 9*
           55 -> 57*
           56 -> 12*
           59 -> 56,12
           64 -> 16*
           69 -> 78*
           70 -> 43,15,18
           72 -> 18*
           80 -> 70,18
           84 -> 64,16
           90 -> 84,64
           92 -> 43,15
           96 -> 8*
           100 -> 90,84,64,16,31,20,4,95
         problem:
          
         Qed