Verification run #1, ipi and no-ipi results

[urcu.git] / formal-model / results / urcu-controldataflow-ipi / urcu_progress_reader.spin.input.trail

diff --git a/formal-model/results/urcu-controldataflow-ipi/urcu_progress_reader.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi/urcu_progress_reader.spin.input.trail
new file mode 100644 (file)
index 0000000..a0cf98c
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi/urcu_progress_reader.spin.input.trail
@@ -0,0 +1,1767 @@
+-2:3:-2
+-4:-4:-4
+1:0:4840
+2:3:4760
+3:3:4763
+4:3:4763
+5:3:4766
+6:3:4774
+7:3:4774
+8:3:4777
+9:3:4783
+10:3:4787
+11:3:4787
+12:3:4790
+13:3:4800
+14:3:4808
+15:3:4808
+16:3:4811
+17:3:4817
+18:3:4821
+19:3:4821
+20:3:4824
+21:3:4830
+22:3:4834
+23:3:4835
+24:0:4840
+25:3:4837
+26:0:4840
+27:2:2871
+28:0:4840
+29:2:2877
+30:0:4840
+31:2:2878
+32:0:4840
+33:2:2880
+34:0:4840
+35:2:2881
+36:0:4840
+37:2:2882
+38:2:2883
+39:2:2887
+40:2:2888
+41:2:2896
+42:2:2897
+43:2:2901
+44:2:2902
+45:2:2910
+46:2:2915
+47:2:2919
+48:2:2920
+49:2:2928
+50:2:2929
+51:2:2933
+52:2:2934
+53:2:2928
+54:2:2929
+55:2:2933
+56:2:2934
+57:2:2942
+58:2:2947
+59:2:2948
+60:2:2959
+61:2:2960
+62:2:2961
+63:2:2972
+64:2:2977
+65:2:2978
+66:2:2989
+67:2:2990
+68:2:2991
+69:2:2989
+70:2:2990
+71:2:2991
+72:2:3002
+73:2:3010
+74:0:4840
+75:2:2881
+76:0:4840
+77:2:3014
+78:2:3018
+79:2:3019
+80:2:3023
+81:2:3027
+82:2:3028
+83:2:3032
+84:2:3040
+85:2:3041
+86:2:3045
+87:2:3049
+88:2:3050
+89:2:3045
+90:2:3046
+91:2:3054
+92:0:4840
+93:2:2881
+94:0:4840
+95:2:3062
+96:2:3063
+97:2:3064
+98:0:4840
+99:2:2881
+100:0:4840
+101:2:3069
+102:0:4840
+103:2:3969
+104:2:3970
+105:2:3974
+106:2:3978
+107:2:3979
+108:2:3983
+109:2:3988
+110:2:3996
+111:2:4000
+112:2:4001
+113:2:3996
+114:2:4000
+115:2:4001
+116:2:4005
+117:2:4012
+118:2:4019
+119:2:4020
+120:2:4027
+121:2:4032
+122:2:4039
+123:2:4040
+124:2:4039
+125:2:4040
+126:2:4047
+127:2:4051
+128:0:4840
+129:2:4056
+130:0:4840
+131:2:4057
+132:0:4840
+133:2:4058
+134:0:4840
+135:2:4059
+136:0:4840
+137:1:2
+138:0:4840
+139:1:8
+140:0:4840
+141:2:4060
+142:0:4840
+143:1:9
+144:0:4840
+145:2:4059
+146:0:4840
+147:1:10
+148:0:4840
+149:2:4060
+150:0:4838
+151:1:11
+152:0:4844
+153:1:12
+154:0:4844
+155:1:13
+156:0:4844
+157:1:14
+158:0:4844
+159:1:15
+160:0:4844
+161:1:16
+162:0:4844
+163:1:17
+164:0:4844
+165:1:26
+166:0:4844
+167:1:30
+168:1:31
+169:1:35
+170:1:39
+171:1:40
+172:1:44
+173:1:52
+174:1:53
+175:1:57
+176:1:61
+177:1:62
+178:1:57
+179:1:61
+180:1:62
+181:1:66
+182:1:73
+183:1:80
+184:1:81
+185:1:88
+186:1:93
+187:1:100
+188:1:101
+189:1:100
+190:1:101
+191:1:108
+192:1:112
+193:0:4844
+194:1:117
+195:0:4844
+196:2:4061
+197:0:4844
+198:2:4066
+199:0:4844
+200:2:4067
+201:0:4844
+202:2:4075
+203:2:4076
+204:2:4080
+205:2:4084
+206:2:4085
+207:2:4089
+208:2:4097
+209:2:4098
+210:2:4102
+211:2:4106
+212:2:4107
+213:2:4102
+214:2:4106
+215:2:4107
+216:2:4111
+217:2:4118
+218:2:4125
+219:2:4126
+220:2:4133
+221:2:4138
+222:2:4145
+223:2:4146
+224:2:4145
+225:2:4146
+226:2:4153
+227:2:4157
+228:0:4844
+229:2:3071
+230:2:3753
+231:0:4844
+232:2:2881
+233:0:4844
+234:2:3072
+235:0:4844
+236:2:2881
+237:0:4844
+238:2:3075
+239:2:3076
+240:2:3080
+241:2:3081
+242:2:3089
+243:2:3090
+244:2:3094
+245:2:3095
+246:2:3103
+247:2:3108
+248:2:3112
+249:2:3113
+250:2:3121
+251:2:3122
+252:2:3126
+253:2:3127
+254:2:3121
+255:2:3122
+256:2:3126
+257:2:3127
+258:2:3135
+259:2:3140
+260:2:3141
+261:2:3152
+262:2:3153
+263:2:3154
+264:2:3165
+265:2:3170
+266:2:3171
+267:2:3182
+268:2:3183
+269:2:3184
+270:2:3182
+271:2:3183
+272:2:3184
+273:2:3195
+274:2:3202
+275:0:4844
+276:2:2881
+277:0:4844
+278:2:3206
+279:2:3207
+280:2:3208
+281:2:3220
+282:2:3221
+283:2:3225
+284:2:3226
+285:2:3234
+286:2:3239
+287:2:3243
+288:2:3244
+289:2:3252
+290:2:3253
+291:2:3257
+292:2:3258
+293:2:3252
+294:2:3253
+295:2:3257
+296:2:3258
+297:2:3266
+298:2:3271
+299:2:3272
+300:2:3283
+301:2:3284
+302:2:3285
+303:2:3296
+304:2:3301
+305:2:3302
+306:2:3313
+307:2:3314
+308:2:3315
+309:2:3313
+310:2:3314
+311:2:3315
+312:2:3326
+313:2:3337
+314:2:3338
+315:0:4844
+316:2:2881
+317:0:4844
+318:2:3344
+319:2:3345
+320:2:3349
+321:2:3350
+322:2:3358
+323:2:3359
+324:2:3363
+325:2:3364
+326:2:3372
+327:2:3377
+328:2:3381
+329:2:3382
+330:2:3390
+331:2:3391
+332:2:3395
+333:2:3396
+334:2:3390
+335:2:3391
+336:2:3395
+337:2:3396
+338:2:3404
+339:2:3409
+340:2:3410
+341:2:3421
+342:2:3422
+343:2:3423
+344:2:3434
+345:2:3439
+346:2:3440
+347:2:3451
+348:2:3452
+349:2:3453
+350:2:3451
+351:2:3452
+352:2:3453
+353:2:3464
+354:0:4844
+355:2:2881
+356:0:4844
+357:2:3473
+358:2:3474
+359:2:3478
+360:2:3479
+361:2:3487
+362:2:3488
+363:2:3492
+364:2:3493
+365:2:3501
+366:2:3506
+367:2:3510
+368:2:3511
+369:2:3519
+370:2:3520
+371:2:3524
+372:2:3525
+373:2:3519
+374:2:3520
+375:2:3524
+376:2:3525
+377:2:3533
+378:2:3538
+379:2:3539
+380:2:3550
+381:2:3551
+382:2:3552
+383:2:3563
+384:2:3568
+385:2:3569
+386:2:3580
+387:2:3581
+388:2:3582
+389:2:3580
+390:2:3581
+391:2:3582
+392:2:3593
+393:2:3600
+394:0:4844
+395:2:2881
+396:0:4844
+397:2:3604
+398:2:3605
+399:2:3606
+400:2:3618
+401:2:3619
+402:2:3623
+403:2:3624
+404:2:3632
+405:2:3637
+406:2:3641
+407:2:3642
+408:2:3650
+409:2:3651
+410:2:3655
+411:2:3656
+412:2:3650
+413:2:3651
+414:2:3655
+415:2:3656
+416:2:3664
+417:2:3669
+418:2:3670
+419:2:3681
+420:2:3682
+421:2:3683
+422:2:3694
+423:2:3699
+424:2:3700
+425:2:3711
+426:2:3712
+427:2:3713
+428:2:3711
+429:2:3712
+430:2:3713
+431:2:3724
+432:2:3734
+433:2:3735
+434:0:4844
+435:2:2881
+436:0:4844
+437:2:3741
+438:0:4844
+439:2:4563
+440:2:4564
+441:2:4568
+442:2:4572
+443:2:4573
+444:2:4577
+445:2:4585
+446:2:4586
+447:2:4590
+448:2:4594
+449:2:4595
+450:2:4590
+451:2:4594
+452:2:4595
+453:2:4599
+454:2:4606
+455:2:4613
+456:2:4614
+457:2:4621
+458:2:4626
+459:2:4633
+460:2:4634
+461:2:4633
+462:2:4634
+463:2:4641
+464:2:4645
+465:0:4844
+466:2:4650
+467:0:4844
+468:2:4651
+469:0:4844
+470:2:4652
+471:0:4844
+472:1:26
+473:0:4844
+474:1:30
+475:1:31
+476:1:35
+477:1:39
+478:1:40
+479:1:44
+480:1:52
+481:1:53
+482:1:57
+483:1:61
+484:1:62
+485:1:57
+486:1:61
+487:1:62
+488:1:66
+489:1:73
+490:1:80
+491:1:81
+492:1:88
+493:1:93
+494:1:100
+495:1:101
+496:1:100
+497:1:101
+498:1:108
+499:1:112
+500:0:4844
+501:1:117
+502:0:4844
+503:2:4655
+504:0:4844
+505:2:4660
+506:0:4844
+507:2:4661
+508:0:4844
+509:2:4669
+510:2:4670
+511:2:4674
+512:2:4678
+513:2:4679
+514:2:4683
+515:2:4691
+516:2:4692
+517:2:4696
+518:2:4700
+519:2:4701
+520:2:4696
+521:2:4700
+522:2:4701
+523:2:4705
+524:2:4712
+525:2:4719
+526:2:4720
+527:2:4727
+528:2:4732
+529:2:4739
+530:2:4740
+531:2:4739
+532:2:4740
+533:2:4747
+534:2:4751
+535:0:4844
+536:2:3743
+537:2:3753
+538:0:4844
+539:2:2881
+540:0:4844
+541:2:3744
+542:2:3745
+543:0:4844
+544:2:2881
+545:0:4844
+546:2:3749
+547:0:4844
+548:2:3757
+549:0:4844
+550:2:2878
+551:0:4844
+552:2:2880
+553:0:4844
+554:2:2881
+555:0:4844
+556:2:2882
+557:2:2883
+558:2:2887
+559:2:2888
+560:2:2896
+561:2:2897
+562:2:2901
+563:2:2902
+564:2:2910
+565:2:2915
+566:2:2919
+567:2:2920
+568:2:2928
+569:2:2929
+570:2:2930
+571:2:2928
+572:2:2929
+573:2:2933
+574:2:2934
+575:2:2942
+576:2:2947
+577:2:2948
+578:2:2959
+579:2:2960
+580:2:2961
+581:2:2972
+582:2:2977
+583:2:2978
+584:2:2989
+585:2:2990
+586:2:2991
+587:2:2989
+588:2:2990
+589:2:2991
+590:2:3002
+591:2:3010
+592:0:4844
+593:2:2881
+594:0:4844
+595:2:3014
+596:2:3018
+597:2:3019
+598:2:3023
+599:2:3027
+600:2:3028
+601:2:3032
+602:2:3040
+603:2:3041
+604:2:3045
+605:2:3046
+606:2:3045
+607:2:3049
+608:2:3050
+609:2:3054
+610:0:4844
+611:2:2881
+612:0:4844
+613:2:3062
+614:2:3063
+615:2:3064
+616:0:4844
+617:2:2881
+618:0:4844
+619:2:3069
+620:0:4844
+621:2:3969
+622:2:3970
+623:2:3974
+624:2:3978
+625:2:3979
+626:2:3983
+627:2:3988
+628:2:3996
+629:2:4000
+630:2:4001
+631:2:3996
+632:2:4000
+633:2:4001
+634:2:4005
+635:2:4012
+636:2:4019
+637:2:4020
+638:2:4027
+639:2:4032
+640:2:4039
+641:2:4040
+642:2:4039
+643:2:4040
+644:2:4047
+645:2:4051
+646:0:4844
+647:2:4056
+648:0:4844
+649:2:4057
+650:0:4844
+651:2:4058
+652:0:4844
+653:1:26
+654:0:4844
+655:1:30
+656:1:31
+657:1:35
+658:1:39
+659:1:40
+660:1:44
+661:1:52
+662:1:53
+663:1:57
+664:1:61
+665:1:62
+666:1:57
+667:1:61
+668:1:62
+669:1:66
+670:1:73
+671:1:80
+672:1:81
+673:1:88
+674:1:93
+675:1:100
+676:1:101
+677:1:100
+678:1:101
+679:1:108
+680:1:112
+681:0:4844
+682:1:117
+683:0:4844
+684:2:4061
+685:0:4844
+686:2:4066
+687:0:4844
+688:2:4067
+689:0:4844
+690:2:4075
+691:2:4076
+692:2:4080
+693:2:4084
+694:2:4085
+695:2:4089
+696:2:4097
+697:2:4098
+698:2:4102
+699:2:4106
+700:2:4107
+701:2:4102
+702:2:4106
+703:2:4107
+704:2:4111
+705:2:4118
+706:2:4125
+707:2:4126
+708:2:4133
+709:2:4138
+710:2:4145
+711:2:4146
+712:2:4145
+713:2:4146
+714:2:4153
+715:2:4157
+716:0:4844
+717:2:3071
+718:2:3753
+719:0:4844
+720:2:2881
+721:0:4844
+722:2:3072
+723:0:4844
+724:2:2881
+725:0:4844
+726:2:3075
+727:2:3076
+728:2:3080
+729:2:3081
+730:2:3089
+731:2:3090
+732:2:3094
+733:2:3095
+734:2:3103
+735:2:3108
+736:2:3112
+737:2:3113
+738:2:3121
+739:2:3122
+740:2:3126
+741:2:3127
+742:2:3121
+743:2:3122
+744:2:3126
+745:2:3127
+746:2:3135
+747:2:3140
+748:2:3141
+749:2:3152
+750:2:3153
+751:2:3154
+752:2:3165
+753:2:3170
+754:2:3171
+755:2:3182
+756:2:3183
+757:2:3184
+758:2:3182
+759:2:3183
+760:2:3184
+761:2:3195
+762:2:3202
+763:0:4844
+764:2:2881
+765:0:4844
+766:2:3206
+767:2:3207
+768:2:3208
+769:2:3220
+770:2:3221
+771:2:3225
+772:2:3226
+773:2:3234
+774:2:3239
+775:2:3243
+776:2:3244
+777:2:3252
+778:2:3253
+779:2:3257
+780:2:3258
+781:2:3252
+782:2:3253
+783:2:3257
+784:2:3258
+785:2:3266
+786:2:3271
+787:2:3272
+788:2:3283
+789:2:3284
+790:2:3285
+791:2:3296
+792:2:3301
+793:2:3302
+794:2:3313
+795:2:3314
+796:2:3315
+797:2:3313
+798:2:3314
+799:2:3315
+800:2:3326
+801:2:3337
+802:2:3338
+803:0:4844
+804:2:2881
+805:0:4844
+806:2:3344
+807:2:3345
+808:2:3349
+809:2:3350
+810:2:3358
+811:2:3359
+812:2:3363
+813:2:3364
+814:2:3372
+815:2:3377
+816:2:3381
+817:2:3382
+818:2:3390
+819:2:3391
+820:2:3395
+821:2:3396
+822:2:3390
+823:2:3391
+824:2:3395
+825:2:3396
+826:2:3404
+827:2:3409
+828:2:3410
+829:2:3421
+830:2:3422
+831:2:3423
+832:2:3434
+833:2:3439
+834:2:3440
+835:2:3451
+836:2:3452
+837:2:3453
+838:2:3451
+839:2:3452
+840:2:3453
+841:2:3464
+842:0:4844
+843:2:2881
+844:0:4844
+845:2:3473
+846:2:3474
+847:2:3478
+848:2:3479
+849:2:3487
+850:2:3488
+851:2:3492
+852:2:3493
+853:2:3501
+854:2:3506
+855:2:3510
+856:2:3511
+857:2:3519
+858:2:3520
+859:2:3524
+860:2:3525
+861:2:3519
+862:2:3520
+863:2:3524
+864:2:3525
+865:2:3533
+866:2:3538
+867:2:3539
+868:2:3550
+869:2:3551
+870:2:3552
+871:2:3563
+872:2:3568
+873:2:3569
+874:2:3580
+875:2:3581
+876:2:3582
+877:2:3580
+878:2:3581
+879:2:3582
+880:2:3593
+881:2:3600
+882:0:4844
+883:2:2881
+884:0:4844
+885:2:3604
+886:2:3605
+887:2:3606
+888:2:3618
+889:2:3619
+890:2:3623
+891:2:3624
+892:2:3632
+893:2:3637
+894:2:3641
+895:2:3642
+896:2:3650
+897:2:3651
+898:2:3655
+899:2:3656
+900:2:3650
+901:2:3651
+902:2:3655
+903:2:3656
+904:2:3664
+905:2:3669
+906:2:3670
+907:2:3681
+908:2:3682
+909:2:3683
+910:2:3694
+911:2:3699
+912:2:3700
+913:2:3711
+914:2:3712
+915:2:3713
+916:2:3711
+917:2:3712
+918:2:3713
+919:2:3724
+920:2:3734
+921:2:3735
+922:0:4844
+923:2:2881
+924:0:4844
+925:2:3741
+926:0:4844
+927:2:4563
+928:2:4564
+929:2:4568
+930:2:4572
+931:2:4573
+932:2:4577
+933:2:4585
+934:2:4586
+935:2:4590
+936:2:4594
+937:2:4595
+938:2:4590
+939:2:4594
+940:2:4595
+941:2:4599
+942:2:4606
+943:2:4613
+944:2:4614
+945:2:4621
+946:2:4626
+947:2:4633
+948:2:4634
+949:2:4633
+950:2:4634
+951:2:4641
+952:2:4645
+953:0:4844
+954:2:4650
+955:0:4844
+956:2:4651
+957:0:4844
+958:2:4652
+959:0:4844
+960:1:26
+961:0:4844
+962:1:30
+963:1:31
+964:1:35
+965:1:39
+966:1:40
+967:1:44
+968:1:52
+969:1:53
+970:1:57
+971:1:61
+972:1:62
+973:1:57
+974:1:61
+975:1:62
+976:1:66
+977:1:73
+978:1:80
+979:1:81
+980:1:88
+981:1:93
+982:1:100
+983:1:101
+984:1:100
+985:1:101
+986:1:108
+987:1:112
+988:0:4844
+989:1:117
+990:0:4844
+991:2:4655
+992:0:4844
+993:2:4660
+994:0:4844
+995:2:4661
+996:0:4844
+997:2:4669
+998:2:4670
+999:2:4674
+1000:2:4678
+1001:2:4679
+1002:2:4683
+1003:2:4691
+1004:2:4692
+1005:2:4696
+1006:2:4700
+1007:2:4701
+1008:2:4696
+1009:2:4700
+1010:2:4701
+1011:2:4705
+1012:2:4712
+1013:2:4719
+1014:2:4720
+1015:2:4727
+1016:2:4732
+1017:2:4739
+1018:2:4740
+1019:2:4739
+1020:2:4740
+1021:2:4747
+1022:2:4751
+1023:0:4844
+1024:2:3743
+1025:2:3753
+1026:0:4844
+1027:2:2881
+1028:0:4844
+1029:2:3744
+1030:2:3745
+1031:0:4844
+1032:2:2881
+1033:0:4844
+1034:2:3749
+1035:0:4844
+1036:2:3757
+1037:0:4844
+1038:2:2878
+1039:0:4844
+1040:2:2880
+1041:0:4844
+1042:2:2881
+1043:0:4844
+1044:2:2882
+1045:2:2883
+1046:2:2887
+1047:2:2888
+1048:2:2896
+1049:2:2897
+1050:2:2901
+1051:2:2902
+1052:2:2910
+1053:2:2915
+1054:2:2919
+1055:2:2920
+1056:2:2928
+1057:2:2929
+1058:2:2933
+1059:2:2934
+1060:2:2928
+1061:2:2929
+1062:2:2930
+1063:2:2942
+1064:2:2947
+1065:2:2948
+1066:2:2959
+1067:2:2960
+1068:2:2961
+1069:2:2972
+1070:2:2977
+1071:2:2978
+1072:2:2989
+1073:2:2990
+1074:2:2991
+1075:2:2989
+1076:2:2990
+1077:2:2991
+1078:2:3002
+1079:2:3010
+1080:0:4844
+1081:2:2881
+1082:0:4844
+1083:2:3014
+1084:2:3018
+1085:2:3019
+1086:2:3023
+1087:2:3027
+1088:2:3028
+1089:2:3032
+1090:2:3040
+1091:2:3041
+1092:2:3045
+1093:2:3049
+1094:2:3050
+1095:2:3045
+1096:2:3046
+1097:2:3054
+1098:0:4844
+1099:2:2881
+1100:0:4844
+1101:2:3062
+1102:2:3063
+1103:2:3064
+1104:0:4844
+1105:2:2881
+1106:0:4844
+1107:2:3069
+1108:0:4844
+1109:2:3969
+1110:2:3970
+1111:2:3974
+1112:2:3978
+1113:2:3979
+1114:2:3983
+1115:2:3988
+1116:2:3996
+1117:2:4000
+1118:2:4001
+1119:2:3996
+1120:2:4000
+1121:2:4001
+1122:2:4005
+1123:2:4012
+1124:2:4019
+1125:2:4020
+1126:2:4027
+1127:2:4032
+1128:2:4039
+1129:2:4040
+1130:2:4039
+1131:2:4040
+1132:2:4047
+1133:2:4051
+1134:0:4844
+1135:2:4056
+1136:0:4844
+1137:2:4057
+1138:0:4844
+1139:2:4058
+1140:0:4844
+1141:1:26
+1142:0:4844
+1143:1:30
+1144:1:31
+1145:1:35
+1146:1:39
+1147:1:40
+1148:1:44
+1149:1:52
+1150:1:53
+1151:1:57
+1152:1:61
+1153:1:62
+1154:1:57
+1155:1:61
+1156:1:62
+1157:1:66
+1158:1:73
+1159:1:80
+1160:1:81
+1161:1:88
+1162:1:93
+1163:1:100
+1164:1:101
+1165:1:100
+1166:1:101
+1167:1:108
+1168:1:112
+1169:0:4844
+1170:1:117
+1171:0:4844
+1172:2:4061
+1173:0:4844
+1174:2:4066
+1175:0:4844
+1176:2:4067
+1177:0:4844
+1178:2:4075
+1179:2:4076
+1180:2:4080
+1181:2:4084
+1182:2:4085
+1183:2:4089
+1184:2:4097
+1185:2:4098
+1186:2:4102
+1187:2:4106
+1188:2:4107
+1189:2:4102
+1190:2:4106
+1191:2:4107
+1192:2:4111
+1193:2:4118
+1194:2:4125
+1195:2:4126
+1196:2:4133
+1197:2:4138
+1198:2:4145
+1199:2:4146
+1200:2:4145
+1201:2:4146
+1202:2:4153
+1203:2:4157
+1204:0:4844
+1205:2:3071
+1206:2:3753
+1207:0:4844
+1208:2:2881
+1209:0:4844
+1210:2:3072
+1211:0:4844
+1212:2:2881
+1213:0:4844
+1214:2:3075
+1215:2:3076
+1216:2:3080
+1217:2:3081
+1218:2:3089
+1219:2:3090
+1220:2:3094
+1221:2:3095
+1222:2:3103
+1223:2:3108
+1224:2:3112
+1225:2:3113
+1226:2:3121
+1227:2:3122
+1228:2:3126
+1229:2:3127
+1230:2:3121
+1231:2:3122
+1232:2:3126
+1233:2:3127
+1234:2:3135
+1235:2:3140
+1236:2:3141
+1237:2:3152
+1238:2:3153
+1239:2:3154
+1240:2:3165
+1241:2:3170
+1242:2:3171
+1243:2:3182
+1244:2:3183
+1245:2:3184
+1246:2:3182
+1247:2:3183
+1248:2:3184
+1249:2:3195
+1250:2:3202
+1251:0:4844
+1252:2:2881
+1253:0:4844
+1254:2:3206
+1255:2:3207
+1256:2:3208
+1257:2:3220
+1258:2:3221
+1259:2:3225
+1260:2:3226
+1261:2:3234
+1262:2:3239
+1263:2:3243
+1264:2:3244
+1265:2:3252
+1266:2:3253
+1267:2:3257
+1268:2:3258
+1269:2:3252
+1270:2:3253
+1271:2:3257
+1272:2:3258
+1273:2:3266
+1274:2:3271
+1275:2:3272
+1276:2:3283
+1277:2:3284
+1278:2:3285
+1279:2:3296
+1280:2:3301
+1281:2:3302
+1282:2:3313
+1283:2:3314
+1284:2:3315
+1285:2:3313
+1286:2:3314
+1287:2:3315
+1288:2:3326
+1289:2:3337
+1290:2:3338
+1291:0:4844
+1292:2:2881
+1293:0:4844
+1294:2:3344
+1295:2:3345
+1296:2:3349
+1297:2:3350
+1298:2:3358
+1299:2:3359
+1300:2:3363
+1301:2:3364
+1302:2:3372
+1303:2:3377
+1304:2:3381
+1305:2:3382
+1306:2:3390
+1307:2:3391
+1308:2:3395
+1309:2:3396
+1310:2:3390
+1311:2:3391
+1312:2:3395
+1313:2:3396
+1314:2:3404
+1315:2:3409
+1316:2:3410
+1317:2:3421
+1318:2:3422
+1319:2:3423
+1320:2:3434
+1321:2:3439
+1322:2:3440
+1323:2:3451
+1324:2:3452
+1325:2:3453
+1326:2:3451
+1327:2:3452
+1328:2:3453
+1329:2:3464
+1330:0:4844
+1331:2:2881
+1332:0:4844
+1333:2:3473
+1334:2:3474
+1335:2:3478
+1336:2:3479
+1337:2:3487
+1338:2:3488
+1339:2:3492
+1340:2:3493
+1341:2:3501
+1342:2:3506
+1343:2:3510
+1344:2:3511
+1345:2:3519
+1346:2:3520
+1347:2:3524
+1348:2:3525
+1349:2:3519
+1350:2:3520
+1351:2:3524
+1352:2:3525
+1353:2:3533
+1354:2:3538
+1355:2:3539
+1356:2:3550
+1357:2:3551
+1358:2:3552
+1359:2:3563
+1360:2:3568
+1361:2:3569
+1362:2:3580
+1363:2:3581
+1364:2:3582
+1365:2:3580
+1366:2:3581
+1367:2:3582
+1368:2:3593
+1369:2:3600
+1370:0:4844
+1371:2:2881
+1372:0:4844
+1373:2:3604
+1374:2:3605
+1375:2:3606
+1376:2:3618
+1377:2:3619
+1378:2:3623
+1379:2:3624
+1380:2:3632
+1381:2:3637
+1382:2:3641
+1383:2:3642
+1384:2:3650
+1385:2:3651
+1386:2:3655
+1387:2:3656
+1388:2:3650
+1389:2:3651
+1390:2:3655
+1391:2:3656
+1392:2:3664
+1393:2:3669
+1394:2:3670
+1395:2:3681
+1396:2:3682
+1397:2:3683
+1398:2:3694
+1399:2:3699
+1400:2:3700
+1401:2:3711
+1402:2:3712
+1403:2:3713
+1404:2:3711
+1405:2:3712
+1406:2:3713
+1407:2:3724
+1408:2:3734
+1409:2:3735
+1410:0:4844
+1411:2:2881
+1412:0:4844
+1413:2:3741
+1414:0:4844
+1415:2:4563
+1416:2:4564
+1417:2:4568
+1418:2:4572
+1419:2:4573
+1420:2:4577
+1421:2:4585
+1422:2:4586
+1423:2:4590
+1424:2:4594
+1425:2:4595
+1426:2:4590
+1427:2:4594
+1428:2:4595
+1429:2:4599
+1430:2:4606
+1431:2:4613
+1432:2:4614
+1433:2:4621
+1434:2:4626
+1435:2:4633
+1436:2:4634
+1437:2:4633
+1438:2:4634
+1439:2:4641
+1440:2:4645
+1441:0:4844
+1442:2:4650
+1443:0:4844
+1444:2:4651
+1445:0:4844
+1446:2:4652
+1447:0:4844
+1448:1:26
+1449:0:4844
+1450:1:30
+1451:1:31
+1452:1:35
+1453:1:39
+1454:1:40
+1455:1:44
+1456:1:52
+1457:1:53
+1458:1:57
+1459:1:61
+1460:1:62
+1461:1:57
+1462:1:61
+1463:1:62
+1464:1:66
+1465:1:73
+1466:1:80
+1467:1:81
+1468:1:88
+1469:1:93
+1470:1:100
+1471:1:101
+1472:1:100
+1473:1:101
+1474:1:108
+1475:1:112
+1476:0:4844
+1477:1:117
+1478:0:4844
+1479:2:4655
+1480:0:4844
+1481:2:4660
+1482:0:4844
+1483:2:4661
+1484:0:4844
+1485:2:4669
+1486:2:4670
+1487:2:4674
+1488:2:4678
+1489:2:4679
+1490:2:4683
+1491:2:4691
+1492:2:4692
+1493:2:4696
+1494:2:4700
+1495:2:4701
+1496:2:4696
+1497:2:4700
+1498:2:4701
+1499:2:4705
+1500:2:4712
+1501:2:4719
+1502:2:4720
+1503:2:4727
+1504:2:4732
+1505:2:4739
+1506:2:4740
+1507:2:4739
+1508:2:4740
+1509:2:4747
+1510:2:4751
+1511:0:4844
+1512:2:3743
+1513:2:3753
+1514:0:4844
+1515:2:2881
+1516:0:4844
+1517:2:3744
+1518:2:3745
+1519:0:4844
+1520:2:2881
+1521:0:4844
+1522:2:3749
+1523:0:4844
+1524:2:3757
+1525:0:4844
+1526:2:3758
+1527:0:4844
+1528:2:3763
+1529:0:4844
+1530:2:3767
+1531:2:3768
+1532:2:3772
+1533:2:3776
+1534:2:3777
+1535:2:3781
+1536:2:3789
+1537:2:3790
+1538:2:3794
+1539:2:3795
+1540:2:3794
+1541:2:3798
+1542:2:3799
+1543:2:3803
+1544:2:3810
+1545:2:3817
+1546:2:3818
+1547:2:3825
+1548:2:3830
+1549:2:3837
+1550:2:3838
+1551:2:3837
+1552:2:3838
+1553:2:3845
+1554:2:3849
+1555:0:4844
+1556:2:3854
+1557:0:4844
+1558:2:3855
+1559:0:4844
+1560:2:3856
+1561:0:4844
+1562:1:26
+1563:0:4844
+1564:1:30
+1565:1:31
+1566:1:35
+1567:1:39
+1568:1:40
+1569:1:44
+1570:1:52
+1571:1:53
+1572:1:57
+1573:1:61
+1574:1:62
+1575:1:57
+1576:1:61
+1577:1:62
+1578:1:66
+1579:1:73
+1580:1:80
+1581:1:81
+1582:1:88
+1583:1:93
+1584:1:100
+1585:1:101
+1586:1:100
+1587:1:101
+1588:1:108
+1589:1:112
+1590:0:4844
+1591:1:117
+1592:0:4844
+1593:2:3859
+1594:0:4844
+1595:2:3864
+1596:0:4844
+1597:2:3865
+1598:0:4844
+1599:2:3873
+1600:2:3874
+1601:2:3878
+1602:2:3882
+1603:2:3883
+1604:2:3887
+1605:2:3895
+1606:2:3896
+1607:2:3900
+1608:2:3904
+1609:2:3905
+1610:2:3900
+1611:2:3904
+1612:2:3905
+1613:2:3909
+1614:2:3916
+1615:2:3923
+1616:2:3924
+1617:2:3931
+1618:2:3936
+1619:2:3943
+1620:2:3944
+1621:2:3943
+1622:2:3944
+1623:2:3951
+1624:2:3955
+1625:0:4844
+1626:2:3961
+1627:0:4844
+1628:2:3763
+1629:0:4844
+1630:2:3767
+1631:2:3768
+1632:2:3772
+1633:2:3776
+1634:2:3777
+1635:2:3781
+1636:2:3789
+1637:2:3790
+1638:2:3794
+1639:2:3798
+1640:2:3799
+1641:2:3794
+1642:2:3798
+1643:2:3799
+1644:2:3803
+1645:2:3810
+1646:2:3817
+1647:2:3818
+1648:2:3825
+1649:2:3830
+1650:2:3837
+1651:2:3838
+1652:2:3837
+1653:2:3838
+1654:2:3845
+1655:2:3849
+1656:0:4844
+1657:2:3854
+1658:0:4844
+1659:2:3855
+1660:0:4844
+1661:2:3856
+1662:0:4844
+1663:1:26
+-1:-1:-1
+1664:0:4844
+1665:1:30
+1666:1:31
+1667:1:35
+1668:1:39
+1669:1:40
+1670:1:44
+1671:1:52
+1672:1:53
+1673:1:57
+1674:1:61
+1675:1:62
+1676:1:57
+1677:1:61
+1678:1:62
+1679:1:66
+1680:1:73
+1681:1:80
+1682:1:81
+1683:1:88
+1684:1:93
+1685:1:100
+1686:1:101
+1687:1:100
+1688:1:101
+1689:1:108
+1690:1:112
+1691:0:4844
+1692:1:117
+1693:0:4844
+1694:2:3859
+1695:0:4844
+1696:2:3864
+1697:0:4844
+1698:2:3865
+1699:0:4844
+1700:2:3873
+1701:2:3874
+1702:2:3878
+1703:2:3882
+1704:2:3883
+1705:2:3887
+1706:2:3895
+1707:2:3896
+1708:2:3900
+1709:2:3904
+1710:2:3905
+1711:2:3900
+1712:2:3904
+1713:2:3905
+1714:2:3909
+1715:2:3916
+1716:2:3923
+1717:2:3924
+1718:2:3931
+1719:2:3936
+1720:2:3943
+1721:2:3944
+1722:2:3943
+1723:2:3944
+1724:2:3951
+1725:2:3955
+1726:0:4844
+1727:2:3961
+1728:0:4844
+1729:2:3763
+1730:0:4844
+1731:2:3767
+1732:2:3768
+1733:2:3772
+1734:2:3776
+1735:2:3777
+1736:2:3781
+1737:2:3789
+1738:2:3790
+1739:2:3794
+1740:2:3798
+1741:2:3799
+1742:2:3794
+1743:2:3798
+1744:2:3799
+1745:2:3803
+1746:2:3810
+1747:2:3817
+1748:2:3818
+1749:2:3825
+1750:2:3830
+1751:2:3837
+1752:2:3838
+1753:2:3837
+1754:2:3838
+1755:2:3845
+1756:2:3849
+1757:0:4844
+1758:2:3854
+1759:0:4844
+1760:2:3855
+1761:0:4844
+1762:2:3856
+1763:0:4844
+1764:1:26