Add verif results

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

diff --git a/formal-model/urcu-controldataflow-intel-ipi-compress/urcu_progress_writer_error.spin.input.trail b/formal-model/urcu-controldataflow-intel-ipi-compress/urcu_progress_writer_error.spin.input.trail
new file mode 100644 (file)
index 0000000..e9b06b3
--- /dev/null
+++ b/formal-model/urcu-controldataflow-intel-ipi-compress/urcu_progress_writer_error.spin.input.trail
@@ -0,0 +1,1699 @@
+-2:3:-2
+-4:-4:-4
+1:0:3997
+2:2:2536
+3:2:2541
+4:2:2545
+5:2:2553
+6:2:2557
+7:2:2561
+8:0:3997
+9:1:0
+10:1:5
+11:1:9
+12:1:17
+13:1:21
+14:1:25
+15:0:3997
+16:3:3967
+17:3:3970
+18:3:3977
+19:3:3984
+20:3:3987
+21:3:3991
+22:3:3992
+23:0:3997
+24:3:3994
+25:0:3997
+26:2:2565
+27:0:3997
+28:2:2571
+29:0:3997
+30:2:2572
+31:0:3997
+32:2:2573
+33:0:3997
+34:2:2574
+35:0:3997
+36:2:2575
+37:0:3997
+38:2:2576
+39:2:2577
+40:2:2581
+41:2:2582
+42:2:2590
+43:2:2591
+44:2:2595
+45:2:2596
+46:2:2604
+47:2:2609
+48:2:2613
+49:2:2614
+50:2:2622
+51:2:2623
+52:2:2627
+53:2:2628
+54:2:2622
+55:2:2623
+56:2:2627
+57:2:2628
+58:2:2636
+59:2:2641
+60:2:2648
+61:2:2649
+62:2:2656
+63:2:2661
+64:2:2668
+65:2:2669
+66:2:2668
+67:2:2669
+68:2:2676
+69:2:2686
+70:0:3997
+71:2:2575
+72:0:3997
+73:2:2690
+74:2:2694
+75:2:2695
+76:2:2699
+77:2:2703
+78:2:2704
+79:2:2708
+80:2:2716
+81:2:2717
+82:2:2721
+83:2:2725
+84:2:2726
+85:2:2721
+86:2:2722
+87:2:2730
+88:0:3997
+89:2:2575
+90:0:3997
+91:2:2738
+92:2:2739
+93:2:2740
+94:0:3997
+95:2:2575
+96:0:3997
+97:2:2745
+98:0:3997
+99:2:3572
+100:2:3573
+101:2:3577
+102:2:3581
+103:2:3582
+104:2:3586
+105:2:3591
+106:2:3599
+107:2:3603
+108:2:3604
+109:2:3599
+110:2:3603
+111:2:3604
+112:2:3608
+113:2:3615
+114:2:3622
+115:2:3623
+116:2:3630
+117:2:3635
+118:2:3642
+119:2:3643
+120:2:3642
+121:2:3643
+122:2:3650
+123:2:3654
+124:0:3997
+125:2:3659
+126:0:3997
+127:2:3660
+128:0:3997
+129:2:3661
+130:0:3997
+131:2:3662
+132:0:3997
+133:1:29
+134:0:3997
+135:1:35
+136:0:3997
+137:1:36
+138:0:3997
+139:2:3663
+140:0:3997
+141:1:37
+142:0:3997
+143:2:3662
+144:0:3997
+145:1:38
+146:0:3997
+147:2:3663
+148:0:3997
+149:1:39
+150:0:3997
+151:2:3662
+152:0:3997
+153:1:40
+154:0:3997
+155:2:3663
+156:0:3997
+157:1:41
+158:0:3997
+159:1:42
+160:0:3997
+161:1:43
+162:0:3997
+163:2:3662
+164:0:3997
+165:1:44
+166:0:3997
+167:2:3663
+168:0:3997
+169:1:53
+170:0:3997
+171:2:3662
+172:0:3997
+173:1:57
+174:1:58
+175:1:62
+176:1:66
+177:1:67
+178:1:71
+179:1:79
+180:1:80
+181:1:84
+182:1:88
+183:1:89
+184:1:84
+185:1:88
+186:1:89
+187:1:93
+188:1:100
+189:1:107
+190:1:108
+191:1:115
+192:1:120
+193:1:127
+194:1:128
+195:1:127
+196:1:128
+197:1:135
+198:1:139
+199:0:3997
+200:2:3663
+201:0:3997
+202:1:144
+203:0:3997
+204:2:3664
+205:0:3997
+206:2:3669
+207:0:3997
+208:2:3670
+209:0:3997
+210:2:3678
+211:2:3679
+212:2:3683
+213:2:3687
+214:2:3688
+215:2:3692
+216:2:3700
+217:2:3701
+218:2:3705
+219:2:3709
+220:2:3710
+221:2:3705
+222:2:3709
+223:2:3710
+224:2:3714
+225:2:3721
+226:2:3728
+227:2:3729
+228:2:3736
+229:2:3741
+230:2:3748
+231:2:3749
+232:2:3748
+233:2:3749
+234:2:3756
+235:2:3760
+236:0:3997
+237:2:2747
+238:2:3553
+239:0:3997
+240:2:2575
+241:0:3997
+242:2:2748
+243:0:3997
+244:2:2575
+245:0:3997
+246:2:2751
+247:2:2752
+248:2:2756
+249:2:2757
+250:2:2765
+251:2:2766
+252:2:2770
+253:2:2771
+254:2:2779
+255:2:2784
+256:2:2788
+257:2:2789
+258:2:2797
+259:2:2798
+260:2:2802
+261:2:2803
+262:2:2797
+263:2:2798
+264:2:2802
+265:2:2803
+266:2:2811
+267:2:2816
+268:2:2823
+269:2:2824
+270:2:2831
+271:2:2836
+272:2:2843
+273:2:2844
+274:2:2843
+275:2:2844
+276:2:2851
+277:2:2860
+278:0:3997
+279:2:2575
+280:0:3997
+281:2:2864
+282:2:2865
+283:2:2866
+284:2:2878
+285:2:2879
+286:2:2883
+287:2:2884
+288:2:2892
+289:2:2897
+290:2:2901
+291:2:2902
+292:2:2910
+293:2:2911
+294:2:2915
+295:2:2916
+296:2:2910
+297:2:2911
+298:2:2915
+299:2:2916
+300:2:2924
+301:2:2929
+302:2:2936
+303:2:2937
+304:2:2944
+305:2:2949
+306:2:2956
+307:2:2957
+308:2:2956
+309:2:2957
+310:2:2964
+311:2:2977
+312:2:2978
+313:0:3997
+314:2:2575
+315:0:3997
+316:2:3091
+317:2:3092
+318:2:3096
+319:2:3097
+320:2:3105
+321:2:3106
+322:2:3110
+323:2:3111
+324:2:3119
+325:2:3124
+326:2:3128
+327:2:3129
+328:2:3137
+329:2:3138
+330:2:3142
+331:2:3143
+332:2:3137
+333:2:3138
+334:2:3142
+335:2:3143
+336:2:3151
+337:2:3156
+338:2:3163
+339:2:3164
+340:2:3171
+341:2:3176
+342:2:3183
+343:2:3184
+344:2:3183
+345:2:3184
+346:2:3191
+347:0:3997
+348:2:2575
+349:0:3997
+350:2:3202
+351:2:3203
+352:2:3207
+353:2:3208
+354:2:3216
+355:2:3217
+356:2:3221
+357:2:3222
+358:2:3230
+359:2:3235
+360:2:3239
+361:2:3240
+362:2:3248
+363:2:3249
+364:2:3253
+365:2:3254
+366:2:3248
+367:2:3249
+368:2:3253
+369:2:3254
+370:2:3262
+371:2:3267
+372:2:3274
+373:2:3275
+374:2:3282
+375:2:3287
+376:2:3294
+377:2:3295
+378:2:3294
+379:2:3295
+380:2:3302
+381:2:3311
+382:0:3997
+383:2:2575
+384:0:3997
+385:2:3315
+386:2:3316
+387:2:3317
+388:2:3329
+389:2:3330
+390:2:3334
+391:2:3335
+392:2:3343
+393:2:3348
+394:2:3352
+395:2:3353
+396:2:3361
+397:2:3362
+398:2:3366
+399:2:3367
+400:2:3361
+401:2:3362
+402:2:3366
+403:2:3367
+404:2:3375
+405:2:3380
+406:2:3387
+407:2:3388
+408:2:3395
+409:2:3400
+410:2:3407
+411:2:3408
+412:2:3407
+413:2:3408
+414:2:3415
+415:2:3427
+416:2:3428
+417:0:3997
+418:2:2575
+419:0:3997
+420:2:3541
+421:0:3997
+422:2:3770
+423:2:3771
+424:2:3775
+425:2:3779
+426:2:3780
+427:2:3784
+428:2:3792
+429:2:3793
+430:2:3797
+431:2:3801
+432:2:3802
+433:2:3797
+434:2:3801
+435:2:3802
+436:2:3806
+437:2:3813
+438:2:3820
+439:2:3821
+440:2:3828
+441:2:3833
+442:2:3840
+443:2:3841
+444:2:3840
+445:2:3841
+446:2:3848
+447:2:3852
+448:0:3997
+449:2:3857
+450:0:3997
+451:2:3858
+452:0:3997
+453:2:3859
+454:0:3997
+455:2:3860
+456:0:3997
+457:1:53
+458:0:3997
+459:2:3861
+460:0:3997
+461:1:57
+462:1:58
+463:1:62
+464:1:66
+465:1:67
+466:1:71
+467:1:79
+468:1:80
+469:1:84
+470:1:88
+471:1:89
+472:1:84
+473:1:88
+474:1:89
+475:1:93
+476:1:100
+477:1:107
+478:1:108
+479:1:115
+480:1:120
+481:1:127
+482:1:128
+483:1:127
+484:1:128
+485:1:135
+486:1:139
+487:0:3997
+488:2:3860
+489:0:3997
+490:1:144
+491:0:3997
+492:2:3861
+493:0:3997
+494:2:3862
+495:0:3997
+496:2:3867
+497:0:3997
+498:2:3868
+499:0:3997
+500:2:3876
+501:2:3877
+502:2:3881
+503:2:3885
+504:2:3886
+505:2:3890
+506:2:3898
+507:2:3899
+508:2:3903
+509:2:3907
+510:2:3908
+511:2:3903
+512:2:3907
+513:2:3908
+514:2:3912
+515:2:3919
+516:2:3926
+517:2:3927
+518:2:3934
+519:2:3939
+520:2:3946
+521:2:3947
+522:2:3946
+523:2:3947
+524:2:3954
+525:2:3958
+526:0:3997
+527:2:3543
+528:2:3553
+529:0:3997
+530:2:2575
+531:0:3997
+532:2:3544
+533:2:3545
+534:0:3997
+535:2:2575
+536:0:3997
+537:2:3549
+538:0:3997
+539:2:3557
+540:0:3997
+541:2:2572
+542:0:3997
+543:2:2573
+544:0:3997
+545:2:2574
+546:0:3997
+547:2:2575
+548:0:3997
+549:2:2576
+550:2:2577
+551:2:2581
+552:2:2582
+553:2:2590
+554:2:2591
+555:2:2595
+556:2:2596
+557:2:2604
+558:2:2609
+559:2:2613
+560:2:2614
+561:2:2622
+562:2:2623
+563:2:2624
+564:2:2622
+565:2:2623
+566:2:2627
+567:2:2628
+568:2:2636
+569:2:2641
+570:2:2648
+571:2:2649
+572:2:2656
+573:2:2661
+574:2:2668
+575:2:2669
+576:2:2668
+577:2:2669
+578:2:2676
+579:2:2686
+580:0:3997
+581:2:2575
+582:0:3997
+583:2:2690
+584:2:2694
+585:2:2695
+586:2:2699
+587:2:2703
+588:2:2704
+589:2:2708
+590:2:2716
+591:2:2717
+592:2:2721
+593:2:2722
+594:2:2721
+595:2:2725
+596:2:2726
+597:2:2730
+598:0:3997
+599:2:2575
+600:0:3997
+601:2:2738
+602:2:2739
+603:2:2740
+604:0:3997
+605:2:2575
+606:0:3997
+607:2:2745
+608:0:3997
+609:2:3572
+610:2:3573
+611:2:3577
+612:2:3581
+613:2:3582
+614:2:3586
+615:2:3591
+616:2:3599
+617:2:3603
+618:2:3604
+619:2:3599
+620:2:3603
+621:2:3604
+622:2:3608
+623:2:3615
+624:2:3622
+625:2:3623
+626:2:3630
+627:2:3635
+628:2:3642
+629:2:3643
+630:2:3642
+631:2:3643
+632:2:3650
+633:2:3654
+634:0:3997
+635:2:3659
+636:0:3997
+637:2:3660
+638:0:3997
+639:2:3661
+640:0:3997
+641:2:3662
+642:0:3997
+643:1:53
+644:0:3997
+645:2:3663
+646:0:3997
+647:1:57
+648:1:58
+649:1:62
+650:1:66
+651:1:67
+652:1:71
+653:1:79
+654:1:80
+655:1:84
+656:1:88
+657:1:89
+658:1:84
+659:1:88
+660:1:89
+661:1:93
+662:1:100
+663:1:107
+664:1:108
+665:1:115
+666:1:120
+667:1:127
+668:1:128
+669:1:127
+670:1:128
+671:1:135
+672:1:139
+673:0:3997
+674:2:3662
+675:0:3997
+676:1:144
+677:0:3997
+678:2:3663
+679:0:3997
+680:2:3664
+681:0:3997
+682:2:3669
+683:0:3997
+684:2:3670
+685:0:3997
+686:2:3678
+687:2:3679
+688:2:3683
+689:2:3687
+690:2:3688
+691:2:3692
+692:2:3700
+693:2:3701
+694:2:3705
+695:2:3709
+696:2:3710
+697:2:3705
+698:2:3709
+699:2:3710
+700:2:3714
+701:2:3721
+702:2:3728
+703:2:3729
+704:2:3736
+705:2:3741
+706:2:3748
+707:2:3749
+708:2:3748
+709:2:3749
+710:2:3756
+711:2:3760
+712:0:3997
+713:2:2747
+714:2:3553
+715:0:3997
+716:2:2575
+717:0:3997
+718:2:2748
+719:0:3997
+720:2:2575
+721:0:3997
+722:2:2751
+723:2:2752
+724:2:2756
+725:2:2757
+726:2:2765
+727:2:2766
+728:2:2770
+729:2:2771
+730:2:2779
+731:2:2784
+732:2:2788
+733:2:2789
+734:2:2797
+735:2:2798
+736:2:2802
+737:2:2803
+738:2:2797
+739:2:2798
+740:2:2802
+741:2:2803
+742:2:2811
+743:2:2816
+744:2:2823
+745:2:2824
+746:2:2831
+747:2:2836
+748:2:2843
+749:2:2844
+750:2:2843
+751:2:2844
+752:2:2851
+753:2:2860
+754:0:3997
+755:2:2575
+756:0:3997
+757:2:2864
+758:2:2865
+759:2:2866
+760:2:2878
+761:2:2879
+762:2:2883
+763:2:2884
+764:2:2892
+765:2:2897
+766:2:2901
+767:2:2902
+768:2:2910
+769:2:2911
+770:2:2915
+771:2:2916
+772:2:2910
+773:2:2911
+774:2:2915
+775:2:2916
+776:2:2924
+777:2:2929
+778:2:2936
+779:2:2937
+780:2:2944
+781:2:2949
+782:2:2956
+783:2:2957
+784:2:2956
+785:2:2957
+786:2:2964
+787:2:2977
+788:2:2978
+789:0:3997
+790:2:2575
+791:0:3997
+792:2:3091
+793:2:3092
+794:2:3096
+795:2:3097
+796:2:3105
+797:2:3106
+798:2:3110
+799:2:3111
+800:2:3119
+801:2:3124
+802:2:3128
+803:2:3129
+804:2:3137
+805:2:3138
+806:2:3142
+807:2:3143
+808:2:3137
+809:2:3138
+810:2:3142
+811:2:3143
+812:2:3151
+813:2:3156
+814:2:3163
+815:2:3164
+816:2:3171
+817:2:3176
+818:2:3183
+819:2:3184
+820:2:3183
+821:2:3184
+822:2:3191
+823:0:3997
+824:2:2575
+825:0:3997
+826:2:3202
+827:2:3203
+828:2:3207
+829:2:3208
+830:2:3216
+831:2:3217
+832:2:3221
+833:2:3222
+834:2:3230
+835:2:3235
+836:2:3239
+837:2:3240
+838:2:3248
+839:2:3249
+840:2:3253
+841:2:3254
+842:2:3248
+843:2:3249
+844:2:3253
+845:2:3254
+846:2:3262
+847:2:3267
+848:2:3274
+849:2:3275
+850:2:3282
+851:2:3287
+852:2:3294
+853:2:3295
+854:2:3294
+855:2:3295
+856:2:3302
+857:2:3311
+858:0:3997
+859:2:2575
+860:0:3997
+861:2:3315
+862:2:3316
+863:2:3317
+864:2:3329
+865:2:3330
+866:2:3334
+867:2:3335
+868:2:3343
+869:2:3348
+870:2:3352
+871:2:3353
+872:2:3361
+873:2:3362
+874:2:3366
+875:2:3367
+876:2:3361
+877:2:3362
+878:2:3366
+879:2:3367
+880:2:3375
+881:2:3380
+882:2:3387
+883:2:3388
+884:2:3395
+885:2:3400
+886:2:3407
+887:2:3408
+888:2:3407
+889:2:3408
+890:2:3415
+891:2:3427
+892:2:3428
+893:0:3997
+894:2:2575
+895:0:3997
+896:2:3541
+897:0:3997
+898:2:3770
+899:2:3771
+900:2:3775
+901:2:3779
+902:2:3780
+903:2:3784
+904:2:3792
+905:2:3793
+906:2:3797
+907:2:3801
+908:2:3802
+909:2:3797
+910:2:3801
+911:2:3802
+912:2:3806
+913:2:3813
+914:2:3820
+915:2:3821
+916:2:3828
+917:2:3833
+918:2:3840
+919:2:3841
+920:2:3840
+921:2:3841
+922:2:3848
+923:2:3852
+924:0:3997
+925:2:3857
+926:0:3997
+927:2:3858
+928:0:3997
+929:2:3859
+930:0:3997
+931:2:3860
+932:0:3997
+933:1:53
+934:0:3997
+935:2:3861
+936:0:3997
+937:1:57
+938:1:58
+939:1:62
+940:1:66
+941:1:67
+942:1:71
+943:1:79
+944:1:80
+945:1:84
+946:1:88
+947:1:89
+948:1:84
+949:1:88
+950:1:89
+951:1:93
+952:1:100
+953:1:107
+954:1:108
+955:1:115
+956:1:120
+957:1:127
+958:1:128
+959:1:127
+960:1:128
+961:1:135
+962:1:139
+963:0:3997
+964:2:3860
+965:0:3997
+966:1:144
+967:0:3997
+968:2:3861
+969:0:3997
+970:2:3862
+971:0:3997
+972:2:3867
+973:0:3997
+974:2:3868
+975:0:3997
+976:2:3876
+977:2:3877
+978:2:3881
+979:2:3885
+980:2:3886
+981:2:3890
+982:2:3898
+983:2:3899
+984:2:3903
+985:2:3907
+986:2:3908
+987:2:3903
+988:2:3907
+989:2:3908
+990:2:3912
+991:2:3919
+992:2:3926
+993:2:3927
+994:2:3934
+995:2:3939
+996:2:3946
+997:2:3947
+998:2:3946
+999:2:3947
+1000:2:3954
+1001:2:3958
+1002:0:3997
+1003:2:3543
+1004:2:3553
+1005:0:3997
+1006:2:2575
+1007:0:3997
+1008:2:3544
+1009:2:3545
+1010:0:3997
+1011:2:2575
+1012:0:3997
+1013:2:3549
+1014:0:3997
+1015:2:3557
+1016:0:3997
+1017:2:2572
+1018:0:3997
+1019:2:2573
+1020:0:3997
+1021:2:2574
+1022:0:3997
+1023:2:2575
+1024:0:3997
+1025:2:2576
+1026:2:2577
+1027:2:2581
+1028:2:2582
+1029:2:2590
+1030:2:2591
+1031:2:2595
+1032:2:2596
+1033:2:2604
+1034:2:2609
+1035:2:2613
+1036:2:2614
+1037:2:2622
+1038:2:2623
+1039:2:2627
+1040:2:2628
+1041:2:2622
+1042:2:2623
+1043:2:2624
+1044:2:2636
+1045:2:2641
+1046:2:2648
+1047:2:2649
+1048:2:2656
+1049:2:2661
+1050:2:2668
+1051:2:2669
+1052:2:2668
+1053:2:2669
+1054:2:2676
+1055:2:2686
+1056:0:3997
+1057:2:2575
+1058:0:3997
+1059:2:2690
+1060:2:2694
+1061:2:2695
+1062:2:2699
+1063:2:2703
+1064:2:2704
+1065:2:2708
+1066:2:2716
+1067:2:2717
+1068:2:2721
+1069:2:2725
+1070:2:2726
+1071:2:2721
+1072:2:2722
+1073:2:2730
+1074:0:3997
+1075:2:2575
+1076:0:3997
+1077:2:2738
+1078:2:2739
+1079:2:2740
+1080:0:3997
+1081:2:2575
+1082:0:3997
+1083:2:2745
+1084:0:3997
+1085:2:3572
+1086:2:3573
+1087:2:3577
+1088:2:3581
+1089:2:3582
+1090:2:3586
+1091:2:3591
+1092:2:3599
+1093:2:3603
+1094:2:3604
+1095:2:3599
+1096:2:3603
+1097:2:3604
+1098:2:3608
+1099:2:3615
+1100:2:3622
+1101:2:3623
+1102:2:3630
+1103:2:3635
+1104:2:3642
+1105:2:3643
+1106:2:3642
+1107:2:3643
+1108:2:3650
+1109:2:3654
+1110:0:3997
+1111:2:3659
+1112:0:3997
+1113:2:3660
+1114:0:3997
+1115:2:3661
+1116:0:3997
+1117:2:3662
+1118:0:3997
+1119:1:53
+1120:0:3997
+1121:2:3663
+1122:0:3997
+1123:1:57
+1124:1:58
+1125:1:62
+1126:1:66
+1127:1:67
+1128:1:71
+1129:1:79
+1130:1:80
+1131:1:84
+1132:1:88
+1133:1:89
+1134:1:84
+1135:1:88
+1136:1:89
+1137:1:93
+1138:1:100
+1139:1:107
+1140:1:108
+1141:1:115
+1142:1:120
+1143:1:127
+1144:1:128
+1145:1:127
+1146:1:128
+1147:1:135
+1148:1:139
+1149:0:3997
+1150:2:3662
+1151:0:3997
+1152:1:144
+1153:0:3997
+1154:2:3663
+1155:0:3997
+1156:2:3664
+1157:0:3997
+1158:2:3669
+1159:0:3997
+1160:2:3670
+1161:0:3997
+1162:2:3678
+1163:2:3679
+1164:2:3683
+1165:2:3687
+1166:2:3688
+1167:2:3692
+1168:2:3700
+1169:2:3701
+1170:2:3705
+1171:2:3709
+1172:2:3710
+1173:2:3705
+1174:2:3709
+1175:2:3710
+1176:2:3714
+1177:2:3721
+1178:2:3728
+1179:2:3729
+1180:2:3736
+1181:2:3741
+1182:2:3748
+1183:2:3749
+1184:2:3748
+1185:2:3749
+1186:2:3756
+1187:2:3760
+1188:0:3997
+1189:2:2747
+1190:2:3553
+1191:0:3997
+1192:2:2575
+1193:0:3997
+1194:2:2748
+1195:0:3997
+1196:2:2575
+1197:0:3997
+1198:2:2751
+1199:2:2752
+1200:2:2756
+1201:2:2757
+1202:2:2765
+1203:2:2766
+1204:2:2770
+1205:2:2771
+1206:2:2779
+1207:2:2784
+1208:2:2788
+1209:2:2789
+1210:2:2797
+1211:2:2798
+1212:2:2802
+1213:2:2803
+1214:2:2797
+1215:2:2798
+1216:2:2802
+1217:2:2803
+1218:2:2811
+1219:2:2816
+1220:2:2823
+1221:2:2824
+1222:2:2831
+1223:2:2836
+1224:2:2843
+1225:2:2844
+1226:2:2843
+1227:2:2844
+1228:2:2851
+1229:2:2860
+1230:0:3997
+1231:2:2575
+1232:0:3997
+1233:2:2864
+1234:2:2865
+1235:2:2866
+1236:2:2878
+1237:2:2879
+1238:2:2883
+1239:2:2884
+1240:2:2892
+1241:2:2897
+1242:2:2901
+1243:2:2902
+1244:2:2910
+1245:2:2911
+1246:2:2915
+1247:2:2916
+1248:2:2910
+1249:2:2911
+1250:2:2915
+1251:2:2916
+1252:2:2924
+1253:2:2929
+1254:2:2936
+1255:2:2937
+1256:2:2944
+1257:2:2949
+1258:2:2956
+1259:2:2957
+1260:2:2956
+1261:2:2957
+1262:2:2964
+1263:2:2977
+1264:2:2978
+1265:0:3997
+1266:2:2575
+1267:0:3997
+1268:2:3091
+1269:2:3092
+1270:2:3096
+1271:2:3097
+1272:2:3105
+1273:2:3106
+1274:2:3110
+1275:2:3111
+1276:2:3119
+1277:2:3124
+1278:2:3128
+1279:2:3129
+1280:2:3137
+1281:2:3138
+1282:2:3142
+1283:2:3143
+1284:2:3137
+1285:2:3138
+1286:2:3142
+1287:2:3143
+1288:2:3151
+1289:2:3156
+1290:2:3163
+1291:2:3164
+1292:2:3171
+1293:2:3176
+1294:2:3183
+1295:2:3184
+1296:2:3183
+1297:2:3184
+1298:2:3191
+1299:0:3997
+1300:2:2575
+1301:0:3997
+1302:2:3202
+1303:2:3203
+1304:2:3207
+1305:2:3208
+1306:2:3216
+1307:2:3217
+1308:2:3221
+1309:2:3222
+1310:2:3230
+1311:2:3235
+1312:2:3239
+1313:2:3240
+1314:2:3248
+1315:2:3249
+1316:2:3253
+1317:2:3254
+1318:2:3248
+1319:2:3249
+1320:2:3253
+1321:2:3254
+1322:2:3262
+1323:2:3267
+1324:2:3274
+1325:2:3275
+1326:2:3282
+1327:2:3287
+1328:2:3294
+1329:2:3295
+1330:2:3294
+1331:2:3295
+1332:2:3302
+1333:2:3311
+1334:0:3997
+1335:2:2575
+1336:0:3997
+1337:1:145
+1338:0:3997
+1339:1:147
+1340:0:3997
+1341:1:46
+1342:0:3997
+1343:1:153
+1344:1:154
+1345:1:158
+1346:1:159
+1347:1:167
+1348:1:168
+1349:1:172
+1350:1:173
+1351:1:181
+1352:1:186
+1353:1:190
+1354:1:191
+1355:1:199
+1356:1:200
+1357:1:204
+1358:1:205
+1359:1:199
+1360:1:200
+1361:1:204
+1362:1:205
+1363:1:213
+1364:1:218
+1365:1:225
+1366:1:226
+1367:1:233
+1368:1:238
+1369:1:245
+1370:1:246
+1371:1:245
+1372:1:246
+1373:1:253
+1374:0:3997
+1375:1:42
+1376:0:3997
+1377:1:43
+1378:0:3997
+1379:1:44
+1380:0:3997
+1381:1:145
+1382:0:3997
+1383:1:147
+1384:0:3997
+1385:1:46
+1386:0:3997
+1387:1:264
+1388:1:265
+1389:0:3997
+1390:1:42
+1391:0:3997
+1392:1:43
+1393:0:3997
+1394:1:44
+1395:0:3997
+1396:1:145
+1397:0:3997
+1398:1:147
+1399:0:3997
+1400:1:46
+1401:0:3997
+1402:1:271
+1403:1:272
+1404:1:276
+1405:1:277
+1406:1:285
+1407:1:286
+1408:1:290
+1409:1:291
+1410:1:299
+1411:1:304
+1412:1:308
+1413:1:309
+1414:1:317
+1415:1:318
+1416:1:322
+1417:1:323
+1418:1:317
+1419:1:318
+1420:1:322
+1421:1:323
+1422:1:331
+1423:1:336
+1424:1:343
+1425:1:344
+1426:1:351
+1427:1:356
+1428:1:363
+1429:1:364
+1430:1:363
+1431:1:364
+1432:1:371
+1433:0:3997
+1434:1:42
+1435:0:3997
+1436:1:43
+1437:0:3997
+1438:1:44
+1439:0:3997
+1440:1:145
+1441:0:3997
+1442:1:147
+1443:0:3997
+1444:1:46
+1445:0:3997
+1446:1:382
+1447:1:383
+1448:1:387
+1449:1:388
+1450:1:396
+1451:1:397
+1452:1:401
+1453:1:402
+1454:1:410
+1455:1:415
+1456:1:419
+1457:1:420
+1458:1:428
+1459:1:429
+1460:1:433
+1461:1:434
+1462:1:428
+1463:1:429
+1464:1:433
+1465:1:434
+1466:1:442
+1467:1:447
+1468:1:454
+1469:1:455
+1470:1:462
+1471:1:467
+1472:1:474
+1473:1:475
+1474:1:474
+1475:1:475
+1476:1:482
+1477:1:491
+1478:0:3997
+1479:1:42
+1480:0:3997
+1481:1:43
+1482:0:3997
+1483:1:44
+1484:0:3997
+1485:1:145
+1486:0:3997
+1487:1:147
+1488:0:3995
+1489:1:46
+1490:0:4001
+1491:1:1067
+1492:1:1068
+1493:1:1072
+1494:1:1073
+1495:1:1081
+1496:1:1082
+1497:1:1083
+1498:1:1095
+1499:1:1100
+1500:1:1104
+1501:1:1105
+1502:1:1113
+1503:1:1114
+1504:1:1118
+1505:1:1119
+1506:1:1113
+1507:1:1114
+1508:1:1118
+1509:1:1119
+1510:1:1127
+1511:1:1132
+1512:1:1139
+1513:1:1140
+1514:1:1147
+1515:1:1152
+1516:1:1159
+1517:1:1160
+1518:1:1159
+1519:1:1160
+1520:1:1167
+1521:0:4001
+1522:1:42
+1523:0:4001
+1524:1:43
+1525:0:4001
+1526:2:3315
+1527:2:3316
+1528:2:3317
+1529:2:3329
+1530:2:3330
+1531:2:3334
+1532:2:3335
+1533:2:3343
+1534:2:3348
+1535:2:3352
+1536:2:3353
+1537:2:3361
+1538:2:3362
+1539:2:3366
+1540:2:3367
+1541:2:3361
+1542:2:3362
+1543:2:3366
+1544:2:3367
+1545:2:3375
+1546:2:3380
+1547:2:3387
+1548:2:3388
+1549:2:3395
+1550:2:3400
+1551:2:3407
+1552:2:3408
+1553:2:3407
+1554:2:3408
+1555:2:3415
+1556:2:3425
+1557:0:4001
+1558:2:2575
+-1:-1:-1
+1559:0:4001
+1560:2:3431
+1561:2:3432
+1562:2:3436
+1563:2:3437
+1564:2:3445
+1565:2:3446
+1566:2:3450
+1567:2:3451
+1568:2:3459
+1569:2:3464
+1570:2:3468
+1571:2:3469
+1572:2:3477
+1573:2:3478
+1574:2:3482
+1575:2:3483
+1576:2:3477
+1577:2:3478
+1578:2:3482
+1579:2:3483
+1580:2:3491
+1581:2:3496
+1582:2:3503
+1583:2:3504
+1584:2:3511
+1585:2:3516
+1586:2:3523
+1587:2:3524
+1588:2:3523
+1589:2:3524
+1590:2:3531
+1591:0:4001
+1592:2:2575
+1593:0:4001
+1594:2:3315
+1595:2:3316
+1596:2:3320
+1597:2:3321
+1598:2:3329
+1599:2:3330
+1600:2:3334
+1601:2:3335
+1602:2:3343
+1603:2:3348
+1604:2:3352
+1605:2:3353
+1606:2:3361
+1607:2:3362
+1608:2:3366
+1609:2:3367
+1610:2:3361
+1611:2:3362
+1612:2:3366
+1613:2:3367
+1614:2:3375
+1615:2:3380
+1616:2:3387
+1617:2:3388
+1618:2:3395
+1619:2:3400
+1620:2:3407
+1621:2:3408
+1622:2:3407
+1623:2:3408
+1624:2:3415
+1625:2:3425
+1626:0:4001
+1627:2:2575
+1628:0:4001
+1629:2:3431
+1630:2:3432
+1631:2:3436
+1632:2:3437
+1633:2:3445
+1634:2:3446
+1635:2:3450
+1636:2:3451
+1637:2:3459
+1638:2:3464
+1639:2:3468
+1640:2:3469
+1641:2:3477
+1642:2:3478
+1643:2:3482
+1644:2:3483
+1645:2:3477
+1646:2:3478
+1647:2:3482
+1648:2:3483
+1649:2:3491
+1650:2:3496
+1651:2:3503
+1652:2:3504
+1653:2:3511
+1654:2:3516
+1655:2:3523
+1656:2:3524
+1657:2:3523
+1658:2:3524
+1659:2:3531
+1660:0:4001
+1661:2:2575
+1662:0:4001
+1663:2:3315
+1664:2:3316
+1665:2:3320
+1666:2:3321
+1667:2:3329
+1668:2:3330
+1669:2:3334
+1670:2:3335
+1671:2:3343
+1672:2:3348
+1673:2:3352
+1674:2:3353
+1675:2:3361
+1676:2:3362
+1677:2:3366
+1678:2:3367
+1679:2:3361
+1680:2:3362
+1681:2:3366
+1682:2:3367
+1683:2:3375
+1684:2:3380
+1685:2:3387
+1686:2:3388
+1687:2:3395
+1688:2:3400
+1689:2:3407
+1690:2:3408
+1691:2:3407
+1692:2:3408
+1693:2:3415
+1694:2:3425
+1695:0:4001
+1696:2:2575