git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk...

diff --git a/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc b/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc
deleted file mode 100644 (file)
index cc437a4..0000000
--- a/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc
+++ /dev/null
@@ -1,329 +0,0 @@
-% 4 alpha helices. Each helix with 6 amino acid (residues), and 4
-% faces (two inner and two outer). Each face has 1 or 2 residues
-% The problem is encoded with two bit bit-vector variable per face.
-
-
-alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4);
-alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32);
-alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(32);
-
-
-alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4);
-alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32);
-alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(32);
-
-
-alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4);
-alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32);
-alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(32);
-
-
-alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4);
-alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32);
-alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(32);
-
-
-coil_12, coil_23, coil34 : BITVECTOR(16);
-coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32);
-coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(32);
-
-contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32);
-contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32);
-contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32);
-contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32);
-
-outer_energy : BITVECTOR(32);
-inner_energy : BITVECTOR(32);
-bits32_one   : BITVECTOR(32);
-bits32_two   : BITVECTOR(32);
-
-ASSERT (bits32_one = 0hex00000001);
-ASSERT (bits32_two = 0hex00000002);
-
-aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(32);
-ASSERT (aminoacid_energies[0hex00000000] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000001] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000002] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000003] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000004] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000005] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000006] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000007] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000008] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000009] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000A] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000000B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000C] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000000D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000010] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000011] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000012] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000013] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000014] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000015] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000016] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000017] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000018] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000019] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001A] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000001B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001D] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000001E] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000001F] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000020] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000021] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000022] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000023] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000024] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000025] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000026] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000027] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000028] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000029] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000002A] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000002B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000002C] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000002D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000002E] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000002F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000030] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000031] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000032] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000033] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000034] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000035] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000036] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000037] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000038] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000039] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000003A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003B] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000003C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003E] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000003F] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000040] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000041] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000042] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000043] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000044] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000045] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000046] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000047] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000048] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000049] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000004A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004B] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000004C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004D] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000004E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004F] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000050] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000051] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000052] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000053] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000054] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000055] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000056] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000057] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000058] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000059] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000005A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005B] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000005C] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000005D] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex0000005E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000060] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000061] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000062] = 0hex00000111);
-ASSERT (aminoacid_energies[0hex00000063] = 0hex00000111);
-
-ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2);
-%ASSERT (alpha1_inner1 = 0hex0);
-ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2);
-
-ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2);
-
-ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2);
-
-ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2);
-
-ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2) = 0hex6);
-ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2) = 0hex6);
-ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2) = 0hex6);
-ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2) = 0hex6);
-
-
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1);
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1);
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1);
-
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1);
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1);
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1);
-
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1);
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1);
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1);
-
-
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1);
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1);
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1);
-
-
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]);
-ASSERT (alpha1_inner1 = 0hex2 =>  
-       alpha1_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index]));
-
-
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer1_index]));
-ASSERT (alpha1_outer1 = 0hex2 =>
-       alpha1_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], 
-                                                             aminoacid_energies[alpha1_outer1_index])));
-
-
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]);
-ASSERT (alpha1_inner2 = 0hex2 =>
-       alpha1_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index]));
-
-
-ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer2_index]));
-ASSERT (alpha1_outer2 = 0hex2 =>
-       alpha1_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], 
-                                                             aminoacid_energies[alpha1_outer2_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]);
-ASSERT (alpha2_inner1 = 0hex2 =>  
-       alpha2_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index]));
-
-
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer1_index]));
-ASSERT (alpha2_outer1 = 0hex2 =>
-       alpha2_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index])));
-
-
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]);
-ASSERT (alpha2_inner2 = 0hex2 =>
-       alpha2_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index]));
-
-
-ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer2_index]));
-ASSERT (alpha2_outer2 = 0hex2 =>
-       alpha2_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]);
-ASSERT (alpha3_inner1 = 0hex2 =>  
-       alpha3_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index]));
-
-
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer1_index]));
-ASSERT (alpha3_outer1 = 0hex2 =>
-       alpha3_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], 
-                                                             aminoacid_energies[alpha3_outer1_index])));
-
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]);
-ASSERT (alpha3_inner2 = 0hex2 =>
-       alpha3_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)],
-                                                                     aminoacid_energies[alpha3_inner2_index]));
-
-
-ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer2_index]));
-ASSERT (alpha3_outer2 = 0hex2 =>
-       alpha3_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], 
-                                                             aminoacid_energies[alpha3_outer2_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]);
-ASSERT (alpha4_inner1 = 0hex2 =>  
-       alpha4_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index]));
-
-
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer1_index]));
-ASSERT (alpha4_outer1 = 0hex2 =>
-       alpha4_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)],
-                                                             aminoacid_energies[alpha4_outer1_index])));
-
-
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]);
-ASSERT (alpha4_inner2 = 0hex2 =>
-       alpha4_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index]));
-
-
-ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer2_index]));
-ASSERT (alpha4_outer2 = 0hex2 =>
-       alpha4_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], 
-                                                            aminoacid_energies[alpha4_outer2_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (contact_energy12_zero = BVMULT(32, alpha1_inner1_energy, alpha2_inner1_energy));
-ASSERT (contact_energy12_one  = BVMULT(32, alpha1_inner2_energy, alpha2_inner2_energy));
-
-
-
-ASSERT (contact_energy23_zero = BVMULT(32, alpha2_inner1_energy, alpha3_inner1_energy));
-ASSERT (contact_energy23_one  = BVMULT(32, alpha2_inner2_energy, alpha3_inner2_energy));
-
-
-
-ASSERT (contact_energy34_zero = BVMULT(32, alpha3_inner1_energy, alpha4_inner1_energy));
-ASSERT (contact_energy34_one  = BVMULT(32, alpha3_inner2_energy, alpha4_inner2_energy));
-
-
-ASSERT (contact_energy41_zero = BVMULT(32, alpha4_inner1_energy, alpha1_inner1_energy));
-ASSERT (contact_energy41_one  = BVMULT(32, alpha4_inner2_energy, alpha1_inner2_energy));
-
-
-ASSERT (outer_energy = BVPLUS(32,  alpha1_outer1_energy, alpha1_outer2_energy,
-                                  alpha2_outer1_energy, alpha2_outer2_energy,
-                                  alpha3_outer1_energy, alpha3_outer2_energy,
-                                  alpha4_outer1_energy, alpha4_outer2_energy));
-
-
-ASSERT (inner_energy = BVPLUS(32,  contact_energy12_zero, contact_energy12_one,
-                                  contact_energy23_zero, contact_energy23_one,
-                                  contact_energy34_zero, contact_energy34_one,
-                                   contact_energy41_zero, contact_energy41_one));
-
-
-% final query
-ASSERT (BVGE(BVMULT(64,0hex00000000@outer_energy,0hex00000000@inner_energy), 
-            0hex1111111111111110));
-QUERY FALSE;
\ No newline at end of file

diff --git a/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc b/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc
deleted file mode 100644 (file)
index e134ad6..0000000
--- a/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc
+++ /dev/null
@@ -1,379 +0,0 @@
-% 4 alpha helices. Each helix with 6 amino acid (residues), and 4
-% faces (two inner and two outer). Each face has 1 or 2 residues
-% The problem is encoded with two bit bit-vector variable per face.
-
-
-alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4);
-alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32);
-alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(32);
-
-
-alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4);
-alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32);
-alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(32);
-
-
-alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4);
-alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32);
-alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(32);
-
-
-alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4);
-alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32);
-alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(32);
-
-
-coil_12, coil_23, coil34 : BITVECTOR(16);
-coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32);
-coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(32);
-
-contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32);
-contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32);
-contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32);
-contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32);
-
-outer_energy : BITVECTOR(32);
-inner_energy : BITVECTOR(32);
-bits32_one   : BITVECTOR(32);
-bits32_two   : BITVECTOR(32);
-
-ASSERT (bits32_one = 0hex00000001);
-ASSERT (bits32_two = 0hex00000002);
-
-aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(32);
-ASSERT (aminoacid_energies[0hex00000000] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000001] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000002] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000003] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000004] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000005] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000006] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000007] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000008] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000009] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000A] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000000B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000C] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000000D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000000F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000010] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000011] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000012] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000013] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000014] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000015] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000016] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000017] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000018] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000019] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001A] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000001B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000001F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000020] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000021] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000022] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000023] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000024] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000025] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000026] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000027] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000028] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000029] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000002A] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000002B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000002C] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000002D] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000002E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000002F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000030] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000031] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000032] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000033] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000034] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000035] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000036] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000037] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000038] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000039] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003B] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000003C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003D] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000003E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000003F] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000040] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000041] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000042] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000043] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000044] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000045] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000046] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000047] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000048] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000049] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000004A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004B] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004D] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000004F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000050] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000051] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000052] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000053] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000054] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000055] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000056] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000057] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000058] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000059] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005A] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005B] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000005C] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005D] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex0000005E] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex0000005F] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000060] = 0hex00000000);
-ASSERT (aminoacid_energies[0hex00000061] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000062] = 0hex00011111);
-ASSERT (aminoacid_energies[0hex00000063] = 0hex00000000);
-
-%ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2);
-ASSERT (alpha1_inner1 = 0hex2);
-ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2);
-ASSERT (alpha1_inner3 = 0hex1 OR alpha1_inner3 = 0hex2);
-ASSERT (alpha1_outer3 = 0hex1 OR alpha1_outer3 = 0hex2);
-
-ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2);
-ASSERT (alpha2_inner3 = 0hex1 OR alpha2_inner3 = 0hex2);
-ASSERT (alpha2_outer3 = 0hex1 OR alpha2_outer3 = 0hex2);
-
-ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2);
-ASSERT (alpha3_inner3 = 0hex1 OR alpha3_inner3 = 0hex2);
-ASSERT (alpha3_outer3 = 0hex1 OR alpha3_outer3 = 0hex2);
-
-ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2);
-ASSERT (alpha4_inner3 = 0hex1 OR alpha4_inner3 = 0hex2);
-ASSERT (alpha4_outer3 = 0hex1 OR alpha4_outer3 = 0hex2);
-
-
-ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3) = 0hex9);
-
-
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1);
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1);
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1);
-ASSERT (alpha1_inner3 = 0hex1 => alpha1_outer3 = 0hex2);
-ASSERT (alpha1_inner3 = 0hex2 => alpha1_outer3 = 0hex1);
-
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1);
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1);
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1);
-ASSERT (alpha2_inner3 = 0hex1 => alpha2_outer3 = 0hex2);
-ASSERT (alpha2_inner3 = 0hex2 => alpha2_outer3 = 0hex1);
-
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1);
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1);
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1);
-ASSERT (alpha3_inner3 = 0hex1 => alpha3_outer3 = 0hex2);
-ASSERT (alpha3_inner3 = 0hex2 => alpha3_outer3 = 0hex1);
-
-
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1);
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1);
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1);
-ASSERT (alpha4_inner3 = 0hex1 => alpha4_outer3 = 0hex2);
-ASSERT (alpha4_inner3 = 0hex2 => alpha4_outer3 = 0hex1);
-
-
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000000)]);
-ASSERT (alpha1_inner1 = 0hex2 =>  
-       alpha1_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index]));
-
-
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer1_index]));
-ASSERT (alpha1_outer1 = 0hex2 =>
-       alpha1_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], aminoacid_energies[alpha1_outer1_index])));
-
-
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000000)]);
-ASSERT (alpha1_inner2 = 0hex2 =>
-       alpha1_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index]));
-
-
-ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer2_index]));
-ASSERT (alpha1_outer2 = 0hex2 =>
-       alpha1_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], aminoacid_energies[alpha1_outer2_index])));
-
-ASSERT (alpha1_inner3 = 0hex1 => alpha1_inner3_energy = aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000000)]);
-ASSERT (alpha1_inner3 = 0hex2 =>
-       alpha1_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000001)],aminoacid_energies[alpha1_inner3_index]));
-
-
-ASSERT (alpha1_outer3 = 0hex1 => alpha1_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer3_index]));
-ASSERT (alpha1_outer3 = 0hex2 =>
-       alpha1_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer3_index,0hex00000001)], aminoacid_energies[alpha1_outer3_index])));
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000000)]);
-ASSERT (alpha2_inner1 = 0hex2 =>  
-       alpha2_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index]));
-
-
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer1_index]));
-ASSERT (alpha2_outer1 = 0hex2 =>
-       alpha2_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index])));
-
-
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000000)]);
-ASSERT (alpha2_inner2 = 0hex2 =>
-       alpha2_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index]));
-
-
-ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer2_index]));
-ASSERT (alpha2_outer2 = 0hex2 =>
-       alpha2_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index])));
-
-
-ASSERT (alpha2_inner3 = 0hex1 => alpha2_inner3_energy = aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000000)]);
-ASSERT (alpha2_inner3 = 0hex2 =>
-       alpha2_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000001)],aminoacid_energies[alpha2_inner3_index]));
-
-
-ASSERT (alpha2_outer3 = 0hex1 => alpha2_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer3_index]));
-ASSERT (alpha2_outer3 = 0hex2 =>
-       alpha2_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer3_index,0hex00000001)], aminoacid_energies[alpha2_outer3_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000000)]);
-ASSERT (alpha3_inner1 = 0hex2 =>  
-       alpha3_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index]));
-
-
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer1_index]));
-ASSERT (alpha3_outer1 = 0hex2 =>
-       alpha3_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], aminoacid_energies[alpha3_outer1_index])));
-
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000000)]);
-ASSERT (alpha3_inner2 = 0hex2 =>
-       alpha3_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)],aminoacid_energies[alpha3_inner2_index]));
-
-
-ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer2_index]));
-ASSERT (alpha3_outer2 = 0hex2 =>
-       alpha3_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], aminoacid_energies[alpha3_outer2_index])));
-
-
-ASSERT (alpha3_inner3 = 0hex1 => alpha3_inner3_energy = aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000000)]);
-ASSERT (alpha3_inner3 = 0hex2 =>
-       alpha3_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000001)],aminoacid_energies[alpha3_inner3_index]));
-
-
-ASSERT (alpha3_outer3 = 0hex1 => alpha3_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer3_index]));
-ASSERT (alpha3_outer3 = 0hex2 =>
-       alpha3_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer3_index,0hex00000001)], aminoacid_energies[alpha3_outer3_index])));
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000000)]);
-ASSERT (alpha4_inner1 = 0hex2 =>  
-       alpha4_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index]));
-
-
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer1_index]));
-ASSERT (alpha4_outer1 = 0hex2 =>
-       alpha4_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)], aminoacid_energies[alpha4_outer1_index])));
-
-
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000000)]);
-ASSERT (alpha4_inner2 = 0hex2 =>
-       alpha4_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index]));
-
-
-ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer2_index]));
-ASSERT (alpha4_outer2 = 0hex2 =>
-       alpha4_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], aminoacid_energies[alpha4_outer2_index])));
-
-
-ASSERT (alpha4_inner3 = 0hex1 => alpha4_inner3_energy = aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000000)]);
-ASSERT (alpha4_inner3 = 0hex2 =>
-       alpha4_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000001)],aminoacid_energies[alpha4_inner3_index]));
-
-
-ASSERT (alpha4_outer3 = 0hex1 => alpha4_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer3_index]));
-ASSERT (alpha4_outer3 = 0hex2 =>
-       alpha4_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer3_index,0hex00000001)], aminoacid_energies[alpha4_outer3_index])));
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-ASSERT (contact_energy12_zero = BVPLUS(32, alpha1_inner1_energy, alpha2_inner1_energy));
-ASSERT (contact_energy12_one  = BVPLUS(32, alpha1_inner2_energy, alpha2_inner2_energy));
-ASSERT (contact_energy12_two  = BVPLUS(32, alpha1_inner3_energy, alpha2_inner3_energy));
-
-
-ASSERT (contact_energy23_zero = BVPLUS(32, alpha2_inner1_energy, alpha3_inner1_energy));
-ASSERT (contact_energy23_one  = BVPLUS(32, alpha2_inner2_energy, alpha3_inner2_energy));
-ASSERT (contact_energy23_two  = BVPLUS(32, alpha2_inner3_energy, alpha3_inner3_energy));
-
-
-ASSERT (contact_energy34_zero = BVPLUS(32, alpha3_inner1_energy, alpha4_inner1_energy));
-ASSERT (contact_energy34_one  = BVPLUS(32, alpha3_inner2_energy, alpha4_inner2_energy));
-ASSERT (contact_energy34_two  = BVPLUS(32, alpha3_inner3_energy, alpha4_inner3_energy));
-
-ASSERT (contact_energy41_zero = BVPLUS(32, alpha4_inner1_energy, alpha1_inner1_energy));
-ASSERT (contact_energy41_one  = BVPLUS(32, alpha4_inner2_energy, alpha1_inner2_energy));
-ASSERT (contact_energy41_two  = BVPLUS(32, alpha4_inner3_energy, alpha1_inner3_energy));
-
-ASSERT (outer_energy = BVPLUS(32,  alpha1_outer1_energy, alpha1_outer2_energy, alpha1_outer3_energy, 
-                                  alpha2_outer1_energy, alpha2_outer2_energy, alpha2_outer3_energy,    
-                                  alpha3_outer1_energy, alpha3_outer2_energy, alpha3_outer3_energy,
-                                  alpha4_outer1_energy, alpha4_outer2_energy, alpha4_outer3_energy));
-
-
-ASSERT (inner_energy = BVPLUS(32,  contact_energy12_zero, contact_energy12_one, contact_energy12_two,
-                                  contact_energy23_zero, contact_energy23_one, contact_energy23_two,
-                                  contact_energy34_zero, contact_energy34_one, contact_energy34_two,
-                                   contact_energy41_zero, contact_energy41_one, contact_energy41_two));
-
-
-% final query
-ASSERT (BVGE(BVPLUS(64,0hex00000000@outer_energy,0hex00000000@inner_energy), 0hex0000000000000001));
-QUERY FALSE;
\ No newline at end of file

