added rna2.cvc to tests/bio-tests dir

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@139 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/tests/bio-tests/rna2.cvc b/tests/bio-tests/rna2.cvc
new file mode 100644 (file)
index 0000000..e2924e2
--- /dev/null
+++ b/tests/bio-tests/rna2.cvc
@@ -0,0 +1,1301 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Preamble
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+X     : ARRAY BITVECTOR(5) OF BITVECTOR(1);
+Y     : ARRAY BITVECTOR(5) OF BITVECTOR(1);
+ZY     : ARRAY BITVECTOR(5) OF BITVECTOR(1);
+LX     : ARRAY BITVECTOR(3) OF BITVECTOR(1);
+LX_i   : BITVECTOR(3);
+ASSERT (BVLE(0bin000, LX_i) AND BVLE(LX_i, 0bin100));
+RX     : ARRAY BITVECTOR(3) OF BITVECTOR(1);
+RX_i   : BITVECTOR(3);
+ASSERT (BVLE(0bin000, RX_i) AND BVLE(RX_i, 0bin100));
+LY     : ARRAY BITVECTOR(3) OF BITVECTOR(1);
+LY_i   : BITVECTOR(3);
+ASSERT (BVLE(0bin000, LY_i) AND BVLE(LY_i, 0bin100));
+RY     : ARRAY BITVECTOR(3) OF BITVECTOR(1);
+RY_i   : BITVECTOR(3);
+ASSERT (BVLE(0bin000, RY_i) AND BVLE(RY_i, 0bin100));
+LT     : ARRAY BITVECTOR(5) OF BITVECTOR(1);
+RT     : ARRAY BITVECTOR(5) OF BITVECTOR(1);
+final_Ex   : ARRAY BITVECTOR(5) OF BITVECTOR(8);
+final_Ey   : ARRAY BITVECTOR(5) OF BITVECTOR(8);
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Constraints
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%% (1) %%%%%%%%%%
+ASSERT(X[0bin00000]=0bin0);
+ASSERT(final_Ex[0bin00000]=0bin00000000);
+ASSERT(X[0bin00001]=0bin0);
+ASSERT(final_Ex[0bin00001]=0bin00000000);
+ASSERT(final_Ex[0bin00010]=0bin00000000);
+ASSERT((X[0bin00011]=0bin1 AND X[0bin00111]=0bin1) => final_Ex[0bin00011]=0bin00011001);
+ASSERT((X[0bin00011]=0bin0 OR X[0bin00111]=0bin0) => final_Ex[0bin00011]=0bin00000000);
+ASSERT((X[0bin00100]=0bin1 AND X[0bin01000]=0bin1) => final_Ex[0bin00100]=0bin00100010);
+ASSERT((X[0bin00100]=0bin0 OR X[0bin01000]=0bin0) => final_Ex[0bin00100]=0bin00000000);
+ASSERT(final_Ex[0bin00101]=0bin00000000);
+ASSERT(X[0bin00110]=0bin0);
+ASSERT(final_Ex[0bin00110]=0bin00000000);
+ASSERT(X[0bin00111]=0bin0);
+ASSERT((X[0bin00111]=0bin1 AND X[0bin01011]=0bin1) => final_Ex[0bin00111]=0bin00001101);
+ASSERT((X[0bin00111]=0bin0 OR X[0bin01011]=0bin0) => final_Ex[0bin00111]=0bin00000000);
+ASSERT(final_Ex[0bin01000]=0bin00000000);
+ASSERT(final_Ex[0bin01001]=0bin00000000);
+ASSERT(final_Ex[0bin01010]=0bin00000000);
+ASSERT((X[0bin01011]=0bin1 AND X[0bin01111]=0bin1) => final_Ex[0bin01011]=0bin00010101);
+ASSERT((X[0bin01011]=0bin0 OR X[0bin01111]=0bin0) => final_Ex[0bin01011]=0bin00000000);
+ASSERT(X[0bin01100]=0bin0);
+ASSERT(final_Ex[0bin01100]=0bin00000000);
+ASSERT(X[0bin01101]=0bin0);
+ASSERT(final_Ex[0bin01101]=0bin00000000);
+ASSERT(final_Ex[0bin01110]=0bin00000000);
+ASSERT(final_Ex[0bin01111]=0bin00000000);
+ASSERT((X[0bin10000]=0bin1 AND X[0bin10100]=0bin1) => final_Ex[0bin10000]=0bin00011000);
+ASSERT((X[0bin10000]=0bin0 OR X[0bin10100]=0bin0) => final_Ex[0bin10000]=0bin00000000);
+ASSERT(final_Ex[0bin10001]=0bin00000000);
+ASSERT(X[0bin10010]=0bin0);
+ASSERT(final_Ex[0bin10010]=0bin00000000);
+ASSERT(X[0bin10011]=0bin0);
+ASSERT(final_Ex[0bin10011]=0bin00000000);
+ASSERT(final_Ex[0bin10100]=0bin00000000);
+ASSERT(final_Ex[0bin10101]=0bin00000000);
+ASSERT(final_Ex[0bin10110]=0bin00000000);
+ASSERT(final_Ex[0bin10111]=0bin00000000);
+ASSERT(X[0bin11000]=0bin0);
+ASSERT(final_Ex[0bin11000]=0bin00000000);
+%%%%%%%%%% (2) %%%%%%%%%%
+ASSERT(Y[0bin00000]=0bin0);
+ASSERT(final_Ey[0bin00000]=0bin00000000);
+ASSERT(Y[0bin00001]=0bin0);
+ASSERT(final_Ey[0bin00001]=0bin00000000);
+ASSERT(final_Ey[0bin00010]=0bin00000000);
+ASSERT((Y[0bin00011]=0bin1 AND Y[0bin00111]=0bin1) => final_Ey[0bin00011]=0bin00010001);
+ASSERT((Y[0bin00011]=0bin0 OR Y[0bin00111]=0bin0) => final_Ey[0bin00011]=0bin00000000);
+ASSERT((Y[0bin00100]=0bin1 AND Y[0bin01000]=0bin1) => final_Ey[0bin00100]=0bin00010111);
+ASSERT((Y[0bin00100]=0bin0 OR Y[0bin01000]=0bin0) => final_Ey[0bin00100]=0bin00000000);
+ASSERT(final_Ey[0bin00101]=0bin00000000);
+ASSERT(Y[0bin00110]=0bin0);
+ASSERT(final_Ey[0bin00110]=0bin00000000);
+ASSERT(Y[0bin00111]=0bin0);
+ASSERT((Y[0bin00111]=0bin1 AND Y[0bin01011]=0bin1) => final_Ey[0bin00111]=0bin00001001);
+ASSERT((Y[0bin00111]=0bin0 OR Y[0bin01011]=0bin0) => final_Ey[0bin00111]=0bin00000000);
+ASSERT(final_Ey[0bin01000]=0bin00000000);
+ASSERT(final_Ey[0bin01001]=0bin00000000);
+ASSERT(final_Ey[0bin01010]=0bin00000000);
+ASSERT((Y[0bin01011]=0bin1 AND Y[0bin01111]=0bin1) => final_Ey[0bin01011]=0bin00001110);
+ASSERT((Y[0bin01011]=0bin0 OR Y[0bin01111]=0bin0) => final_Ey[0bin01011]=0bin00000000);
+ASSERT(Y[0bin01100]=0bin0);
+ASSERT(final_Ey[0bin01100]=0bin00000000);
+ASSERT(Y[0bin01101]=0bin0);
+ASSERT(final_Ey[0bin01101]=0bin00000000);
+ASSERT(final_Ey[0bin01110]=0bin00000000);
+ASSERT(final_Ey[0bin01111]=0bin00000000);
+ASSERT((Y[0bin10000]=0bin1 AND Y[0bin10100]=0bin1) => final_Ey[0bin10000]=0bin00010000);
+ASSERT((Y[0bin10000]=0bin0 OR Y[0bin10100]=0bin0) => final_Ey[0bin10000]=0bin00000000);
+ASSERT(final_Ey[0bin10001]=0bin00000000);
+ASSERT(Y[0bin10010]=0bin0);
+ASSERT(final_Ey[0bin10010]=0bin00000000);
+ASSERT(Y[0bin10011]=0bin0);
+ASSERT(final_Ey[0bin10011]=0bin00000000);
+ASSERT(final_Ey[0bin10100]=0bin00000000);
+ASSERT(final_Ey[0bin10101]=0bin00000000);
+ASSERT(final_Ey[0bin10110]=0bin00000000);
+ASSERT(final_Ey[0bin10111]=0bin00000000);
+ASSERT(Y[0bin11000]=0bin0);
+ASSERT(final_Ey[0bin11000]=0bin00000000);
+%%%%%%%%%% (3) %%%%%%%%%%
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00101], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin00101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin00001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01010], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01011], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin00010]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin00111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01111], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10000], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10001], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01101], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin01111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin00011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10100], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00100], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10101], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01001], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10110], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01110], 0bin0@X[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10111]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin00100]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10111], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin10011], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin01110]), 0bin01));
+%%%%%%%%%% (4) %%%%%%%%%%
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin01111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin01111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00101], 0bin0@Y[0bin00001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00001], 0bin0@Y[0bin00001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin00111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin00111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin01001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin01001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin01010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin01010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01010], 0bin0@Y[0bin00010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00010], 0bin0@Y[0bin00010]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin01011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin01011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01011], 0bin0@Y[0bin00111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00111], 0bin0@Y[0bin00111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin01111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin01111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01111], 0bin0@Y[0bin00011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00011], 0bin0@Y[0bin00011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin10000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin10000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10000], 0bin0@Y[0bin01000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01000], 0bin0@Y[0bin01000]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin10001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin10001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10001], 0bin0@Y[0bin01101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01101], 0bin0@Y[0bin01101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin10100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin10100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10100], 0bin0@Y[0bin00100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin00100], 0bin0@Y[0bin00100]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin10101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin10101]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10101], 0bin0@Y[0bin01001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01001], 0bin0@Y[0bin01001]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin10110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin10110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10110], 0bin0@Y[0bin01110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin01110], 0bin0@Y[0bin01110]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10111]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10111], 0bin0@Y[0bin10011]), 0bin01) );
+ASSERT(BVLE( BVPLUS(2, 0bin0@X[0bin10011], 0bin0@Y[0bin10011]), 0bin01) );
+%%%%%%%%%% (5) %%%%%%%%%%
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00010], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin00011], 0bin0@X[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@X[0bin01000], 0bin0@X[0bin01110]), 0bin01));
+%%%%%%%%%% (6) %%%%%%%%%%
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01000]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin01001]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00011], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin01000], 0bin0@Y[0bin01110]), 0bin01));
+%%%%%%%%%% (7) %%%%%%%%%%
+ASSERT (BVSUB(3, 0bin00@LX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+%%%%%%%%%% (8) %%%%%%%%%%
+ASSERT (BVSUB(3, 0bin00@RX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RX[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+%%%%%%%%%% (9) %%%%%%%%%%
+ASSERT (BVSUB(3, 0bin00@LY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@LY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+%%%%%%%%%% (10) %%%%%%%%%%
+ASSERT (BVSUB(3, 0bin00@RY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin000], BVPLUS(3, 0bin00@X[0bin00001], 0bin00@X[0bin00010], 0bin00@X[0bin00011], 0bin00@X[0bin00100]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin001], BVPLUS(3, 0bin00@X[0bin00111], 0bin00@X[0bin01000], 0bin00@X[0bin01001]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin010], BVPLUS(3, 0bin00@X[0bin01101], 0bin00@X[0bin01110]) ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+ASSERT (BVSUB(3, 0bin00@RY[0bin011], 0bin00@X[0bin10011] ) = 0bin000 );
+%%%%%%%%%% (11) %%%%%%%%%%
+ASSERT (BVLE(0bin01, BVPLUS(2, 0bin0@LX[BVSUB(3, LX_i, 0bin001)], BVSUB(2, 0bin01, 0bin0@LX[LX_i]), 0bin0@LX[BVPLUS(3, LX_i, 0bin001)] ) ));
+%%%%%%%%%% (12) %%%%%%%%%%
+ASSERT (BVLE(0bin01, BVPLUS(2, 0bin0@RX[BVSUB(3, RX_i, 0bin001)], BVSUB(2, 0bin01, 0bin0@RX[RX_i]), 0bin0@RX[BVPLUS(3, RX_i, 0bin001)] ) ));
+%%%%%%%%%% (13) %%%%%%%%%%
+ASSERT (BVLE(0bin01, BVPLUS(2, 0bin0@LY[BVSUB(3, LY_i, 0bin001)], BVSUB(2, 0bin01, 0bin0@LY[LY_i]), 0bin0@LY[BVPLUS(3, LY_i, 0bin001)] ) ));
+%%%%%%%%%% (14) %%%%%%%%%%
+ASSERT (BVLE(0bin01, BVPLUS(2, 0bin0@RY[BVSUB(3, RY_i, 0bin001)], BVSUB(2, 0bin01, 0bin0@RY[RY_i]), 0bin0@RY[BVPLUS(3, RY_i, 0bin001)] ) ));
+%%%%%%%%%% (15) %%%%%%%%%%
+ASSERT (BVLE( BVDIV(6, BVPLUS(6, 0bin00000@X[0bin01000], 0bin00000@X[0bin01001]), 0bin011001),  0bin00000@LT[0bin00010]));
+ASSERT (BVLE( BVDIV(6, BVPLUS(6, 0bin00000@X[0bin01001], 0bin00000@X[0bin01110]), 0bin011001),  0bin00000@LT[0bin00011]));
+ASSERT (BVLE( BVDIV(6 , 0bin00000@X[0bin01110], 0bin011001),  0bin00000@LT[0bin01000]));
+%%%%%%%%%% (16) %%%%%%%%%%
+ASSERT (BVLE( BVDIV(6, BVPLUS(6, 0bin00000@X[0bin01000], 0bin00000@X[0bin01001]), 0bin011001),  0bin00000@RT[0bin00010]));
+ASSERT (BVLE( BVDIV(6, BVPLUS(6, 0bin00000@X[0bin01001], 0bin00000@X[0bin01110]), 0bin011001),  0bin00000@RT[0bin00011]));
+ASSERT (BVLE( BVDIV(6 , 0bin00000@X[0bin01110], 0bin011001),  0bin00000@RT[0bin01000]));
+%%%%%%%%%% (17) %%%%%%%%%%
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00000], 0bin0@RT[0bin00000]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00001], 0bin0@RT[0bin00001]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00010], 0bin0@RT[0bin00010]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00011], 0bin0@RT[0bin00011]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00100], 0bin0@RT[0bin00100]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00101], 0bin0@RT[0bin00101]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00110], 0bin0@RT[0bin00110]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin00111], 0bin0@RT[0bin00111]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01000], 0bin0@RT[0bin01000]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01001], 0bin0@RT[0bin01001]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01010], 0bin0@RT[0bin01010]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01011], 0bin0@RT[0bin01011]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01100], 0bin0@RT[0bin01100]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01101], 0bin0@RT[0bin01101]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01110], 0bin0@RT[0bin01110]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin01111], 0bin0@RT[0bin01111]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10000], 0bin0@RT[0bin10000]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10001], 0bin0@RT[0bin10001]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10010], 0bin0@RT[0bin10010]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10011], 0bin0@RT[0bin10011]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10100], 0bin0@RT[0bin10100]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10101], 0bin0@RT[0bin10101]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10110], 0bin0@RT[0bin10110]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin10111], 0bin0@RT[0bin10111]), 0bin01) );
+ASSERT (BVLE( BVPLUS(2, 0bin0@LT[0bin11000], 0bin0@RT[0bin11000]), 0bin01) );
+%%%%%%%%%% (18) %%%%%%%%%%
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01101]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin01110]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00001], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00010], 0bin0@Y[0bin10011]), 0bin01));
+ASSERT (BVLE(BVPLUS(2, 0bin0@Y[0bin00111], 0bin0@Y[0bin10011]), 0bin01));
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Objective function
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+total_energy : BITVECTOR(16);
+ASSERT(total_energy = BVPLUS(16, BVPLUS(16, 0bin00000000@final_Ex[0bin00000], 0bin00000000@final_Ey[0bin00000]), BVPLUS(16, 0bin00000000@final_Ex[0bin00001], 0bin00000000@final_Ey[0bin00001]), BVPLUS(16, 0bin00000000@final_Ex[0bin00010], 0bin00000000@final_Ey[0bin00010]), BVPLUS(16, 0bin00000000@final_Ex[0bin00011], 0bin00000000@final_Ey[0bin00011]), BVPLUS(16, 0bin00000000@final_Ex[0bin00100], 0bin00000000@final_Ey[0bin00100]), BVPLUS(16, 0bin00000000@final_Ex[0bin00101], 0bin00000000@final_Ey[0bin00101]), BVPLUS(16, 0bin00000000@final_Ex[0bin00110], 0bin00000000@final_Ey[0bin00110]), BVPLUS(16, 0bin00000000@final_Ex[0bin00111], 0bin00000000@final_Ey[0bin00111]), BVPLUS(16, 0bin00000000@final_Ex[0bin01000], 0bin00000000@final_Ey[0bin01000]), BVPLUS(16, 0bin00000000@final_Ex[0bin01001], 0bin00000000@final_Ey[0bin01001]), BVPLUS(16, 0bin00000000@final_Ex[0bin01010], 0bin00000000@final_Ey[0bin01010]), BVPLUS(16, 0bin00000000@final_Ex[0bin01011], 0bin00000000@final_Ey[0bin01011]), BVPLUS(16, 0bin00000000@final_Ex[0bin01100], 0bin00000000@final_Ey[0bin01100]), BVPLUS(16, 0bin00000000@final_Ex[0bin01101], 0bin00000000@final_Ey[0bin01101]), BVPLUS(16, 0bin00000000@final_Ex[0bin01110], 0bin00000000@final_Ey[0bin01110]), BVPLUS(16, 0bin00000000@final_Ex[0bin01111], 0bin00000000@final_Ey[0bin01111]), BVPLUS(16, 0bin00000000@final_Ex[0bin10000], 0bin00000000@final_Ey[0bin10000]), BVPLUS(16, 0bin00000000@final_Ex[0bin10001], 0bin00000000@final_Ey[0bin10001]), BVPLUS(16, 0bin00000000@final_Ex[0bin10010], 0bin00000000@final_Ey[0bin10010]), BVPLUS(16, 0bin00000000@final_Ex[0bin10011], 0bin00000000@final_Ey[0bin10011]), BVPLUS(16, 0bin00000000@final_Ex[0bin10100], 0bin00000000@final_Ey[0bin10100]), BVPLUS(16, 0bin00000000@final_Ex[0bin10101], 0bin00000000@final_Ey[0bin10101]), BVPLUS(16, 0bin00000000@final_Ex[0bin10110], 0bin00000000@final_Ey[0bin10110]), BVPLUS(16, 0bin00000000@final_Ex[0bin10111], 0bin00000000@final_Ey[0bin10111]), BVPLUS(16, 0bin00000000@final_Ex[0bin11000], 0bin00000000@final_Ey[0bin11000])) );
+ASSERT (BVGE(total_energy, 0bin0000000000110010));
+QUERY FALSE;