Add Intel ipi urcu model run results

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

diff --git a/formal-model/results/urcu-controldataflow-ipi-intel/urcu_progress_writer_error.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi-intel/urcu_progress_writer_error.spin.input.trail
new file mode 100644 (file)
index 0000000..ee9e4b8
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi-intel/urcu_progress_writer_error.spin.input.trail
@@ -0,0 +1,1700 @@
+-2:3:-2
+-4:-4:-4
+1:0:3993
+2:3:3913
+3:3:3916
+4:3:3916
+5:3:3919
+6:3:3927
+7:3:3927
+8:3:3930
+9:3:3936
+10:3:3940
+11:3:3940
+12:3:3943
+13:3:3953
+14:3:3961
+15:3:3961
+16:3:3964
+17:3:3970
+18:3:3974
+19:3:3974
+20:3:3977
+21:3:3983
+22:3:3987
+23:3:3988
+24:0:3993
+25:3:3990
+26:0:3993
+27:2:2511
+28:0:3993
+29:2:2517
+30:0:3993
+31:2:2518
+32:0:3993
+33:2:2519
+34:0:3993
+35:2:2520
+36:0:3993
+37:2:2521
+38:0:3993
+39:2:2522
+40:2:2523
+41:2:2527
+42:2:2528
+43:2:2536
+44:2:2537
+45:2:2541
+46:2:2542
+47:2:2550
+48:2:2555
+49:2:2559
+50:2:2560
+51:2:2568
+52:2:2569
+53:2:2573
+54:2:2574
+55:2:2568
+56:2:2569
+57:2:2573
+58:2:2574
+59:2:2582
+60:2:2587
+61:2:2594
+62:2:2595
+63:2:2602
+64:2:2607
+65:2:2614
+66:2:2615
+67:2:2614
+68:2:2615
+69:2:2622
+70:2:2632
+71:0:3993
+72:2:2521
+73:0:3993
+74:2:2636
+75:2:2640
+76:2:2641
+77:2:2645
+78:2:2649
+79:2:2650
+80:2:2654
+81:2:2662
+82:2:2663
+83:2:2667
+84:2:2671
+85:2:2672
+86:2:2667
+87:2:2668
+88:2:2676
+89:0:3993
+90:2:2521
+91:0:3993
+92:2:2684
+93:2:2685
+94:2:2686
+95:0:3993
+96:2:2521
+97:0:3993
+98:2:2691
+99:0:3993
+100:2:3518
+101:2:3519
+102:2:3523
+103:2:3527
+104:2:3528
+105:2:3532
+106:2:3537
+107:2:3545
+108:2:3549
+109:2:3550
+110:2:3545
+111:2:3549
+112:2:3550
+113:2:3554
+114:2:3561
+115:2:3568
+116:2:3569
+117:2:3576
+118:2:3581
+119:2:3588
+120:2:3589
+121:2:3588
+122:2:3589
+123:2:3596
+124:2:3600
+125:0:3993
+126:2:3605
+127:0:3993
+128:2:3606
+129:0:3993
+130:2:3607
+131:0:3993
+132:2:3608
+133:0:3993
+134:1:2
+135:0:3993
+136:1:8
+137:0:3993
+138:1:9
+139:0:3993
+140:2:3609
+141:0:3993
+142:1:10
+143:0:3993
+144:2:3608
+145:0:3993
+146:1:11
+147:0:3993
+148:2:3609
+149:0:3993
+150:1:12
+151:0:3993
+152:2:3608
+153:0:3993
+154:1:13
+155:0:3993
+156:2:3609
+157:0:3993
+158:1:14
+159:0:3993
+160:1:15
+161:0:3993
+162:1:16
+163:0:3993
+164:2:3608
+165:0:3993
+166:1:17
+167:0:3993
+168:2:3609
+169:0:3993
+170:1:26
+171:0:3993
+172:2:3608
+173:0:3993
+174:1:30
+175:1:31
+176:1:35
+177:1:39
+178:1:40
+179:1:44
+180:1:52
+181:1:53
+182:1:57
+183:1:61
+184:1:62
+185:1:57
+186:1:61
+187:1:62
+188:1:66
+189:1:73
+190:1:80
+191:1:81
+192:1:88
+193:1:93
+194:1:100
+195:1:101
+196:1:100
+197:1:101
+198:1:108
+199:1:112
+200:0:3993
+201:2:3609
+202:0:3993
+203:1:117
+204:0:3993
+205:2:3610
+206:0:3993
+207:2:3615
+208:0:3993
+209:2:3616
+210:0:3993
+211:2:3624
+212:2:3625
+213:2:3629
+214:2:3633
+215:2:3634
+216:2:3638
+217:2:3646
+218:2:3647
+219:2:3651
+220:2:3655
+221:2:3656
+222:2:3651
+223:2:3655
+224:2:3656
+225:2:3660
+226:2:3667
+227:2:3674
+228:2:3675
+229:2:3682
+230:2:3687
+231:2:3694
+232:2:3695
+233:2:3694
+234:2:3695
+235:2:3702
+236:2:3706
+237:0:3993
+238:2:2693
+239:2:3499
+240:0:3993
+241:2:2521
+242:0:3993
+243:2:2694
+244:0:3993
+245:2:2521
+246:0:3993
+247:2:2697
+248:2:2698
+249:2:2702
+250:2:2703
+251:2:2711
+252:2:2712
+253:2:2716
+254:2:2717
+255:2:2725
+256:2:2730
+257:2:2734
+258:2:2735
+259:2:2743
+260:2:2744
+261:2:2748
+262:2:2749
+263:2:2743
+264:2:2744
+265:2:2748
+266:2:2749
+267:2:2757
+268:2:2762
+269:2:2769
+270:2:2770
+271:2:2777
+272:2:2782
+273:2:2789
+274:2:2790
+275:2:2789
+276:2:2790
+277:2:2797
+278:2:2806
+279:0:3993
+280:2:2521
+281:0:3993
+282:2:2810
+283:2:2811
+284:2:2812
+285:2:2824
+286:2:2825
+287:2:2829
+288:2:2830
+289:2:2838
+290:2:2843
+291:2:2847
+292:2:2848
+293:2:2856
+294:2:2857
+295:2:2861
+296:2:2862
+297:2:2856
+298:2:2857
+299:2:2861
+300:2:2862
+301:2:2870
+302:2:2875
+303:2:2882
+304:2:2883
+305:2:2890
+306:2:2895
+307:2:2902
+308:2:2903
+309:2:2902
+310:2:2903
+311:2:2910
+312:2:2923
+313:2:2924
+314:0:3993
+315:2:2521
+316:0:3993
+317:2:3037
+318:2:3038
+319:2:3042
+320:2:3043
+321:2:3051
+322:2:3052
+323:2:3056
+324:2:3057
+325:2:3065
+326:2:3070
+327:2:3074
+328:2:3075
+329:2:3083
+330:2:3084
+331:2:3088
+332:2:3089
+333:2:3083
+334:2:3084
+335:2:3088
+336:2:3089
+337:2:3097
+338:2:3102
+339:2:3109
+340:2:3110
+341:2:3117
+342:2:3122
+343:2:3129
+344:2:3130
+345:2:3129
+346:2:3130
+347:2:3137
+348:0:3993
+349:2:2521
+350:0:3993
+351:2:3148
+352:2:3149
+353:2:3153
+354:2:3154
+355:2:3162
+356:2:3163
+357:2:3167
+358:2:3168
+359:2:3176
+360:2:3181
+361:2:3185
+362:2:3186
+363:2:3194
+364:2:3195
+365:2:3199
+366:2:3200
+367:2:3194
+368:2:3195
+369:2:3199
+370:2:3200
+371:2:3208
+372:2:3213
+373:2:3220
+374:2:3221
+375:2:3228
+376:2:3233
+377:2:3240
+378:2:3241
+379:2:3240
+380:2:3241
+381:2:3248
+382:2:3257
+383:0:3993
+384:2:2521
+385:0:3993
+386:2:3261
+387:2:3262
+388:2:3263
+389:2:3275
+390:2:3276
+391:2:3280
+392:2:3281
+393:2:3289
+394:2:3294
+395:2:3298
+396:2:3299
+397:2:3307
+398:2:3308
+399:2:3312
+400:2:3313
+401:2:3307
+402:2:3308
+403:2:3312
+404:2:3313
+405:2:3321
+406:2:3326
+407:2:3333
+408:2:3334
+409:2:3341
+410:2:3346
+411:2:3353
+412:2:3354
+413:2:3353
+414:2:3354
+415:2:3361
+416:2:3373
+417:2:3374
+418:0:3993
+419:2:2521
+420:0:3993
+421:2:3487
+422:0:3993
+423:2:3716
+424:2:3717
+425:2:3721
+426:2:3725
+427:2:3726
+428:2:3730
+429:2:3738
+430:2:3739
+431:2:3743
+432:2:3747
+433:2:3748
+434:2:3743
+435:2:3747
+436:2:3748
+437:2:3752
+438:2:3759
+439:2:3766
+440:2:3767
+441:2:3774
+442:2:3779
+443:2:3786
+444:2:3787
+445:2:3786
+446:2:3787
+447:2:3794
+448:2:3798
+449:0:3993
+450:2:3803
+451:0:3993
+452:2:3804
+453:0:3993
+454:2:3805
+455:0:3993
+456:2:3806
+457:0:3993
+458:1:26
+459:0:3993
+460:2:3807
+461:0:3993
+462:1:30
+463:1:31
+464:1:35
+465:1:39
+466:1:40
+467:1:44
+468:1:52
+469:1:53
+470:1:57
+471:1:61
+472:1:62
+473:1:57
+474:1:61
+475:1:62
+476:1:66
+477:1:73
+478:1:80
+479:1:81
+480:1:88
+481:1:93
+482:1:100
+483:1:101
+484:1:100
+485:1:101
+486:1:108
+487:1:112
+488:0:3993
+489:2:3806
+490:0:3993
+491:1:117
+492:0:3993
+493:2:3807
+494:0:3993
+495:2:3808
+496:0:3993
+497:2:3813
+498:0:3993
+499:2:3814
+500:0:3993
+501:2:3822
+502:2:3823
+503:2:3827
+504:2:3831
+505:2:3832
+506:2:3836
+507:2:3844
+508:2:3845
+509:2:3849
+510:2:3853
+511:2:3854
+512:2:3849
+513:2:3853
+514:2:3854
+515:2:3858
+516:2:3865
+517:2:3872
+518:2:3873
+519:2:3880
+520:2:3885
+521:2:3892
+522:2:3893
+523:2:3892
+524:2:3893
+525:2:3900
+526:2:3904
+527:0:3993
+528:2:3489
+529:2:3499
+530:0:3993
+531:2:2521
+532:0:3993
+533:2:3490
+534:2:3491
+535:0:3993
+536:2:2521
+537:0:3993
+538:2:3495
+539:0:3993
+540:2:3503
+541:0:3993
+542:2:2518
+543:0:3993
+544:2:2519
+545:0:3993
+546:2:2520
+547:0:3993
+548:2:2521
+549:0:3993
+550:2:2522
+551:2:2523
+552:2:2527
+553:2:2528
+554:2:2536
+555:2:2537
+556:2:2541
+557:2:2542
+558:2:2550
+559:2:2555
+560:2:2559
+561:2:2560
+562:2:2568
+563:2:2569
+564:2:2570
+565:2:2568
+566:2:2569
+567:2:2573
+568:2:2574
+569:2:2582
+570:2:2587
+571:2:2594
+572:2:2595
+573:2:2602
+574:2:2607
+575:2:2614
+576:2:2615
+577:2:2614
+578:2:2615
+579:2:2622
+580:2:2632
+581:0:3993
+582:2:2521
+583:0:3993
+584:2:2636
+585:2:2640
+586:2:2641
+587:2:2645
+588:2:2649
+589:2:2650
+590:2:2654
+591:2:2662
+592:2:2663
+593:2:2667
+594:2:2668
+595:2:2667
+596:2:2671
+597:2:2672
+598:2:2676
+599:0:3993
+600:2:2521
+601:0:3993
+602:2:2684
+603:2:2685
+604:2:2686
+605:0:3993
+606:2:2521
+607:0:3993
+608:2:2691
+609:0:3993
+610:2:3518
+611:2:3519
+612:2:3523
+613:2:3527
+614:2:3528
+615:2:3532
+616:2:3537
+617:2:3545
+618:2:3549
+619:2:3550
+620:2:3545
+621:2:3549
+622:2:3550
+623:2:3554
+624:2:3561
+625:2:3568
+626:2:3569
+627:2:3576
+628:2:3581
+629:2:3588
+630:2:3589
+631:2:3588
+632:2:3589
+633:2:3596
+634:2:3600
+635:0:3993
+636:2:3605
+637:0:3993
+638:2:3606
+639:0:3993
+640:2:3607
+641:0:3993
+642:2:3608
+643:0:3993
+644:1:26
+645:0:3993
+646:2:3609
+647:0:3993
+648:1:30
+649:1:31
+650:1:35
+651:1:39
+652:1:40
+653:1:44
+654:1:52
+655:1:53
+656:1:57
+657:1:61
+658:1:62
+659:1:57
+660:1:61
+661:1:62
+662:1:66
+663:1:73
+664:1:80
+665:1:81
+666:1:88
+667:1:93
+668:1:100
+669:1:101
+670:1:100
+671:1:101
+672:1:108
+673:1:112
+674:0:3993
+675:2:3608
+676:0:3993
+677:1:117
+678:0:3993
+679:2:3609
+680:0:3993
+681:2:3610
+682:0:3993
+683:2:3615
+684:0:3993
+685:2:3616
+686:0:3993
+687:2:3624
+688:2:3625
+689:2:3629
+690:2:3633
+691:2:3634
+692:2:3638
+693:2:3646
+694:2:3647
+695:2:3651
+696:2:3655
+697:2:3656
+698:2:3651
+699:2:3655
+700:2:3656
+701:2:3660
+702:2:3667
+703:2:3674
+704:2:3675
+705:2:3682
+706:2:3687
+707:2:3694
+708:2:3695
+709:2:3694
+710:2:3695
+711:2:3702
+712:2:3706
+713:0:3993
+714:2:2693
+715:2:3499
+716:0:3993
+717:2:2521
+718:0:3993
+719:2:2694
+720:0:3993
+721:2:2521
+722:0:3993
+723:2:2697
+724:2:2698
+725:2:2702
+726:2:2703
+727:2:2711
+728:2:2712
+729:2:2716
+730:2:2717
+731:2:2725
+732:2:2730
+733:2:2734
+734:2:2735
+735:2:2743
+736:2:2744
+737:2:2748
+738:2:2749
+739:2:2743
+740:2:2744
+741:2:2748
+742:2:2749
+743:2:2757
+744:2:2762
+745:2:2769
+746:2:2770
+747:2:2777
+748:2:2782
+749:2:2789
+750:2:2790
+751:2:2789
+752:2:2790
+753:2:2797
+754:2:2806
+755:0:3993
+756:2:2521
+757:0:3993
+758:2:2810
+759:2:2811
+760:2:2812
+761:2:2824
+762:2:2825
+763:2:2829
+764:2:2830
+765:2:2838
+766:2:2843
+767:2:2847
+768:2:2848
+769:2:2856
+770:2:2857
+771:2:2861
+772:2:2862
+773:2:2856
+774:2:2857
+775:2:2861
+776:2:2862
+777:2:2870
+778:2:2875
+779:2:2882
+780:2:2883
+781:2:2890
+782:2:2895
+783:2:2902
+784:2:2903
+785:2:2902
+786:2:2903
+787:2:2910
+788:2:2923
+789:2:2924
+790:0:3993
+791:2:2521
+792:0:3993
+793:2:3037
+794:2:3038
+795:2:3042
+796:2:3043
+797:2:3051
+798:2:3052
+799:2:3056
+800:2:3057
+801:2:3065
+802:2:3070
+803:2:3074
+804:2:3075
+805:2:3083
+806:2:3084
+807:2:3088
+808:2:3089
+809:2:3083
+810:2:3084
+811:2:3088
+812:2:3089
+813:2:3097
+814:2:3102
+815:2:3109
+816:2:3110
+817:2:3117
+818:2:3122
+819:2:3129
+820:2:3130
+821:2:3129
+822:2:3130
+823:2:3137
+824:0:3993
+825:2:2521
+826:0:3993
+827:2:3148
+828:2:3149
+829:2:3153
+830:2:3154
+831:2:3162
+832:2:3163
+833:2:3167
+834:2:3168
+835:2:3176
+836:2:3181
+837:2:3185
+838:2:3186
+839:2:3194
+840:2:3195
+841:2:3199
+842:2:3200
+843:2:3194
+844:2:3195
+845:2:3199
+846:2:3200
+847:2:3208
+848:2:3213
+849:2:3220
+850:2:3221
+851:2:3228
+852:2:3233
+853:2:3240
+854:2:3241
+855:2:3240
+856:2:3241
+857:2:3248
+858:2:3257
+859:0:3993
+860:2:2521
+861:0:3993
+862:2:3261
+863:2:3262
+864:2:3263
+865:2:3275
+866:2:3276
+867:2:3280
+868:2:3281
+869:2:3289
+870:2:3294
+871:2:3298
+872:2:3299
+873:2:3307
+874:2:3308
+875:2:3312
+876:2:3313
+877:2:3307
+878:2:3308
+879:2:3312
+880:2:3313
+881:2:3321
+882:2:3326
+883:2:3333
+884:2:3334
+885:2:3341
+886:2:3346
+887:2:3353
+888:2:3354
+889:2:3353
+890:2:3354
+891:2:3361
+892:2:3373
+893:2:3374
+894:0:3993
+895:2:2521
+896:0:3993
+897:2:3487
+898:0:3993
+899:2:3716
+900:2:3717
+901:2:3721
+902:2:3725
+903:2:3726
+904:2:3730
+905:2:3738
+906:2:3739
+907:2:3743
+908:2:3747
+909:2:3748
+910:2:3743
+911:2:3747
+912:2:3748
+913:2:3752
+914:2:3759
+915:2:3766
+916:2:3767
+917:2:3774
+918:2:3779
+919:2:3786
+920:2:3787
+921:2:3786
+922:2:3787
+923:2:3794
+924:2:3798
+925:0:3993
+926:2:3803
+927:0:3993
+928:2:3804
+929:0:3993
+930:2:3805
+931:0:3993
+932:2:3806
+933:0:3993
+934:1:26
+935:0:3993
+936:2:3807
+937:0:3993
+938:1:30
+939:1:31
+940:1:35
+941:1:39
+942:1:40
+943:1:44
+944:1:52
+945:1:53
+946:1:57
+947:1:61
+948:1:62
+949:1:57
+950:1:61
+951:1:62
+952:1:66
+953:1:73
+954:1:80
+955:1:81
+956:1:88
+957:1:93
+958:1:100
+959:1:101
+960:1:100
+961:1:101
+962:1:108
+963:1:112
+964:0:3993
+965:2:3806
+966:0:3993
+967:1:117
+968:0:3993
+969:2:3807
+970:0:3993
+971:2:3808
+972:0:3993
+973:2:3813
+974:0:3993
+975:2:3814
+976:0:3993
+977:2:3822
+978:2:3823
+979:2:3827
+980:2:3831
+981:2:3832
+982:2:3836
+983:2:3844
+984:2:3845
+985:2:3849
+986:2:3853
+987:2:3854
+988:2:3849
+989:2:3853
+990:2:3854
+991:2:3858
+992:2:3865
+993:2:3872
+994:2:3873
+995:2:3880
+996:2:3885
+997:2:3892
+998:2:3893
+999:2:3892
+1000:2:3893
+1001:2:3900
+1002:2:3904
+1003:0:3993
+1004:2:3489
+1005:2:3499
+1006:0:3993
+1007:2:2521
+1008:0:3993
+1009:2:3490
+1010:2:3491
+1011:0:3993
+1012:2:2521
+1013:0:3993
+1014:2:3495
+1015:0:3993
+1016:2:3503
+1017:0:3993
+1018:2:2518
+1019:0:3993
+1020:2:2519
+1021:0:3993
+1022:2:2520
+1023:0:3993
+1024:2:2521
+1025:0:3993
+1026:2:2522
+1027:2:2523
+1028:2:2527
+1029:2:2528
+1030:2:2536
+1031:2:2537
+1032:2:2541
+1033:2:2542
+1034:2:2550
+1035:2:2555
+1036:2:2559
+1037:2:2560
+1038:2:2568
+1039:2:2569
+1040:2:2573
+1041:2:2574
+1042:2:2568
+1043:2:2569
+1044:2:2570
+1045:2:2582
+1046:2:2587
+1047:2:2594
+1048:2:2595
+1049:2:2602
+1050:2:2607
+1051:2:2614
+1052:2:2615
+1053:2:2614
+1054:2:2615
+1055:2:2622
+1056:2:2632
+1057:0:3993
+1058:2:2521
+1059:0:3993
+1060:2:2636
+1061:2:2640
+1062:2:2641
+1063:2:2645
+1064:2:2649
+1065:2:2650
+1066:2:2654
+1067:2:2662
+1068:2:2663
+1069:2:2667
+1070:2:2671
+1071:2:2672
+1072:2:2667
+1073:2:2668
+1074:2:2676
+1075:0:3993
+1076:2:2521
+1077:0:3993
+1078:2:2684
+1079:2:2685
+1080:2:2686
+1081:0:3993
+1082:2:2521
+1083:0:3993
+1084:2:2691
+1085:0:3993
+1086:2:3518
+1087:2:3519
+1088:2:3523
+1089:2:3527
+1090:2:3528
+1091:2:3532
+1092:2:3537
+1093:2:3545
+1094:2:3549
+1095:2:3550
+1096:2:3545
+1097:2:3549
+1098:2:3550
+1099:2:3554
+1100:2:3561
+1101:2:3568
+1102:2:3569
+1103:2:3576
+1104:2:3581
+1105:2:3588
+1106:2:3589
+1107:2:3588
+1108:2:3589
+1109:2:3596
+1110:2:3600
+1111:0:3993
+1112:2:3605
+1113:0:3993
+1114:2:3606
+1115:0:3993
+1116:2:3607
+1117:0:3993
+1118:2:3608
+1119:0:3993
+1120:1:26
+1121:0:3993
+1122:2:3609
+1123:0:3993
+1124:1:30
+1125:1:31
+1126:1:35
+1127:1:39
+1128:1:40
+1129:1:44
+1130:1:52
+1131:1:53
+1132:1:57
+1133:1:61
+1134:1:62
+1135:1:57
+1136:1:61
+1137:1:62
+1138:1:66
+1139:1:73
+1140:1:80
+1141:1:81
+1142:1:88
+1143:1:93
+1144:1:100
+1145:1:101
+1146:1:100
+1147:1:101
+1148:1:108
+1149:1:112
+1150:0:3993
+1151:2:3608
+1152:0:3993
+1153:1:117
+1154:0:3993
+1155:2:3609
+1156:0:3993
+1157:2:3610
+1158:0:3993
+1159:2:3615
+1160:0:3993
+1161:2:3616
+1162:0:3993
+1163:2:3624
+1164:2:3625
+1165:2:3629
+1166:2:3633
+1167:2:3634
+1168:2:3638
+1169:2:3646
+1170:2:3647
+1171:2:3651
+1172:2:3655
+1173:2:3656
+1174:2:3651
+1175:2:3655
+1176:2:3656
+1177:2:3660
+1178:2:3667
+1179:2:3674
+1180:2:3675
+1181:2:3682
+1182:2:3687
+1183:2:3694
+1184:2:3695
+1185:2:3694
+1186:2:3695
+1187:2:3702
+1188:2:3706
+1189:0:3993
+1190:2:2693
+1191:2:3499
+1192:0:3993
+1193:2:2521
+1194:0:3993
+1195:2:2694
+1196:0:3993
+1197:2:2521
+1198:0:3993
+1199:2:2697
+1200:2:2698
+1201:2:2702
+1202:2:2703
+1203:2:2711
+1204:2:2712
+1205:2:2716
+1206:2:2717
+1207:2:2725
+1208:2:2730
+1209:2:2734
+1210:2:2735
+1211:2:2743
+1212:2:2744
+1213:2:2748
+1214:2:2749
+1215:2:2743
+1216:2:2744
+1217:2:2748
+1218:2:2749
+1219:2:2757
+1220:2:2762
+1221:2:2769
+1222:2:2770
+1223:2:2777
+1224:2:2782
+1225:2:2789
+1226:2:2790
+1227:2:2789
+1228:2:2790
+1229:2:2797
+1230:2:2806
+1231:0:3993
+1232:2:2521
+1233:0:3993
+1234:2:2810
+1235:2:2811
+1236:2:2812
+1237:2:2824
+1238:2:2825
+1239:2:2829
+1240:2:2830
+1241:2:2838
+1242:2:2843
+1243:2:2847
+1244:2:2848
+1245:2:2856
+1246:2:2857
+1247:2:2861
+1248:2:2862
+1249:2:2856
+1250:2:2857
+1251:2:2861
+1252:2:2862
+1253:2:2870
+1254:2:2875
+1255:2:2882
+1256:2:2883
+1257:2:2890
+1258:2:2895
+1259:2:2902
+1260:2:2903
+1261:2:2902
+1262:2:2903
+1263:2:2910
+1264:2:2923
+1265:2:2924
+1266:0:3993
+1267:2:2521
+1268:0:3993
+1269:2:3037
+1270:2:3038
+1271:2:3042
+1272:2:3043
+1273:2:3051
+1274:2:3052
+1275:2:3056
+1276:2:3057
+1277:2:3065
+1278:2:3070
+1279:2:3074
+1280:2:3075
+1281:2:3083
+1282:2:3084
+1283:2:3088
+1284:2:3089
+1285:2:3083
+1286:2:3084
+1287:2:3088
+1288:2:3089
+1289:2:3097
+1290:2:3102
+1291:2:3109
+1292:2:3110
+1293:2:3117
+1294:2:3122
+1295:2:3129
+1296:2:3130
+1297:2:3129
+1298:2:3130
+1299:2:3137
+1300:0:3993
+1301:2:2521
+1302:0:3993
+1303:2:3148
+1304:2:3149
+1305:2:3153
+1306:2:3154
+1307:2:3162
+1308:2:3163
+1309:2:3167
+1310:2:3168
+1311:2:3176
+1312:2:3181
+1313:2:3185
+1314:2:3186
+1315:2:3194
+1316:2:3195
+1317:2:3199
+1318:2:3200
+1319:2:3194
+1320:2:3195
+1321:2:3199
+1322:2:3200
+1323:2:3208
+1324:2:3213
+1325:2:3220
+1326:2:3221
+1327:2:3228
+1328:2:3233
+1329:2:3240
+1330:2:3241
+1331:2:3240
+1332:2:3241
+1333:2:3248
+1334:2:3257
+1335:0:3993
+1336:2:2521
+1337:0:3993
+1338:1:118
+1339:0:3993
+1340:1:120
+1341:0:3993
+1342:1:19
+1343:0:3993
+1344:1:126
+1345:1:127
+1346:1:131
+1347:1:132
+1348:1:140
+1349:1:141
+1350:1:145
+1351:1:146
+1352:1:154
+1353:1:159
+1354:1:163
+1355:1:164
+1356:1:172
+1357:1:173
+1358:1:177
+1359:1:178
+1360:1:172
+1361:1:173
+1362:1:177
+1363:1:178
+1364:1:186
+1365:1:191
+1366:1:198
+1367:1:199
+1368:1:206
+1369:1:211
+1370:1:218
+1371:1:219
+1372:1:218
+1373:1:219
+1374:1:226
+1375:0:3993
+1376:1:15
+1377:0:3993
+1378:1:16
+1379:0:3993
+1380:1:17
+1381:0:3993
+1382:1:118
+1383:0:3993
+1384:1:120
+1385:0:3993
+1386:1:19
+1387:0:3993
+1388:1:237
+1389:1:238
+1390:0:3993
+1391:1:15
+1392:0:3993
+1393:1:16
+1394:0:3993
+1395:1:17
+1396:0:3993
+1397:1:118
+1398:0:3993
+1399:1:120
+1400:0:3993
+1401:1:19
+1402:0:3993
+1403:1:244
+1404:1:245
+1405:1:249
+1406:1:250
+1407:1:258
+1408:1:259
+1409:1:263
+1410:1:264
+1411:1:272
+1412:1:277
+1413:1:281
+1414:1:282
+1415:1:290
+1416:1:291
+1417:1:295
+1418:1:296
+1419:1:290
+1420:1:291
+1421:1:295
+1422:1:296
+1423:1:304
+1424:1:309
+1425:1:316
+1426:1:317
+1427:1:324
+1428:1:329
+1429:1:336
+1430:1:337
+1431:1:336
+1432:1:337
+1433:1:344
+1434:0:3993
+1435:1:15
+1436:0:3993
+1437:1:16
+1438:0:3993
+1439:1:17
+1440:0:3993
+1441:1:118
+1442:0:3993
+1443:1:120
+1444:0:3993
+1445:1:19
+1446:0:3993
+1447:1:355
+1448:1:356
+1449:1:360
+1450:1:361
+1451:1:369
+1452:1:370
+1453:1:374
+1454:1:375
+1455:1:383
+1456:1:388
+1457:1:392
+1458:1:393
+1459:1:401
+1460:1:402
+1461:1:406
+1462:1:407
+1463:1:401
+1464:1:402
+1465:1:406
+1466:1:407
+1467:1:415
+1468:1:420
+1469:1:427
+1470:1:428
+1471:1:435
+1472:1:440
+1473:1:447
+1474:1:448
+1475:1:447
+1476:1:448
+1477:1:455
+1478:1:464
+1479:0:3993
+1480:1:15
+1481:0:3993
+1482:1:16
+1483:0:3993
+1484:1:17
+1485:0:3993
+1486:1:118
+1487:0:3993
+1488:1:120
+1489:0:3991
+1490:1:19
+1491:0:3997
+1492:1:1040
+1493:1:1041
+1494:1:1045
+1495:1:1046
+1496:1:1054
+1497:1:1055
+1498:1:1056
+1499:1:1068
+1500:1:1073
+1501:1:1077
+1502:1:1078
+1503:1:1086
+1504:1:1087
+1505:1:1091
+1506:1:1092
+1507:1:1086
+1508:1:1087
+1509:1:1091
+1510:1:1092
+1511:1:1100
+1512:1:1105
+1513:1:1112
+1514:1:1113
+1515:1:1120
+1516:1:1125
+1517:1:1132
+1518:1:1133
+1519:1:1132
+1520:1:1133
+1521:1:1140
+1522:0:3997
+1523:1:15
+1524:0:3997
+1525:1:16
+1526:0:3997
+1527:2:3261
+1528:2:3262
+1529:2:3263
+1530:2:3275
+1531:2:3276
+1532:2:3280
+1533:2:3281
+1534:2:3289
+1535:2:3294
+1536:2:3298
+1537:2:3299
+1538:2:3307
+1539:2:3308
+1540:2:3312
+1541:2:3313
+1542:2:3307
+1543:2:3308
+1544:2:3312
+1545:2:3313
+1546:2:3321
+1547:2:3326
+1548:2:3333
+1549:2:3334
+1550:2:3341
+1551:2:3346
+1552:2:3353
+1553:2:3354
+1554:2:3353
+1555:2:3354
+1556:2:3361
+1557:2:3371
+1558:0:3997
+1559:2:2521
+-1:-1:-1
+1560:0:3997
+1561:2:3377
+1562:2:3378
+1563:2:3382
+1564:2:3383
+1565:2:3391
+1566:2:3392
+1567:2:3396
+1568:2:3397
+1569:2:3405
+1570:2:3410
+1571:2:3414
+1572:2:3415
+1573:2:3423
+1574:2:3424
+1575:2:3428
+1576:2:3429
+1577:2:3423
+1578:2:3424
+1579:2:3428
+1580:2:3429
+1581:2:3437
+1582:2:3442
+1583:2:3449
+1584:2:3450
+1585:2:3457
+1586:2:3462
+1587:2:3469
+1588:2:3470
+1589:2:3469
+1590:2:3470
+1591:2:3477
+1592:0:3997
+1593:2:2521
+1594:0:3997
+1595:2:3261
+1596:2:3262
+1597:2:3266
+1598:2:3267
+1599:2:3275
+1600:2:3276
+1601:2:3280
+1602:2:3281
+1603:2:3289
+1604:2:3294
+1605:2:3298
+1606:2:3299
+1607:2:3307
+1608:2:3308
+1609:2:3312
+1610:2:3313
+1611:2:3307
+1612:2:3308
+1613:2:3312
+1614:2:3313
+1615:2:3321
+1616:2:3326
+1617:2:3333
+1618:2:3334
+1619:2:3341
+1620:2:3346
+1621:2:3353
+1622:2:3354
+1623:2:3353
+1624:2:3354
+1625:2:3361
+1626:2:3371
+1627:0:3997
+1628:2:2521
+1629:0:3997
+1630:2:3377
+1631:2:3378
+1632:2:3382
+1633:2:3383
+1634:2:3391
+1635:2:3392
+1636:2:3396
+1637:2:3397
+1638:2:3405
+1639:2:3410
+1640:2:3414
+1641:2:3415
+1642:2:3423
+1643:2:3424
+1644:2:3428
+1645:2:3429
+1646:2:3423
+1647:2:3424
+1648:2:3428
+1649:2:3429
+1650:2:3437
+1651:2:3442
+1652:2:3449
+1653:2:3450
+1654:2:3457
+1655:2:3462
+1656:2:3469
+1657:2:3470
+1658:2:3469
+1659:2:3470
+1660:2:3477
+1661:0:3997
+1662:2:2521
+1663:0:3997
+1664:2:3261
+1665:2:3262
+1666:2:3266
+1667:2:3267
+1668:2:3275
+1669:2:3276
+1670:2:3280
+1671:2:3281
+1672:2:3289
+1673:2:3294
+1674:2:3298
+1675:2:3299
+1676:2:3307
+1677:2:3308
+1678:2:3312
+1679:2:3313
+1680:2:3307
+1681:2:3308
+1682:2:3312
+1683:2:3313
+1684:2:3321
+1685:2:3326
+1686:2:3333
+1687:2:3334
+1688:2:3341
+1689:2:3346
+1690:2:3353
+1691:2:3354
+1692:2:3353
+1693:2:3354
+1694:2:3361
+1695:2:3371
+1696:0:3997
+1697:2:2521