Add verif results

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

diff --git a/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_wmb.spin.input.trail b/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_wmb.spin.input.trail
new file mode 100644 (file)
index 0000000..b250110
--- /dev/null
+++ b/formal-model/urcu-controldataflow-alpha-no-ipi/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1423 @@
+-2:3:-2
+-4:-4:-4
+1:0:4463
+2:3:4383
+3:3:4386
+4:3:4386
+5:3:4389
+6:3:4397
+7:3:4397
+8:3:4400
+9:3:4406
+10:3:4410
+11:3:4410
+12:3:4413
+13:3:4423
+14:3:4431
+15:3:4431
+16:3:4434
+17:3:4440
+18:3:4444
+19:3:4444
+20:3:4447
+21:3:4453
+22:3:4457
+23:3:4458
+24:0:4463
+25:3:4460
+26:0:4463
+27:2:3117
+28:0:4463
+29:2:3123
+30:0:4463
+31:2:3124
+32:0:4463
+33:2:3126
+34:0:4463
+35:2:3127
+36:0:4463
+37:2:3128
+38:0:4463
+39:2:3129
+40:2:3130
+41:2:3134
+42:2:3135
+43:2:3143
+44:2:3144
+45:2:3148
+46:2:3149
+47:2:3157
+48:2:3162
+49:2:3166
+50:2:3167
+51:2:3175
+52:2:3176
+53:2:3180
+54:2:3181
+55:2:3175
+56:2:3176
+57:2:3180
+58:2:3181
+59:2:3189
+60:2:3194
+61:2:3195
+62:2:3206
+63:2:3207
+64:2:3208
+65:2:3219
+66:2:3224
+67:2:3225
+68:2:3236
+69:2:3237
+70:2:3238
+71:2:3236
+72:2:3237
+73:2:3238
+74:2:3249
+75:2:3257
+76:0:4463
+77:2:3128
+78:0:4463
+79:2:3309
+80:2:3310
+81:2:3311
+82:0:4463
+83:2:3128
+84:0:4463
+85:2:3316
+86:0:4463
+87:2:4020
+88:2:4021
+89:2:4025
+90:2:4029
+91:2:4030
+92:2:4034
+93:2:4039
+94:2:4047
+95:2:4051
+96:2:4052
+97:2:4047
+98:2:4048
+99:2:4056
+100:2:4063
+101:2:4070
+102:2:4071
+103:2:4078
+104:2:4083
+105:2:4090
+106:2:4091
+107:2:4090
+108:2:4091
+109:2:4098
+110:2:4102
+111:0:4463
+112:2:3318
+113:2:4001
+114:0:4463
+115:2:3128
+116:0:4463
+117:2:3319
+118:0:4463
+119:2:3128
+120:0:4463
+121:2:3322
+122:2:3323
+123:2:3327
+124:2:3328
+125:2:3336
+126:2:3337
+127:2:3341
+128:2:3342
+129:2:3350
+130:2:3355
+131:2:3359
+132:2:3360
+133:2:3368
+134:2:3369
+135:2:3373
+136:2:3374
+137:2:3368
+138:2:3369
+139:2:3373
+140:2:3374
+141:2:3382
+142:2:3387
+143:2:3388
+144:2:3399
+145:2:3400
+146:2:3401
+147:2:3412
+148:2:3417
+149:2:3418
+150:2:3429
+151:2:3430
+152:2:3431
+153:2:3429
+154:2:3430
+155:2:3431
+156:2:3442
+157:2:3449
+158:0:4463
+159:2:3128
+160:0:4463
+161:2:3453
+162:2:3454
+163:2:3455
+164:2:3467
+165:2:3468
+166:2:3472
+167:2:3473
+168:2:3481
+169:2:3486
+170:2:3490
+171:2:3491
+172:2:3499
+173:2:3500
+174:2:3504
+175:2:3505
+176:2:3499
+177:2:3500
+178:2:3504
+179:2:3505
+180:2:3513
+181:2:3518
+182:2:3519
+183:2:3530
+184:2:3531
+185:2:3532
+186:2:3543
+187:2:3548
+188:2:3549
+189:2:3560
+190:2:3561
+191:2:3562
+192:2:3560
+193:2:3561
+194:2:3562
+195:2:3573
+196:2:3584
+197:2:3585
+198:0:4463
+199:2:3128
+200:0:4463
+201:2:3592
+202:2:3593
+203:2:3597
+204:2:3598
+205:2:3606
+206:2:3607
+207:2:3611
+208:2:3612
+209:2:3620
+210:2:3625
+211:2:3629
+212:2:3630
+213:2:3638
+214:2:3639
+215:2:3643
+216:2:3644
+217:2:3638
+218:2:3639
+219:2:3643
+220:2:3644
+221:2:3652
+222:2:3657
+223:2:3658
+224:2:3669
+225:2:3670
+226:2:3671
+227:2:3682
+228:2:3687
+229:2:3688
+230:2:3699
+231:2:3700
+232:2:3701
+233:2:3699
+234:2:3700
+235:2:3701
+236:2:3712
+237:0:4463
+238:2:3128
+239:0:4463
+240:2:3721
+241:2:3722
+242:2:3726
+243:2:3727
+244:2:3735
+245:2:3736
+246:2:3740
+247:2:3741
+248:2:3749
+249:2:3754
+250:2:3758
+251:2:3759
+252:2:3767
+253:2:3768
+254:2:3772
+255:2:3773
+256:2:3767
+257:2:3768
+258:2:3772
+259:2:3773
+260:2:3781
+261:2:3786
+262:2:3787
+263:2:3798
+264:2:3799
+265:2:3800
+266:2:3811
+267:2:3816
+268:2:3817
+269:2:3828
+270:2:3829
+271:2:3830
+272:2:3828
+273:2:3829
+274:2:3830
+275:2:3841
+276:2:3848
+277:0:4463
+278:2:3128
+279:0:4463
+280:2:3852
+281:2:3853
+282:2:3854
+283:2:3866
+284:2:3867
+285:2:3871
+286:2:3872
+287:2:3880
+288:2:3885
+289:2:3889
+290:2:3890
+291:2:3898
+292:2:3899
+293:2:3903
+294:2:3904
+295:2:3898
+296:2:3899
+297:2:3903
+298:2:3904
+299:2:3912
+300:2:3917
+301:2:3918
+302:2:3929
+303:2:3930
+304:2:3931
+305:2:3942
+306:2:3947
+307:2:3948
+308:2:3959
+309:2:3960
+310:2:3961
+311:2:3959
+312:2:3960
+313:2:3961
+314:2:3972
+315:2:3982
+316:2:3983
+317:0:4463
+318:2:3128
+319:0:4463
+320:2:3989
+321:0:4463
+322:2:4293
+323:2:4294
+324:2:4298
+325:2:4302
+326:2:4303
+327:2:4307
+328:2:4315
+329:2:4316
+330:2:4320
+331:2:4324
+332:2:4325
+333:2:4320
+334:2:4324
+335:2:4325
+336:2:4329
+337:2:4336
+338:2:4343
+339:2:4344
+340:2:4351
+341:2:4356
+342:2:4363
+343:2:4364
+344:2:4363
+345:2:4364
+346:2:4371
+347:2:4375
+348:0:4463
+349:2:3991
+350:2:4001
+351:0:4463
+352:2:3128
+353:0:4463
+354:2:3992
+355:2:3993
+356:0:4463
+357:2:3128
+358:0:4463
+359:2:3997
+360:0:4463
+361:2:4005
+362:0:4463
+363:2:3124
+364:0:4463
+365:2:3126
+366:0:4463
+367:2:3127
+368:0:4463
+369:2:3128
+370:0:4463
+371:2:3309
+372:2:3310
+373:2:3311
+374:0:4463
+375:2:3128
+376:0:4463
+377:2:3129
+378:2:3130
+379:2:3134
+380:2:3135
+381:2:3143
+382:2:3144
+383:2:3148
+384:2:3149
+385:2:3157
+386:2:3162
+387:2:3163
+388:2:3175
+389:2:3176
+390:2:3177
+391:2:3175
+392:2:3176
+393:2:3180
+394:2:3181
+395:2:3189
+396:2:3194
+397:2:3195
+398:2:3206
+399:2:3207
+400:2:3208
+401:2:3219
+402:2:3224
+403:2:3225
+404:2:3236
+405:2:3237
+406:2:3238
+407:2:3236
+408:2:3237
+409:2:3238
+410:2:3249
+411:2:3257
+412:0:4463
+413:2:3128
+414:0:4463
+415:2:3316
+416:0:4463
+417:2:4020
+418:2:4021
+419:2:4025
+420:2:4029
+421:2:4030
+422:2:4034
+423:2:4042
+424:2:4043
+425:2:4047
+426:2:4048
+427:2:4047
+428:2:4051
+429:2:4052
+430:2:4056
+431:2:4063
+432:2:4070
+433:2:4071
+434:2:4078
+435:2:4083
+436:2:4090
+437:2:4091
+438:2:4090
+439:2:4091
+440:2:4098
+441:2:4102
+442:0:4463
+443:2:3318
+444:2:4001
+445:0:4463
+446:2:3128
+447:0:4463
+448:2:3319
+449:0:4463
+450:2:3128
+451:0:4463
+452:2:3322
+453:2:3323
+454:2:3327
+455:2:3328
+456:2:3336
+457:2:3337
+458:2:3341
+459:2:3342
+460:2:3350
+461:2:3355
+462:2:3359
+463:2:3360
+464:2:3368
+465:2:3369
+466:2:3373
+467:2:3374
+468:2:3368
+469:2:3369
+470:2:3373
+471:2:3374
+472:2:3382
+473:2:3387
+474:2:3388
+475:2:3399
+476:2:3400
+477:2:3401
+478:2:3412
+479:2:3417
+480:2:3418
+481:2:3429
+482:2:3430
+483:2:3431
+484:2:3429
+485:2:3430
+486:2:3431
+487:2:3442
+488:2:3449
+489:0:4463
+490:2:3128
+491:0:4463
+492:2:3453
+493:2:3454
+494:2:3455
+495:2:3467
+496:2:3468
+497:2:3472
+498:2:3473
+499:2:3481
+500:2:3486
+501:2:3490
+502:2:3491
+503:2:3499
+504:2:3500
+505:2:3504
+506:2:3505
+507:2:3499
+508:2:3500
+509:2:3504
+510:2:3505
+511:2:3513
+512:2:3518
+513:2:3519
+514:2:3530
+515:2:3531
+516:2:3532
+517:2:3543
+518:2:3548
+519:2:3549
+520:2:3560
+521:2:3561
+522:2:3562
+523:2:3560
+524:2:3561
+525:2:3562
+526:2:3573
+527:2:3584
+528:2:3585
+529:0:4463
+530:2:3128
+531:0:4463
+532:2:3592
+533:2:3593
+534:2:3597
+535:2:3598
+536:2:3606
+537:2:3607
+538:2:3611
+539:2:3612
+540:2:3620
+541:2:3625
+542:2:3629
+543:2:3630
+544:2:3638
+545:2:3639
+546:2:3643
+547:2:3644
+548:2:3638
+549:2:3639
+550:2:3643
+551:2:3644
+552:2:3652
+553:2:3657
+554:2:3658
+555:2:3669
+556:2:3670
+557:2:3671
+558:2:3682
+559:2:3687
+560:2:3688
+561:2:3699
+562:2:3700
+563:2:3701
+564:2:3699
+565:2:3700
+566:2:3701
+567:2:3712
+568:0:4463
+569:2:3128
+570:0:4463
+571:2:3721
+572:2:3722
+573:2:3726
+574:2:3727
+575:2:3735
+576:2:3736
+577:2:3740
+578:2:3741
+579:2:3749
+580:2:3754
+581:2:3758
+582:2:3759
+583:2:3767
+584:2:3768
+585:2:3772
+586:2:3773
+587:2:3767
+588:2:3768
+589:2:3772
+590:2:3773
+591:2:3781
+592:2:3786
+593:2:3787
+594:2:3798
+595:2:3799
+596:2:3800
+597:2:3811
+598:2:3816
+599:2:3817
+600:2:3828
+601:2:3829
+602:2:3830
+603:2:3828
+604:2:3829
+605:2:3830
+606:2:3841
+607:2:3848
+608:0:4463
+609:2:3128
+610:0:4463
+611:2:3852
+612:2:3853
+613:2:3854
+614:2:3866
+615:2:3867
+616:2:3871
+617:2:3872
+618:2:3880
+619:2:3885
+620:2:3889
+621:2:3890
+622:2:3898
+623:2:3899
+624:2:3903
+625:2:3904
+626:2:3898
+627:2:3899
+628:2:3903
+629:2:3904
+630:2:3912
+631:2:3917
+632:2:3918
+633:2:3929
+634:2:3930
+635:2:3931
+636:2:3942
+637:2:3947
+638:2:3948
+639:2:3959
+640:2:3960
+641:2:3961
+642:2:3959
+643:2:3960
+644:2:3961
+645:2:3972
+646:2:3982
+647:2:3983
+648:0:4463
+649:2:3128
+650:0:4463
+651:2:3989
+652:0:4463
+653:2:4293
+654:2:4294
+655:2:4298
+656:2:4302
+657:2:4303
+658:2:4307
+659:2:4315
+660:2:4316
+661:2:4320
+662:2:4324
+663:2:4325
+664:2:4320
+665:2:4324
+666:2:4325
+667:2:4329
+668:2:4336
+669:2:4343
+670:2:4344
+671:2:4351
+672:2:4356
+673:2:4363
+674:2:4364
+675:2:4363
+676:2:4364
+677:2:4371
+678:2:4375
+679:0:4463
+680:2:3991
+681:2:4001
+682:0:4463
+683:2:3128
+684:0:4463
+685:2:3992
+686:2:3993
+687:0:4463
+688:2:3128
+689:0:4463
+690:2:3997
+691:0:4463
+692:2:4005
+693:0:4463
+694:2:3124
+695:0:4463
+696:2:3126
+697:0:4463
+698:2:3127
+699:0:4463
+700:2:3128
+701:0:4463
+702:2:3129
+703:2:3130
+704:2:3134
+705:2:3135
+706:2:3143
+707:2:3144
+708:2:3148
+709:2:3149
+710:2:3157
+711:2:3162
+712:2:3166
+713:2:3167
+714:2:3175
+715:2:3176
+716:2:3180
+717:2:3181
+718:2:3175
+719:2:3176
+720:2:3177
+721:2:3189
+722:2:3194
+723:2:3195
+724:2:3206
+725:2:3207
+726:2:3208
+727:2:3219
+728:2:3224
+729:2:3225
+730:2:3236
+731:2:3237
+732:2:3238
+733:2:3236
+734:2:3237
+735:2:3238
+736:2:3249
+737:2:3257
+738:0:4463
+739:2:3128
+740:0:4463
+741:2:3309
+742:2:3310
+743:2:3311
+744:0:4463
+745:2:3128
+746:0:4463
+747:2:3316
+748:0:4463
+749:1:2
+750:0:4463
+751:1:8
+752:0:4463
+753:1:9
+754:0:4463
+755:1:10
+756:0:4463
+757:1:11
+758:0:4463
+759:1:12
+760:1:13
+761:1:17
+762:1:18
+763:1:26
+764:1:27
+765:1:31
+766:1:32
+767:1:40
+768:1:45
+769:1:49
+770:1:50
+771:1:58
+772:1:59
+773:1:63
+774:1:64
+775:1:58
+776:1:59
+777:1:63
+778:1:64
+779:1:72
+780:1:77
+781:1:78
+782:1:89
+783:1:90
+784:1:91
+785:1:102
+786:1:107
+787:1:108
+788:1:119
+789:1:120
+790:1:121
+791:1:119
+792:1:120
+793:1:121
+794:1:132
+795:0:4463
+796:1:11
+797:0:4463
+798:1:141
+799:1:142
+800:0:4463
+801:1:11
+802:0:4463
+803:1:148
+804:1:149
+805:1:153
+806:1:154
+807:1:162
+808:1:163
+809:1:167
+810:1:168
+811:1:176
+812:1:181
+813:1:185
+814:1:186
+815:1:194
+816:1:195
+817:1:199
+818:1:200
+819:1:194
+820:1:195
+821:1:199
+822:1:200
+823:1:208
+824:1:213
+825:1:214
+826:1:225
+827:1:226
+828:1:227
+829:1:238
+830:1:243
+831:1:244
+832:1:255
+833:1:256
+834:1:257
+835:1:255
+836:1:256
+837:1:257
+838:1:268
+839:0:4463
+840:1:11
+841:0:4463
+842:1:277
+843:1:278
+844:1:282
+845:1:283
+846:1:291
+847:1:292
+848:1:296
+849:1:297
+850:1:305
+851:1:310
+852:1:314
+853:1:315
+854:1:323
+855:1:324
+856:1:328
+857:1:329
+858:1:323
+859:1:324
+860:1:328
+861:1:329
+862:1:337
+863:1:342
+864:1:343
+865:1:354
+866:1:355
+867:1:356
+868:1:367
+869:1:372
+870:1:373
+871:1:384
+872:1:385
+873:1:386
+874:1:384
+875:1:385
+876:1:386
+877:1:397
+878:1:404
+879:0:4463
+880:1:11
+881:0:4463
+882:1:540
+883:1:544
+884:1:545
+885:1:549
+886:1:550
+887:1:558
+888:1:566
+889:1:567
+890:1:571
+891:1:575
+892:1:576
+893:1:571
+894:1:575
+895:1:576
+896:1:580
+897:1:587
+898:1:594
+899:1:595
+900:1:602
+901:1:607
+902:1:614
+903:1:615
+904:1:614
+905:1:615
+906:1:622
+907:0:4463
+908:1:11
+909:0:4463
+910:1:632
+911:1:633
+912:1:637
+913:1:638
+914:1:646
+915:1:647
+916:1:651
+917:1:652
+918:1:660
+919:1:665
+920:1:669
+921:1:670
+922:1:678
+923:1:679
+924:1:683
+925:1:684
+926:1:678
+927:1:679
+928:1:683
+929:1:684
+930:1:692
+931:1:697
+932:1:698
+933:1:709
+934:1:710
+935:1:711
+936:1:722
+937:1:727
+938:1:728
+939:1:739
+940:1:740
+941:1:741
+942:1:739
+943:1:740
+944:1:741
+945:1:752
+946:0:4463
+947:1:11
+948:0:4463
+949:1:761
+950:1:764
+951:1:765
+952:0:4463
+953:1:11
+954:0:4463
+955:1:768
+956:1:769
+957:1:773
+958:1:774
+959:1:782
+960:1:783
+961:1:787
+962:1:788
+963:1:796
+964:1:801
+965:1:805
+966:1:806
+967:1:814
+968:1:815
+969:1:819
+970:1:820
+971:1:814
+972:1:815
+973:1:819
+974:1:820
+975:1:828
+976:1:833
+977:1:834
+978:1:845
+979:1:846
+980:1:847
+981:1:858
+982:1:863
+983:1:864
+984:1:875
+985:1:876
+986:1:877
+987:1:875
+988:1:876
+989:1:877
+990:1:888
+991:0:4463
+992:1:11
+993:0:4463
+994:1:1028
+995:1:1029
+996:1:1033
+997:1:1034
+998:1:1042
+999:1:1043
+1000:1:1047
+1001:1:1048
+1002:1:1056
+1003:1:1061
+1004:1:1065
+1005:1:1066
+1006:1:1074
+1007:1:1075
+1008:1:1079
+1009:1:1080
+1010:1:1074
+1011:1:1075
+1012:1:1079
+1013:1:1080
+1014:1:1088
+1015:1:1093
+1016:1:1094
+1017:1:1105
+1018:1:1106
+1019:1:1107
+1020:1:1118
+1021:1:1123
+1022:1:1124
+1023:1:1135
+1024:1:1136
+1025:1:1137
+1026:1:1135
+1027:1:1136
+1028:1:1137
+1029:1:1148
+1030:1:1155
+1031:1:1159
+1032:0:4463
+1033:1:11
+1034:0:4463
+1035:1:1160
+1036:1:1161
+1037:1:1165
+1038:1:1166
+1039:1:1174
+1040:1:1175
+1041:1:1176
+1042:1:1188
+1043:1:1193
+1044:1:1197
+1045:1:1198
+1046:1:1206
+1047:1:1207
+1048:1:1211
+1049:1:1212
+1050:1:1206
+1051:1:1207
+1052:1:1211
+1053:1:1212
+1054:1:1220
+1055:1:1225
+1056:1:1226
+1057:1:1237
+1058:1:1238
+1059:1:1239
+1060:1:1250
+1061:1:1255
+1062:1:1256
+1063:1:1267
+1064:1:1268
+1065:1:1269
+1066:1:1267
+1067:1:1268
+1068:1:1269
+1069:1:1280
+1070:0:4463
+1071:1:11
+1072:0:4463
+1073:1:1289
+1074:0:4463
+1075:1:3023
+1076:1:3030
+1077:1:3031
+1078:1:3038
+1079:1:3043
+1080:1:3050
+1081:1:3051
+1082:1:3050
+1083:1:3051
+1084:1:3058
+1085:1:3062
+1086:0:4463
+1087:2:4020
+1088:2:4021
+1089:2:4025
+1090:2:4029
+1091:2:4030
+1092:2:4034
+1093:2:4039
+1094:2:4047
+1095:2:4051
+1096:2:4052
+1097:2:4047
+1098:2:4048
+1099:2:4056
+1100:2:4063
+1101:2:4070
+1102:2:4071
+1103:2:4078
+1104:2:4083
+1105:2:4090
+1106:2:4091
+1107:2:4090
+1108:2:4091
+1109:2:4098
+1110:2:4102
+1111:0:4463
+1112:2:3318
+1113:2:4001
+1114:0:4463
+1115:2:3128
+1116:0:4463
+1117:2:3319
+1118:0:4463
+1119:2:3128
+1120:0:4463
+1121:2:3322
+1122:2:3323
+1123:2:3327
+1124:2:3328
+1125:2:3336
+1126:2:3337
+1127:2:3341
+1128:2:3342
+1129:2:3350
+1130:2:3355
+1131:2:3359
+1132:2:3360
+1133:2:3368
+1134:2:3369
+1135:2:3373
+1136:2:3374
+1137:2:3368
+1138:2:3369
+1139:2:3373
+1140:2:3374
+1141:2:3382
+1142:2:3387
+1143:2:3388
+1144:2:3399
+1145:2:3400
+1146:2:3401
+1147:2:3412
+1148:2:3417
+1149:2:3418
+1150:2:3429
+1151:2:3430
+1152:2:3431
+1153:2:3429
+1154:2:3430
+1155:2:3431
+1156:2:3442
+1157:2:3449
+1158:0:4463
+1159:2:3128
+1160:0:4463
+1161:2:3453
+1162:2:3454
+1163:2:3455
+1164:2:3467
+1165:2:3468
+1166:2:3472
+1167:2:3473
+1168:2:3481
+1169:2:3486
+1170:2:3490
+1171:2:3491
+1172:2:3499
+1173:2:3500
+1174:2:3504
+1175:2:3505
+1176:2:3499
+1177:2:3500
+1178:2:3504
+1179:2:3505
+1180:2:3513
+1181:2:3518
+1182:2:3519
+1183:2:3530
+1184:2:3531
+1185:2:3532
+1186:2:3543
+1187:2:3548
+1188:2:3549
+1189:2:3560
+1190:2:3561
+1191:2:3562
+1192:2:3560
+1193:2:3561
+1194:2:3562
+1195:2:3573
+1196:2:3582
+1197:0:4463
+1198:2:3128
+1199:0:4463
+1200:2:3588
+1201:0:4463
+1202:2:4111
+1203:2:4112
+1204:2:4116
+1205:2:4120
+1206:2:4121
+1207:2:4125
+1208:2:4133
+1209:2:4134
+1210:2:4138
+1211:2:4142
+1212:2:4143
+1213:2:4138
+1214:2:4142
+1215:2:4143
+1216:2:4147
+1217:2:4154
+1218:2:4161
+1219:2:4162
+1220:2:4169
+1221:2:4174
+1222:2:4181
+1223:2:4182
+1224:2:4181
+1225:2:4182
+1226:2:4189
+1227:2:4193
+1228:0:4463
+1229:2:3590
+1230:2:3591
+1231:0:4463
+1232:2:3128
+1233:0:4463
+1234:2:3592
+1235:2:3593
+1236:2:3597
+1237:2:3598
+1238:2:3606
+1239:2:3607
+1240:2:3611
+1241:2:3612
+1242:2:3620
+1243:2:3625
+1244:2:3629
+1245:2:3630
+1246:2:3638
+1247:2:3639
+1248:2:3643
+1249:2:3644
+1250:2:3638
+1251:2:3639
+1252:2:3643
+1253:2:3644
+1254:2:3652
+1255:2:3657
+1256:2:3658
+1257:2:3669
+1258:2:3670
+1259:2:3671
+1260:2:3682
+1261:2:3687
+1262:2:3688
+1263:2:3699
+1264:2:3700
+1265:2:3701
+1266:2:3699
+1267:2:3700
+1268:2:3701
+1269:2:3712
+1270:0:4463
+1271:2:3128
+1272:0:4463
+1273:2:3453
+1274:2:3454
+1275:2:3458
+1276:2:3459
+1277:2:3467
+1278:2:3468
+1279:2:3472
+1280:2:3473
+1281:2:3481
+1282:2:3486
+1283:2:3490
+1284:2:3491
+1285:2:3499
+1286:2:3500
+1287:2:3504
+1288:2:3505
+1289:2:3499
+1290:2:3500
+1291:2:3504
+1292:2:3505
+1293:2:3513
+1294:2:3518
+1295:2:3519
+1296:2:3530
+1297:2:3531
+1298:2:3532
+1299:2:3543
+1300:2:3548
+1301:2:3549
+1302:2:3560
+1303:2:3561
+1304:2:3562
+1305:2:3560
+1306:2:3561
+1307:2:3562
+1308:2:3573
+1309:2:3582
+1310:0:4463
+1311:2:3128
+1312:0:4463
+1313:2:3588
+1314:0:4463
+1315:2:4111
+1316:2:4112
+1317:2:4116
+1318:2:4120
+1319:2:4121
+1320:2:4125
+1321:2:4133
+1322:2:4134
+1323:2:4138
+1324:2:4142
+1325:2:4143
+1326:2:4138
+1327:2:4142
+1328:2:4143
+1329:2:4147
+1330:2:4154
+1331:2:4161
+1332:2:4162
+1333:2:4169
+1334:2:4174
+1335:2:4181
+1336:2:4182
+1337:2:4181
+1338:2:4182
+1339:2:4189
+1340:2:4193
+1341:0:4463
+1342:2:3590
+1343:2:3591
+1344:0:4463
+1345:2:3128
+1346:0:4463
+1347:2:3453
+1348:2:3454
+1349:2:3458
+1350:2:3459
+1351:2:3467
+1352:2:3468
+1353:2:3472
+1354:2:3473
+1355:2:3481
+1356:2:3486
+1357:2:3490
+1358:2:3491
+1359:2:3499
+1360:2:3500
+1361:2:3504
+1362:2:3505
+1363:2:3499
+1364:2:3500
+1365:2:3504
+1366:2:3505
+1367:2:3513
+1368:2:3518
+1369:2:3519
+1370:2:3530
+1371:2:3531
+1372:2:3532
+1373:2:3543
+1374:2:3548
+1375:2:3549
+1376:2:3560
+1377:2:3561
+1378:2:3562
+1379:2:3560
+1380:2:3561
+1381:2:3562
+1382:2:3573
+1383:2:3582
+1384:0:4463
+1385:2:3128
+1386:0:4463
+1387:2:3588
+1388:0:4463
+1389:2:4111
+1390:2:4112
+1391:2:4116
+1392:2:4120
+1393:2:4121
+1394:2:4125
+1395:2:4133
+1396:2:4134
+1397:2:4138
+1398:2:4142
+1399:2:4143
+1400:2:4138
+1401:2:4142
+1402:2:4143
+1403:2:4147
+1404:2:4154
+1405:2:4161
+1406:2:4162
+1407:2:4169
+1408:2:4174
+1409:2:4181
+1410:2:4182
+1411:2:4181
+1412:2:4182
+1413:2:4189
+1414:2:4193
+1415:0:4463
+1416:1:1291
+1417:1:1292
+1418:0:4461
+1419:1:11
+1420:0:4467
+1421:1:2299