Verification run #1, ipi and no-ipi results

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

diff --git a/formal-model/results/urcu-controldataflow-ipi/urcu_free_single_flip.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi/urcu_free_single_flip.spin.input.trail
new file mode 100644 (file)
index 0000000..f09d0eb
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi/urcu_free_single_flip.spin.input.trail
@@ -0,0 +1,1386 @@
+-2:3:-2
+-4:-4:-4
+1:0:4646
+2:3:4566
+3:3:4569
+4:3:4569
+5:3:4572
+6:3:4580
+7:3:4580
+8:3:4583
+9:3:4589
+10:3:4593
+11:3:4593
+12:3:4596
+13:3:4606
+14:3:4614
+15:3:4614
+16:3:4617
+17:3:4623
+18:3:4627
+19:3:4627
+20:3:4630
+21:3:4636
+22:3:4640
+23:3:4641
+24:0:4646
+25:3:4643
+26:0:4646
+27:2:2871
+28:0:4646
+29:2:2877
+30:0:4646
+31:2:2878
+32:0:4646
+33:2:2880
+34:0:4646
+35:2:2881
+36:0:4646
+37:2:2882
+38:0:4646
+39:2:2883
+40:0:4646
+41:2:2884
+42:0:4646
+43:2:2885
+44:0:4646
+45:2:2886
+46:2:2887
+47:2:2891
+48:2:2892
+49:2:2900
+50:2:2901
+51:2:2905
+52:2:2906
+53:2:2914
+54:2:2919
+55:2:2923
+56:2:2924
+57:2:2932
+58:2:2933
+59:2:2937
+60:2:2938
+61:2:2932
+62:2:2933
+63:2:2937
+64:2:2938
+65:2:2946
+66:2:2951
+67:2:2952
+68:2:2963
+69:2:2964
+70:2:2965
+71:2:2976
+72:2:2981
+73:2:2982
+74:2:2993
+75:2:2994
+76:2:2995
+77:2:2993
+78:2:2994
+79:2:2995
+80:2:3006
+81:2:3014
+82:0:4646
+83:2:2885
+84:0:4646
+85:2:3018
+86:2:3022
+87:2:3023
+88:2:3027
+89:2:3031
+90:2:3032
+91:2:3036
+92:2:3044
+93:2:3045
+94:2:3049
+95:2:3053
+96:2:3054
+97:2:3049
+98:2:3050
+99:2:3058
+100:0:4646
+101:2:2885
+102:0:4646
+103:2:3066
+104:2:3067
+105:2:3068
+106:0:4646
+107:2:2885
+108:0:4646
+109:2:3073
+110:0:4646
+111:2:3775
+112:2:3776
+113:2:3780
+114:2:3784
+115:2:3785
+116:2:3789
+117:2:3794
+118:2:3802
+119:2:3806
+120:2:3807
+121:2:3802
+122:2:3806
+123:2:3807
+124:2:3811
+125:2:3818
+126:2:3825
+127:2:3826
+128:2:3833
+129:2:3838
+130:2:3845
+131:2:3846
+132:2:3845
+133:2:3846
+134:2:3853
+135:2:3857
+136:0:4646
+137:2:3862
+138:0:4646
+139:2:3863
+140:0:4646
+141:2:3864
+142:0:4646
+143:2:3865
+144:0:4646
+145:1:2
+146:0:4646
+147:2:3866
+148:0:4646
+149:1:8
+150:0:4646
+151:1:9
+152:0:4646
+153:2:3865
+154:0:4646
+155:1:10
+156:0:4646
+157:2:3866
+158:0:4646
+159:1:11
+160:0:4646
+161:2:3865
+162:0:4646
+163:1:12
+164:0:4646
+165:2:3866
+166:0:4646
+167:1:13
+168:0:4646
+169:2:3865
+170:0:4646
+171:1:14
+172:0:4646
+173:2:3866
+174:0:4646
+175:1:15
+176:0:4646
+177:1:16
+178:0:4646
+179:2:3865
+180:0:4646
+181:1:17
+182:0:4646
+183:2:3866
+184:0:4646
+185:1:26
+186:0:4646
+187:2:3865
+188:0:4646
+189:1:30
+190:1:31
+191:1:35
+192:1:39
+193:1:40
+194:1:44
+195:1:52
+196:1:53
+197:1:57
+198:1:61
+199:1:62
+200:1:57
+201:1:61
+202:1:62
+203:1:66
+204:1:73
+205:1:80
+206:1:81
+207:1:88
+208:1:93
+209:1:100
+210:1:101
+211:1:100
+212:1:101
+213:1:108
+214:1:112
+215:0:4646
+216:2:3866
+217:0:4646
+218:1:117
+219:0:4646
+220:2:3867
+221:0:4646
+222:2:3872
+223:0:4646
+224:2:3873
+225:0:4646
+226:2:3881
+227:2:3882
+228:2:3886
+229:2:3890
+230:2:3891
+231:2:3895
+232:2:3903
+233:2:3904
+234:2:3908
+235:2:3912
+236:2:3913
+237:2:3908
+238:2:3912
+239:2:3913
+240:2:3917
+241:2:3924
+242:2:3931
+243:2:3932
+244:2:3939
+245:2:3944
+246:2:3951
+247:2:3952
+248:2:3951
+249:2:3952
+250:2:3959
+251:2:3963
+252:0:4646
+253:2:3075
+254:2:3756
+255:0:4646
+256:2:2885
+257:0:4646
+258:2:3076
+259:0:4646
+260:2:2885
+261:0:4646
+262:2:3079
+263:2:3080
+264:2:3084
+265:2:3085
+266:2:3093
+267:2:3094
+268:2:3098
+269:2:3099
+270:2:3107
+271:2:3112
+272:2:3116
+273:2:3117
+274:2:3125
+275:2:3126
+276:2:3130
+277:2:3131
+278:2:3125
+279:2:3126
+280:2:3130
+281:2:3131
+282:2:3139
+283:2:3144
+284:2:3145
+285:2:3156
+286:2:3157
+287:2:3158
+288:2:3169
+289:2:3174
+290:2:3175
+291:2:3186
+292:2:3187
+293:2:3188
+294:2:3186
+295:2:3187
+296:2:3188
+297:2:3199
+298:2:3206
+299:0:4646
+300:2:2885
+301:0:4646
+302:2:3210
+303:2:3211
+304:2:3212
+305:2:3224
+306:2:3225
+307:2:3229
+308:2:3230
+309:2:3238
+310:2:3243
+311:2:3247
+312:2:3248
+313:2:3256
+314:2:3257
+315:2:3261
+316:2:3262
+317:2:3256
+318:2:3257
+319:2:3261
+320:2:3262
+321:2:3270
+322:2:3275
+323:2:3276
+324:2:3287
+325:2:3288
+326:2:3289
+327:2:3300
+328:2:3305
+329:2:3306
+330:2:3317
+331:2:3318
+332:2:3319
+333:2:3317
+334:2:3318
+335:2:3319
+336:2:3330
+337:2:3340
+338:2:3341
+339:0:4646
+340:2:2885
+341:0:4646
+342:2:3744
+343:0:4646
+344:2:4369
+345:2:4370
+346:2:4374
+347:2:4378
+348:2:4379
+349:2:4383
+350:2:4391
+351:2:4392
+352:2:4396
+353:2:4400
+354:2:4401
+355:2:4396
+356:2:4400
+357:2:4401
+358:2:4405
+359:2:4412
+360:2:4419
+361:2:4420
+362:2:4427
+363:2:4432
+364:2:4439
+365:2:4440
+366:2:4439
+367:2:4440
+368:2:4447
+369:2:4451
+370:0:4646
+371:2:4456
+372:0:4646
+373:2:4457
+374:0:4646
+375:2:4458
+376:0:4646
+377:2:4459
+378:0:4646
+379:1:118
+380:0:4646
+381:2:4460
+382:0:4646
+383:1:120
+384:0:4646
+385:2:4459
+386:0:4646
+387:1:19
+388:0:4646
+389:2:4460
+390:0:4646
+391:1:126
+392:1:127
+393:1:131
+394:1:132
+395:1:140
+396:1:141
+397:1:145
+398:1:146
+399:1:154
+400:1:159
+401:1:163
+402:1:164
+403:1:172
+404:1:173
+405:1:177
+406:1:178
+407:1:172
+408:1:173
+409:1:177
+410:1:178
+411:1:186
+412:1:198
+413:1:199
+414:1:203
+415:1:204
+416:1:205
+417:1:216
+418:1:221
+419:1:222
+420:1:233
+421:1:234
+422:1:235
+423:1:233
+424:1:234
+425:1:235
+426:1:246
+427:0:4646
+428:1:15
+429:0:4646
+430:1:16
+431:0:4646
+432:2:4459
+433:0:4646
+434:1:17
+435:0:4646
+436:2:4460
+437:0:4646
+438:1:118
+439:0:4646
+440:1:120
+441:0:4646
+442:2:4459
+443:0:4646
+444:1:19
+445:0:4646
+446:2:4460
+447:0:4646
+448:1:255
+449:1:256
+450:0:4646
+451:1:15
+452:0:4646
+453:1:16
+454:0:4646
+455:2:4459
+456:0:4646
+457:1:17
+458:0:4646
+459:2:4460
+460:0:4646
+461:1:118
+462:0:4646
+463:1:120
+464:0:4646
+465:2:4459
+466:0:4646
+467:1:19
+468:0:4646
+469:2:4460
+470:0:4646
+471:1:262
+472:1:263
+473:1:267
+474:1:268
+475:1:276
+476:1:277
+477:1:281
+478:1:282
+479:1:290
+480:1:295
+481:1:299
+482:1:300
+483:1:308
+484:1:309
+485:1:313
+486:1:314
+487:1:308
+488:1:309
+489:1:313
+490:1:314
+491:1:322
+492:1:334
+493:1:335
+494:1:339
+495:1:340
+496:1:341
+497:1:352
+498:1:357
+499:1:358
+500:1:369
+501:1:370
+502:1:371
+503:1:369
+504:1:370
+505:1:371
+506:1:382
+507:0:4646
+508:1:15
+509:0:4646
+510:1:16
+511:0:4646
+512:2:4459
+513:0:4646
+514:1:17
+515:0:4646
+516:2:4460
+517:0:4646
+518:1:26
+519:0:4646
+520:2:4459
+521:0:4646
+522:1:30
+523:1:31
+524:1:35
+525:1:39
+526:1:40
+527:1:44
+528:1:52
+529:1:53
+530:1:57
+531:1:61
+532:1:62
+533:1:57
+534:1:61
+535:1:62
+536:1:66
+537:1:73
+538:1:80
+539:1:81
+540:1:88
+541:1:93
+542:1:100
+543:1:101
+544:1:100
+545:1:101
+546:1:108
+547:1:112
+548:0:4646
+549:2:4460
+550:0:4646
+551:1:117
+552:0:4646
+553:2:4461
+554:0:4646
+555:2:4466
+556:0:4646
+557:2:4467
+558:0:4646
+559:2:4475
+560:2:4476
+561:2:4480
+562:2:4484
+563:2:4485
+564:2:4489
+565:2:4497
+566:2:4498
+567:2:4502
+568:2:4506
+569:2:4507
+570:2:4502
+571:2:4506
+572:2:4507
+573:2:4511
+574:2:4518
+575:2:4525
+576:2:4526
+577:2:4533
+578:2:4538
+579:2:4545
+580:2:4546
+581:2:4545
+582:2:4546
+583:2:4553
+584:2:4557
+585:0:4646
+586:2:3746
+587:2:3756
+588:0:4646
+589:2:2885
+590:0:4646
+591:2:3747
+592:2:3748
+593:0:4646
+594:2:2885
+595:0:4646
+596:2:3752
+597:0:4646
+598:2:3760
+599:0:4646
+600:2:2878
+601:0:4646
+602:2:2880
+603:0:4646
+604:2:2881
+605:0:4646
+606:2:2882
+607:0:4646
+608:2:2883
+609:0:4646
+610:2:2884
+611:0:4646
+612:2:2885
+613:0:4646
+614:2:2886
+615:2:2887
+616:2:2891
+617:2:2892
+618:2:2900
+619:2:2901
+620:2:2905
+621:2:2906
+622:2:2914
+623:2:2919
+624:2:2923
+625:2:2924
+626:2:2932
+627:2:2933
+628:2:2934
+629:2:2932
+630:2:2933
+631:2:2937
+632:2:2938
+633:2:2946
+634:2:2951
+635:2:2952
+636:2:2963
+637:2:2964
+638:2:2965
+639:2:2976
+640:2:2981
+641:2:2982
+642:2:2993
+643:2:2994
+644:2:2995
+645:2:2993
+646:2:2994
+647:2:2995
+648:2:3006
+649:2:3014
+650:0:4646
+651:2:2885
+652:0:4646
+653:2:3018
+654:2:3022
+655:2:3023
+656:2:3027
+657:2:3031
+658:2:3032
+659:2:3036
+660:2:3044
+661:2:3045
+662:2:3049
+663:2:3050
+664:2:3049
+665:2:3053
+666:2:3054
+667:2:3058
+668:0:4646
+669:2:2885
+670:0:4646
+671:2:3066
+672:2:3067
+673:2:3068
+674:0:4646
+675:2:2885
+676:0:4646
+677:2:3073
+678:0:4646
+679:2:3775
+680:2:3776
+681:2:3780
+682:2:3784
+683:2:3785
+684:2:3789
+685:2:3794
+686:2:3802
+687:2:3806
+688:2:3807
+689:2:3802
+690:2:3806
+691:2:3807
+692:2:3811
+693:2:3818
+694:2:3825
+695:2:3826
+696:2:3833
+697:2:3838
+698:2:3845
+699:2:3846
+700:2:3845
+701:2:3846
+702:2:3853
+703:2:3857
+704:0:4646
+705:2:3862
+706:0:4646
+707:2:3863
+708:0:4646
+709:2:3864
+710:0:4646
+711:2:3865
+712:0:4646
+713:1:118
+714:0:4646
+715:2:3866
+716:0:4646
+717:1:120
+718:0:4646
+719:2:3865
+720:0:4646
+721:1:19
+722:0:4646
+723:2:3866
+724:0:4646
+725:1:391
+726:1:392
+727:1:396
+728:1:397
+729:1:405
+730:1:406
+731:1:410
+732:1:411
+733:1:419
+734:1:424
+735:1:428
+736:1:429
+737:1:437
+738:1:438
+739:1:442
+740:1:443
+741:1:437
+742:1:438
+743:1:442
+744:1:443
+745:1:451
+746:1:456
+747:1:457
+748:1:468
+749:1:469
+750:1:470
+751:1:481
+752:1:493
+753:1:494
+754:1:498
+755:1:499
+756:1:500
+757:1:498
+758:1:499
+759:1:500
+760:1:511
+761:1:518
+762:0:4646
+763:1:15
+764:0:4646
+765:1:16
+766:0:4646
+767:2:3865
+768:0:4646
+769:1:17
+770:0:4646
+771:2:3866
+772:0:4646
+773:1:118
+774:0:4646
+775:1:120
+776:0:4646
+777:2:3865
+778:0:4646
+779:1:19
+780:0:4646
+781:2:3866
+782:0:4646
+783:1:656
+784:1:657
+785:1:661
+786:1:662
+787:1:670
+788:1:671
+789:1:672
+790:1:684
+791:1:689
+792:1:693
+793:1:694
+794:1:702
+795:1:703
+796:1:707
+797:1:708
+798:1:702
+799:1:703
+800:1:707
+801:1:708
+802:1:716
+803:1:721
+804:1:722
+805:1:733
+806:1:734
+807:1:735
+808:1:746
+809:1:758
+810:1:759
+811:1:763
+812:1:764
+813:1:765
+814:1:763
+815:1:764
+816:1:765
+817:1:776
+818:0:4646
+819:1:15
+820:0:4646
+821:1:16
+822:0:4646
+823:2:3865
+824:0:4646
+825:1:17
+826:0:4646
+827:2:3866
+828:0:4646
+829:1:118
+830:0:4646
+831:1:120
+832:0:4646
+833:2:3865
+834:0:4646
+835:1:19
+836:0:4646
+837:2:3866
+838:0:4646
+839:1:785
+840:1:788
+841:1:789
+842:0:4646
+843:1:15
+844:0:4646
+845:1:16
+846:0:4646
+847:2:3865
+848:0:4646
+849:1:17
+850:0:4646
+851:2:3866
+852:0:4646
+853:1:118
+854:0:4646
+855:1:120
+856:0:4646
+857:2:3865
+858:0:4646
+859:1:19
+860:0:4646
+861:2:3866
+862:0:4646
+863:1:1052
+864:1:1053
+865:1:1057
+866:1:1058
+867:1:1066
+868:1:1067
+869:1:1071
+870:1:1072
+871:1:1080
+872:1:1085
+873:1:1089
+874:1:1090
+875:1:1098
+876:1:1099
+877:1:1103
+878:1:1104
+879:1:1098
+880:1:1099
+881:1:1103
+882:1:1104
+883:1:1112
+884:1:1117
+885:1:1118
+886:1:1129
+887:1:1130
+888:1:1131
+889:1:1142
+890:1:1154
+891:1:1155
+892:1:1159
+893:1:1160
+894:1:1161
+895:1:1159
+896:1:1160
+897:1:1161
+898:1:1172
+899:1:1179
+900:1:1183
+901:0:4646
+902:1:15
+903:0:4646
+904:1:16
+905:0:4646
+906:2:3865
+907:0:4646
+908:1:17
+909:0:4646
+910:2:3866
+911:0:4646
+912:1:118
+913:0:4646
+914:1:120
+915:0:4646
+916:2:3865
+917:0:4646
+918:1:19
+919:0:4646
+920:2:3866
+921:0:4646
+922:1:1184
+923:1:1185
+924:1:1189
+925:1:1190
+926:1:1198
+927:1:1199
+928:1:1200
+929:1:1212
+930:1:1217
+931:1:1221
+932:1:1222
+933:1:1230
+934:1:1231
+935:1:1235
+936:1:1236
+937:1:1230
+938:1:1231
+939:1:1235
+940:1:1236
+941:1:1244
+942:1:1249
+943:1:1250
+944:1:1261
+945:1:1262
+946:1:1263
+947:1:1274
+948:1:1286
+949:1:1287
+950:1:1291
+951:1:1292
+952:1:1293
+953:1:1291
+954:1:1292
+955:1:1293
+956:1:1304
+957:0:4646
+958:1:15
+959:0:4646
+960:1:16
+961:0:4646
+962:2:3865
+963:0:4646
+964:1:17
+965:0:4646
+966:2:3866
+967:0:4646
+968:1:26
+969:0:4646
+970:2:3865
+971:0:4646
+972:1:30
+973:1:31
+974:1:35
+975:1:39
+976:1:40
+977:1:44
+978:1:52
+979:1:53
+980:1:57
+981:1:61
+982:1:62
+983:1:57
+984:1:61
+985:1:62
+986:1:66
+987:1:73
+988:1:80
+989:1:81
+990:1:88
+991:1:93
+992:1:100
+993:1:101
+994:1:100
+995:1:101
+996:1:108
+997:1:112
+998:0:4646
+999:2:3866
+1000:0:4646
+1001:1:117
+1002:0:4646
+1003:2:3867
+1004:0:4646
+1005:2:3872
+1006:0:4646
+1007:2:3873
+1008:0:4646
+1009:2:3881
+1010:2:3882
+1011:2:3886
+1012:2:3890
+1013:2:3891
+1014:2:3895
+1015:2:3903
+1016:2:3904
+1017:2:3908
+1018:2:3912
+1019:2:3913
+1020:2:3908
+1021:2:3912
+1022:2:3913
+1023:2:3917
+1024:2:3924
+1025:2:3931
+1026:2:3932
+1027:2:3939
+1028:2:3944
+1029:2:3951
+1030:2:3952
+1031:2:3951
+1032:2:3952
+1033:2:3959
+1034:2:3963
+1035:0:4646
+1036:2:3075
+1037:2:3756
+1038:0:4646
+1039:2:2885
+1040:0:4646
+1041:2:3076
+1042:0:4646
+1043:2:2885
+1044:0:4646
+1045:2:3079
+1046:2:3080
+1047:2:3084
+1048:2:3085
+1049:2:3093
+1050:2:3094
+1051:2:3098
+1052:2:3099
+1053:2:3107
+1054:2:3112
+1055:2:3116
+1056:2:3117
+1057:2:3125
+1058:2:3126
+1059:2:3130
+1060:2:3131
+1061:2:3125
+1062:2:3126
+1063:2:3130
+1064:2:3131
+1065:2:3139
+1066:2:3144
+1067:2:3145
+1068:2:3156
+1069:2:3157
+1070:2:3158
+1071:2:3169
+1072:2:3174
+1073:2:3175
+1074:2:3186
+1075:2:3187
+1076:2:3188
+1077:2:3186
+1078:2:3187
+1079:2:3188
+1080:2:3199
+1081:2:3206
+1082:0:4646
+1083:2:2885
+1084:0:4646
+1085:2:3210
+1086:2:3211
+1087:2:3212
+1088:2:3224
+1089:2:3225
+1090:2:3229
+1091:2:3230
+1092:2:3238
+1093:2:3243
+1094:2:3247
+1095:2:3248
+1096:2:3256
+1097:2:3257
+1098:2:3261
+1099:2:3262
+1100:2:3256
+1101:2:3257
+1102:2:3261
+1103:2:3262
+1104:2:3270
+1105:2:3275
+1106:2:3276
+1107:2:3287
+1108:2:3288
+1109:2:3289
+1110:2:3300
+1111:2:3305
+1112:2:3306
+1113:2:3317
+1114:2:3318
+1115:2:3319
+1116:2:3317
+1117:2:3318
+1118:2:3319
+1119:2:3330
+1120:2:3340
+1121:2:3341
+1122:0:4646
+1123:2:2885
+1124:0:4646
+1125:2:3744
+1126:0:4646
+1127:2:4369
+1128:2:4370
+1129:2:4374
+1130:2:4378
+1131:2:4379
+1132:2:4383
+1133:2:4391
+1134:2:4392
+1135:2:4396
+1136:2:4400
+1137:2:4401
+1138:2:4396
+1139:2:4400
+1140:2:4401
+1141:2:4405
+1142:2:4412
+1143:2:4419
+1144:2:4420
+1145:2:4427
+1146:2:4432
+1147:2:4439
+1148:2:4440
+1149:2:4439
+1150:2:4440
+1151:2:4447
+1152:2:4451
+1153:0:4646
+1154:2:4456
+1155:0:4646
+1156:2:4457
+1157:0:4646
+1158:2:4458
+1159:0:4646
+1160:2:4459
+1161:0:4646
+1162:1:26
+1163:0:4646
+1164:2:4460
+1165:0:4646
+1166:1:30
+1167:1:31
+1168:1:35
+1169:1:39
+1170:1:40
+1171:1:44
+1172:1:52
+1173:1:53
+1174:1:57
+1175:1:61
+1176:1:62
+1177:1:57
+1178:1:61
+1179:1:62
+1180:1:66
+1181:1:73
+1182:1:80
+1183:1:81
+1184:1:88
+1185:1:93
+1186:1:100
+1187:1:101
+1188:1:100
+1189:1:101
+1190:1:108
+1191:1:112
+1192:0:4646
+1193:2:4459
+1194:0:4646
+1195:1:117
+1196:0:4646
+1197:2:4460
+1198:0:4646
+1199:2:4461
+1200:0:4646
+1201:2:4466
+1202:0:4646
+1203:2:4467
+1204:0:4646
+1205:2:4475
+1206:2:4476
+1207:2:4480
+1208:2:4484
+1209:2:4485
+1210:2:4489
+1211:2:4497
+1212:2:4498
+1213:2:4502
+1214:2:4506
+1215:2:4507
+1216:2:4502
+1217:2:4506
+1218:2:4507
+1219:2:4511
+1220:2:4518
+1221:2:4525
+1222:2:4526
+1223:2:4533
+1224:2:4538
+1225:2:4545
+1226:2:4546
+1227:2:4545
+1228:2:4546
+1229:2:4553
+1230:2:4557
+1231:0:4646
+1232:2:3746
+1233:2:3756
+1234:0:4646
+1235:2:2885
+1236:0:4646
+1237:2:3747
+1238:2:3748
+1239:0:4646
+1240:2:2885
+1241:0:4646
+1242:2:3752
+1243:0:4646
+1244:2:3760
+1245:0:4646
+1246:2:2878
+1247:0:4646
+1248:2:2880
+1249:0:4646
+1250:2:2881
+1251:0:4646
+1252:2:2882
+1253:0:4646
+1254:2:2883
+1255:0:4646
+1256:2:2884
+1257:0:4646
+1258:2:2885
+1259:0:4646
+1260:2:2886
+1261:2:2887
+1262:2:2891
+1263:2:2892
+1264:2:2900
+1265:2:2901
+1266:2:2905
+1267:2:2906
+1268:2:2914
+1269:2:2919
+1270:2:2923
+1271:2:2924
+1272:2:2932
+1273:2:2933
+1274:2:2937
+1275:2:2938
+1276:2:2932
+1277:2:2933
+1278:2:2934
+1279:2:2946
+1280:2:2951
+1281:2:2952
+1282:2:2963
+1283:2:2964
+1284:2:2965
+1285:2:2976
+1286:2:2981
+1287:2:2982
+1288:2:2993
+1289:2:2994
+1290:2:2995
+1291:2:2993
+1292:2:2994
+1293:2:2995
+1294:2:3006
+1295:2:3014
+1296:0:4646
+1297:2:2885
+1298:0:4646
+1299:1:118
+1300:0:4646
+1301:1:120
+1302:0:4646
+1303:1:19
+1304:0:4646
+1305:1:1313
+1306:0:4646
+1307:1:2777
+1308:1:2784
+1309:1:2785
+1310:1:2792
+1311:1:2797
+1312:1:2804
+1313:1:2805
+1314:1:2804
+1315:1:2805
+1316:1:2812
+1317:1:2816
+1318:0:4646
+1319:2:3018
+1320:2:3022
+1321:2:3023
+1322:2:3027
+1323:2:3031
+1324:2:3032
+1325:2:3036
+1326:2:3044
+1327:2:3045
+1328:2:3049
+1329:2:3053
+1330:2:3054
+1331:2:3049
+1332:2:3050
+1333:2:3058
+1334:0:4646
+1335:2:2885
+1336:0:4646
+1337:2:3066
+1338:2:3067
+1339:2:3068
+1340:0:4646
+1341:2:2885
+1342:0:4646
+1343:2:3073
+1344:0:4646
+1345:2:3775
+1346:2:3776
+1347:2:3780
+1348:2:3784
+1349:2:3785
+1350:2:3789
+1351:2:3794
+1352:2:3802
+1353:2:3806
+1354:2:3807
+1355:2:3802
+1356:2:3806
+1357:2:3807
+1358:2:3811
+1359:2:3818
+1360:2:3825
+1361:2:3826
+1362:2:3833
+1363:2:3838
+1364:2:3845
+1365:2:3846
+1366:2:3845
+1367:2:3846
+1368:2:3853
+1369:2:3857
+1370:0:4646
+1371:2:3862
+1372:0:4646
+1373:2:3863
+1374:0:4646
+1375:2:3864
+1376:0:4646
+1377:2:3865
+1378:0:4646
+1379:1:1315
+1380:1:1316
+1381:0:4644
+1382:2:3866
+1383:0:4650
+1384:1:2431