c pigeon-15: placing 16 pigeons into 15 holes c c File generated by 'pigeonhole', (c) Tjark Weber c c The SAT encoding of this problem is very straightforward. For each pigeon i c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i c is placed in hole j. Then we have n+1 clauses which say that a pigeon has c to be placed in some hole. Then for each hole we have a set of clauses c ensuring that only one single pigeon is placed into that hole. c c This encoding leads to a total of (n+1) * n propositional variables and c (n+1) + n * (n * (n+1) / 2) clauses. c c The resulting SAT problem is unsatisfiable. c p cnf 240 1816 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 0 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 0 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 0 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 0 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 0 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 0 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 0 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 0 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 0 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 0 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 0 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 0 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 0 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 0 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 0 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 0 -1 -16 0 -1 -31 0 -1 -46 0 -1 -61 0 -1 -76 0 -1 -91 0 -1 -106 0 -1 -121 0 -1 -136 0 -1 -151 0 -1 -166 0 -1 -181 0 -1 -196 0 -1 -211 0 -1 -226 0 -16 -31 0 -16 -46 0 -16 -61 0 -16 -76 0 -16 -91 0 -16 -106 0 -16 -121 0 -16 -136 0 -16 -151 0 -16 -166 0 -16 -181 0 -16 -196 0 -16 -211 0 -16 -226 0 -31 -46 0 -31 -61 0 -31 -76 0 -31 -91 0 -31 -106 0 -31 -121 0 -31 -136 0 -31 -151 0 -31 -166 0 -31 -181 0 -31 -196 0 -31 -211 0 -31 -226 0 -46 -61 0 -46 -76 0 -46 -91 0 -46 -106 0 -46 -121 0 -46 -136 0 -46 -151 0 -46 -166 0 -46 -181 0 -46 -196 0 -46 -211 0 -46 -226 0 -61 -76 0 -61 -91 0 -61 -106 0 -61 -121 0 -61 -136 0 -61 -151 0 -61 -166 0 -61 -181 0 -61 -196 0 -61 -211 0 -61 -226 0 -76 -91 0 -76 -106 0 -76 -121 0 -76 -136 0 -76 -151 0 -76 -166 0 -76 -181 0 -76 -196 0 -76 -211 0 -76 -226 0 -91 -106 0 -91 -121 0 -91 -136 0 -91 -151 0 -91 -166 0 -91 -181 0 -91 -196 0 -91 -211 0 -91 -226 0 -106 -121 0 -106 -136 0 -106 -151 0 -106 -166 0 -106 -181 0 -106 -196 0 -106 -211 0 -106 -226 0 -121 -136 0 -121 -151 0 -121 -166 0 -121 -181 0 -121 -196 0 -121 -211 0 -121 -226 0 -136 -151 0 -136 -166 0 -136 -181 0 -136 -196 0 -136 -211 0 -136 -226 0 -151 -166 0 -151 -181 0 -151 -196 0 -151 -211 0 -151 -226 0 -166 -181 0 -166 -196 0 -166 -211 0 -166 -226 0 -181 -196 0 -181 -211 0 -181 -226 0 -196 -211 0 -196 -226 0 -211 -226 0 -2 -17 0 -2 -32 0 -2 -47 0 -2 -62 0 -2 -77 0 -2 -92 0 -2 -107 0 -2 -122 0 -2 -137 0 -2 -152 0 -2 -167 0 -2 -182 0 -2 -197 0 -2 -212 0 -2 -227 0 -17 -32 0 -17 -47 0 -17 -62 0 -17 -77 0 -17 -92 0 -17 -107 0 -17 -122 0 -17 -137 0 -17 -152 0 -17 -167 0 -17 -182 0 -17 -197 0 -17 -212 0 -17 -227 0 -32 -47 0 -32 -62 0 -32 -77 0 -32 -92 0 -32 -107 0 -32 -122 0 -32 -137 0 -32 -152 0 -32 -167 0 -32 -182 0 -32 -197 0 -32 -212 0 -32 -227 0 -47 -62 0 -47 -77 0 -47 -92 0 -47 -107 0 -47 -122 0 -47 -137 0 -47 -152 0 -47 -167 0 -47 -182 0 -47 -197 0 -47 -212 0 -47 -227 0 -62 -77 0 -62 -92 0 -62 -107 0 -62 -122 0 -62 -137 0 -62 -152 0 -62 -167 0 -62 -182 0 -62 -197 0 -62 -212 0 -62 -227 0 -77 -92 0 -77 -107 0 -77 -122 0 -77 -137 0 -77 -152 0 -77 -167 0 -77 -182 0 -77 -197 0 -77 -212 0 -77 -227 0 -92 -107 0 -92 -122 0 -92 -137 0 -92 -152 0 -92 -167 0 -92 -182 0 -92 -197 0 -92 -212 0 -92 -227 0 -107 -122 0 -107 -137 0 -107 -152 0 -107 -167 0 -107 -182 0 -107 -197 0 -107 -212 0 -107 -227 0 -122 -137 0 -122 -152 0 -122 -167 0 -122 -182 0 -122 -197 0 -122 -212 0 -122 -227 0 -137 -152 0 -137 -167 0 -137 -182 0 -137 -197 0 -137 -212 0 -137 -227 0 -152 -167 0 -152 -182 0 -152 -197 0 -152 -212 0 -152 -227 0 -167 -182 0 -167 -197 0 -167 -212 0 -167 -227 0 -182 -197 0 -182 -212 0 -182 -227 0 -197 -212 0 -197 -227 0 -212 -227 0 -3 -18 0 -3 -33 0 -3 -48 0 -3 -63 0 -3 -78 0 -3 -93 0 -3 -108 0 -3 -123 0 -3 -138 0 -3 -153 0 -3 -168 0 -3 -183 0 -3 -198 0 -3 -213 0 -3 -228 0 -18 -33 0 -18 -48 0 -18 -63 0 -18 -78 0 -18 -93 0 -18 -108 0 -18 -123 0 -18 -138 0 -18 -153 0 -18 -168 0 -18 -183 0 -18 -198 0 -18 -213 0 -18 -228 0 -33 -48 0 -33 -63 0 -33 -78 0 -33 -93 0 -33 -108 0 -33 -123 0 -33 -138 0 -33 -153 0 -33 -168 0 -33 -183 0 -33 -198 0 -33 -213 0 -33 -228 0 -48 -63 0 -48 -78 0 -48 -93 0 -48 -108 0 -48 -123 0 -48 -138 0 -48 -153 0 -48 -168 0 -48 -183 0 -48 -198 0 -48 -213 0 -48 -228 0 -63 -78 0 -63 -93 0 -63 -108 0 -63 -123 0 -63 -138 0 -63 -153 0 -63 -168 0 -63 -183 0 -63 -198 0 -63 -213 0 -63 -228 0 -78 -93 0 -78 -108 0 -78 -123 0 -78 -138 0 -78 -153 0 -78 -168 0 -78 -183 0 -78 -198 0 -78 -213 0 -78 -228 0 -93 -108 0 -93 -123 0 -93 -138 0 -93 -153 0 -93 -168 0 -93 -183 0 -93 -198 0 -93 -213 0 -93 -228 0 -108 -123 0 -108 -138 0 -108 -153 0 -108 -168 0 -108 -183 0 -108 -198 0 -108 -213 0 -108 -228 0 -123 -138 0 -123 -153 0 -123 -168 0 -123 -183 0 -123 -198 0 -123 -213 0 -123 -228 0 -138 -153 0 -138 -168 0 -138 -183 0 -138 -198 0 -138 -213 0 -138 -228 0 -153 -168 0 -153 -183 0 -153 -198 0 -153 -213 0 -153 -228 0 -168 -183 0 -168 -198 0 -168 -213 0 -168 -228 0 -183 -198 0 -183 -213 0 -183 -228 0 -198 -213 0 -198 -228 0 -213 -228 0 -4 -19 0 -4 -34 0 -4 -49 0 -4 -64 0 -4 -79 0 -4 -94 0 -4 -109 0 -4 -124 0 -4 -139 0 -4 -154 0 -4 -169 0 -4 -184 0 -4 -199 0 -4 -214 0 -4 -229 0 -19 -34 0 -19 -49 0 -19 -64 0 -19 -79 0 -19 -94 0 -19 -109 0 -19 -124 0 -19 -139 0 -19 -154 0 -19 -169 0 -19 -184 0 -19 -199 0 -19 -214 0 -19 -229 0 -34 -49 0 -34 -64 0 -34 -79 0 -34 -94 0 -34 -109 0 -34 -124 0 -34 -139 0 -34 -154 0 -34 -169 0 -34 -184 0 -34 -199 0 -34 -214 0 -34 -229 0 -49 -64 0 -49 -79 0 -49 -94 0 -49 -109 0 -49 -124 0 -49 -139 0 -49 -154 0 -49 -169 0 -49 -184 0 -49 -199 0 -49 -214 0 -49 -229 0 -64 -79 0 -64 -94 0 -64 -109 0 -64 -124 0 -64 -139 0 -64 -154 0 -64 -169 0 -64 -184 0 -64 -199 0 -64 -214 0 -64 -229 0 -79 -94 0 -79 -109 0 -79 -124 0 -79 -139 0 -79 -154 0 -79 -169 0 -79 -184 0 -79 -199 0 -79 -214 0 -79 -229 0 -94 -109 0 -94 -124 0 -94 -139 0 -94 -154 0 -94 -169 0 -94 -184 0 -94 -199 0 -94 -214 0 -94 -229 0 -109 -124 0 -109 -139 0 -109 -154 0 -109 -169 0 -109 -184 0 -109 -199 0 -109 -214 0 -109 -229 0 -124 -139 0 -124 -154 0 -124 -169 0 -124 -184 0 -124 -199 0 -124 -214 0 -124 -229 0 -139 -154 0 -139 -169 0 -139 -184 0 -139 -199 0 -139 -214 0 -139 -229 0 -154 -169 0 -154 -184 0 -154 -199 0 -154 -214 0 -154 -229 0 -169 -184 0 -169 -199 0 -169 -214 0 -169 -229 0 -184 -199 0 -184 -214 0 -184 -229 0 -199 -214 0 -199 -229 0 -214 -229 0 -5 -20 0 -5 -35 0 -5 -50 0 -5 -65 0 -5 -80 0 -5 -95 0 -5 -110 0 -5 -125 0 -5 -140 0 -5 -155 0 -5 -170 0 -5 -185 0 -5 -200 0 -5 -215 0 -5 -230 0 -20 -35 0 -20 -50 0 -20 -65 0 -20 -80 0 -20 -95 0 -20 -110 0 -20 -125 0 -20 -140 0 -20 -155 0 -20 -170 0 -20 -185 0 -20 -200 0 -20 -215 0 -20 -230 0 -35 -50 0 -35 -65 0 -35 -80 0 -35 -95 0 -35 -110 0 -35 -125 0 -35 -140 0 -35 -155 0 -35 -170 0 -35 -185 0 -35 -200 0 -35 -215 0 -35 -230 0 -50 -65 0 -50 -80 0 -50 -95 0 -50 -110 0 -50 -125 0 -50 -140 0 -50 -155 0 -50 -170 0 -50 -185 0 -50 -200 0 -50 -215 0 -50 -230 0 -65 -80 0 -65 -95 0 -65 -110 0 -65 -125 0 -65 -140 0 -65 -155 0 -65 -170 0 -65 -185 0 -65 -200 0 -65 -215 0 -65 -230 0 -80 -95 0 -80 -110 0 -80 -125 0 -80 -140 0 -80 -155 0 -80 -170 0 -80 -185 0 -80 -200 0 -80 -215 0 -80 -230 0 -95 -110 0 -95 -125 0 -95 -140 0 -95 -155 0 -95 -170 0 -95 -185 0 -95 -200 0 -95 -215 0 -95 -230 0 -110 -125 0 -110 -140 0 -110 -155 0 -110 -170 0 -110 -185 0 -110 -200 0 -110 -215 0 -110 -230 0 -125 -140 0 -125 -155 0 -125 -170 0 -125 -185 0 -125 -200 0 -125 -215 0 -125 -230 0 -140 -155 0 -140 -170 0 -140 -185 0 -140 -200 0 -140 -215 0 -140 -230 0 -155 -170 0 -155 -185 0 -155 -200 0 -155 -215 0 -155 -230 0 -170 -185 0 -170 -200 0 -170 -215 0 -170 -230 0 -185 -200 0 -185 -215 0 -185 -230 0 -200 -215 0 -200 -230 0 -215 -230 0 -6 -21 0 -6 -36 0 -6 -51 0 -6 -66 0 -6 -81 0 -6 -96 0 -6 -111 0 -6 -126 0 -6 -141 0 -6 -156 0 -6 -171 0 -6 -186 0 -6 -201 0 -6 -216 0 -6 -231 0 -21 -36 0 -21 -51 0 -21 -66 0 -21 -81 0 -21 -96 0 -21 -111 0 -21 -126 0 -21 -141 0 -21 -156 0 -21 -171 0 -21 -186 0 -21 -201 0 -21 -216 0 -21 -231 0 -36 -51 0 -36 -66 0 -36 -81 0 -36 -96 0 -36 -111 0 -36 -126 0 -36 -141 0 -36 -156 0 -36 -171 0 -36 -186 0 -36 -201 0 -36 -216 0 -36 -231 0 -51 -66 0 -51 -81 0 -51 -96 0 -51 -111 0 -51 -126 0 -51 -141 0 -51 -156 0 -51 -171 0 -51 -186 0 -51 -201 0 -51 -216 0 -51 -231 0 -66 -81 0 -66 -96 0 -66 -111 0 -66 -126 0 -66 -141 0 -66 -156 0 -66 -171 0 -66 -186 0 -66 -201 0 -66 -216 0 -66 -231 0 -81 -96 0 -81 -111 0 -81 -126 0 -81 -141 0 -81 -156 0 -81 -171 0 -81 -186 0 -81 -201 0 -81 -216 0 -81 -231 0 -96 -111 0 -96 -126 0 -96 -141 0 -96 -156 0 -96 -171 0 -96 -186 0 -96 -201 0 -96 -216 0 -96 -231 0 -111 -126 0 -111 -141 0 -111 -156 0 -111 -171 0 -111 -186 0 -111 -201 0 -111 -216 0 -111 -231 0 -126 -141 0 -126 -156 0 -126 -171 0 -126 -186 0 -126 -201 0 -126 -216 0 -126 -231 0 -141 -156 0 -141 -171 0 -141 -186 0 -141 -201 0 -141 -216 0 -141 -231 0 -156 -171 0 -156 -186 0 -156 -201 0 -156 -216 0 -156 -231 0 -171 -186 0 -171 -201 0 -171 -216 0 -171 -231 0 -186 -201 0 -186 -216 0 -186 -231 0 -201 -216 0 -201 -231 0 -216 -231 0 -7 -22 0 -7 -37 0 -7 -52 0 -7 -67 0 -7 -82 0 -7 -97 0 -7 -112 0 -7 -127 0 -7 -142 0 -7 -157 0 -7 -172 0 -7 -187 0 -7 -202 0 -7 -217 0 -7 -232 0 -22 -37 0 -22 -52 0 -22 -67 0 -22 -82 0 -22 -97 0 -22 -112 0 -22 -127 0 -22 -142 0 -22 -157 0 -22 -172 0 -22 -187 0 -22 -202 0 -22 -217 0 -22 -232 0 -37 -52 0 -37 -67 0 -37 -82 0 -37 -97 0 -37 -112 0 -37 -127 0 -37 -142 0 -37 -157 0 -37 -172 0 -37 -187 0 -37 -202 0 -37 -217 0 -37 -232 0 -52 -67 0 -52 -82 0 -52 -97 0 -52 -112 0 -52 -127 0 -52 -142 0 -52 -157 0 -52 -172 0 -52 -187 0 -52 -202 0 -52 -217 0 -52 -232 0 -67 -82 0 -67 -97 0 -67 -112 0 -67 -127 0 -67 -142 0 -67 -157 0 -67 -172 0 -67 -187 0 -67 -202 0 -67 -217 0 -67 -232 0 -82 -97 0 -82 -112 0 -82 -127 0 -82 -142 0 -82 -157 0 -82 -172 0 -82 -187 0 -82 -202 0 -82 -217 0 -82 -232 0 -97 -112 0 -97 -127 0 -97 -142 0 -97 -157 0 -97 -172 0 -97 -187 0 -97 -202 0 -97 -217 0 -97 -232 0 -112 -127 0 -112 -142 0 -112 -157 0 -112 -172 0 -112 -187 0 -112 -202 0 -112 -217 0 -112 -232 0 -127 -142 0 -127 -157 0 -127 -172 0 -127 -187 0 -127 -202 0 -127 -217 0 -127 -232 0 -142 -157 0 -142 -172 0 -142 -187 0 -142 -202 0 -142 -217 0 -142 -232 0 -157 -172 0 -157 -187 0 -157 -202 0 -157 -217 0 -157 -232 0 -172 -187 0 -172 -202 0 -172 -217 0 -172 -232 0 -187 -202 0 -187 -217 0 -187 -232 0 -202 -217 0 -202 -232 0 -217 -232 0 -8 -23 0 -8 -38 0 -8 -53 0 -8 -68 0 -8 -83 0 -8 -98 0 -8 -113 0 -8 -128 0 -8 -143 0 -8 -158 0 -8 -173 0 -8 -188 0 -8 -203 0 -8 -218 0 -8 -233 0 -23 -38 0 -23 -53 0 -23 -68 0 -23 -83 0 -23 -98 0 -23 -113 0 -23 -128 0 -23 -143 0 -23 -158 0 -23 -173 0 -23 -188 0 -23 -203 0 -23 -218 0 -23 -233 0 -38 -53 0 -38 -68 0 -38 -83 0 -38 -98 0 -38 -113 0 -38 -128 0 -38 -143 0 -38 -158 0 -38 -173 0 -38 -188 0 -38 -203 0 -38 -218 0 -38 -233 0 -53 -68 0 -53 -83 0 -53 -98 0 -53 -113 0 -53 -128 0 -53 -143 0 -53 -158 0 -53 -173 0 -53 -188 0 -53 -203 0 -53 -218 0 -53 -233 0 -68 -83 0 -68 -98 0 -68 -113 0 -68 -128 0 -68 -143 0 -68 -158 0 -68 -173 0 -68 -188 0 -68 -203 0 -68 -218 0 -68 -233 0 -83 -98 0 -83 -113 0 -83 -128 0 -83 -143 0 -83 -158 0 -83 -173 0 -83 -188 0 -83 -203 0 -83 -218 0 -83 -233 0 -98 -113 0 -98 -128 0 -98 -143 0 -98 -158 0 -98 -173 0 -98 -188 0 -98 -203 0 -98 -218 0 -98 -233 0 -113 -128 0 -113 -143 0 -113 -158 0 -113 -173 0 -113 -188 0 -113 -203 0 -113 -218 0 -113 -233 0 -128 -143 0 -128 -158 0 -128 -173 0 -128 -188 0 -128 -203 0 -128 -218 0 -128 -233 0 -143 -158 0 -143 -173 0 -143 -188 0 -143 -203 0 -143 -218 0 -143 -233 0 -158 -173 0 -158 -188 0 -158 -203 0 -158 -218 0 -158 -233 0 -173 -188 0 -173 -203 0 -173 -218 0 -173 -233 0 -188 -203 0 -188 -218 0 -188 -233 0 -203 -218 0 -203 -233 0 -218 -233 0 -9 -24 0 -9 -39 0 -9 -54 0 -9 -69 0 -9 -84 0 -9 -99 0 -9 -114 0 -9 -129 0 -9 -144 0 -9 -159 0 -9 -174 0 -9 -189 0 -9 -204 0 -9 -219 0 -9 -234 0 -24 -39 0 -24 -54 0 -24 -69 0 -24 -84 0 -24 -99 0 -24 -114 0 -24 -129 0 -24 -144 0 -24 -159 0 -24 -174 0 -24 -189 0 -24 -204 0 -24 -219 0 -24 -234 0 -39 -54 0 -39 -69 0 -39 -84 0 -39 -99 0 -39 -114 0 -39 -129 0 -39 -144 0 -39 -159 0 -39 -174 0 -39 -189 0 -39 -204 0 -39 -219 0 -39 -234 0 -54 -69 0 -54 -84 0 -54 -99 0 -54 -114 0 -54 -129 0 -54 -144 0 -54 -159 0 -54 -174 0 -54 -189 0 -54 -204 0 -54 -219 0 -54 -234 0 -69 -84 0 -69 -99 0 -69 -114 0 -69 -129 0 -69 -144 0 -69 -159 0 -69 -174 0 -69 -189 0 -69 -204 0 -69 -219 0 -69 -234 0 -84 -99 0 -84 -114 0 -84 -129 0 -84 -144 0 -84 -159 0 -84 -174 0 -84 -189 0 -84 -204 0 -84 -219 0 -84 -234 0 -99 -114 0 -99 -129 0 -99 -144 0 -99 -159 0 -99 -174 0 -99 -189 0 -99 -204 0 -99 -219 0 -99 -234 0 -114 -129 0 -114 -144 0 -114 -159 0 -114 -174 0 -114 -189 0 -114 -204 0 -114 -219 0 -114 -234 0 -129 -144 0 -129 -159 0 -129 -174 0 -129 -189 0 -129 -204 0 -129 -219 0 -129 -234 0 -144 -159 0 -144 -174 0 -144 -189 0 -144 -204 0 -144 -219 0 -144 -234 0 -159 -174 0 -159 -189 0 -159 -204 0 -159 -219 0 -159 -234 0 -174 -189 0 -174 -204 0 -174 -219 0 -174 -234 0 -189 -204 0 -189 -219 0 -189 -234 0 -204 -219 0 -204 -234 0 -219 -234 0 -10 -25 0 -10 -40 0 -10 -55 0 -10 -70 0 -10 -85 0 -10 -100 0 -10 -115 0 -10 -130 0 -10 -145 0 -10 -160 0 -10 -175 0 -10 -190 0 -10 -205 0 -10 -220 0 -10 -235 0 -25 -40 0 -25 -55 0 -25 -70 0 -25 -85 0 -25 -100 0 -25 -115 0 -25 -130 0 -25 -145 0 -25 -160 0 -25 -175 0 -25 -190 0 -25 -205 0 -25 -220 0 -25 -235 0 -40 -55 0 -40 -70 0 -40 -85 0 -40 -100 0 -40 -115 0 -40 -130 0 -40 -145 0 -40 -160 0 -40 -175 0 -40 -190 0 -40 -205 0 -40 -220 0 -40 -235 0 -55 -70 0 -55 -85 0 -55 -100 0 -55 -115 0 -55 -130 0 -55 -145 0 -55 -160 0 -55 -175 0 -55 -190 0 -55 -205 0 -55 -220 0 -55 -235 0 -70 -85 0 -70 -100 0 -70 -115 0 -70 -130 0 -70 -145 0 -70 -160 0 -70 -175 0 -70 -190 0 -70 -205 0 -70 -220 0 -70 -235 0 -85 -100 0 -85 -115 0 -85 -130 0 -85 -145 0 -85 -160 0 -85 -175 0 -85 -190 0 -85 -205 0 -85 -220 0 -85 -235 0 -100 -115 0 -100 -130 0 -100 -145 0 -100 -160 0 -100 -175 0 -100 -190 0 -100 -205 0 -100 -220 0 -100 -235 0 -115 -130 0 -115 -145 0 -115 -160 0 -115 -175 0 -115 -190 0 -115 -205 0 -115 -220 0 -115 -235 0 -130 -145 0 -130 -160 0 -130 -175 0 -130 -190 0 -130 -205 0 -130 -220 0 -130 -235 0 -145 -160 0 -145 -175 0 -145 -190 0 -145 -205 0 -145 -220 0 -145 -235 0 -160 -175 0 -160 -190 0 -160 -205 0 -160 -220 0 -160 -235 0 -175 -190 0 -175 -205 0 -175 -220 0 -175 -235 0 -190 -205 0 -190 -220 0 -190 -235 0 -205 -220 0 -205 -235 0 -220 -235 0 -11 -26 0 -11 -41 0 -11 -56 0 -11 -71 0 -11 -86 0 -11 -101 0 -11 -116 0 -11 -131 0 -11 -146 0 -11 -161 0 -11 -176 0 -11 -191 0 -11 -206 0 -11 -221 0 -11 -236 0 -26 -41 0 -26 -56 0 -26 -71 0 -26 -86 0 -26 -101 0 -26 -116 0 -26 -131 0 -26 -146 0 -26 -161 0 -26 -176 0 -26 -191 0 -26 -206 0 -26 -221 0 -26 -236 0 -41 -56 0 -41 -71 0 -41 -86 0 -41 -101 0 -41 -116 0 -41 -131 0 -41 -146 0 -41 -161 0 -41 -176 0 -41 -191 0 -41 -206 0 -41 -221 0 -41 -236 0 -56 -71 0 -56 -86 0 -56 -101 0 -56 -116 0 -56 -131 0 -56 -146 0 -56 -161 0 -56 -176 0 -56 -191 0 -56 -206 0 -56 -221 0 -56 -236 0 -71 -86 0 -71 -101 0 -71 -116 0 -71 -131 0 -71 -146 0 -71 -161 0 -71 -176 0 -71 -191 0 -71 -206 0 -71 -221 0 -71 -236 0 -86 -101 0 -86 -116 0 -86 -131 0 -86 -146 0 -86 -161 0 -86 -176 0 -86 -191 0 -86 -206 0 -86 -221 0 -86 -236 0 -101 -116 0 -101 -131 0 -101 -146 0 -101 -161 0 -101 -176 0 -101 -191 0 -101 -206 0 -101 -221 0 -101 -236 0 -116 -131 0 -116 -146 0 -116 -161 0 -116 -176 0 -116 -191 0 -116 -206 0 -116 -221 0 -116 -236 0 -131 -146 0 -131 -161 0 -131 -176 0 -131 -191 0 -131 -206 0 -131 -221 0 -131 -236 0 -146 -161 0 -146 -176 0 -146 -191 0 -146 -206 0 -146 -221 0 -146 -236 0 -161 -176 0 -161 -191 0 -161 -206 0 -161 -221 0 -161 -236 0 -176 -191 0 -176 -206 0 -176 -221 0 -176 -236 0 -191 -206 0 -191 -221 0 -191 -236 0 -206 -221 0 -206 -236 0 -221 -236 0 -12 -27 0 -12 -42 0 -12 -57 0 -12 -72 0 -12 -87 0 -12 -102 0 -12 -117 0 -12 -132 0 -12 -147 0 -12 -162 0 -12 -177 0 -12 -192 0 -12 -207 0 -12 -222 0 -12 -237 0 -27 -42 0 -27 -57 0 -27 -72 0 -27 -87 0 -27 -102 0 -27 -117 0 -27 -132 0 -27 -147 0 -27 -162 0 -27 -177 0 -27 -192 0 -27 -207 0 -27 -222 0 -27 -237 0 -42 -57 0 -42 -72 0 -42 -87 0 -42 -102 0 -42 -117 0 -42 -132 0 -42 -147 0 -42 -162 0 -42 -177 0 -42 -192 0 -42 -207 0 -42 -222 0 -42 -237 0 -57 -72 0 -57 -87 0 -57 -102 0 -57 -117 0 -57 -132 0 -57 -147 0 -57 -162 0 -57 -177 0 -57 -192 0 -57 -207 0 -57 -222 0 -57 -237 0 -72 -87 0 -72 -102 0 -72 -117 0 -72 -132 0 -72 -147 0 -72 -162 0 -72 -177 0 -72 -192 0 -72 -207 0 -72 -222 0 -72 -237 0 -87 -102 0 -87 -117 0 -87 -132 0 -87 -147 0 -87 -162 0 -87 -177 0 -87 -192 0 -87 -207 0 -87 -222 0 -87 -237 0 -102 -117 0 -102 -132 0 -102 -147 0 -102 -162 0 -102 -177 0 -102 -192 0 -102 -207 0 -102 -222 0 -102 -237 0 -117 -132 0 -117 -147 0 -117 -162 0 -117 -177 0 -117 -192 0 -117 -207 0 -117 -222 0 -117 -237 0 -132 -147 0 -132 -162 0 -132 -177 0 -132 -192 0 -132 -207 0 -132 -222 0 -132 -237 0 -147 -162 0 -147 -177 0 -147 -192 0 -147 -207 0 -147 -222 0 -147 -237 0 -162 -177 0 -162 -192 0 -162 -207 0 -162 -222 0 -162 -237 0 -177 -192 0 -177 -207 0 -177 -222 0 -177 -237 0 -192 -207 0 -192 -222 0 -192 -237 0 -207 -222 0 -207 -237 0 -222 -237 0 -13 -28 0 -13 -43 0 -13 -58 0 -13 -73 0 -13 -88 0 -13 -103 0 -13 -118 0 -13 -133 0 -13 -148 0 -13 -163 0 -13 -178 0 -13 -193 0 -13 -208 0 -13 -223 0 -13 -238 0 -28 -43 0 -28 -58 0 -28 -73 0 -28 -88 0 -28 -103 0 -28 -118 0 -28 -133 0 -28 -148 0 -28 -163 0 -28 -178 0 -28 -193 0 -28 -208 0 -28 -223 0 -28 -238 0 -43 -58 0 -43 -73 0 -43 -88 0 -43 -103 0 -43 -118 0 -43 -133 0 -43 -148 0 -43 -163 0 -43 -178 0 -43 -193 0 -43 -208 0 -43 -223 0 -43 -238 0 -58 -73 0 -58 -88 0 -58 -103 0 -58 -118 0 -58 -133 0 -58 -148 0 -58 -163 0 -58 -178 0 -58 -193 0 -58 -208 0 -58 -223 0 -58 -238 0 -73 -88 0 -73 -103 0 -73 -118 0 -73 -133 0 -73 -148 0 -73 -163 0 -73 -178 0 -73 -193 0 -73 -208 0 -73 -223 0 -73 -238 0 -88 -103 0 -88 -118 0 -88 -133 0 -88 -148 0 -88 -163 0 -88 -178 0 -88 -193 0 -88 -208 0 -88 -223 0 -88 -238 0 -103 -118 0 -103 -133 0 -103 -148 0 -103 -163 0 -103 -178 0 -103 -193 0 -103 -208 0 -103 -223 0 -103 -238 0 -118 -133 0 -118 -148 0 -118 -163 0 -118 -178 0 -118 -193 0 -118 -208 0 -118 -223 0 -118 -238 0 -133 -148 0 -133 -163 0 -133 -178 0 -133 -193 0 -133 -208 0 -133 -223 0 -133 -238 0 -148 -163 0 -148 -178 0 -148 -193 0 -148 -208 0 -148 -223 0 -148 -238 0 -163 -178 0 -163 -193 0 -163 -208 0 -163 -223 0 -163 -238 0 -178 -193 0 -178 -208 0 -178 -223 0 -178 -238 0 -193 -208 0 -193 -223 0 -193 -238 0 -208 -223 0 -208 -238 0 -223 -238 0 -14 -29 0 -14 -44 0 -14 -59 0 -14 -74 0 -14 -89 0 -14 -104 0 -14 -119 0 -14 -134 0 -14 -149 0 -14 -164 0 -14 -179 0 -14 -194 0 -14 -209 0 -14 -224 0 -14 -239 0 -29 -44 0 -29 -59 0 -29 -74 0 -29 -89 0 -29 -104 0 -29 -119 0 -29 -134 0 -29 -149 0 -29 -164 0 -29 -179 0 -29 -194 0 -29 -209 0 -29 -224 0 -29 -239 0 -44 -59 0 -44 -74 0 -44 -89 0 -44 -104 0 -44 -119 0 -44 -134 0 -44 -149 0 -44 -164 0 -44 -179 0 -44 -194 0 -44 -209 0 -44 -224 0 -44 -239 0 -59 -74 0 -59 -89 0 -59 -104 0 -59 -119 0 -59 -134 0 -59 -149 0 -59 -164 0 -59 -179 0 -59 -194 0 -59 -209 0 -59 -224 0 -59 -239 0 -74 -89 0 -74 -104 0 -74 -119 0 -74 -134 0 -74 -149 0 -74 -164 0 -74 -179 0 -74 -194 0 -74 -209 0 -74 -224 0 -74 -239 0 -89 -104 0 -89 -119 0 -89 -134 0 -89 -149 0 -89 -164 0 -89 -179 0 -89 -194 0 -89 -209 0 -89 -224 0 -89 -239 0 -104 -119 0 -104 -134 0 -104 -149 0 -104 -164 0 -104 -179 0 -104 -194 0 -104 -209 0 -104 -224 0 -104 -239 0 -119 -134 0 -119 -149 0 -119 -164 0 -119 -179 0 -119 -194 0 -119 -209 0 -119 -224 0 -119 -239 0 -134 -149 0 -134 -164 0 -134 -179 0 -134 -194 0 -134 -209 0 -134 -224 0 -134 -239 0 -149 -164 0 -149 -179 0 -149 -194 0 -149 -209 0 -149 -224 0 -149 -239 0 -164 -179 0 -164 -194 0 -164 -209 0 -164 -224 0 -164 -239 0 -179 -194 0 -179 -209 0 -179 -224 0 -179 -239 0 -194 -209 0 -194 -224 0 -194 -239 0 -209 -224 0 -209 -239 0 -224 -239 0 -15 -30 0 -15 -45 0 -15 -60 0 -15 -75 0 -15 -90 0 -15 -105 0 -15 -120 0 -15 -135 0 -15 -150 0 -15 -165 0 -15 -180 0 -15 -195 0 -15 -210 0 -15 -225 0 -15 -240 0 -30 -45 0 -30 -60 0 -30 -75 0 -30 -90 0 -30 -105 0 -30 -120 0 -30 -135 0 -30 -150 0 -30 -165 0 -30 -180 0 -30 -195 0 -30 -210 0 -30 -225 0 -30 -240 0 -45 -60 0 -45 -75 0 -45 -90 0 -45 -105 0 -45 -120 0 -45 -135 0 -45 -150 0 -45 -165 0 -45 -180 0 -45 -195 0 -45 -210 0 -45 -225 0 -45 -240 0 -60 -75 0 -60 -90 0 -60 -105 0 -60 -120 0 -60 -135 0 -60 -150 0 -60 -165 0 -60 -180 0 -60 -195 0 -60 -210 0 -60 -225 0 -60 -240 0 -75 -90 0 -75 -105 0 -75 -120 0 -75 -135 0 -75 -150 0 -75 -165 0 -75 -180 0 -75 -195 0 -75 -210 0 -75 -225 0 -75 -240 0 -90 -105 0 -90 -120 0 -90 -135 0 -90 -150 0 -90 -165 0 -90 -180 0 -90 -195 0 -90 -210 0 -90 -225 0 -90 -240 0 -105 -120 0 -105 -135 0 -105 -150 0 -105 -165 0 -105 -180 0 -105 -195 0 -105 -210 0 -105 -225 0 -105 -240 0 -120 -135 0 -120 -150 0 -120 -165 0 -120 -180 0 -120 -195 0 -120 -210 0 -120 -225 0 -120 -240 0 -135 -150 0 -135 -165 0 -135 -180 0 -135 -195 0 -135 -210 0 -135 -225 0 -135 -240 0 -150 -165 0 -150 -180 0 -150 -195 0 -150 -210 0 -150 -225 0 -150 -240 0 -165 -180 0 -165 -195 0 -165 -210 0 -165 -225 0 -165 -240 0 -180 -195 0 -180 -210 0 -180 -225 0 -180 -240 0 -195 -210 0 -195 -225 0 -195 -240 0 -210 -225 0 -210 -240 0 -225 -240 0