YES

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

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