Add verif results

[urcu.git] / formal-model / urcu-controldataflow-intel-no-ipi / urcu_free_no_wmb.spin.input.trail

diff --git a/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_wmb.spin.input.trail b/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_wmb.spin.input.trail
new file mode 100644 (file)
index 0000000..aca9da8
--- /dev/null
+++ b/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1298 @@
+-2:3:-2
+-4:-4:-4
+1:0:3995
+2:3:3915
+3:3:3918
+4:3:3918
+5:3:3921
+6:3:3929
+7:3:3929
+8:3:3932
+9:3:3938
+10:3:3942
+11:3:3942
+12:3:3945
+13:3:3955
+14:3:3963
+15:3:3963
+16:3:3966
+17:3:3972
+18:3:3976
+19:3:3976
+20:3:3979
+21:3:3985
+22:3:3989
+23:3:3990
+24:0:3995
+25:3:3992
+26:0:3995
+27:2:2757
+28:0:3995
+29:2:2763
+30:0:3995
+31:2:2764
+32:0:3995
+33:2:2766
+34:0:3995
+35:2:2767
+36:0:3995
+37:2:2768
+38:0:3995
+39:2:2769
+40:2:2770
+41:2:2774
+42:2:2775
+43:2:2783
+44:2:2784
+45:2:2788
+46:2:2789
+47:2:2797
+48:2:2802
+49:2:2806
+50:2:2807
+51:2:2815
+52:2:2816
+53:2:2820
+54:2:2821
+55:2:2815
+56:2:2816
+57:2:2820
+58:2:2821
+59:2:2829
+60:2:2834
+61:2:2841
+62:2:2842
+63:2:2849
+64:2:2854
+65:2:2861
+66:2:2862
+67:2:2861
+68:2:2862
+69:2:2869
+70:2:2879
+71:0:3995
+72:2:2768
+73:0:3995
+74:2:2931
+75:2:2932
+76:2:2933
+77:0:3995
+78:2:2768
+79:0:3995
+80:2:2938
+81:0:3995
+82:2:3552
+83:2:3553
+84:2:3557
+85:2:3561
+86:2:3562
+87:2:3566
+88:2:3571
+89:2:3579
+90:2:3583
+91:2:3584
+92:2:3579
+93:2:3580
+94:2:3588
+95:2:3595
+96:2:3602
+97:2:3603
+98:2:3610
+99:2:3615
+100:2:3622
+101:2:3623
+102:2:3622
+103:2:3623
+104:2:3630
+105:2:3634
+106:0:3995
+107:2:2940
+108:2:3533
+109:0:3995
+110:2:2768
+111:0:3995
+112:2:2941
+113:0:3995
+114:2:2768
+115:0:3995
+116:2:2944
+117:2:2945
+118:2:2949
+119:2:2950
+120:2:2958
+121:2:2959
+122:2:2963
+123:2:2964
+124:2:2972
+125:2:2977
+126:2:2981
+127:2:2982
+128:2:2990
+129:2:2991
+130:2:2995
+131:2:2996
+132:2:2990
+133:2:2991
+134:2:2995
+135:2:2996
+136:2:3004
+137:2:3009
+138:2:3016
+139:2:3017
+140:2:3024
+141:2:3029
+142:2:3036
+143:2:3037
+144:2:3036
+145:2:3037
+146:2:3044
+147:2:3053
+148:0:3995
+149:2:2768
+150:0:3995
+151:2:3057
+152:2:3058
+153:2:3059
+154:2:3071
+155:2:3072
+156:2:3076
+157:2:3077
+158:2:3085
+159:2:3090
+160:2:3094
+161:2:3095
+162:2:3103
+163:2:3104
+164:2:3108
+165:2:3109
+166:2:3103
+167:2:3104
+168:2:3108
+169:2:3109
+170:2:3117
+171:2:3122
+172:2:3129
+173:2:3130
+174:2:3137
+175:2:3142
+176:2:3149
+177:2:3150
+178:2:3149
+179:2:3150
+180:2:3157
+181:2:3170
+182:2:3171
+183:0:3995
+184:2:2768
+185:0:3995
+186:2:3178
+187:2:3179
+188:2:3183
+189:2:3184
+190:2:3192
+191:2:3193
+192:2:3197
+193:2:3198
+194:2:3206
+195:2:3211
+196:2:3215
+197:2:3216
+198:2:3224
+199:2:3225
+200:2:3229
+201:2:3230
+202:2:3224
+203:2:3225
+204:2:3229
+205:2:3230
+206:2:3238
+207:2:3243
+208:2:3250
+209:2:3251
+210:2:3258
+211:2:3263
+212:2:3270
+213:2:3271
+214:2:3270
+215:2:3271
+216:2:3278
+217:0:3995
+218:2:2768
+219:0:3995
+220:2:3289
+221:2:3290
+222:2:3294
+223:2:3295
+224:2:3303
+225:2:3304
+226:2:3308
+227:2:3309
+228:2:3317
+229:2:3322
+230:2:3326
+231:2:3327
+232:2:3335
+233:2:3336
+234:2:3340
+235:2:3341
+236:2:3335
+237:2:3336
+238:2:3340
+239:2:3341
+240:2:3349
+241:2:3354
+242:2:3361
+243:2:3362
+244:2:3369
+245:2:3374
+246:2:3381
+247:2:3382
+248:2:3381
+249:2:3382
+250:2:3389
+251:2:3398
+252:0:3995
+253:2:2768
+254:0:3995
+255:2:3402
+256:2:3403
+257:2:3404
+258:2:3416
+259:2:3417
+260:2:3421
+261:2:3422
+262:2:3430
+263:2:3435
+264:2:3439
+265:2:3440
+266:2:3448
+267:2:3449
+268:2:3453
+269:2:3454
+270:2:3448
+271:2:3449
+272:2:3453
+273:2:3454
+274:2:3462
+275:2:3467
+276:2:3474
+277:2:3475
+278:2:3482
+279:2:3487
+280:2:3494
+281:2:3495
+282:2:3494
+283:2:3495
+284:2:3502
+285:2:3514
+286:2:3515
+287:0:3995
+288:2:2768
+289:0:3995
+290:2:3521
+291:0:3995
+292:2:3825
+293:2:3826
+294:2:3830
+295:2:3834
+296:2:3835
+297:2:3839
+298:2:3847
+299:2:3848
+300:2:3852
+301:2:3856
+302:2:3857
+303:2:3852
+304:2:3856
+305:2:3857
+306:2:3861
+307:2:3868
+308:2:3875
+309:2:3876
+310:2:3883
+311:2:3888
+312:2:3895
+313:2:3896
+314:2:3895
+315:2:3896
+316:2:3903
+317:2:3907
+318:0:3995
+319:2:3523
+320:2:3533
+321:0:3995
+322:2:2768
+323:0:3995
+324:2:3524
+325:2:3525
+326:0:3995
+327:2:2768
+328:0:3995
+329:2:3529
+330:0:3995
+331:2:3537
+332:0:3995
+333:2:2764
+334:0:3995
+335:2:2766
+336:0:3995
+337:2:2767
+338:0:3995
+339:2:2768
+340:0:3995
+341:2:2931
+342:2:2932
+343:2:2933
+344:0:3995
+345:2:2768
+346:0:3995
+347:2:2769
+348:2:2770
+349:2:2774
+350:2:2775
+351:2:2783
+352:2:2784
+353:2:2788
+354:2:2789
+355:2:2797
+356:2:2802
+357:2:2803
+358:2:2815
+359:2:2816
+360:2:2817
+361:2:2815
+362:2:2816
+363:2:2820
+364:2:2821
+365:2:2829
+366:2:2834
+367:2:2841
+368:2:2842
+369:2:2849
+370:2:2854
+371:2:2861
+372:2:2862
+373:2:2861
+374:2:2862
+375:2:2869
+376:2:2879
+377:0:3995
+378:2:2768
+379:0:3995
+380:2:2938
+381:0:3995
+382:2:3552
+383:2:3553
+384:2:3557
+385:2:3561
+386:2:3562
+387:2:3566
+388:2:3574
+389:2:3575
+390:2:3579
+391:2:3580
+392:2:3579
+393:2:3583
+394:2:3584
+395:2:3588
+396:2:3595
+397:2:3602
+398:2:3603
+399:2:3610
+400:2:3615
+401:2:3622
+402:2:3623
+403:2:3622
+404:2:3623
+405:2:3630
+406:2:3634
+407:0:3995
+408:2:2940
+409:2:3533
+410:0:3995
+411:2:2768
+412:0:3995
+413:2:2941
+414:0:3995
+415:2:2768
+416:0:3995
+417:2:2944
+418:2:2945
+419:2:2949
+420:2:2950
+421:2:2958
+422:2:2959
+423:2:2963
+424:2:2964
+425:2:2972
+426:2:2977
+427:2:2981
+428:2:2982
+429:2:2990
+430:2:2991
+431:2:2995
+432:2:2996
+433:2:2990
+434:2:2991
+435:2:2995
+436:2:2996
+437:2:3004
+438:2:3009
+439:2:3016
+440:2:3017
+441:2:3024
+442:2:3029
+443:2:3036
+444:2:3037
+445:2:3036
+446:2:3037
+447:2:3044
+448:2:3053
+449:0:3995
+450:2:2768
+451:0:3995
+452:2:3057
+453:2:3058
+454:2:3059
+455:2:3071
+456:2:3072
+457:2:3076
+458:2:3077
+459:2:3085
+460:2:3090
+461:2:3094
+462:2:3095
+463:2:3103
+464:2:3104
+465:2:3108
+466:2:3109
+467:2:3103
+468:2:3104
+469:2:3108
+470:2:3109
+471:2:3117
+472:2:3122
+473:2:3129
+474:2:3130
+475:2:3137
+476:2:3142
+477:2:3149
+478:2:3150
+479:2:3149
+480:2:3150
+481:2:3157
+482:2:3170
+483:2:3171
+484:0:3995
+485:2:2768
+486:0:3995
+487:2:3178
+488:2:3179
+489:2:3183
+490:2:3184
+491:2:3192
+492:2:3193
+493:2:3197
+494:2:3198
+495:2:3206
+496:2:3211
+497:2:3215
+498:2:3216
+499:2:3224
+500:2:3225
+501:2:3229
+502:2:3230
+503:2:3224
+504:2:3225
+505:2:3229
+506:2:3230
+507:2:3238
+508:2:3243
+509:2:3250
+510:2:3251
+511:2:3258
+512:2:3263
+513:2:3270
+514:2:3271
+515:2:3270
+516:2:3271
+517:2:3278
+518:0:3995
+519:2:2768
+520:0:3995
+521:2:3289
+522:2:3290
+523:2:3294
+524:2:3295
+525:2:3303
+526:2:3304
+527:2:3308
+528:2:3309
+529:2:3317
+530:2:3322
+531:2:3326
+532:2:3327
+533:2:3335
+534:2:3336
+535:2:3340
+536:2:3341
+537:2:3335
+538:2:3336
+539:2:3340
+540:2:3341
+541:2:3349
+542:2:3354
+543:2:3361
+544:2:3362
+545:2:3369
+546:2:3374
+547:2:3381
+548:2:3382
+549:2:3381
+550:2:3382
+551:2:3389
+552:2:3398
+553:0:3995
+554:2:2768
+555:0:3995
+556:2:3402
+557:2:3403
+558:2:3404
+559:2:3416
+560:2:3417
+561:2:3421
+562:2:3422
+563:2:3430
+564:2:3435
+565:2:3439
+566:2:3440
+567:2:3448
+568:2:3449
+569:2:3453
+570:2:3454
+571:2:3448
+572:2:3449
+573:2:3453
+574:2:3454
+575:2:3462
+576:2:3467
+577:2:3474
+578:2:3475
+579:2:3482
+580:2:3487
+581:2:3494
+582:2:3495
+583:2:3494
+584:2:3495
+585:2:3502
+586:2:3514
+587:2:3515
+588:0:3995
+589:2:2768
+590:0:3995
+591:2:3521
+592:0:3995
+593:2:3825
+594:2:3826
+595:2:3830
+596:2:3834
+597:2:3835
+598:2:3839
+599:2:3847
+600:2:3848
+601:2:3852
+602:2:3856
+603:2:3857
+604:2:3852
+605:2:3856
+606:2:3857
+607:2:3861
+608:2:3868
+609:2:3875
+610:2:3876
+611:2:3883
+612:2:3888
+613:2:3895
+614:2:3896
+615:2:3895
+616:2:3896
+617:2:3903
+618:2:3907
+619:0:3995
+620:2:3523
+621:2:3533
+622:0:3995
+623:2:2768
+624:0:3995
+625:2:3524
+626:2:3525
+627:0:3995
+628:2:2768
+629:0:3995
+630:2:3529
+631:0:3995
+632:2:3537
+633:0:3995
+634:2:2764
+635:0:3995
+636:2:2766
+637:0:3995
+638:2:2767
+639:0:3995
+640:2:2768
+641:0:3995
+642:2:2769
+643:2:2770
+644:2:2774
+645:2:2775
+646:2:2783
+647:2:2784
+648:2:2788
+649:2:2789
+650:2:2797
+651:2:2802
+652:2:2806
+653:2:2807
+654:2:2815
+655:2:2816
+656:2:2820
+657:2:2821
+658:2:2815
+659:2:2816
+660:2:2817
+661:2:2829
+662:2:2834
+663:2:2841
+664:2:2842
+665:2:2849
+666:2:2854
+667:2:2861
+668:2:2862
+669:2:2861
+670:2:2862
+671:2:2869
+672:2:2879
+673:0:3995
+674:2:2768
+675:0:3995
+676:2:2931
+677:2:2932
+678:2:2933
+679:0:3995
+680:2:2768
+681:0:3995
+682:2:2938
+683:0:3995
+684:1:2
+685:0:3995
+686:1:8
+687:0:3995
+688:1:9
+689:0:3995
+690:1:10
+691:0:3995
+692:1:11
+693:0:3995
+694:1:12
+695:1:13
+696:1:17
+697:1:18
+698:1:26
+699:1:27
+700:1:31
+701:1:32
+702:1:40
+703:1:45
+704:1:49
+705:1:50
+706:1:58
+707:1:59
+708:1:63
+709:1:64
+710:1:58
+711:1:59
+712:1:63
+713:1:64
+714:1:72
+715:1:77
+716:1:84
+717:1:85
+718:1:92
+719:1:97
+720:1:104
+721:1:105
+722:1:104
+723:1:105
+724:1:112
+725:0:3995
+726:1:11
+727:0:3995
+728:1:123
+729:1:124
+730:0:3995
+731:1:11
+732:0:3995
+733:1:130
+734:1:131
+735:1:135
+736:1:136
+737:1:144
+738:1:145
+739:1:149
+740:1:150
+741:1:158
+742:1:163
+743:1:167
+744:1:168
+745:1:176
+746:1:177
+747:1:181
+748:1:182
+749:1:176
+750:1:177
+751:1:181
+752:1:182
+753:1:190
+754:1:195
+755:1:202
+756:1:203
+757:1:210
+758:1:215
+759:1:222
+760:1:223
+761:1:222
+762:1:223
+763:1:230
+764:0:3995
+765:1:11
+766:0:3995
+767:1:241
+768:1:242
+769:1:246
+770:1:247
+771:1:255
+772:1:256
+773:1:260
+774:1:261
+775:1:269
+776:1:274
+777:1:278
+778:1:279
+779:1:287
+780:1:288
+781:1:292
+782:1:293
+783:1:287
+784:1:288
+785:1:292
+786:1:293
+787:1:301
+788:1:306
+789:1:313
+790:1:314
+791:1:321
+792:1:326
+793:1:333
+794:1:334
+795:1:333
+796:1:334
+797:1:341
+798:1:350
+799:0:3995
+800:1:11
+801:0:3995
+802:1:468
+803:1:472
+804:1:473
+805:1:477
+806:1:478
+807:1:486
+808:1:494
+809:1:495
+810:1:499
+811:1:503
+812:1:504
+813:1:499
+814:1:503
+815:1:504
+816:1:508
+817:1:515
+818:1:522
+819:1:523
+820:1:530
+821:1:535
+822:1:542
+823:1:543
+824:1:542
+825:1:543
+826:1:550
+827:0:3995
+828:1:11
+829:0:3995
+830:1:560
+831:1:561
+832:1:565
+833:1:566
+834:1:574
+835:1:575
+836:1:579
+837:1:580
+838:1:588
+839:1:593
+840:1:597
+841:1:598
+842:1:606
+843:1:607
+844:1:611
+845:1:612
+846:1:606
+847:1:607
+848:1:611
+849:1:612
+850:1:620
+851:1:625
+852:1:632
+853:1:633
+854:1:640
+855:1:645
+856:1:652
+857:1:653
+858:1:652
+859:1:653
+860:1:660
+861:0:3995
+862:1:11
+863:0:3995
+864:1:671
+865:1:674
+866:1:675
+867:0:3995
+868:1:11
+869:0:3995
+870:1:678
+871:1:679
+872:1:683
+873:1:684
+874:1:692
+875:1:693
+876:1:697
+877:1:698
+878:1:706
+879:1:711
+880:1:715
+881:1:716
+882:1:724
+883:1:725
+884:1:729
+885:1:730
+886:1:724
+887:1:725
+888:1:729
+889:1:730
+890:1:738
+891:1:743
+892:1:750
+893:1:751
+894:1:758
+895:1:763
+896:1:770
+897:1:771
+898:1:770
+899:1:771
+900:1:778
+901:0:3995
+902:1:11
+903:0:3995
+904:1:902
+905:1:903
+906:1:907
+907:1:908
+908:1:916
+909:1:917
+910:1:921
+911:1:922
+912:1:930
+913:1:935
+914:1:939
+915:1:940
+916:1:948
+917:1:949
+918:1:953
+919:1:954
+920:1:948
+921:1:949
+922:1:953
+923:1:954
+924:1:962
+925:1:967
+926:1:974
+927:1:975
+928:1:982
+929:1:987
+930:1:994
+931:1:995
+932:1:994
+933:1:995
+934:1:1002
+935:1:1011
+936:1:1015
+937:0:3995
+938:1:11
+939:0:3995
+940:1:1016
+941:1:1017
+942:1:1021
+943:1:1022
+944:1:1030
+945:1:1031
+946:1:1032
+947:1:1044
+948:1:1049
+949:1:1053
+950:1:1054
+951:1:1062
+952:1:1063
+953:1:1067
+954:1:1068
+955:1:1062
+956:1:1063
+957:1:1067
+958:1:1068
+959:1:1076
+960:1:1081
+961:1:1088
+962:1:1089
+963:1:1096
+964:1:1101
+965:1:1108
+966:1:1109
+967:1:1108
+968:1:1109
+969:1:1116
+970:0:3995
+971:1:11
+972:0:3995
+973:1:1127
+974:0:3995
+975:1:2663
+976:1:2670
+977:1:2671
+978:1:2678
+979:1:2683
+980:1:2690
+981:1:2691
+982:1:2690
+983:1:2691
+984:1:2698
+985:1:2702
+986:0:3995
+987:2:3552
+988:2:3553
+989:2:3557
+990:2:3561
+991:2:3562
+992:2:3566
+993:2:3571
+994:2:3579
+995:2:3583
+996:2:3584
+997:2:3579
+998:2:3580
+999:2:3588
+1000:2:3595
+1001:2:3602
+1002:2:3603
+1003:2:3610
+1004:2:3615
+1005:2:3622
+1006:2:3623
+1007:2:3622
+1008:2:3623
+1009:2:3630
+1010:2:3634
+1011:0:3995
+1012:2:2940
+1013:2:3533
+1014:0:3995
+1015:2:2768
+1016:0:3995
+1017:2:2941
+1018:0:3995
+1019:2:2768
+1020:0:3995
+1021:2:2944
+1022:2:2945
+1023:2:2949
+1024:2:2950
+1025:2:2958
+1026:2:2959
+1027:2:2963
+1028:2:2964
+1029:2:2972
+1030:2:2977
+1031:2:2981
+1032:2:2982
+1033:2:2990
+1034:2:2991
+1035:2:2995
+1036:2:2996
+1037:2:2990
+1038:2:2991
+1039:2:2995
+1040:2:2996
+1041:2:3004
+1042:2:3009
+1043:2:3016
+1044:2:3017
+1045:2:3024
+1046:2:3029
+1047:2:3036
+1048:2:3037
+1049:2:3036
+1050:2:3037
+1051:2:3044
+1052:2:3053
+1053:0:3995
+1054:2:2768
+1055:0:3995
+1056:2:3057
+1057:2:3058
+1058:2:3059
+1059:2:3071
+1060:2:3072
+1061:2:3076
+1062:2:3077
+1063:2:3085
+1064:2:3090
+1065:2:3094
+1066:2:3095
+1067:2:3103
+1068:2:3104
+1069:2:3108
+1070:2:3109
+1071:2:3103
+1072:2:3104
+1073:2:3108
+1074:2:3109
+1075:2:3117
+1076:2:3122
+1077:2:3129
+1078:2:3130
+1079:2:3137
+1080:2:3142
+1081:2:3149
+1082:2:3150
+1083:2:3149
+1084:2:3150
+1085:2:3157
+1086:2:3168
+1087:0:3995
+1088:2:2768
+1089:0:3995
+1090:2:3174
+1091:0:3995
+1092:2:3643
+1093:2:3644
+1094:2:3648
+1095:2:3652
+1096:2:3653
+1097:2:3657
+1098:2:3665
+1099:2:3666
+1100:2:3670
+1101:2:3674
+1102:2:3675
+1103:2:3670
+1104:2:3674
+1105:2:3675
+1106:2:3679
+1107:2:3686
+1108:2:3693
+1109:2:3694
+1110:2:3701
+1111:2:3706
+1112:2:3713
+1113:2:3714
+1114:2:3713
+1115:2:3714
+1116:2:3721
+1117:2:3725
+1118:0:3995
+1119:2:3176
+1120:2:3177
+1121:0:3995
+1122:2:2768
+1123:0:3995
+1124:2:3178
+1125:2:3179
+1126:2:3183
+1127:2:3184
+1128:2:3192
+1129:2:3193
+1130:2:3197
+1131:2:3198
+1132:2:3206
+1133:2:3211
+1134:2:3215
+1135:2:3216
+1136:2:3224
+1137:2:3225
+1138:2:3229
+1139:2:3230
+1140:2:3224
+1141:2:3225
+1142:2:3229
+1143:2:3230
+1144:2:3238
+1145:2:3243
+1146:2:3250
+1147:2:3251
+1148:2:3258
+1149:2:3263
+1150:2:3270
+1151:2:3271
+1152:2:3270
+1153:2:3271
+1154:2:3278
+1155:0:3995
+1156:2:2768
+1157:0:3995
+1158:2:3057
+1159:2:3058
+1160:2:3062
+1161:2:3063
+1162:2:3071
+1163:2:3072
+1164:2:3076
+1165:2:3077
+1166:2:3085
+1167:2:3090
+1168:2:3094
+1169:2:3095
+1170:2:3103
+1171:2:3104
+1172:2:3108
+1173:2:3109
+1174:2:3103
+1175:2:3104
+1176:2:3108
+1177:2:3109
+1178:2:3117
+1179:2:3122
+1180:2:3129
+1181:2:3130
+1182:2:3137
+1183:2:3142
+1184:2:3149
+1185:2:3150
+1186:2:3149
+1187:2:3150
+1188:2:3157
+1189:2:3168
+1190:0:3995
+1191:2:2768
+1192:0:3995
+1193:2:3174
+1194:0:3995
+1195:2:3643
+1196:2:3644
+1197:2:3648
+1198:2:3652
+1199:2:3653
+1200:2:3657
+1201:2:3665
+1202:2:3666
+1203:2:3670
+1204:2:3674
+1205:2:3675
+1206:2:3670
+1207:2:3674
+1208:2:3675
+1209:2:3679
+1210:2:3686
+1211:2:3693
+1212:2:3694
+1213:2:3701
+1214:2:3706
+1215:2:3713
+1216:2:3714
+1217:2:3713
+1218:2:3714
+1219:2:3721
+1220:2:3725
+1221:0:3995
+1222:2:3176
+1223:2:3177
+1224:0:3995
+1225:2:2768
+1226:0:3995
+1227:2:3057
+1228:2:3058
+1229:2:3062
+1230:2:3063
+1231:2:3071
+1232:2:3072
+1233:2:3076
+1234:2:3077
+1235:2:3085
+1236:2:3090
+1237:2:3094
+1238:2:3095
+1239:2:3103
+1240:2:3104
+1241:2:3108
+1242:2:3109
+1243:2:3103
+1244:2:3104
+1245:2:3108
+1246:2:3109
+1247:2:3117
+1248:2:3122
+1249:2:3129
+1250:2:3130
+1251:2:3137
+1252:2:3142
+1253:2:3149
+1254:2:3150
+1255:2:3149
+1256:2:3150
+1257:2:3157
+1258:2:3168
+1259:0:3995
+1260:2:2768
+1261:0:3995
+1262:2:3174
+1263:0:3995
+1264:2:3643
+1265:2:3644
+1266:2:3648
+1267:2:3652
+1268:2:3653
+1269:2:3657
+1270:2:3665
+1271:2:3666
+1272:2:3670
+1273:2:3674
+1274:2:3675
+1275:2:3670
+1276:2:3674
+1277:2:3675
+1278:2:3679
+1279:2:3686
+1280:2:3693
+1281:2:3694
+1282:2:3701
+1283:2:3706
+1284:2:3713
+1285:2:3714
+1286:2:3713
+1287:2:3714
+1288:2:3721
+1289:2:3725
+1290:0:3995
+1291:1:1129
+1292:1:1130
+1293:0:3993
+1294:1:11
+1295:0:3999
+1296:1:2142