c Filename: ii8a2.sat c c Source: Mauricio Resende (AT&T Bell Labs) (mgcr@gauss.att.com) c c Reference: "A continuous approach to inductive inference" by c Kamath, Karmarkar, Ramakrishnan, and Resende (Math Prog 57, c 215--238) (1992). c c Note: Instance is satisfiable c p cnf 180 800 1 2 0 3 4 0 5 6 0 7 8 0 9 10 0 11 12 0 13 14 0 15 16 0 17 18 0 19 20 0 21 22 0 23 24 0 25 26 0 27 28 0 29 30 0 31 32 0 33 34 0 35 36 0 37 38 0 39 40 0 41 42 0 43 44 0 45 46 0 47 48 0 49 50 0 51 52 0 53 54 0 55 56 0 57 58 0 59 60 0 61 62 0 63 64 0 65 66 0 67 68 0 69 70 0 71 72 0 73 74 0 75 76 0 77 78 0 79 80 0 81 82 0 83 84 0 85 86 0 87 88 0 89 90 0 91 92 0 93 94 0 95 96 0 -2 -3 -6 -8 -9 -12 -14 -16 0 -18 -19 -22 -24 -25 -28 -30 -32 0 -34 -35 -38 -40 -41 -44 -46 -48 0 -50 -51 -54 -56 -57 -60 -62 -64 0 -66 -67 -70 -72 -73 -76 -78 -80 0 -82 -83 -86 -88 -89 -92 -94 -96 0 -1 -4 -6 -7 -10 -11 -13 -16 0 -17 -20 -22 -23 -26 -27 -29 -32 0 -33 -36 -38 -39 -42 -43 -45 -48 0 -49 -52 -54 -55 -58 -59 -61 -64 0 -65 -68 -70 -71 -74 -75 -77 -80 0 -81 -84 -86 -87 -90 -91 -93 -96 0 -2 -3 -6 -8 -9 -11 -14 -15 0 -18 -19 -22 -24 -25 -27 -30 -31 0 -34 -35 -38 -40 -41 -43 -46 -47 0 -50 -51 -54 -56 -57 -59 -62 -63 0 -66 -67 -70 -72 -73 -75 -78 -79 0 -82 -83 -86 -88 -89 -91 -94 -95 0 -1 -3 -5 -7 -9 -12 -13 -15 0 -17 -19 -21 -23 -25 -28 -29 -31 0 -33 -35 -37 -39 -41 -44 -45 -47 0 -49 -51 -53 -55 -57 -60 -61 -63 0 -65 -67 -69 -71 -73 -76 -77 -79 0 -81 -83 -85 -87 -89 -92 -93 -95 0 -2 -3 -6 -7 -9 -11 -13 -16 0 -18 -19 -22 -23 -25 -27 -29 -32 0 -34 -35 -38 -39 -41 -43 -45 -48 0 -50 -51 -54 -55 -57 -59 -61 -64 0 -66 -67 -70 -71 -73 -75 -77 -80 0 -82 -83 -86 -87 -89 -91 -93 -96 0 -1 -4 -6 -8 -10 -11 -14 -16 0 -17 -20 -22 -24 -26 -27 -30 -32 0 -33 -36 -38 -40 -42 -43 -46 -48 0 -49 -52 -54 -56 -58 -59 -62 -64 0 -65 -68 -70 -72 -74 -75 -78 -80 0 -81 -84 -86 -88 -90 -91 -94 -96 0 -1 -4 -5 -7 -10 -11 -13 -15 0 -17 -20 -21 -23 -26 -27 -29 -31 0 -33 -36 -37 -39 -42 -43 -45 -47 0 -49 -52 -53 -55 -58 -59 -61 -63 0 -65 -68 -69 -71 -74 -75 -77 -79 0 -81 -84 -85 -87 -90 -91 -93 -95 0 -2 -3 -6 -7 -10 -11 -13 -15 0 -18 -19 -22 -23 -26 -27 -29 -31 0 -34 -35 -38 -39 -42 -43 -45 -47 0 -50 -51 -54 -55 -58 -59 -61 -63 0 -66 -67 -70 -71 -74 -75 -77 -79 0 -82 -83 -86 -87 -90 -91 -93 -95 0 -1 -3 -5 -7 -9 -11 -14 -16 0 -17 -19 -21 -23 -25 -27 -30 -32 0 -33 -35 -37 -39 -41 -43 -46 -48 0 -49 -51 -53 -55 -57 -59 -62 -64 0 -65 -67 -69 -71 -73 -75 -78 -80 0 -81 -83 -85 -87 -89 -91 -94 -96 0 -1 -4 -6 -7 -9 -11 -14 -16 0 -17 -20 -22 -23 -25 -27 -30 -32 0 -33 -36 -38 -39 -41 -43 -46 -48 0 -49 -52 -54 -55 -57 -59 -62 -64 0 -65 -68 -70 -71 -73 -75 -78 -80 0 -81 -84 -86 -87 -89 -91 -94 -96 0 -2 -3 -6 -8 -9 -11 -14 -15 0 -18 -19 -22 -24 -25 -27 -30 -31 0 -34 -35 -38 -40 -41 -43 -46 -47 0 -50 -51 -54 -56 -57 -59 -62 -63 0 -66 -67 -70 -72 -73 -75 -78 -79 0 -82 -83 -86 -88 -89 -91 -94 -95 0 1 -97 0 3 -97 0 5 -97 0 8 -97 0 10 -97 0 11 -97 0 13 -97 0 15 -97 0 17 -98 0 19 -98 0 21 -98 0 24 -98 0 26 -98 0 27 -98 0 29 -98 0 31 -98 0 33 -99 0 35 -99 0 37 -99 0 40 -99 0 42 -99 0 43 -99 0 45 -99 0 47 -99 0 49 -100 0 51 -100 0 53 -100 0 56 -100 0 58 -100 0 59 -100 0 61 -100 0 63 -100 0 65 -101 0 67 -101 0 69 -101 0 72 -101 0 74 -101 0 75 -101 0 77 -101 0 79 -101 0 81 -102 0 83 -102 0 85 -102 0 88 -102 0 90 -102 0 91 -102 0 93 -102 0 95 -102 0 2 -103 0 3 -103 0 6 -103 0 8 -103 0 9 -103 0 12 -103 0 13 -103 0 16 -103 0 18 -104 0 19 -104 0 22 -104 0 24 -104 0 25 -104 0 28 -104 0 29 -104 0 32 -104 0 34 -105 0 35 -105 0 38 -105 0 40 -105 0 41 -105 0 44 -105 0 45 -105 0 48 -105 0 50 -106 0 51 -106 0 54 -106 0 56 -106 0 57 -106 0 60 -106 0 61 -106 0 64 -106 0 66 -107 0 67 -107 0 70 -107 0 72 -107 0 73 -107 0 76 -107 0 77 -107 0 80 -107 0 82 -108 0 83 -108 0 86 -108 0 88 -108 0 89 -108 0 92 -108 0 93 -108 0 96 -108 0 2 -109 0 4 -109 0 5 -109 0 8 -109 0 10 -109 0 11 -109 0 13 -109 0 16 -109 0 18 -110 0 20 -110 0 21 -110 0 24 -110 0 26 -110 0 27 -110 0 29 -110 0 32 -110 0 34 -111 0 36 -111 0 37 -111 0 40 -111 0 42 -111 0 43 -111 0 45 -111 0 48 -111 0 50 -112 0 52 -112 0 53 -112 0 56 -112 0 58 -112 0 59 -112 0 61 -112 0 64 -112 0 66 -113 0 68 -113 0 69 -113 0 72 -113 0 74 -113 0 75 -113 0 77 -113 0 80 -113 0 82 -114 0 84 -114 0 85 -114 0 88 -114 0 90 -114 0 91 -114 0 93 -114 0 96 -114 0 2 -115 0 4 -115 0 5 -115 0 7 -115 0 9 -115 0 11 -115 0 14 -115 0 15 -115 0 18 -116 0 20 -116 0 21 -116 0 23 -116 0 25 -116 0 27 -116 0 30 -116 0 31 -116 0 34 -117 0 36 -117 0 37 -117 0 39 -117 0 41 -117 0 43 -117 0 46 -117 0 47 -117 0 50 -118 0 52 -118 0 53 -118 0 55 -118 0 57 -118 0 59 -118 0 62 -118 0 63 -118 0 66 -119 0 68 -119 0 69 -119 0 71 -119 0 73 -119 0 75 -119 0 78 -119 0 79 -119 0 82 -120 0 84 -120 0 85 -120 0 87 -120 0 89 -120 0 91 -120 0 94 -120 0 95 -120 0 1 -121 0 3 -121 0 5 -121 0 8 -121 0 9 -121 0 11 -121 0 13 -121 0 16 -121 0 17 -122 0 19 -122 0 21 -122 0 24 -122 0 25 -122 0 27 -122 0 29 -122 0 32 -122 0 33 -123 0 35 -123 0 37 -123 0 40 -123 0 41 -123 0 43 -123 0 45 -123 0 48 -123 0 49 -124 0 51 -124 0 53 -124 0 56 -124 0 57 -124 0 59 -124 0 61 -124 0 64 -124 0 65 -125 0 67 -125 0 69 -125 0 72 -125 0 73 -125 0 75 -125 0 77 -125 0 80 -125 0 81 -126 0 83 -126 0 85 -126 0 88 -126 0 89 -126 0 91 -126 0 93 -126 0 96 -126 0 1 -127 0 4 -127 0 5 -127 0 8 -127 0 10 -127 0 12 -127 0 14 -127 0 16 -127 0 17 -128 0 20 -128 0 21 -128 0 24 -128 0 26 -128 0 28 -128 0 30 -128 0 32 -128 0 33 -129 0 36 -129 0 37 -129 0 40 -129 0 42 -129 0 44 -129 0 46 -129 0 48 -129 0 49 -130 0 52 -130 0 53 -130 0 56 -130 0 58 -130 0 60 -130 0 62 -130 0 64 -130 0 65 -131 0 68 -131 0 69 -131 0 72 -131 0 74 -131 0 76 -131 0 78 -131 0 80 -131 0 81 -132 0 84 -132 0 85 -132 0 88 -132 0 90 -132 0 92 -132 0 94 -132 0 96 -132 0 1 -133 0 4 -133 0 5 -133 0 8 -133 0 10 -133 0 11 -133 0 13 -133 0 16 -133 0 17 -134 0 20 -134 0 21 -134 0 24 -134 0 26 -134 0 27 -134 0 29 -134 0 32 -134 0 33 -135 0 36 -135 0 37 -135 0 40 -135 0 42 -135 0 43 -135 0 45 -135 0 48 -135 0 49 -136 0 52 -136 0 53 -136 0 56 -136 0 58 -136 0 59 -136 0 61 -136 0 64 -136 0 65 -137 0 68 -137 0 69 -137 0 72 -137 0 74 -137 0 75 -137 0 77 -137 0 80 -137 0 81 -138 0 84 -138 0 85 -138 0 88 -138 0 90 -138 0 91 -138 0 93 -138 0 96 -138 0 2 -139 0 3 -139 0 5 -139 0 8 -139 0 10 -139 0 11 -139 0 13 -139 0 16 -139 0 18 -140 0 19 -140 0 21 -140 0 24 -140 0 26 -140 0 27 -140 0 29 -140 0 32 -140 0 34 -141 0 35 -141 0 37 -141 0 40 -141 0 42 -141 0 43 -141 0 45 -141 0 48 -141 0 50 -142 0 51 -142 0 53 -142 0 56 -142 0 58 -142 0 59 -142 0 61 -142 0 64 -142 0 66 -143 0 67 -143 0 69 -143 0 72 -143 0 74 -143 0 75 -143 0 77 -143 0 80 -143 0 82 -144 0 83 -144 0 85 -144 0 88 -144 0 90 -144 0 91 -144 0 93 -144 0 96 -144 0 1 -145 0 3 -145 0 6 -145 0 8 -145 0 9 -145 0 11 -145 0 13 -145 0 15 -145 0 17 -146 0 19 -146 0 22 -146 0 24 -146 0 25 -146 0 27 -146 0 29 -146 0 31 -146 0 33 -147 0 35 -147 0 38 -147 0 40 -147 0 41 -147 0 43 -147 0 45 -147 0 47 -147 0 49 -148 0 51 -148 0 54 -148 0 56 -148 0 57 -148 0 59 -148 0 61 -148 0 63 -148 0 65 -149 0 67 -149 0 70 -149 0 72 -149 0 73 -149 0 75 -149 0 77 -149 0 79 -149 0 81 -150 0 83 -150 0 86 -150 0 88 -150 0 89 -150 0 91 -150 0 93 -150 0 95 -150 0 1 -151 0 3 -151 0 6 -151 0 8 -151 0 10 -151 0 12 -151 0 13 -151 0 15 -151 0 17 -152 0 19 -152 0 22 -152 0 24 -152 0 26 -152 0 28 -152 0 29 -152 0 31 -152 0 33 -153 0 35 -153 0 38 -153 0 40 -153 0 42 -153 0 44 -153 0 45 -153 0 47 -153 0 49 -154 0 51 -154 0 54 -154 0 56 -154 0 58 -154 0 60 -154 0 61 -154 0 63 -154 0 65 -155 0 67 -155 0 70 -155 0 72 -155 0 74 -155 0 76 -155 0 77 -155 0 79 -155 0 81 -156 0 83 -156 0 86 -156 0 88 -156 0 90 -156 0 92 -156 0 93 -156 0 95 -156 0 2 -157 0 3 -157 0 5 -157 0 8 -157 0 9 -157 0 12 -157 0 14 -157 0 16 -157 0 18 -158 0 19 -158 0 21 -158 0 24 -158 0 25 -158 0 28 -158 0 30 -158 0 32 -158 0 34 -159 0 35 -159 0 37 -159 0 40 -159 0 41 -159 0 44 -159 0 46 -159 0 48 -159 0 50 -160 0 51 -160 0 53 -160 0 56 -160 0 57 -160 0 60 -160 0 62 -160 0 64 -160 0 66 -161 0 67 -161 0 69 -161 0 72 -161 0 73 -161 0 76 -161 0 78 -161 0 80 -161 0 82 -162 0 83 -162 0 85 -162 0 88 -162 0 89 -162 0 92 -162 0 94 -162 0 96 -162 0 1 -163 0 4 -163 0 5 -163 0 8 -163 0 10 -163 0 12 -163 0 13 -163 0 16 -163 0 17 -164 0 20 -164 0 21 -164 0 24 -164 0 26 -164 0 28 -164 0 29 -164 0 32 -164 0 33 -165 0 36 -165 0 37 -165 0 40 -165 0 42 -165 0 44 -165 0 45 -165 0 48 -165 0 49 -166 0 52 -166 0 53 -166 0 56 -166 0 58 -166 0 60 -166 0 61 -166 0 64 -166 0 65 -167 0 68 -167 0 69 -167 0 72 -167 0 74 -167 0 76 -167 0 77 -167 0 80 -167 0 81 -168 0 84 -168 0 85 -168 0 88 -168 0 90 -168 0 92 -168 0 93 -168 0 96 -168 0 2 -169 0 4 -169 0 5 -169 0 7 -169 0 10 -169 0 11 -169 0 14 -169 0 15 -169 0 18 -170 0 20 -170 0 21 -170 0 23 -170 0 26 -170 0 27 -170 0 30 -170 0 31 -170 0 34 -171 0 36 -171 0 37 -171 0 39 -171 0 42 -171 0 43 -171 0 46 -171 0 47 -171 0 50 -172 0 52 -172 0 53 -172 0 55 -172 0 58 -172 0 59 -172 0 62 -172 0 63 -172 0 66 -173 0 68 -173 0 69 -173 0 71 -173 0 74 -173 0 75 -173 0 78 -173 0 79 -173 0 82 -174 0 84 -174 0 85 -174 0 87 -174 0 90 -174 0 91 -174 0 94 -174 0 95 -174 0 1 -175 0 3 -175 0 6 -175 0 8 -175 0 9 -175 0 11 -175 0 13 -175 0 16 -175 0 17 -176 0 19 -176 0 22 -176 0 24 -176 0 25 -176 0 27 -176 0 29 -176 0 32 -176 0 33 -177 0 35 -177 0 38 -177 0 40 -177 0 41 -177 0 43 -177 0 45 -177 0 48 -177 0 49 -178 0 51 -178 0 54 -178 0 56 -178 0 57 -178 0 59 -178 0 61 -178 0 64 -178 0 65 -179 0 67 -179 0 70 -179 0 72 -179 0 73 -179 0 75 -179 0 77 -179 0 80 -179 0 81 -180 0 83 -180 0 86 -180 0 88 -180 0 89 -180 0 91 -180 0 93 -180 0 96 -180 0 97 98 99 100 101 102 0 103 104 105 106 107 108 0 109 110 111 112 113 114 0 115 116 117 118 119 120 0 121 122 123 124 125 126 0 127 128 129 130 131 132 0 133 134 135 136 137 138 0 139 140 141 142 143 144 0 145 146 147 148 149 150 0 151 152 153 154 155 156 0 157 158 159 160 161 162 0 163 164 165 166 167 168 0 169 170 171 172 173 174 0 175 176 177 178 179 180 0