Verification run #1, ipi and no-ipi results

[urcu.git] / formal-model / results / urcu-controldataflow-no-ipi / result-ipi-urcu_free / urcu_free_no_wmb.spin.input.trail

diff --git a/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_wmb.spin.input.trail b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_wmb.spin.input.trail
new file mode 100644 (file)
index 0000000..befcb5f
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1467 @@
+-2:3:-2
+-4:-4:-4
+1:0:4645
+2:3:4565
+3:3:4568
+4:3:4568
+5:3:4571
+6:3:4579
+7:3:4579
+8:3:4582
+9:3:4588
+10:3:4592
+11:3:4592
+12:3:4595
+13:3:4605
+14:3:4613
+15:3:4613
+16:3:4616
+17:3:4622
+18:3:4626
+19:3:4626
+20:3:4629
+21:3:4635
+22:3:4639
+23:3:4640
+24:0:4645
+25:3:4642
+26:0:4645
+27:2:2872
+28:0:4645
+29:2:2878
+30:0:4645
+31:2:2879
+32:0:4645
+33:2:2881
+34:0:4645
+35:2:2882
+36:0:4645
+37:2:2883
+38:0:4645
+39:2:2884
+40:2:2885
+41:2:2889
+42:2:2890
+43:2:2898
+44:2:2899
+45:2:2903
+46:2:2904
+47:2:2912
+48:2:2917
+49:2:2921
+50:2:2922
+51:2:2930
+52:2:2931
+53:2:2935
+54:2:2936
+55:2:2930
+56:2:2931
+57:2:2935
+58:2:2936
+59:2:2944
+60:2:2949
+61:2:2950
+62:2:2961
+63:2:2962
+64:2:2963
+65:2:2974
+66:2:2979
+67:2:2980
+68:2:2991
+69:2:2992
+70:2:2993
+71:2:2991
+72:2:2992
+73:2:2993
+74:2:3004
+75:2:3012
+76:0:4645
+77:2:2883
+78:0:4645
+79:2:3064
+80:2:3065
+81:2:3066
+82:0:4645
+83:2:2883
+84:0:4645
+85:2:3071
+86:0:4645
+87:2:3774
+88:2:3775
+89:2:3779
+90:2:3783
+91:2:3784
+92:2:3788
+93:2:3793
+94:2:3801
+95:2:3805
+96:2:3806
+97:2:3801
+98:2:3802
+99:2:3810
+100:2:3817
+101:2:3824
+102:2:3825
+103:2:3832
+104:2:3837
+105:2:3844
+106:2:3845
+107:2:3844
+108:2:3845
+109:2:3852
+110:2:3856
+111:0:4645
+112:2:3861
+113:0:4645
+114:2:3862
+115:0:4645
+116:2:3863
+117:0:4645
+118:2:3864
+119:0:4645
+120:1:2
+121:0:4645
+122:2:3865
+123:0:4645
+124:1:8
+125:0:4645
+126:1:9
+127:0:4645
+128:2:3864
+129:0:4645
+130:1:10
+131:0:4645
+132:2:3865
+133:0:4645
+134:1:11
+135:0:4645
+136:2:3864
+137:0:4645
+138:1:12
+139:0:4645
+140:2:3865
+141:0:4645
+142:1:13
+143:0:4645
+144:2:3864
+145:0:4645
+146:1:14
+147:0:4645
+148:2:3865
+149:0:4645
+150:1:15
+151:0:4645
+152:1:16
+153:0:4645
+154:2:3864
+155:0:4645
+156:1:17
+157:0:4645
+158:2:3865
+159:0:4645
+160:1:28
+161:0:4645
+162:2:3864
+163:0:4645
+164:1:32
+165:1:33
+166:1:37
+167:1:41
+168:1:42
+169:1:46
+170:1:54
+171:1:55
+172:1:59
+173:1:63
+174:1:64
+175:1:59
+176:1:63
+177:1:64
+178:1:68
+179:1:75
+180:1:82
+181:1:83
+182:1:90
+183:1:95
+184:1:102
+185:1:103
+186:1:102
+187:1:103
+188:1:110
+189:1:114
+190:0:4645
+191:2:3865
+192:0:4645
+193:1:119
+194:0:4645
+195:2:3866
+196:0:4645
+197:2:3871
+198:0:4645
+199:2:3872
+200:0:4645
+201:2:3880
+202:2:3881
+203:2:3885
+204:2:3889
+205:2:3890
+206:2:3894
+207:2:3902
+208:2:3903
+209:2:3907
+210:2:3911
+211:2:3912
+212:2:3907
+213:2:3911
+214:2:3912
+215:2:3916
+216:2:3923
+217:2:3930
+218:2:3931
+219:2:3938
+220:2:3943
+221:2:3950
+222:2:3951
+223:2:3950
+224:2:3951
+225:2:3958
+226:2:3962
+227:0:4645
+228:2:3073
+229:2:3755
+230:0:4645
+231:2:2883
+232:0:4645
+233:2:3074
+234:0:4645
+235:2:2883
+236:0:4645
+237:2:3077
+238:2:3078
+239:2:3082
+240:2:3083
+241:2:3091
+242:2:3092
+243:2:3096
+244:2:3097
+245:2:3105
+246:2:3110
+247:2:3114
+248:2:3115
+249:2:3123
+250:2:3124
+251:2:3128
+252:2:3129
+253:2:3123
+254:2:3124
+255:2:3128
+256:2:3129
+257:2:3137
+258:2:3142
+259:2:3143
+260:2:3154
+261:2:3155
+262:2:3156
+263:2:3167
+264:2:3172
+265:2:3173
+266:2:3184
+267:2:3185
+268:2:3186
+269:2:3184
+270:2:3185
+271:2:3186
+272:2:3197
+273:2:3204
+274:0:4645
+275:2:2883
+276:0:4645
+277:2:3208
+278:2:3209
+279:2:3210
+280:2:3222
+281:2:3223
+282:2:3227
+283:2:3228
+284:2:3236
+285:2:3241
+286:2:3245
+287:2:3246
+288:2:3254
+289:2:3255
+290:2:3259
+291:2:3260
+292:2:3254
+293:2:3255
+294:2:3259
+295:2:3260
+296:2:3268
+297:2:3273
+298:2:3274
+299:2:3285
+300:2:3286
+301:2:3287
+302:2:3298
+303:2:3303
+304:2:3304
+305:2:3315
+306:2:3316
+307:2:3317
+308:2:3315
+309:2:3316
+310:2:3317
+311:2:3328
+312:2:3339
+313:2:3340
+314:0:4645
+315:2:2883
+316:0:4645
+317:2:3346
+318:2:3347
+319:2:3351
+320:2:3352
+321:2:3360
+322:2:3361
+323:2:3365
+324:2:3366
+325:2:3374
+326:2:3379
+327:2:3383
+328:2:3384
+329:2:3392
+330:2:3393
+331:2:3397
+332:2:3398
+333:2:3392
+334:2:3393
+335:2:3397
+336:2:3398
+337:2:3406
+338:2:3411
+339:2:3412
+340:2:3423
+341:2:3424
+342:2:3425
+343:2:3436
+344:2:3441
+345:2:3442
+346:2:3453
+347:2:3454
+348:2:3455
+349:2:3453
+350:2:3454
+351:2:3455
+352:2:3466
+353:0:4645
+354:2:2883
+355:0:4645
+356:2:3475
+357:2:3476
+358:2:3480
+359:2:3481
+360:2:3489
+361:2:3490
+362:2:3494
+363:2:3495
+364:2:3503
+365:2:3508
+366:2:3512
+367:2:3513
+368:2:3521
+369:2:3522
+370:2:3526
+371:2:3527
+372:2:3521
+373:2:3522
+374:2:3526
+375:2:3527
+376:2:3535
+377:2:3540
+378:2:3541
+379:2:3552
+380:2:3553
+381:2:3554
+382:2:3565
+383:2:3570
+384:2:3571
+385:2:3582
+386:2:3583
+387:2:3584
+388:2:3582
+389:2:3583
+390:2:3584
+391:2:3595
+392:2:3602
+393:0:4645
+394:2:2883
+395:0:4645
+396:2:3606
+397:2:3607
+398:2:3608
+399:2:3620
+400:2:3621
+401:2:3625
+402:2:3626
+403:2:3634
+404:2:3639
+405:2:3643
+406:2:3644
+407:2:3652
+408:2:3653
+409:2:3657
+410:2:3658
+411:2:3652
+412:2:3653
+413:2:3657
+414:2:3658
+415:2:3666
+416:2:3671
+417:2:3672
+418:2:3683
+419:2:3684
+420:2:3685
+421:2:3696
+422:2:3701
+423:2:3702
+424:2:3713
+425:2:3714
+426:2:3715
+427:2:3713
+428:2:3714
+429:2:3715
+430:2:3726
+431:2:3736
+432:2:3737
+433:0:4645
+434:2:2883
+435:0:4645
+436:2:3743
+437:0:4645
+438:2:4368
+439:2:4369
+440:2:4373
+441:2:4377
+442:2:4378
+443:2:4382
+444:2:4390
+445:2:4391
+446:2:4395
+447:2:4399
+448:2:4400
+449:2:4395
+450:2:4399
+451:2:4400
+452:2:4404
+453:2:4411
+454:2:4418
+455:2:4419
+456:2:4426
+457:2:4431
+458:2:4438
+459:2:4439
+460:2:4438
+461:2:4439
+462:2:4446
+463:2:4450
+464:0:4645
+465:2:4455
+466:0:4645
+467:2:4456
+468:0:4645
+469:2:4457
+470:0:4645
+471:2:4458
+472:0:4645
+473:1:28
+474:0:4645
+475:2:4459
+476:0:4645
+477:1:32
+478:1:33
+479:1:37
+480:1:41
+481:1:42
+482:1:46
+483:1:54
+484:1:55
+485:1:59
+486:1:63
+487:1:64
+488:1:59
+489:1:63
+490:1:64
+491:1:68
+492:1:75
+493:1:82
+494:1:83
+495:1:90
+496:1:95
+497:1:102
+498:1:103
+499:1:102
+500:1:103
+501:1:110
+502:1:114
+503:0:4645
+504:2:4458
+505:0:4645
+506:1:119
+507:0:4645
+508:2:4459
+509:0:4645
+510:2:4460
+511:0:4645
+512:2:4465
+513:0:4645
+514:2:4466
+515:0:4645
+516:2:4474
+517:2:4475
+518:2:4479
+519:2:4483
+520:2:4484
+521:2:4488
+522:2:4496
+523:2:4497
+524:2:4501
+525:2:4505
+526:2:4506
+527:2:4501
+528:2:4505
+529:2:4506
+530:2:4510
+531:2:4517
+532:2:4524
+533:2:4525
+534:2:4532
+535:2:4537
+536:2:4544
+537:2:4545
+538:2:4544
+539:2:4545
+540:2:4552
+541:2:4556
+542:0:4645
+543:2:3745
+544:2:3755
+545:0:4645
+546:2:2883
+547:0:4645
+548:2:3746
+549:2:3747
+550:0:4645
+551:2:2883
+552:0:4645
+553:2:3751
+554:0:4645
+555:2:3759
+556:0:4645
+557:2:2879
+558:0:4645
+559:2:2881
+560:0:4645
+561:2:2882
+562:0:4645
+563:2:2883
+564:0:4645
+565:2:3064
+566:2:3065
+567:2:3066
+568:0:4645
+569:2:2883
+570:0:4645
+571:2:2884
+572:2:2885
+573:2:2889
+574:2:2890
+575:2:2898
+576:2:2899
+577:2:2903
+578:2:2904
+579:2:2912
+580:2:2917
+581:2:2918
+582:2:2930
+583:2:2931
+584:2:2932
+585:2:2930
+586:2:2931
+587:2:2935
+588:2:2936
+589:2:2944
+590:2:2949
+591:2:2950
+592:2:2961
+593:2:2962
+594:2:2963
+595:2:2974
+596:2:2979
+597:2:2980
+598:2:2991
+599:2:2992
+600:2:2993
+601:2:2991
+602:2:2992
+603:2:2993
+604:2:3004
+605:2:3012
+606:0:4645
+607:2:2883
+608:0:4645
+609:2:3071
+610:0:4645
+611:2:3774
+612:2:3775
+613:2:3779
+614:2:3783
+615:2:3784
+616:2:3788
+617:2:3796
+618:2:3797
+619:2:3801
+620:2:3802
+621:2:3801
+622:2:3805
+623:2:3806
+624:2:3810
+625:2:3817
+626:2:3824
+627:2:3825
+628:2:3832
+629:2:3837
+630:2:3844
+631:2:3845
+632:2:3844
+633:2:3845
+634:2:3852
+635:2:3856
+636:0:4645
+637:2:3861
+638:0:4645
+639:2:3862
+640:0:4645
+641:2:3863
+642:0:4645
+643:2:3864
+644:0:4645
+645:1:28
+646:0:4645
+647:2:3865
+648:0:4645
+649:1:32
+650:1:33
+651:1:37
+652:1:41
+653:1:42
+654:1:46
+655:1:54
+656:1:55
+657:1:59
+658:1:63
+659:1:64
+660:1:59
+661:1:63
+662:1:64
+663:1:68
+664:1:75
+665:1:82
+666:1:83
+667:1:90
+668:1:95
+669:1:102
+670:1:103
+671:1:102
+672:1:103
+673:1:110
+674:1:114
+675:0:4645
+676:2:3864
+677:0:4645
+678:1:119
+679:0:4645
+680:2:3865
+681:0:4645
+682:2:3866
+683:0:4645
+684:2:3871
+685:0:4645
+686:2:3872
+687:0:4645
+688:2:3880
+689:2:3881
+690:2:3885
+691:2:3889
+692:2:3890
+693:2:3894
+694:2:3902
+695:2:3903
+696:2:3907
+697:2:3911
+698:2:3912
+699:2:3907
+700:2:3911
+701:2:3912
+702:2:3916
+703:2:3923
+704:2:3930
+705:2:3931
+706:2:3938
+707:2:3943
+708:2:3950
+709:2:3951
+710:2:3950
+711:2:3951
+712:2:3958
+713:2:3962
+714:0:4645
+715:2:3073
+716:2:3755
+717:0:4645
+718:2:2883
+719:0:4645
+720:2:3074
+721:0:4645
+722:2:2883
+723:0:4645
+724:2:3077
+725:2:3078
+726:2:3082
+727:2:3083
+728:2:3091
+729:2:3092
+730:2:3096
+731:2:3097
+732:2:3105
+733:2:3110
+734:2:3114
+735:2:3115
+736:2:3123
+737:2:3124
+738:2:3128
+739:2:3129
+740:2:3123
+741:2:3124
+742:2:3128
+743:2:3129
+744:2:3137
+745:2:3142
+746:2:3143
+747:2:3154
+748:2:3155
+749:2:3156
+750:2:3167
+751:2:3172
+752:2:3173
+753:2:3184
+754:2:3185
+755:2:3186
+756:2:3184
+757:2:3185
+758:2:3186
+759:2:3197
+760:2:3204
+761:0:4645
+762:2:2883
+763:0:4645
+764:2:3208
+765:2:3209
+766:2:3210
+767:2:3222
+768:2:3223
+769:2:3227
+770:2:3228
+771:2:3236
+772:2:3241
+773:2:3245
+774:2:3246
+775:2:3254
+776:2:3255
+777:2:3259
+778:2:3260
+779:2:3254
+780:2:3255
+781:2:3259
+782:2:3260
+783:2:3268
+784:2:3273
+785:2:3274
+786:2:3285
+787:2:3286
+788:2:3287
+789:2:3298
+790:2:3303
+791:2:3304
+792:2:3315
+793:2:3316
+794:2:3317
+795:2:3315
+796:2:3316
+797:2:3317
+798:2:3328
+799:2:3339
+800:2:3340
+801:0:4645
+802:2:2883
+803:0:4645
+804:2:3346
+805:2:3347
+806:2:3351
+807:2:3352
+808:2:3360
+809:2:3361
+810:2:3365
+811:2:3366
+812:2:3374
+813:2:3379
+814:2:3383
+815:2:3384
+816:2:3392
+817:2:3393
+818:2:3397
+819:2:3398
+820:2:3392
+821:2:3393
+822:2:3397
+823:2:3398
+824:2:3406
+825:2:3411
+826:2:3412
+827:2:3423
+828:2:3424
+829:2:3425
+830:2:3436
+831:2:3441
+832:2:3442
+833:2:3453
+834:2:3454
+835:2:3455
+836:2:3453
+837:2:3454
+838:2:3455
+839:2:3466
+840:0:4645
+841:2:2883
+842:0:4645
+843:2:3475
+844:2:3476
+845:2:3480
+846:2:3481
+847:2:3489
+848:2:3490
+849:2:3494
+850:2:3495
+851:2:3503
+852:2:3508
+853:2:3512
+854:2:3513
+855:2:3521
+856:2:3522
+857:2:3526
+858:2:3527
+859:2:3521
+860:2:3522
+861:2:3526
+862:2:3527
+863:2:3535
+864:2:3540
+865:2:3541
+866:2:3552
+867:2:3553
+868:2:3554
+869:2:3565
+870:2:3570
+871:2:3571
+872:2:3582
+873:2:3583
+874:2:3584
+875:2:3582
+876:2:3583
+877:2:3584
+878:2:3595
+879:2:3602
+880:0:4645
+881:2:2883
+882:0:4645
+883:2:3606
+884:2:3607
+885:2:3608
+886:2:3620
+887:2:3621
+888:2:3625
+889:2:3626
+890:2:3634
+891:2:3639
+892:2:3643
+893:2:3644
+894:2:3652
+895:2:3653
+896:2:3657
+897:2:3658
+898:2:3652
+899:2:3653
+900:2:3657
+901:2:3658
+902:2:3666
+903:2:3671
+904:2:3672
+905:2:3683
+906:2:3684
+907:2:3685
+908:2:3696
+909:2:3701
+910:2:3702
+911:2:3713
+912:2:3714
+913:2:3715
+914:2:3713
+915:2:3714
+916:2:3715
+917:2:3726
+918:2:3736
+919:2:3737
+920:0:4645
+921:2:2883
+922:0:4645
+923:2:3743
+924:0:4645
+925:2:4368
+926:2:4369
+927:2:4373
+928:2:4377
+929:2:4378
+930:2:4382
+931:2:4390
+932:2:4391
+933:2:4395
+934:2:4399
+935:2:4400
+936:2:4395
+937:2:4399
+938:2:4400
+939:2:4404
+940:2:4411
+941:2:4418
+942:2:4419
+943:2:4426
+944:2:4431
+945:2:4438
+946:2:4439
+947:2:4438
+948:2:4439
+949:2:4446
+950:2:4450
+951:0:4645
+952:2:4455
+953:0:4645
+954:2:4456
+955:0:4645
+956:2:4457
+957:0:4645
+958:2:4458
+959:0:4645
+960:1:28
+961:0:4645
+962:2:4459
+963:0:4645
+964:1:32
+965:1:33
+966:1:37
+967:1:41
+968:1:42
+969:1:46
+970:1:54
+971:1:55
+972:1:59
+973:1:63
+974:1:64
+975:1:59
+976:1:63
+977:1:64
+978:1:68
+979:1:75
+980:1:82
+981:1:83
+982:1:90
+983:1:95
+984:1:102
+985:1:103
+986:1:102
+987:1:103
+988:1:110
+989:1:114
+990:0:4645
+991:2:4458
+992:0:4645
+993:1:119
+994:0:4645
+995:2:4459
+996:0:4645
+997:2:4460
+998:0:4645
+999:2:4465
+1000:0:4645
+1001:2:4466
+1002:0:4645
+1003:2:4474
+1004:2:4475
+1005:2:4479
+1006:2:4483
+1007:2:4484
+1008:2:4488
+1009:2:4496
+1010:2:4497
+1011:2:4501
+1012:2:4505
+1013:2:4506
+1014:2:4501
+1015:2:4505
+1016:2:4506
+1017:2:4510
+1018:2:4517
+1019:2:4524
+1020:2:4525
+1021:2:4532
+1022:2:4537
+1023:2:4544
+1024:2:4545
+1025:2:4544
+1026:2:4545
+1027:2:4552
+1028:2:4556
+1029:0:4645
+1030:2:3745
+1031:2:3755
+1032:0:4645
+1033:2:2883
+1034:0:4645
+1035:2:3746
+1036:2:3747
+1037:0:4645
+1038:2:2883
+1039:0:4645
+1040:2:3751
+1041:0:4645
+1042:2:3759
+1043:0:4645
+1044:2:2879
+1045:0:4645
+1046:2:2881
+1047:0:4645
+1048:2:2882
+1049:0:4645
+1050:2:2883
+1051:0:4645
+1052:2:2884
+1053:2:2885
+1054:2:2889
+1055:2:2890
+1056:2:2898
+1057:2:2899
+1058:2:2903
+1059:2:2904
+1060:2:2912
+1061:2:2917
+1062:2:2921
+1063:2:2922
+1064:2:2930
+1065:2:2931
+1066:2:2935
+1067:2:2936
+1068:2:2930
+1069:2:2931
+1070:2:2932
+1071:2:2944
+1072:2:2949
+1073:2:2950
+1074:2:2961
+1075:2:2962
+1076:2:2963
+1077:2:2974
+1078:2:2979
+1079:2:2980
+1080:2:2991
+1081:2:2992
+1082:2:2993
+1083:2:2991
+1084:2:2992
+1085:2:2993
+1086:2:3004
+1087:2:3012
+1088:0:4645
+1089:2:2883
+1090:0:4645
+1091:2:3064
+1092:2:3065
+1093:2:3066
+1094:0:4645
+1095:2:2883
+1096:0:4645
+1097:2:3071
+1098:0:4645
+1099:1:120
+1100:0:4645
+1101:1:19
+1102:0:4645
+1103:1:127
+1104:1:128
+1105:1:132
+1106:1:133
+1107:1:141
+1108:1:142
+1109:1:146
+1110:1:147
+1111:1:155
+1112:1:160
+1113:1:164
+1114:1:165
+1115:1:173
+1116:1:174
+1117:1:178
+1118:1:179
+1119:1:173
+1120:1:174
+1121:1:178
+1122:1:179
+1123:1:187
+1124:1:192
+1125:1:193
+1126:1:204
+1127:1:205
+1128:1:206
+1129:1:217
+1130:1:222
+1131:1:223
+1132:1:234
+1133:1:235
+1134:1:236
+1135:1:234
+1136:1:235
+1137:1:236
+1138:1:247
+1139:0:4645
+1140:1:15
+1141:0:4645
+1142:1:16
+1143:0:4645
+1144:1:17
+1145:0:4645
+1146:1:120
+1147:0:4645
+1148:1:19
+1149:0:4645
+1150:1:256
+1151:1:257
+1152:0:4645
+1153:1:15
+1154:0:4645
+1155:1:16
+1156:0:4645
+1157:1:17
+1158:0:4645
+1159:1:120
+1160:0:4645
+1161:1:19
+1162:0:4645
+1163:1:263
+1164:1:264
+1165:1:268
+1166:1:269
+1167:1:277
+1168:1:278
+1169:1:282
+1170:1:283
+1171:1:291
+1172:1:296
+1173:1:300
+1174:1:301
+1175:1:309
+1176:1:310
+1177:1:314
+1178:1:315
+1179:1:309
+1180:1:310
+1181:1:314
+1182:1:315
+1183:1:323
+1184:1:328
+1185:1:329
+1186:1:340
+1187:1:341
+1188:1:342
+1189:1:353
+1190:1:358
+1191:1:359
+1192:1:370
+1193:1:371
+1194:1:372
+1195:1:370
+1196:1:371
+1197:1:372
+1198:1:383
+1199:0:4645
+1200:1:15
+1201:0:4645
+1202:1:16
+1203:0:4645
+1204:1:17
+1205:0:4645
+1206:1:120
+1207:0:4645
+1208:1:19
+1209:0:4645
+1210:1:392
+1211:1:393
+1212:1:397
+1213:1:398
+1214:1:406
+1215:1:407
+1216:1:411
+1217:1:412
+1218:1:420
+1219:1:425
+1220:1:429
+1221:1:430
+1222:1:438
+1223:1:439
+1224:1:443
+1225:1:444
+1226:1:438
+1227:1:439
+1228:1:443
+1229:1:444
+1230:1:452
+1231:1:457
+1232:1:458
+1233:1:469
+1234:1:470
+1235:1:471
+1236:1:482
+1237:1:487
+1238:1:488
+1239:1:499
+1240:1:500
+1241:1:501
+1242:1:499
+1243:1:500
+1244:1:501
+1245:1:512
+1246:1:519
+1247:0:4645
+1248:1:15
+1249:0:4645
+1250:1:16
+1251:0:4645
+1252:1:17
+1253:0:4645
+1254:1:120
+1255:0:4645
+1256:1:19
+1257:0:4645
+1258:1:657
+1259:1:658
+1260:1:662
+1261:1:663
+1262:1:671
+1263:1:672
+1264:1:673
+1265:1:685
+1266:1:690
+1267:1:694
+1268:1:695
+1269:1:703
+1270:1:704
+1271:1:708
+1272:1:709
+1273:1:703
+1274:1:704
+1275:1:708
+1276:1:709
+1277:1:717
+1278:1:722
+1279:1:723
+1280:1:734
+1281:1:735
+1282:1:736
+1283:1:747
+1284:1:752
+1285:1:753
+1286:1:764
+1287:1:765
+1288:1:766
+1289:1:764
+1290:1:765
+1291:1:766
+1292:1:777
+1293:0:4645
+1294:1:15
+1295:0:4645
+1296:1:16
+1297:0:4645
+1298:1:17
+1299:0:4645
+1300:1:120
+1301:0:4645
+1302:1:19
+1303:0:4645
+1304:1:786
+1305:1:789
+1306:1:790
+1307:0:4645
+1308:1:15
+1309:0:4645
+1310:1:16
+1311:0:4645
+1312:1:17
+1313:0:4645
+1314:1:120
+1315:0:4645
+1316:1:19
+1317:0:4645
+1318:1:1053
+1319:1:1054
+1320:1:1058
+1321:1:1059
+1322:1:1067
+1323:1:1068
+1324:1:1072
+1325:1:1073
+1326:1:1081
+1327:1:1086
+1328:1:1090
+1329:1:1091
+1330:1:1099
+1331:1:1100
+1332:1:1104
+1333:1:1105
+1334:1:1099
+1335:1:1100
+1336:1:1104
+1337:1:1105
+1338:1:1113
+1339:1:1118
+1340:1:1119
+1341:1:1130
+1342:1:1131
+1343:1:1132
+1344:1:1143
+1345:1:1148
+1346:1:1149
+1347:1:1160
+1348:1:1161
+1349:1:1162
+1350:1:1160
+1351:1:1161
+1352:1:1162
+1353:1:1173
+1354:1:1180
+1355:1:1184
+1356:0:4645
+1357:1:15
+1358:0:4645
+1359:1:16
+1360:0:4645
+1361:1:17
+1362:0:4645
+1363:1:120
+1364:0:4645
+1365:1:19
+1366:0:4645
+1367:1:1185
+1368:1:1186
+1369:1:1190
+1370:1:1191
+1371:1:1199
+1372:1:1200
+1373:1:1201
+1374:1:1213
+1375:1:1218
+1376:1:1222
+1377:1:1223
+1378:1:1231
+1379:1:1232
+1380:1:1236
+1381:1:1237
+1382:1:1231
+1383:1:1232
+1384:1:1236
+1385:1:1237
+1386:1:1245
+1387:1:1250
+1388:1:1251
+1389:1:1262
+1390:1:1263
+1391:1:1264
+1392:1:1275
+1393:1:1280
+1394:1:1281
+1395:1:1292
+1396:1:1293
+1397:1:1294
+1398:1:1292
+1399:1:1293
+1400:1:1294
+1401:1:1305
+1402:0:4645
+1403:1:15
+1404:0:4645
+1405:1:16
+1406:0:4645
+1407:1:17
+1408:0:4645
+1409:1:120
+1410:0:4645
+1411:1:19
+1412:0:4645
+1413:1:1314
+1414:0:4645
+1415:1:2778
+1416:1:2785
+1417:1:2786
+1418:1:2793
+1419:1:2798
+1420:1:2805
+1421:1:2806
+1422:1:2805
+1423:1:2806
+1424:1:2813
+1425:1:2817
+1426:0:4645
+1427:2:3774
+1428:2:3775
+1429:2:3779
+1430:2:3783
+1431:2:3784
+1432:2:3788
+1433:2:3793
+1434:2:3801
+1435:2:3805
+1436:2:3806
+1437:2:3801
+1438:2:3802
+1439:2:3810
+1440:2:3817
+1441:2:3824
+1442:2:3825
+1443:2:3832
+1444:2:3837
+1445:2:3844
+1446:2:3845
+1447:2:3844
+1448:2:3845
+1449:2:3852
+1450:2:3856
+1451:0:4645
+1452:2:3861
+1453:0:4645
+1454:2:3862
+1455:0:4645
+1456:2:3863
+1457:0:4645
+1458:2:3864
+1459:0:4645
+1460:1:1316
+1461:1:1317
+1462:0:4643
+1463:2:3865
+1464:0:4649
+1465:1:2475