c Boolean vector synthesis problem 2bitcomp_5 c n=4 m=1 k=5 A=16 c Specification: c 0 0 0 0 --> 1 c 0 0 0 1 --> 1 c 0 0 1 0 --> 1 c 0 0 1 1 --> 1 c 0 1 0 0 --> 0 c 0 1 0 1 --> 1 c 0 1 1 0 --> 1 c 0 1 1 1 --> 1 c 1 0 0 0 --> 0 c 1 0 0 1 --> 0 c 1 0 1 0 --> 1 c 1 0 1 1 --> 1 c 1 1 0 0 --> 0 c 1 1 0 1 --> 0 c 1 1 1 0 --> 0 c 1 1 1 1 --> 1 c Decision variables: c s[1][1] is 1 c s[1][2] is 2 c s[1][3] is 3 c s[1][4] is 4 c s[2][1] is 5 c s[2][2] is 6 c s[2][3] is 7 c s[2][4] is 8 c s[3][1] is 9 c s[3][2] is 10 c s[3][3] is 11 c s[3][4] is 12 c s[4][1] is 13 c s[4][2] is 14 c s[4][3] is 15 c s[4][4] is 16 c s[5][1] is 17 c s[5][2] is 18 c s[5][3] is 19 c s[5][4] is 20 c sp[1][1] is 21 c sp[1][2] is 22 c sp[1][3] is 23 c sp[1][4] is 24 c sp[2][1] is 25 c sp[2][2] is 26 c sp[2][3] is 27 c sp[2][4] is 28 c sp[3][1] is 29 c sp[3][2] is 30 c sp[3][3] is 31 c sp[3][4] is 32 c sp[4][1] is 33 c sp[4][2] is 34 c sp[4][3] is 35 c sp[4][4] is 36 c sp[5][1] is 37 c sp[5][2] is 38 c sp[5][3] is 39 c sp[5][4] is 40 c w[1][1] is 41 c w[2][1] is 42 c w[3][1] is 43 c w[4][1] is 44 c w[5][1] is 45 c Auxiliary variables: c z[1][1][1] is 46 c z[1][2][1] is 47 c z[1][3][1] is 48 c z[1][4][1] is 49 c z[1][5][1] is 50 c z[2][1][1] is 51 c z[2][2][1] is 52 c z[2][3][1] is 53 c z[2][4][1] is 54 c z[2][5][1] is 55 c z[3][1][1] is 56 c z[3][2][1] is 57 c z[3][3][1] is 58 c z[3][4][1] is 59 c z[3][5][1] is 60 c z[4][1][1] is 61 c z[4][2][1] is 62 c z[4][3][1] is 63 c z[4][4][1] is 64 c z[4][5][1] is 65 c z[5][1][1] is 66 c z[5][2][1] is 67 c z[5][3][1] is 68 c z[5][4][1] is 69 c z[5][5][1] is 70 c z[6][1][1] is 71 c z[6][2][1] is 72 c z[6][3][1] is 73 c z[6][4][1] is 74 c z[6][5][1] is 75 c z[7][1][1] is 76 c z[7][2][1] is 77 c z[7][3][1] is 78 c z[7][4][1] is 79 c z[7][5][1] is 80 c z[8][1][1] is 81 c z[8][2][1] is 82 c z[8][3][1] is 83 c z[8][4][1] is 84 c z[8][5][1] is 85 c z[9][1][1] is 86 c z[9][2][1] is 87 c z[9][3][1] is 88 c z[9][4][1] is 89 c z[9][5][1] is 90 c z[10][1][1] is 91 c z[10][2][1] is 92 c z[10][3][1] is 93 c z[10][4][1] is 94 c z[10][5][1] is 95 c z[11][1][1] is 96 c z[11][2][1] is 97 c z[11][3][1] is 98 c z[11][4][1] is 99 c z[11][5][1] is 100 c z[12][1][1] is 101 c z[12][2][1] is 102 c z[12][3][1] is 103 c z[12][4][1] is 104 c z[12][5][1] is 105 c z[13][1][1] is 106 c z[13][2][1] is 107 c z[13][3][1] is 108 c z[13][4][1] is 109 c z[13][5][1] is 110 c z[14][1][1] is 111 c z[14][2][1] is 112 c z[14][3][1] is 113 c z[14][4][1] is 114 c z[14][5][1] is 115 c z[15][1][1] is 116 c z[15][2][1] is 117 c z[15][3][1] is 118 c z[15][4][1] is 119 c z[15][5][1] is 120 c z[16][1][1] is 121 c z[16][2][1] is 122 c z[16][3][1] is 123 c z[16][4][1] is 124 c z[16][5][1] is 125 p cnf 125 310 1 21 0 5 25 0 9 29 0 13 33 0 17 37 0 2 22 0 6 26 0 10 30 0 14 34 0 18 38 0 3 23 0 7 27 0 11 31 0 15 35 0 19 39 0 4 24 0 8 28 0 12 32 0 16 36 0 20 40 0 -41 -1 -22 -3 -4 0 -42 -5 -26 -7 -8 0 -43 -9 -30 -11 -12 0 -44 -13 -34 -15 -16 0 -45 -17 -38 -19 -20 0 -41 -21 -2 -3 -4 0 -42 -25 -6 -7 -8 0 -43 -29 -10 -11 -12 0 -44 -33 -14 -15 -16 0 -45 -37 -18 -19 -20 0 -41 -21 -2 -3 -24 0 -42 -25 -6 -7 -28 0 -43 -29 -10 -11 -32 0 -44 -33 -14 -15 -36 0 -45 -37 -18 -19 -40 0 -41 -21 -22 -3 -4 0 -42 -25 -26 -7 -8 0 -43 -29 -30 -11 -12 0 -44 -33 -34 -15 -16 0 -45 -37 -38 -19 -20 0 -41 -21 -22 -3 -24 0 -42 -25 -26 -7 -28 0 -43 -29 -30 -11 -32 0 -44 -33 -34 -15 -36 0 -45 -37 -38 -19 -40 0 -41 -21 -22 -23 -4 0 -42 -25 -26 -27 -8 0 -43 -29 -30 -31 -12 0 -44 -33 -34 -35 -16 0 -45 -37 -38 -39 -20 0 46 47 48 49 50 0 51 52 53 54 55 0 56 57 58 59 60 0 61 62 63 64 65 0 71 72 73 74 75 0 76 77 78 79 80 0 81 82 83 84 85 0 96 97 98 99 100 0 101 102 103 104 105 0 121 122 123 124 125 0 -46 41 0 -47 42 0 -48 43 0 -49 44 0 -50 45 0 -51 41 0 -52 42 0 -53 43 0 -54 44 0 -55 45 0 -56 41 0 -57 42 0 -58 43 0 -59 44 0 -60 45 0 -61 41 0 -62 42 0 -63 43 0 -64 44 0 -65 45 0 -71 41 0 -72 42 0 -73 43 0 -74 44 0 -75 45 0 -76 41 0 -77 42 0 -78 43 0 -79 44 0 -80 45 0 -81 41 0 -82 42 0 -83 43 0 -84 44 0 -85 45 0 -96 41 0 -97 42 0 -98 43 0 -99 44 0 -100 45 0 -101 41 0 -102 42 0 -103 43 0 -104 44 0 -105 45 0 -121 41 0 -122 42 0 -123 43 0 -124 44 0 -125 45 0 -46 1 0 -47 5 0 -48 9 0 -49 13 0 -50 17 0 -46 2 0 -47 6 0 -48 10 0 -49 14 0 -50 18 0 -46 3 0 -47 7 0 -48 11 0 -49 15 0 -50 19 0 -46 4 0 -47 8 0 -48 12 0 -49 16 0 -50 20 0 -51 1 0 -52 5 0 -53 9 0 -54 13 0 -55 17 0 -51 2 0 -52 6 0 -53 10 0 -54 14 0 -55 18 0 -51 3 0 -52 7 0 -53 11 0 -54 15 0 -55 19 0 -51 24 0 -52 28 0 -53 32 0 -54 36 0 -55 40 0 -56 1 0 -57 5 0 -58 9 0 -59 13 0 -60 17 0 -56 2 0 -57 6 0 -58 10 0 -59 14 0 -60 18 0 -56 23 0 -57 27 0 -58 31 0 -59 35 0 -60 39 0 -56 4 0 -57 8 0 -58 12 0 -59 16 0 -60 20 0 -61 1 0 -62 5 0 -63 9 0 -64 13 0 -65 17 0 -61 2 0 -62 6 0 -63 10 0 -64 14 0 -65 18 0 -61 23 0 -62 27 0 -63 31 0 -64 35 0 -65 39 0 -61 24 0 -62 28 0 -63 32 0 -64 36 0 -65 40 0 -71 1 0 -72 5 0 -73 9 0 -74 13 0 -75 17 0 -71 22 0 -72 26 0 -73 30 0 -74 34 0 -75 38 0 -71 3 0 -72 7 0 -73 11 0 -74 15 0 -75 19 0 -71 24 0 -72 28 0 -73 32 0 -74 36 0 -75 40 0 -76 1 0 -77 5 0 -78 9 0 -79 13 0 -80 17 0 -76 22 0 -77 26 0 -78 30 0 -79 34 0 -80 38 0 -76 23 0 -77 27 0 -78 31 0 -79 35 0 -80 39 0 -76 4 0 -77 8 0 -78 12 0 -79 16 0 -80 20 0 -81 1 0 -82 5 0 -83 9 0 -84 13 0 -85 17 0 -81 22 0 -82 26 0 -83 30 0 -84 34 0 -85 38 0 -81 23 0 -82 27 0 -83 31 0 -84 35 0 -85 39 0 -81 24 0 -82 28 0 -83 32 0 -84 36 0 -85 40 0 -96 21 0 -97 25 0 -98 29 0 -99 33 0 -100 37 0 -96 2 0 -97 6 0 -98 10 0 -99 14 0 -100 18 0 -96 23 0 -97 27 0 -98 31 0 -99 35 0 -100 39 0 -96 4 0 -97 8 0 -98 12 0 -99 16 0 -100 20 0 -101 21 0 -102 25 0 -103 29 0 -104 33 0 -105 37 0 -101 2 0 -102 6 0 -103 10 0 -104 14 0 -105 18 0 -101 23 0 -102 27 0 -103 31 0 -104 35 0 -105 39 0 -101 24 0 -102 28 0 -103 32 0 -104 36 0 -105 40 0 -121 21 0 -122 25 0 -123 29 0 -124 33 0 -125 37 0 -121 22 0 -122 26 0 -123 30 0 -124 34 0 -125 38 0 -121 23 0 -122 27 0 -123 31 0 -124 35 0 -125 39 0 -121 24 0 -122 28 0 -123 32 0 -124 36 0 -125 40 0