diff --git a/tests/bio-tests/4-alpha-helices-3-rungs.cvc b/tests/bio-tests/4-alpha-helices-3-rungs.cvc
index f407ddb8dacdd7c19bfcd3b6097efbe66600c77a..e1fc120e8b7d7b985b859f499ec7d97b439d6da5 100644 (file)
--- a/tests/bio-tests/4-alpha-helices-3-rungs.cvc
+++ b/tests/bio-tests/4-alpha-helices-3-rungs.cvc
@@ -3,380 +3,386 @@
 % The problem is encoded with two bit bit-vector variable per face.
 
 
-alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4);
-alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32);
-alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(64);
-
-
-alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4);
-alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32);
-alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(64);
-
-
-alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4);
-alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32);
-alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(64);
-
-
-alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4);
-alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32);
-alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(64);
-
-
-coil_12, coil_23, coil34 : BITVECTOR(16);
-coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32);
-coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(64);
-
-contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(64);
-contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(64);
-contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(64);
-contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(64);
-
-outer_energy : BITVECTOR(64);
-inner_energy : BITVECTOR(64);
-bits64_one   : BITVECTOR(64);
-bits64_two   : BITVECTOR(64);
-
-ASSERT (bits64_one = 0hex0000000000000001);
-ASSERT (bits64_two = 0hex0000000000000002);
-
-aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(64);
-ASSERT (aminoacid_energies[0hex00000000] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000001] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000002] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000003] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000004] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000005] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000006] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000007] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000008] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000009] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000000F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000010] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000011] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000012] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000013] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000014] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000015] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000016] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000017] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000018] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000019] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000001F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000020] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000021] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000022] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000023] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000024] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000025] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000026] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000027] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000028] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000029] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000002F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000030] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000031] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000032] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000033] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000034] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000035] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000036] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000037] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000038] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000039] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000003F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000040] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000041] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000042] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000043] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000044] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000045] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000046] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000047] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000048] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000049] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000004F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000050] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000051] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000052] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000053] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000054] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000055] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000056] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000057] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000058] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000059] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005A] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005B] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005C] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005D] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005E] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex0000005F] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000060] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000061] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000062] = 0hex0000000000000000);
-ASSERT (aminoacid_energies[0hex00000063] = 0hex0000000000000000);
-
-ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2);
-ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2);
-ASSERT (alpha1_inner3 = 0hex1 OR alpha1_inner3 = 0hex2);
-ASSERT (alpha1_outer3 = 0hex1 OR alpha1_outer3 = 0hex2);
-
-ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2);
-ASSERT (alpha2_inner3 = 0hex1 OR alpha2_inner3 = 0hex2);
-ASSERT (alpha2_outer3 = 0hex1 OR alpha2_outer3 = 0hex2);
-
-ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2);
-ASSERT (alpha3_inner3 = 0hex1 OR alpha3_inner3 = 0hex2);
-ASSERT (alpha3_outer3 = 0hex1 OR alpha3_outer3 = 0hex2);
-
-ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2);
-ASSERT (alpha4_inner3 = 0hex1 OR alpha4_inner3 = 0hex2);
-ASSERT (alpha4_outer3 = 0hex1 OR alpha4_outer3 = 0hex2);
-
-
-ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3) = 0hex9);
-ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3) = 0hex9);
-
-
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2);
-ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1);
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2);
-ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1);
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2);
-ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1);
-ASSERT (alpha1_inner3 = 0hex1 => alpha1_outer3 = 0hex2);
-ASSERT (alpha1_inner3 = 0hex2 => alpha1_outer3 = 0hex1);
-
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2);
-ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1);
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2);
-ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1);
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2);
-ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1);
-ASSERT (alpha2_inner3 = 0hex1 => alpha2_outer3 = 0hex2);
-ASSERT (alpha2_inner3 = 0hex2 => alpha2_outer3 = 0hex1);
-
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2);
-ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1);
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2);
-ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1);
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2);
-ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1);
-ASSERT (alpha3_inner3 = 0hex1 => alpha3_outer3 = 0hex2);
-ASSERT (alpha3_inner3 = 0hex2 => alpha3_outer3 = 0hex1);
-
-
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2);
-ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1);
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2);
-ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1);
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2);
-ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1);
-ASSERT (alpha4_inner3 = 0hex1 => alpha4_outer3 = 0hex2);
-ASSERT (alpha4_inner3 = 0hex2 => alpha4_outer3 = 0hex1);
+%%% ALPHA1 Helix variables
+alpha1_inner1_length, alpha1_outer1_length, alpha1_inner2_length, alpha1_outer2_length, alpha1_inner3_length, alpha1_outer3_length : BITVECTOR(4);
+alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(16);
+alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(20);
+
+
+%%% ALPHA2 Helix variables
+alpha2_inner1_length, alpha2_outer1_length, alpha2_inner2_length, alpha2_outer2_length, alpha2_inner3_length, alpha2_outer3_length : BITVECTOR(4);
+alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(16);
+alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(20);
+
+
+%%% ALPHA3 Helix variables
+alpha3_inner1_length, alpha3_outer1_length, alpha3_inner2_length, alpha3_outer2_length, alpha3_inner3_length, alpha3_outer3_length : BITVECTOR(4);
+alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(16);
+alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(20);
+
+
+%%% ALPHA4 Helix variables
+alpha4_inner1_length, alpha4_outer1_length, alpha4_inner2_length, alpha4_outer2_length, alpha4_inner3_length, alpha4_outer3_length : BITVECTOR(4);
+alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(16);
+alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(20);
+
+
+coil_12_length, coil_23_length, coil34_length : BITVECTOR(8);
+coil_12_index, coil_23_index, coil_34_index : BITVECTOR(16);
+coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(20);
+
+contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32);
+contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32);
+contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32);
+contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32);
+
+outer_energy : BITVECTOR(32);
+inner_energy : BITVECTOR(32);
+bits20_one   : BITVECTOR(20);
+bits20_two   : BITVECTOR(20);
+
+ASSERT (bits20_one = 0hex00001);
+ASSERT (bits20_two = 0hex00002);
+
+
+%%%%%%%%%%%%%% START OF AMINO ACID ENERGY ARRAY %%%%%%%%%%%%%
+
+aminoacid_energies : ARRAY BITVECTOR(12) OF BITVECTOR(20);
+ASSERT (aminoacid_energies[0hex000] = 0hex01111);
+ASSERT (aminoacid_energies[0hex001] = 0hex01111);
+ASSERT (aminoacid_energies[0hex002] = 0hex00011);
+ASSERT (aminoacid_energies[0hex003] = 0hex01111);
+ASSERT (aminoacid_energies[0hex004] = 0hex00011);
+ASSERT (aminoacid_energies[0hex005] = 0hex01111);
+ASSERT (aminoacid_energies[0hex006] = 0hex00011);
+ASSERT (aminoacid_energies[0hex007] = 0hex01111);
+ASSERT (aminoacid_energies[0hex008] = 0hex00011);
+ASSERT (aminoacid_energies[0hex009] = 0hex01111);
+ASSERT (aminoacid_energies[0hex00A] = 0hex00011);
+ASSERT (aminoacid_energies[0hex00B] = 0hex01111);
+ASSERT (aminoacid_energies[0hex00C] = 0hex00011);
+ASSERT (aminoacid_energies[0hex00D] = 0hex01111);
+ASSERT (aminoacid_energies[0hex00E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex00F] = 0hex01111);
+ASSERT (aminoacid_energies[0hex010] = 0hex01111);
+ASSERT (aminoacid_energies[0hex011] = 0hex00011);
+ASSERT (aminoacid_energies[0hex012] = 0hex01111);
+ASSERT (aminoacid_energies[0hex013] = 0hex01111);
+ASSERT (aminoacid_energies[0hex014] = 0hex00011);
+ASSERT (aminoacid_energies[0hex015] = 0hex01111);
+ASSERT (aminoacid_energies[0hex016] = 0hex00011);
+ASSERT (aminoacid_energies[0hex017] = 0hex01111);
+ASSERT (aminoacid_energies[0hex018] = 0hex00011);
+ASSERT (aminoacid_energies[0hex019] = 0hex01111);
+ASSERT (aminoacid_energies[0hex01A] = 0hex00011);
+ASSERT (aminoacid_energies[0hex01B] = 0hex01111);
+ASSERT (aminoacid_energies[0hex01C] = 0hex01111);
+ASSERT (aminoacid_energies[0hex01D] = 0hex01111);
+ASSERT (aminoacid_energies[0hex01E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex01F] = 0hex01111);
+ASSERT (aminoacid_energies[0hex020] = 0hex01111);
+ASSERT (aminoacid_energies[0hex021] = 0hex00011);
+ASSERT (aminoacid_energies[0hex022] = 0hex01111);
+ASSERT (aminoacid_energies[0hex023] = 0hex00011);
+ASSERT (aminoacid_energies[0hex024] = 0hex01111);
+ASSERT (aminoacid_energies[0hex025] = 0hex00011);
+ASSERT (aminoacid_energies[0hex026] = 0hex01111);
+ASSERT (aminoacid_energies[0hex027] = 0hex00011);
+ASSERT (aminoacid_energies[0hex028] = 0hex01111);
+ASSERT (aminoacid_energies[0hex029] = 0hex01111);
+ASSERT (aminoacid_energies[0hex02A] = 0hex00011);
+ASSERT (aminoacid_energies[0hex02B] = 0hex01111);
+ASSERT (aminoacid_energies[0hex02C] = 0hex00011);
+ASSERT (aminoacid_energies[0hex02D] = 0hex00011);
+ASSERT (aminoacid_energies[0hex02E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex02F] = 0hex01111);
+ASSERT (aminoacid_energies[0hex030] = 0hex00011);
+ASSERT (aminoacid_energies[0hex031] = 0hex01111);
+ASSERT (aminoacid_energies[0hex032] = 0hex00011);
+ASSERT (aminoacid_energies[0hex033] = 0hex01111);
+ASSERT (aminoacid_energies[0hex034] = 0hex00011);
+ASSERT (aminoacid_energies[0hex035] = 0hex01111);
+ASSERT (aminoacid_energies[0hex036] = 0hex00011);
+ASSERT (aminoacid_energies[0hex037] = 0hex01111);
+ASSERT (aminoacid_energies[0hex038] = 0hex00011);
+ASSERT (aminoacid_energies[0hex039] = 0hex01111);
+ASSERT (aminoacid_energies[0hex03A] = 0hex01111);
+ASSERT (aminoacid_energies[0hex03B] = 0hex00011);
+ASSERT (aminoacid_energies[0hex03C] = 0hex01111);
+ASSERT (aminoacid_energies[0hex03D] = 0hex00011);
+ASSERT (aminoacid_energies[0hex03E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex03F] = 0hex00011);
+ASSERT (aminoacid_energies[0hex040] = 0hex01111);
+ASSERT (aminoacid_energies[0hex041] = 0hex00011);
+ASSERT (aminoacid_energies[0hex042] = 0hex01111);
+ASSERT (aminoacid_energies[0hex043] = 0hex00011);
+ASSERT (aminoacid_energies[0hex044] = 0hex01111);
+ASSERT (aminoacid_energies[0hex045] = 0hex00011);
+ASSERT (aminoacid_energies[0hex046] = 0hex01111);
+ASSERT (aminoacid_energies[0hex047] = 0hex00011);
+ASSERT (aminoacid_energies[0hex048] = 0hex01111);
+ASSERT (aminoacid_energies[0hex049] = 0hex00011);
+ASSERT (aminoacid_energies[0hex04A] = 0hex01111);
+ASSERT (aminoacid_energies[0hex04B] = 0hex01111);
+ASSERT (aminoacid_energies[0hex04C] = 0hex01111);
+ASSERT (aminoacid_energies[0hex04D] = 0hex01111);
+ASSERT (aminoacid_energies[0hex04E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex04F] = 0hex01111);
+ASSERT (aminoacid_energies[0hex050] = 0hex01111);
+ASSERT (aminoacid_energies[0hex051] = 0hex00011);
+ASSERT (aminoacid_energies[0hex052] = 0hex01111);
+ASSERT (aminoacid_energies[0hex053] = 0hex00011);
+ASSERT (aminoacid_energies[0hex054] = 0hex01111);
+ASSERT (aminoacid_energies[0hex055] = 0hex00011);
+ASSERT (aminoacid_energies[0hex056] = 0hex01111);
+ASSERT (aminoacid_energies[0hex057] = 0hex00011);
+ASSERT (aminoacid_energies[0hex058] = 0hex01111);
+ASSERT (aminoacid_energies[0hex059] = 0hex01111);
+ASSERT (aminoacid_energies[0hex05A] = 0hex01111);
+ASSERT (aminoacid_energies[0hex05B] = 0hex00011);
+ASSERT (aminoacid_energies[0hex05C] = 0hex01111);
+ASSERT (aminoacid_energies[0hex05D] = 0hex00011);
+ASSERT (aminoacid_energies[0hex05E] = 0hex01111);
+ASSERT (aminoacid_energies[0hex05F] = 0hex01111);
+ASSERT (aminoacid_energies[0hex060] = 0hex00011);
+ASSERT (aminoacid_energies[0hex061] = 0hex01111);
+ASSERT (aminoacid_energies[0hex062] = 0hex01111);
+ASSERT (aminoacid_energies[0hex063] = 0hex00000);
+
+%%%%%%%%%%%%%% END OF AMINO ACID ENERGY ARRAY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF RUNG LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%
+
+ASSERT (alpha1_inner1_length = 0hex1 OR alpha1_inner1_length = 0hex2);
+ASSERT (alpha1_outer1_length = 0hex1 OR alpha1_outer1_length = 0hex2);
+ASSERT (alpha1_inner2_length = 0hex1 OR alpha1_inner2_length = 0hex2);
+ASSERT (alpha1_outer2_length = 0hex1 OR alpha1_outer2_length = 0hex2);
+ASSERT (alpha1_inner3_length = 0hex1 OR alpha1_inner3_length = 0hex2);
+ASSERT (alpha1_outer3_length = 0hex1 OR alpha1_outer3_length = 0hex2);
+
+ASSERT (alpha2_inner1_length = 0hex1 OR alpha2_inner1_length = 0hex2);
+ASSERT (alpha2_outer1_length = 0hex1 OR alpha2_outer1_length = 0hex2);
+ASSERT (alpha2_inner2_length = 0hex1 OR alpha2_inner2_length = 0hex2);
+ASSERT (alpha2_outer2_length = 0hex1 OR alpha2_outer2_length = 0hex2);
+ASSERT (alpha2_inner3_length = 0hex1 OR alpha2_inner3_length = 0hex2);
+ASSERT (alpha2_outer3_length = 0hex1 OR alpha2_outer3_length = 0hex2);
+
+ASSERT (alpha3_inner1_length = 0hex1 OR alpha3_inner1_length = 0hex2);
+ASSERT (alpha3_outer1_length = 0hex1 OR alpha3_outer1_length = 0hex2);
+ASSERT (alpha3_inner2_length = 0hex1 OR alpha3_inner2_length = 0hex2);
+ASSERT (alpha3_outer2_length = 0hex1 OR alpha3_outer2_length = 0hex2);
+ASSERT (alpha3_inner3_length = 0hex1 OR alpha3_inner3_length = 0hex2);
+ASSERT (alpha3_outer3_length = 0hex1 OR alpha3_outer3_length = 0hex2);
+
+ASSERT (alpha4_inner1_length = 0hex1 OR alpha4_inner1_length = 0hex2);
+ASSERT (alpha4_outer1_length = 0hex1 OR alpha4_outer1_length = 0hex2);
+ASSERT (alpha4_inner2_length = 0hex1 OR alpha4_inner2_length = 0hex2);
+ASSERT (alpha4_outer2_length = 0hex1 OR alpha4_outer2_length = 0hex2);
+ASSERT (alpha4_inner3_length = 0hex1 OR alpha4_inner3_length = 0hex2);
+ASSERT (alpha4_outer3_length = 0hex1 OR alpha4_outer3_length = 0hex2);
+
+
+ASSERT (BVPLUS(4, alpha1_inner1_length, alpha1_outer1_length, alpha1_inner2_length,
+                 alpha1_outer2_length, alpha1_inner3_length, alpha1_outer3_length) = 0hex9);
+ASSERT (BVPLUS(4, alpha2_inner1_length, alpha2_outer1_length, alpha2_inner2_length, 
+                 alpha2_outer2_length, alpha2_inner3_length, alpha2_outer3_length) = 0hex9);
+ASSERT (BVPLUS(4, alpha3_inner1_length, alpha3_outer1_length, alpha3_inner2_length, 
+                 alpha3_outer2_length, alpha3_inner3_length, alpha3_outer3_length) = 0hex9);
+ASSERT (BVPLUS(4, alpha4_inner1_length, alpha4_outer1_length, alpha4_inner2_length, 
+                 alpha4_outer2_length, alpha4_inner3_length, alpha4_outer3_length) = 0hex9);
 
 
-ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]);
-ASSERT (alpha1_inner1 = 0hex2 =>  
-       alpha1_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index]));
+ASSERT (BVPLUS(4, alpha1_inner1_length, alpha1_outer1_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha1_inner2_length, alpha1_outer2_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha1_inner3_length, alpha1_outer3_length) = 0hex3);
 
