c NOTE: Not Satisfiable c p cnf 200 400 22 101 108 0 22 108 130 0 21 -22 178 0 9 37 90 0 9 -37 178 0 8 165 -178 0 90 165 -178 0 26 -90 165 0 -26 -90 145 0 -22 -90 -145 0 44 105 144 0 44 -105 -165 0 130 -144 -165 0 -22 -44 130 0 112 162 183 0 -130 162 -183 0 -112 -130 162 0 39 147 -162 0 9 -39 147 0 108 -130 -147 0 73 131 189 0 74 -131 189 0 73 74 -189 0 -13 73 -189 0 -74 -108 186 0 -74 155 -186 0 -74 -155 -186 0 61 -73 -108 0 -61 -73 -108 0 12 24 35 0 65 89 139 0 -35 -89 139 0 -35 65 -139 0 12 -65 100 0 -12 24 28 0 -12 28 -72 0 -12 -28 155 0 -28 81 100 0 -81 100 -155 0 6 -9 24 0 -6 -9 -100 0 35 48 115 0 -48 171 188 0 35 171 -188 0 -48 143 -171 0 -35 115 143 0 72 -143 156 0 16 -143 -156 0 115 -143 -156 0 -24 79 148 0 12 -115 -148 0 4 38 137 0 11 -115 -148 0 -4 -11 38 0 -38 79 137 0 -115 -137 -148 0 -24 -79 170 0 72 -79 -170 0 -9 -72 79 0 -24 -72 -79 0 -75 107 -113 0 -46 122 -150 0 -23 83 183 0 -23 -83 183 0 71 146 151 0 52 146 151 0 -23 -146 151 0 22 87 -183 0 52 97 141 0 52 -151 -191 0 -97 141 -151 0 87 -141 159 0 -141 -159 -183 0 -57 160 -162 0 66 -161 199 0 66 -87 -161 0 21 -161 199 0 -78 84 -181 0 -71 -84 131 0 -84 -131 189 0 -84 161 -189 0 14 132 149 0 14 67 -132 0 -14 67 149 0 -5 47 135 0 -5 -18 154 0 -18 -47 -154 0 42 -57 69 0 122 186 193 0 122 -186 193 0 -122 184 193 0 -122 138 -184 0 135 -138 -184 0 135 -178 -184 0 15 -100 -155 0 -15 65 -98 0 -15 -65 195 0 -60 -103 127 0 -60 -103 -127 0 29 -65 -162 0 51 -107 -149 0 -51 -107 -149 0 -80 -124 -149 0 38 94 -160 0 -38 -110 -160 0 32 -53 196 0 -32 136 196 0 27 56 153 0 -16 50 80 0 -16 -80 143 0 113 119 -200 0 53 -113 -200 0 31 94 127 0 66 -98 -142 0 -66 93 -98 0 -31 -66 -93 0 -78 176 178 0 -114 116 182 0 163 -182 -197 0 -114 116 -163 0 -21 97 126 0 -21 -110 -126 0 -21 -97 -165 0 17 -106 139 0 17 -139 195 0 21 31 195 0 16 -17 -31 0 -16 -17 -31 0 18 -88 150 0 -75 133 177 0 -75 -133 177 0 -51 -73 180 0 -36 76 156 0 111 137 -157 0 129 -171 199 0 31 -37 197 0 -37 -52 -197 0 -8 -15 129 0 39 -85 112 0 -80 -110 138 0 17 48 159 0 -41 -157 -159 0 -17 48 -157 0 90 -105 -170 0 -101 160 -176 0 13 28 -193 0 13 43 -137 0 -8 50 106 0 50 -106 -151 0 -6 97 -170 0 -52 109 155 0 -38 -52 109 0 -87 -139 -173 0 -13 -36 -77 0 -85 164 190 0 33 -85 -190 0 -3 80 -197 0 10 111 -164 0 62 -142 161 0 32 74 -125 0 126 -158 191 0 -45 -97 134 0 78 116 170 0 -8 167 -190 0 -40 59 145 0 -59 -112 166 0 -40 -112 -166 0 47 88 173 0 47 173 -185 0 -3 -42 -150 0 -117 -150 187 0 -10 -113 141 0 -64 -94 -138 0 -49 71 192 0 20 -71 176 0 -20 -71 192 0 -49 -94 176 0 -30 76 -180 0 -18 -30 -76 0 -43 -69 158 0 -43 -69 -158 0 -58 82 182 0 -58 182 198 0 -58 -82 -198 0 59 -94 -126 0 -59 -126 -164 0 166 -182 186 0 8 -26 -39 0 -26 -39 -122 0 41 120 192 0 -19 -34 -49 0 -56 63 -164 0 42 128 133 0 104 107 -193 0 -103 104 -107 0 -50 147 164 0 -50 164 181 0 -41 -50 -181 0 18 44 -152 0 4 83 96 0 -4 83 -156 0 -129 -145 -200 0 7 58 -176 0 7 -61 185 0 -44 -109 112 0 110 120 166 0 -124 169 185 0 119 -169 185 0 -119 -124 157 0 -32 124 -142 0 88 120 -138 0 -33 -66 123 0 -33 70 -123 0 -34 -163 174 0 18 110 -123 0 -105 138 -160 0 8 -100 -180 0 107 -188 -194 0 13 -28 -176 0 -11 41 105 0 127 -169 172 0 81 179 -194 0 -2 -152 167 0 -19 42 188 0 95 113 128 0 57 88 174 0 11 36 121 0 84 -136 -180 0 -5 77 -102 0 -48 -114 117 0 -47 95 129 0 -47 -95 177 0 64 157 -158 0 41 -64 157 0 86 -191 200 0 -13 -96 -128 0 2 -10 -145 0 -46 75 153 0 54 75 -153 0 -46 54 133 0 14 -53 69 0 4 -42 152 0 -82 152 -177 0 -42 -82 -152 0 59 61 -81 0 -11 29 49 0 103 128 -166 0 10 113 197 0 15 -68 71 0 -83 91 -199 0 -96 -104 191 0 10 -104 -191 0 -96 -104 -147 0 55 109 144 0 20 -167 172 0 -1 -54 102 0 67 163 -182 0 136 -154 -198 0 96 104 174 0 43 96 -174 0 -43 -57 -174 0 -102 169 196 0 57 93 -120 0 -3 6 -54 0 6 -44 -199 0 -109 -140 -177 0 55 -101 -171 0 29 91 -179 0 -89 99 -173 0 5 167 200 0 5 -167 200 0 26 -111 136 0 26 -111 150 0 55 -111 -136 0 36 -76 -136 0 -29 82 188 0 105 148 179 0 -2 -53 159 0 -2 39 -159 0 15 131 156 0 -29 -120 -163 0 45 70 101 0 70 -101 126 0 -10 82 95 0 -14 69 170 0 -34 45 168 0 3 146 191 0 2 -61 -95 0 5 7 149 0 -19 34 98 0 75 -121 134 0 45 60 -185 0 -60 -135 -166 0 49 -67 180 0 -36 101 171 0 -20 -56 -185 0 20 49 -190 0 36 -123 154 0 -51 54 118 0 25 140 -153 0 -56 -132 163 0 -29 -93 119 0 -78 -169 172 0 51 53 78 0 93 -109 -116 0 -45 68 86 0 -95 -119 173 0 37 91 -199 0 -63 85 124 0 62 -127 -188 0 85 -129 -141 0 89 -89 -146 0 11 161 -179 0 -30 34 -117 0 56 92 -120 0 -25 -195 198 0 -121 -134 152 0 30 -102 -134 0 -118 -140 145 0 -64 89 114 0 -68 117 198 0 -27 57 -195 0 61 -144 -177 0 27 -125 140 0 46 -175 -194 0 -67 106 -192 0 111 -132 154 0 40 -54 -153 0 3 -77 -172 0 187 190 -193 0 160 -172 -187 0 33 99 121 0 27 43 63 0 -27 -63 -93 0 -67 -70 142 0 68 -134 184 0 -119 -187 190 0 1 53 194 0 -121 142 175 0 32 110 123 0 2 -7 -86 0 19 64 -69 0 92 124 158 0 3 -62 -133 0 -1 -27 -70 0 63 -117 -128 0 60 86 132 0 -4 -91 -173 0 84 -88 -144 0 -32 -168 -195 0 37 103 -128 0 94 -99 -137 0 23 -99 -175 0 -175 181 197 0 33 46 134 0 -87 106 144 0 56 -76 -106 0 16 -135 179 0 19 30 -40 0 58 121 125 0 -86 -116 -154 0 19 30 -167 0 -83 153 -179 0 -7 125 194 0 1 -45 -135 0 -7 51 -168 0 -20 -41 -198 0 77 158 -187 0 -86 98 -125 0 62 123 -127 0 -55 -55 58 0 80 -99 -140 0 -68 92 -116 0 -25 -63 -192 0 81 180 181 0 23 60 -133 0 40 68 -196 0 46 142 -192 0 -25 76 -146 0 23 -55 77 0 -118 132 -181 0 87 169 -172 0 -91 125 -174 0 40 -88 118 0 -62 118 -129 0 1 -92 -118 0 102 -131 194 0 -6 -77 99 0 -33 114 168 0 25 -70 -196 0 103 -147 175 0 64 117 -196 0 -1 -92 175 0 34 114 187 0 -59 -81 -168 0 25 72 150 0 140 148 184 0 85 -91 168 0 -62 -92 102 0 -14 78 98 0