YES

Problem:
 a12(a12(x1)) -> x1
 a13(a13(x1)) -> x1
 a14(a14(x1)) -> x1
 a15(a15(x1)) -> x1
 a16(a16(x1)) -> x1
 a23(a23(x1)) -> x1
 a24(a24(x1)) -> x1
 a25(a25(x1)) -> x1
 a26(a26(x1)) -> x1
 a34(a34(x1)) -> x1
 a35(a35(x1)) -> x1
 a36(a36(x1)) -> x1
 a45(a45(x1)) -> x1
 a46(a46(x1)) -> x1
 a56(a56(x1)) -> x1
 a13(x1) -> a12(a23(a12(x1)))
 a14(x1) -> a12(a23(a34(a23(a12(x1)))))
 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
 a24(x1) -> a23(a34(a23(x1)))
 a25(x1) -> a23(a34(a45(a34(a23(x1)))))
 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
 a35(x1) -> a34(a45(a34(x1)))
 a36(x1) -> a34(a45(a56(a45(a34(x1)))))
 a46(x1) -> a45(a56(a45(x1)))
 a12(a23(a12(a23(a12(a23(x1)))))) -> x1
 a23(a34(a23(a34(a23(a34(x1)))))) -> x1
 a34(a45(a34(a45(a34(a45(x1)))))) -> x1
 a45(a56(a45(a56(a45(a56(x1)))))) -> x1
 a12(a34(x1)) -> a34(a12(x1))
 a12(a45(x1)) -> a45(a12(x1))
 a12(a56(x1)) -> a56(a12(x1))
 a23(a45(x1)) -> a45(a23(x1))
 a23(a56(x1)) -> a56(a23(x1))
 a34(a56(x1)) -> a56(a34(x1))

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [a56](x0) = x0,
   
   [a46](x0) = 8x0,
   
   [a45](x0) = 4x0,
   
   [a36](x0) = 8x0,
   
   [a35](x0) = 4x0,
   
   [a34](x0) = x0,
   
   [a26](x0) = 8x0,
   
   [a25](x0) = 10x0,
   
   [a24](x0) = 8x0,
   
   [a23](x0) = x0,
   
   [a16](x0) = 8x0,
   
   [a15](x0) = 9x0,
   
   [a14](x0) = x0,
   
   [a13](x0) = x0,
   
   [a12](x0) = x0
  orientation:
   a12(a12(x1)) = x1 >= x1 = x1
   
   a13(a13(x1)) = x1 >= x1 = x1
   
   a14(a14(x1)) = x1 >= x1 = x1
   
   a15(a15(x1)) = 18x1 >= x1 = x1
   
   a16(a16(x1)) = 16x1 >= x1 = x1
   
   a23(a23(x1)) = x1 >= x1 = x1
   
   a24(a24(x1)) = 16x1 >= x1 = x1
   
   a25(a25(x1)) = 20x1 >= x1 = x1
   
   a26(a26(x1)) = 16x1 >= x1 = x1
   
   a34(a34(x1)) = x1 >= x1 = x1
   
   a35(a35(x1)) = 8x1 >= x1 = x1
   
   a36(a36(x1)) = 16x1 >= x1 = x1
   
   a45(a45(x1)) = 8x1 >= x1 = x1
   
   a46(a46(x1)) = 16x1 >= x1 = x1
   
   a56(a56(x1)) = x1 >= x1 = x1
   
   a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
   
   a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
   
   a15(x1) = 9x1 >= 4x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
   
   a16(x1) = 8x1 >= 8x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
   
   a24(x1) = 8x1 >= x1 = a23(a34(a23(x1)))
   
   a25(x1) = 10x1 >= 4x1 = a23(a34(a45(a34(a23(x1)))))
   
   a26(x1) = 8x1 >= 8x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
   
   a35(x1) = 4x1 >= 4x1 = a34(a45(a34(x1)))
   
   a36(x1) = 8x1 >= 8x1 = a34(a45(a56(a45(a34(x1)))))
   
   a46(x1) = 8x1 >= 8x1 = a45(a56(a45(x1)))
   
   a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
   
   a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
   
   a34(a45(a34(a45(a34(a45(x1)))))) = 12x1 >= x1 = x1
   
   a45(a56(a45(a56(a45(a56(x1)))))) = 12x1 >= x1 = x1
   
   a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
   
   a12(a45(x1)) = 4x1 >= 4x1 = a45(a12(x1))
   
   a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
   
   a23(a45(x1)) = 4x1 >= 4x1 = a45(a23(x1))
   
   a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
   
   a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
  problem:
   a12(a12(x1)) -> x1
   a13(a13(x1)) -> x1
   a14(a14(x1)) -> x1
   a23(a23(x1)) -> x1
   a34(a34(x1)) -> x1
   a56(a56(x1)) -> x1
   a13(x1) -> a12(a23(a12(x1)))
   a14(x1) -> a12(a23(a34(a23(a12(x1)))))
   a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
   a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
   a35(x1) -> a34(a45(a34(x1)))
   a36(x1) -> a34(a45(a56(a45(a34(x1)))))
   a46(x1) -> a45(a56(a45(x1)))
   a12(a23(a12(a23(a12(a23(x1)))))) -> x1
   a23(a34(a23(a34(a23(a34(x1)))))) -> x1
   a12(a34(x1)) -> a34(a12(x1))
   a12(a45(x1)) -> a45(a12(x1))
   a12(a56(x1)) -> a56(a12(x1))
   a23(a45(x1)) -> a45(a23(x1))
   a23(a56(x1)) -> a56(a23(x1))
   a34(a56(x1)) -> a56(a34(x1))
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [a56](x0) = x0,
    
    [a46](x0) = 6x0,
    
    [a45](x0) = x0,
    
    [a36](x0) = 14x0,
    
    [a35](x0) = 14x0,
    
    [a34](x0) = 7x0,
    
    [a26](x0) = 14x0,
    
    [a23](x0) = x0,
    
    [a16](x0) = 14x0,
    
    [a14](x0) = 7x0,
    
    [a13](x0) = x0,
    
    [a12](x0) = x0
   orientation:
    a12(a12(x1)) = x1 >= x1 = x1
    
    a13(a13(x1)) = x1 >= x1 = x1
    
    a14(a14(x1)) = 14x1 >= x1 = x1
    
    a23(a23(x1)) = x1 >= x1 = x1
    
    a34(a34(x1)) = 14x1 >= x1 = x1
    
    a56(a56(x1)) = x1 >= x1 = x1
    
    a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
    
    a14(x1) = 7x1 >= 7x1 = a12(a23(a34(a23(a12(x1)))))
    
    a16(x1) = 14x1 >= 14x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
    
    a26(x1) = 14x1 >= 14x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
    
    a35(x1) = 14x1 >= 14x1 = a34(a45(a34(x1)))
    
    a36(x1) = 14x1 >= 14x1 = a34(a45(a56(a45(a34(x1)))))
    
    a46(x1) = 6x1 >= x1 = a45(a56(a45(x1)))
    
    a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
    
    a23(a34(a23(a34(a23(a34(x1)))))) = 21x1 >= x1 = x1
    
    a12(a34(x1)) = 7x1 >= 7x1 = a34(a12(x1))
    
    a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
    
    a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
    
    a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
    
    a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
    
    a34(a56(x1)) = 7x1 >= 7x1 = a56(a34(x1))
   problem:
    a12(a12(x1)) -> x1
    a13(a13(x1)) -> x1
    a23(a23(x1)) -> x1
    a56(a56(x1)) -> x1
    a13(x1) -> a12(a23(a12(x1)))
    a14(x1) -> a12(a23(a34(a23(a12(x1)))))
    a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
    a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
    a35(x1) -> a34(a45(a34(x1)))
    a36(x1) -> a34(a45(a56(a45(a34(x1)))))
    a12(a23(a12(a23(a12(a23(x1)))))) -> x1
    a12(a34(x1)) -> a34(a12(x1))
    a12(a45(x1)) -> a45(a12(x1))
    a12(a56(x1)) -> a56(a12(x1))
    a23(a45(x1)) -> a45(a23(x1))
    a23(a56(x1)) -> a56(a23(x1))
    a34(a56(x1)) -> a56(a34(x1))
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [a56](x0) = 1x0,
     
     [a45](x0) = 5x0,
     
     [a36](x0) = 11x0,
     
     [a35](x0) = 5x0,
     
     [a34](x0) = x0,
     
     [a26](x0) = 11x0,
     
     [a23](x0) = x0,
     
     [a16](x0) = 11x0,
     
     [a14](x0) = x0,
     
     [a13](x0) = x0,
     
     [a12](x0) = x0
    orientation:
     a12(a12(x1)) = x1 >= x1 = x1
     
     a13(a13(x1)) = x1 >= x1 = x1
     
     a23(a23(x1)) = x1 >= x1 = x1
     
     a56(a56(x1)) = 2x1 >= x1 = x1
     
     a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
     
     a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
     
     a16(x1) = 11x1 >= 11x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
     
     a26(x1) = 11x1 >= 11x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
     
     a35(x1) = 5x1 >= 5x1 = a34(a45(a34(x1)))
     
     a36(x1) = 11x1 >= 11x1 = a34(a45(a56(a45(a34(x1)))))
     
     a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
     
     a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
     
     a12(a45(x1)) = 5x1 >= 5x1 = a45(a12(x1))
     
     a12(a56(x1)) = 1x1 >= 1x1 = a56(a12(x1))
     
     a23(a45(x1)) = 5x1 >= 5x1 = a45(a23(x1))
     
     a23(a56(x1)) = 1x1 >= 1x1 = a56(a23(x1))
     
     a34(a56(x1)) = 1x1 >= 1x1 = a56(a34(x1))
    problem:
     a12(a12(x1)) -> x1
     a13(a13(x1)) -> x1
     a23(a23(x1)) -> x1
     a13(x1) -> a12(a23(a12(x1)))
     a14(x1) -> a12(a23(a34(a23(a12(x1)))))
     a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
     a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
     a35(x1) -> a34(a45(a34(x1)))
     a36(x1) -> a34(a45(a56(a45(a34(x1)))))
     a12(a23(a12(a23(a12(a23(x1)))))) -> x1
     a12(a34(x1)) -> a34(a12(x1))
     a12(a45(x1)) -> a45(a12(x1))
     a12(a56(x1)) -> a56(a12(x1))
     a23(a45(x1)) -> a45(a23(x1))
     a23(a56(x1)) -> a56(a23(x1))
     a34(a56(x1)) -> a56(a34(x1))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [a56](x0) = 1x0,
      
      [a45](x0) = x0,
      
      [a36](x0) = 1x0,
      
      [a35](x0) = x0,
      
      [a34](x0) = x0,
      
      [a26](x0) = 3x0,
      
      [a23](x0) = 1x0,
      
      [a16](x0) = 3x0,
      
      [a14](x0) = 2x0,
      
      [a13](x0) = 1x0,
      
      [a12](x0) = x0
     orientation:
      a12(a12(x1)) = x1 >= x1 = x1
      
      a13(a13(x1)) = 2x1 >= x1 = x1
      
      a23(a23(x1)) = 2x1 >= x1 = x1
      
      a13(x1) = 1x1 >= 1x1 = a12(a23(a12(x1)))
      
      a14(x1) = 2x1 >= 2x1 = a12(a23(a34(a23(a12(x1)))))
      
      a16(x1) = 3x1 >= 3x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
      
      a26(x1) = 3x1 >= 3x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
      
      a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
      
      a36(x1) = 1x1 >= 1x1 = a34(a45(a56(a45(a34(x1)))))
      
      a12(a23(a12(a23(a12(a23(x1)))))) = 3x1 >= x1 = x1
      
      a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
      
      a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
      
      a12(a56(x1)) = 1x1 >= 1x1 = a56(a12(x1))
      
      a23(a45(x1)) = 1x1 >= 1x1 = a45(a23(x1))
      
      a23(a56(x1)) = 2x1 >= 2x1 = a56(a23(x1))
      
      a34(a56(x1)) = 1x1 >= 1x1 = a56(a34(x1))
     problem:
      a12(a12(x1)) -> x1
      a13(x1) -> a12(a23(a12(x1)))
      a14(x1) -> a12(a23(a34(a23(a12(x1)))))
      a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
      a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
      a35(x1) -> a34(a45(a34(x1)))
      a36(x1) -> a34(a45(a56(a45(a34(x1)))))
      a12(a34(x1)) -> a34(a12(x1))
      a12(a45(x1)) -> a45(a12(x1))
      a12(a56(x1)) -> a56(a12(x1))
      a23(a45(x1)) -> a45(a23(x1))
      a23(a56(x1)) -> a56(a23(x1))
      a34(a56(x1)) -> a56(a34(x1))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [a56](x0) = 2x0,
       
       [a45](x0) = x0,
       
       [a36](x0) = 4x0,
       
       [a35](x0) = 2x0,
       
       [a34](x0) = 1x0,
       
       [a26](x0) = 8x0,
       
       [a23](x0) = x0,
       
       [a16](x0) = 6x0,
       
       [a14](x0) = 3x0,
       
       [a13](x0) = 2x0,
       
       [a12](x0) = 1x0
      orientation:
       a12(a12(x1)) = 2x1 >= x1 = x1
       
       a13(x1) = 2x1 >= 2x1 = a12(a23(a12(x1)))
       
       a14(x1) = 3x1 >= 3x1 = a12(a23(a34(a23(a12(x1)))))
       
       a16(x1) = 6x1 >= 6x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
       
       a26(x1) = 8x1 >= 4x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
       
       a35(x1) = 2x1 >= 2x1 = a34(a45(a34(x1)))
       
       a36(x1) = 4x1 >= 4x1 = a34(a45(a56(a45(a34(x1)))))
       
       a12(a34(x1)) = 2x1 >= 2x1 = a34(a12(x1))
       
       a12(a45(x1)) = 1x1 >= 1x1 = a45(a12(x1))
       
       a12(a56(x1)) = 3x1 >= 3x1 = a56(a12(x1))
       
       a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
       
       a23(a56(x1)) = 2x1 >= 2x1 = a56(a23(x1))
       
       a34(a56(x1)) = 3x1 >= 3x1 = a56(a34(x1))
      problem:
       a13(x1) -> a12(a23(a12(x1)))
       a14(x1) -> a12(a23(a34(a23(a12(x1)))))
       a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
       a35(x1) -> a34(a45(a34(x1)))
       a36(x1) -> a34(a45(a56(a45(a34(x1)))))
       a12(a34(x1)) -> a34(a12(x1))
       a12(a45(x1)) -> a45(a12(x1))
       a12(a56(x1)) -> a56(a12(x1))
       a23(a45(x1)) -> a45(a23(x1))
       a23(a56(x1)) -> a56(a23(x1))
       a34(a56(x1)) -> a56(a34(x1))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [a56](x0) = 4x0,
        
        [a45](x0) = x0,
        
        [a36](x0) = 8x0,
        
        [a35](x0) = x0,
        
        [a34](x0) = x0,
        
        [a23](x0) = x0,
        
        [a16](x0) = 4x0,
        
        [a14](x0) = x0,
        
        [a13](x0) = x0,
        
        [a12](x0) = x0
       orientation:
        a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
        
        a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
        
        a16(x1) = 4x1 >= 4x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
        
        a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
        
        a36(x1) = 8x1 >= 4x1 = a34(a45(a56(a45(a34(x1)))))
        
        a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
        
        a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
        
        a12(a56(x1)) = 4x1 >= 4x1 = a56(a12(x1))
        
        a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
        
        a23(a56(x1)) = 4x1 >= 4x1 = a56(a23(x1))
        
        a34(a56(x1)) = 4x1 >= 4x1 = a56(a34(x1))
       problem:
        a13(x1) -> a12(a23(a12(x1)))
        a14(x1) -> a12(a23(a34(a23(a12(x1)))))
        a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
        a35(x1) -> a34(a45(a34(x1)))
        a12(a34(x1)) -> a34(a12(x1))
        a12(a45(x1)) -> a45(a12(x1))
        a12(a56(x1)) -> a56(a12(x1))
        a23(a45(x1)) -> a45(a23(x1))
        a23(a56(x1)) -> a56(a23(x1))
        a34(a56(x1)) -> a56(a34(x1))
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [a56](x0) = 2x0,
         
         [a45](x0) = 2x0,
         
         [a35](x0) = 4x0,
         
         [a34](x0) = 1x0,
         
         [a23](x0) = x0,
         
         [a16](x0) = 8x0,
         
         [a14](x0) = 2x0,
         
         [a13](x0) = 4x0,
         
         [a12](x0) = x0
        orientation:
         a13(x1) = 4x1 >= x1 = a12(a23(a12(x1)))
         
         a14(x1) = 2x1 >= 1x1 = a12(a23(a34(a23(a12(x1)))))
         
         a16(x1) = 8x1 >= 8x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
         
         a35(x1) = 4x1 >= 4x1 = a34(a45(a34(x1)))
         
         a12(a34(x1)) = 1x1 >= 1x1 = a34(a12(x1))
         
         a12(a45(x1)) = 2x1 >= 2x1 = a45(a12(x1))
         
         a12(a56(x1)) = 2x1 >= 2x1 = a56(a12(x1))
         
         a23(a45(x1)) = 2x1 >= 2x1 = a45(a23(x1))
         
         a23(a56(x1)) = 2x1 >= 2x1 = a56(a23(x1))
         
         a34(a56(x1)) = 3x1 >= 3x1 = a56(a34(x1))
        problem:
         a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
         a35(x1) -> a34(a45(a34(x1)))
         a12(a34(x1)) -> a34(a12(x1))
         a12(a45(x1)) -> a45(a12(x1))
         a12(a56(x1)) -> a56(a12(x1))
         a23(a45(x1)) -> a45(a23(x1))
         a23(a56(x1)) -> a56(a23(x1))
         a34(a56(x1)) -> a56(a34(x1))
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [a56](x0) = 6x0,
          
          [a45](x0) = x0,
          
          [a35](x0) = 8x0,
          
          [a34](x0) = 1x0,
          
          [a23](x0) = x0,
          
          [a16](x0) = 14x0,
          
          [a12](x0) = 3x0
         orientation:
          a16(x1) = 14x1 >= 14x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
          
          a35(x1) = 8x1 >= 2x1 = a34(a45(a34(x1)))
          
          a12(a34(x1)) = 4x1 >= 4x1 = a34(a12(x1))
          
          a12(a45(x1)) = 3x1 >= 3x1 = a45(a12(x1))
          
          a12(a56(x1)) = 9x1 >= 9x1 = a56(a12(x1))
          
          a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
          
          a23(a56(x1)) = 6x1 >= 6x1 = a56(a23(x1))
          
          a34(a56(x1)) = 7x1 >= 7x1 = a56(a34(x1))
         problem:
          a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
          a12(a34(x1)) -> a34(a12(x1))
          a12(a45(x1)) -> a45(a12(x1))
          a12(a56(x1)) -> a56(a12(x1))
          a23(a45(x1)) -> a45(a23(x1))
          a23(a56(x1)) -> a56(a23(x1))
          a34(a56(x1)) -> a56(a34(x1))
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [a56](x0) = 12x0,
           
           [a45](x0) = x0,
           
           [a34](x0) = x0,
           
           [a23](x0) = x0,
           
           [a16](x0) = 14x0,
           
           [a12](x0) = x0
          orientation:
           a16(x1) = 14x1 >= 12x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
           
           a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
           
           a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
           
           a12(a56(x1)) = 12x1 >= 12x1 = a56(a12(x1))
           
           a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
           
           a23(a56(x1)) = 12x1 >= 12x1 = a56(a23(x1))
           
           a34(a56(x1)) = 12x1 >= 12x1 = a56(a34(x1))
          problem:
           a12(a34(x1)) -> a34(a12(x1))
           a12(a45(x1)) -> a45(a12(x1))
           a12(a56(x1)) -> a56(a12(x1))
           a23(a45(x1)) -> a45(a23(x1))
           a23(a56(x1)) -> a56(a23(x1))
           a34(a56(x1)) -> a56(a34(x1))
          KBO Processor:
           weight function:
            w0 = 1
            w(a56) = w(a45) = w(a34) = w(a23) = w(a12) = 1
           precedence:
            a23 > a12 > a34 > a56 ~ a45
           problem:
            
           Qed