+ASSERT (BVPLUS(4, alpha2_inner1_length, alpha2_outer1_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha2_inner2_length, alpha2_outer2_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha2_inner3_length, alpha2_outer3_length) = 0hex3);
 
-ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer1_index]));
-ASSERT (alpha1_outer1 = 0hex2 =>
-       alpha1_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], aminoacid_energies[alpha1_outer1_index])));
+ASSERT (BVPLUS(4, alpha3_inner1_length, alpha3_outer1_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha3_inner2_length, alpha3_outer2_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha3_inner3_length, alpha3_outer3_length) = 0hex3);
 
+ASSERT (BVPLUS(4, alpha4_inner1_length, alpha4_outer1_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha4_inner2_length, alpha4_outer2_length) = 0hex3);
+ASSERT (BVPLUS(4, alpha4_inner3_length, alpha4_outer3_length) = 0hex3);
 
-ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]);
-ASSERT (alpha1_inner2 = 0hex2 =>
-       alpha1_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index]));
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF RUNG LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF COIL LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer2_index]));
-ASSERT (alpha1_outer2 = 0hex2 =>
-       alpha1_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], aminoacid_energies[alpha1_outer2_index])));
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF COIL LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha1_inner3 = 0hex1 => alpha1_inner3_energy = aminoacid_energies[alpha1_inner3_index]);
-ASSERT (alpha1_inner3 = 0hex2 =>
-       alpha1_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000001)],aminoacid_energies[alpha1_inner3_index]));
 
 
-ASSERT (alpha1_outer3 = 0hex1 => alpha1_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer3_index]));
-ASSERT (alpha1_outer3 = 0hex2 =>
-       alpha1_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer3_index,0hex00000001)], aminoacid_energies[alpha1_outer3_index])));
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF CHAINING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%ASSERT (BVLE(0hex
 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF CHAINING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]);
