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

diff --git a/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_rmb.spin.input.trail b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_rmb.spin.input.trail
new file mode 100644
index 0000000..abd4423
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_rmb.spin.input.trail
@@ -0,0 +1,1609 @@
+-2:3:-2
+-4:-4:-4
+1:0:4812
+2:3:4732
+3:3:4735
+4:3:4735
+5:3:4738
+6:3:4746
+7:3:4746
+8:3:4749
+9:3:4755
+10:3:4759
+11:3:4759
+12:3:4762
+13:3:4772
+14:3:4780
+15:3:4780
+16:3:4783
+17:3:4789
+18:3:4793
+19:3:4793
+20:3:4796
+21:3:4802
+22:3:4806
+23:3:4807
+24:0:4812
+25:3:4809
+26:0:4812
+27:2:3040
+28:0:4812
+29:2:3046
+30:0:4812
+31:2:3047
+32:0:4812
+33:2:3049
+34:0:4812
+35:2:3050
+36:0:4812
+37:2:3051
+38:2:3052
+39:2:3056
+40:2:3057
+41:2:3065
+42:2:3066
+43:2:3070
+44:2:3071
+45:2:3079
+46:2:3084
+47:2:3088
+48:2:3089
+49:2:3097
+50:2:3098
+51:2:3102
+52:2:3103
+53:2:3097
+54:2:3098
+55:2:3102
+56:2:3103
+57:2:3111
+58:2:3116
+59:2:3117
+60:2:3128
+61:2:3129
+62:2:3130
+63:2:3141
+64:2:3146
+65:2:3147
+66:2:3158
+67:2:3159
+68:2:3160
+69:2:3158
+70:2:3159
+71:2:3160
+72:2:3171
+73:2:3179
+74:0:4812
+75:2:3050
+76:0:4812
+77:2:3183
+78:2:3187
+79:2:3188
+80:2:3192
+81:2:3196
+82:2:3197
+83:2:3201
+84:2:3209
+85:2:3210
+86:2:3214
+87:2:3218
+88:2:3219
+89:2:3214
+90:2:3215
+91:2:3223
+92:0:4812
+93:2:3050
+94:0:4812
+95:2:3231
+96:2:3232
+97:2:3233
+98:0:4812
+99:2:3050
+100:0:4812
+101:2:3238
+102:0:4812
+103:2:3941
+104:2:3942
+105:2:3946
+106:2:3950
+107:2:3951
+108:2:3955
+109:2:3960
+110:2:3968
+111:2:3972
+112:2:3973
+113:2:3968
+114:2:3972
+115:2:3973
+116:2:3977
+117:2:3984
+118:2:3991
+119:2:3992
+120:2:3999
+121:2:4004
+122:2:4011
+123:2:4012
+124:2:4011
+125:2:4012
+126:2:4019
+127:2:4023
+128:0:4812
+129:2:4028
+130:0:4812
+131:2:4029
+132:0:4812
+133:2:4030
+134:0:4812
+135:2:4031
+136:0:4812
+137:1:2
+138:0:4812
+139:2:4032
+140:0:4812
+141:1:8
+142:0:4812
+143:1:9
+144:0:4812
+145:2:4031
+146:0:4812
+147:1:10
+148:0:4812
+149:2:4032
+150:0:4812
+151:1:11
+152:0:4812
+153:2:4031
+154:0:4812
+155:1:12
+156:0:4812
+157:2:4032
+158:0:4812
+159:1:13
+160:0:4812
+161:2:4031
+162:0:4812
+163:1:14
+164:0:4812
+165:2:4032
+166:0:4812
+167:1:15
+168:0:4812
+169:1:16
+170:0:4812
+171:2:4031
+172:0:4812
+173:1:17
+174:0:4812
+175:2:4032
+176:0:4812
+177:1:28
+178:0:4812
+179:2:4031
+180:0:4812
+181:1:32
+182:1:33
+183:1:37
+184:1:41
+185:1:42
+186:1:46
+187:1:54
+188:1:55
+189:1:59
+190:1:63
+191:1:64
+192:1:59
+193:1:63
+194:1:64
+195:1:68
+196:1:75
+197:1:82
+198:1:83
+199:1:90
+200:1:95
+201:1:102
+202:1:103
+203:1:102
+204:1:103
+205:1:110
+206:1:114
+207:0:4812
+208:2:4032
+209:0:4812
+210:1:119
+211:0:4812
+212:2:4033
+213:0:4812
+214:2:4038
+215:0:4812
+216:2:4039
+217:0:4812
+218:2:4047
+219:2:4048
+220:2:4052
+221:2:4056
+222:2:4057
+223:2:4061
+224:2:4069
+225:2:4070
+226:2:4074
+227:2:4078
+228:2:4079
+229:2:4074
+230:2:4078
+231:2:4079
+232:2:4083
+233:2:4090
+234:2:4097
+235:2:4098
+236:2:4105
+237:2:4110
+238:2:4117
+239:2:4118
+240:2:4117
+241:2:4118
+242:2:4125
+243:2:4129
+244:0:4812
+245:2:3240
+246:2:3922
+247:0:4812
+248:2:3050
+249:0:4812
+250:2:3241
+251:0:4812
+252:2:3050
+253:0:4812
+254:2:3244
+255:2:3245
+256:2:3249
+257:2:3250
+258:2:3258
+259:2:3259
+260:2:3263
+261:2:3264
+262:2:3272
+263:2:3277
+264:2:3281
+265:2:3282
+266:2:3290
+267:2:3291
+268:2:3295
+269:2:3296
+270:2:3290
+271:2:3291
+272:2:3295
+273:2:3296
+274:2:3304
+275:2:3309
+276:2:3310
+277:2:3321
+278:2:3322
+279:2:3323
+280:2:3334
+281:2:3339
+282:2:3340
+283:2:3351
+284:2:3352
+285:2:3353
+286:2:3351
+287:2:3352
+288:2:3353
+289:2:3364
+290:2:3371
+291:0:4812
+292:2:3050
+293:0:4812
+294:2:3375
+295:2:3376
+296:2:3377
+297:2:3389
+298:2:3390
+299:2:3394
+300:2:3395
+301:2:3403
+302:2:3408
+303:2:3412
+304:2:3413
+305:2:3421
+306:2:3422
+307:2:3426
+308:2:3427
+309:2:3421
+310:2:3422
+311:2:3426
+312:2:3427
+313:2:3435
+314:2:3440
+315:2:3441
+316:2:3452
+317:2:3453
+318:2:3454
+319:2:3465
+320:2:3470
+321:2:3471
+322:2:3482
+323:2:3483
+324:2:3484
+325:2:3482
+326:2:3483
+327:2:3484
+328:2:3495
+329:2:3506
+330:2:3507
+331:0:4812
+332:2:3050
+333:0:4812
+334:2:3513
+335:2:3514
+336:2:3518
+337:2:3519
+338:2:3527
+339:2:3528
+340:2:3532
+341:2:3533
+342:2:3541
+343:2:3546
+344:2:3550
+345:2:3551
+346:2:3559
+347:2:3560
+348:2:3564
+349:2:3565
+350:2:3559
+351:2:3560
+352:2:3564
+353:2:3565
+354:2:3573
+355:2:3578
+356:2:3579
+357:2:3590
+358:2:3591
+359:2:3592
+360:2:3603
+361:2:3608
+362:2:3609
+363:2:3620
+364:2:3621
+365:2:3622
+366:2:3620
+367:2:3621
+368:2:3622
+369:2:3633
+370:0:4812
+371:2:3050
+372:0:4812
+373:2:3642
+374:2:3643
+375:2:3647
+376:2:3648
+377:2:3656
+378:2:3657
+379:2:3661
+380:2:3662
+381:2:3670
+382:2:3675
+383:2:3679
+384:2:3680
+385:2:3688
+386:2:3689
+387:2:3693
+388:2:3694
+389:2:3688
+390:2:3689
+391:2:3693
+392:2:3694
+393:2:3702
+394:2:3707
+395:2:3708
+396:2:3719
+397:2:3720
+398:2:3721
+399:2:3732
+400:2:3737
+401:2:3738
+402:2:3749
+403:2:3750
+404:2:3751
+405:2:3749
+406:2:3750
+407:2:3751
+408:2:3762
+409:2:3769
+410:0:4812
+411:2:3050
+412:0:4812
+413:2:3773
+414:2:3774
+415:2:3775
+416:2:3787
+417:2:3788
+418:2:3792
+419:2:3793
+420:2:3801
+421:2:3806
+422:2:3810
+423:2:3811
+424:2:3819
+425:2:3820
+426:2:3824
+427:2:3825
+428:2:3819
+429:2:3820
+430:2:3824
+431:2:3825
+432:2:3833
+433:2:3838
+434:2:3839
+435:2:3850
+436:2:3851
+437:2:3852
+438:2:3863
+439:2:3868
+440:2:3869
+441:2:3880
+442:2:3881
+443:2:3882
+444:2:3880
+445:2:3881
+446:2:3882
+447:2:3893
+448:2:3903
+449:2:3904
+450:0:4812
+451:2:3050
+452:0:4812
+453:2:3910
+454:0:4812
+455:2:4535
+456:2:4536
+457:2:4540
+458:2:4544
+459:2:4545
+460:2:4549
+461:2:4557
+462:2:4558
+463:2:4562
+464:2:4566
+465:2:4567
+466:2:4562
+467:2:4566
+468:2:4567
+469:2:4571
+470:2:4578
+471:2:4585
+472:2:4586
+473:2:4593
+474:2:4598
+475:2:4605
+476:2:4606
+477:2:4605
+478:2:4606
+479:2:4613
+480:2:4617
+481:0:4812
+482:2:4622
+483:0:4812
+484:2:4623
+485:0:4812
+486:2:4624
+487:0:4812
+488:2:4625
+489:0:4812
+490:1:28
+491:0:4812
+492:2:4626
+493:0:4812
+494:1:32
+495:1:33
+496:1:37
+497:1:41
+498:1:42
+499:1:46
+500:1:54
+501:1:55
+502:1:59
+503:1:63
+504:1:64
+505:1:59
+506:1:63
+507:1:64
+508:1:68
+509:1:75
+510:1:82
+511:1:83
+512:1:90
+513:1:95
+514:1:102
+515:1:103
+516:1:102
+517:1:103
+518:1:110
+519:1:114
+520:0:4812
+521:2:4625
+522:0:4812
+523:1:119
+524:0:4812
+525:2:4626
+526:0:4812
+527:2:4627
+528:0:4812
+529:2:4632
+530:0:4812
+531:2:4633
+532:0:4812
+533:2:4641
+534:2:4642
+535:2:4646
+536:2:4650
+537:2:4651
+538:2:4655
+539:2:4663
+540:2:4664
+541:2:4668
+542:2:4672
+543:2:4673
+544:2:4668
+545:2:4672
+546:2:4673
+547:2:4677
+548:2:4684
+549:2:4691
+550:2:4692
+551:2:4699
+552:2:4704
+553:2:4711
+554:2:4712
+555:2:4711
+556:2:4712
+557:2:4719
+558:2:4723
+559:0:4812
+560:2:3912
+561:2:3922
+562:0:4812
+563:2:3050
+564:0:4812
+565:2:3913
+566:2:3914
+567:0:4812
+568:2:3050
+569:0:4812
+570:2:3918
+571:0:4812
+572:2:3926
+573:0:4812
+574:2:3047
+575:0:4812
+576:2:3049
+577:0:4812
+578:2:3050
+579:0:4812
+580:2:3051
+581:2:3052
+582:2:3056
+583:2:3057
+584:2:3065
+585:2:3066
+586:2:3070
+587:2:3071
+588:2:3079
+589:2:3084
+590:2:3088
+591:2:3089
+592:2:3097
+593:2:3098
+594:2:3099
+595:2:3097
+596:2:3098
+597:2:3102
+598:2:3103
+599:2:3111
+600:2:3116
+601:2:3117
+602:2:3128
+603:2:3129
+604:2:3130
+605:2:3141
+606:2:3146
+607:2:3147
+608:2:3158
+609:2:3159
+610:2:3160
+611:2:3158
+612:2:3159
+613:2:3160
+614:2:3171
+615:2:3179
+616:0:4812
+617:2:3050
+618:0:4812
+619:2:3183
+620:2:3187
+621:2:3188
+622:2:3192
+623:2:3196
+624:2:3197
+625:2:3201
+626:2:3209
+627:2:3210
+628:2:3214
+629:2:3215
+630:2:3214
+631:2:3218
+632:2:3219
+633:2:3223
+634:0:4812
+635:2:3050
+636:0:4812
+637:2:3231
+638:2:3232
+639:2:3233
+640:0:4812
+641:2:3050
+642:0:4812
+643:2:3238
+644:0:4812
+645:2:3941
+646:2:3942
+647:2:3946
+648:2:3950
+649:2:3951
+650:2:3955
+651:2:3960
+652:2:3968
+653:2:3972
+654:2:3973
+655:2:3968
+656:2:3972
+657:2:3973
+658:2:3977
+659:2:3984
+660:2:3991
+661:2:3992
+662:2:3999
+663:2:4004
+664:2:4011
+665:2:4012
+666:2:4011
+667:2:4012
+668:2:4019
+669:2:4023
+670:0:4812
+671:2:4028
+672:0:4812
+673:2:4029
+674:0:4812
+675:2:4030
+676:0:4812
+677:2:4031
+678:0:4812
+679:1:28
+680:0:4812
+681:2:4032
+682:0:4812
+683:1:32
+684:1:33
+685:1:37
+686:1:41
+687:1:42
+688:1:46
+689:1:54
+690:1:55
+691:1:59
+692:1:63
+693:1:64
+694:1:59
+695:1:63
+696:1:64
+697:1:68
+698:1:75
+699:1:82
+700:1:83
+701:1:90
+702:1:95
+703:1:102
+704:1:103
+705:1:102
+706:1:103
+707:1:110
+708:1:114
+709:0:4812
+710:2:4031
+711:0:4812
+712:1:119
+713:0:4812
+714:2:4032
+715:0:4812
+716:2:4033
+717:0:4812
+718:2:4038
+719:0:4812
+720:2:4039
+721:0:4812
+722:2:4047
+723:2:4048
+724:2:4052
+725:2:4056
+726:2:4057
+727:2:4061
+728:2:4069
+729:2:4070
+730:2:4074
+731:2:4078
+732:2:4079
+733:2:4074
+734:2:4078
+735:2:4079
+736:2:4083
+737:2:4090
+738:2:4097
+739:2:4098
+740:2:4105
+741:2:4110
+742:2:4117
+743:2:4118
+744:2:4117
+745:2:4118
+746:2:4125
+747:2:4129
+748:0:4812
+749:2:3240
+750:2:3922
+751:0:4812
+752:2:3050
+753:0:4812
+754:2:3241
+755:0:4812
+756:2:3050
+757:0:4812
+758:2:3244
+759:2:3245
+760:2:3249
+761:2:3250
+762:2:3258
+763:2:3259
+764:2:3263
+765:2:3264
+766:2:3272
+767:2:3277
+768:2:3281
+769:2:3282
+770:2:3290
+771:2:3291
+772:2:3295
+773:2:3296
+774:2:3290
+775:2:3291
+776:2:3295
+777:2:3296
+778:2:3304
+779:2:3309
+780:2:3310
+781:2:3321
+782:2:3322
+783:2:3323
+784:2:3334
+785:2:3339
+786:2:3340
+787:2:3351
+788:2:3352
+789:2:3353
+790:2:3351
+791:2:3352
+792:2:3353
+793:2:3364
+794:2:3371
+795:0:4812
+796:2:3050
+797:0:4812
+798:2:3375
+799:2:3376
+800:2:3377
+801:2:3389
+802:2:3390
+803:2:3394
+804:2:3395
+805:2:3403
+806:2:3408
+807:2:3412
+808:2:3413
+809:2:3421
+810:2:3422
+811:2:3426
+812:2:3427
+813:2:3421
+814:2:3422
+815:2:3426
+816:2:3427
+817:2:3435
+818:2:3440
+819:2:3441
+820:2:3452
+821:2:3453
+822:2:3454
+823:2:3465
+824:2:3470
+825:2:3471
+826:2:3482
+827:2:3483
+828:2:3484
+829:2:3482
+830:2:3483
+831:2:3484
+832:2:3495
+833:2:3506
+834:2:3507
+835:0:4812
+836:2:3050
+837:0:4812
+838:2:3513
+839:2:3514
+840:2:3518
+841:2:3519
+842:2:3527
+843:2:3528
+844:2:3532
+845:2:3533
+846:2:3541
+847:2:3546
+848:2:3550
+849:2:3551
+850:2:3559
+851:2:3560
+852:2:3564
+853:2:3565
+854:2:3559
+855:2:3560
+856:2:3564
+857:2:3565
+858:2:3573
+859:2:3578
+860:2:3579
+861:2:3590
+862:2:3591
+863:2:3592
+864:2:3603
+865:2:3608
+866:2:3609
+867:2:3620
+868:2:3621
+869:2:3622
+870:2:3620
+871:2:3621
+872:2:3622
+873:2:3633
+874:0:4812
+875:2:3050
+876:0:4812
+877:2:3642
+878:2:3643
+879:2:3647
+880:2:3648
+881:2:3656
+882:2:3657
+883:2:3661
+884:2:3662
+885:2:3670
+886:2:3675
+887:2:3679
+888:2:3680
+889:2:3688
+890:2:3689
+891:2:3693
+892:2:3694
+893:2:3688
+894:2:3689
+895:2:3693
+896:2:3694
+897:2:3702
+898:2:3707
+899:2:3708
+900:2:3719
+901:2:3720
+902:2:3721
+903:2:3732
+904:2:3737
+905:2:3738
+906:2:3749
+907:2:3750
+908:2:3751
+909:2:3749
+910:2:3750
+911:2:3751
+912:2:3762
+913:2:3769
+914:0:4812
+915:2:3050
+916:0:4812
+917:2:3773
+918:2:3774
+919:2:3775
+920:2:3787
+921:2:3788
+922:2:3792
+923:2:3793
+924:2:3801
+925:2:3806
+926:2:3810
+927:2:3811
+928:2:3819
+929:2:3820
+930:2:3824
+931:2:3825
+932:2:3819
+933:2:3820
+934:2:3824
+935:2:3825
+936:2:3833
+937:2:3838
+938:2:3839
+939:2:3850
+940:2:3851
+941:2:3852
+942:2:3863
+943:2:3868
+944:2:3869
+945:2:3880
+946:2:3881
+947:2:3882
+948:2:3880
+949:2:3881
+950:2:3882
+951:2:3893
+952:2:3903
+953:2:3904
+954:0:4812
+955:2:3050
+956:0:4812
+957:2:3910
+958:0:4812
+959:2:4535
+960:2:4536
+961:2:4540
+962:2:4544
+963:2:4545
+964:2:4549
+965:2:4557
+966:2:4558
+967:2:4562
+968:2:4566
+969:2:4567
+970:2:4562
+971:2:4566
+972:2:4567
+973:2:4571
+974:2:4578
+975:2:4585
+976:2:4586
+977:2:4593
+978:2:4598
+979:2:4605
+980:2:4606
+981:2:4605
+982:2:4606
+983:2:4613
+984:2:4617
+985:0:4812
+986:2:4622
+987:0:4812
+988:2:4623
+989:0:4812
+990:2:4624
+991:0:4812
+992:2:4625
+993:0:4812
+994:1:28
+995:0:4812
+996:2:4626
+997:0:4812
+998:1:32
+999:1:33
+1000:1:37
+1001:1:41
+1002:1:42
+1003:1:46
+1004:1:54
+1005:1:55
+1006:1:59
+1007:1:63
+1008:1:64
+1009:1:59
+1010:1:63
+1011:1:64
+1012:1:68
+1013:1:75
+1014:1:82
+1015:1:83
+1016:1:90
+1017:1:95
+1018:1:102
+1019:1:103
+1020:1:102
+1021:1:103
+1022:1:110
+1023:1:114
+1024:0:4812
+1025:2:4625
+1026:0:4812
+1027:1:119
+1028:0:4812
+1029:2:4626
+1030:0:4812
+1031:2:4627
+1032:0:4812
+1033:2:4632
+1034:0:4812
+1035:2:4633
+1036:0:4812
+1037:2:4641
+1038:2:4642
+1039:2:4646
+1040:2:4650
+1041:2:4651
+1042:2:4655
+1043:2:4663
+1044:2:4664
+1045:2:4668
+1046:2:4672
+1047:2:4673
+1048:2:4668
+1049:2:4672
+1050:2:4673
+1051:2:4677
+1052:2:4684
+1053:2:4691
+1054:2:4692
+1055:2:4699
+1056:2:4704
+1057:2:4711
+1058:2:4712
+1059:2:4711
+1060:2:4712
+1061:2:4719
+1062:2:4723
+1063:0:4812
+1064:2:3912
+1065:2:3922
+1066:0:4812
+1067:2:3050
+1068:0:4812
+1069:2:3913
+1070:2:3914
+1071:0:4812
+1072:2:3050
+1073:0:4812
+1074:2:3918
+1075:0:4812
+1076:2:3926
+1077:0:4812
+1078:2:3047
+1079:0:4812
+1080:2:3049
+1081:0:4812
+1082:2:3050
+1083:0:4812
+1084:2:3051
+1085:2:3052
+1086:2:3056
+1087:2:3057
+1088:2:3065
+1089:2:3066
+1090:2:3070
+1091:2:3071
+1092:2:3079
+1093:2:3084
+1094:2:3088
+1095:2:3089
+1096:2:3097
+1097:2:3098
+1098:2:3102
+1099:2:3103
+1100:2:3097
+1101:2:3098
+1102:2:3099
+1103:2:3111
+1104:2:3116
+1105:2:3117
+1106:2:3128
+1107:2:3129
+1108:2:3130
+1109:2:3141
+1110:2:3146
+1111:2:3147
+1112:2:3158
+1113:2:3159
+1114:2:3160
+1115:2:3158
+1116:2:3159
+1117:2:3160
+1118:2:3171
+1119:2:3179
+1120:0:4812
+1121:2:3050
+1122:0:4812
+1123:1:120
+1124:0:4812
+1125:1:19
+1126:0:4812
+1127:1:127
+1128:1:128
+1129:1:132
+1130:1:133
+1131:1:141
+1132:1:142
+1133:1:146
+1134:1:147
+1135:1:155
+1136:1:160
+1137:1:164
+1138:1:165
+1139:1:173
+1140:1:174
+1141:1:178
+1142:1:179
+1143:1:173
+1144:1:174
+1145:1:178
+1146:1:179
+1147:1:187
+1148:1:192
+1149:1:193
+1150:1:204
+1151:1:205
+1152:1:206
+1153:1:217
+1154:1:222
+1155:1:223
+1156:1:234
+1157:1:235
+1158:1:236
+1159:1:234
+1160:1:235
+1161:1:236
+1162:1:247
+1163:0:4812
+1164:1:15
+1165:0:4812
+1166:1:16
+1167:0:4812
+1168:2:3183
+1169:2:3187
+1170:2:3188
+1171:2:3192
+1172:2:3196
+1173:2:3197
+1174:2:3201
+1175:2:3209
+1176:2:3210
+1177:2:3214
+1178:2:3218
+1179:2:3219
+1180:2:3214
+1181:2:3215
+1182:2:3223
+1183:0:4812
+1184:2:3050
+1185:0:4812
+1186:2:3231
+1187:2:3232
+1188:2:3233
+1189:0:4812
+1190:2:3050
+1191:0:4812
+1192:2:3238
+1193:0:4812
+1194:2:3941
+1195:2:3942
+1196:2:3946
+1197:2:3950
+1198:2:3951
+1199:2:3955
+1200:2:3960
+1201:2:3968
+1202:2:3972
+1203:2:3973
+1204:2:3968
+1205:2:3972
+1206:2:3973
+1207:2:3977
+1208:2:3984
+1209:2:3991
+1210:2:3992
+1211:2:3999
+1212:2:4004
+1213:2:4011
+1214:2:4012
+1215:2:4011
+1216:2:4012
+1217:2:4019
+1218:2:4023
+1219:0:4812
+1220:2:4028
+1221:0:4812
+1222:2:4029
+1223:0:4812
+1224:2:4030
+1225:0:4812
+1226:2:4031
+1227:0:4812
+1228:1:17
+1229:0:4812
+1230:2:4032
+1231:0:4812
+1232:1:120
+1233:0:4812
+1234:2:4031
+1235:0:4812
+1236:1:19
+1237:0:4812
+1238:2:4032
+1239:0:4812
+1240:1:256
+1241:1:257
+1242:0:4812
+1243:1:15
+1244:0:4812
+1245:1:16
+1246:0:4812
+1247:2:4031
+1248:0:4812
+1249:1:17
+1250:0:4812
+1251:2:4032
+1252:0:4812
+1253:1:120
+1254:0:4812
+1255:2:4031
+1256:0:4812
+1257:1:19
+1258:0:4812
+1259:2:4032
+1260:0:4812
+1261:1:263
+1262:1:264
+1263:1:268
+1264:1:269
+1265:1:277
+1266:1:278
+1267:1:282
+1268:1:283
+1269:1:291
+1270:1:296
+1271:1:300
+1272:1:301
+1273:1:309
+1274:1:310
+1275:1:314
+1276:1:315
+1277:1:309
+1278:1:310
+1279:1:314
+1280:1:315
+1281:1:323
+1282:1:328
+1283:1:329
+1284:1:340
+1285:1:341
+1286:1:342
+1287:1:353
+1288:1:358
+1289:1:359
+1290:1:370
+1291:1:371
+1292:1:372
+1293:1:370
+1294:1:378
+1295:1:379
+1296:1:383
+1297:0:4812
+1298:1:15
+1299:0:4812
+1300:1:16
+1301:0:4812
+1302:2:4031
+1303:0:4812
+1304:1:17
+1305:0:4812
+1306:2:4032
+1307:0:4812
+1308:1:120
+1309:0:4812
+1310:2:4031
+1311:0:4812
+1312:1:19
+1313:0:4812
+1314:2:4032
+1315:0:4812
+1316:1:392
+1317:1:393
+1318:1:397
+1319:1:398
+1320:1:406
+1321:1:407
+1322:1:411
+1323:1:412
+1324:1:420
+1325:1:425
+1326:1:429
+1327:1:430
+1328:1:438
+1329:1:439
+1330:1:443
+1331:1:444
+1332:1:438
+1333:1:439
+1334:1:443
+1335:1:444
+1336:1:452
+1337:1:457
+1338:1:458
+1339:1:469
+1340:1:470
+1341:1:471
+1342:1:482
+1343:1:487
+1344:1:488
+1345:1:499
+1346:1:500
+1347:1:501
+1348:1:499
+1349:1:507
+1350:1:508
+1351:1:512
+1352:1:519
+1353:0:4812
+1354:1:15
+1355:0:4812
+1356:1:16
+1357:0:4812
+1358:2:4031
+1359:0:4812
+1360:1:17
+1361:0:4812
+1362:2:4032
+1363:0:4812
+1364:1:120
+1365:0:4812
+1366:2:4031
+1367:0:4812
+1368:1:19
+1369:0:4812
+1370:2:4032
+1371:0:4812
+1372:1:657
+1373:1:658
+1374:1:662
+1375:1:663
+1376:1:671
+1377:1:672
+1378:1:673
+1379:1:685
+1380:1:690
+1381:1:694
+1382:1:695
+1383:1:703
+1384:1:704
+1385:1:708
+1386:1:709
+1387:1:703
+1388:1:704
+1389:1:708
+1390:1:709
+1391:1:717
+1392:1:722
+1393:1:723
+1394:1:734
+1395:1:735
+1396:1:736
+1397:1:747
+1398:1:752
+1399:1:753
+1400:1:764
+1401:1:765
+1402:1:766
+1403:1:764
+1404:1:772
+1405:1:773
+1406:1:777
+1407:0:4812
+1408:1:15
+1409:0:4812
+1410:1:16
+1411:0:4812
+1412:2:4031
+1413:0:4812
+1414:1:17
+1415:0:4812
+1416:2:4032
+1417:0:4812
+1418:1:120
+1419:0:4812
+1420:2:4031
+1421:0:4812
+1422:1:19
+1423:0:4812
+1424:2:4032
+1425:0:4812
+1426:1:786
+1427:1:789
+1428:1:790
+1429:0:4812
+1430:1:15
+1431:0:4812
+1432:1:16
+1433:0:4812
+1434:2:4031
+1435:0:4812
+1436:1:17
+1437:0:4812
+1438:2:4032
+1439:0:4812
+1440:1:120
+1441:0:4812
+1442:2:4031
+1443:0:4812
+1444:1:19
+1445:0:4812
+1446:2:4032
+1447:0:4812
+1448:1:1053
+1449:1:1054
+1450:1:1058
+1451:1:1059
+1452:1:1067
+1453:1:1068
+1454:1:1072
+1455:1:1073
+1456:1:1081
+1457:1:1086
+1458:1:1090
+1459:1:1091
+1460:1:1099
+1461:1:1100
+1462:1:1104
+1463:1:1105
+1464:1:1099
+1465:1:1100
+1466:1:1104
+1467:1:1105
+1468:1:1113
+1469:1:1118
+1470:1:1119
+1471:1:1130
+1472:1:1131
+1473:1:1132
+1474:1:1143
+1475:1:1148
+1476:1:1149
+1477:1:1160
+1478:1:1161
+1479:1:1162
+1480:1:1160
+1481:1:1168
+1482:1:1169
+1483:1:1173
+1484:1:1180
+1485:1:1184
+1486:0:4812
+1487:1:15
+1488:0:4812
+1489:1:16
+1490:0:4812
+1491:2:4031
+1492:0:4812
+1493:1:17
+1494:0:4812
+1495:2:4032
+1496:0:4812
+1497:1:120
+1498:0:4812
+1499:2:4031
+1500:0:4812
+1501:1:19
+1502:0:4812
+1503:2:4032
+1504:0:4812
+1505:1:1185
+1506:1:1186
+1507:1:1190
+1508:1:1191
+1509:1:1199
+1510:1:1200
+1511:1:1201
+1512:1:1213
+1513:1:1218
+1514:1:1222
+1515:1:1223
+1516:1:1231
+1517:1:1232
+1518:1:1236
+1519:1:1237
+1520:1:1231
+1521:1:1232
+1522:1:1236
+1523:1:1237
+1524:1:1245
+1525:1:1250
+1526:1:1251
+1527:1:1262
+1528:1:1263
+1529:1:1264
+1530:1:1275
+1531:1:1280
+1532:1:1281
+1533:1:1292
+1534:1:1293
+1535:1:1294
+1536:1:1292
+1537:1:1300
+1538:1:1301
+1539:1:1305
+1540:0:4812
+1541:1:15
+1542:0:4812
+1543:1:16
+1544:0:4812
+1545:2:4031
+1546:0:4812
+1547:1:17
+1548:0:4812
+1549:2:4032
+1550:0:4812
+1551:1:120
+1552:0:4812
+1553:2:4031
+1554:0:4812
+1555:1:19
+1556:0:4812
+1557:2:4032
+1558:0:4812
+1559:1:1314
+1560:0:4812
+1561:2:4031
+1562:0:4812
+1563:1:2778
+1564:1:2782
+1565:1:2783
+1566:1:2791
+1567:1:2792
+1568:1:2796
+1569:1:2797
+1570:1:2805
+1571:1:2810
+1572:1:2814
+1573:1:2815
+1574:1:2823
+1575:1:2824
+1576:1:2828
+1577:1:2829
+1578:1:2823
+1579:1:2824
+1580:1:2828
+1581:1:2829
+1582:1:2837
+1583:1:2842
+1584:1:2843
+1585:1:2854
+1586:1:2855
+1587:1:2856
+1588:1:2867
+1589:1:2872
+1590:1:2873
+1591:1:2884
+1592:1:2885
+1593:1:2886
+1594:1:2884
+1595:1:2892
+1596:1:2893
+1597:1:2897
+1598:1:2901
+1599:0:4812
+1600:2:4032
+1601:0:4812
+1602:1:1316
+1603:1:1317
+1604:0:4810
+1605:1:15
+1606:0:4816
+1607:1:1637