Cleanup verif directory.

[urcu.git] / formal-model / results / urcu-controldataflow-ipi / urcu_free_no_rmb.spin.input.trail

diff --git a/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_rmb.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_rmb.spin.input.trail
deleted file mode 100644 (file)
index ad65225..0000000
--- a/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_rmb.spin.input.trail
+++ /dev/null
@@ -1,1627 +0,0 @@
--2:3:-2
--4:-4:-4
-1:0:4811
-2:3:4731
-3:3:4734
-4:3:4734
-5:3:4737
-6:3:4745
-7:3:4745
-8:3:4748
-9:3:4754
-10:3:4758
-11:3:4758
-12:3:4761
-13:3:4771
-14:3:4779
-15:3:4779
-16:3:4782
-17:3:4788
-18:3:4792
-19:3:4792
-20:3:4795
-21:3:4801
-22:3:4805
-23:3:4806
-24:0:4811
-25:3:4808
-26:0:4811
-27:2:3039
-28:0:4811
-29:2:3045
-30:0:4811
-31:2:3046
-32:0:4811
-33:2:3048
-34:0:4811
-35:2:3049
-36:0:4811
-37:2:3050
-38:2:3051
-39:2:3055
-40:2:3056
-41:2:3064
-42:2:3065
-43:2:3069
-44:2:3070
-45:2:3078
-46:2:3083
-47:2:3087
-48:2:3088
-49:2:3096
-50:2:3097
-51:2:3101
-52:2:3102
-53:2:3096
-54:2:3097
-55:2:3101
-56:2:3102
-57:2:3110
-58:2:3115
-59:2:3116
-60:2:3127
-61:2:3128
-62:2:3129
-63:2:3140
-64:2:3145
-65:2:3146
-66:2:3157
-67:2:3158
-68:2:3159
-69:2:3157
-70:2:3158
-71:2:3159
-72:2:3170
-73:2:3178
-74:0:4811
-75:2:3049
-76:0:4811
-77:2:3182
-78:2:3186
-79:2:3187
-80:2:3191
-81:2:3195
-82:2:3196
-83:2:3200
-84:2:3208
-85:2:3209
-86:2:3213
-87:2:3217
-88:2:3218
-89:2:3213
-90:2:3214
-91:2:3222
-92:0:4811
-93:2:3049
-94:0:4811
-95:2:3230
-96:2:3231
-97:2:3232
-98:0:4811
-99:2:3049
-100:0:4811
-101:2:3237
-102:0:4811
-103:2:3940
-104:2:3941
-105:2:3945
-106:2:3949
-107:2:3950
-108:2:3954
-109:2:3959
-110:2:3967
-111:2:3971
-112:2:3972
-113:2:3967
-114:2:3971
-115:2:3972
-116:2:3976
-117:2:3983
-118:2:3990
-119:2:3991
-120:2:3998
-121:2:4003
-122:2:4010
-123:2:4011
-124:2:4010
-125:2:4011
-126:2:4018
-127:2:4022
-128:0:4811
-129:2:4027
-130:0:4811
-131:2:4028
-132:0:4811
-133:2:4029
-134:0:4811
-135:2:4030
-136:0:4811
-137:1:2
-138:0:4811
-139:2:4031
-140:0:4811
-141:1:8
-142:0:4811
-143:1:9
-144:0:4811
-145:2:4030
-146:0:4811
-147:1:10
-148:0:4811
-149:2:4031
-150:0:4811
-151:1:11
-152:0:4811
-153:2:4030
-154:0:4811
-155:1:12
-156:0:4811
-157:2:4031
-158:0:4811
-159:1:13
-160:0:4811
-161:2:4030
-162:0:4811
-163:1:14
-164:0:4811
-165:2:4031
-166:0:4811
-167:1:15
-168:0:4811
-169:1:16
-170:0:4811
-171:2:4030
-172:0:4811
-173:1:17
-174:0:4811
-175:2:4031
-176:0:4811
-177:1:26
-178:0:4811
-179:2:4030
-180:0:4811
-181:1:30
-182:1:31
-183:1:35
-184:1:39
-185:1:40
-186:1:44
-187:1:52
-188:1:53
-189:1:57
-190:1:61
-191:1:62
-192:1:57
-193:1:61
-194:1:62
-195:1:66
-196:1:73
-197:1:80
-198:1:81
-199:1:88
-200:1:93
-201:1:100
-202:1:101
-203:1:100
-204:1:101
-205:1:108
-206:1:112
-207:0:4811
-208:2:4031
-209:0:4811
-210:1:117
-211:0:4811
-212:2:4032
-213:0:4811
-214:2:4037
-215:0:4811
-216:2:4038
-217:0:4811
-218:2:4046
-219:2:4047
-220:2:4051
-221:2:4055
-222:2:4056
-223:2:4060
-224:2:4068
-225:2:4069
-226:2:4073
-227:2:4077
-228:2:4078
-229:2:4073
-230:2:4077
-231:2:4078
-232:2:4082
-233:2:4089
-234:2:4096
-235:2:4097
-236:2:4104
-237:2:4109
-238:2:4116
-239:2:4117
-240:2:4116
-241:2:4117
-242:2:4124
-243:2:4128
-244:0:4811
-245:2:3239
-246:2:3921
-247:0:4811
-248:2:3049
-249:0:4811
-250:2:3240
-251:0:4811
-252:2:3049
-253:0:4811
-254:2:3243
-255:2:3244
-256:2:3248
-257:2:3249
-258:2:3257
-259:2:3258
-260:2:3262
-261:2:3263
-262:2:3271
-263:2:3276
-264:2:3280
-265:2:3281
-266:2:3289
-267:2:3290
-268:2:3294
-269:2:3295
-270:2:3289
-271:2:3290
-272:2:3294
-273:2:3295
-274:2:3303
-275:2:3308
-276:2:3309
-277:2:3320
-278:2:3321
-279:2:3322
-280:2:3333
-281:2:3338
-282:2:3339
-283:2:3350
-284:2:3351
-285:2:3352
-286:2:3350
-287:2:3351
-288:2:3352
-289:2:3363
-290:2:3370
-291:0:4811
-292:2:3049
-293:0:4811
-294:2:3374
-295:2:3375
-296:2:3376
-297:2:3388
-298:2:3389
-299:2:3393
-300:2:3394
-301:2:3402
-302:2:3407
-303:2:3411
-304:2:3412
-305:2:3420
-306:2:3421
-307:2:3425
-308:2:3426
-309:2:3420
-310:2:3421
-311:2:3425
-312:2:3426
-313:2:3434
-314:2:3439
-315:2:3440
-316:2:3451
-317:2:3452
-318:2:3453
-319:2:3464
-320:2:3469
-321:2:3470
-322:2:3481
-323:2:3482
-324:2:3483
-325:2:3481
-326:2:3482
-327:2:3483
-328:2:3494
-329:2:3505
-330:2:3506
-331:0:4811
-332:2:3049
-333:0:4811
-334:2:3512
-335:2:3513
-336:2:3517
-337:2:3518
-338:2:3526
-339:2:3527
-340:2:3531
-341:2:3532
-342:2:3540
-343:2:3545
-344:2:3549
-345:2:3550
-346:2:3558
-347:2:3559
-348:2:3563
-349:2:3564
-350:2:3558
-351:2:3559
-352:2:3563
-353:2:3564
-354:2:3572
-355:2:3577
-356:2:3578
-357:2:3589
-358:2:3590
-359:2:3591
-360:2:3602
-361:2:3607
-362:2:3608
-363:2:3619
-364:2:3620
-365:2:3621
-366:2:3619
-367:2:3620
-368:2:3621
-369:2:3632
-370:0:4811
-371:2:3049
-372:0:4811
-373:2:3641
-374:2:3642
-375:2:3646
-376:2:3647
-377:2:3655
-378:2:3656
-379:2:3660
-380:2:3661
-381:2:3669
-382:2:3674
-383:2:3678
-384:2:3679
-385:2:3687
-386:2:3688
-387:2:3692
-388:2:3693
-389:2:3687
-390:2:3688
-391:2:3692
-392:2:3693
-393:2:3701
-394:2:3706
-395:2:3707
-396:2:3718
-397:2:3719
-398:2:3720
-399:2:3731
-400:2:3736
-401:2:3737
-402:2:3748
-403:2:3749
-404:2:3750
-405:2:3748
-406:2:3749
-407:2:3750
-408:2:3761
-409:2:3768
-410:0:4811
-411:2:3049
-412:0:4811
-413:2:3772
-414:2:3773
-415:2:3774
-416:2:3786
-417:2:3787
-418:2:3791
-419:2:3792
-420:2:3800
-421:2:3805
-422:2:3809
-423:2:3810
-424:2:3818
-425:2:3819
-426:2:3823
-427:2:3824
-428:2:3818
-429:2:3819
-430:2:3823
-431:2:3824
-432:2:3832
-433:2:3837
-434:2:3838
-435:2:3849
-436:2:3850
-437:2:3851
-438:2:3862
-439:2:3867
-440:2:3868
-441:2:3879
-442:2:3880
-443:2:3881
-444:2:3879
-445:2:3880
-446:2:3881
-447:2:3892
-448:2:3902
-449:2:3903
-450:0:4811
-451:2:3049
-452:0:4811
-453:2:3909
-454:0:4811
-455:2:4534
-456:2:4535
-457:2:4539
-458:2:4543
-459:2:4544
-460:2:4548
-461:2:4556
-462:2:4557
-463:2:4561
-464:2:4565
-465:2:4566
-466:2:4561
-467:2:4565
-468:2:4566
-469:2:4570
-470:2:4577
-471:2:4584
-472:2:4585
-473:2:4592
-474:2:4597
-475:2:4604
-476:2:4605
-477:2:4604
-478:2:4605
-479:2:4612
-480:2:4616
-481:0:4811
-482:2:4621
-483:0:4811
-484:2:4622
-485:0:4811
-486:2:4623
-487:0:4811
-488:2:4624
-489:0:4811
-490:1:26
-491:0:4811
-492:2:4625
-493:0:4811
-494:1:30
-495:1:31
-496:1:35
-497:1:39
-498:1:40
-499:1:44
-500:1:52
-501:1:53
-502:1:57
-503:1:61
-504:1:62
-505:1:57
-506:1:61
-507:1:62
-508:1:66
-509:1:73
-510:1:80
-511:1:81
-512:1:88
-513:1:93
-514:1:100
-515:1:101
-516:1:100
-517:1:101
-518:1:108
-519:1:112
-520:0:4811
-521:2:4624
-522:0:4811
-523:1:117
-524:0:4811
-525:2:4625
-526:0:4811
-527:2:4626
-528:0:4811
-529:2:4631
-530:0:4811
-531:2:4632
-532:0:4811
-533:2:4640
-534:2:4641
-535:2:4645
-536:2:4649
-537:2:4650
-538:2:4654
-539:2:4662
-540:2:4663
-541:2:4667
-542:2:4671
-543:2:4672
-544:2:4667
-545:2:4671
-546:2:4672
-547:2:4676
-548:2:4683
-549:2:4690
-550:2:4691
-551:2:4698
-552:2:4703
-553:2:4710
-554:2:4711
-555:2:4710
-556:2:4711
-557:2:4718
-558:2:4722
-559:0:4811
-560:2:3911
-561:2:3921
-562:0:4811
-563:2:3049
-564:0:4811
-565:2:3912
-566:2:3913
-567:0:4811
-568:2:3049
-569:0:4811
-570:2:3917
-571:0:4811
-572:2:3925
-573:0:4811
-574:2:3046
-575:0:4811
-576:2:3048
-577:0:4811
-578:2:3049
-579:0:4811
-580:2:3050
-581:2:3051
-582:2:3055
-583:2:3056
-584:2:3064
-585:2:3065
-586:2:3069
-587:2:3070
-588:2:3078
-589:2:3083
-590:2:3087
-591:2:3088
-592:2:3096
-593:2:3097
-594:2:3098
-595:2:3096
-596:2:3097
-597:2:3101
-598:2:3102
-599:2:3110
-600:2:3115
-601:2:3116
-602:2:3127
-603:2:3128
-604:2:3129
-605:2:3140
-606:2:3145
-607:2:3146
-608:2:3157
-609:2:3158
-610:2:3159
-611:2:3157
-612:2:3158
-613:2:3159
-614:2:3170
-615:2:3178
-616:0:4811
-617:2:3049
-618:0:4811
-619:2:3182
-620:2:3186
-621:2:3187
-622:2:3191
-623:2:3195
-624:2:3196
-625:2:3200
-626:2:3208
-627:2:3209
-628:2:3213
-629:2:3214
-630:2:3213
-631:2:3217
-632:2:3218
-633:2:3222
-634:0:4811
-635:2:3049
-636:0:4811
-637:2:3230
-638:2:3231
-639:2:3232
-640:0:4811
-641:2:3049
-642:0:4811
-643:2:3237
-644:0:4811
-645:2:3940
-646:2:3941
-647:2:3945
-648:2:3949
-649:2:3950
-650:2:3954
-651:2:3959
-652:2:3967
-653:2:3971
-654:2:3972
-655:2:3967
-656:2:3971
-657:2:3972
-658:2:3976
-659:2:3983
-660:2:3990
-661:2:3991
-662:2:3998
-663:2:4003
-664:2:4010
-665:2:4011
-666:2:4010
-667:2:4011
-668:2:4018
-669:2:4022
-670:0:4811
-671:2:4027
-672:0:4811
-673:2:4028
-674:0:4811
-675:2:4029
-676:0:4811
-677:2:4030
-678:0:4811
-679:1:26
-680:0:4811
-681:2:4031
-682:0:4811
-683:1:30
-684:1:31
-685:1:35
-686:1:39
-687:1:40
-688:1:44
-689:1:52
-690:1:53
-691:1:57
-692:1:61
-693:1:62
-694:1:57
-695:1:61
-696:1:62
-697:1:66
-698:1:73
-699:1:80
-700:1:81
-701:1:88
-702:1:93
-703:1:100
-704:1:101
-705:1:100
-706:1:101
-707:1:108
-708:1:112
-709:0:4811
-710:2:4030
-711:0:4811
-712:1:117
-713:0:4811
-714:2:4031
-715:0:4811
-716:2:4032
-717:0:4811
-718:2:4037
-719:0:4811
-720:2:4038
-721:0:4811
-722:2:4046
-723:2:4047
-724:2:4051
-725:2:4055
-726:2:4056
-727:2:4060
-728:2:4068
-729:2:4069
-730:2:4073
-731:2:4077
-732:2:4078
-733:2:4073
-734:2:4077
-735:2:4078
-736:2:4082
-737:2:4089
-738:2:4096
-739:2:4097
-740:2:4104
-741:2:4109
-742:2:4116
-743:2:4117
-744:2:4116
-745:2:4117
-746:2:4124
-747:2:4128
-748:0:4811
-749:2:3239
-750:2:3921
-751:0:4811
-752:2:3049
-753:0:4811
-754:2:3240
-755:0:4811
-756:2:3049
-757:0:4811
-758:2:3243
-759:2:3244
-760:2:3248
-761:2:3249
-762:2:3257
-763:2:3258
-764:2:3262
-765:2:3263
-766:2:3271
-767:2:3276
-768:2:3280
-769:2:3281
-770:2:3289
-771:2:3290
-772:2:3294
-773:2:3295
-774:2:3289
-775:2:3290
-776:2:3294
-777:2:3295
-778:2:3303
-779:2:3308
-780:2:3309
-781:2:3320
-782:2:3321
-783:2:3322
-784:2:3333
-785:2:3338
-786:2:3339
-787:2:3350
-788:2:3351
-789:2:3352
-790:2:3350
-791:2:3351
-792:2:3352
-793:2:3363
-794:2:3370
-795:0:4811
-796:2:3049
-797:0:4811
-798:2:3374
-799:2:3375
-800:2:3376
-801:2:3388
-802:2:3389
-803:2:3393
-804:2:3394
-805:2:3402
-806:2:3407
-807:2:3411
-808:2:3412
-809:2:3420
-810:2:3421
-811:2:3425
-812:2:3426
-813:2:3420
-814:2:3421
-815:2:3425
-816:2:3426
-817:2:3434
-818:2:3439
-819:2:3440
-820:2:3451
-821:2:3452
-822:2:3453
-823:2:3464
-824:2:3469
-825:2:3470
-826:2:3481
-827:2:3482
-828:2:3483
-829:2:3481
-830:2:3482
-831:2:3483
-832:2:3494
-833:2:3505
-834:2:3506
-835:0:4811
-836:2:3049
-837:0:4811
-838:2:3512
-839:2:3513
-840:2:3517
-841:2:3518
-842:2:3526
-843:2:3527
-844:2:3531
-845:2:3532
-846:2:3540
-847:2:3545
-848:2:3549
-849:2:3550
-850:2:3558
-851:2:3559
-852:2:3563
-853:2:3564
-854:2:3558
-855:2:3559
-856:2:3563
-857:2:3564
-858:2:3572
-859:2:3577
-860:2:3578
-861:2:3589
-862:2:3590
-863:2:3591
-864:2:3602
-865:2:3607
-866:2:3608
-867:2:3619
-868:2:3620
-869:2:3621
-870:2:3619
-871:2:3620
-872:2:3621
-873:2:3632
-874:0:4811
-875:2:3049
-876:0:4811
-877:2:3641
-878:2:3642
-879:2:3646
-880:2:3647
-881:2:3655
-882:2:3656
-883:2:3660
-884:2:3661
-885:2:3669
-886:2:3674
-887:2:3678
-888:2:3679
-889:2:3687
-890:2:3688
-891:2:3692
-892:2:3693
-893:2:3687
-894:2:3688
-895:2:3692
-896:2:3693
-897:2:3701
-898:2:3706
-899:2:3707
-900:2:3718
-901:2:3719
-902:2:3720
-903:2:3731
-904:2:3736
-905:2:3737
-906:2:3748
-907:2:3749
-908:2:3750
-909:2:3748
-910:2:3749
-911:2:3750
-912:2:3761
-913:2:3768
-914:0:4811
-915:2:3049
-916:0:4811
-917:2:3772
-918:2:3773
-919:2:3774
-920:2:3786
-921:2:3787
-922:2:3791
-923:2:3792
-924:2:3800
-925:2:3805
-926:2:3809
-927:2:3810
-928:2:3818
-929:2:3819
-930:2:3823
-931:2:3824
-932:2:3818
-933:2:3819
-934:2:3823
-935:2:3824
-936:2:3832
-937:2:3837
-938:2:3838
-939:2:3849
-940:2:3850
-941:2:3851
-942:2:3862
-943:2:3867
-944:2:3868
-945:2:3879
-946:2:3880
-947:2:3881
-948:2:3879
-949:2:3880
-950:2:3881
-951:2:3892
-952:2:3902
-953:2:3903
-954:0:4811
-955:2:3049
-956:0:4811
-957:2:3909
-958:0:4811
-959:2:4534
-960:2:4535
-961:2:4539
-962:2:4543
-963:2:4544
-964:2:4548
-965:2:4556
-966:2:4557
-967:2:4561
-968:2:4565
-969:2:4566
-970:2:4561
-971:2:4565
-972:2:4566
-973:2:4570
-974:2:4577
-975:2:4584
-976:2:4585
-977:2:4592
-978:2:4597
-979:2:4604
-980:2:4605
-981:2:4604
-982:2:4605
-983:2:4612
-984:2:4616
-985:0:4811
-986:2:4621
-987:0:4811
-988:2:4622
-989:0:4811
-990:2:4623
-991:0:4811
-992:2:4624
-993:0:4811
-994:1:26
-995:0:4811
-996:2:4625
-997:0:4811
-998:1:30
-999:1:31
-1000:1:35
-1001:1:39
-1002:1:40
-1003:1:44
-1004:1:52
-1005:1:53
-1006:1:57
-1007:1:61
-1008:1:62
-1009:1:57
-1010:1:61
-1011:1:62
-1012:1:66
-1013:1:73
-1014:1:80
-1015:1:81
-1016:1:88
-1017:1:93
-1018:1:100
-1019:1:101
-1020:1:100
-1021:1:101
-1022:1:108
-1023:1:112
-1024:0:4811
-1025:2:4624
-1026:0:4811
-1027:1:117
-1028:0:4811
-1029:2:4625
-1030:0:4811
-1031:2:4626
-1032:0:4811
-1033:2:4631
-1034:0:4811
-1035:2:4632
-1036:0:4811
-1037:2:4640
-1038:2:4641
-1039:2:4645
-1040:2:4649
-1041:2:4650
-1042:2:4654
-1043:2:4662
-1044:2:4663
-1045:2:4667
-1046:2:4671
-1047:2:4672
-1048:2:4667
-1049:2:4671
-1050:2:4672
-1051:2:4676
-1052:2:4683
-1053:2:4690
-1054:2:4691
-1055:2:4698
-1056:2:4703
-1057:2:4710
-1058:2:4711
-1059:2:4710
-1060:2:4711
-1061:2:4718
-1062:2:4722
-1063:0:4811
-1064:2:3911
-1065:2:3921
-1066:0:4811
-1067:2:3049
-1068:0:4811
-1069:2:3912
-1070:2:3913
-1071:0:4811
-1072:2:3049
-1073:0:4811
-1074:2:3917
-1075:0:4811
-1076:2:3925
-1077:0:4811
-1078:2:3046
-1079:0:4811
-1080:2:3048
-1081:0:4811
-1082:2:3049
-1083:0:4811
-1084:2:3050
-1085:2:3051
-1086:2:3055
-1087:2:3056
-1088:2:3064
-1089:2:3065
-1090:2:3069
-1091:2:3070
-1092:2:3078
-1093:2:3083
-1094:2:3087
-1095:2:3088
-1096:2:3096
-1097:2:3097
-1098:2:3101
-1099:2:3102
-1100:2:3096
-1101:2:3097
-1102:2:3098
-1103:2:3110
-1104:2:3115
-1105:2:3116
-1106:2:3127
-1107:2:3128
-1108:2:3129
-1109:2:3140
-1110:2:3145
-1111:2:3146
-1112:2:3157
-1113:2:3158
-1114:2:3159
-1115:2:3157
-1116:2:3158
-1117:2:3159
-1118:2:3170
-1119:2:3178
-1120:0:4811
-1121:2:3049
-1122:0:4811
-1123:1:118
-1124:0:4811
-1125:1:120
-1126:0:4811
-1127:1:19
-1128:0:4811
-1129:1:126
-1130:1:127
-1131:1:131
-1132:1:132
-1133:1:140
-1134:1:141
-1135:1:145
-1136:1:146
-1137:1:154
-1138:1:159
-1139:1:163
-1140:1:164
-1141:1:172
-1142:1:173
-1143:1:177
-1144:1:178
-1145:1:172
-1146:1:173
-1147:1:177
-1148:1:178
-1149:1:186
-1150:1:191
-1151:1:192
-1152:1:203
-1153:1:204
-1154:1:205
-1155:1:216
-1156:1:221
-1157:1:222
-1158:1:233
-1159:1:234
-1160:1:235
-1161:1:233
-1162:1:234
-1163:1:235
-1164:1:246
-1165:0:4811
-1166:1:15
-1167:0:4811
-1168:1:16
-1169:0:4811
-1170:2:3182
-1171:2:3186
-1172:2:3187
-1173:2:3191
-1174:2:3195
-1175:2:3196
-1176:2:3200
-1177:2:3208
-1178:2:3209
-1179:2:3213
-1180:2:3217
-1181:2:3218
-1182:2:3213
-1183:2:3214
-1184:2:3222
-1185:0:4811
-1186:2:3049
-1187:0:4811
-1188:2:3230
-1189:2:3231
-1190:2:3232
-1191:0:4811
-1192:2:3049
-1193:0:4811
-1194:2:3237
-1195:0:4811
-1196:2:3940
-1197:2:3941
-1198:2:3945
-1199:2:3949
-1200:2:3950
-1201:2:3954
-1202:2:3959
-1203:2:3967
-1204:2:3971
-1205:2:3972
-1206:2:3967
-1207:2:3971
-1208:2:3972
-1209:2:3976
-1210:2:3983
-1211:2:3990
-1212:2:3991
-1213:2:3998
-1214:2:4003
-1215:2:4010
-1216:2:4011
-1217:2:4010
-1218:2:4011
-1219:2:4018
-1220:2:4022
-1221:0:4811
-1222:2:4027
-1223:0:4811
-1224:2:4028
-1225:0:4811
-1226:2:4029
-1227:0:4811
-1228:2:4030
-1229:0:4811
-1230:1:17
-1231:0:4811
-1232:2:4031
-1233:0:4811
-1234:1:118
-1235:0:4811
-1236:1:120
-1237:0:4811
-1238:2:4030
-1239:0:4811
-1240:1:19
-1241:0:4811
-1242:2:4031
-1243:0:4811
-1244:1:255
-1245:1:256
-1246:0:4811
-1247:1:15
-1248:0:4811
-1249:1:16
-1250:0:4811
-1251:2:4030
-1252:0:4811
-1253:1:17
-1254:0:4811
-1255:2:4031
-1256:0:4811
-1257:1:118
-1258:0:4811
-1259:1:120
-1260:0:4811
-1261:2:4030
-1262:0:4811
-1263:1:19
-1264:0:4811
-1265:2:4031
-1266:0:4811
-1267:1:262
-1268:1:263
-1269:1:267
-1270:1:268
-1271:1:276
-1272:1:277
-1273:1:281
-1274:1:282
-1275:1:290
-1276:1:295
-1277:1:299
-1278:1:300
-1279:1:308
-1280:1:309
-1281:1:313
-1282:1:314
-1283:1:308
-1284:1:309
-1285:1:313
-1286:1:314
-1287:1:322
-1288:1:327
-1289:1:328
-1290:1:339
-1291:1:340
-1292:1:341
-1293:1:352
-1294:1:357
-1295:1:358
-1296:1:369
-1297:1:370
-1298:1:371
-1299:1:369
-1300:1:377
-1301:1:378
-1302:1:382
-1303:0:4811
-1304:1:15
-1305:0:4811
-1306:1:16
-1307:0:4811
-1308:2:4030
-1309:0:4811
-1310:1:17
-1311:0:4811
-1312:2:4031
-1313:0:4811
-1314:1:118
-1315:0:4811
-1316:1:120
-1317:0:4811
-1318:2:4030
-1319:0:4811
-1320:1:19
-1321:0:4811
-1322:2:4031
-1323:0:4811
-1324:1:391
-1325:1:392
-1326:1:396
-1327:1:397
-1328:1:405
-1329:1:406
-1330:1:410
-1331:1:411
-1332:1:419
-1333:1:424
-1334:1:428
-1335:1:429
-1336:1:437
-1337:1:438
-1338:1:442
-1339:1:443
-1340:1:437
-1341:1:438
-1342:1:442
-1343:1:443
-1344:1:451
-1345:1:456
-1346:1:457
-1347:1:468
-1348:1:469
-1349:1:470
-1350:1:481
-1351:1:486
-1352:1:487
-1353:1:498
-1354:1:499
-1355:1:500
-1356:1:498
-1357:1:506
-1358:1:507
-1359:1:511
-1360:1:518
-1361:0:4811
-1362:1:15
-1363:0:4811
-1364:1:16
-1365:0:4811
-1366:2:4030
-1367:0:4811
-1368:1:17
-1369:0:4811
-1370:2:4031
-1371:0:4811
-1372:1:118
-1373:0:4811
-1374:1:120
-1375:0:4811
-1376:2:4030
-1377:0:4811
-1378:1:19
-1379:0:4811
-1380:2:4031
-1381:0:4811
-1382:1:656
-1383:1:657
-1384:1:661
-1385:1:662
-1386:1:670
-1387:1:671
-1388:1:672
-1389:1:684
-1390:1:689
-1391:1:693
-1392:1:694
-1393:1:702
-1394:1:703
-1395:1:707
-1396:1:708
-1397:1:702
-1398:1:703
-1399:1:707
-1400:1:708
-1401:1:716
-1402:1:721
-1403:1:722
-1404:1:733
-1405:1:734
-1406:1:735
-1407:1:746
-1408:1:751
-1409:1:752
-1410:1:763
-1411:1:764
-1412:1:765
-1413:1:763
-1414:1:771
-1415:1:772
-1416:1:776
-1417:0:4811
-1418:1:15
-1419:0:4811
-1420:1:16
-1421:0:4811
-1422:2:4030
-1423:0:4811
-1424:1:17
-1425:0:4811
-1426:2:4031
-1427:0:4811
-1428:1:118
-1429:0:4811
-1430:1:120
-1431:0:4811
-1432:2:4030
-1433:0:4811
-1434:1:19
-1435:0:4811
-1436:2:4031
-1437:0:4811
-1438:1:785
-1439:1:788
-1440:1:789
-1441:0:4811
-1442:1:15
-1443:0:4811
-1444:1:16
-1445:0:4811
-1446:2:4030
-1447:0:4811
-1448:1:17
-1449:0:4811
-1450:2:4031
-1451:0:4811
-1452:1:118
-1453:0:4811
-1454:1:120
-1455:0:4811
-1456:2:4030
-1457:0:4811
-1458:1:19
-1459:0:4811
-1460:2:4031
-1461:0:4811
-1462:1:1052
-1463:1:1053
-1464:1:1057
-1465:1:1058
-1466:1:1066
-1467:1:1067
-1468:1:1071
-1469:1:1072
-1470:1:1080
-1471:1:1085
-1472:1:1089
-1473:1:1090
-1474:1:1098
-1475:1:1099
-1476:1:1103
-1477:1:1104
-1478:1:1098
-1479:1:1099
-1480:1:1103
-1481:1:1104
-1482:1:1112
-1483:1:1117
-1484:1:1118
-1485:1:1129
-1486:1:1130
-1487:1:1131
-1488:1:1142
-1489:1:1147
-1490:1:1148
-1491:1:1159
-1492:1:1160
-1493:1:1161
-1494:1:1159
-1495:1:1167
-1496:1:1168
-1497:1:1172
-1498:1:1179
-1499:1:1183
-1500:0:4811
-1501:1:15
-1502:0:4811
-1503:1:16
-1504:0:4811
-1505:2:4030
-1506:0:4811
-1507:1:17
-1508:0:4811
-1509:2:4031
-1510:0:4811
-1511:1:118
-1512:0:4811
-1513:1:120
-1514:0:4811
-1515:2:4030
-1516:0:4811
-1517:1:19
-1518:0:4811
-1519:2:4031
-1520:0:4811
-1521:1:1184
-1522:1:1185
-1523:1:1189
-1524:1:1190
-1525:1:1198
-1526:1:1199
-1527:1:1200
-1528:1:1212
-1529:1:1217
-1530:1:1221
-1531:1:1222
-1532:1:1230
-1533:1:1231
-1534:1:1235
-1535:1:1236
-1536:1:1230
-1537:1:1231
-1538:1:1235
-1539:1:1236
-1540:1:1244
-1541:1:1249
-1542:1:1250
-1543:1:1261
-1544:1:1262
-1545:1:1263
-1546:1:1274
-1547:1:1279
-1548:1:1280
-1549:1:1291
-1550:1:1292
-1551:1:1293
-1552:1:1291
-1553:1:1299
-1554:1:1300
-1555:1:1304
-1556:0:4811
-1557:1:15
-1558:0:4811
-1559:1:16
-1560:0:4811
-1561:2:4030
-1562:0:4811
-1563:1:17
-1564:0:4811
-1565:2:4031
-1566:0:4811
-1567:1:118
-1568:0:4811
-1569:1:120
-1570:0:4811
-1571:2:4030
-1572:0:4811
-1573:1:19
-1574:0:4811
-1575:2:4031
-1576:0:4811
-1577:1:1313
-1578:0:4811
-1579:2:4030
-1580:0:4811
-1581:1:2777
-1582:1:2781
-1583:1:2782
-1584:1:2790
-1585:1:2791
-1586:1:2795
-1587:1:2796
-1588:1:2804
-1589:1:2809
-1590:1:2813
-1591:1:2814
-1592:1:2822
-1593:1:2823
-1594:1:2827
-1595:1:2828
-1596:1:2822
-1597:1:2823
-1598:1:2827
-1599:1:2828
-1600:1:2836
-1601:1:2841
-1602:1:2842
-1603:1:2853
-1604:1:2854
-1605:1:2855
-1606:1:2866
-1607:1:2871
-1608:1:2872
-1609:1:2883
-1610:1:2884
-1611:1:2885
-1612:1:2883
-1613:1:2891
-1614:1:2892
-1615:1:2896
-1616:1:2900
-1617:0:4811
-1618:2:4031
-1619:0:4811
-1620:1:1315
-1621:1:1316
-1622:0:4809
-1623:1:15
-1624:0:4815
-1625:1:120