-ASSERT (alpha2_inner1 = 0hex2 =>  
-       alpha2_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index]));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer1_index]));
-ASSERT (alpha2_outer1 = 0hex2 =>
-       alpha2_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index])));
+ASSERT (alpha1_inner1_length = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]);
+ASSERT (alpha1_inner1_length = 0hex2 => alpha1_inner1_energy = BVPLUS(20,aminoacid_energies[alpha1_inner1_index],
+                                                                        aminoacid_energies[BVSUB(12,alpha1_inner1_index,0hex001)]));
 
+ASSERT (alpha1_outer1_length = 0hex1 => alpha1_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer1_index]));
+ASSERT (alpha1_outer1_length = 0hex2 => alpha1_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha1_outer1_index],
+                                                                                            aminoacid_energies[BVSUB(12,alpha1_outer1_index,0hex001)])));
 
-ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]);
-ASSERT (alpha2_inner2 = 0hex2 =>
-       alpha2_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index]));
 
+ASSERT (alpha1_inner2_length = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]);
+ASSERT (alpha1_inner2_length = 0hex2 => alpha1_inner2_energy = BVPLUS(20,aminoacid_energies[alpha1_inner2_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha1_inner2_index,0hex001)]));
 
-ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer2_index]));
-ASSERT (alpha2_outer2 = 0hex2 =>
-       alpha2_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index])));
 
