X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;ds=sidebyside;f=formal-model%2Furcu-controldataflow-intel-ipi%2Furcu_free_single_flip.spin.input.trail;fp=formal-model%2Furcu-controldataflow-intel-ipi%2Furcu_free_single_flip.spin.input.trail;h=05857aab2de72ed2d43743869520932c6b78610b;hb=b6b17880a1a83b679d968907e2ff6cf72dd645fb;hp=0000000000000000000000000000000000000000;hpb=06e8b2a87f862183a26e0005bf04221633f49d0c;p=userspace-rcu.git

diff --git a/formal-model/urcu-controldataflow-intel-ipi/urcu_free_single_flip.spin.input.trail b/formal-model/urcu-controldataflow-intel-ipi/urcu_free_single_flip.spin.input.trail
new file mode 100644
index 0000000..05857aa
--- /dev/null
+++ b/formal-model/urcu-controldataflow-intel-ipi/urcu_free_single_flip.spin.input.trail
@@ -0,0 +1,1301 @@
+-2:3:-2
+-4:-4:-4
+1:0:4179
+2:3:4099
+3:3:4102
+4:3:4102
+5:3:4105
+6:3:4113
+7:3:4113
+8:3:4116
+9:3:4122
+10:3:4126
+11:3:4126
+12:3:4129
+13:3:4139
+14:3:4147
+15:3:4147
+16:3:4150
+17:3:4156
+18:3:4160
+19:3:4160
+20:3:4163
+21:3:4169
+22:3:4173
+23:3:4174
+24:0:4179
+25:3:4176
+26:0:4179
+27:2:2511
+28:0:4179
+29:2:2517
+30:0:4179
+31:2:2518
+32:0:4179
+33:2:2520
+34:0:4179
+35:2:2521
+36:0:4179
+37:2:2522
+38:0:4179
+39:2:2523
+40:0:4179
+41:2:2524
+42:0:4179
+43:2:2525
+44:0:4179
+45:2:2526
+46:2:2527
+47:2:2531
+48:2:2532
+49:2:2540
+50:2:2541
+51:2:2545
+52:2:2546
+53:2:2554
+54:2:2559
+55:2:2563
+56:2:2564
+57:2:2572
+58:2:2573
+59:2:2577
+60:2:2578
+61:2:2572
+62:2:2573
+63:2:2577
+64:2:2578
+65:2:2586
+66:2:2591
+67:2:2598
+68:2:2599
+69:2:2606
+70:2:2611
+71:2:2618
+72:2:2619
+73:2:2618
+74:2:2619
+75:2:2626
+76:2:2636
+77:0:4179
+78:2:2525
+79:0:4179
+80:2:2640
+81:2:2644
+82:2:2645
+83:2:2649
+84:2:2653
+85:2:2654
+86:2:2658
+87:2:2666
+88:2:2667
+89:2:2671
+90:2:2675
+91:2:2676
+92:2:2671
+93:2:2672
+94:2:2680
+95:0:4179
+96:2:2525
+97:0:4179
+98:2:2688
+99:2:2689
+100:2:2690
+101:0:4179
+102:2:2525
+103:0:4179
+104:2:2695
+105:0:4179
+106:2:3308
+107:2:3309
+108:2:3313
+109:2:3317
+110:2:3318
+111:2:3322
+112:2:3327
+113:2:3335
+114:2:3339
+115:2:3340
+116:2:3335
+117:2:3339
+118:2:3340
+119:2:3344
+120:2:3351
+121:2:3358
+122:2:3359
+123:2:3366
+124:2:3371
+125:2:3378
+126:2:3379
+127:2:3378
+128:2:3379
+129:2:3386
+130:2:3390
+131:0:4179
+132:2:3395
+133:0:4179
+134:2:3396
+135:0:4179
+136:2:3397
+137:0:4179
+138:2:3398
+139:0:4179
+140:1:2
+141:0:4179
+142:2:3399
+143:0:4179
+144:1:8
+145:0:4179
+146:1:9
+147:0:4179
+148:2:3398
+149:0:4179
+150:1:10
+151:0:4179
+152:2:3399
+153:0:4179
+154:1:11
+155:0:4179
+156:2:3398
+157:0:4179
+158:1:12
+159:0:4179
+160:2:3399
+161:0:4179
+162:1:13
+163:0:4179
+164:2:3398
+165:0:4179
+166:1:14
+167:0:4179
+168:2:3399
+169:0:4179
+170:1:15
+171:0:4179
+172:1:16
+173:0:4179
+174:2:3398
+175:0:4179
+176:1:17
+177:0:4179
+178:2:3399
+179:0:4179
+180:1:26
+181:0:4179
+182:2:3398
+183:0:4179
+184:1:30
+185:1:31
+186:1:35
+187:1:39
+188:1:40
+189:1:44
+190:1:52
+191:1:53
+192:1:57
+193:1:61
+194:1:62
+195:1:57
+196:1:61
+197:1:62
+198:1:66
+199:1:73
+200:1:80
+201:1:81
+202:1:88
+203:1:93
+204:1:100
+205:1:101
+206:1:100
+207:1:101
+208:1:108
+209:1:112
+210:0:4179
+211:2:3399
+212:0:4179
+213:1:117
+214:0:4179
+215:2:3400
+216:0:4179
+217:2:3405
+218:0:4179
+219:2:3406
+220:0:4179
+221:2:3414
+222:2:3415
+223:2:3419
+224:2:3423
+225:2:3424
+226:2:3428
+227:2:3436
+228:2:3437
+229:2:3441
+230:2:3445
+231:2:3446
+232:2:3441
+233:2:3445
+234:2:3446
+235:2:3450
+236:2:3457
+237:2:3464
+238:2:3465
+239:2:3472
+240:2:3477
+241:2:3484
+242:2:3485
+243:2:3484
+244:2:3485
+245:2:3492
+246:2:3496
+247:0:4179
+248:2:2697
+249:2:3289
+250:0:4179
+251:2:2525
+252:0:4179
+253:2:2698
+254:0:4179
+255:2:2525
+256:0:4179
+257:2:2701
+258:2:2702
+259:2:2706
+260:2:2707
+261:2:2715
+262:2:2716
+263:2:2720
+264:2:2721
+265:2:2729
+266:2:2734
+267:2:2738
+268:2:2739
+269:2:2747
+270:2:2748
+271:2:2752
+272:2:2753
+273:2:2747
+274:2:2748
+275:2:2752
+276:2:2753
+277:2:2761
+278:2:2766
+279:2:2773
+280:2:2774
+281:2:2781
+282:2:2786
+283:2:2793
+284:2:2794
+285:2:2793
+286:2:2794
+287:2:2801
+288:2:2810
+289:0:4179
+290:2:2525
+291:0:4179
+292:2:2814
+293:2:2823
+294:2:2824
+295:2:2828
+296:2:2829
+297:2:2833
+298:2:2834
+299:2:2842
+300:2:2847
+301:2:2851
+302:2:2852
+303:2:2860
+304:2:2861
+305:2:2865
+306:2:2866
+307:2:2860
+308:2:2861
+309:2:2865
+310:2:2866
+311:2:2874
+312:2:2881
+313:2:2882
+314:2:2886
+315:2:2887
+316:2:2894
+317:2:2899
+318:2:2906
+319:2:2907
+320:2:2906
+321:2:2907
+322:2:2914
+323:2:2926
+324:2:2927
+325:0:4179
+326:2:2525
+327:0:4179
+328:2:3277
+329:0:4179
+330:1:118
+331:0:4179
+332:1:120
+333:0:4179
+334:1:19
+335:0:4179
+336:1:126
+337:1:127
+338:1:131
+339:1:132
+340:1:140
+341:1:141
+342:1:145
+343:1:146
+344:1:154
+345:1:159
+346:1:163
+347:1:164
+348:1:172
+349:1:173
+350:1:177
+351:1:178
+352:1:172
+353:1:173
+354:1:177
+355:1:178
+356:1:186
+357:1:191
+358:1:198
+359:1:199
+360:1:206
+361:1:211
+362:1:218
+363:1:219
+364:1:218
+365:1:219
+366:1:226
+367:0:4179
+368:1:15
+369:0:4179
+370:1:16
+371:0:4179
+372:1:17
+373:0:4179
+374:1:118
+375:0:4179
+376:1:120
+377:0:4179
+378:1:19
+379:0:4179
+380:1:237
+381:1:238
+382:0:4179
+383:1:15
+384:0:4179
+385:1:16
+386:0:4179
+387:1:17
+388:0:4179
+389:1:118
+390:0:4179
+391:1:120
+392:0:4179
+393:1:19
+394:0:4179
+395:1:244
+396:1:245
+397:1:249
+398:1:250
+399:1:258
+400:1:259
+401:1:263
+402:1:264
+403:1:272
+404:1:277
+405:1:281
+406:1:282
+407:1:290
+408:1:291
+409:1:295
+410:1:296
+411:1:290
+412:1:291
+413:1:295
+414:1:296
+415:1:304
+416:1:309
+417:1:316
+418:1:317
+419:1:324
+420:1:329
+421:1:336
+422:1:337
+423:1:336
+424:1:337
+425:1:344
+426:0:4179
+427:1:15
+428:0:4179
+429:1:16
+430:0:4179
+431:2:3899
+432:2:3907
+433:2:3911
+434:2:3912
+435:2:3916
+436:2:3924
+437:2:3925
+438:2:3929
+439:2:3933
+440:2:3934
+441:2:3929
+442:2:3933
+443:2:3934
+444:2:3938
+445:2:3945
+446:2:3952
+447:2:3953
+448:2:3960
+449:2:3965
+450:2:3972
+451:2:3973
+452:2:3972
+453:2:3973
+454:2:3980
+455:2:3984
+456:0:4179
+457:2:3989
+458:0:4179
+459:2:3990
+460:0:4179
+461:2:3991
+462:0:4179
+463:2:3992
+464:0:4179
+465:1:17
+466:0:4179
+467:2:3993
+468:0:4179
+469:1:26
+470:0:4179
+471:2:3992
+472:0:4179
+473:1:30
+474:1:31
+475:1:35
+476:1:39
+477:1:40
+478:1:44
+479:1:52
+480:1:53
+481:1:57
+482:1:61
+483:1:62
+484:1:57
+485:1:61
+486:1:62
+487:1:66
+488:1:73
+489:1:80
+490:1:81
+491:1:88
+492:1:93
+493:1:100
+494:1:101
+495:1:100
+496:1:101
+497:1:108
+498:1:112
+499:0:4179
+500:2:3993
+501:0:4179
+502:1:117
+503:0:4179
+504:2:3994
+505:0:4179
+506:2:3999
+507:0:4179
+508:2:4000
+509:0:4179
+510:2:4008
+511:2:4009
+512:2:4013
+513:2:4017
+514:2:4018
+515:2:4022
+516:2:4030
+517:2:4031
+518:2:4035
+519:2:4039
+520:2:4040
+521:2:4035
+522:2:4039
+523:2:4040
+524:2:4044
+525:2:4051
+526:2:4058
+527:2:4059
+528:2:4066
+529:2:4071
+530:2:4078
+531:2:4079
+532:2:4078
+533:2:4079
+534:2:4086
+535:2:4090
+536:0:4179
+537:2:3279
+538:2:3289
+539:0:4179
+540:2:2525
+541:0:4179
+542:2:3280
+543:2:3281
+544:0:4179
+545:2:2525
+546:0:4179
+547:2:3285
+548:0:4179
+549:2:3293
+550:0:4179
+551:2:2518
+552:0:4179
+553:2:2520
+554:0:4179
+555:2:2521
+556:0:4179
+557:2:2522
+558:0:4179
+559:2:2523
+560:0:4179
+561:2:2524
+562:0:4179
+563:2:2525
+564:0:4179
+565:2:2526
+566:2:2527
+567:2:2531
+568:2:2532
+569:2:2540
+570:2:2541
+571:2:2545
+572:2:2546
+573:2:2554
+574:2:2559
+575:2:2563
+576:2:2564
+577:2:2572
+578:2:2573
+579:2:2574
+580:2:2572
+581:2:2573
+582:2:2577
+583:2:2578
+584:2:2586
+585:2:2591
+586:2:2598
+587:2:2599
+588:2:2606
+589:2:2611
+590:2:2618
+591:2:2619
+592:2:2618
+593:2:2619
+594:2:2626
+595:2:2636
+596:0:4179
+597:2:2525
+598:0:4179
+599:2:2640
+600:2:2644
+601:2:2645
+602:2:2649
+603:2:2653
+604:2:2654
+605:2:2658
+606:2:2666
+607:2:2667
+608:2:2671
+609:2:2672
+610:2:2671
+611:2:2675
+612:2:2676
+613:2:2680
+614:0:4179
+615:2:2525
+616:0:4179
+617:2:2688
+618:2:2689
+619:2:2690
+620:0:4179
+621:2:2525
+622:0:4179
+623:2:2695
+624:0:4179
+625:1:118
+626:0:4179
+627:1:120
+628:0:4179
+629:1:19
+630:0:4179
+631:1:355
+632:1:356
+633:1:360
+634:1:361
+635:1:369
+636:1:370
+637:1:374
+638:1:375
+639:1:383
+640:1:388
+641:1:392
+642:1:393
+643:1:401
+644:1:402
+645:1:406
+646:1:407
+647:1:401
+648:1:402
+649:1:406
+650:1:407
+651:1:415
+652:1:420
+653:1:427
+654:1:428
+655:1:435
+656:1:440
+657:1:447
+658:1:448
+659:1:447
+660:1:448
+661:1:455
+662:1:464
+663:0:4179
+664:1:15
+665:0:4179
+666:1:16
+667:0:4179
+668:1:17
+669:0:4179
+670:1:118
+671:0:4179
+672:1:120
+673:0:4179
+674:1:19
+675:0:4179
+676:1:584
+677:1:585
+678:1:589
+679:1:590
+680:1:598
+681:1:599
+682:1:600
+683:1:612
+684:1:617
+685:1:621
+686:1:622
+687:1:630
+688:1:631
+689:1:635
+690:1:636
+691:1:630
+692:1:631
+693:1:635
+694:1:636
+695:1:644
+696:1:649
+697:1:656
+698:1:657
+699:1:664
+700:1:669
+701:1:676
+702:1:677
+703:1:676
+704:1:677
+705:1:684
+706:0:4179
+707:1:15
+708:0:4179
+709:1:16
+710:0:4179
+711:1:17
+712:0:4179
+713:1:118
+714:0:4179
+715:1:120
+716:0:4179
+717:1:19
+718:0:4179
+719:1:695
+720:1:698
+721:1:699
+722:0:4179
+723:1:15
+724:0:4179
+725:1:16
+726:0:4179
+727:1:17
+728:0:4179
+729:1:118
+730:0:4179
+731:1:120
+732:0:4179
+733:1:19
+734:0:4179
+735:1:702
+736:1:703
+737:1:707
+738:1:708
+739:1:716
+740:1:717
+741:1:721
+742:1:722
+743:1:730
+744:1:735
+745:1:739
+746:1:740
+747:1:748
+748:1:749
+749:1:753
+750:1:754
+751:1:748
+752:1:749
+753:1:753
+754:1:754
+755:1:762
+756:1:767
+757:1:774
+758:1:775
+759:1:782
+760:1:787
+761:1:794
+762:1:795
+763:1:794
+764:1:795
+765:1:802
+766:0:4179
+767:1:15
+768:0:4179
+769:1:16
+770:0:4179
+771:1:17
+772:0:4179
+773:1:118
+774:0:4179
+775:1:120
+776:0:4179
+777:1:19
+778:0:4179
+779:1:926
+780:1:927
+781:1:931
+782:1:932
+783:1:940
+784:1:941
+785:1:945
+786:1:946
+787:1:954
+788:1:959
+789:1:963
+790:1:964
+791:1:972
+792:1:973
+793:1:977
+794:1:978
+795:1:972
+796:1:973
+797:1:977
+798:1:978
+799:1:986
+800:1:991
+801:1:998
+802:1:999
+803:1:1006
+804:1:1011
+805:1:1018
+806:1:1019
+807:1:1018
+808:1:1019
+809:1:1026
+810:1:1035
+811:1:1039
+812:0:4179
+813:1:15
+814:0:4179
+815:1:16
+816:0:4179
+817:1:17
+818:0:4179
+819:1:118
+820:0:4179
+821:1:120
+822:0:4179
+823:1:19
+824:0:4179
+825:1:1040
+826:1:1041
+827:1:1045
+828:1:1046
+829:1:1054
+830:1:1055
+831:1:1056
+832:1:1068
+833:1:1073
+834:1:1077
+835:1:1078
+836:1:1086
+837:1:1087
+838:1:1091
+839:1:1092
+840:1:1086
+841:1:1087
+842:1:1091
+843:1:1092
+844:1:1100
+845:1:1105
+846:1:1112
+847:1:1113
+848:1:1120
+849:1:1125
+850:1:1132
+851:1:1133
+852:1:1132
+853:1:1133
+854:1:1140
+855:0:4179
+856:1:15
+857:0:4179
+858:1:16
+859:0:4179
+860:2:3308
+861:2:3309
+862:2:3313
+863:2:3317
+864:2:3318
+865:2:3322
+866:2:3327
+867:2:3335
+868:2:3339
+869:2:3340
+870:2:3335
+871:2:3339
+872:2:3340
+873:2:3344
+874:2:3351
+875:2:3358
+876:2:3359
+877:2:3366
+878:2:3371
+879:2:3378
+880:2:3379
+881:2:3378
+882:2:3379
+883:2:3386
+884:2:3390
+885:0:4179
+886:2:3395
+887:0:4179
+888:2:3396
+889:0:4179
+890:2:3397
+891:0:4179
+892:2:3398
+893:0:4179
+894:1:17
+895:0:4179
+896:2:3399
+897:0:4179
+898:1:26
+899:0:4179
+900:2:3398
+901:0:4179
+902:1:30
+903:1:31
+904:1:35
+905:1:39
+906:1:40
+907:1:44
+908:1:52
+909:1:53
+910:1:57
+911:1:61
+912:1:62
+913:1:57
+914:1:61
+915:1:62
+916:1:66
+917:1:73
+918:1:80
+919:1:81
+920:1:88
+921:1:93
+922:1:100
+923:1:101
+924:1:100
+925:1:101
+926:1:108
+927:1:112
+928:0:4179
+929:2:3399
+930:0:4179
+931:1:117
+932:0:4179
+933:2:3400
+934:0:4179
+935:2:3405
+936:0:4179
+937:2:3406
+938:0:4179
+939:2:3414
+940:2:3415
+941:2:3419
+942:2:3423
+943:2:3424
+944:2:3428
+945:2:3436
+946:2:3437
+947:2:3441
+948:2:3445
+949:2:3446
+950:2:3441
+951:2:3445
+952:2:3446
+953:2:3450
+954:2:3457
+955:2:3464
+956:2:3465
+957:2:3472
+958:2:3477
+959:2:3484
+960:2:3485
+961:2:3484
+962:2:3485
+963:2:3492
+964:2:3496
+965:0:4179
+966:2:2697
+967:2:3289
+968:0:4179
+969:2:2525
+970:0:4179
+971:2:2698
+972:0:4179
+973:2:2525
+974:0:4179
+975:2:2701
+976:2:2702
+977:2:2706
+978:2:2707
+979:2:2715
+980:2:2716
+981:2:2720
+982:2:2721
+983:2:2729
+984:2:2734
+985:2:2738
+986:2:2739
+987:2:2747
+988:2:2748
+989:2:2752
+990:2:2753
+991:2:2747
+992:2:2748
+993:2:2752
+994:2:2753
+995:2:2761
+996:2:2766
+997:2:2773
+998:2:2774
+999:2:2781
+1000:2:2786
+1001:2:2793
+1002:2:2794
+1003:2:2793
+1004:2:2794
+1005:2:2801
+1006:2:2810
+1007:0:4179
+1008:2:2525
+1009:0:4179
+1010:2:2814
+1011:2:2815
+1012:2:2816
+1013:2:2828
+1014:2:2829
+1015:2:2833
+1016:2:2834
+1017:2:2842
+1018:2:2847
+1019:2:2851
+1020:2:2852
+1021:2:2860
+1022:2:2861
+1023:2:2865
+1024:2:2866
+1025:2:2860
+1026:2:2861
+1027:2:2865
+1028:2:2866
+1029:2:2874
+1030:2:2879
+1031:2:2886
+1032:2:2887
+1033:2:2894
+1034:2:2899
+1035:2:2906
+1036:2:2907
+1037:2:2906
+1038:2:2907
+1039:2:2914
+1040:2:2926
+1041:2:2927
+1042:0:4179
+1043:2:2525
+1044:0:4179
+1045:2:3277
+1046:0:4179
+1047:2:3902
+1048:2:3903
+1049:2:3907
+1050:2:3911
+1051:2:3912
+1052:2:3916
+1053:2:3924
+1054:2:3925
+1055:2:3929
+1056:2:3933
+1057:2:3934
+1058:2:3929
+1059:2:3933
+1060:2:3934
+1061:2:3938
+1062:2:3945
+1063:2:3952
+1064:2:3953
+1065:2:3960
+1066:2:3965
+1067:2:3972
+1068:2:3973
+1069:2:3972
+1070:2:3973
+1071:2:3980
+1072:2:3984
+1073:0:4179
+1074:2:3989
+1075:0:4179
+1076:2:3990
+1077:0:4179
+1078:2:3991
+1079:0:4179
+1080:2:3992
+1081:0:4179
+1082:1:26
+1083:0:4179
+1084:2:3993
+1085:0:4179
+1086:1:30
+1087:1:31
+1088:1:35
+1089:1:39
+1090:1:40
+1091:1:44
+1092:1:52
+1093:1:53
+1094:1:57
+1095:1:61
+1096:1:62
+1097:1:57
+1098:1:61
+1099:1:62
+1100:1:66
+1101:1:73
+1102:1:80
+1103:1:81
+1104:1:88
+1105:1:93
+1106:1:100
+1107:1:101
+1108:1:100
+1109:1:101
+1110:1:108
+1111:1:112
+1112:0:4179
+1113:2:3992
+1114:0:4179
+1115:1:117
+1116:0:4179
+1117:2:3993
+1118:0:4179
+1119:2:3994
+1120:0:4179
+1121:2:3999
+1122:0:4179
+1123:2:4000
+1124:0:4179
+1125:2:4008
+1126:2:4009
+1127:2:4013
+1128:2:4017
+1129:2:4018
+1130:2:4022
+1131:2:4030
+1132:2:4031
+1133:2:4035
+1134:2:4039
+1135:2:4040
+1136:2:4035
+1137:2:4039
+1138:2:4040
+1139:2:4044
+1140:2:4051
+1141:2:4058
+1142:2:4059
+1143:2:4066
+1144:2:4071
+1145:2:4078
+1146:2:4079
+1147:2:4078
+1148:2:4079
+1149:2:4086
+1150:2:4090
+1151:0:4179
+1152:2:3279
+1153:2:3289
+1154:0:4179
+1155:2:2525
+1156:0:4179
+1157:2:3280
+1158:2:3281
+1159:0:4179
+1160:2:2525
+1161:0:4179
+1162:2:3285
+1163:0:4179
+1164:2:3293
+1165:0:4179
+1166:2:2518
+1167:0:4179
+1168:2:2520
+1169:0:4179
+1170:2:2521
+1171:0:4179
+1172:2:2522
+1173:0:4179
+1174:2:2523
+1175:0:4179
+1176:2:2524
+1177:0:4179
+1178:2:2525
+1179:0:4179
+1180:2:2526
+1181:2:2527
+1182:2:2531
+1183:2:2532
+1184:2:2540
+1185:2:2541
+1186:2:2545
+1187:2:2546
+1188:2:2554
+1189:2:2559
+1190:2:2563
+1191:2:2564
+1192:2:2572
+1193:2:2573
+1194:2:2577
+1195:2:2578
+1196:2:2572
+1197:2:2573
+1198:2:2574
+1199:2:2586
+1200:2:2591
+1201:2:2598
+1202:2:2599
+1203:2:2606
+1204:2:2611
+1205:2:2618
+1206:2:2619
+1207:2:2618
+1208:2:2619
+1209:2:2626
+1210:2:2636
+1211:0:4179
+1212:2:2525
+1213:0:4179
+1214:1:118
+1215:0:4179
+1216:1:120
+1217:0:4179
+1218:1:19
+1219:0:4179
+1220:1:1151
+1221:0:4179
+1222:1:2417
+1223:1:2424
+1224:1:2425
+1225:1:2432
+1226:1:2437
+1227:1:2444
+1228:1:2445
+1229:1:2444
+1230:1:2445
+1231:1:2452
+1232:1:2456
+1233:0:4179
+1234:2:2640
+1235:2:2644
+1236:2:2645
+1237:2:2649
+1238:2:2653
+1239:2:2654
+1240:2:2658
+1241:2:2666
+1242:2:2667
+1243:2:2671
+1244:2:2675
+1245:2:2676
+1246:2:2671
+1247:2:2672
+1248:2:2680
+1249:0:4179
+1250:2:2525
+1251:0:4179
+1252:2:2688
+1253:2:2689
+1254:2:2690
+1255:0:4179
+1256:2:2525
+1257:0:4179
+1258:2:2695
+1259:0:4179
+1260:2:3308
+1261:2:3309
+1262:2:3313
+1263:2:3317
+1264:2:3318
+1265:2:3322
+1266:2:3327
+1267:2:3335
+1268:2:3339
+1269:2:3340
+1270:2:3335
+1271:2:3339
+1272:2:3340
+1273:2:3344
+1274:2:3351
+1275:2:3358
+1276:2:3359
+1277:2:3366
+1278:2:3371
+1279:2:3378
+1280:2:3379
+1281:2:3378
+1282:2:3379
+1283:2:3386
+1284:2:3390
+1285:0:4179
+1286:2:3395
+1287:0:4179
+1288:2:3396
+1289:0:4179
+1290:2:3397
+1291:0:4179
+1292:2:3398
+1293:0:4179
+1294:1:1153
+1295:1:1154
+1296:0:4177
+1297:2:3399
+1298:0:4183
+1299:1:2145