p cnf 303 841 -8 1 0 -8 2 0 8 -1 -2 0 -9 1 0 -9 3 0 9 -1 -3 0 -10 3 0 -10 8 0 10 -3 -8 0 -11 -3 0 -11 -8 0 11 3 8 0 -12 -10 0 -12 -11 0 12 10 11 0 -13 9 0 -13 12 0 13 -9 -12 0 -14 -9 0 -14 -12 0 14 9 12 0 -15 -13 0 -15 -14 0 15 13 14 0 -16 8 0 -16 15 0 16 -8 -15 0 -17 -8 0 -17 -15 0 18 16 17 0 -19 1 0 -19 4 0 19 -1 -4 0 -20 2 0 -20 3 0 20 -2 -3 0 -21 -10 0 -21 -13 0 21 10 13 0 -22 19 0 -22 20 0 22 -19 -20 0 -23 -19 0 -23 -20 0 23 19 20 0 -24 -22 0 -24 -23 0 24 22 23 0 -25 -21 0 -25 24 0 25 21 -24 0 -26 21 0 -26 -24 0 26 -21 24 0 -27 -25 0 -27 -26 0 27 25 26 0 -28 20 0 -28 27 0 28 -20 -27 0 -29 -20 0 -29 -27 0 29 20 27 0 -30 -28 0 -30 -29 0 30 28 29 0 -31 16 0 -31 30 0 31 -16 -30 0 -32 -16 0 -32 -30 0 32 16 30 0 -33 -31 0 -33 -32 0 33 31 32 0 -34 19 0 -34 33 0 34 -19 -33 0 35 19 33 0 -36 -34 0 -36 -35 0 -37 1 0 -37 5 0 37 -1 -5 0 -38 3 0 -38 4 0 38 -3 -4 0 -39 -28 0 -39 -31 0 39 28 31 0 -40 -22 0 -40 -25 0 40 22 25 0 -41 37 0 -41 38 0 41 -37 -38 0 -42 -37 0 -42 -38 0 42 37 38 0 -43 -41 0 -43 -42 0 43 41 42 0 -44 -40 0 -44 43 0 44 40 -43 0 -45 40 0 -45 -43 0 45 -40 43 0 -46 -44 0 -46 -45 0 46 44 45 0 -47 2 0 -47 46 0 47 -2 -46 0 -48 -2 0 -48 -46 0 48 2 46 0 -49 -47 0 -49 -48 0 49 47 48 0 -50 -39 0 -50 49 0 50 39 -49 0 -51 39 0 -51 -49 0 51 -39 49 0 -52 -50 0 -52 -51 0 52 50 51 0 -53 38 0 -53 52 0 53 -38 -52 0 -54 -38 0 -54 -52 0 54 38 52 0 -55 -53 0 -55 -54 0 55 53 54 0 -56 34 0 -56 55 0 56 -34 -55 0 -57 -34 0 -57 -55 0 57 34 55 0 -58 -56 0 -58 -57 0 58 56 57 0 -59 37 0 -59 58 0 59 -37 -58 0 -60 -37 0 -60 -58 0 61 59 60 0 -62 1 0 -62 6 0 62 -1 -6 0 -63 3 0 -63 5 0 63 -3 -5 0 -64 -53 0 -64 -56 0 64 53 56 0 -65 2 0 -65 4 0 65 -2 -4 0 -66 -47 0 -66 -50 0 66 47 50 0 -67 -41 0 -67 -44 0 67 41 44 0 -68 62 0 -68 63 0 68 -62 -63 0 -69 -62 0 -69 -63 0 69 62 63 0 -70 -68 0 -70 -69 0 70 68 69 0 -71 -67 0 -71 70 0 71 67 -70 0 -72 67 0 -72 -70 0 72 -67 70 0 -73 -71 0 -73 -72 0 73 71 72 0 -74 65 0 -74 73 0 74 -65 -73 0 -75 -65 0 -75 -73 0 75 65 73 0 -76 -74 0 -76 -75 0 76 74 75 0 -77 -66 0 -77 76 0 77 66 -76 0 -78 66 0 -78 -76 0 78 -66 76 0 -79 -77 0 -79 -78 0 79 77 78 0 -80 65 0 -80 79 0 80 -65 -79 0 -81 -65 0 -81 -79 0 81 65 79 0 -82 -80 0 -82 -81 0 82 80 81 0 -83 -64 0 -83 82 0 83 64 -82 0 -84 64 0 -84 -82 0 84 -64 82 0 -85 -83 0 -85 -84 0 85 83 84 0 -86 63 0 -86 85 0 86 -63 -85 0 -87 -63 0 -87 -85 0 87 63 85 0 -88 -86 0 -88 -87 0 88 86 87 0 -89 59 0 -89 88 0 89 -59 -88 0 -90 -59 0 -90 -88 0 90 59 88 0 -91 -89 0 -91 -90 0 91 89 90 0 -92 62 0 -92 91 0 92 -62 -91 0 93 62 91 0 -94 -92 0 -94 -93 0 -95 1 0 -95 7 0 95 -1 -7 0 -96 3 0 -96 6 0 96 -3 -6 0 -97 -86 0 -97 -89 0 97 86 89 0 -98 2 0 -98 5 0 98 -2 -5 0 -99 -80 0 -99 -83 0 99 80 83 0 -100 -74 0 -100 -77 0 100 74 77 0 -101 -68 0 -101 -71 0 101 68 71 0 -102 95 0 -102 96 0 102 -95 -96 0 -103 -95 0 -103 -96 0 103 95 96 0 -104 -102 0 -104 -103 0 104 102 103 0 -105 -101 0 -105 104 0 105 101 -104 0 -106 101 0 -106 -104 0 106 -101 104 0 -107 -105 0 -107 -106 0 107 105 106 0 -108 98 0 -108 107 0 108 -98 -107 0 -109 -98 0 -109 -107 0 109 98 107 0 -110 -108 0 -110 -109 0 110 108 109 0 -111 -100 0 -111 110 0 111 100 -110 0 -112 100 0 -112 -110 0 112 -100 110 0 -113 -111 0 -113 -112 0 113 111 112 0 -114 4 0 -114 113 0 114 -4 -113 0 -115 -4 0 -115 -113 0 115 4 113 0 -116 -114 0 -116 -115 0 116 114 115 0 -117 -99 0 -117 116 0 117 99 -116 0 -118 99 0 -118 -116 0 118 -99 116 0 -119 -117 0 -119 -118 0 119 117 118 0 -120 98 0 -120 119 0 120 -98 -119 0 -121 -98 0 -121 -119 0 121 98 119 0 -122 -120 0 -122 -121 0 122 120 121 0 -123 -97 0 -123 122 0 123 97 -122 0 -124 97 0 -124 -122 0 124 -97 122 0 -125 -123 0 -125 -124 0 125 123 124 0 -126 96 0 -126 125 0 126 -96 -125 0 -127 -96 0 -127 -125 0 127 96 125 0 -128 -126 0 -128 -127 0 128 126 127 0 -129 92 0 -129 128 0 129 -92 -128 0 -130 -92 0 -130 -128 0 130 92 128 0 -131 -129 0 -131 -130 0 131 129 130 0 -132 95 0 -132 131 0 132 -95 -131 0 133 95 131 0 -134 -132 0 -134 -133 0 -135 3 0 -135 7 0 135 -3 -7 0 -136 -126 0 -136 -129 0 136 126 129 0 -137 2 0 -137 6 0 137 -2 -6 0 -138 -120 0 -138 -123 0 138 120 123 0 -139 4 0 -139 5 0 139 -4 -5 0 -140 -114 0 -140 -117 0 140 114 117 0 -141 -108 0 -141 -111 0 141 108 111 0 -142 -102 0 -142 -105 0 142 102 105 0 -143 135 0 -143 -142 0 143 -135 142 0 -144 -135 0 -144 142 0 144 135 -142 0 -145 -143 0 -145 -144 0 145 143 144 0 -146 137 0 -146 145 0 146 -137 -145 0 -147 -137 0 -147 -145 0 147 137 145 0 -148 -146 0 -148 -147 0 148 146 147 0 -149 -141 0 -149 148 0 149 141 -148 0 -150 141 0 -150 -148 0 150 -141 148 0 -151 -149 0 -151 -150 0 151 149 150 0 -152 139 0 -152 151 0 152 -139 -151 0 -153 -139 0 -153 -151 0 153 139 151 0 -154 -152 0 -154 -153 0 154 152 153 0 -155 -140 0 -155 154 0 155 140 -154 0 -156 140 0 -156 -154 0 156 -140 154 0 -157 -155 0 -157 -156 0 157 155 156 0 -158 139 0 -158 157 0 158 -139 -157 0 -159 -139 0 -159 -157 0 159 139 157 0 -160 -158 0 -160 -159 0 160 158 159 0 -161 -138 0 -161 160 0 161 138 -160 0 -162 138 0 -162 -160 0 162 -138 160 0 -163 -161 0 -163 -162 0 163 161 162 0 -164 137 0 -164 163 0 164 -137 -163 0 -165 -137 0 -165 -163 0 165 137 163 0 -166 -164 0 -166 -165 0 166 164 165 0 -167 -136 0 -167 166 0 167 136 -166 0 -168 136 0 -168 -166 0 168 -136 166 0 -169 -167 0 -169 -168 0 169 167 168 0 -170 135 0 -170 169 0 170 -135 -169 0 -171 -135 0 -171 -169 0 171 135 169 0 -172 -170 0 -172 -171 0 172 170 171 0 -173 132 0 -173 172 0 173 -132 -172 0 -174 -132 0 -174 -172 0 175 173 174 0 -176 -170 0 -176 -173 0 176 170 173 0 -177 2 0 -177 7 0 177 -2 -7 0 -178 -164 0 -178 -167 0 178 164 167 0 -179 4 0 -179 6 0 179 -4 -6 0 -180 -158 0 -180 -161 0 180 158 161 0 -181 -152 0 -181 -155 0 181 152 155 0 -182 -146 0 -182 -149 0 182 146 149 0 -183 143 0 -183 177 0 183 -143 -177 0 -184 -143 0 -184 -177 0 184 143 177 0 -185 -183 0 -185 -184 0 185 183 184 0 -186 -182 0 -186 185 0 186 182 -185 0 -187 182 0 -187 -185 0 187 -182 185 0 -188 -186 0 -188 -187 0 188 186 187 0 -189 179 0 -189 188 0 189 -179 -188 0 -190 -179 0 -190 -188 0 190 179 188 0 -191 -189 0 -191 -190 0 191 189 190 0 -192 -181 0 -192 191 0 192 181 -191 0 -193 181 0 -193 -191 0 193 -181 191 0 -194 -192 0 -194 -193 0 194 192 193 0 -195 5 0 -195 194 0 195 -5 -194 0 -196 -5 0 -196 -194 0 196 5 194 0 -197 -195 0 -197 -196 0 197 195 196 0 -198 -180 0 -198 197 0 198 180 -197 0 -199 180 0 -199 -197 0 199 -180 197 0 -200 -198 0 -200 -199 0 200 198 199 0 -201 179 0 -201 200 0 201 -179 -200 0 -202 -179 0 -202 -200 0 202 179 200 0 -203 -201 0 -203 -202 0 203 201 202 0 -204 -178 0 -204 203 0 204 178 -203 0 -205 178 0 -205 -203 0 205 -178 203 0 -206 -204 0 -206 -205 0 206 204 205 0 -207 177 0 -207 206 0 207 -177 -206 0 -208 -177 0 -208 -206 0 208 177 206 0 -209 -207 0 -209 -208 0 209 207 208 0 -210 -176 0 -210 209 0 210 176 -209 0 -211 176 0 -211 -209 0 212 210 211 0 -213 -207 0 -213 -210 0 213 207 210 0 -214 4 0 -214 7 0 214 -4 -7 0 -215 -201 0 -215 -204 0 215 201 204 0 -216 5 0 -216 6 0 216 -5 -6 0 -217 -195 0 -217 -198 0 217 195 198 0 -218 -189 0 -218 -192 0 218 189 192 0 -219 -183 0 -219 -186 0 219 183 186 0 -220 214 0 -220 -219 0 220 -214 219 0 -221 -214 0 -221 219 0 221 214 -219 0 -222 -220 0 -222 -221 0 222 220 221 0 -223 -218 0 -223 222 0 223 218 -222 0 -224 218 0 -224 -222 0 224 -218 222 0 -225 -223 0 -225 -224 0 225 223 224 0 -226 216 0 -226 225 0 226 -216 -225 0 -227 -216 0 -227 -225 0 227 216 225 0 -228 -226 0 -228 -227 0 228 226 227 0 -229 -217 0 -229 228 0 229 217 -228 0 -230 217 0 -230 -228 0 230 -217 228 0 -231 -229 0 -231 -230 0 231 229 230 0 -232 216 0 -232 231 0 232 -216 -231 0 -233 -216 0 -233 -231 0 233 216 231 0 -234 -232 0 -234 -233 0 234 232 233 0 -235 -215 0 -235 234 0 235 215 -234 0 -236 215 0 -236 -234 0 236 -215 234 0 -237 -235 0 -237 -236 0 237 235 236 0 -238 214 0 -238 237 0 238 -214 -237 0 -239 -214 0 -239 -237 0 239 214 237 0 -240 -238 0 -240 -239 0 240 238 239 0 -241 -213 0 -241 240 0 241 213 -240 0 242 -213 240 0 -243 -241 0 -243 -242 0 -244 -238 0 -244 -241 0 244 238 241 0 -245 5 0 -245 7 0 245 -5 -7 0 -246 -232 0 -246 -235 0 246 232 235 0 -247 -226 0 -247 -229 0 247 226 229 0 -248 -220 0 -248 -223 0 248 220 223 0 -249 245 0 -249 -248 0 249 -245 248 0 -250 -245 0 -250 248 0 250 245 -248 0 -251 -249 0 -251 -250 0 251 249 250 0 -252 -247 0 -252 251 0 252 247 -251 0 -253 247 0 -253 -251 0 253 -247 251 0 -254 -252 0 -254 -253 0 254 252 253 0 -255 6 0 -255 254 0 255 -6 -254 0 -256 -6 0 -256 -254 0 256 6 254 0 -257 -255 0 -257 -256 0 257 255 256 0 -258 -246 0 -258 257 0 258 246 -257 0 -259 246 0 -259 -257 0 259 -246 257 0 -260 -258 0 -260 -259 0 260 258 259 0 -261 245 0 -261 260 0 261 -245 -260 0 -262 -245 0 -262 -260 0 262 245 260 0 -263 -261 0 -263 -262 0 263 261 262 0 -264 -244 0 -264 263 0 264 244 -263 0 265 -244 263 0 -266 -264 0 -266 -265 0 -267 -261 0 -267 -264 0 267 261 264 0 -268 6 0 -268 7 0 268 -6 -7 0 -269 -255 0 -269 -258 0 269 255 258 0 -270 -249 0 -270 -252 0 270 249 252 0 -271 268 0 -271 -270 0 271 -268 270 0 -272 -268 0 -272 270 0 272 268 -270 0 -273 -271 0 -273 -272 0 273 271 272 0 -274 -269 0 -274 273 0 274 269 -273 0 -275 269 0 -275 -273 0 275 -269 273 0 -276 -274 0 -276 -275 0 276 274 275 0 -277 268 0 -277 276 0 277 -268 -276 0 -278 -268 0 -278 -276 0 278 268 276 0 -279 -277 0 -279 -278 0 279 277 278 0 -280 -267 0 -280 279 0 280 267 -279 0 281 -267 279 0 -282 -280 0 -282 -281 0 -283 -277 0 -283 -280 0 283 277 280 0 -284 -271 0 -284 -274 0 284 271 274 0 -285 7 0 -285 -284 0 285 -7 284 0 -286 -7 0 -286 284 0 286 7 -284 0 -287 -285 0 -287 -286 0 287 285 286 0 -288 -283 0 -288 287 0 -289 283 0 -289 -287 0 290 288 289 0 291 285 288 0 -292 -290 0 -292 -291 0 -293 282 0 -293 292 0 -294 266 0 -294 293 0 -295 243 0 -295 294 0 -296 -212 0 -296 295 0 -297 -175 0 -297 296 0 -298 134 0 -298 297 0 -299 94 0 -299 298 0 -300 -61 0 -300 299 0 -301 36 0 -301 300 0 -302 -18 0 -302 301 0 -303 1 0 -303 302 0 303 0