X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;ds=sidebyside;f=formal-model%2Fresults%2Furcu-controldataflow-no-ipi%2Fresult-ipi-urcu_free%2Furcu_free_single_flip.spin.input.trail;fp=formal-model%2Fresults%2Furcu-controldataflow-no-ipi%2Fresult-ipi-urcu_free%2Furcu_free_single_flip.spin.input.trail;h=eaf17807ecfa8c589fce48c7a7deedece6da8dfe;hb=dbf6928575dc30b5d8602b9a50ca385670f26ff1;hp=0000000000000000000000000000000000000000;hpb=6b0de96380f9abdb7a77b79d3b2d0cf5762f266f;p=urcu.git

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