Add verif results

[urcu.git] / formal-model / urcu-controldataflow-alpha-no-ipi / urcu_free_no_mb.spin.input.trail

diff --git a/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_mb.spin.input.trail b/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_mb.spin.input.trail
new file mode 100644 (file)
index 0000000..fbd72f1
--- /dev/null
+++ b/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,1270 @@
+-2:3:-2
+-4:-4:-4
+1:0:4468
+2:3:4388
+3:3:4391
+4:3:4391
+5:3:4394
+6:3:4402
+7:3:4402
+8:3:4405
+9:3:4411
+10:3:4415
+11:3:4415
+12:3:4418
+13:3:4428
+14:3:4436
+15:3:4436
+16:3:4439
+17:3:4445
+18:3:4449
+19:3:4449
+20:3:4452
+21:3:4458
+22:3:4462
+23:3:4463
+24:0:4468
+25:3:4465
+26:0:4468
+27:2:3121
+28:0:4468
+29:2:3127
+30:0:4468
+31:2:3128
+32:0:4468
+33:2:3130
+34:0:4468
+35:2:3131
+36:0:4468
+37:2:3132
+38:0:4468
+39:2:3133
+40:0:4468
+41:2:3134
+42:2:3135
+43:2:3139
+44:2:3140
+45:2:3148
+46:2:3149
+47:2:3153
+48:2:3154
+49:2:3162
+50:2:3167
+51:2:3171
+52:2:3172
+53:2:3180
+54:2:3181
+55:2:3185
+56:2:3186
+57:2:3180
+58:2:3181
+59:2:3185
+60:2:3186
+61:2:3194
+62:2:3199
+63:2:3200
+64:2:3211
+65:2:3212
+66:2:3213
+67:2:3224
+68:2:3229
+69:2:3230
+70:2:3241
+71:2:3242
+72:2:3243
+73:2:3241
+74:2:3242
+75:2:3243
+76:2:3254
+77:2:3262
+78:0:4468
+79:2:3133
+80:0:4468
+81:2:3266
+82:2:3270
+83:2:3271
+84:2:3275
+85:2:3279
+86:2:3280
+87:2:3284
+88:2:3292
+89:2:3293
+90:2:3297
+91:2:3301
+92:2:3302
+93:2:3297
+94:2:3298
+95:2:3306
+96:0:4468
+97:2:3133
+98:0:4468
+99:2:3314
+100:2:3315
+101:2:3316
+102:0:4468
+103:2:3133
+104:0:4468
+105:2:3324
+106:0:4468
+107:2:3133
+108:0:4468
+109:2:3327
+110:2:3328
+111:2:3332
+112:2:3333
+113:2:3341
+114:2:3342
+115:2:3346
+116:2:3347
+117:2:3355
+118:2:3360
+119:2:3361
+120:2:3373
+121:2:3374
+122:2:3378
+123:2:3379
+124:2:3373
+125:2:3374
+126:2:3378
+127:2:3379
+128:2:3387
+129:2:3392
+130:2:3393
+131:2:3404
+132:2:3405
+133:2:3406
+134:2:3417
+135:2:3422
+136:2:3423
+137:2:3434
+138:2:3435
+139:2:3436
+140:2:3434
+141:2:3435
+142:2:3436
+143:2:3447
+144:2:3454
+145:0:4468
+146:2:3133
+147:0:4468
+148:2:3458
+149:2:3459
+150:2:3460
+151:2:3472
+152:2:3473
+153:2:3477
+154:2:3478
+155:2:3486
+156:2:3491
+157:2:3495
+158:2:3496
+159:2:3504
+160:2:3505
+161:2:3509
+162:2:3510
+163:2:3504
+164:2:3505
+165:2:3509
+166:2:3510
+167:2:3518
+168:2:3523
+169:2:3524
+170:2:3535
+171:2:3536
+172:2:3537
+173:2:3548
+174:2:3553
+175:2:3554
+176:2:3565
+177:2:3566
+178:2:3567
+179:2:3565
+180:2:3566
+181:2:3567
+182:2:3578
+183:2:3589
+184:2:3590
+185:0:4468
+186:2:3133
+187:0:4468
+188:2:3597
+189:2:3598
+190:2:3602
+191:2:3603
+192:2:3611
+193:2:3612
+194:2:3616
+195:2:3617
+196:2:3625
+197:2:3630
+198:2:3634
+199:2:3635
+200:2:3643
+201:2:3644
+202:2:3648
+203:2:3649
+204:2:3643
+205:2:3644
+206:2:3648
+207:2:3649
+208:2:3657
+209:2:3662
+210:2:3663
+211:2:3674
+212:2:3675
+213:2:3676
+214:2:3687
+215:2:3692
+216:2:3693
+217:2:3704
+218:2:3705
+219:2:3706
+220:2:3704
+221:2:3705
+222:2:3706
+223:2:3717
+224:0:4468
+225:2:3133
+226:0:4468
+227:2:3726
+228:2:3727
+229:2:3731
+230:2:3732
+231:2:3740
+232:2:3741
+233:2:3745
+234:2:3746
+235:2:3754
+236:2:3759
+237:2:3763
+238:2:3764
+239:2:3772
+240:2:3773
+241:2:3777
+242:2:3778
+243:2:3772
+244:2:3773
+245:2:3777
+246:2:3778
+247:2:3786
+248:2:3791
+249:2:3792
+250:2:3803
+251:2:3804
+252:2:3805
+253:2:3816
+254:2:3821
+255:2:3822
+256:2:3833
+257:2:3834
+258:2:3835
+259:2:3833
+260:2:3834
+261:2:3835
+262:2:3846
+263:2:3853
+264:0:4468
+265:2:3133
+266:0:4468
+267:2:3857
+268:2:3858
+269:2:3859
+270:2:3871
+271:2:3872
+272:2:3876
+273:2:3877
+274:2:3885
+275:2:3890
+276:2:3894
+277:2:3895
+278:2:3903
+279:2:3904
+280:2:3908
+281:2:3909
+282:2:3903
+283:2:3904
+284:2:3908
+285:2:3909
+286:2:3917
+287:2:3922
+288:2:3923
+289:2:3934
+290:2:3935
+291:2:3936
+292:2:3947
+293:2:3952
+294:2:3953
+295:2:3964
+296:2:3965
+297:2:3966
+298:2:3964
+299:2:3965
+300:2:3966
+301:2:3977
+302:2:3987
+303:2:3988
+304:0:4468
+305:2:3133
+306:0:4468
+307:2:3997
+308:2:3998
+309:0:4468
+310:2:3133
+311:0:4468
+312:2:4002
+313:0:4468
+314:2:4010
+315:0:4468
+316:2:3128
+317:0:4468
+318:2:3130
+319:0:4468
+320:2:3131
+321:0:4468
+322:2:3132
+323:0:4468
+324:2:3133
+325:0:4468
+326:2:3134
+327:2:3135
+328:2:3139
+329:2:3140
+330:2:3148
+331:2:3149
+332:2:3153
+333:2:3154
+334:2:3162
+335:2:3167
+336:2:3171
+337:2:3172
+338:2:3180
+339:2:3181
+340:2:3182
+341:2:3180
+342:2:3181
+343:2:3185
+344:2:3186
+345:2:3194
+346:2:3199
+347:2:3200
+348:2:3211
+349:2:3212
+350:2:3213
+351:2:3224
+352:2:3229
+353:2:3230
+354:2:3241
+355:2:3242
+356:2:3243
+357:2:3241
+358:2:3242
+359:2:3243
+360:2:3254
+361:2:3262
+362:0:4468
+363:2:3133
+364:0:4468
+365:2:3266
+366:2:3270
+367:2:3271
+368:2:3275
+369:2:3279
+370:2:3280
+371:2:3284
+372:2:3292
+373:2:3293
+374:2:3297
+375:2:3298
+376:2:3297
+377:2:3301
+378:2:3302
+379:2:3306
+380:0:4468
+381:2:3133
+382:0:4468
+383:2:3314
+384:2:3315
+385:2:3316
+386:0:4468
+387:2:3133
+388:0:4468
+389:2:3324
+390:0:4468
+391:2:3133
+392:0:4468
+393:2:3327
+394:2:3328
+395:2:3332
+396:2:3333
+397:2:3341
+398:2:3342
+399:2:3346
+400:2:3347
+401:2:3355
+402:2:3360
+403:2:3361
+404:2:3373
+405:2:3374
+406:2:3378
+407:2:3379
+408:2:3373
+409:2:3374
+410:2:3378
+411:2:3379
+412:2:3387
+413:2:3392
+414:2:3393
+415:2:3404
+416:2:3405
+417:2:3406
+418:2:3417
+419:2:3422
+420:2:3423
+421:2:3434
+422:2:3435
+423:2:3436
+424:2:3434
+425:2:3435
+426:2:3436
+427:2:3447
+428:2:3454
+429:0:4468
+430:2:3133
+431:0:4468
+432:2:3458
+433:2:3459
+434:2:3460
+435:2:3472
+436:2:3473
+437:2:3477
+438:2:3478
+439:2:3486
+440:2:3491
+441:2:3495
+442:2:3496
+443:2:3504
+444:2:3505
+445:2:3509
+446:2:3510
+447:2:3504
+448:2:3505
+449:2:3509
+450:2:3510
+451:2:3518
+452:2:3523
+453:2:3524
+454:2:3535
+455:2:3536
+456:2:3537
+457:2:3548
+458:2:3553
+459:2:3554
+460:2:3565
+461:2:3566
+462:2:3567
+463:2:3565
+464:2:3566
+465:2:3567
+466:2:3578
+467:2:3589
+468:2:3590
+469:0:4468
+470:2:3133
+471:0:4468
+472:2:3597
+473:2:3598
+474:2:3602
+475:2:3603
+476:2:3611
+477:2:3612
+478:2:3616
+479:2:3617
+480:2:3625
+481:2:3630
+482:2:3634
+483:2:3635
+484:2:3643
+485:2:3644
+486:2:3648
+487:2:3649
+488:2:3643
+489:2:3644
+490:2:3648
+491:2:3649
+492:2:3657
+493:2:3662
+494:2:3663
+495:2:3674
+496:2:3675
+497:2:3676
+498:2:3687
+499:2:3692
+500:2:3693
+501:2:3704
+502:2:3705
+503:2:3706
+504:2:3704
+505:2:3705
+506:2:3706
+507:2:3717
+508:0:4468
+509:2:3133
+510:0:4468
+511:2:3726
+512:2:3727
+513:2:3731
+514:2:3732
+515:2:3740
+516:2:3741
+517:2:3745
+518:2:3746
+519:2:3754
+520:2:3759
+521:2:3763
+522:2:3764
+523:2:3772
+524:2:3773
+525:2:3777
+526:2:3778
+527:2:3772
+528:2:3773
+529:2:3777
+530:2:3778
+531:2:3786
+532:2:3791
+533:2:3792
+534:2:3803
+535:2:3804
+536:2:3805
+537:2:3816
+538:2:3821
+539:2:3822
+540:2:3833
+541:2:3834
+542:2:3835
+543:2:3833
+544:2:3834
+545:2:3835
+546:2:3846
+547:2:3853
+548:0:4468
+549:2:3133
+550:0:4468
+551:2:3857
+552:2:3858
+553:2:3859
+554:2:3871
+555:2:3872
+556:2:3876
+557:2:3877
+558:2:3885
+559:2:3890
+560:2:3894
+561:2:3895
+562:2:3903
+563:2:3904
+564:2:3908
+565:2:3909
+566:2:3903
+567:2:3904
+568:2:3908
+569:2:3909
+570:2:3917
+571:2:3922
+572:2:3923
+573:2:3934
+574:2:3935
+575:2:3936
+576:2:3947
+577:2:3952
+578:2:3953
+579:2:3964
+580:2:3965
+581:2:3966
+582:2:3964
+583:2:3965
+584:2:3966
+585:2:3977
+586:2:3987
+587:2:3988
+588:0:4468
+589:2:3133
+590:0:4468
+591:2:3997
+592:2:3998
+593:0:4468
+594:2:3133
+595:0:4468
+596:2:4002
+597:0:4468
+598:2:4010
+599:0:4468
+600:2:3128
+601:0:4468
+602:2:3130
+603:0:4468
+604:2:3131
+605:0:4468
+606:2:3132
+607:0:4468
+608:2:3133
+609:0:4468
+610:2:3134
+611:2:3135
+612:2:3139
+613:2:3140
+614:2:3148
+615:2:3149
+616:2:3153
+617:2:3154
+618:2:3162
+619:2:3167
+620:2:3171
+621:2:3172
+622:2:3180
+623:2:3181
+624:2:3185
+625:2:3186
+626:2:3180
+627:2:3181
+628:2:3182
+629:2:3194
+630:2:3199
+631:2:3200
+632:2:3211
+633:2:3212
+634:2:3213
+635:2:3224
+636:2:3229
+637:2:3230
+638:2:3241
+639:2:3242
+640:2:3243
+641:2:3241
+642:2:3242
+643:2:3243
+644:2:3254
+645:2:3262
+646:0:4468
+647:2:3133
+648:0:4468
+649:2:3266
+650:2:3270
+651:2:3271
+652:2:3275
+653:2:3279
+654:2:3280
+655:2:3284
+656:2:3292
+657:2:3293
+658:2:3297
+659:2:3301
+660:2:3302
+661:2:3297
+662:2:3298
+663:2:3306
+664:0:4468
+665:2:3133
+666:0:4468
+667:2:3314
+668:2:3315
+669:2:3316
+670:0:4468
+671:2:3133
+672:0:4468
+673:2:3324
+674:0:4468
+675:2:3133
+676:0:4468
+677:2:3327
+678:2:3328
+679:2:3332
+680:2:3333
+681:2:3341
+682:2:3342
+683:2:3346
+684:2:3347
+685:2:3355
+686:2:3360
+687:2:3361
+688:2:3373
+689:2:3374
+690:2:3378
+691:2:3379
+692:2:3373
+693:2:3374
+694:2:3378
+695:2:3379
+696:2:3387
+697:2:3392
+698:2:3393
+699:2:3404
+700:2:3405
+701:2:3406
+702:2:3417
+703:2:3422
+704:2:3423
+705:2:3434
+706:2:3435
+707:2:3436
+708:2:3434
+709:2:3435
+710:2:3436
+711:2:3447
+712:2:3454
+713:0:4468
+714:2:3133
+715:0:4468
+716:2:3458
+717:2:3459
+718:2:3460
+719:2:3472
+720:2:3473
+721:2:3477
+722:2:3478
+723:2:3486
+724:2:3491
+725:2:3495
+726:2:3496
+727:2:3504
+728:2:3505
+729:2:3509
+730:2:3510
+731:2:3504
+732:2:3505
+733:2:3509
+734:2:3510
+735:2:3518
+736:2:3523
+737:2:3524
+738:2:3535
+739:2:3536
+740:2:3537
+741:2:3548
+742:2:3553
+743:2:3554
+744:2:3565
+745:2:3566
+746:2:3567
+747:2:3565
+748:2:3566
+749:2:3567
+750:2:3578
+751:2:3589
+752:2:3590
+753:0:4468
+754:2:3133
+755:0:4468
+756:2:3597
+757:2:3598
+758:2:3602
+759:2:3603
+760:2:3611
+761:2:3612
+762:2:3616
+763:2:3617
+764:2:3625
+765:2:3630
+766:2:3634
+767:2:3635
+768:2:3643
+769:2:3644
+770:2:3648
+771:2:3649
+772:2:3643
+773:2:3644
+774:2:3648
+775:2:3649
+776:2:3657
+777:2:3662
+778:2:3663
+779:2:3674
+780:2:3675
+781:2:3676
+782:2:3687
+783:2:3692
+784:2:3693
+785:2:3704
+786:2:3705
+787:2:3706
+788:2:3704
+789:2:3705
+790:2:3706
+791:2:3717
+792:0:4468
+793:2:3133
+794:0:4468
+795:2:3857
+796:2:3858
+797:2:3862
+798:2:3863
+799:2:3871
+800:2:3872
+801:2:3876
+802:2:3877
+803:2:3885
+804:2:3890
+805:2:3894
+806:2:3895
+807:2:3903
+808:2:3904
+809:2:3908
+810:2:3909
+811:2:3903
+812:2:3904
+813:2:3908
+814:2:3909
+815:2:3917
+816:2:3922
+817:2:3923
+818:2:3934
+819:2:3935
+820:2:3936
+821:2:3947
+822:2:3952
+823:2:3953
+824:2:3964
+825:2:3965
+826:2:3966
+827:2:3964
+828:2:3965
+829:2:3966
+830:2:3977
+831:2:3987
+832:2:3988
+833:0:4468
+834:2:3133
+835:0:4468
+836:2:3997
+837:2:3998
+838:0:4468
+839:2:3133
+840:0:4468
+841:2:3726
+842:2:3727
+843:2:3731
+844:2:3732
+845:2:3740
+846:2:3741
+847:2:3745
+848:2:3746
+849:2:3754
+850:2:3759
+851:2:3763
+852:2:3764
+853:2:3772
+854:2:3773
+855:2:3774
+856:2:3772
+857:2:3773
+858:2:3777
+859:2:3778
+860:2:3786
+861:2:3791
+862:2:3792
+863:2:3803
+864:2:3804
+865:2:3805
+866:2:3816
+867:2:3821
+868:2:3822
+869:2:3833
+870:2:3834
+871:2:3835
+872:2:3833
+873:2:3834
+874:2:3835
+875:2:3846
+876:2:3853
+877:0:4468
+878:2:3133
+879:0:4468
+880:2:4002
+881:0:4468
+882:2:4010
+883:0:4468
+884:2:4011
+885:0:4468
+886:2:4016
+887:0:4468
+888:1:2
+889:0:4468
+890:2:4017
+891:0:4468
+892:1:8
+893:0:4468
+894:2:4016
+895:0:4468
+896:1:9
+897:0:4468
+898:2:4017
+899:0:4468
+900:1:10
+901:0:4468
+902:2:4016
+903:0:4468
+904:1:11
+905:0:4468
+906:2:4017
+907:0:4468
+908:1:12
+909:0:4468
+910:2:4016
+911:0:4468
+912:1:13
+913:0:4468
+914:2:4017
+915:0:4468
+916:1:14
+917:0:4468
+918:2:4016
+919:0:4468
+920:1:15
+921:0:4468
+922:2:4017
+923:0:4468
+924:1:16
+925:1:17
+926:1:21
+927:1:22
+928:1:30
+929:1:31
+930:1:35
+931:1:36
+932:1:44
+933:1:49
+934:1:53
+935:1:54
+936:1:62
+937:1:63
+938:1:67
+939:1:68
+940:1:62
+941:1:63
+942:1:67
+943:1:68
+944:1:76
+945:1:81
+946:1:82
+947:1:93
+948:1:94
+949:1:95
+950:1:106
+951:1:118
+952:1:119
+953:1:123
+954:1:124
+955:1:125
+956:1:123
+957:1:124
+958:1:125
+959:1:136
+960:0:4468
+961:2:4016
+962:0:4468
+963:1:15
+964:0:4468
+965:2:4017
+966:0:4468
+967:1:145
+968:1:146
+969:0:4468
+970:2:4016
+971:0:4468
+972:1:15
+973:0:4468
+974:2:4017
+975:0:4468
+976:1:152
+977:1:153
+978:1:157
+979:1:158
+980:1:166
+981:1:167
+982:1:171
+983:1:172
+984:1:180
+985:1:185
+986:1:189
+987:1:190
+988:1:198
+989:1:199
+990:1:203
+991:1:204
+992:1:198
+993:1:199
+994:1:203
+995:1:204
+996:1:212
+997:1:217
+998:1:218
+999:1:229
+1000:1:230
+1001:1:231
+1002:1:242
+1003:1:254
+1004:1:255
+1005:1:259
+1006:1:260
+1007:1:261
+1008:1:259
+1009:1:260
+1010:1:261
+1011:1:272
+1012:0:4468
+1013:2:4016
+1014:0:4468
+1015:1:15
+1016:0:4468
+1017:2:4017
+1018:0:4468
+1019:1:281
+1020:1:282
+1021:1:286
+1022:1:287
+1023:1:295
+1024:1:296
+1025:1:300
+1026:1:301
+1027:1:309
+1028:1:314
+1029:1:318
+1030:1:319
+1031:1:327
+1032:1:328
+1033:1:332
+1034:1:333
+1035:1:327
+1036:1:328
+1037:1:332
+1038:1:333
+1039:1:341
+1040:1:346
+1041:1:347
+1042:1:358
+1043:1:359
+1044:1:360
+1045:1:371
+1046:1:383
+1047:1:384
+1048:1:388
+1049:1:389
+1050:1:390
+1051:1:388
+1052:1:389
+1053:1:390
+1054:1:401
+1055:1:408
+1056:0:4468
+1057:2:4016
+1058:0:4468
+1059:1:15
+1060:0:4468
+1061:2:4017
+1062:0:4468
+1063:1:636
+1064:1:637
+1065:1:641
+1066:1:642
+1067:1:650
+1068:1:651
+1069:1:652
+1070:1:664
+1071:1:669
+1072:1:673
+1073:1:674
+1074:1:682
+1075:1:683
+1076:1:687
+1077:1:688
+1078:1:682
+1079:1:683
+1080:1:687
+1081:1:688
+1082:1:696
+1083:1:701
+1084:1:702
+1085:1:713
+1086:1:714
+1087:1:715
+1088:1:726
+1089:1:738
+1090:1:739
+1091:1:743
+1092:1:744
+1093:1:745
+1094:1:743
+1095:1:744
+1096:1:745
+1097:1:756
+1098:0:4468
+1099:2:4016
+1100:0:4468
+1101:1:15
+1102:0:4468
+1103:2:4017
+1104:0:4468
+1105:1:765
+1106:1:768
+1107:1:769
+1108:0:4468
+1109:2:4016
+1110:0:4468
+1111:1:15
+1112:0:4468
+1113:2:4017
+1114:0:4468
+1115:1:772
+1116:1:773
+1117:1:777
+1118:1:778
+1119:1:786
+1120:1:787
+1121:1:791
+1122:1:792
+1123:1:800
+1124:1:805
+1125:1:809
+1126:1:810
+1127:1:818
+1128:1:819
+1129:1:823
+1130:1:824
+1131:1:818
+1132:1:819
+1133:1:823
+1134:1:824
+1135:1:832
+1136:1:837
+1137:1:838
+1138:1:849
+1139:1:850
+1140:1:851
+1141:1:862
+1142:1:874
+1143:1:875
+1144:1:879
+1145:1:880
+1146:1:881
+1147:1:879
+1148:1:880
+1149:1:881
+1150:1:892
+1151:0:4468
+1152:2:4016
+1153:0:4468
+1154:1:15
+1155:0:4468
+1156:2:4017
+1157:0:4468
+1158:1:1032
+1159:1:1033
+1160:1:1037
+1161:1:1038
+1162:1:1046
+1163:1:1047
+1164:1:1051
+1165:1:1052
+1166:1:1060
+1167:1:1065
+1168:1:1069
+1169:1:1070
+1170:1:1078
+1171:1:1079
+1172:1:1083
+1173:1:1084
+1174:1:1078
+1175:1:1079
+1176:1:1083
+1177:1:1084
+1178:1:1092
+1179:1:1097
+1180:1:1098
+1181:1:1109
+1182:1:1110
+1183:1:1111
+1184:1:1122
+1185:1:1134
+1186:1:1135
+1187:1:1139
+1188:1:1140
+1189:1:1141
+1190:1:1139
+1191:1:1140
+1192:1:1141
+1193:1:1152
+1194:1:1159
+1195:1:1163
+1196:0:4468
+1197:2:4016
+1198:0:4468
+1199:1:15
+1200:0:4468
+1201:2:4017
+1202:0:4468
+1203:1:1164
+1204:1:1165
+1205:1:1169
+1206:1:1170
+1207:1:1178
+1208:1:1179
+1209:1:1180
+1210:1:1192
+1211:1:1197
+1212:1:1201
+1213:1:1202
+1214:1:1210
+1215:1:1211
+1216:1:1215
+1217:1:1216
+1218:1:1210
+1219:1:1211
+1220:1:1215
+1221:1:1216
+1222:1:1224
+1223:1:1229
+1224:1:1230
+1225:1:1241
+1226:1:1242
+1227:1:1243
+1228:1:1254
+1229:1:1266
+1230:1:1267
+1231:1:1271
+1232:1:1272
+1233:1:1273
+1234:1:1271
+1235:1:1272
+1236:1:1273
+1237:1:1284
+1238:0:4468
+1239:2:4016
+1240:0:4468
+1241:1:15
+1242:0:4468
+1243:2:4017
+1244:0:4468
+1245:1:1293
+1246:0:4468
+1247:2:4016
+1248:0:4468
+1249:1:3027
+1250:1:3034
+1251:1:3035
+1252:1:3042
+1253:1:3047
+1254:1:3054
+1255:1:3055
+1256:1:3054
+1257:1:3055
+1258:1:3062
+1259:1:3066
+1260:0:4468
+1261:2:4017
+1262:0:4468
+1263:1:1295
+1264:1:1296
+1265:0:4466
+1266:2:4016
+1267:0:4472
+1268:1:756