Verification run #1, ipi and no-ipi results

[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
new file mode 100644 (file)
index 0000000..ad65225
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi/urcu_free_no_rmb.spin.input.trail
@@ -0,0 +1,1627 @@
+-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