Verification run #1, ipi and no-ipi results

[urcu.git] / formal-model / results / urcu-controldataflow-no-ipi / result-ipi-urcu_free / urcu_free_no_mb.spin.input.trail

diff --git a/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_mb.spin.input.trail b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_mb.spin.input.trail
new file mode 100644 (file)
index 0000000..4be75cd
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-no-ipi/result-ipi-urcu_free/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,1387 @@
+-2:3:-2
+-4:-4:-4
+1:0:4650
+2:3:4570
+3:3:4573
+4:3:4573
+5:3:4576
+6:3:4584
+7:3:4584
+8:3:4587
+9:3:4593
+10:3:4597
+11:3:4597
+12:3:4600
+13:3:4610
+14:3:4618
+15:3:4618
+16:3:4621
+17:3:4627
+18:3:4631
+19:3:4631
+20:3:4634
+21:3:4640
+22:3:4644
+23:3:4645
+24:0:4650
+25:3:4647
+26:0:4650
+27:2:2876
+28:0:4650
+29:2:2882
+30:0:4650
+31:2:2883
+32:0:4650
+33:2:2885
+34:0:4650
+35:2:2886
+36:0:4650
+37:2:2887
+38:0:4650
+39:2:2888
+40:0:4650
+41:2:2889
+42:2:2890
+43:2:2894
+44:2:2895
+45:2:2903
+46:2:2904
+47:2:2908
+48:2:2909
+49:2:2917
+50:2:2922
+51:2:2926
+52:2:2927
+53:2:2935
+54:2:2936
+55:2:2940
+56:2:2941
+57:2:2935
+58:2:2936
+59:2:2940
+60:2:2941
+61:2:2949
+62:2:2954
+63:2:2955
+64:2:2966
+65:2:2967
+66:2:2968
+67:2:2979
+68:2:2984
+69:2:2985
+70:2:2996
+71:2:2997
+72:2:2998
+73:2:2996
+74:2:2997
+75:2:2998
+76:2:3009
+77:2:3017
+78:0:4650
+79:2:2888
+80:0:4650
+81:2:3021
+82:2:3025
+83:2:3026
+84:2:3030
+85:2:3034
+86:2:3035
+87:2:3039
+88:2:3047
+89:2:3048
+90:2:3052
+91:2:3056
+92:2:3057
+93:2:3052
+94:2:3053
+95:2:3061
+96:0:4650
+97:2:2888
+98:0:4650
+99:2:3069
+100:2:3070
+101:2:3071
+102:0:4650
+103:2:2888
+104:0:4650
+105:2:3079
+106:0:4650
+107:2:2888
+108:0:4650
+109:2:3082
+110:2:3083
+111:2:3087
+112:2:3088
+113:2:3096
+114:2:3097
+115:2:3101
+116:2:3102
+117:2:3110
+118:2:3115
+119:2:3116
+120:2:3128
+121:2:3129
+122:2:3133
+123:2:3134
+124:2:3128
+125:2:3129
+126:2:3133
+127:2:3134
+128:2:3142
+129:2:3147
+130:2:3148
+131:2:3159
+132:2:3160
+133:2:3161
+134:2:3172
+135:2:3177
+136:2:3178
+137:2:3189
+138:2:3190
+139:2:3191
+140:2:3189
+141:2:3190
+142:2:3191
+143:2:3202
+144:2:3209
+145:0:4650
+146:2:2888
+147:0:4650
+148:2:3213
+149:2:3214
+150:2:3215
+151:2:3227
+152:2:3228
+153:2:3232
+154:2:3233
+155:2:3241
+156:2:3246
+157:2:3250
+158:2:3251
+159:2:3259
+160:2:3260
+161:2:3264
+162:2:3265
+163:2:3259
+164:2:3260
+165:2:3264
+166:2:3265
+167:2:3273
+168:2:3278
+169:2:3279
+170:2:3290
+171:2:3291
+172:2:3292
+173:2:3303
+174:2:3308
+175:2:3309
+176:2:3320
+177:2:3321
+178:2:3322
+179:2:3320
+180:2:3321
+181:2:3322
+182:2:3333
+183:2:3344
+184:2:3345
+185:0:4650
+186:2:2888
+187:0:4650
+188:2:3351
+189:2:3352
+190:2:3356
+191:2:3357
+192:2:3365
+193:2:3366
+194:2:3370
+195:2:3371
+196:2:3379
+197:2:3384
+198:2:3388
+199:2:3389
+200:2:3397
+201:2:3398
+202:2:3402
+203:2:3403
+204:2:3397
+205:2:3398
+206:2:3402
+207:2:3403
+208:2:3411
+209:2:3416
+210:2:3417
+211:2:3428
+212:2:3429
+213:2:3430
+214:2:3441
+215:2:3446
+216:2:3447
+217:2:3458
+218:2:3459
+219:2:3460
+220:2:3458
+221:2:3459
+222:2:3460
+223:2:3471
+224:0:4650
+225:2:2888
+226:0:4650
+227:2:3480
+228:2:3481
+229:2:3485
+230:2:3486
+231:2:3494
+232:2:3495
+233:2:3499
+234:2:3500
+235:2:3508
+236:2:3513
+237:2:3517
+238:2:3518
+239:2:3526
+240:2:3527
+241:2:3531
+242:2:3532
+243:2:3526
+244:2:3527
+245:2:3531
+246:2:3532
+247:2:3540
+248:2:3545
+249:2:3546
+250:2:3557
+251:2:3558
+252:2:3559
+253:2:3570
+254:2:3575
+255:2:3576
+256:2:3587
+257:2:3588
+258:2:3589
+259:2:3587
+260:2:3588
+261:2:3589
+262:2:3600
+263:2:3607
+264:0:4650
+265:2:2888
+266:0:4650
+267:2:3611
+268:2:3612
+269:2:3613
+270:2:3625
+271:2:3626
+272:2:3630
+273:2:3631
+274:2:3639
+275:2:3644
+276:2:3648
+277:2:3649
+278:2:3657
+279:2:3658
+280:2:3662
+281:2:3663
+282:2:3657
+283:2:3658
+284:2:3662
+285:2:3663
+286:2:3671
+287:2:3676
+288:2:3677
+289:2:3688
+290:2:3689
+291:2:3690
+292:2:3701
+293:2:3706
+294:2:3707
+295:2:3718
+296:2:3719
+297:2:3720
+298:2:3718
+299:2:3719
+300:2:3720
+301:2:3731
+302:2:3741
+303:2:3742
+304:0:4650
+305:2:2888
+306:0:4650
+307:2:3751
+308:2:3752
+309:0:4650
+310:2:2888
+311:0:4650
+312:2:3756
+313:0:4650
+314:2:3764
+315:0:4650
+316:2:2883
+317:0:4650
+318:2:2885
+319:0:4650
+320:2:2886
+321:0:4650
+322:2:2887
+323:0:4650
+324:2:2888
+325:0:4650
+326:2:2889
+327:2:2890
+328:2:2894
+329:2:2895
+330:2:2903
+331:2:2904
+332:2:2908
+333:2:2909
+334:2:2917
+335:2:2922
+336:2:2926
+337:2:2927
+338:2:2935
+339:2:2936
+340:2:2937
+341:2:2935
+342:2:2936
+343:2:2940
+344:2:2941
+345:2:2949
+346:2:2954
+347:2:2955
+348:2:2966
+349:2:2967
+350:2:2968
+351:2:2979
+352:2:2984
+353:2:2985
+354:2:2996
+355:2:2997
+356:2:2998
+357:2:2996
+358:2:2997
+359:2:2998
+360:2:3009
+361:2:3017
+362:0:4650
+363:2:2888
+364:0:4650
+365:2:3021
+366:2:3025
+367:2:3026
+368:2:3030
+369:2:3034
+370:2:3035
+371:2:3039
+372:2:3047
+373:2:3048
+374:2:3052
+375:2:3053
+376:2:3052
+377:2:3056
+378:2:3057
+379:2:3061
+380:0:4650
+381:2:2888
+382:0:4650
+383:2:3069
+384:2:3070
+385:2:3071
+386:0:4650
+387:2:2888
+388:0:4650
+389:2:3079
+390:0:4650
+391:2:2888
+392:0:4650
+393:2:3082
+394:2:3083
+395:2:3087
+396:2:3088
+397:2:3096
+398:2:3097
+399:2:3101
+400:2:3102
+401:2:3110
+402:2:3115
+403:2:3116
+404:2:3128
+405:2:3129
+406:2:3133
+407:2:3134
+408:2:3128
+409:2:3129
+410:2:3133
+411:2:3134
+412:2:3142
+413:2:3147
+414:2:3148
+415:2:3159
+416:2:3160
+417:2:3161
+418:2:3172
+419:2:3177
+420:2:3178
+421:2:3189
+422:2:3190
+423:2:3191
+424:2:3189
+425:2:3190
+426:2:3191
+427:2:3202
+428:2:3209
+429:0:4650
+430:2:2888
+431:0:4650
+432:2:3213
+433:2:3214
+434:2:3215
+435:2:3227
+436:2:3228
+437:2:3232
+438:2:3233
+439:2:3241
+440:2:3246
+441:2:3250
+442:2:3251
+443:2:3259
+444:2:3260
+445:2:3264
+446:2:3265
+447:2:3259
+448:2:3260
+449:2:3264
+450:2:3265
+451:2:3273
+452:2:3278
+453:2:3279
+454:2:3290
+455:2:3291
+456:2:3292
+457:2:3303
+458:2:3308
+459:2:3309
+460:2:3320
+461:2:3321
+462:2:3322
+463:2:3320
+464:2:3321
+465:2:3322
+466:2:3333
+467:2:3344
+468:2:3345
+469:0:4650
+470:2:2888
+471:0:4650
+472:2:3351
+473:2:3352
+474:2:3356
+475:2:3357
+476:2:3365
+477:2:3366
+478:2:3370
+479:2:3371
+480:2:3379
+481:2:3384
+482:2:3388
+483:2:3389
+484:2:3397
+485:2:3398
+486:2:3402
+487:2:3403
+488:2:3397
+489:2:3398
+490:2:3402
+491:2:3403
+492:2:3411
+493:2:3416
+494:2:3417
+495:2:3428
+496:2:3429
+497:2:3430
+498:2:3441
+499:2:3446
+500:2:3447
+501:2:3458
+502:2:3459
+503:2:3460
+504:2:3458
+505:2:3459
+506:2:3460
+507:2:3471
+508:0:4650
+509:2:2888
+510:0:4650
+511:2:3480
+512:2:3481
+513:2:3485
+514:2:3486
+515:2:3494
+516:2:3495
+517:2:3499
+518:2:3500
+519:2:3508
+520:2:3513
+521:2:3517
+522:2:3518
+523:2:3526
+524:2:3527
+525:2:3531
+526:2:3532
+527:2:3526
+528:2:3527
+529:2:3531
+530:2:3532
+531:2:3540
+532:2:3545
+533:2:3546
+534:2:3557
+535:2:3558
+536:2:3559
+537:2:3570
+538:2:3575
+539:2:3576
+540:2:3587
+541:2:3588
+542:2:3589
+543:2:3587
+544:2:3588
+545:2:3589
+546:2:3600
+547:2:3607
+548:0:4650
+549:2:2888
+550:0:4650
+551:2:3611
+552:2:3612
+553:2:3613
+554:2:3625
+555:2:3626
+556:2:3630
+557:2:3631
+558:2:3639
+559:2:3644
+560:2:3648
+561:2:3649
+562:2:3657
+563:2:3658
+564:2:3662
+565:2:3663
+566:2:3657
+567:2:3658
+568:2:3662
+569:2:3663
+570:2:3671
+571:2:3676
+572:2:3677
+573:2:3688
+574:2:3689
+575:2:3690
+576:2:3701
+577:2:3706
+578:2:3707
+579:2:3718
+580:2:3719
+581:2:3720
+582:2:3718
+583:2:3719
+584:2:3720
+585:2:3731
+586:2:3741
+587:2:3742
+588:0:4650
+589:2:2888
+590:0:4650
+591:2:3751
+592:2:3752
+593:0:4650
+594:2:2888
+595:0:4650
+596:2:3756
+597:0:4650
+598:2:3764
+599:0:4650
+600:2:2883
+601:0:4650
+602:2:2885
+603:0:4650
+604:2:2886
+605:0:4650
+606:2:2887
+607:0:4650
+608:2:2888
+609:0:4650
+610:2:2889
+611:2:2890
+612:2:2894
+613:2:2895
+614:2:2903
+615:2:2904
+616:2:2908
+617:2:2909
+618:2:2917
+619:2:2922
+620:2:2926
+621:2:2927
+622:2:2935
+623:2:2936
+624:2:2940
+625:2:2941
+626:2:2935
+627:2:2936
+628:2:2937
+629:2:2949
+630:2:2954
+631:2:2955
+632:2:2966
+633:2:2967
+634:2:2968
+635:2:2979
+636:2:2984
+637:2:2985
+638:2:2996
+639:2:2997
+640:2:2998
+641:2:2996
+642:2:2997
+643:2:2998
+644:2:3009
+645:2:3017
+646:0:4650
+647:2:2888
+648:0:4650
+649:2:3021
+650:2:3025
+651:2:3026
+652:2:3030
+653:2:3034
+654:2:3035
+655:2:3039
+656:2:3047
+657:2:3048
+658:2:3052
+659:2:3056
+660:2:3057
+661:2:3052
+662:2:3053
+663:2:3061
+664:0:4650
+665:2:2888
+666:0:4650
+667:2:3069
+668:2:3070
+669:2:3071
+670:0:4650
+671:2:2888
+672:0:4650
+673:2:3079
+674:0:4650
+675:2:2888
+676:0:4650
+677:2:3082
+678:2:3083
+679:2:3087
+680:2:3088
+681:2:3096
+682:2:3097
+683:2:3101
+684:2:3102
+685:2:3110
+686:2:3115
+687:2:3116
+688:2:3128
+689:2:3129
+690:2:3133
+691:2:3134
+692:2:3128
+693:2:3129
+694:2:3133
+695:2:3134
+696:2:3142
+697:2:3147
+698:2:3148
+699:2:3159
+700:2:3160
+701:2:3161
+702:2:3172
+703:2:3177
+704:2:3178
+705:2:3189
+706:2:3190
+707:2:3191
+708:2:3189
+709:2:3190
+710:2:3191
+711:2:3202
+712:2:3209
+713:0:4650
+714:2:2888
+715:0:4650
+716:2:3213
+717:2:3214
+718:2:3215
+719:2:3227
+720:2:3228
+721:2:3232
+722:2:3233
+723:2:3241
+724:2:3246
+725:2:3250
+726:2:3251
+727:2:3259
+728:2:3260
+729:2:3264
+730:2:3265
+731:2:3259
+732:2:3260
+733:2:3264
+734:2:3265
+735:2:3273
+736:2:3278
+737:2:3279
+738:2:3290
+739:2:3291
+740:2:3292
+741:2:3303
+742:2:3308
+743:2:3309
+744:2:3320
+745:2:3321
+746:2:3322
+747:2:3320
+748:2:3321
+749:2:3322
+750:2:3333
+751:2:3344
+752:2:3345
+753:0:4650
+754:2:2888
+755:0:4650
+756:2:3351
+757:2:3352
+758:2:3356
+759:2:3357
+760:2:3365
+761:2:3366
+762:2:3370
+763:2:3371
+764:2:3379
+765:2:3384
+766:2:3388
+767:2:3389
+768:2:3397
+769:2:3398
+770:2:3402
+771:2:3403
+772:2:3397
+773:2:3398
+774:2:3402
+775:2:3403
+776:2:3411
+777:2:3416
+778:2:3417
+779:2:3428
+780:2:3429
+781:2:3430
+782:2:3441
+783:2:3446
+784:2:3447
+785:2:3458
+786:2:3459
+787:2:3460
+788:2:3458
+789:2:3459
+790:2:3460
+791:2:3471
+792:0:4650
+793:2:2888
+794:0:4650
+795:2:3611
+796:2:3612
+797:2:3616
+798:2:3617
+799:2:3625
+800:2:3626
+801:2:3630
+802:2:3631
+803:2:3639
+804:2:3644
+805:2:3648
+806:2:3649
+807:2:3657
+808:2:3658
+809:2:3662
+810:2:3663
+811:2:3657
+812:2:3658
+813:2:3662
+814:2:3663
+815:2:3671
+816:2:3676
+817:2:3677
+818:2:3688
+819:2:3689
+820:2:3690
+821:2:3701
+822:2:3706
+823:2:3707
+824:2:3718
+825:2:3719
+826:2:3720
+827:2:3718
+828:2:3719
+829:2:3720
+830:2:3731
+831:2:3741
+832:2:3742
+833:0:4650
+834:2:2888
+835:0:4650
+836:2:3751
+837:2:3752
+838:0:4650
+839:2:2888
+840:0:4650
+841:2:3480
+842:2:3481
+843:2:3485
+844:2:3486
+845:2:3494
+846:2:3495
+847:2:3499
+848:2:3500
+849:2:3508
+850:2:3513
+851:2:3517
+852:2:3518
+853:2:3526
+854:2:3527
+855:2:3528
+856:2:3526
+857:2:3527
+858:2:3531
+859:2:3532
+860:2:3540
+861:2:3545
+862:2:3546
+863:2:3557
+864:2:3558
+865:2:3559
+866:2:3570
+867:2:3575
+868:2:3576
+869:2:3587
+870:2:3588
+871:2:3589
+872:2:3587
+873:2:3588
+874:2:3589
+875:2:3600
+876:2:3607
+877:0:4650
+878:2:2888
+879:0:4650
+880:2:3756
+881:0:4650
+882:2:3764
+883:0:4650
+884:2:3765
+885:0:4650
+886:2:3770
+887:0:4650
+888:1:2
+889:0:4650
+890:2:3771
+891:0:4650
+892:1:8
+893:0:4650
+894:2:3770
+895:0:4650
+896:1:9
+897:0:4650
+898:2:3771
+899:0:4650
+900:1:10
+901:0:4650
+902:2:3770
+903:0:4650
+904:1:11
+905:0:4650
+906:2:3771
+907:0:4650
+908:1:12
+909:0:4650
+910:2:3770
+911:0:4650
+912:1:13
+913:0:4650
+914:2:3771
+915:0:4650
+916:1:14
+917:0:4650
+918:2:3770
+919:0:4650
+920:1:15
+921:0:4650
+922:2:3771
+923:0:4650
+924:1:16
+925:0:4650
+926:2:3770
+927:0:4650
+928:1:17
+929:0:4650
+930:2:3771
+931:0:4650
+932:1:18
+933:0:4650
+934:2:3770
+935:0:4650
+936:1:19
+937:0:4650
+938:2:3771
+939:0:4650
+940:1:20
+941:0:4650
+942:2:3770
+943:0:4650
+944:1:21
+945:0:4650
+946:2:3771
+947:0:4650
+948:1:124
+949:0:4650
+950:2:3770
+951:0:4650
+952:1:23
+953:0:4650
+954:2:3771
+955:0:4650
+956:1:131
+957:1:132
+958:1:136
+959:1:137
+960:1:145
+961:1:146
+962:1:150
+963:1:151
+964:1:159
+965:1:164
+966:1:168
+967:1:169
+968:1:177
+969:1:178
+970:1:182
+971:1:183
+972:1:177
+973:1:178
+974:1:182
+975:1:183
+976:1:191
+977:1:196
+978:1:197
+979:1:208
+980:1:209
+981:1:210
+982:1:221
+983:1:233
+984:1:234
+985:1:238
+986:1:239
+987:1:240
+988:1:238
+989:1:239
+990:1:240
+991:1:251
+992:0:4650
+993:2:3770
+994:0:4650
+995:1:19
+996:0:4650
+997:2:3771
+998:0:4650
+999:1:20
+1000:0:4650
+1001:2:3770
+1002:0:4650
+1003:1:21
+1004:0:4650
+1005:2:3771
+1006:0:4650
+1007:1:124
+1008:0:4650
+1009:2:3770
+1010:0:4650
+1011:1:23
+1012:0:4650
+1013:2:3771
+1014:0:4650
+1015:1:260
+1016:1:261
+1017:0:4650
+1018:2:3770
+1019:0:4650
+1020:1:19
+1021:0:4650
+1022:2:3771
+1023:0:4650
+1024:1:20
+1025:0:4650
+1026:2:3770
+1027:0:4650
+1028:1:21
+1029:0:4650
+1030:2:3771
+1031:0:4650
+1032:1:124
+1033:0:4650
+1034:2:3770
+1035:0:4650
+1036:1:23
+1037:0:4650
+1038:2:3771
+1039:0:4650
+1040:1:267
+1041:1:268
+1042:1:272
+1043:1:273
+1044:1:281
+1045:1:282
+1046:1:286
+1047:1:287
+1048:1:295
+1049:1:300
+1050:1:304
+1051:1:305
+1052:1:313
+1053:1:314
+1054:1:318
+1055:1:319
+1056:1:313
+1057:1:314
+1058:1:318
+1059:1:319
+1060:1:327
+1061:1:332
+1062:1:333
+1063:1:344
+1064:1:345
+1065:1:346
+1066:1:357
+1067:1:369
+1068:1:370
+1069:1:374
+1070:1:375
+1071:1:376
+1072:1:374
+1073:1:375
+1074:1:376
+1075:1:387
+1076:0:4650
+1077:2:3770
+1078:0:4650
+1079:1:19
+1080:0:4650
+1081:2:3771
+1082:0:4650
+1083:1:20
+1084:0:4650
+1085:2:3770
+1086:0:4650
+1087:1:21
+1088:0:4650
+1089:2:3771
+1090:0:4650
+1091:1:124
+1092:0:4650
+1093:2:3770
+1094:0:4650
+1095:1:23
+1096:0:4650
+1097:2:3771
+1098:0:4650
+1099:1:396
+1100:1:397
+1101:1:401
+1102:1:402
+1103:1:410
+1104:1:411
+1105:1:415
+1106:1:416
+1107:1:424
+1108:1:429
+1109:1:433
+1110:1:434
+1111:1:442
+1112:1:443
+1113:1:447
+1114:1:448
+1115:1:442
+1116:1:443
+1117:1:447
+1118:1:448
+1119:1:456
+1120:1:461
+1121:1:462
+1122:1:473
+1123:1:474
+1124:1:475
+1125:1:486
+1126:1:498
+1127:1:499
+1128:1:503
+1129:1:504
+1130:1:505
+1131:1:503
+1132:1:504
+1133:1:505
+1134:1:516
+1135:1:523
+1136:0:4650
+1137:2:3770
+1138:0:4650
+1139:1:19
+1140:0:4650
+1141:2:3771
+1142:0:4650
+1143:1:20
+1144:0:4650
+1145:2:3770
+1146:0:4650
+1147:1:21
+1148:0:4650
+1149:2:3771
+1150:0:4650
+1151:1:124
+1152:0:4650
+1153:2:3770
+1154:0:4650
+1155:1:23
+1156:0:4650
+1157:2:3771
+1158:0:4650
+1159:1:661
+1160:1:662
+1161:1:666
+1162:1:667
+1163:1:675
+1164:1:676
+1165:1:677
+1166:1:689
+1167:1:694
+1168:1:698
+1169:1:699
+1170:1:707
+1171:1:708
+1172:1:712
+1173:1:713
+1174:1:707
+1175:1:708
+1176:1:712
+1177:1:713
+1178:1:721
+1179:1:726
+1180:1:727
+1181:1:738
+1182:1:739
+1183:1:740
+1184:1:751
+1185:1:763
+1186:1:764
+1187:1:768
+1188:1:769
+1189:1:770
+1190:1:768
+1191:1:769
+1192:1:770
+1193:1:781
+1194:0:4650
+1195:2:3770
+1196:0:4650
+1197:1:19
+1198:0:4650
+1199:2:3771
+1200:0:4650
+1201:1:20
+1202:0:4650
+1203:2:3770
+1204:0:4650
+1205:1:21
+1206:0:4650
+1207:2:3771
+1208:0:4650
+1209:1:124
+1210:0:4650
+1211:2:3770
+1212:0:4650
+1213:1:23
+1214:0:4650
+1215:2:3771
+1216:0:4650
+1217:1:790
+1218:1:793
+1219:1:794
+1220:0:4650
+1221:2:3770
+1222:0:4650
+1223:1:19
+1224:0:4650
+1225:2:3771
+1226:0:4650
+1227:1:20
+1228:0:4650
+1229:2:3770
+1230:0:4650
+1231:1:21
+1232:0:4650
+1233:2:3771
+1234:0:4650
+1235:1:124
+1236:0:4650
+1237:2:3770
+1238:0:4650
+1239:1:23
+1240:0:4650
+1241:2:3771
+1242:0:4650
+1243:1:1057
+1244:1:1058
+1245:1:1062
+1246:1:1063
+1247:1:1071
+1248:1:1072
+1249:1:1076
+1250:1:1077
+1251:1:1085
+1252:1:1090
+1253:1:1094
+1254:1:1095
+1255:1:1103
+1256:1:1104
+1257:1:1108
+1258:1:1109
+1259:1:1103
+1260:1:1104
+1261:1:1108
+1262:1:1109
+1263:1:1117
+1264:1:1122
+1265:1:1123
+1266:1:1134
+1267:1:1135
+1268:1:1136
+1269:1:1147
+1270:1:1159
+1271:1:1160
+1272:1:1164
+1273:1:1165
+1274:1:1166
+1275:1:1164
+1276:1:1165
+1277:1:1166
+1278:1:1177
+1279:1:1184
+1280:1:1188
+1281:0:4650
+1282:2:3770
+1283:0:4650
+1284:1:19
+1285:0:4650
+1286:2:3771
+1287:0:4650
+1288:1:20
+1289:0:4650
+1290:2:3770
+1291:0:4650
+1292:1:21
+1293:0:4650
+1294:2:3771
+1295:0:4650
+1296:1:124
+1297:0:4650
+1298:2:3770
+1299:0:4650
+1300:1:23
+1301:0:4650
+1302:2:3771
+1303:0:4650
+1304:1:1189
+1305:1:1190
+1306:1:1194
+1307:1:1195
+1308:1:1203
+1309:1:1204
+1310:1:1205
+1311:1:1217
+1312:1:1222
+1313:1:1226
+1314:1:1227
+1315:1:1235
+1316:1:1236
+1317:1:1240
+1318:1:1241
+1319:1:1235
+1320:1:1236
+1321:1:1240
+1322:1:1241
+1323:1:1249
+1324:1:1254
+1325:1:1255
+1326:1:1266
+1327:1:1267
+1328:1:1268
+1329:1:1279
+1330:1:1291
+1331:1:1292
+1332:1:1296
+1333:1:1297
+1334:1:1298
+1335:1:1296
+1336:1:1297
+1337:1:1298
+1338:1:1309
+1339:0:4650
+1340:2:3770
+1341:0:4650
+1342:1:19
+1343:0:4650
+1344:2:3771
+1345:0:4650
+1346:1:20
+1347:0:4650
+1348:2:3770
+1349:0:4650
+1350:1:21
+1351:0:4650
+1352:2:3771
+1353:0:4650
+1354:1:124
+1355:0:4650
+1356:2:3770
+1357:0:4650
+1358:1:23
+1359:0:4650
+1360:2:3771
+1361:0:4650
+1362:1:1318
+1363:0:4650
+1364:2:3770
+1365:0:4650
+1366:1:2782
+1367:1:2789
+1368:1:2790
+1369:1:2797
+1370:1:2802
+1371:1:2809
+1372:1:2810
+1373:1:2809
+1374:1:2810
+1375:1:2817
+1376:1:2821
+1377:0:4650
+1378:2:3771
+1379:0:4650
+1380:1:1320
+1381:1:1321
+1382:0:4648
+1383:2:3770
+1384:0:4654
+1385:1:1438