Verification run #1, ipi and no-ipi results

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

diff --git a/formal-model/results/urcu-controldataflow-no-ipi/urcu_free_no_rmb.spin.input.trail b/formal-model/results/urcu-controldataflow-no-ipi/urcu_free_no_rmb.spin.input.trail
new file mode 100644 (file)
index 0000000..e179cd5
--- /dev/null
+++ b/formal-model/results/urcu-controldataflow-no-ipi/urcu_free_no_rmb.spin.input.trail
@@ -0,0 +1,1717 @@
+-2:3:-2
+-4:-4:-4
+1:0:4629
+2:3:4549
+3:3:4552
+4:3:4552
+5:3:4555
+6:3:4563
+7:3:4563
+8:3:4566
+9:3:4572
+10:3:4576
+11:3:4576
+12:3:4579
+13:3:4589
+14:3:4597
+15:3:4597
+16:3:4600
+17:3:4606
+18:3:4610
+19:3:4610
+20:3:4613
+21:3:4619
+22:3:4623
+23:3:4624
+24:0:4629
+25:3:4626
+26:0:4629
+27:2:3285
+28:0:4629
+29:2:3291
+30:0:4629
+31:2:3292
+32:0:4629
+33:2:3294
+34:0:4629
+35:2:3295
+36:0:4629
+37:2:3296
+38:2:3297
+39:2:3301
+40:2:3302
+41:2:3310
+42:2:3311
+43:2:3315
+44:2:3316
+45:2:3324
+46:2:3329
+47:2:3333
+48:2:3334
+49:2:3342
+50:2:3343
+51:2:3347
+52:2:3348
+53:2:3342
+54:2:3343
+55:2:3347
+56:2:3348
+57:2:3356
+58:2:3361
+59:2:3362
+60:2:3373
+61:2:3374
+62:2:3375
+63:2:3386
+64:2:3391
+65:2:3392
+66:2:3403
+67:2:3404
+68:2:3405
+69:2:3403
+70:2:3404
+71:2:3405
+72:2:3416
+73:2:3424
+74:0:4629
+75:2:3295
+76:0:4629
+77:2:3428
+78:2:3432
+79:2:3433
+80:2:3437
+81:2:3441
+82:2:3442
+83:2:3446
+84:2:3454
+85:2:3455
+86:2:3459
+87:2:3463
+88:2:3464
+89:2:3459
+90:2:3460
+91:2:3468
+92:0:4629
+93:2:3295
+94:0:4629
+95:2:3476
+96:2:3477
+97:2:3478
+98:0:4629
+99:2:3295
+100:0:4629
+101:2:3483
+102:0:4629
+103:2:4186
+104:2:4187
+105:2:4191
+106:2:4195
+107:2:4196
+108:2:4200
+109:2:4205
+110:2:4213
+111:2:4217
+112:2:4218
+113:2:4213
+114:2:4217
+115:2:4218
+116:2:4222
+117:2:4229
+118:2:4236
+119:2:4237
+120:2:4244
+121:2:4249
+122:2:4256
+123:2:4257
+124:2:4256
+125:2:4257
+126:2:4264
+127:2:4268
+128:0:4629
+129:2:3485
+130:2:4167
+131:0:4629
+132:2:3295
+133:0:4629
+134:2:3486
+135:0:4629
+136:2:3295
+137:0:4629
+138:2:3489
+139:2:3490
+140:2:3494
+141:2:3495
+142:2:3503
+143:2:3504
+144:2:3508
+145:2:3509
+146:2:3517
+147:2:3522
+148:2:3526
+149:2:3527
+150:2:3535
+151:2:3536
+152:2:3540
+153:2:3541
+154:2:3535
+155:2:3536
+156:2:3540
+157:2:3541
+158:2:3549
+159:2:3554
+160:2:3555
+161:2:3566
+162:2:3567
+163:2:3568
+164:2:3579
+165:2:3584
+166:2:3585
+167:2:3596
+168:2:3597
+169:2:3598
+170:2:3596
+171:2:3597
+172:2:3598
+173:2:3609
+174:2:3616
+175:0:4629
+176:2:3295
+177:0:4629
+178:2:3620
+179:2:3621
+180:2:3622
+181:2:3634
+182:2:3635
+183:2:3639
+184:2:3640
+185:2:3648
+186:2:3653
+187:2:3657
+188:2:3658
+189:2:3666
+190:2:3667
+191:2:3671
+192:2:3672
+193:2:3666
+194:2:3667
+195:2:3671
+196:2:3672
+197:2:3680
+198:2:3685
+199:2:3686
+200:2:3697
+201:2:3698
+202:2:3699
+203:2:3710
+204:2:3715
+205:2:3716
+206:2:3727
+207:2:3728
+208:2:3729
+209:2:3727
+210:2:3728
+211:2:3729
+212:2:3740
+213:2:3751
+214:2:3752
+215:0:4629
+216:2:3295
+217:0:4629
+218:2:3758
+219:2:3759
+220:2:3763
+221:2:3764
+222:2:3772
+223:2:3773
+224:2:3777
+225:2:3778
+226:2:3786
+227:2:3791
+228:2:3795
+229:2:3796
+230:2:3804
+231:2:3805
+232:2:3809
+233:2:3810
+234:2:3804
+235:2:3805
+236:2:3809
+237:2:3810
+238:2:3818
+239:2:3823
+240:2:3824
+241:2:3835
+242:2:3836
+243:2:3837
+244:2:3848
+245:2:3853
+246:2:3854
+247:2:3865
+248:2:3866
+249:2:3867
+250:2:3865
+251:2:3866
+252:2:3867
+253:2:3878
+254:0:4629
+255:2:3295
+256:0:4629
+257:2:3887
+258:2:3888
+259:2:3892
+260:2:3893
+261:2:3901
+262:2:3902
+263:2:3906
+264:2:3907
+265:2:3915
+266:2:3920
+267:2:3924
+268:2:3925
+269:2:3933
+270:2:3934
+271:2:3938
+272:2:3939
+273:2:3933
+274:2:3934
+275:2:3938
+276:2:3939
+277:2:3947
+278:2:3952
+279:2:3953
+280:2:3964
+281:2:3965
+282:2:3966
+283:2:3977
+284:2:3982
+285:2:3983
+286:2:3994
+287:2:3995
+288:2:3996
+289:2:3994
+290:2:3995
+291:2:3996
+292:2:4007
+293:2:4014
+294:0:4629
+295:2:3295
+296:0:4629
+297:2:4018
+298:2:4019
+299:2:4020
+300:2:4032
+301:2:4033
+302:2:4037
+303:2:4038
+304:2:4046
+305:2:4051
+306:2:4055
+307:2:4056
+308:2:4064
+309:2:4065
+310:2:4069
+311:2:4070
+312:2:4064
+313:2:4065
+314:2:4069
+315:2:4070
+316:2:4078
+317:2:4083
+318:2:4084
+319:2:4095
+320:2:4096
+321:2:4097
+322:2:4108
+323:2:4113
+324:2:4114
+325:2:4125
+326:2:4126
+327:2:4127
+328:2:4125
+329:2:4126
+330:2:4127
+331:2:4138
+332:2:4148
+333:2:4149
+334:0:4629
+335:2:3295
+336:0:4629
+337:2:4155
+338:0:4629
+339:2:4459
+340:2:4460
+341:2:4464
+342:2:4468
+343:2:4469
+344:2:4473
+345:2:4481
+346:2:4482
+347:2:4486
+348:2:4490
+349:2:4491
+350:2:4486
+351:2:4490
+352:2:4491
+353:2:4495
+354:2:4502
+355:2:4509
+356:2:4510
+357:2:4517
+358:2:4522
+359:2:4529
+360:2:4530
+361:2:4529
+362:2:4530
+363:2:4537
+364:2:4541
+365:0:4629
+366:2:4157
+367:2:4167
+368:0:4629
+369:2:3295
+370:0:4629
+371:2:4158
+372:2:4159
+373:0:4629
+374:2:3295
+375:0:4629
+376:2:4163
+377:0:4629
+378:2:4171
+379:0:4629
+380:2:3292
+381:0:4629
+382:2:3294
+383:0:4629
+384:2:3295
+385:0:4629
+386:2:3296
+387:2:3297
+388:2:3301
+389:2:3302
+390:2:3310
+391:2:3311
+392:2:3315
+393:2:3316
+394:2:3324
+395:2:3329
+396:2:3333
+397:2:3334
+398:2:3342
+399:2:3343
+400:2:3344
+401:2:3342
+402:2:3343
+403:2:3347
+404:2:3348
+405:2:3356
+406:2:3361
+407:2:3362
+408:2:3373
+409:2:3374
+410:2:3375
+411:2:3386
+412:2:3391
+413:2:3392
+414:2:3403
+415:2:3404
+416:2:3405
+417:2:3403
+418:2:3404
+419:2:3405
+420:2:3416
+421:2:3424
+422:0:4629
+423:2:3295
+424:0:4629
+425:2:3428
+426:2:3432
+427:2:3433
+428:2:3437
+429:2:3441
+430:2:3442
+431:2:3446
+432:2:3454
+433:2:3455
+434:2:3459
+435:2:3460
+436:2:3459
+437:2:3463
+438:2:3464
+439:2:3468
+440:0:4629
+441:2:3295
+442:0:4629
+443:2:3476
+444:2:3477
+445:2:3478
+446:0:4629
+447:2:3295
+448:0:4629
+449:2:3483
+450:0:4629
+451:2:4186
+452:2:4187
+453:2:4191
+454:2:4195
+455:2:4196
+456:2:4200
+457:2:4205
+458:2:4213
+459:2:4217
+460:2:4218
+461:2:4213
+462:2:4217
+463:2:4218
+464:2:4222
+465:2:4229
+466:2:4236
+467:2:4237
+468:2:4244
+469:2:4249
+470:2:4256
+471:2:4257
+472:2:4256
+473:2:4257
+474:2:4264
+475:2:4268
+476:0:4629
+477:2:3485
+478:2:4167
+479:0:4629
+480:2:3295
+481:0:4629
+482:2:3486
+483:0:4629
+484:2:3295
+485:0:4629
+486:2:3489
+487:2:3490
+488:2:3494
+489:2:3495
+490:2:3503
+491:2:3504
+492:2:3508
+493:2:3509
+494:2:3517
+495:2:3522
+496:2:3526
+497:2:3527
+498:2:3535
+499:2:3536
+500:2:3540
+501:2:3541
+502:2:3535
+503:2:3536
+504:2:3540
+505:2:3541
+506:2:3549
+507:2:3554
+508:2:3555
+509:2:3566
+510:2:3567
+511:2:3568
+512:2:3579
+513:2:3584
+514:2:3585
+515:2:3596
+516:2:3597
+517:2:3598
+518:2:3596
+519:2:3597
+520:2:3598
+521:2:3609
+522:2:3616
+523:0:4629
+524:2:3295
+525:0:4629
+526:2:3620
+527:2:3621
+528:2:3622
+529:2:3634
+530:2:3635
+531:2:3639
+532:2:3640
+533:2:3648
+534:2:3653
+535:2:3657
+536:2:3658
+537:2:3666
+538:2:3667
+539:2:3671
+540:2:3672
+541:2:3666
+542:2:3667
+543:2:3671
+544:2:3672
+545:2:3680
+546:2:3685
+547:2:3686
+548:2:3697
+549:2:3698
+550:2:3699
+551:2:3710
+552:2:3715
+553:2:3716
+554:2:3727
+555:2:3728
+556:2:3729
+557:2:3727
+558:2:3728
+559:2:3729
+560:2:3740
+561:2:3751
+562:2:3752
+563:0:4629
+564:2:3295
+565:0:4629
+566:2:3758
+567:2:3759
+568:2:3763
+569:2:3764
+570:2:3772
+571:2:3773
+572:2:3777
+573:2:3778
+574:2:3786
+575:2:3791
+576:2:3795
+577:2:3796
+578:2:3804
+579:2:3805
+580:2:3809
+581:2:3810
+582:2:3804
+583:2:3805
+584:2:3809
+585:2:3810
+586:2:3818
+587:2:3823
+588:2:3824
+589:2:3835
+590:2:3836
+591:2:3837
+592:2:3848
+593:2:3853
+594:2:3854
+595:2:3865
+596:2:3866
+597:2:3867
+598:2:3865
+599:2:3866
+600:2:3867
+601:2:3878
+602:0:4629
+603:2:3295
+604:0:4629
+605:2:3887
+606:2:3888
+607:2:3892
+608:2:3893
+609:2:3901
+610:2:3902
+611:2:3906
+612:2:3907
+613:2:3915
+614:2:3920
+615:2:3924
+616:2:3925
+617:2:3933
+618:2:3934
+619:2:3938
+620:2:3939
+621:2:3933
+622:2:3934
+623:2:3938
+624:2:3939
+625:2:3947
+626:2:3952
+627:2:3953
+628:2:3964
+629:2:3965
+630:2:3966
+631:2:3977
+632:2:3982
+633:2:3983
+634:2:3994
+635:2:3995
+636:2:3996
+637:2:3994
+638:2:3995
+639:2:3996
+640:2:4007
+641:2:4014
+642:0:4629
+643:2:3295
+644:0:4629
+645:2:4018
+646:2:4019
+647:2:4020
+648:2:4032
+649:2:4033
+650:2:4037
+651:2:4038
+652:2:4046
+653:2:4051
+654:2:4055
+655:2:4056
+656:2:4064
+657:2:4065
+658:2:4069
+659:2:4070
+660:2:4064
+661:2:4065
+662:2:4069
+663:2:4070
+664:2:4078
+665:2:4083
+666:2:4084
+667:2:4095
+668:2:4096
+669:2:4097
+670:2:4108
+671:2:4113
+672:2:4114
+673:2:4125
+674:2:4126
+675:2:4127
+676:2:4125
+677:2:4126
+678:2:4127
+679:2:4138
+680:2:4148
+681:2:4149
+682:0:4629
+683:2:3295
+684:0:4629
+685:2:4155
+686:0:4629
+687:2:4459
+688:2:4460
+689:2:4464
+690:2:4468
+691:2:4469
+692:2:4473
+693:2:4481
+694:2:4482
+695:2:4486
+696:2:4490
+697:2:4491
+698:2:4486
+699:2:4490
+700:2:4491
+701:2:4495
+702:2:4502
+703:2:4509
+704:2:4510
+705:2:4517
+706:2:4522
+707:2:4529
+708:2:4530
+709:2:4529
+710:2:4530
+711:2:4537
+712:2:4541
+713:0:4629
+714:2:4157
+715:2:4167
+716:0:4629
+717:2:3295
+718:0:4629
+719:2:4158
+720:2:4159
+721:0:4629
+722:2:3295
+723:0:4629
+724:2:4163
+725:0:4629
+726:2:4171
+727:0:4629
+728:2:3292
+729:0:4629
+730:2:3294
+731:0:4629
+732:2:3295
+733:0:4629
+734:2:3296
+735:2:3297
+736:2:3301
+737:2:3302
+738:2:3310
+739:2:3311
+740:2:3315
+741:2:3316
+742:2:3324
+743:2:3329
+744:2:3333
+745:2:3334
+746:2:3342
+747:2:3343
+748:2:3347
+749:2:3348
+750:2:3342
+751:2:3343
+752:2:3344
+753:2:3356
+754:2:3361
+755:2:3362
+756:2:3373
+757:2:3374
+758:2:3375
+759:2:3386
+760:2:3391
+761:2:3392
+762:2:3403
+763:2:3404
+764:2:3405
+765:2:3403
+766:2:3404
+767:2:3405
+768:2:3416
+769:2:3424
+770:0:4629
+771:2:3295
+772:0:4629
+773:1:2
+774:0:4629
+775:1:8
+776:0:4629
+777:1:9
+778:0:4629
+779:1:10
+780:0:4629
+781:1:11
+782:0:4629
+783:1:12
+784:1:13
+785:1:17
+786:1:18
+787:1:26
+788:1:27
+789:1:31
+790:1:32
+791:1:40
+792:1:45
+793:1:49
+794:1:50
+795:1:58
+796:1:59
+797:1:63
+798:1:64
+799:1:58
+800:1:59
+801:1:63
+802:1:64
+803:1:72
+804:1:77
+805:1:78
+806:1:89
+807:1:90
+808:1:91
+809:1:102
+810:1:107
+811:1:108
+812:1:119
+813:1:120
+814:1:121
+815:1:119
+816:1:120
+817:1:121
+818:1:132
+819:0:4629
+820:1:11
+821:0:4629
+822:1:141
+823:1:142
+824:0:4629
+825:1:11
+826:0:4629
+827:1:148
+828:1:149
+829:1:153
+830:1:154
+831:1:162
+832:1:163
+833:1:167
+834:1:168
+835:1:176
+836:1:181
+837:1:185
+838:1:186
+839:1:194
+840:1:195
+841:1:199
+842:1:200
+843:1:194
+844:1:195
+845:1:199
+846:1:200
+847:1:208
+848:1:213
+849:1:214
+850:1:225
+851:1:226
+852:1:227
+853:1:238
+854:1:243
+855:1:244
+856:1:255
+857:1:256
+858:1:257
+859:1:255
+860:1:256
+861:1:257
+862:1:268
+863:0:4629
+864:1:11
+865:0:4629
+866:1:277
+867:1:278
+868:1:282
+869:1:283
+870:1:291
+871:1:292
+872:1:296
+873:1:297
+874:1:305
+875:1:310
+876:1:314
+877:1:315
+878:1:323
+879:1:324
+880:1:328
+881:1:329
+882:1:323
+883:1:324
+884:1:328
+885:1:329
+886:1:337
+887:1:342
+888:1:343
+889:1:354
+890:1:355
+891:1:356
+892:1:367
+893:1:372
+894:1:373
+895:1:384
+896:1:385
+897:1:386
+898:1:384
+899:1:385
+900:1:386
+901:1:397
+902:1:404
+903:0:4629
+904:1:11
+905:0:4629
+906:1:540
+907:1:544
+908:1:545
+909:1:549
+910:1:550
+911:1:558
+912:1:566
+913:1:567
+914:1:571
+915:1:575
+916:1:576
+917:1:571
+918:1:575
+919:1:576
+920:1:580
+921:1:587
+922:1:594
+923:1:595
+924:1:602
+925:1:607
+926:1:614
+927:1:615
+928:1:614
+929:1:615
+930:1:622
+931:0:4629
+932:1:11
+933:0:4629
+934:2:3428
+935:2:3432
+936:2:3433
+937:2:3437
+938:2:3441
+939:2:3442
+940:2:3446
+941:2:3454
+942:2:3455
+943:2:3459
+944:2:3463
+945:2:3464
+946:2:3459
+947:2:3460
+948:2:3468
+949:0:4629
+950:2:3295
+951:0:4629
+952:2:3476
+953:2:3477
+954:2:3478
+955:0:4629
+956:2:3295
+957:0:4629
+958:2:3483
+959:0:4629
+960:2:4186
+961:2:4187
+962:2:4191
+963:2:4195
+964:2:4196
+965:2:4200
+966:2:4205
+967:2:4213
+968:2:4217
+969:2:4218
+970:2:4213
+971:2:4217
+972:2:4218
+973:2:4222
+974:2:4229
+975:2:4236
+976:2:4237
+977:2:4244
+978:2:4249
+979:2:4256
+980:2:4257
+981:2:4256
+982:2:4257
+983:2:4264
+984:2:4268
+985:0:4629
+986:2:3485
+987:2:4167
+988:0:4629
+989:2:3295
+990:0:4629
+991:2:3486
+992:0:4629
+993:2:3295
+994:0:4629
+995:2:3489
+996:2:3490
+997:2:3494
+998:2:3495
+999:2:3503
+1000:2:3504
+1001:2:3508
+1002:2:3509
+1003:2:3517
+1004:2:3522
+1005:2:3526
+1006:2:3527
+1007:2:3535
+1008:2:3536
+1009:2:3540
+1010:2:3541
+1011:2:3535
+1012:2:3536
+1013:2:3540
+1014:2:3541
+1015:2:3549
+1016:2:3554
+1017:2:3555
+1018:2:3566
+1019:2:3567
+1020:2:3568
+1021:2:3579
+1022:2:3584
+1023:2:3585
+1024:2:3596
+1025:2:3597
+1026:2:3598
+1027:2:3596
+1028:2:3597
+1029:2:3598
+1030:2:3609
+1031:2:3616
+1032:0:4629
+1033:2:3295
+1034:0:4629
+1035:2:3620
+1036:2:3621
+1037:2:3622
+1038:2:3634
+1039:2:3635
+1040:2:3639
+1041:2:3640
+1042:2:3648
+1043:2:3653
+1044:2:3657
+1045:2:3658
+1046:2:3666
+1047:2:3667
+1048:2:3671
+1049:2:3672
+1050:2:3666
+1051:2:3667
+1052:2:3671
+1053:2:3672
+1054:2:3680
+1055:2:3685
+1056:2:3686
+1057:2:3697
+1058:2:3698
+1059:2:3699
+1060:2:3710
+1061:2:3715
+1062:2:3716
+1063:2:3727
+1064:2:3728
+1065:2:3729
+1066:2:3727
+1067:2:3728
+1068:2:3729
+1069:2:3740
+1070:2:3749
+1071:0:4629
+1072:2:3295
+1073:0:4629
+1074:2:3755
+1075:0:4629
+1076:2:4277
+1077:2:4278
+1078:2:4282
+1079:2:4286
+1080:2:4287
+1081:2:4291
+1082:2:4299
+1083:2:4300
+1084:2:4304
+1085:2:4308
+1086:2:4309
+1087:2:4304
+1088:2:4308
+1089:2:4309
+1090:2:4313
+1091:2:4320
+1092:2:4327
+1093:2:4328
+1094:2:4335
+1095:2:4340
+1096:2:4347
+1097:2:4348
+1098:2:4347
+1099:2:4348
+1100:2:4355
+1101:2:4359
+1102:0:4629
+1103:2:3757
+1104:2:4167
+1105:0:4629
+1106:2:3295
+1107:0:4629
+1108:1:632
+1109:1:633
+1110:1:637
+1111:1:638
+1112:1:646
+1113:1:647
+1114:1:651
+1115:1:652
+1116:1:660
+1117:1:665
+1118:1:669
+1119:1:670
+1120:1:678
+1121:1:679
+1122:1:683
+1123:1:684
+1124:1:678
+1125:1:679
+1126:1:683
+1127:1:684
+1128:1:692
+1129:1:697
+1130:1:698
+1131:1:709
+1132:1:710
+1133:1:711
+1134:1:722
+1135:1:727
+1136:1:728
+1137:1:739
+1138:1:740
+1139:1:741
+1140:1:739
+1141:1:747
+1142:1:748
+1143:1:752
+1144:0:4629
+1145:1:11
+1146:0:4629
+1147:2:3620
+1148:2:3621
+1149:2:3625
+1150:2:3626
+1151:2:3634
+1152:2:3635
+1153:2:3639
+1154:2:3640
+1155:2:3648
+1156:2:3653
+1157:2:3657
+1158:2:3658
+1159:2:3666
+1160:2:3667
+1161:2:3671
+1162:2:3672
+1163:2:3666
+1164:2:3667
+1165:2:3671
+1166:2:3672
+1167:2:3680
+1168:2:3685
+1169:2:3686
+1170:2:3697
+1171:2:3698
+1172:2:3699
+1173:2:3710
+1174:2:3715
+1175:2:3716
+1176:2:3727
+1177:2:3728
+1178:2:3729
+1179:2:3727
+1180:2:3728
+1181:2:3729
+1182:2:3740
+1183:2:3749
+1184:0:4629
+1185:2:3295
+1186:0:4629
+1187:2:3755
+1188:0:4629
+1189:2:4277
+1190:2:4278
+1191:2:4282
+1192:2:4286
+1193:2:4287
+1194:2:4291
+1195:2:4299
+1196:2:4300
+1197:2:4304
+1198:2:4308
+1199:2:4309
+1200:2:4304
+1201:2:4308
+1202:2:4309
+1203:2:4313
+1204:2:4320
+1205:2:4327
+1206:2:4328
+1207:2:4335
+1208:2:4340
+1209:2:4347
+1210:2:4348
+1211:2:4347
+1212:2:4348
+1213:2:4355
+1214:2:4359
+1215:0:4629
+1216:2:3757
+1217:2:4167
+1218:0:4629
+1219:1:761
+1220:1:764
+1221:1:765
+1222:0:4629
+1223:2:3295
+1224:0:4629
+1225:1:11
+1226:0:4629
+1227:2:3620
+1228:2:3621
+1229:2:3625
+1230:2:3626
+1231:2:3634
+1232:2:3635
+1233:2:3639
+1234:2:3640
+1235:2:3648
+1236:2:3653
+1237:2:3657
+1238:2:3658
+1239:2:3666
+1240:2:3667
+1241:2:3671
+1242:2:3672
+1243:2:3666
+1244:2:3667
+1245:2:3671
+1246:2:3672
+1247:2:3680
+1248:2:3685
+1249:2:3686
+1250:2:3697
+1251:2:3698
+1252:2:3699
+1253:2:3710
+1254:2:3715
+1255:2:3716
+1256:2:3727
+1257:2:3728
+1258:2:3729
+1259:2:3727
+1260:2:3728
+1261:2:3729
+1262:2:3740
+1263:2:3749
+1264:0:4629
+1265:2:3295
+1266:0:4629
+1267:2:3755
+1268:0:4629
+1269:2:4277
+1270:2:4278
+1271:2:4282
+1272:2:4286
+1273:2:4287
+1274:2:4291
+1275:2:4299
+1276:2:4300
+1277:2:4304
+1278:2:4308
+1279:2:4309
+1280:2:4304
+1281:2:4308
+1282:2:4309
+1283:2:4313
+1284:2:4320
+1285:2:4327
+1286:2:4328
+1287:2:4335
+1288:2:4340
+1289:2:4347
+1290:2:4348
+1291:2:4347
+1292:2:4348
+1293:2:4355
+1294:2:4359
+1295:0:4629
+1296:2:3757
+1297:2:4167
+1298:0:4629
+1299:1:1028
+1300:1:1029
+1301:1:1033
+1302:1:1034
+1303:1:1042
+1304:1:1043
+1305:1:1047
+1306:1:1048
+1307:1:1056
+1308:1:1061
+1309:1:1065
+1310:1:1066
+1311:1:1074
+1312:1:1075
+1313:1:1079
+1314:1:1080
+1315:1:1074
+1316:1:1075
+1317:1:1079
+1318:1:1080
+1319:1:1088
+1320:1:1093
+1321:1:1094
+1322:1:1105
+1323:1:1106
+1324:1:1107
+1325:1:1118
+1326:1:1123
+1327:1:1124
+1328:1:1135
+1329:1:1136
+1330:1:1137
+1331:1:1135
+1332:1:1143
+1333:1:1144
+1334:1:1148
+1335:1:1155
+1336:1:1159
+1337:0:4629
+1338:2:3295
+1339:0:4629
+1340:1:11
+1341:0:4629
+1342:2:3620
+1343:2:3621
+1344:2:3625
+1345:2:3626
+1346:2:3634
+1347:2:3635
+1348:2:3639
+1349:2:3640
+1350:2:3648
+1351:2:3653
+1352:2:3657
+1353:2:3658
+1354:2:3666
+1355:2:3667
+1356:2:3671
+1357:2:3672
+1358:2:3666
+1359:2:3667
+1360:2:3671
+1361:2:3672
+1362:2:3680
+1363:2:3685
+1364:2:3686
+1365:2:3697
+1366:2:3698
+1367:2:3699
+1368:2:3710
+1369:2:3715
+1370:2:3716
+1371:2:3727
+1372:2:3728
+1373:2:3729
+1374:2:3727
+1375:2:3728
+1376:2:3729
+1377:2:3740
+1378:2:3749
+1379:0:4629
+1380:2:3295
+1381:0:4629
+1382:2:3755
+1383:0:4629
+1384:2:4277
+1385:2:4278
+1386:2:4282
+1387:2:4286
+1388:2:4287
+1389:2:4291
+1390:2:4299
+1391:2:4300
+1392:2:4304
+1393:2:4308
+1394:2:4309
+1395:2:4304
+1396:2:4308
+1397:2:4309
+1398:2:4313
+1399:2:4320
+1400:2:4327
+1401:2:4328
+1402:2:4335
+1403:2:4340
+1404:2:4347
+1405:2:4348
+1406:2:4347
+1407:2:4348
+1408:2:4355
+1409:2:4359
+1410:0:4629
+1411:2:3757
+1412:2:4167
+1413:0:4629
+1414:1:1160
+1415:1:1161
+1416:1:1165
+1417:1:1166
+1418:1:1174
+1419:1:1175
+1420:1:1176
+1421:1:1188
+1422:1:1193
+1423:1:1197
+1424:1:1198
+1425:1:1206
+1426:1:1207
+1427:1:1211
+1428:1:1212
+1429:1:1206
+1430:1:1207
+1431:1:1211
+1432:1:1212
+1433:1:1220
+1434:1:1225
+1435:1:1226
+1436:1:1237
+1437:1:1238
+1438:1:1239
+1439:1:1250
+1440:1:1255
+1441:1:1256
+1442:1:1267
+1443:1:1268
+1444:1:1269
+1445:1:1267
+1446:1:1275
+1447:1:1276
+1448:1:1280
+1449:0:4629
+1450:2:3295
+1451:0:4629
+1452:1:11
+1453:0:4629
+1454:2:3620
+1455:2:3621
+1456:2:3625
+1457:2:3626
+1458:2:3634
+1459:2:3635
+1460:2:3639
+1461:2:3640
+1462:2:3648
+1463:2:3653
+1464:2:3657
+1465:2:3658
+1466:2:3666
+1467:2:3667
+1468:2:3671
+1469:2:3672
+1470:2:3666
+1471:2:3667
+1472:2:3671
+1473:2:3672
+1474:2:3680
+1475:2:3685
+1476:2:3686
+1477:2:3697
+1478:2:3698
+1479:2:3699
+1480:2:3710
+1481:2:3715
+1482:2:3716
+1483:2:3727
+1484:2:3728
+1485:2:3729
+1486:2:3727
+1487:2:3728
+1488:2:3729
+1489:2:3740
+1490:2:3749
+1491:0:4629
+1492:2:3295
+1493:0:4629
+1494:2:3755
+1495:0:4629
+1496:2:4277
+1497:2:4278
+1498:2:4282
+1499:2:4286
+1500:2:4287
+1501:2:4291
+1502:2:4299
+1503:2:4300
+1504:2:4304
+1505:2:4308
+1506:2:4309
+1507:2:4304
+1508:2:4308
+1509:2:4309
+1510:2:4313
+1511:2:4320
+1512:2:4327
+1513:2:4328
+1514:2:4335
+1515:2:4340
+1516:2:4347
+1517:2:4348
+1518:2:4347
+1519:2:4348
+1520:2:4355
+1521:2:4359
+1522:0:4629
+1523:2:3757
+1524:2:4167
+1525:0:4629
+1526:2:3295
+1527:0:4629
+1528:1:1289
+1529:0:4629
+1530:2:3620
+1531:2:3621
+1532:2:3625
+1533:2:3626
+1534:2:3634
+1535:2:3635
+1536:2:3639
+1537:2:3640
+1538:2:3648
+1539:2:3653
+1540:2:3657
+1541:2:3658
+1542:2:3666
+1543:2:3667
+1544:2:3671
+1545:2:3672
+1546:2:3666
+1547:2:3667
+1548:2:3671
+1549:2:3672
+1550:2:3680
+1551:2:3685
+1552:2:3686
+1553:2:3697
+1554:2:3698
+1555:2:3699
+1556:2:3710
+1557:2:3715
+1558:2:3716
+1559:2:3727
+1560:2:3728
+1561:2:3729
+1562:2:3727
+1563:2:3728
+1564:2:3729
+1565:2:3740
+1566:2:3749
+1567:0:4629
+1568:2:3295
+1569:0:4629
+1570:2:3755
+1571:0:4629
+1572:2:4277
+1573:2:4278
+1574:2:4282
+1575:2:4286
+1576:2:4287
+1577:2:4291
+1578:2:4299
+1579:2:4300
+1580:2:4304
+1581:2:4308
+1582:2:4309
+1583:2:4304
+1584:2:4308
+1585:2:4309
+1586:2:4313
+1587:2:4320
+1588:2:4327
+1589:2:4328
+1590:2:4335
+1591:2:4340
+1592:2:4347
+1593:2:4348
+1594:2:4347
+1595:2:4348
+1596:2:4355
+1597:2:4359
+1598:0:4629
+1599:2:3757
+1600:2:4167
+1601:0:4629
+1602:1:3023
+1603:1:3027
+1604:1:3028
+1605:1:3036
+1606:1:3037
+1607:1:3041
+1608:1:3042
+1609:1:3050
+1610:1:3055
+1611:1:3059
+1612:1:3060
+1613:1:3068
+1614:1:3069
+1615:1:3073
+1616:1:3074
+1617:1:3068
+1618:1:3069
+1619:1:3073
+1620:1:3074
+1621:1:3082
+1622:1:3087
+1623:1:3088
+1624:1:3099
+1625:1:3100
+1626:1:3101
+1627:1:3112
+1628:1:3117
+1629:1:3118
+1630:1:3129
+1631:1:3130
+1632:1:3131
+1633:1:3129
+1634:1:3137
+1635:1:3138
+1636:1:3142
+1637:1:3146
+1638:0:4629
+1639:2:3295
+1640:0:4629
+1641:2:3620
+1642:2:3621
+1643:2:3625
+1644:2:3626
+1645:2:3634
+1646:2:3635
+1647:2:3639
+1648:2:3640
+1649:2:3648
+1650:2:3653
+1651:2:3657
+1652:2:3658
+1653:2:3666
+1654:2:3667
+1655:2:3671
+1656:2:3672
+1657:2:3666
+1658:2:3667
+1659:2:3671
+1660:2:3672
+1661:2:3680
+1662:2:3685
+1663:2:3686
+1664:2:3697
+1665:2:3698
+1666:2:3699
+1667:2:3710
+1668:2:3715
+1669:2:3716
+1670:2:3727
+1671:2:3728
+1672:2:3729
+1673:2:3727
+1674:2:3728
+1675:2:3729
+1676:2:3740
+1677:2:3749
+1678:0:4629
+1679:2:3295
+1680:0:4629
+1681:2:3755
+1682:0:4629
+1683:2:4277
+1684:2:4278
+1685:2:4282
+1686:2:4286
+1687:2:4287
+1688:2:4291
+1689:2:4299
+1690:2:4300
+1691:2:4304
+1692:2:4308
+1693:2:4309
+1694:2:4304
+1695:2:4308
+1696:2:4309
+1697:2:4313
+1698:2:4320
+1699:2:4327
+1700:2:4328
+1701:2:4335
+1702:2:4340
+1703:2:4347
+1704:2:4348
+1705:2:4347
+1706:2:4348
+1707:2:4355
+1708:2:4359
+1709:0:4629
+1710:1:1291
+1711:1:1292
+1712:0:4627
+1713:1:11
+1714:0:4633
+1715:1:208