+ASSERT (alpha1_outer2_length = 0hex1 => alpha1_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer2_index]));
+ASSERT (alpha1_outer2_length = 0hex2 => alpha1_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha1_outer2_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha1_outer2_index,0hex001)],)));
 
-ASSERT (alpha2_inner3 = 0hex1 => alpha2_inner3_energy = aminoacid_energies[alpha2_inner3_index]);
-ASSERT (alpha2_inner3 = 0hex2 =>
-       alpha2_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000001)],aminoacid_energies[alpha2_inner3_index]));
+ASSERT (alpha1_inner3_length = 0hex1 => alpha1_inner3_energy = aminoacid_energies[alpha1_inner3_index]);
+ASSERT (alpha1_inner3_length = 0hex2 => alpha1_inner3_energy = BVPLUS(20,aminoacid_energies[alpha1_inner3_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha1_inner3_index,0hex001)]));
 
 
-ASSERT (alpha2_outer3 = 0hex1 => alpha2_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer3_index]));
-ASSERT (alpha2_outer3 = 0hex2 =>
-       alpha2_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer3_index,0hex00000001)], aminoacid_energies[alpha2_outer3_index])));
+ASSERT (alpha1_outer3_length = 0hex1 => alpha1_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer3_index]));
+ASSERT (alpha1_outer3_length = 0hex2 => alpha1_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha1_outer3_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha1_outer3_index,0hex001)])));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]);
-ASSERT (alpha3_inner1 = 0hex2 =>  
-       alpha3_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index]));
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+ASSERT (alpha2_inner1_length = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]);
+ASSERT (alpha2_inner1_length = 0hex2 => alpha2_inner1_energy = BVPLUS(20,aminoacid_energies[alpha2_inner1_index],
+                                                                        aminoacid_energies[BVSUB(12,alpha2_inner1_index,0hex001)]));
 
-ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer1_index]));
-ASSERT (alpha3_outer1 = 0hex2 =>
-       alpha3_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], aminoacid_energies[alpha3_outer1_index])));
+ASSERT (alpha2_outer1_length = 0hex1 => alpha2_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer1_index]));
+ASSERT (alpha2_outer1_length = 0hex2 => alpha2_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha2_outer1_index],
+                                                                                            aminoacid_energies[BVSUB(12,alpha2_outer1_index,0hex001)])));
 
-% ASSERT (alpha3_outer1 = 0hex2 =>
-%      alpha3_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,0hex0, 0hex0)));
 
+ASSERT (alpha2_inner2_length = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]);
+ASSERT (alpha2_inner2_length = 0hex2 => alpha2_inner2_energy = BVPLUS(20,aminoacid_energies[alpha2_inner2_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha2_inner2_index,0hex001)]));
 
-ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]);
-ASSERT (alpha3_inner2 = 0hex2 =>
-       alpha3_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)],aminoacid_energies[alpha3_inner2_index]));
 
+ASSERT (alpha2_outer2_length = 0hex1 => alpha2_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer2_index]));
+ASSERT (alpha2_outer2_length = 0hex2 => alpha2_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha2_outer2_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha2_outer2_index,0hex001)],)));
 
-ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer2_index]));
-ASSERT (alpha3_outer2 = 0hex2 =>
-       alpha3_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], aminoacid_energies[alpha3_outer2_index])));
+ASSERT (alpha2_inner3_length = 0hex1 => alpha2_inner3_energy = aminoacid_energies[alpha2_inner3_index]);
+ASSERT (alpha2_inner3_length = 0hex2 => alpha2_inner3_energy = BVPLUS(20,aminoacid_energies[alpha2_inner3_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha2_inner3_index,0hex001)]));
 
 
-ASSERT (alpha3_inner3 = 0hex1 => alpha3_inner3_energy = aminoacid_energies[alpha3_inner3_index]);
-ASSERT (alpha3_inner3 = 0hex2 =>
-       alpha3_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000001)],aminoacid_energies[alpha3_inner3_index]));
+ASSERT (alpha2_outer3_length = 0hex1 => alpha2_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer3_index]));
+ASSERT (alpha2_outer3_length = 0hex2 => alpha2_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha2_outer3_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha2_outer3_index,0hex001)])));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha3_outer3 = 0hex1 => alpha3_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer3_index]));
-ASSERT (alpha3_outer3 = 0hex2 =>
-       alpha3_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer3_index,0hex00000001)], aminoacid_energies[alpha3_outer3_index])));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+ASSERT (alpha3_inner1_length = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]);
+ASSERT (alpha3_inner1_length = 0hex2 => alpha3_inner1_energy = BVPLUS(20,aminoacid_energies[alpha3_inner1_index],
+                                                                        aminoacid_energies[BVSUB(12,alpha3_inner1_index,0hex001)]));
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ASSERT (alpha3_outer1_length = 0hex1 => alpha3_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer1_index]));
+ASSERT (alpha3_outer1_length = 0hex2 => alpha3_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha3_outer1_index],
+                                                                                            aminoacid_energies[BVSUB(12,alpha3_outer1_index,0hex001)])));
 
-ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]);
-ASSERT (alpha4_inner1 = 0hex2 =>  
-       alpha4_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index]));
 
+ASSERT (alpha3_inner2_length = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]);
+ASSERT (alpha3_inner2_length = 0hex2 => alpha3_inner2_energy = BVPLUS(20,aminoacid_energies[alpha3_inner2_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha3_inner2_index,0hex001)]));
 
-ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer1_index]));
-ASSERT (alpha4_outer1 = 0hex2 =>
-       alpha4_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)], aminoacid_energies[alpha4_outer1_index])));
 
+ASSERT (alpha3_outer2_length = 0hex1 => alpha3_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer2_index]));
+ASSERT (alpha3_outer2_length = 0hex2 => alpha3_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha3_outer2_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha3_outer2_index,0hex001)],)));
 
-ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]);
-ASSERT (alpha4_inner2 = 0hex2 =>
-       alpha4_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index]));
+ASSERT (alpha3_inner3_length = 0hex1 => alpha3_inner3_energy = aminoacid_energies[alpha3_inner3_index]);
+ASSERT (alpha3_inner3_length = 0hex2 => alpha3_inner3_energy = BVPLUS(20,aminoacid_energies[alpha3_inner3_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha3_inner3_index,0hex001)]));
 
 
-ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer2_index]));
-ASSERT (alpha4_outer2 = 0hex2 =>
-       alpha4_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], aminoacid_energies[alpha4_outer2_index])));
+ASSERT (alpha3_outer3_length = 0hex1 => alpha3_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer3_index]));
+ASSERT (alpha3_outer3_length = 0hex2 => alpha3_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha3_outer3_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha3_outer3_index,0hex001)])));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha4_inner3 = 0hex1 => alpha4_inner3_energy = aminoacid_energies[alpha4_inner3_index]);
-ASSERT (alpha4_inner3 = 0hex2 =>
-       alpha4_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000001)],aminoacid_energies[alpha4_inner3_index]));
 
+%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA4 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (alpha4_outer3 = 0hex1 => alpha4_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer3_index]));
-ASSERT (alpha4_outer3 = 0hex2 =>
-       alpha4_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer3_index,0hex00000001)], aminoacid_energies[alpha4_outer3_index])));
+ASSERT (alpha4_inner1_length = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]);
+ASSERT (alpha4_inner1_length = 0hex2 => alpha4_inner1_energy = BVPLUS(20,aminoacid_energies[alpha4_inner1_index],
+                                                                        aminoacid_energies[BVSUB(12,alpha4_inner1_index,0hex001)]));
 
