X-Git-Url: https://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Fresults%2Furcu-controldataflow-ipi%2Furcu_free_no_wmb.spin.input.trail;fp=formal-model%2Fresults%2Furcu-controldataflow-ipi%2Furcu_free_no_wmb.spin.input.trail;h=ddfccff25a07d06f31fb6563b47aa9b52cebb82e;hb=dbf6928575dc30b5d8602b9a50ca385670f26ff1;hp=0000000000000000000000000000000000000000;hpb=6b0de96380f9abdb7a77b79d3b2d0cf5762f266f;p=urcu.git

diff --git a/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_wmb.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_wmb.spin.input.trail
new file mode 100644
index 0000000..ddfccff
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1485 @@
+-2:3:-2
+-4:-4:-4
+1:0:4644
+2:3:4564
+3:3:4567
+4:3:4567
+5:3:4570
+6:3:4578
+7:3:4578
+8:3:4581
+9:3:4587
+10:3:4591
+11:3:4591
+12:3:4594
+13:3:4604
+14:3:4612
+15:3:4612
+16:3:4615
+17:3:4621
+18:3:4625
+19:3:4625
+20:3:4628
+21:3:4634
+22:3:4638
+23:3:4639
+24:0:4644
+25:3:4641
+26:0:4644
+27:2:2871
+28:0:4644
+29:2:2877
+30:0:4644
+31:2:2878
+32:0:4644
+33:2:2880
+34:0:4644
+35:2:2881
+36:0:4644
+37:2:2882
+38:0:4644
+39:2:2883
+40:2:2884
+41:2:2888
+42:2:2889
+43:2:2897
+44:2:2898
+45:2:2902
+46:2:2903
+47:2:2911
+48:2:2916
+49:2:2920
+50:2:2921
+51:2:2929
+52:2:2930
+53:2:2934
+54:2:2935
+55:2:2929
+56:2:2930
+57:2:2934
+58:2:2935
+59:2:2943
+60:2:2948
+61:2:2949
+62:2:2960
+63:2:2961
+64:2:2962
+65:2:2973
+66:2:2978
+67:2:2979
+68:2:2990
+69:2:2991
+70:2:2992
+71:2:2990
+72:2:2991
+73:2:2992
+74:2:3003
+75:2:3011
+76:0:4644
+77:2:2882
+78:0:4644
+79:2:3063
+80:2:3064
+81:2:3065
+82:0:4644
+83:2:2882
+84:0:4644
+85:2:3070
+86:0:4644
+87:2:3773
+88:2:3774
+89:2:3778
+90:2:3782
+91:2:3783
+92:2:3787
+93:2:3792
+94:2:3800
+95:2:3804
+96:2:3805
+97:2:3800
+98:2:3801
+99:2:3809
+100:2:3816
+101:2:3823
+102:2:3824
+103:2:3831
+104:2:3836
+105:2:3843
+106:2:3844
+107:2:3843
+108:2:3844
+109:2:3851
+110:2:3855
+111:0:4644
+112:2:3860
+113:0:4644
+114:2:3861
+115:0:4644
+116:2:3862
+117:0:4644
+118:2:3863
+119:0:4644
+120:1:2
+121:0:4644
+122:2:3864
+123:0:4644
+124:1:8
+125:0:4644
+126:1:9
+127:0:4644
+128:2:3863
+129:0:4644
+130:1:10
+131:0:4644
+132:2:3864
+133:0:4644
+134:1:11
+135:0:4644
+136:2:3863
+137:0:4644
+138:1:12
+139:0:4644
+140:2:3864
+141:0:4644
+142:1:13
+143:0:4644
+144:2:3863
+145:0:4644
+146:1:14
+147:0:4644
+148:2:3864
+149:0:4644
+150:1:15
+151:0:4644
+152:1:16
+153:0:4644
+154:2:3863
+155:0:4644
+156:1:17
+157:0:4644
+158:2:3864
+159:0:4644
+160:1:26
+161:0:4644
+162:2:3863
+163:0:4644
+164:1:30
+165:1:31
+166:1:35
+167:1:39
+168:1:40
+169:1:44
+170:1:52
+171:1:53
+172:1:57
+173:1:61
+174:1:62
+175:1:57
+176:1:61
+177:1:62
+178:1:66
+179:1:73
+180:1:80
+181:1:81
+182:1:88
+183:1:93
+184:1:100
+185:1:101
+186:1:100
+187:1:101
+188:1:108
+189:1:112
+190:0:4644
+191:2:3864
+192:0:4644
+193:1:117
+194:0:4644
+195:2:3865
+196:0:4644
+197:2:3870
+198:0:4644
+199:2:3871
+200:0:4644
+201:2:3879
+202:2:3880
+203:2:3884
+204:2:3888
+205:2:3889
+206:2:3893
+207:2:3901
+208:2:3902
+209:2:3906
+210:2:3910
+211:2:3911
+212:2:3906
+213:2:3910
+214:2:3911
+215:2:3915
+216:2:3922
+217:2:3929
+218:2:3930
+219:2:3937
+220:2:3942
+221:2:3949
+222:2:3950
+223:2:3949
+224:2:3950
+225:2:3957
+226:2:3961
+227:0:4644
+228:2:3072
+229:2:3754
+230:0:4644
+231:2:2882
+232:0:4644
+233:2:3073
+234:0:4644
+235:2:2882
+236:0:4644
+237:2:3076
+238:2:3077
+239:2:3081
+240:2:3082
+241:2:3090
+242:2:3091
+243:2:3095
+244:2:3096
+245:2:3104
+246:2:3109
+247:2:3113
+248:2:3114
+249:2:3122
+250:2:3123
+251:2:3127
+252:2:3128
+253:2:3122
+254:2:3123
+255:2:3127
+256:2:3128
+257:2:3136
+258:2:3141
+259:2:3142
+260:2:3153
+261:2:3154
+262:2:3155
+263:2:3166
+264:2:3171
+265:2:3172
+266:2:3183
+267:2:3184
+268:2:3185
+269:2:3183
+270:2:3184
+271:2:3185
+272:2:3196
+273:2:3203
+274:0:4644
+275:2:2882
+276:0:4644
+277:2:3207
+278:2:3208
+279:2:3209
+280:2:3221
+281:2:3222
+282:2:3226
+283:2:3227
+284:2:3235
+285:2:3240
+286:2:3244
+287:2:3245
+288:2:3253
+289:2:3254
+290:2:3258
+291:2:3259
+292:2:3253
+293:2:3254
+294:2:3258
+295:2:3259
+296:2:3267
+297:2:3272
+298:2:3273
+299:2:3284
+300:2:3285
+301:2:3286
+302:2:3297
+303:2:3302
+304:2:3303
+305:2:3314
+306:2:3315
+307:2:3316
+308:2:3314
+309:2:3315
+310:2:3316
+311:2:3327
+312:2:3338
+313:2:3339
+314:0:4644
+315:2:2882
+316:0:4644
+317:2:3345
+318:2:3346
+319:2:3350
+320:2:3351
+321:2:3359
+322:2:3360
+323:2:3364
+324:2:3365
+325:2:3373
+326:2:3378
+327:2:3382
+328:2:3383
+329:2:3391
+330:2:3392
+331:2:3396
+332:2:3397
+333:2:3391
+334:2:3392
+335:2:3396
+336:2:3397
+337:2:3405
+338:2:3410
+339:2:3411
+340:2:3422
+341:2:3423
+342:2:3424
+343:2:3435
+344:2:3440
+345:2:3441
+346:2:3452
+347:2:3453
+348:2:3454
+349:2:3452
+350:2:3453
+351:2:3454
+352:2:3465
+353:0:4644
+354:2:2882
+355:0:4644
+356:2:3474
+357:2:3475
+358:2:3479
+359:2:3480
+360:2:3488
+361:2:3489
+362:2:3493
+363:2:3494
+364:2:3502
+365:2:3507
+366:2:3511
+367:2:3512
+368:2:3520
+369:2:3521
+370:2:3525
+371:2:3526
+372:2:3520
+373:2:3521
+374:2:3525
+375:2:3526
+376:2:3534
+377:2:3539
+378:2:3540
+379:2:3551
+380:2:3552
+381:2:3553
+382:2:3564
+383:2:3569
+384:2:3570
+385:2:3581
+386:2:3582
+387:2:3583
+388:2:3581
+389:2:3582
+390:2:3583
+391:2:3594
+392:2:3601
+393:0:4644
+394:2:2882
+395:0:4644
+396:2:3605
+397:2:3606
+398:2:3607
+399:2:3619
+400:2:3620
+401:2:3624
+402:2:3625
+403:2:3633
+404:2:3638
+405:2:3642
+406:2:3643
+407:2:3651
+408:2:3652
+409:2:3656
+410:2:3657
+411:2:3651
+412:2:3652
+413:2:3656
+414:2:3657
+415:2:3665
+416:2:3670
+417:2:3671
+418:2:3682
+419:2:3683
+420:2:3684
+421:2:3695
+422:2:3700
+423:2:3701
+424:2:3712
+425:2:3713
+426:2:3714
+427:2:3712
+428:2:3713
+429:2:3714
+430:2:3725
+431:2:3735
+432:2:3736
+433:0:4644
+434:2:2882
+435:0:4644
+436:2:3742
+437:0:4644
+438:2:4367
+439:2:4368
+440:2:4372
+441:2:4376
+442:2:4377
+443:2:4381
+444:2:4389
+445:2:4390
+446:2:4394
+447:2:4398
+448:2:4399
+449:2:4394
+450:2:4398
+451:2:4399
+452:2:4403
+453:2:4410
+454:2:4417
+455:2:4418
+456:2:4425
+457:2:4430
+458:2:4437
+459:2:4438
+460:2:4437
+461:2:4438
+462:2:4445
+463:2:4449
+464:0:4644
+465:2:4454
+466:0:4644
+467:2:4455
+468:0:4644
+469:2:4456
+470:0:4644
+471:2:4457
+472:0:4644
+473:1:26
+474:0:4644
+475:2:4458
+476:0:4644
+477:1:30
+478:1:31
+479:1:35
+480:1:39
+481:1:40
+482:1:44
+483:1:52
+484:1:53
+485:1:57
+486:1:61
+487:1:62
+488:1:57
+489:1:61
+490:1:62
+491:1:66
+492:1:73
+493:1:80
+494:1:81
+495:1:88
+496:1:93
+497:1:100
+498:1:101
+499:1:100
+500:1:101
+501:1:108
+502:1:112
+503:0:4644
+504:2:4457
+505:0:4644
+506:1:117
+507:0:4644
+508:2:4458
+509:0:4644
+510:2:4459
+511:0:4644
+512:2:4464
+513:0:4644
+514:2:4465
+515:0:4644
+516:2:4473
+517:2:4474
+518:2:4478
+519:2:4482
+520:2:4483
+521:2:4487
+522:2:4495
+523:2:4496
+524:2:4500
+525:2:4504
+526:2:4505
+527:2:4500
+528:2:4504
+529:2:4505
+530:2:4509
+531:2:4516
+532:2:4523
+533:2:4524
+534:2:4531
+535:2:4536
+536:2:4543
+537:2:4544
+538:2:4543
+539:2:4544
+540:2:4551
+541:2:4555
+542:0:4644
+543:2:3744
+544:2:3754
+545:0:4644
+546:2:2882
+547:0:4644
+548:2:3745
+549:2:3746
+550:0:4644
+551:2:2882
+552:0:4644
+553:2:3750
+554:0:4644
+555:2:3758
+556:0:4644
+557:2:2878
+558:0:4644
+559:2:2880
+560:0:4644
+561:2:2881
+562:0:4644
+563:2:2882
+564:0:4644
+565:2:3063
+566:2:3064
+567:2:3065
+568:0:4644
+569:2:2882
+570:0:4644
+571:2:2883
+572:2:2884
+573:2:2888
+574:2:2889
+575:2:2897
+576:2:2898
+577:2:2902
+578:2:2903
+579:2:2911
+580:2:2916
+581:2:2917
+582:2:2929
+583:2:2930
+584:2:2931
+585:2:2929
+586:2:2930
+587:2:2934
+588:2:2935
+589:2:2943
+590:2:2948
+591:2:2949
+592:2:2960
+593:2:2961
+594:2:2962
+595:2:2973
+596:2:2978
+597:2:2979
+598:2:2990
+599:2:2991
+600:2:2992
+601:2:2990
+602:2:2991
+603:2:2992
+604:2:3003
+605:2:3011
+606:0:4644
+607:2:2882
+608:0:4644
+609:2:3070
+610:0:4644
+611:2:3773
+612:2:3774
+613:2:3778
+614:2:3782
+615:2:3783
+616:2:3787
+617:2:3795
+618:2:3796
+619:2:3800
+620:2:3801
+621:2:3800
+622:2:3804
+623:2:3805
+624:2:3809
+625:2:3816
+626:2:3823
+627:2:3824
+628:2:3831
+629:2:3836
+630:2:3843
+631:2:3844
+632:2:3843
+633:2:3844
+634:2:3851
+635:2:3855
+636:0:4644
+637:2:3860
+638:0:4644
+639:2:3861
+640:0:4644
+641:2:3862
+642:0:4644
+643:2:3863
+644:0:4644
+645:1:26
+646:0:4644
+647:2:3864
+648:0:4644
+649:1:30
+650:1:31
+651:1:35
+652:1:39
+653:1:40
+654:1:44
+655:1:52
+656:1:53
+657:1:57
+658:1:61
+659:1:62
+660:1:57
+661:1:61
+662:1:62
+663:1:66
+664:1:73
+665:1:80
+666:1:81
+667:1:88
+668:1:93
+669:1:100
+670:1:101
+671:1:100
+672:1:101
+673:1:108
+674:1:112
+675:0:4644
+676:2:3863
+677:0:4644
+678:1:117
+679:0:4644
+680:2:3864
+681:0:4644
+682:2:3865
+683:0:4644
+684:2:3870
+685:0:4644
+686:2:3871
+687:0:4644
+688:2:3879
+689:2:3880
+690:2:3884
+691:2:3888
+692:2:3889
+693:2:3893
+694:2:3901
+695:2:3902
+696:2:3906
+697:2:3910
+698:2:3911
+699:2:3906
+700:2:3910
+701:2:3911
+702:2:3915
+703:2:3922
+704:2:3929
+705:2:3930
+706:2:3937
+707:2:3942
+708:2:3949
+709:2:3950
+710:2:3949
+711:2:3950
+712:2:3957
+713:2:3961
+714:0:4644
+715:2:3072
+716:2:3754
+717:0:4644
+718:2:2882
+719:0:4644
+720:2:3073
+721:0:4644
+722:2:2882
+723:0:4644
+724:2:3076
+725:2:3077
+726:2:3081
+727:2:3082
+728:2:3090
+729:2:3091
+730:2:3095
+731:2:3096
+732:2:3104
+733:2:3109
+734:2:3113
+735:2:3114
+736:2:3122
+737:2:3123
+738:2:3127
+739:2:3128
+740:2:3122
+741:2:3123
+742:2:3127
+743:2:3128
+744:2:3136
+745:2:3141
+746:2:3142
+747:2:3153
+748:2:3154
+749:2:3155
+750:2:3166
+751:2:3171
+752:2:3172
+753:2:3183
+754:2:3184
+755:2:3185
+756:2:3183
+757:2:3184
+758:2:3185
+759:2:3196
+760:2:3203
+761:0:4644
+762:2:2882
+763:0:4644
+764:2:3207
+765:2:3208
+766:2:3209
+767:2:3221
+768:2:3222
+769:2:3226
+770:2:3227
+771:2:3235
+772:2:3240
+773:2:3244
+774:2:3245
+775:2:3253
+776:2:3254
+777:2:3258
+778:2:3259
+779:2:3253
+780:2:3254
+781:2:3258
+782:2:3259
+783:2:3267
+784:2:3272
+785:2:3273
+786:2:3284
+787:2:3285
+788:2:3286
+789:2:3297
+790:2:3302
+791:2:3303
+792:2:3314
+793:2:3315
+794:2:3316
+795:2:3314
+796:2:3315
+797:2:3316
+798:2:3327
+799:2:3338
+800:2:3339
+801:0:4644
+802:2:2882
+803:0:4644
+804:2:3345
+805:2:3346
+806:2:3350
+807:2:3351
+808:2:3359
+809:2:3360
+810:2:3364
+811:2:3365
+812:2:3373
+813:2:3378
+814:2:3382
+815:2:3383
+816:2:3391
+817:2:3392
+818:2:3396
+819:2:3397
+820:2:3391
+821:2:3392
+822:2:3396
+823:2:3397
+824:2:3405
+825:2:3410
+826:2:3411
+827:2:3422
+828:2:3423
+829:2:3424
+830:2:3435
+831:2:3440
+832:2:3441
+833:2:3452
+834:2:3453
+835:2:3454
+836:2:3452
+837:2:3453
+838:2:3454
+839:2:3465
+840:0:4644
+841:2:2882
+842:0:4644
+843:2:3474
+844:2:3475
+845:2:3479
+846:2:3480
+847:2:3488
+848:2:3489
+849:2:3493
+850:2:3494
+851:2:3502
+852:2:3507
+853:2:3511
+854:2:3512
+855:2:3520
+856:2:3521
+857:2:3525
+858:2:3526
+859:2:3520
+860:2:3521
+861:2:3525
+862:2:3526
+863:2:3534
+864:2:3539
+865:2:3540
+866:2:3551
+867:2:3552
+868:2:3553
+869:2:3564
+870:2:3569
+871:2:3570
+872:2:3581
+873:2:3582
+874:2:3583
+875:2:3581
+876:2:3582
+877:2:3583
+878:2:3594
+879:2:3601
+880:0:4644
+881:2:2882
+882:0:4644
+883:2:3605
+884:2:3606
+885:2:3607
+886:2:3619
+887:2:3620
+888:2:3624
+889:2:3625
+890:2:3633
+891:2:3638
+892:2:3642
+893:2:3643
+894:2:3651
+895:2:3652
+896:2:3656
+897:2:3657
+898:2:3651
+899:2:3652
+900:2:3656
+901:2:3657
+902:2:3665
+903:2:3670
+904:2:3671
+905:2:3682
+906:2:3683
+907:2:3684
+908:2:3695
+909:2:3700
+910:2:3701
+911:2:3712
+912:2:3713
+913:2:3714
+914:2:3712
+915:2:3713
+916:2:3714
+917:2:3725
+918:2:3735
+919:2:3736
+920:0:4644
+921:2:2882
+922:0:4644
+923:2:3742
+924:0:4644
+925:2:4367
+926:2:4368
+927:2:4372
+928:2:4376
+929:2:4377
+930:2:4381
+931:2:4389
+932:2:4390
+933:2:4394
+934:2:4398
+935:2:4399
+936:2:4394
+937:2:4398
+938:2:4399
+939:2:4403
+940:2:4410
+941:2:4417
+942:2:4418
+943:2:4425
+944:2:4430
+945:2:4437
+946:2:4438
+947:2:4437
+948:2:4438
+949:2:4445
+950:2:4449
+951:0:4644
+952:2:4454
+953:0:4644
+954:2:4455
+955:0:4644
+956:2:4456
+957:0:4644
+958:2:4457
+959:0:4644
+960:1:26
+961:0:4644
+962:2:4458
+963:0:4644
+964:1:30
+965:1:31
+966:1:35
+967:1:39
+968:1:40
+969:1:44
+970:1:52
+971:1:53
+972:1:57
+973:1:61
+974:1:62
+975:1:57
+976:1:61
+977:1:62
+978:1:66
+979:1:73
+980:1:80
+981:1:81
+982:1:88
+983:1:93
+984:1:100
+985:1:101
+986:1:100
+987:1:101
+988:1:108
+989:1:112
+990:0:4644
+991:2:4457
+992:0:4644
+993:1:117
+994:0:4644
+995:2:4458
+996:0:4644
+997:2:4459
+998:0:4644
+999:2:4464
+1000:0:4644
+1001:2:4465
+1002:0:4644
+1003:2:4473
+1004:2:4474
+1005:2:4478
+1006:2:4482
+1007:2:4483
+1008:2:4487
+1009:2:4495
+1010:2:4496
+1011:2:4500
+1012:2:4504
+1013:2:4505
+1014:2:4500
+1015:2:4504
+1016:2:4505
+1017:2:4509
+1018:2:4516
+1019:2:4523
+1020:2:4524
+1021:2:4531
+1022:2:4536
+1023:2:4543
+1024:2:4544
+1025:2:4543
+1026:2:4544
+1027:2:4551
+1028:2:4555
+1029:0:4644
+1030:2:3744
+1031:2:3754
+1032:0:4644
+1033:2:2882
+1034:0:4644
+1035:2:3745
+1036:2:3746
+1037:0:4644
+1038:2:2882
+1039:0:4644
+1040:2:3750
+1041:0:4644
+1042:2:3758
+1043:0:4644
+1044:2:2878
+1045:0:4644
+1046:2:2880
+1047:0:4644
+1048:2:2881
+1049:0:4644
+1050:2:2882
+1051:0:4644
+1052:2:2883
+1053:2:2884
+1054:2:2888
+1055:2:2889
+1056:2:2897
+1057:2:2898
+1058:2:2902
+1059:2:2903
+1060:2:2911
+1061:2:2916
+1062:2:2920
+1063:2:2921
+1064:2:2929
+1065:2:2930
+1066:2:2934
+1067:2:2935
+1068:2:2929
+1069:2:2930
+1070:2:2931
+1071:2:2943
+1072:2:2948
+1073:2:2949
+1074:2:2960
+1075:2:2961
+1076:2:2962
+1077:2:2973
+1078:2:2978
+1079:2:2979
+1080:2:2990
+1081:2:2991
+1082:2:2992
+1083:2:2990
+1084:2:2991
+1085:2:2992
+1086:2:3003
+1087:2:3011
+1088:0:4644
+1089:2:2882
+1090:0:4644
+1091:2:3063
+1092:2:3064
+1093:2:3065
+1094:0:4644
+1095:2:2882
+1096:0:4644
+1097:2:3070
+1098:0:4644
+1099:1:118
+1100:0:4644
+1101:1:120
+1102:0:4644
+1103:1:19
+1104:0:4644
+1105:1:126
+1106:1:127
+1107:1:131
+1108:1:132
+1109:1:140
+1110:1:141
+1111:1:145
+1112:1:146
+1113:1:154
+1114:1:159
+1115:1:163
+1116:1:164
+1117:1:172
+1118:1:173
+1119:1:177
+1120:1:178
+1121:1:172
+1122:1:173
+1123:1:177
+1124:1:178
+1125:1:186
+1126:1:191
+1127:1:192
+1128:1:203
+1129:1:204
+1130:1:205
+1131:1:216
+1132:1:221
+1133:1:222
+1134:1:233
+1135:1:234
+1136:1:235
+1137:1:233
+1138:1:234
+1139:1:235
+1140:1:246
+1141:0:4644
+1142:1:15
+1143:0:4644
+1144:1:16
+1145:0:4644
+1146:1:17
+1147:0:4644
+1148:1:118
+1149:0:4644
+1150:1:120
+1151:0:4644
+1152:1:19
+1153:0:4644
+1154:1:255
+1155:1:256
+1156:0:4644
+1157:1:15
+1158:0:4644
+1159:1:16
+1160:0:4644
+1161:1:17
+1162:0:4644
+1163:1:118
+1164:0:4644
+1165:1:120
+1166:0:4644
+1167:1:19
+1168:0:4644
+1169:1:262
+1170:1:263
+1171:1:267
+1172:1:268
+1173:1:276
+1174:1:277
+1175:1:281
+1176:1:282
+1177:1:290
+1178:1:295
+1179:1:299
+1180:1:300
+1181:1:308
+1182:1:309
+1183:1:313
+1184:1:314
+1185:1:308
+1186:1:309
+1187:1:313
+1188:1:314
+1189:1:322
+1190:1:327
+1191:1:328
+1192:1:339
+1193:1:340
+1194:1:341
+1195:1:352
+1196:1:357
+1197:1:358
+1198:1:369
+1199:1:370
+1200:1:371
+1201:1:369
+1202:1:370
+1203:1:371
+1204:1:382
+1205:0:4644
+1206:1:15
+1207:0:4644
+1208:1:16
+1209:0:4644
+1210:1:17
+1211:0:4644
+1212:1:118
+1213:0:4644
+1214:1:120
+1215:0:4644
+1216:1:19
+1217:0:4644
+1218:1:391
+1219:1:392
+1220:1:396
+1221:1:397
+1222:1:405
+1223:1:406
+1224:1:410
+1225:1:411
+1226:1:419
+1227:1:424
+1228:1:428
+1229:1:429
+1230:1:437
+1231:1:438
+1232:1:442
+1233:1:443
+1234:1:437
+1235:1:438
+1236:1:442
+1237:1:443
+1238:1:451
+1239:1:456
+1240:1:457
+1241:1:468
+1242:1:469
+1243:1:470
+1244:1:481
+1245:1:486
+1246:1:487
+1247:1:498
+1248:1:499
+1249:1:500
+1250:1:498
+1251:1:499
+1252:1:500
+1253:1:511
+1254:1:518
+1255:0:4644
+1256:1:15
+1257:0:4644
+1258:1:16
+1259:0:4644
+1260:1:17
+1261:0:4644
+1262:1:118
+1263:0:4644
+1264:1:120
+1265:0:4644
+1266:1:19
+1267:0:4644
+1268:1:656
+1269:1:657
+1270:1:661
+1271:1:662
+1272:1:670
+1273:1:671
+1274:1:672
+1275:1:684
+1276:1:689
+1277:1:693
+1278:1:694
+1279:1:702
+1280:1:703
+1281:1:707
+1282:1:708
+1283:1:702
+1284:1:703
+1285:1:707
+1286:1:708
+1287:1:716
+1288:1:721
+1289:1:722
+1290:1:733
+1291:1:734
+1292:1:735
+1293:1:746
+1294:1:751
+1295:1:752
+1296:1:763
+1297:1:764
+1298:1:765
+1299:1:763
+1300:1:764
+1301:1:765
+1302:1:776
+1303:0:4644
+1304:1:15
+1305:0:4644
+1306:1:16
+1307:0:4644
+1308:1:17
+1309:0:4644
+1310:1:118
+1311:0:4644
+1312:1:120
+1313:0:4644
+1314:1:19
+1315:0:4644
+1316:1:785
+1317:1:788
+1318:1:789
+1319:0:4644
+1320:1:15
+1321:0:4644
+1322:1:16
+1323:0:4644
+1324:1:17
+1325:0:4644
+1326:1:118
+1327:0:4644
+1328:1:120
+1329:0:4644
+1330:1:19
+1331:0:4644
+1332:1:1052
+1333:1:1053
+1334:1:1057
+1335:1:1058
+1336:1:1066
+1337:1:1067
+1338:1:1071
+1339:1:1072
+1340:1:1080
+1341:1:1085
+1342:1:1089
+1343:1:1090
+1344:1:1098
+1345:1:1099
+1346:1:1103
+1347:1:1104
+1348:1:1098
+1349:1:1099
+1350:1:1103
+1351:1:1104
+1352:1:1112
+1353:1:1117
+1354:1:1118
+1355:1:1129
+1356:1:1130
+1357:1:1131
+1358:1:1142
+1359:1:1147
+1360:1:1148
+1361:1:1159
+1362:1:1160
+1363:1:1161
+1364:1:1159
+1365:1:1160
+1366:1:1161
+1367:1:1172
+1368:1:1179
+1369:1:1183
+1370:0:4644
+1371:1:15
+1372:0:4644
+1373:1:16
+1374:0:4644
+1375:1:17
+1376:0:4644
+1377:1:118
+1378:0:4644
+1379:1:120
+1380:0:4644
+1381:1:19
+1382:0:4644
+1383:1:1184
+1384:1:1185
+1385:1:1189
+1386:1:1190
+1387:1:1198
+1388:1:1199
+1389:1:1200
+1390:1:1212
+1391:1:1217
+1392:1:1221
+1393:1:1222
+1394:1:1230
+1395:1:1231
+1396:1:1235
+1397:1:1236
+1398:1:1230
+1399:1:1231
+1400:1:1235
+1401:1:1236
+1402:1:1244
+1403:1:1249
+1404:1:1250
+1405:1:1261
+1406:1:1262
+1407:1:1263
+1408:1:1274
+1409:1:1279
+1410:1:1280
+1411:1:1291
+1412:1:1292
+1413:1:1293
+1414:1:1291
+1415:1:1292
+1416:1:1293
+1417:1:1304
+1418:0:4644
+1419:1:15
+1420:0:4644
+1421:1:16
+1422:0:4644
+1423:1:17
+1424:0:4644
+1425:1:118
+1426:0:4644
+1427:1:120
+1428:0:4644
+1429:1:19
+1430:0:4644
+1431:1:1313
+1432:0:4644
+1433:1:2777
+1434:1:2784
+1435:1:2785
+1436:1:2792
+1437:1:2797
+1438:1:2804
+1439:1:2805
+1440:1:2804
+1441:1:2805
+1442:1:2812
+1443:1:2816
+1444:0:4644
+1445:2:3773
+1446:2:3774
+1447:2:3778
+1448:2:3782
+1449:2:3783
+1450:2:3787
+1451:2:3792
+1452:2:3800
+1453:2:3804
+1454:2:3805
+1455:2:3800
+1456:2:3801
+1457:2:3809
+1458:2:3816
+1459:2:3823
+1460:2:3824
+1461:2:3831
+1462:2:3836
+1463:2:3843
+1464:2:3844
+1465:2:3843
+1466:2:3844
+1467:2:3851
+1468:2:3855
+1469:0:4644
+1470:2:3860
+1471:0:4644
+1472:2:3861
+1473:0:4644
+1474:2:3862
+1475:0:4644
+1476:2:3863
+1477:0:4644
+1478:1:1315
+1479:1:1316
+1480:0:4642
+1481:2:3864
+1482:0:4648
+1483:1:2474