a <- [ 1 -> 1000, 2 -> 1000, 3 -> 1000, 4 -> 1000, 5 -> 1000, 6 -> 1000, 7 -> 1000, 8 -> 1000, 9 -> 1000, 10 -> 1000, 11 -> 1000, 12 -> 1000, 13 -> 1000, 14 -> 1000, 15 -> 1000, 16 -> 1000, 17 -> 1000, 18 -> 1000, 19 -> 1000, 20 -> 1000, 21 -> 1000, 22 -> 1000, 23 -> 1000, 24 -> 1000, 25 -> 1000, 26 -> 1000, 27 -> 1000, 28 -> 1000, 29 -> 1000, 30 -> 1000, 31 -> 1000, 32 -> 1000, 33 -> 1000, 34 -> 1000, 35 -> 1000, 36 -> 1000, 37 -> 1000, 38 -> 1000, 39 -> 1000, 40 -> 1000, 41 -> 1000, 42 -> 1000, 43 -> 1000, 44 -> 1000, 45 -> 1000, 46 -> 1000, 47 -> 1000, 48 -> 1000, 49 -> 1000, 50 -> 1000, 51 -> 1000, 52 -> 1000, 53 -> 1000, 54 -> 1000, 55 -> 1000, 56 -> 1000, 57 -> 1000, 58 -> 1000, 59 -> 1000, 60 -> 1000, 61 -> 1000, 62 -> 1000, 63 -> 1000, 64 -> 1000, 65 -> 1000, 66 -> 1000, 67 -> 1000, 68 -> 1000, 69 -> 1000, 70 -> 1000, 71 -> 1000, 72 -> 1000, 73 -> 1000, 74 -> 1000, 75 -> 1000, 76 -> 1000, 77 -> 1000, 78 -> 1000, 79 -> 1000, 80 -> 1000, 81 -> 1000, 82 -> 1000, 83 -> 1000, 84 -> 1000, 85 -> 1000, 86 -> 1000, 87 -> 1000, 88 -> 1000, 89 -> 1000, 90 -> 1000, 91 -> 1000, 92 -> 1000, 93 -> 1000, 94 -> 1000, 95 -> 1000, 96 -> 1000, 97 -> 1000, 98 -> 1000, 99 -> 1000, 100 -> 1000, 101 -> 1000, 102 -> 1000, 103 -> 1000, 104 -> 1000, 105 -> 1000, 106 -> 1000, 107 -> 1000, 108 -> 1000, 109 -> 1000, 110 -> 1000, 111 -> 1000, 112 -> 1000, 113 -> 1000, 114 -> 1000, 115 -> 1000, 116 -> 1000, 117 -> 1000, 118 -> 1000, 119 -> 1000, 120 -> 1000, 121 -> 1000, 122 -> 1000, 123 -> 1000, 124 -> 1000, 125 -> 1000, 126 -> 1000, 127 -> 1000, 128 -> 1000, 129 -> 1000, 130 -> 1000, 131 -> 1000, 132 -> 1000, 133 -> 1000, 134 -> 1000, 135 -> 1000, 136 -> 1000, 137 -> 1000, 138 -> 1000, 139 -> 1000, 140 -> 1000, 141 -> 1000, 142 -> 1000, 143 -> 1000, 144 -> 1000, 145 -> 1000, 146 -> 1000, 147 -> 1000, 148 -> 1000, 149 -> 1000, 150 -> 1000, 151 -> 1000, 152 -> 1000, 153 -> 1000, 154 -> 1000, 155 -> 1000, 156 -> 1000, 157 -> 1000, 158 -> 1000, 159 -> 1000, 160 -> 1000, 161 -> 1000, 162 -> 1000, 163 -> 1000, 164 -> 1000, 165 -> 1000, 166 -> 1000, 167 -> 1000, 168 -> 1000, 169 -> 1000, 170 -> 1000, 171 -> 1000, 172 -> 1000, 173 -> 1000, 174 -> 1000, 175 -> 1000, 176 -> 1000, 177 -> 1000, 178 -> 1000, 179 -> 1000, 180 -> 1000, 181 -> 1000, 182 -> 1000, 183 -> 1000, 184 -> 1000, 185 -> 1000, 186 -> 1000, 187 -> 1000, 188 -> 1000, 189 -> 1000, 190 -> 1000, 191 -> 1000, 192 -> 1000, 193 -> 1000, 194 -> 1000, 195 -> 1000, 196 -> 1000, 197 -> 1000, 198 -> 1000, 199 -> 1000, 200 -> 1000, 201 -> 1000, 202 -> 1000, 203 -> 1000, 204 -> 1000, 205 -> 1000, 206 -> 1000, 207 -> 1000, 208 -> 1000, 209 -> 1000, 210 -> 1000, 211 -> 1000, 212 -> 1000, 213 -> 1000, 214 -> 1000, 215 -> 1000, 216 -> 1000, 217 -> 1000, 218 -> 1000, 219 -> 1000, 220 -> 1000, 221 -> 1000, 222 -> 1000, 223 -> 1000, 224 -> 1000, 225 -> 1000, 226 -> 1000, 227 -> 1000, 228 -> 1000, 229 -> 1000, 230 -> 1000, 231 -> 1000, 232 -> 1000, 233 -> 1000, 234 -> 1000, 235 -> 1000, 236 -> 1000, 237 -> 1000, 238 -> 1000, 239 -> 1000, 240 -> 1000, 241 -> 1000, 242 -> 1000, 243 -> 1000, 244 -> 1000, 245 -> 1000, 246 -> 1000, 247 -> 1000, 248 -> 1000, 249 -> 1000, 250 -> 1000, 251 -> 1000, 252 -> 1000, 253 -> 1000, 254 -> 1000, 255 -> 1000, 256 -> 1000, 257 -> 1000, 258 -> 1000, 259 -> 1000, 260 -> 1000, 261 -> 1000, 262 -> 1000, 263 -> 1000, 264 -> 1000, 265 -> 1000, 266 -> 1000, 267 -> 1000, 268 -> 1000, 269 -> 1000, 270 -> 1000, 271 -> 1000, 272 -> 1000, 273 -> 1000, 274 -> 1000, 275 -> 1000, 276 -> 1000, 277 -> 1000, 278 -> 1000, 279 -> 1000, 280 -> 1000, 281 -> 1000, 282 -> 1000, 283 -> 1000, 284 -> 1000, 285 -> 1000, 286 -> 1000, 287 -> 1000, 288 -> 1000, 289 -> 1000, 290 -> 1000, 291 -> 1000, 292 -> 1000, 293 -> 1000, 294 -> 1000, 295 -> 1000, 296 -> 1000, 297 -> 1000, 298 -> 1000, 299 -> 1000, 300 -> 1000, 301 -> 1000, 302 -> 1000, 303 -> 1000, 304 -> 1000, 305 -> 1000, 306 -> 1000, 307 -> 1000, 308 -> 1000, 309 -> 1000, 310 -> 1000, 311 -> 1000, 312 -> 1000, 313 -> 1000, 314 -> 1000, 315 -> 1000, 316 -> 1000, 317 -> 1000, 318 -> 1000, 319 -> 1000, 320 -> 1000, 321 -> 1000, 322 -> 1000, 323 -> 1000, 324 -> 1000, 325 -> 1000, 326 -> 1000, 327 -> 1000, 328 -> 1000, 329 -> 1000, 330 -> 1000, 331 -> 1000, 332 -> 1000, 333 -> 1000, 334 -> 1000, 335 -> 1000, 336 -> 1000, 337 -> 1000, 338 -> 1000, 339 -> 1000, 340 -> 1000, 341 -> 1000, 342 -> 1000, 343 -> 1000, 344 -> 1000, 345 -> 1000, 346 -> 1000, 347 -> 1000, 348 -> 1000, 349 -> 1000, 350 -> 1000, 351 -> 1000, 352 -> 1000, 353 -> 1000, 354 -> 1000, 355 -> 1000, 356 -> 1000, 357 -> 1000, 358 -> 1000, 359 -> 1000, 360 -> 1000, 361 -> 1000, 362 -> 1000, 363 -> 1000, 364 -> 1000, 365 -> 1000, 366 -> 1000, 367 -> 1000, 368 -> 1000, 369 -> 1000, 370 -> 1000, 371 -> 1000, 372 -> 1000, 373 -> 1000, 374 -> 1000, 375 -> 1000, 376 -> 1000, 377 -> 1000, 378 -> 1000, 379 -> 1000, 380 -> 1000, 381 -> 1000, 382 -> 1000, 383 -> 1000, 384 -> 1000, 385 -> 1000, 386 -> 1000, 387 -> 1000, 388 -> 1000, 389 -> 1000, 390 -> 1000, 391 -> 1000, 392 -> 1000, 393 -> 1000, 394 -> 1000, 395 -> 1000, 396 -> 1000, 397 -> 1000, 398 -> 1000, 399 -> 1000, 400 -> 1000, 401 -> 1000, 402 -> 1000, 403 -> 1000, 404 -> 1000, 405 -> 1000, 406 -> 1000, 407 -> 1000, 408 -> 1000, 409 -> 1000, 410 -> 1000, 411 -> 1000, 412 -> 1000, 413 -> 1000, 414 -> 1000, 415 -> 1000, 416 -> 1000, 417 -> 1000, 418 -> 1000, 419 -> 1000, 420 -> 1000, 421 -> 1000, 422 -> 1000, 423 -> 1000, 424 -> 1000, 425 -> 1000, 426 -> 1000, 427 -> 1000, 428 -> 1000, 429 -> 1000, 430 -> 1000, 431 -> 1000, 432 -> 1000, 433 -> 1000, 434 -> 1000, 435 -> 1000, 436 -> 1000, 437 -> 1000, 438 -> 1000, 439 -> 1000, 440 -> 1000, 441 -> 1000, 442 -> 1000, 443 -> 1000, 444 -> 1000, 445 -> 1000, 446 -> 1000, 447 -> 1000, 448 -> 1000, 449 -> 1000, 450 -> 1000, 451 -> 1000, 452 -> 1000, 453 -> 1000, 454 -> 1000, 455 -> 1000, 456 -> 1000, 457 -> 1000, 458 -> 1000, 459 -> 1000, 460 -> 1000, 461 -> 1000, 462 -> 1000, 463 -> 1000, 464 -> 1000, 465 -> 1000, 466 -> 1000, 467 -> 1000, 468 -> 1000, 469 -> 1000, 470 -> 1000, 471 -> 1000, 472 -> 1000, 473 -> 1000, 474 -> 1000, 475 -> 1000, 476 -> 1000, 477 -> 1000, 478 -> 1000, 479 -> 1000, 480 -> 1000, 481 -> 1000, 482 -> 1000, 483 -> 1000, 484 -> 1000, 485 -> 1000, 486 -> 1000, 487 -> 1000, 488 -> 1000, 489 -> 1000, 490 -> 1000, 491 -> 1000, 492 -> 1000, 493 -> 1000, 494 -> 1000, 495 -> 1000, 496 -> 1000, 497 -> 1000, 498 -> 1000, 499 -> 1000, 500 -> 1000, 501 -> 1000, 502 -> 1000, 503 -> 1000, 504 -> 1000, 505 -> 1000, 506 -> 1000, 507 -> 1000, 508 -> 1000, 509 -> 1000, 510 -> 1000, 511 -> 1000, 512 -> 1000, 513 -> 1000, 514 -> 1000, 515 -> 1000, 516 -> 1000, 517 -> 1000, 518 -> 1000, 519 -> 1000, 520 -> 1000, 521 -> 1000, 522 -> 1000, 523 -> 1000, 524 -> 1000, 525 -> 1000, 526 -> 1000, 527 -> 1000, 528 -> 1000, 529 -> 1000, 530 -> 1000, 531 -> 1000, 532 -> 1000, 533 -> 1000, 534 -> 1000, 535 -> 1000, 536 -> 1000, 537 -> 1000, 538 -> 1000, 539 -> 1000, 540 -> 1000, 541 -> 1000, 542 -> 1000, 543 -> 1000, 544 -> 1000, 545 -> 1000, 546 -> 1000, 547 -> 1000, 548 -> 1000, 549 -> 1000, 550 -> 1000, 551 -> 1000, 552 -> 1000, 553 -> 1000, 554 -> 1000, 555 -> 1000, 556 -> 1000, 557 -> 1000, 558 -> 1000, 559 -> 1000, 560 -> 1000, 561 -> 1000, 562 -> 1000, 563 -> 1000, 564 -> 1000, 565 -> 1000, 566 -> 1000, 567 -> 1000, 568 -> 1000, 569 -> 1000, 570 -> 1000, 571 -> 1000, 572 -> 1000, 573 -> 1000, 574 -> 1000, 575 -> 1000, 576 -> 1000, 577 -> 1000, 578 -> 1000, 579 -> 1000, 580 -> 1000, 581 -> 1000, 582 -> 1000, 583 -> 1000, 584 -> 1000, 585 -> 1000, 586 -> 1000, 587 -> 1000, 588 -> 1000, 589 -> 1000, 590 -> 1000, 591 -> 1000, 592 -> 1000, 593 -> 1000, 594 -> 1000, 595 -> 1000, 596 -> 1000, 597 -> 1000, 598 -> 1000, 599 -> 1000, 600 -> 1000 ] ; pp(if(card(dom(a))==600 -> 'ok, else -> 'error)); quit.