From: vijay_ganesh Date: Fri, 21 Aug 2009 22:28:05 +0000 (+0000) Subject: added rna2.cvc to tests/bio-tests dir X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8dfbba55634d410ed9a2ddd968978c35d47e7860;p=francis%2Fstp.git 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 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;