X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-controldataflow-intel-ipi%2Furcu_free_no_wmb.spin.input.trail;fp=formal-model%2Furcu-controldataflow-intel-ipi%2Furcu_free_no_wmb.spin.input.trail;h=62969b96673bbc04ed2f14abb13bc5bafe9f55bc;hp=0000000000000000000000000000000000000000;hb=b6b17880a1a83b679d968907e2ff6cf72dd645fb;hpb=06e8b2a87f862183a26e0005bf04221633f49d0c

diff --git a/formal-model/urcu-controldataflow-intel-ipi/urcu_free_no_wmb.spin.input.trail b/formal-model/urcu-controldataflow-intel-ipi/urcu_free_no_wmb.spin.input.trail
new file mode 100644
index 0000000..62969b9
--- /dev/null
+++ b/formal-model/urcu-controldataflow-intel-ipi/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1434 @@
+-2:3:-2
+-4:-4:-4
+1:0:4177
+2:3:4097
+3:3:4100
+4:3:4100
+5:3:4103
+6:3:4111
+7:3:4111
+8:3:4114
+9:3:4120
+10:3:4124
+11:3:4124
+12:3:4127
+13:3:4137
+14:3:4145
+15:3:4145
+16:3:4148
+17:3:4154
+18:3:4158
+19:3:4158
+20:3:4161
+21:3:4167
+22:3:4171
+23:3:4172
+24:0:4177
+25:3:4174
+26:0:4177
+27:2:2511
+28:0:4177
+29:2:2517
+30:0:4177
+31:2:2518
+32:0:4177
+33:2:2520
+34:0:4177
+35:2:2521
+36:0:4177
+37:2:2522
+38:0:4177
+39:2:2523
+40:2:2524
+41:2:2528
+42:2:2529
+43:2:2537
+44:2:2538
+45:2:2542
+46:2:2543
+47:2:2551
+48:2:2556
+49:2:2560
+50:2:2561
+51:2:2569
+52:2:2570
+53:2:2574
+54:2:2575
+55:2:2569
+56:2:2570
+57:2:2574
+58:2:2575
+59:2:2583
+60:2:2588
+61:2:2595
+62:2:2596
+63:2:2603
+64:2:2608
+65:2:2615
+66:2:2616
+67:2:2615
+68:2:2616
+69:2:2623
+70:2:2633
+71:0:4177
+72:2:2522
+73:0:4177
+74:2:2685
+75:2:2686
+76:2:2687
+77:0:4177
+78:2:2522
+79:0:4177
+80:2:2692
+81:0:4177
+82:2:3306
+83:2:3307
+84:2:3311
+85:2:3315
+86:2:3316
+87:2:3320
+88:2:3325
+89:2:3333
+90:2:3337
+91:2:3338
+92:2:3333
+93:2:3334
+94:2:3342
+95:2:3349
+96:2:3356
+97:2:3357
+98:2:3364
+99:2:3369
+100:2:3376
+101:2:3377
+102:2:3376
+103:2:3377
+104:2:3384
+105:2:3388
+106:0:4177
+107:2:3393
+108:0:4177
+109:2:3394
+110:0:4177
+111:2:3395
+112:0:4177
+113:2:3396
+114:0:4177
+115:1:2
+116:0:4177
+117:2:3397
+118:0:4177
+119:1:8
+120:0:4177
+121:1:9
+122:0:4177
+123:2:3396
+124:0:4177
+125:1:10
+126:0:4177
+127:2:3397
+128:0:4177
+129:1:11
+130:0:4177
+131:2:3396
+132:0:4177
+133:1:12
+134:0:4177
+135:2:3397
+136:0:4177
+137:1:13
+138:0:4177
+139:2:3396
+140:0:4177
+141:1:14
+142:0:4177
+143:2:3397
+144:0:4177
+145:1:15
+146:0:4177
+147:1:16
+148:0:4177
+149:2:3396
+150:0:4177
+151:1:17
+152:0:4177
+153:2:3397
+154:0:4177
+155:1:26
+156:0:4177
+157:2:3396
+158:0:4177
+159:1:30
+160:1:31
+161:1:35
+162:1:39
+163:1:40
+164:1:44
+165:1:52
+166:1:53
+167:1:57
+168:1:61
+169:1:62
+170:1:57
+171:1:61
+172:1:62
+173:1:66
+174:1:73
+175:1:80
+176:1:81
+177:1:88
+178:1:93
+179:1:100
+180:1:101
+181:1:100
+182:1:101
+183:1:108
+184:1:112
+185:0:4177
+186:2:3397
+187:0:4177
+188:1:117
+189:0:4177
+190:2:3398
+191:0:4177
+192:2:3403
+193:0:4177
+194:2:3404
+195:0:4177
+196:2:3412
+197:2:3413
+198:2:3417
+199:2:3421
+200:2:3422
+201:2:3426
+202:2:3434
+203:2:3435
+204:2:3439
+205:2:3443
+206:2:3444
+207:2:3439
+208:2:3443
+209:2:3444
+210:2:3448
+211:2:3455
+212:2:3462
+213:2:3463
+214:2:3470
+215:2:3475
+216:2:3482
+217:2:3483
+218:2:3482
+219:2:3483
+220:2:3490
+221:2:3494
+222:0:4177
+223:2:2694
+224:2:3287
+225:0:4177
+226:2:2522
+227:0:4177
+228:2:2695
+229:0:4177
+230:2:2522
+231:0:4177
+232:2:2698
+233:2:2699
+234:2:2703
+235:2:2704
+236:2:2712
+237:2:2713
+238:2:2717
+239:2:2718
+240:2:2726
+241:2:2731
+242:2:2735
+243:2:2736
+244:2:2744
+245:2:2745
+246:2:2749
+247:2:2750
+248:2:2744
+249:2:2745
+250:2:2749
+251:2:2750
+252:2:2758
+253:2:2763
+254:2:2770
+255:2:2771
+256:2:2778
+257:2:2783
+258:2:2790
+259:2:2791
+260:2:2790
+261:2:2791
+262:2:2798
+263:2:2807
+264:0:4177
+265:2:2522
+266:0:4177
+267:2:2811
+268:2:2812
+269:2:2813
+270:2:2825
+271:2:2826
+272:2:2830
+273:2:2831
+274:2:2839
+275:2:2844
+276:2:2848
+277:2:2849
+278:2:2857
+279:2:2858
+280:2:2862
+281:2:2863
+282:2:2857
+283:2:2858
+284:2:2862
+285:2:2863
+286:2:2871
+287:2:2876
+288:2:2883
+289:2:2884
+290:2:2891
+291:2:2896
+292:2:2903
+293:2:2904
+294:2:2903
+295:2:2904
+296:2:2911
+297:2:2924
+298:2:2925
+299:0:4177
+300:2:2522
+301:0:4177
+302:2:2932
+303:2:2933
+304:2:2937
+305:2:2938
+306:2:2946
+307:2:2947
+308:2:2951
+309:2:2952
+310:2:2960
+311:2:2965
+312:2:2969
+313:2:2970
+314:2:2978
+315:2:2979
+316:2:2983
+317:2:2984
+318:2:2978
+319:2:2979
+320:2:2983
+321:2:2984
+322:2:2992
+323:2:2997
+324:2:3004
+325:2:3005
+326:2:3012
+327:2:3017
+328:2:3024
+329:2:3025
+330:2:3024
+331:2:3025
+332:2:3032
+333:0:4177
+334:2:2522
+335:0:4177
+336:2:3043
+337:2:3044
+338:2:3048
+339:2:3049
+340:2:3057
+341:2:3058
+342:2:3062
+343:2:3063
+344:2:3071
+345:2:3076
+346:2:3080
+347:2:3081
+348:2:3089
+349:2:3090
+350:2:3094
+351:2:3095
+352:2:3089
+353:2:3090
+354:2:3094
+355:2:3095
+356:2:3103
+357:2:3108
+358:2:3115
+359:2:3116
+360:2:3123
+361:2:3128
+362:2:3135
+363:2:3136
+364:2:3135
+365:2:3136
+366:2:3143
+367:2:3152
+368:0:4177
+369:2:2522
+370:0:4177
+371:2:3156
+372:2:3157
+373:2:3158
+374:2:3170
+375:2:3171
+376:2:3175
+377:2:3176
+378:2:3184
+379:2:3189
+380:2:3193
+381:2:3194
+382:2:3202
+383:2:3203
+384:2:3207
+385:2:3208
+386:2:3202
+387:2:3203
+388:2:3207
+389:2:3208
+390:2:3216
+391:2:3221
+392:2:3228
+393:2:3229
+394:2:3236
+395:2:3241
+396:2:3248
+397:2:3249
+398:2:3248
+399:2:3249
+400:2:3256
+401:2:3268
+402:2:3269
+403:0:4177
+404:2:2522
+405:0:4177
+406:2:3275
+407:0:4177
+408:2:3900
+409:2:3901
+410:2:3905
+411:2:3909
+412:2:3910
+413:2:3914
+414:2:3922
+415:2:3923
+416:2:3927
+417:2:3931
+418:2:3932
+419:2:3927
+420:2:3931
+421:2:3932
+422:2:3936
+423:2:3943
+424:2:3950
+425:2:3951
+426:2:3958
+427:2:3963
+428:2:3970
+429:2:3971
+430:2:3970
+431:2:3971
+432:2:3978
+433:2:3982
+434:0:4177
+435:2:3987
+436:0:4177
+437:2:3988
+438:0:4177
+439:2:3989
+440:0:4177
+441:2:3990
+442:0:4177
+443:1:26
+444:0:4177
+445:2:3991
+446:0:4177
+447:1:30
+448:1:31
+449:1:35
+450:1:39
+451:1:40
+452:1:44
+453:1:52
+454:1:53
+455:1:57
+456:1:61
+457:1:62
+458:1:57
+459:1:61
+460:1:62
+461:1:66
+462:1:73
+463:1:80
+464:1:81
+465:1:88
+466:1:93
+467:1:100
+468:1:101
+469:1:100
+470:1:101
+471:1:108
+472:1:112
+473:0:4177
+474:2:3990
+475:0:4177
+476:1:117
+477:0:4177
+478:2:3991
+479:0:4177
+480:2:3992
+481:0:4177
+482:2:3997
+483:0:4177
+484:2:3998
+485:0:4177
+486:2:4006
+487:2:4007
+488:2:4011
+489:2:4015
+490:2:4016
+491:2:4020
+492:2:4028
+493:2:4029
+494:2:4033
+495:2:4037
+496:2:4038
+497:2:4033
+498:2:4037
+499:2:4038
+500:2:4042
+501:2:4049
+502:2:4056
+503:2:4057
+504:2:4064
+505:2:4069
+506:2:4076
+507:2:4077
+508:2:4076
+509:2:4077
+510:2:4084
+511:2:4088
+512:0:4177
+513:2:3277
+514:2:3287
+515:0:4177
+516:2:2522
+517:0:4177
+518:2:3278
+519:2:3279
+520:0:4177
+521:2:2522
+522:0:4177
+523:2:3283
+524:0:4177
+525:2:3291
+526:0:4177
+527:2:2518
+528:0:4177
+529:2:2520
+530:0:4177
+531:2:2521
+532:0:4177
+533:2:2522
+534:0:4177
+535:2:2685
+536:2:2686
+537:2:2687
+538:0:4177
+539:2:2522
+540:0:4177
+541:2:2523
+542:2:2524
+543:2:2528
+544:2:2529
+545:2:2537
+546:2:2538
+547:2:2542
+548:2:2543
+549:2:2551
+550:2:2556
+551:2:2557
+552:2:2569
+553:2:2570
+554:2:2571
+555:2:2569
+556:2:2570
+557:2:2574
+558:2:2575
+559:2:2583
+560:2:2588
+561:2:2595
+562:2:2596
+563:2:2603
+564:2:2608
+565:2:2615
+566:2:2616
+567:2:2615
+568:2:2616
+569:2:2623
+570:2:2633
+571:0:4177
+572:2:2522
+573:0:4177
+574:2:2692
+575:0:4177
+576:2:3306
+577:2:3307
+578:2:3311
+579:2:3315
+580:2:3316
+581:2:3320
+582:2:3328
+583:2:3329
+584:2:3333
+585:2:3334
+586:2:3333
+587:2:3337
+588:2:3338
+589:2:3342
+590:2:3349
+591:2:3356
+592:2:3357
+593:2:3364
+594:2:3369
+595:2:3376
+596:2:3377
+597:2:3376
+598:2:3377
+599:2:3384
+600:2:3388
+601:0:4177
+602:2:3393
+603:0:4177
+604:2:3394
+605:0:4177
+606:2:3395
+607:0:4177
+608:2:3396
+609:0:4177
+610:1:26
+611:0:4177
+612:2:3397
+613:0:4177
+614:1:30
+615:1:31
+616:1:35
+617:1:39
+618:1:40
+619:1:44
+620:1:52
+621:1:53
+622:1:57
+623:1:61
+624:1:62
+625:1:57
+626:1:61
+627:1:62
+628:1:66
+629:1:73
+630:1:80
+631:1:81
+632:1:88
+633:1:93
+634:1:100
+635:1:101
+636:1:100
+637:1:101
+638:1:108
+639:1:112
+640:0:4177
+641:2:3396
+642:0:4177
+643:1:117
+644:0:4177
+645:2:3397
+646:0:4177
+647:2:3398
+648:0:4177
+649:2:3403
+650:0:4177
+651:2:3404
+652:0:4177
+653:2:3412
+654:2:3413
+655:2:3417
+656:2:3421
+657:2:3422
+658:2:3426
+659:2:3434
+660:2:3435
+661:2:3439
+662:2:3443
+663:2:3444
+664:2:3439
+665:2:3443
+666:2:3444
+667:2:3448
+668:2:3455
+669:2:3462
+670:2:3463
+671:2:3470
+672:2:3475
+673:2:3482
+674:2:3483
+675:2:3482
+676:2:3483
+677:2:3490
+678:2:3494
+679:0:4177
+680:2:2694
+681:2:3287
+682:0:4177
+683:2:2522
+684:0:4177
+685:2:2695
+686:0:4177
+687:2:2522
+688:0:4177
+689:2:2698
+690:2:2699
+691:2:2703
+692:2:2704
+693:2:2712
+694:2:2713
+695:2:2717
+696:2:2718
+697:2:2726
+698:2:2731
+699:2:2735
+700:2:2736
+701:2:2744
+702:2:2745
+703:2:2749
+704:2:2750
+705:2:2744
+706:2:2745
+707:2:2749
+708:2:2750
+709:2:2758
+710:2:2763
+711:2:2770
+712:2:2771
+713:2:2778
+714:2:2783
+715:2:2790
+716:2:2791
+717:2:2790
+718:2:2791
+719:2:2798
+720:2:2807
+721:0:4177
+722:2:2522
+723:0:4177
+724:2:2811
+725:2:2812
+726:2:2813
+727:2:2825
+728:2:2826
+729:2:2830
+730:2:2831
+731:2:2839
+732:2:2844
+733:2:2848
+734:2:2849
+735:2:2857
+736:2:2858
+737:2:2862
+738:2:2863
+739:2:2857
+740:2:2858
+741:2:2862
+742:2:2863
+743:2:2871
+744:2:2876
+745:2:2883
+746:2:2884
+747:2:2891
+748:2:2896
+749:2:2903
+750:2:2904
+751:2:2903
+752:2:2904
+753:2:2911
+754:2:2924
+755:2:2925
+756:0:4177
+757:2:2522
+758:0:4177
+759:2:2932
+760:2:2933
+761:2:2937
+762:2:2938
+763:2:2946
+764:2:2947
+765:2:2951
+766:2:2952
+767:2:2960
+768:2:2965
+769:2:2969
+770:2:2970
+771:2:2978
+772:2:2979
+773:2:2983
+774:2:2984
+775:2:2978
+776:2:2979
+777:2:2983
+778:2:2984
+779:2:2992
+780:2:2997
+781:2:3004
+782:2:3005
+783:2:3012
+784:2:3017
+785:2:3024
+786:2:3025
+787:2:3024
+788:2:3025
+789:2:3032
+790:0:4177
+791:2:2522
+792:0:4177
+793:2:3043
+794:2:3044
+795:2:3048
+796:2:3049
+797:2:3057
+798:2:3058
+799:2:3062
+800:2:3063
+801:2:3071
+802:2:3076
+803:2:3080
+804:2:3081
+805:2:3089
+806:2:3090
+807:2:3094
+808:2:3095
+809:2:3089
+810:2:3090
+811:2:3094
+812:2:3095
+813:2:3103
+814:2:3108
+815:2:3115
+816:2:3116
+817:2:3123
+818:2:3128
+819:2:3135
+820:2:3136
+821:2:3135
+822:2:3136
+823:2:3143
+824:2:3152
+825:0:4177
+826:2:2522
+827:0:4177
+828:2:3156
+829:2:3157
+830:2:3158
+831:2:3170
+832:2:3171
+833:2:3175
+834:2:3176
+835:2:3184
+836:2:3189
+837:2:3193
+838:2:3194
+839:2:3202
+840:2:3203
+841:2:3207
+842:2:3208
+843:2:3202
+844:2:3203
+845:2:3207
+846:2:3208
+847:2:3216
+848:2:3221
+849:2:3228
+850:2:3229
+851:2:3236
+852:2:3241
+853:2:3248
+854:2:3249
+855:2:3248
+856:2:3249
+857:2:3256
+858:2:3268
+859:2:3269
+860:0:4177
+861:2:2522
+862:0:4177
+863:2:3275
+864:0:4177
+865:2:3900
+866:2:3901
+867:2:3905
+868:2:3909
+869:2:3910
+870:2:3914
+871:2:3922
+872:2:3923
+873:2:3927
+874:2:3931
+875:2:3932
+876:2:3927
+877:2:3931
+878:2:3932
+879:2:3936
+880:2:3943
+881:2:3950
+882:2:3951
+883:2:3958
+884:2:3963
+885:2:3970
+886:2:3971
+887:2:3970
+888:2:3971
+889:2:3978
+890:2:3982
+891:0:4177
+892:2:3987
+893:0:4177
+894:2:3988
+895:0:4177
+896:2:3989
+897:0:4177
+898:2:3990
+899:0:4177
+900:1:26
+901:0:4177
+902:2:3991
+903:0:4177
+904:1:30
+905:1:31
+906:1:35
+907:1:39
+908:1:40
+909:1:44
+910:1:52
+911:1:53
+912:1:57
+913:1:61
+914:1:62
+915:1:57
+916:1:61
+917:1:62
+918:1:66
+919:1:73
+920:1:80
+921:1:81
+922:1:88
+923:1:93
+924:1:100
+925:1:101
+926:1:100
+927:1:101
+928:1:108
+929:1:112
+930:0:4177
+931:2:3990
+932:0:4177
+933:1:117
+934:0:4177
+935:2:3991
+936:0:4177
+937:2:3992
+938:0:4177
+939:2:3997
+940:0:4177
+941:2:3998
+942:0:4177
+943:2:4006
+944:2:4007
+945:2:4011
+946:2:4015
+947:2:4016
+948:2:4020
+949:2:4028
+950:2:4029
+951:2:4033
+952:2:4037
+953:2:4038
+954:2:4033
+955:2:4037
+956:2:4038
+957:2:4042
+958:2:4049
+959:2:4056
+960:2:4057
+961:2:4064
+962:2:4069
+963:2:4076
+964:2:4077
+965:2:4076
+966:2:4077
+967:2:4084
+968:2:4088
+969:0:4177
+970:2:3277
+971:2:3287
+972:0:4177
+973:2:2522
+974:0:4177
+975:2:3278
+976:2:3279
+977:0:4177
+978:2:2522
+979:0:4177
+980:2:3283
+981:0:4177
+982:2:3291
+983:0:4177
+984:2:2518
+985:0:4177
+986:2:2520
+987:0:4177
+988:2:2521
+989:0:4177
+990:2:2522
+991:0:4177
+992:2:2523
+993:2:2524
+994:2:2528
+995:2:2529
+996:2:2537
+997:2:2538
+998:2:2542
+999:2:2543
+1000:2:2551
+1001:2:2556
+1002:2:2560
+1003:2:2561
+1004:2:2569
+1005:2:2570
+1006:2:2574
+1007:2:2575
+1008:2:2569
+1009:2:2570
+1010:2:2571
+1011:2:2583
+1012:2:2588
+1013:2:2595
+1014:2:2596
+1015:2:2603
+1016:2:2608
+1017:2:2615
+1018:2:2616
+1019:2:2615
+1020:2:2616
+1021:2:2623
+1022:2:2633
+1023:0:4177
+1024:2:2522
+1025:0:4177
+1026:2:2685
+1027:2:2686
+1028:2:2687
+1029:0:4177
+1030:2:2522
+1031:0:4177
+1032:2:2692
+1033:0:4177
+1034:1:118
+1035:0:4177
+1036:1:120
+1037:0:4177
+1038:1:19
+1039:0:4177
+1040:1:126
+1041:1:127
+1042:1:131
+1043:1:132
+1044:1:140
+1045:1:141
+1046:1:145
+1047:1:146
+1048:1:154
+1049:1:159
+1050:1:163
+1051:1:164
+1052:1:172
+1053:1:173
+1054:1:177
+1055:1:178
+1056:1:172
+1057:1:173
+1058:1:177
+1059:1:178
+1060:1:186
+1061:1:191
+1062:1:198
+1063:1:199
+1064:1:206
+1065:1:211
+1066:1:218
+1067:1:219
+1068:1:218
+1069:1:219
+1070:1:226
+1071:0:4177
+1072:1:15
+1073:0:4177
+1074:1:16
+1075:0:4177
+1076:1:17
+1077:0:4177
+1078:1:118
+1079:0:4177
+1080:1:120
+1081:0:4177
+1082:1:19
+1083:0:4177
+1084:1:237
+1085:1:238
+1086:0:4177
+1087:1:15
+1088:0:4177
+1089:1:16
+1090:0:4177
+1091:1:17
+1092:0:4177
+1093:1:118
+1094:0:4177
+1095:1:120
+1096:0:4177
+1097:1:19
+1098:0:4177
+1099:1:244
+1100:1:245
+1101:1:249
+1102:1:250
+1103:1:258
+1104:1:259
+1105:1:263
+1106:1:264
+1107:1:272
+1108:1:277
+1109:1:281
+1110:1:282
+1111:1:290
+1112:1:291
+1113:1:295
+1114:1:296
+1115:1:290
+1116:1:291
+1117:1:295
+1118:1:296
+1119:1:304
+1120:1:309
+1121:1:316
+1122:1:317
+1123:1:324
+1124:1:329
+1125:1:336
+1126:1:337
+1127:1:336
+1128:1:337
+1129:1:344
+1130:0:4177
+1131:1:15
+1132:0:4177
+1133:1:16
+1134:0:4177
+1135:1:17
+1136:0:4177
+1137:1:118
+1138:0:4177
+1139:1:120
+1140:0:4177
+1141:1:19
+1142:0:4177
+1143:1:355
+1144:1:356
+1145:1:360
+1146:1:361
+1147:1:369
+1148:1:370
+1149:1:374
+1150:1:375
+1151:1:383
+1152:1:388
+1153:1:392
+1154:1:393
+1155:1:401
+1156:1:402
+1157:1:406
+1158:1:407
+1159:1:401
+1160:1:402
+1161:1:406
+1162:1:407
+1163:1:415
+1164:1:420
+1165:1:427
+1166:1:428
+1167:1:435
+1168:1:440
+1169:1:447
+1170:1:448
+1171:1:447
+1172:1:448
+1173:1:455
+1174:1:464
+1175:0:4177
+1176:1:15
+1177:0:4177
+1178:1:16
+1179:0:4177
+1180:1:17
+1181:0:4177
+1182:1:118
+1183:0:4177
+1184:1:120
+1185:0:4177
+1186:1:19
+1187:0:4177
+1188:1:584
+1189:1:585
+1190:1:589
+1191:1:590
+1192:1:598
+1193:1:599
+1194:1:600
+1195:1:612
+1196:1:617
+1197:1:621
+1198:1:622
+1199:1:630
+1200:1:631
+1201:1:635
+1202:1:636
+1203:1:630
+1204:1:631
+1205:1:635
+1206:1:636
+1207:1:644
+1208:1:649
+1209:1:656
+1210:1:657
+1211:1:664
+1212:1:669
+1213:1:676
+1214:1:677
+1215:1:676
+1216:1:677
+1217:1:684
+1218:0:4177
+1219:1:15
+1220:0:4177
+1221:1:16
+1222:0:4177
+1223:1:17
+1224:0:4177
+1225:1:118
+1226:0:4177
+1227:1:120
+1228:0:4177
+1229:1:19
+1230:0:4177
+1231:1:695
+1232:1:698
+1233:1:699
+1234:0:4177
+1235:1:15
+1236:0:4177
+1237:1:16
+1238:0:4177
+1239:1:17
+1240:0:4177
+1241:1:118
+1242:0:4177
+1243:1:120
+1244:0:4177
+1245:1:19
+1246:0:4177
+1247:1:702
+1248:1:703
+1249:1:707
+1250:1:708
+1251:1:716
+1252:1:717
+1253:1:721
+1254:1:722
+1255:1:730
+1256:1:735
+1257:1:739
+1258:1:740
+1259:1:748
+1260:1:749
+1261:1:753
+1262:1:754
+1263:1:748
+1264:1:749
+1265:1:753
+1266:1:754
+1267:1:762
+1268:1:767
+1269:1:774
+1270:1:775
+1271:1:782
+1272:1:787
+1273:1:794
+1274:1:795
+1275:1:794
+1276:1:795
+1277:1:802
+1278:0:4177
+1279:1:15
+1280:0:4177
+1281:1:16
+1282:0:4177
+1283:1:17
+1284:0:4177
+1285:1:118
+1286:0:4177
+1287:1:120
+1288:0:4177
+1289:1:19
+1290:0:4177
+1291:1:926
+1292:1:927
+1293:1:931
+1294:1:932
+1295:1:940
+1296:1:941
+1297:1:945
+1298:1:946
+1299:1:954
+1300:1:959
+1301:1:963
+1302:1:964
+1303:1:972
+1304:1:973
+1305:1:977
+1306:1:978
+1307:1:972
+1308:1:973
+1309:1:977
+1310:1:978
+1311:1:986
+1312:1:991
+1313:1:998
+1314:1:999
+1315:1:1006
+1316:1:1011
+1317:1:1018
+1318:1:1019
+1319:1:1018
+1320:1:1019
+1321:1:1026
+1322:1:1035
+1323:1:1039
+1324:0:4177
+1325:1:15
+1326:0:4177
+1327:1:16
+1328:0:4177
+1329:1:17
+1330:0:4177
+1331:1:118
+1332:0:4177
+1333:1:120
+1334:0:4177
+1335:1:19
+1336:0:4177
+1337:1:1040
+1338:1:1041
+1339:1:1045
+1340:1:1046
+1341:1:1054
+1342:1:1055
+1343:1:1056
+1344:1:1068
+1345:1:1073
+1346:1:1077
+1347:1:1078
+1348:1:1086
+1349:1:1087
+1350:1:1091
+1351:1:1092
+1352:1:1086
+1353:1:1087
+1354:1:1091
+1355:1:1092
+1356:1:1100
+1357:1:1105
+1358:1:1112
+1359:1:1113
+1360:1:1120
+1361:1:1125
+1362:1:1132
+1363:1:1133
+1364:1:1132
+1365:1:1133
+1366:1:1140
+1367:0:4177
+1368:1:15
+1369:0:4177
+1370:1:16
+1371:0:4177
+1372:1:17
+1373:0:4177
+1374:1:118
+1375:0:4177
+1376:1:120
+1377:0:4177
+1378:1:19
+1379:0:4177
+1380:1:1151
+1381:0:4177
+1382:1:2417
+1383:1:2424
+1384:1:2425
+1385:1:2432
+1386:1:2437
+1387:1:2444
+1388:1:2445
+1389:1:2444
+1390:1:2445
+1391:1:2452
+1392:1:2456
+1393:0:4177
+1394:2:3306
+1395:2:3307
+1396:2:3311
+1397:2:3315
+1398:2:3316
+1399:2:3320
+1400:2:3325
+1401:2:3333
+1402:2:3337
+1403:2:3338
+1404:2:3333
+1405:2:3334
+1406:2:3342
+1407:2:3349
+1408:2:3356
+1409:2:3357
+1410:2:3364
+1411:2:3369
+1412:2:3376
+1413:2:3377
+1414:2:3376
+1415:2:3377
+1416:2:3384
+1417:2:3388
+1418:0:4177
+1419:2:3393
+1420:0:4177
+1421:2:3394
+1422:0:4177
+1423:2:3395
+1424:0:4177
+1425:2:3396
+1426:0:4177
+1427:1:1153
+1428:1:1154
+1429:0:4175
+1430:2:3397
+1431:0:4181
+1432:1:2165