+ASSERT (alpha4_outer1_length = 0hex1 => alpha4_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer1_index]));
+ASSERT (alpha4_outer1_length = 0hex2 => alpha4_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha4_outer1_index],
+                                                                                            aminoacid_energies[BVSUB(12,alpha4_outer1_index,0hex001)])));
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-ASSERT (contact_energy12_zero = BVPLUS(64, alpha1_inner1_energy, alpha2_inner1_energy));
-ASSERT (contact_energy12_one  = BVPLUS(64, alpha1_inner2_energy, alpha2_inner2_energy));
-ASSERT (contact_energy12_two  = BVPLUS(64, alpha1_inner3_energy, alpha2_inner3_energy));
+ASSERT (alpha4_inner2_length = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]);
+ASSERT (alpha4_inner2_length = 0hex2 => alpha4_inner2_energy = BVPLUS(20,aminoacid_energies[alpha4_inner2_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha4_inner2_index,0hex001)]));
 
 
-ASSERT (contact_energy23_zero = BVPLUS(64, alpha2_inner1_energy, alpha3_inner1_energy));
-ASSERT (contact_energy23_one  = BVPLUS(64, alpha2_inner2_energy, alpha3_inner2_energy));
-ASSERT (contact_energy23_two  = BVPLUS(64, alpha2_inner3_energy, alpha3_inner3_energy));
+ASSERT (alpha4_outer2_length = 0hex1 => alpha4_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer2_index]));
+ASSERT (alpha4_outer2_length = 0hex2 => alpha4_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha4_outer2_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha4_outer2_index,0hex001)],)));
 
+ASSERT (alpha4_inner3_length = 0hex1 => alpha4_inner3_energy = aminoacid_energies[alpha4_inner3_index]);
+ASSERT (alpha4_inner3_length = 0hex2 => alpha4_inner3_energy = BVPLUS(20,aminoacid_energies[alpha4_inner3_index], 
+                                                                        aminoacid_energies[BVSUB(12,alpha4_inner3_index,0hex001)]));
 
-ASSERT (contact_energy34_zero = BVPLUS(64, alpha3_inner1_energy, alpha4_inner1_energy));
-ASSERT (contact_energy34_one  = BVPLUS(64, alpha3_inner2_energy, alpha4_inner2_energy));
-ASSERT (contact_energy34_two  = BVPLUS(64, alpha3_inner3_energy, alpha4_inner3_energy));
 
-ASSERT (contact_energy41_zero = BVPLUS(64, alpha4_inner1_energy, alpha1_inner1_energy));
-ASSERT (contact_energy41_one  = BVPLUS(64, alpha4_inner2_energy, alpha1_inner2_energy));
-ASSERT (contact_energy41_two  = BVPLUS(64, alpha4_inner3_energy, alpha1_inner3_energy));
+ASSERT (alpha4_outer3_length = 0hex1 => alpha4_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer3_index]));
+ASSERT (alpha4_outer3_length = 0hex2 => alpha4_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha4_outer3_index],
+                                                                                             aminoacid_energies[BVSUB(12,alpha4_outer3_index,0hex001)])));
 
-ASSERT (outer_energy = BVPLUS(64,  alpha1_outer1_energy, alpha1_outer2_energy, alpha1_outer3_energy, 
-                                  alpha2_outer1_energy, alpha2_outer2_energy, alpha2_outer3_energy,    
-                                  alpha3_outer1_energy, alpha3_outer2_energy, alpha3_outer3_energy,
-                                  alpha4_outer1_energy, alpha4_outer2_energy, alpha4_outer3_energy));
+%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA4 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 
-ASSERT (inner_energy = BVPLUS(64,  contact_energy12_zero, contact_energy12_one, contact_energy12_two,
+ASSERT (contact_energy12_zero = BVPLUS(32, 0hex000@alpha1_inner1_energy, 0hex000@alpha2_inner1_energy));
+ASSERT (contact_energy12_one  = BVPLUS(32, 0hex000@alpha1_inner2_energy, 0hex000@alpha2_inner2_energy));
+ASSERT (contact_energy12_two  = BVPLUS(32, 0hex000@alpha1_inner3_energy, 0hex000@alpha2_inner3_energy));
+
+
+ASSERT (contact_energy23_zero = BVPLUS(32, 0hex000@alpha2_inner1_energy, 0hex000@alpha3_inner1_energy));
+ASSERT (contact_energy23_one  = BVPLUS(32, 0hex000@alpha2_inner2_energy, 0hex000@alpha3_inner2_energy));
+ASSERT (contact_energy23_two  = BVPLUS(32, 0hex000@alpha2_inner3_energy, 0hex000@alpha3_inner3_energy));
+
+
+ASSERT (contact_energy34_zero = BVPLUS(32, 0hex000@alpha3_inner1_energy, 0hex000@alpha4_inner1_energy));
+ASSERT (contact_energy34_one  = BVPLUS(32, 0hex000@alpha3_inner2_energy, 0hex000@alpha4_inner2_energy));
+ASSERT (contact_energy34_two  = BVPLUS(32, 0hex000@alpha3_inner3_energy, 0hex000@alpha4_inner3_energy));
+
+ASSERT (contact_energy41_zero = BVPLUS(32, 0hex000@alpha4_inner1_energy, 0hex000@alpha1_inner1_energy));
+ASSERT (contact_energy41_one  = BVPLUS(32, 0hex000@alpha4_inner2_energy, 0hex000@alpha1_inner2_energy));
+ASSERT (contact_energy41_two  = BVPLUS(32, 0hex000@alpha4_inner3_energy, 0hex000@alpha1_inner3_energy));
+
+ASSERT (outer_energy = BVPLUS(32,  0hex000@alpha1_outer1_energy, 0hex000@alpha1_outer2_energy, 0hex000@alpha1_outer3_energy, 
+                                  0hex000@alpha2_outer1_energy, 0hex000@alpha2_outer2_energy, 0hex000@alpha2_outer3_energy,    
+                                  0hex000@alpha3_outer1_energy, 0hex000@alpha3_outer2_energy, 0hex000@alpha3_outer3_energy,
+                                  0hex000@alpha4_outer1_energy, 0hex000@alpha4_outer2_energy, 0hex000@alpha4_outer3_energy));
+
+
+ASSERT (inner_energy = BVPLUS(32,  contact_energy12_zero, contact_energy12_one, contact_energy12_two,
                                   contact_energy23_zero, contact_energy23_one, contact_energy23_two,
                                   contact_energy34_zero, contact_energy34_one, contact_energy34_two,
                                    contact_energy41_zero, contact_energy41_one, contact_energy41_two));
 
 
 % final query
-ASSERT (BVGE(BVPLUS(64,outer_energy,inner_energy), 0hex1111111111111110));
+ASSERT (BVGE(BVMULT(64,0hex00000000@outer_energy,0hex00000000@inner_energy), 0hex0011111111111110));
 QUERY FALSE;
\ No newline at end of file