Verification run #1, ipi and no-ipi results

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

diff --git a/formal-model/results/urcu-controldataflow-ipi/urcu_progress_writer_error.spin.input.trail b/formal-model/results/urcu-controldataflow-ipi/urcu_progress_writer_error.spin.input.trail
new file mode 100644 (file)
index 0000000..64285b2
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-ipi/urcu_progress_writer_error.spin.input.trail
@@ -0,0 +1,1830 @@
+-2:3:-2
+-4:-4:-4
+1:0:4497
+2:3:4417
+3:3:4420
+4:3:4420
+5:3:4423
+6:3:4431
+7:3:4431
+8:3:4434
+9:3:4440
+10:3:4444
+11:3:4444
+12:3:4447
+13:3:4457
+14:3:4465
+15:3:4465
+16:3:4468
+17:3:4474
+18:3:4478
+19:3:4478
+20:3:4481
+21:3:4487
+22:3:4491
+23:3:4492
+24:0:4497
+25:3:4494
+26:0:4497
+27:2:2871
+28:0:4497
+29:2:2877
+30:0:4497
+31:2:2878
+32:0:4497
+33:2:2879
+34:0:4497
+35:2:2880
+36:0:4497
+37:2:2881
+38:0:4497
+39:2:2882
+40:2:2883
+41:2:2887
+42:2:2888
+43:2:2896
+44:2:2897
+45:2:2901
+46:2:2902
+47:2:2910
+48:2:2915
+49:2:2919
+50:2:2920
+51:2:2928
+52:2:2929
+53:2:2933
+54:2:2934
+55:2:2928
+56:2:2929
+57:2:2933
+58:2:2934
+59:2:2942
+60:2:2947
+61:2:2948
+62:2:2959
+63:2:2960
+64:2:2961
+65:2:2972
+66:2:2977
+67:2:2978
+68:2:2989
+69:2:2990
+70:2:2991
+71:2:2989
+72:2:2990
+73:2:2991
+74:2:3002
+75:2:3010
+76:0:4497
+77:2:2881
+78:0:4497
+79:2:3014
+80:2:3018
+81:2:3019
+82:2:3023
+83:2:3027
+84:2:3028
+85:2:3032
+86:2:3040
+87:2:3041
+88:2:3045
+89:2:3049
+90:2:3050
+91:2:3045
+92:2:3046
+93:2:3054
+94:0:4497
+95:2:2881
+96:0:4497
+97:2:3062
+98:2:3063
+99:2:3064
+100:0:4497
+101:2:2881
+102:0:4497
+103:2:3069
+104:0:4497
+105:2:4022
+106:2:4023
+107:2:4027
+108:2:4031
+109:2:4032
+110:2:4036
+111:2:4041
+112:2:4049
+113:2:4053
+114:2:4054
+115:2:4049
+116:2:4053
+117:2:4054
+118:2:4058
+119:2:4065
+120:2:4072
+121:2:4073
+122:2:4080
+123:2:4085
+124:2:4092
+125:2:4093
+126:2:4092
+127:2:4093
+128:2:4100
+129:2:4104
+130:0:4497
+131:2:4109
+132:0:4497
+133:2:4110
+134:0:4497
+135:2:4111
+136:0:4497
+137:2:4112
+138:0:4497
+139:1:2
+140:0:4497
+141:1:8
+142:0:4497
+143:1:9
+144:0:4497
+145:2:4113
+146:0:4497
+147:1:10
+148:0:4497
+149:2:4112
+150:0:4497
+151:1:11
+152:0:4497
+153:2:4113
+154:0:4497
+155:1:12
+156:0:4497
+157:2:4112
+158:0:4497
+159:1:13
+160:0:4497
+161:2:4113
+162:0:4497
+163:1:14
+164:0:4497
+165:1:15
+166:0:4497
+167:1:16
+168:0:4497
+169:2:4112
+170:0:4497
+171:1:17
+172:0:4497
+173:2:4113
+174:0:4497
+175:1:26
+176:0:4497
+177:2:4112
+178:0:4497
+179:1:30
+180:1:31
+181:1:35
+182:1:39
+183:1:40
+184:1:44
+185:1:52
+186:1:53
+187:1:57
+188:1:61
+189:1:62
+190:1:57
+191:1:61
+192:1:62
+193:1:66
+194:1:73
+195:1:80
+196:1:81
+197:1:88
+198:1:93
+199:1:100
+200:1:101
+201:1:100
+202:1:101
+203:1:108
+204:1:112
+205:0:4497
+206:2:4113
+207:0:4497
+208:1:117
+209:0:4497
+210:2:4114
+211:0:4497
+212:2:4119
+213:0:4497
+214:2:4120
+215:0:4497
+216:2:4128
+217:2:4129
+218:2:4133
+219:2:4137
+220:2:4138
+221:2:4142
+222:2:4150
+223:2:4151
+224:2:4155
+225:2:4159
+226:2:4160
+227:2:4155
+228:2:4159
+229:2:4160
+230:2:4164
+231:2:4171
+232:2:4178
+233:2:4179
+234:2:4186
+235:2:4191
+236:2:4198
+237:2:4199
+238:2:4198
+239:2:4199
+240:2:4206
+241:2:4210
+242:0:4497
+243:2:3071
+244:2:4003
+245:0:4497
+246:2:2881
+247:0:4497
+248:2:3072
+249:0:4497
+250:2:2881
+251:0:4497
+252:2:3075
+253:2:3076
+254:2:3080
+255:2:3081
+256:2:3089
+257:2:3090
+258:2:3094
+259:2:3095
+260:2:3103
+261:2:3108
+262:2:3112
+263:2:3113
+264:2:3121
+265:2:3122
+266:2:3126
+267:2:3127
+268:2:3121
+269:2:3122
+270:2:3126
+271:2:3127
+272:2:3135
+273:2:3140
+274:2:3141
+275:2:3152
+276:2:3153
+277:2:3154
+278:2:3165
+279:2:3170
+280:2:3171
+281:2:3182
+282:2:3183
+283:2:3184
+284:2:3182
+285:2:3183
+286:2:3184
+287:2:3195
+288:2:3202
+289:0:4497
+290:2:2881
+291:0:4497
+292:2:3206
+293:2:3207
+294:2:3208
+295:2:3220
+296:2:3221
+297:2:3225
+298:2:3226
+299:2:3234
+300:2:3239
+301:2:3243
+302:2:3244
+303:2:3252
+304:2:3253
+305:2:3257
+306:2:3258
+307:2:3252
+308:2:3253
+309:2:3257
+310:2:3258
+311:2:3266
+312:2:3271
+313:2:3272
+314:2:3283
+315:2:3284
+316:2:3285
+317:2:3296
+318:2:3301
+319:2:3302
+320:2:3313
+321:2:3314
+322:2:3315
+323:2:3313
+324:2:3314
+325:2:3315
+326:2:3326
+327:2:3337
+328:2:3338
+329:0:4497
+330:2:2881
+331:0:4497
+332:2:3469
+333:2:3470
+334:2:3474
+335:2:3475
+336:2:3483
+337:2:3484
+338:2:3488
+339:2:3489
+340:2:3497
+341:2:3502
+342:2:3506
+343:2:3507
+344:2:3515
+345:2:3516
+346:2:3520
+347:2:3521
+348:2:3515
+349:2:3516
+350:2:3520
+351:2:3521
+352:2:3529
+353:2:3534
+354:2:3535
+355:2:3546
+356:2:3547
+357:2:3548
+358:2:3559
+359:2:3564
+360:2:3565
+361:2:3576
+362:2:3577
+363:2:3578
+364:2:3576
+365:2:3577
+366:2:3578
+367:2:3589
+368:0:4497
+369:2:2881
+370:0:4497
+371:2:3598
+372:2:3599
+373:2:3603
+374:2:3604
+375:2:3612
+376:2:3613
+377:2:3617
+378:2:3618
+379:2:3626
+380:2:3631
+381:2:3635
+382:2:3636
+383:2:3644
+384:2:3645
+385:2:3649
+386:2:3650
+387:2:3644
+388:2:3645
+389:2:3649
+390:2:3650
+391:2:3658
+392:2:3663
+393:2:3664
+394:2:3675
+395:2:3676
+396:2:3677
+397:2:3688
+398:2:3693
+399:2:3694
+400:2:3705
+401:2:3706
+402:2:3707
+403:2:3705
+404:2:3706
+405:2:3707
+406:2:3718
+407:2:3725
+408:0:4497
+409:2:2881
+410:0:4497
+411:2:3729
+412:2:3730
+413:2:3731
+414:2:3743
+415:2:3744
+416:2:3748
+417:2:3749
+418:2:3757
+419:2:3762
+420:2:3766
+421:2:3767
+422:2:3775
+423:2:3776
+424:2:3780
+425:2:3781
+426:2:3775
+427:2:3776
+428:2:3780
+429:2:3781
+430:2:3789
+431:2:3794
+432:2:3795
+433:2:3806
+434:2:3807
+435:2:3808
+436:2:3819
+437:2:3824
+438:2:3825
+439:2:3836
+440:2:3837
+441:2:3838
+442:2:3836
+443:2:3837
+444:2:3838
+445:2:3849
+446:2:3859
+447:2:3860
+448:0:4497
+449:2:2881
+450:0:4497
+451:2:3991
+452:0:4497
+453:2:4220
+454:2:4221
+455:2:4225
+456:2:4229
+457:2:4230
+458:2:4234
+459:2:4242
+460:2:4243
+461:2:4247
+462:2:4251
+463:2:4252
+464:2:4247
+465:2:4251
+466:2:4252
+467:2:4256
+468:2:4263
+469:2:4270
+470:2:4271
+471:2:4278
+472:2:4283
+473:2:4290
+474:2:4291
+475:2:4290
+476:2:4291
+477:2:4298
+478:2:4302
+479:0:4497
+480:2:4307
+481:0:4497
+482:2:4308
+483:0:4497
+484:2:4309
+485:0:4497
+486:2:4310
+487:0:4497
+488:1:26
+489:0:4497
+490:2:4311
+491:0:4497
+492:1:30
+493:1:31
+494:1:35
+495:1:39
+496:1:40
+497:1:44
+498:1:52
+499:1:53
+500:1:57
+501:1:61
+502:1:62
+503:1:57
+504:1:61
+505:1:62
+506:1:66
+507:1:73
+508:1:80
+509:1:81
+510:1:88
+511:1:93
+512:1:100
+513:1:101
+514:1:100
+515:1:101
+516:1:108
+517:1:112
+518:0:4497
+519:2:4310
+520:0:4497
+521:1:117
+522:0:4497
+523:2:4311
+524:0:4497
+525:2:4312
+526:0:4497
+527:2:4317
+528:0:4497
+529:2:4318
+530:0:4497
+531:2:4326
+532:2:4327
+533:2:4331
+534:2:4335
+535:2:4336
+536:2:4340
+537:2:4348
+538:2:4349
+539:2:4353
+540:2:4357
+541:2:4358
+542:2:4353
+543:2:4357
+544:2:4358
+545:2:4362
+546:2:4369
+547:2:4376
+548:2:4377
+549:2:4384
+550:2:4389
+551:2:4396
+552:2:4397
+553:2:4396
+554:2:4397
+555:2:4404
+556:2:4408
+557:0:4497
+558:2:3993
+559:2:4003
+560:0:4497
+561:2:2881
+562:0:4497
+563:2:3994
+564:2:3995
+565:0:4497
+566:2:2881
+567:0:4497
+568:2:3999
+569:0:4497
+570:2:4007
+571:0:4497
+572:2:2878
+573:0:4497
+574:2:2879
+575:0:4497
+576:2:2880
+577:0:4497
+578:2:2881
+579:0:4497
+580:2:2882
+581:2:2883
+582:2:2887
+583:2:2888
+584:2:2896
+585:2:2897
+586:2:2901
+587:2:2902
+588:2:2910
+589:2:2915
+590:2:2919
+591:2:2920
+592:2:2928
+593:2:2929
+594:2:2930
+595:2:2928
+596:2:2929
+597:2:2933
+598:2:2934
+599:2:2942
+600:2:2947
+601:2:2948
+602:2:2959
+603:2:2960
+604:2:2961
+605:2:2972
+606:2:2977
+607:2:2978
+608:2:2989
+609:2:2990
+610:2:2991
+611:2:2989
+612:2:2990
+613:2:2991
+614:2:3002
+615:2:3010
+616:0:4497
+617:2:2881
+618:0:4497
+619:2:3014
+620:2:3018
+621:2:3019
+622:2:3023
+623:2:3027
+624:2:3028
+625:2:3032
+626:2:3040
+627:2:3041
+628:2:3045
+629:2:3046
+630:2:3045
+631:2:3049
+632:2:3050
+633:2:3054
+634:0:4497
+635:2:2881
+636:0:4497
+637:2:3062
+638:2:3063
+639:2:3064
+640:0:4497
+641:2:2881
+642:0:4497
+643:2:3069
+644:0:4497
+645:2:4022
+646:2:4023
+647:2:4027
+648:2:4031
+649:2:4032
+650:2:4036
+651:2:4041
+652:2:4049
+653:2:4053
+654:2:4054
+655:2:4049
+656:2:4053
+657:2:4054
+658:2:4058
+659:2:4065
+660:2:4072
+661:2:4073
+662:2:4080
+663:2:4085
+664:2:4092
+665:2:4093
+666:2:4092
+667:2:4093
+668:2:4100
+669:2:4104
+670:0:4497
+671:2:4109
+672:0:4497
+673:2:4110
+674:0:4497
+675:2:4111
+676:0:4497
+677:2:4112
+678:0:4497
+679:1:26
+680:0:4497
+681:2:4113
+682:0:4497
+683:1:30
+684:1:31
+685:1:35
+686:1:39
+687:1:40
+688:1:44
+689:1:52
+690:1:53
+691:1:57
+692:1:61
+693:1:62
+694:1:57
+695:1:61
+696:1:62
+697:1:66
+698:1:73
+699:1:80
+700:1:81
+701:1:88
+702:1:93
+703:1:100
+704:1:101
+705:1:100
+706:1:101
+707:1:108
+708:1:112
+709:0:4497
+710:2:4112
+711:0:4497
+712:1:117
+713:0:4497
+714:2:4113
+715:0:4497
+716:2:4114
+717:0:4497
+718:2:4119
+719:0:4497
+720:2:4120
+721:0:4497
+722:2:4128
+723:2:4129
+724:2:4133
+725:2:4137
+726:2:4138
+727:2:4142
+728:2:4150
+729:2:4151
+730:2:4155
+731:2:4159
+732:2:4160
+733:2:4155
+734:2:4159
+735:2:4160
+736:2:4164
+737:2:4171
+738:2:4178
+739:2:4179
+740:2:4186
+741:2:4191
+742:2:4198
+743:2:4199
+744:2:4198
+745:2:4199
+746:2:4206
+747:2:4210
+748:0:4497
+749:2:3071
+750:2:4003
+751:0:4497
+752:2:2881
+753:0:4497
+754:2:3072
+755:0:4497
+756:2:2881
+757:0:4497
+758:2:3075
+759:2:3076
+760:2:3080
+761:2:3081
+762:2:3089
+763:2:3090
+764:2:3094
+765:2:3095
+766:2:3103
+767:2:3108
+768:2:3112
+769:2:3113
+770:2:3121
+771:2:3122
+772:2:3126
+773:2:3127
+774:2:3121
+775:2:3122
+776:2:3126
+777:2:3127
+778:2:3135
+779:2:3140
+780:2:3141
+781:2:3152
+782:2:3153
+783:2:3154
+784:2:3165
+785:2:3170
+786:2:3171
+787:2:3182
+788:2:3183
+789:2:3184
+790:2:3182
+791:2:3183
+792:2:3184
+793:2:3195
+794:2:3202
+795:0:4497
+796:2:2881
+797:0:4497
+798:2:3206
+799:2:3207
+800:2:3208
+801:2:3220
+802:2:3221
+803:2:3225
+804:2:3226
+805:2:3234
+806:2:3239
+807:2:3243
+808:2:3244
+809:2:3252
+810:2:3253
+811:2:3257
+812:2:3258
+813:2:3252
+814:2:3253
+815:2:3257
+816:2:3258
+817:2:3266
+818:2:3271
+819:2:3272
+820:2:3283
+821:2:3284
+822:2:3285
+823:2:3296
+824:2:3301
+825:2:3302
+826:2:3313
+827:2:3314
+828:2:3315
+829:2:3313
+830:2:3314
+831:2:3315
+832:2:3326
+833:2:3337
+834:2:3338
+835:0:4497
+836:2:2881
+837:0:4497
+838:2:3469
+839:2:3470
+840:2:3474
+841:2:3475
+842:2:3483
+843:2:3484
+844:2:3488
+845:2:3489
+846:2:3497
+847:2:3502
+848:2:3506
+849:2:3507
+850:2:3515
+851:2:3516
+852:2:3520
+853:2:3521
+854:2:3515
+855:2:3516
+856:2:3520
+857:2:3521
+858:2:3529
+859:2:3534
+860:2:3535
+861:2:3546
+862:2:3547
+863:2:3548
+864:2:3559
+865:2:3564
+866:2:3565
+867:2:3576
+868:2:3577
+869:2:3578
+870:2:3576
+871:2:3577
+872:2:3578
+873:2:3589
+874:0:4497
+875:2:2881
+876:0:4497
+877:2:3598
+878:2:3599
+879:2:3603
+880:2:3604
+881:2:3612
+882:2:3613
+883:2:3617
+884:2:3618
+885:2:3626
+886:2:3631
+887:2:3635
+888:2:3636
+889:2:3644
+890:2:3645
+891:2:3649
+892:2:3650
+893:2:3644
+894:2:3645
+895:2:3649
+896:2:3650
+897:2:3658
+898:2:3663
+899:2:3664
+900:2:3675
+901:2:3676
+902:2:3677
+903:2:3688
+904:2:3693
+905:2:3694
+906:2:3705
+907:2:3706
+908:2:3707
+909:2:3705
+910:2:3706
+911:2:3707
+912:2:3718
+913:2:3725
+914:0:4497
+915:2:2881
+916:0:4497
+917:2:3729
+918:2:3730
+919:2:3731
+920:2:3743
+921:2:3744
+922:2:3748
+923:2:3749
+924:2:3757
+925:2:3762
+926:2:3766
+927:2:3767
+928:2:3775
+929:2:3776
+930:2:3780
+931:2:3781
+932:2:3775
+933:2:3776
+934:2:3780
+935:2:3781
+936:2:3789
+937:2:3794
+938:2:3795
+939:2:3806
+940:2:3807
+941:2:3808
+942:2:3819
+943:2:3824
+944:2:3825
+945:2:3836
+946:2:3837
+947:2:3838
+948:2:3836
+949:2:3837
+950:2:3838
+951:2:3849
+952:2:3859
+953:2:3860
+954:0:4497
+955:2:2881
+956:0:4497
+957:2:3991
+958:0:4497
+959:2:4220
+960:2:4221
+961:2:4225
+962:2:4229
+963:2:4230
+964:2:4234
+965:2:4242
+966:2:4243
+967:2:4247
+968:2:4251
+969:2:4252
+970:2:4247
+971:2:4251
+972:2:4252
+973:2:4256
+974:2:4263
+975:2:4270
+976:2:4271
+977:2:4278
+978:2:4283
+979:2:4290
+980:2:4291
+981:2:4290
+982:2:4291
+983:2:4298
+984:2:4302
+985:0:4497
+986:2:4307
+987:0:4497
+988:2:4308
+989:0:4497
+990:2:4309
+991:0:4497
+992:2:4310
+993:0:4497
+994:1:26
+995:0:4497
+996:2:4311
+997:0:4497
+998:1:30
+999:1:31
+1000:1:35
+1001:1:39
+1002:1:40
+1003:1:44
+1004:1:52
+1005:1:53
+1006:1:57
+1007:1:61
+1008:1:62
+1009:1:57
+1010:1:61
+1011:1:62
+1012:1:66
+1013:1:73
+1014:1:80
+1015:1:81
+1016:1:88
+1017:1:93
+1018:1:100
+1019:1:101
+1020:1:100
+1021:1:101
+1022:1:108
+1023:1:112
+1024:0:4497
+1025:2:4310
+1026:0:4497
+1027:1:117
+1028:0:4497
+1029:2:4311
+1030:0:4497
+1031:2:4312
+1032:0:4497
+1033:2:4317
+1034:0:4497
+1035:2:4318
+1036:0:4497
+1037:2:4326
+1038:2:4327
+1039:2:4331
+1040:2:4335
+1041:2:4336
+1042:2:4340
+1043:2:4348
+1044:2:4349
+1045:2:4353
+1046:2:4357
+1047:2:4358
+1048:2:4353
+1049:2:4357
+1050:2:4358
+1051:2:4362
+1052:2:4369
+1053:2:4376
+1054:2:4377
+1055:2:4384
+1056:2:4389
+1057:2:4396
+1058:2:4397
+1059:2:4396
+1060:2:4397
+1061:2:4404
+1062:2:4408
+1063:0:4497
+1064:2:3993
+1065:2:4003
+1066:0:4497
+1067:2:2881
+1068:0:4497
+1069:2:3994
+1070:2:3995
+1071:0:4497
+1072:2:2881
+1073:0:4497
+1074:2:3999
+1075:0:4497
+1076:2:4007
+1077:0:4497
+1078:2:2878
+1079:0:4497
+1080:2:2879
+1081:0:4497
+1082:2:2880
+1083:0:4497
+1084:2:2881
+1085:0:4497
+1086:2:2882
+1087:2:2883
+1088:2:2887
+1089:2:2888
+1090:2:2896
+1091:2:2897
+1092:2:2901
+1093:2:2902
+1094:2:2910
+1095:2:2915
+1096:2:2919
+1097:2:2920
+1098:2:2928
+1099:2:2929
+1100:2:2933
+1101:2:2934
+1102:2:2928
+1103:2:2929
+1104:2:2930
+1105:2:2942
+1106:2:2947
+1107:2:2948
+1108:2:2959
+1109:2:2960
+1110:2:2961
+1111:2:2972
+1112:2:2977
+1113:2:2978
+1114:2:2989
+1115:2:2990
+1116:2:2991
+1117:2:2989
+1118:2:2990
+1119:2:2991
+1120:2:3002
+1121:2:3010
+1122:0:4497
+1123:2:2881
+1124:0:4497
+1125:2:3014
+1126:2:3018
+1127:2:3019
+1128:2:3023
+1129:2:3027
+1130:2:3028
+1131:2:3032
+1132:2:3040
+1133:2:3041
+1134:2:3045
+1135:2:3049
+1136:2:3050
+1137:2:3045
+1138:2:3046
+1139:2:3054
+1140:0:4497
+1141:2:2881
+1142:0:4497
+1143:2:3062
+1144:2:3063
+1145:2:3064
+1146:0:4497
+1147:2:2881
+1148:0:4497
+1149:2:3069
+1150:0:4497
+1151:2:4022
+1152:2:4023
+1153:2:4027
+1154:2:4031
+1155:2:4032
+1156:2:4036
+1157:2:4041
+1158:2:4049
+1159:2:4053
+1160:2:4054
+1161:2:4049
+1162:2:4053
+1163:2:4054
+1164:2:4058
+1165:2:4065
+1166:2:4072
+1167:2:4073
+1168:2:4080
+1169:2:4085
+1170:2:4092
+1171:2:4093
+1172:2:4092
+1173:2:4093
+1174:2:4100
+1175:2:4104
+1176:0:4497
+1177:2:4109
+1178:0:4497
+1179:2:4110
+1180:0:4497
+1181:2:4111
+1182:0:4497
+1183:2:4112
+1184:0:4497
+1185:1:26
+1186:0:4497
+1187:2:4113
+1188:0:4497
+1189:1:30
+1190:1:31
+1191:1:35
+1192:1:39
+1193:1:40
+1194:1:44
+1195:1:52
+1196:1:53
+1197:1:57
+1198:1:61
+1199:1:62
+1200:1:57
+1201:1:61
+1202:1:62
+1203:1:66
+1204:1:73
+1205:1:80
+1206:1:81
+1207:1:88
+1208:1:93
+1209:1:100
+1210:1:101
+1211:1:100
+1212:1:101
+1213:1:108
+1214:1:112
+1215:0:4497
+1216:2:4112
+1217:0:4497
+1218:1:117
+1219:0:4497
+1220:2:4113
+1221:0:4497
+1222:2:4114
+1223:0:4497
+1224:2:4119
+1225:0:4497
+1226:2:4120
+1227:0:4497
+1228:2:4128
+1229:2:4129
+1230:2:4133
+1231:2:4137
+1232:2:4138
+1233:2:4142
+1234:2:4150
+1235:2:4151
+1236:2:4155
+1237:2:4159
+1238:2:4160
+1239:2:4155
+1240:2:4159
+1241:2:4160
+1242:2:4164
+1243:2:4171
+1244:2:4178
+1245:2:4179
+1246:2:4186
+1247:2:4191
+1248:2:4198
+1249:2:4199
+1250:2:4198
+1251:2:4199
+1252:2:4206
+1253:2:4210
+1254:0:4497
+1255:2:3071
+1256:2:4003
+1257:0:4497
+1258:2:2881
+1259:0:4497
+1260:2:3072
+1261:0:4497
+1262:2:2881
+1263:0:4497
+1264:2:3075
+1265:2:3076
+1266:2:3080
+1267:2:3081
+1268:2:3089
+1269:2:3090
+1270:2:3094
+1271:2:3095
+1272:2:3103
+1273:2:3108
+1274:2:3112
+1275:2:3113
+1276:2:3121
+1277:2:3122
+1278:2:3126
+1279:2:3127
+1280:2:3121
+1281:2:3122
+1282:2:3126
+1283:2:3127
+1284:2:3135
+1285:2:3140
+1286:2:3141
+1287:2:3152
+1288:2:3153
+1289:2:3154
+1290:2:3165
+1291:2:3170
+1292:2:3171
+1293:2:3182
+1294:2:3183
+1295:2:3184
+1296:2:3182
+1297:2:3183
+1298:2:3184
+1299:2:3195
+1300:2:3202
+1301:0:4497
+1302:2:2881
+1303:0:4497
+1304:2:3206
+1305:2:3207
+1306:2:3208
+1307:2:3220
+1308:2:3221
+1309:2:3225
+1310:2:3226
+1311:2:3234
+1312:2:3239
+1313:2:3243
+1314:2:3244
+1315:2:3252
+1316:2:3253
+1317:2:3257
+1318:2:3258
+1319:2:3252
+1320:2:3253
+1321:2:3257
+1322:2:3258
+1323:2:3266
+1324:2:3271
+1325:2:3272
+1326:2:3283
+1327:2:3284
+1328:2:3285
+1329:2:3296
+1330:2:3301
+1331:2:3302
+1332:2:3313
+1333:2:3314
+1334:2:3315
+1335:2:3313
+1336:2:3314
+1337:2:3315
+1338:2:3326
+1339:2:3337
+1340:2:3338
+1341:0:4497
+1342:2:2881
+1343:0:4497
+1344:2:3469
+1345:2:3470
+1346:2:3474
+1347:2:3475
+1348:2:3483
+1349:2:3484
+1350:2:3488
+1351:2:3489
+1352:2:3497
+1353:2:3502
+1354:2:3506
+1355:2:3507
+1356:2:3515
+1357:2:3516
+1358:2:3520
+1359:2:3521
+1360:2:3515
+1361:2:3516
+1362:2:3520
+1363:2:3521
+1364:2:3529
+1365:2:3534
+1366:2:3535
+1367:2:3546
+1368:2:3547
+1369:2:3548
+1370:2:3559
+1371:2:3564
+1372:2:3565
+1373:2:3576
+1374:2:3577
+1375:2:3578
+1376:2:3576
+1377:2:3577
+1378:2:3578
+1379:2:3589
+1380:0:4497
+1381:2:2881
+1382:0:4497
+1383:2:3598
+1384:2:3599
+1385:2:3603
+1386:2:3604
+1387:2:3612
+1388:2:3613
+1389:2:3617
+1390:2:3618
+1391:2:3626
+1392:2:3631
+1393:2:3635
+1394:2:3636
+1395:2:3644
+1396:2:3645
+1397:2:3649
+1398:2:3650
+1399:2:3644
+1400:2:3645
+1401:2:3649
+1402:2:3650
+1403:2:3658
+1404:2:3663
+1405:2:3664
+1406:2:3675
+1407:2:3676
+1408:2:3677
+1409:2:3688
+1410:2:3693
+1411:2:3694
+1412:2:3705
+1413:2:3706
+1414:2:3707
+1415:2:3705
+1416:2:3706
+1417:2:3707
+1418:2:3718
+1419:2:3725
+1420:0:4497
+1421:2:2881
+1422:0:4497
+1423:1:118
+1424:0:4497
+1425:1:120
+1426:0:4497
+1427:1:19
+1428:0:4497
+1429:1:126
+1430:1:127
+1431:1:131
+1432:1:132
+1433:1:140
+1434:1:141
+1435:1:145
+1436:1:146
+1437:1:154
+1438:1:159
+1439:1:163
+1440:1:164
+1441:1:172
+1442:1:173
+1443:1:177
+1444:1:178
+1445:1:172
+1446:1:173
+1447:1:177
+1448:1:178
+1449:1:186
+1450:1:191
+1451:1:192
+1452:1:203
+1453:1:204
+1454:1:205
+1455:1:216
+1456:1:221
+1457:1:222
+1458:1:233
+1459:1:234
+1460:1:235
+1461:1:233
+1462:1:234
+1463:1:235
+1464:1:246
+1465:0:4497
+1466:1:15
+1467:0:4497
+1468:1:16
+1469:0:4497
+1470:1:17
+1471:0:4497
+1472:1:118
+1473:0:4497
+1474:1:120
+1475:0:4497
+1476:1:19
+1477:0:4497
+1478:1:255
+1479:1:256
+1480:0:4497
+1481:1:15
+1482:0:4497
+1483:1:16
+1484:0:4497
+1485:1:17
+1486:0:4497
+1487:1:118
+1488:0:4497
+1489:1:120
+1490:0:4497
+1491:1:19
+1492:0:4497
+1493:1:262
+1494:1:263
+1495:1:267
+1496:1:268
+1497:1:276
+1498:1:277
+1499:1:281
+1500:1:282
+1501:1:290
+1502:1:295
+1503:1:299
+1504:1:300
+1505:1:308
+1506:1:309
+1507:1:313
+1508:1:314
+1509:1:308
+1510:1:309
+1511:1:313
+1512:1:314
+1513:1:322
+1514:1:327
+1515:1:328
+1516:1:339
+1517:1:340
+1518:1:341
+1519:1:352
+1520:1:357
+1521:1:358
+1522:1:369
+1523:1:370
+1524:1:371
+1525:1:369
+1526:1:370
+1527:1:371
+1528:1:382
+1529:0:4497
+1530:1:15
+1531:0:4497
+1532:1:16
+1533:0:4497
+1534:1:17
+1535:0:4497
+1536:1:118
+1537:0:4497
+1538:1:120
+1539:0:4497
+1540:1:19
+1541:0:4497
+1542:1:391
+1543:1:392
+1544:1:396
+1545:1:397
+1546:1:405
+1547:1:406
+1548:1:410
+1549:1:411
+1550:1:419
+1551:1:424
+1552:1:428
+1553:1:429
+1554:1:437
+1555:1:438
+1556:1:442
+1557:1:443
+1558:1:437
+1559:1:438
+1560:1:442
+1561:1:443
+1562:1:451
+1563:1:456
+1564:1:457
+1565:1:468
+1566:1:469
+1567:1:470
+1568:1:481
+1569:1:486
+1570:1:487
+1571:1:498
+1572:1:499
+1573:1:500
+1574:1:498
+1575:1:499
+1576:1:500
+1577:1:511
+1578:1:518
+1579:0:4497
+1580:1:15
+1581:0:4497
+1582:1:16
+1583:0:4497
+1584:1:17
+1585:0:4497
+1586:1:118
+1587:0:4497
+1588:1:120
+1589:0:4495
+1590:1:19
+1591:0:4501
+1592:1:1184
+1593:1:1185
+1594:1:1189
+1595:1:1190
+1596:1:1198
+1597:1:1199
+1598:1:1200
+1599:1:1212
+1600:1:1217
+1601:1:1221
+1602:1:1222
+1603:1:1230
+1604:1:1231
+1605:1:1235
+1606:1:1236
+1607:1:1230
+1608:1:1231
+1609:1:1235
+1610:1:1236
+1611:1:1244
+1612:1:1249
+1613:1:1250
+1614:1:1261
+1615:1:1262
+1616:1:1263
+1617:1:1274
+1618:1:1279
+1619:1:1280
+1620:1:1291
+1621:1:1292
+1622:1:1293
+1623:1:1291
+1624:1:1292
+1625:1:1293
+1626:1:1304
+1627:0:4501
+1628:1:15
+1629:0:4501
+1630:1:16
+1631:0:4501
+1632:2:3729
+1633:2:3730
+1634:2:3731
+1635:2:3743
+1636:2:3744
+1637:2:3748
+1638:2:3749
+1639:2:3757
+1640:2:3762
+1641:2:3766
+1642:2:3767
+1643:2:3775
+1644:2:3776
+1645:2:3780
+1646:2:3781
+1647:2:3775
+1648:2:3776
+1649:2:3780
+1650:2:3781
+1651:2:3789
+1652:2:3794
+1653:2:3795
+1654:2:3806
+1655:2:3807
+1656:2:3808
+1657:2:3819
+1658:2:3824
+1659:2:3825
+1660:2:3836
+1661:2:3837
+1662:2:3838
+1663:2:3836
+1664:2:3837
+1665:2:3838
+1666:2:3849
+1667:2:3857
+1668:0:4501
+1669:2:2881
+-1:-1:-1
+1670:0:4501
+1671:2:3863
+1672:2:3864
+1673:2:3868
+1674:2:3869
+1675:2:3877
+1676:2:3878
+1677:2:3882
+1678:2:3883
+1679:2:3891
+1680:2:3896
+1681:2:3900
+1682:2:3901
+1683:2:3909
+1684:2:3910
+1685:2:3914
+1686:2:3915
+1687:2:3909
+1688:2:3910
+1689:2:3914
+1690:2:3915
+1691:2:3923
+1692:2:3928
+1693:2:3929
+1694:2:3940
+1695:2:3941
+1696:2:3942
+1697:2:3953
+1698:2:3958
+1699:2:3959
+1700:2:3970
+1701:2:3971
+1702:2:3972
+1703:2:3970
+1704:2:3971
+1705:2:3972
+1706:2:3983
+1707:0:4501
+1708:2:2881
+1709:0:4501
+1710:2:3729
+1711:2:3730
+1712:2:3734
+1713:2:3735
+1714:2:3743
+1715:2:3744
+1716:2:3748
+1717:2:3749
+1718:2:3757
+1719:2:3762
+1720:2:3766
+1721:2:3767
+1722:2:3775
+1723:2:3776
+1724:2:3780
+1725:2:3781
+1726:2:3775
+1727:2:3776
+1728:2:3780
+1729:2:3781
+1730:2:3789
+1731:2:3794
+1732:2:3795
+1733:2:3806
+1734:2:3807
+1735:2:3808
+1736:2:3819
+1737:2:3824
+1738:2:3825
+1739:2:3836
+1740:2:3837
+1741:2:3838
+1742:2:3836
+1743:2:3837
+1744:2:3838
+1745:2:3849
+1746:2:3857
+1747:0:4501
+1748:2:2881
+1749:0:4501
+1750:2:3863
+1751:2:3864
+1752:2:3868
+1753:2:3869
+1754:2:3877
+1755:2:3878
+1756:2:3882
+1757:2:3883
+1758:2:3891
+1759:2:3896
+1760:2:3900
+1761:2:3901
+1762:2:3909
+1763:2:3910
+1764:2:3914
+1765:2:3915
+1766:2:3909
+1767:2:3910
+1768:2:3914
+1769:2:3915
+1770:2:3923
+1771:2:3928
+1772:2:3929
+1773:2:3940
+1774:2:3941
+1775:2:3942
+1776:2:3953
+1777:2:3958
+1778:2:3959
+1779:2:3970
+1780:2:3971
+1781:2:3972
+1782:2:3970
+1783:2:3971
+1784:2:3972
+1785:2:3983
+1786:0:4501
+1787:2:2881
+1788:0:4501
+1789:2:3729
+1790:2:3730
+1791:2:3734
+1792:2:3735
+1793:2:3743
+1794:2:3744
+1795:2:3748
+1796:2:3749
+1797:2:3757
+1798:2:3762
+1799:2:3766
+1800:2:3767
+1801:2:3775
+1802:2:3776
+1803:2:3780
+1804:2:3781
+1805:2:3775
+1806:2:3776
+1807:2:3780
+1808:2:3781
+1809:2:3789
+1810:2:3794
+1811:2:3795
+1812:2:3806
+1813:2:3807
+1814:2:3808
+1815:2:3819
+1816:2:3824
+1817:2:3825
+1818:2:3836
+1819:2:3837
+1820:2:3838
+1821:2:3836
+1822:2:3837
+1823:2:3838
+1824:2:3849
+1825:2:3857
+1826:0:4501
+1827:2:2881