X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-nosched-model%2Fresult-standard-execution-nest%2Furcu_free_no_mb.spin.input.trail;fp=formal-model%2Furcu-nosched-model%2Fresult-standard-execution-nest%2Furcu_free_no_mb.spin.input.trail;h=04e7425790e5a6ba41df99337abd7fb4fe0c67e4;hp=0000000000000000000000000000000000000000;hb=06e8b2a87f862183a26e0005bf04221633f49d0c;hpb=8322221dc666e720badeb06bc780a1f8e69020a0

diff --git a/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_mb.spin.input.trail b/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_mb.spin.input.trail
new file mode 100644
index 0000000..04e7425
--- /dev/null
+++ b/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,2149 @@
+-2:3:-2
+-4:-4:-4
+1:0:2654
+2:3:2606
+3:3:2609
+4:3:2609
+5:3:2612
+6:3:2620
+7:3:2620
+8:3:2623
+9:3:2629
+10:3:2633
+11:3:2633
+12:3:2636
+13:3:2644
+14:3:2648
+15:3:2649
+16:0:2654
+17:3:2651
+18:0:2654
+19:2:416
+20:0:2654
+21:2:422
+22:0:2654
+23:2:423
+24:0:2654
+25:2:424
+26:2:428
+27:2:429
+28:2:437
+29:2:438
+30:2:442
+31:2:443
+32:2:451
+33:2:456
+34:2:460
+35:2:461
+36:2:468
+37:2:469
+38:2:480
+39:2:481
+40:2:482
+41:2:493
+42:2:498
+43:2:499
+44:0:2654
+45:2:511
+46:0:2654
+47:2:513
+48:2:514
+49:0:2654
+50:2:518
+51:2:522
+52:2:523
+53:2:531
+54:2:532
+55:2:536
+56:2:537
+57:2:545
+58:2:550
+59:2:551
+60:2:562
+61:2:563
+62:2:574
+63:2:575
+64:2:576
+65:2:587
+66:2:592
+67:2:593
+68:0:2654
+69:2:605
+70:0:2654
+71:2:607
+72:0:2654
+73:2:608
+74:0:2654
+75:2:618
+76:0:2654
+77:2:619
+78:2:623
+79:2:624
+80:2:632
+81:2:633
+82:2:637
+83:2:638
+84:2:646
+85:2:651
+86:2:655
+87:2:656
+88:2:663
+89:2:664
+90:2:675
+91:2:676
+92:2:677
+93:2:688
+94:2:693
+95:2:694
+96:0:2654
+97:2:709
+98:0:2654
+99:2:710
+100:2:714
+101:2:715
+102:2:723
+103:2:724
+104:2:728
+105:2:729
+106:2:737
+107:2:742
+108:2:746
+109:2:747
+110:2:754
+111:2:755
+112:2:766
+113:2:767
+114:2:768
+115:2:779
+116:2:784
+117:2:785
+118:0:2654
+119:2:800
+120:0:2654
+121:2:805
+122:2:809
+123:2:810
+124:2:818
+125:2:819
+126:2:823
+127:2:824
+128:2:832
+129:2:837
+130:2:841
+131:2:842
+132:2:849
+133:2:850
+134:2:861
+135:2:862
+136:2:863
+137:2:874
+138:2:879
+139:2:880
+140:0:2654
+141:2:895
+142:0:2654
+143:2:897
+144:0:2654
+145:2:898
+146:2:902
+147:2:903
+148:2:911
+149:2:912
+150:2:916
+151:2:917
+152:2:925
+153:2:930
+154:2:934
+155:2:935
+156:2:942
+157:2:943
+158:2:954
+159:2:955
+160:2:956
+161:2:967
+162:2:972
+163:2:973
+164:0:2654
+165:2:985
+166:0:2654
+167:2:987
+168:0:2654
+169:2:990
+170:2:991
+171:2:1003
+172:2:1004
+173:2:1008
+174:2:1009
+175:2:1017
+176:2:1022
+177:2:1026
+178:2:1027
+179:2:1034
+180:2:1035
+181:2:1046
+182:2:1047
+183:2:1048
+184:2:1059
+185:2:1064
+186:2:1065
+187:0:2654
+188:2:1077
+189:0:2654
+190:2:1079
+191:0:2654
+192:2:1080
+193:0:2654
+194:2:1081
+195:0:2654
+196:2:1082
+197:0:2654
+198:2:1083
+199:2:1087
+200:2:1088
+201:2:1096
+202:2:1097
+203:2:1101
+204:2:1102
+205:2:1110
+206:2:1115
+207:2:1119
+208:2:1120
+209:2:1127
+210:2:1128
+211:2:1139
+212:2:1140
+213:2:1141
+214:2:1152
+215:2:1157
+216:2:1158
+217:0:2654
+218:2:1170
+219:0:2654
+220:2:1451
+221:0:2654
+222:2:1549
+223:0:2654
+224:2:1550
+225:0:2654
+226:2:1554
+227:0:2654
+228:2:1560
+229:2:1564
+230:2:1565
+231:2:1573
+232:2:1574
+233:2:1578
+234:2:1579
+235:2:1587
+236:2:1592
+237:2:1596
+238:2:1597
+239:2:1604
+240:2:1605
+241:2:1616
+242:2:1617
+243:2:1618
+244:2:1629
+245:2:1634
+246:2:1635
+247:0:2654
+248:2:1647
+249:0:2654
+250:2:1649
+251:0:2654
+252:2:1650
+253:2:1654
+254:2:1655
+255:2:1663
+256:2:1664
+257:2:1668
+258:2:1669
+259:2:1677
+260:2:1682
+261:2:1686
+262:2:1687
+263:2:1694
+264:2:1695
+265:2:1706
+266:2:1707
+267:2:1708
+268:2:1719
+269:2:1724
+270:2:1725
+271:0:2654
+272:2:1737
+273:0:2654
+274:2:1739
+275:0:2654
+276:2:1742
+277:2:1743
+278:2:1755
+279:2:1756
+280:2:1760
+281:2:1761
+282:2:1769
+283:2:1774
+284:2:1778
+285:2:1779
+286:2:1786
+287:2:1787
+288:2:1798
+289:2:1799
+290:2:1800
+291:2:1811
+292:2:1816
+293:2:1817
+294:0:2654
+295:2:1829
+296:0:2654
+297:2:1831
+298:0:2654
+299:2:1832
+300:0:2654
+301:2:1833
+302:0:2654
+303:2:1834
+304:0:2654
+305:2:1835
+306:2:1839
+307:2:1840
+308:2:1848
+309:2:1849
+310:2:1853
+311:2:1854
+312:2:1862
+313:2:1867
+314:2:1871
+315:2:1872
+316:2:1879
+317:2:1880
+318:2:1891
+319:2:1892
+320:2:1893
+321:2:1904
+322:2:1909
+323:2:1910
+324:0:2654
+325:2:1922
+326:0:2654
+327:2:2203
+328:0:2654
+329:2:2301
+330:0:2654
+331:2:2302
+332:0:2654
+333:2:2306
+334:0:2654
+335:2:2312
+336:2:2316
+337:2:2317
+338:2:2325
+339:2:2326
+340:2:2330
+341:2:2331
+342:2:2339
+343:2:2344
+344:2:2348
+345:2:2349
+346:2:2356
+347:2:2357
+348:2:2368
+349:2:2369
+350:2:2370
+351:2:2381
+352:2:2386
+353:2:2387
+354:0:2654
+355:2:2402
+356:0:2654
+357:2:2403
+358:2:2407
+359:2:2408
+360:2:2416
+361:2:2417
+362:2:2421
+363:2:2422
+364:2:2430
+365:2:2435
+366:2:2439
+367:2:2440
+368:2:2447
+369:2:2448
+370:2:2459
+371:2:2460
+372:2:2461
+373:2:2472
+374:2:2477
+375:2:2478
+376:0:2654
+377:2:2493
+378:0:2654
+379:2:2498
+380:2:2502
+381:2:2503
+382:2:2511
+383:2:2512
+384:2:2516
+385:2:2517
+386:2:2525
+387:2:2530
+388:2:2534
+389:2:2535
+390:2:2542
+391:2:2543
+392:2:2554
+393:2:2555
+394:2:2556
+395:2:2567
+396:2:2572
+397:2:2573
+398:0:2654
+399:2:2588
+400:0:2654
+401:2:2590
+402:0:2654
+403:2:2591
+404:0:2654
+405:2:423
+406:0:2654
+407:2:424
+408:2:428
+409:2:429
+410:2:437
+411:2:438
+412:2:442
+413:2:443
+414:2:451
+415:2:456
+416:2:460
+417:2:461
+418:2:468
+419:2:469
+420:2:480
+421:2:481
+422:2:482
+423:2:493
+424:2:498
+425:2:499
+426:0:2654
+427:2:511
+428:0:2654
+429:2:513
+430:2:514
+431:0:2654
+432:2:518
+433:2:522
+434:2:523
+435:2:531
+436:2:532
+437:2:536
+438:2:537
+439:2:545
+440:2:550
+441:2:551
+442:2:562
+443:2:563
+444:2:574
+445:2:575
+446:2:576
+447:2:587
+448:2:592
+449:2:593
+450:0:2654
+451:2:605
+452:0:2654
+453:2:607
+454:0:2654
+455:2:608
+456:0:2654
+457:2:618
+458:0:2654
+459:2:619
+460:2:623
+461:2:624
+462:2:632
+463:2:633
+464:2:637
+465:2:638
+466:2:646
+467:2:651
+468:2:655
+469:2:656
+470:2:663
+471:2:664
+472:2:675
+473:2:676
+474:2:677
+475:2:688
+476:2:693
+477:2:694
+478:0:2654
+479:2:709
+480:0:2654
+481:2:710
+482:2:714
+483:2:715
+484:2:723
+485:2:724
+486:2:728
+487:2:729
+488:2:737
+489:2:742
+490:2:746
+491:2:747
+492:2:754
+493:2:755
+494:2:766
+495:2:767
+496:2:768
+497:2:779
+498:2:784
+499:2:785
+500:0:2654
+501:2:800
+502:0:2654
+503:2:805
+504:2:809
+505:2:810
+506:2:818
+507:2:819
+508:2:823
+509:2:824
+510:2:832
+511:2:837
+512:2:841
+513:2:842
+514:2:849
+515:2:850
+516:2:861
+517:2:862
+518:2:863
+519:2:874
+520:2:879
+521:2:880
+522:0:2654
+523:2:895
+524:0:2654
+525:2:897
+526:0:2654
+527:2:898
+528:2:902
+529:2:903
+530:2:911
+531:2:912
+532:2:916
+533:2:917
+534:2:925
+535:2:930
+536:2:934
+537:2:935
+538:2:942
+539:2:943
+540:2:954
+541:2:955
+542:2:956
+543:2:967
+544:2:972
+545:2:973
+546:0:2654
+547:2:985
+548:0:2654
+549:2:987
+550:0:2654
+551:2:990
+552:2:991
+553:2:1003
+554:2:1004
+555:2:1008
+556:2:1009
+557:2:1017
+558:2:1022
+559:2:1026
+560:2:1027
+561:2:1034
+562:2:1035
+563:2:1046
+564:2:1047
+565:2:1048
+566:2:1059
+567:2:1064
+568:2:1065
+569:0:2654
+570:2:1077
+571:0:2654
+572:2:1079
+573:0:2654
+574:2:1080
+575:0:2654
+576:2:1081
+577:0:2654
+578:2:1082
+579:0:2654
+580:2:1083
+581:2:1087
+582:2:1088
+583:2:1096
+584:2:1097
+585:2:1101
+586:2:1102
+587:2:1110
+588:2:1115
+589:2:1119
+590:2:1120
+591:2:1127
+592:2:1128
+593:2:1139
+594:2:1140
+595:2:1141
+596:2:1152
+597:2:1157
+598:2:1158
+599:0:2654
+600:2:1170
+601:0:2654
+602:2:1451
+603:0:2654
+604:2:1549
+605:0:2654
+606:2:1550
+607:0:2654
+608:2:1554
+609:0:2654
+610:2:1560
+611:2:1564
+612:2:1565
+613:2:1573
+614:2:1574
+615:2:1578
+616:2:1579
+617:2:1587
+618:2:1592
+619:2:1596
+620:2:1597
+621:2:1604
+622:2:1605
+623:2:1616
+624:2:1617
+625:2:1618
+626:2:1629
+627:2:1634
+628:2:1635
+629:0:2654
+630:2:1647
+631:0:2654
+632:2:1649
+633:0:2654
+634:2:1650
+635:2:1654
+636:2:1655
+637:2:1663
+638:2:1664
+639:2:1668
+640:2:1669
+641:2:1677
+642:2:1682
+643:2:1686
+644:2:1687
+645:2:1694
+646:2:1695
+647:2:1706
+648:2:1707
+649:2:1708
+650:2:1719
+651:2:1724
+652:2:1725
+653:0:2654
+654:2:1737
+655:0:2654
+656:2:1739
+657:0:2654
+658:2:1742
+659:2:1743
+660:2:1755
+661:2:1756
+662:2:1760
+663:2:1761
+664:2:1769
+665:2:1774
+666:2:1778
+667:2:1779
+668:2:1786
+669:2:1787
+670:2:1798
+671:2:1799
+672:2:1800
+673:2:1811
+674:2:1816
+675:2:1817
+676:0:2654
+677:2:1829
+678:0:2654
+679:2:1831
+680:0:2654
+681:2:1832
+682:0:2654
+683:2:1833
+684:0:2654
+685:2:1834
+686:0:2654
+687:2:1835
+688:2:1839
+689:2:1840
+690:2:1848
+691:2:1849
+692:2:1853
+693:2:1854
+694:2:1862
+695:2:1867
+696:2:1871
+697:2:1872
+698:2:1879
+699:2:1880
+700:2:1891
+701:2:1892
+702:2:1893
+703:2:1904
+704:2:1909
+705:2:1910
+706:0:2654
+707:2:1922
+708:0:2654
+709:2:2203
+710:0:2654
+711:2:2301
+712:0:2654
+713:2:2302
+714:0:2654
+715:2:2306
+716:0:2654
+717:2:2312
+718:2:2316
+719:2:2317
+720:2:2325
+721:2:2326
+722:2:2330
+723:2:2331
+724:2:2339
+725:2:2344
+726:2:2348
+727:2:2349
+728:2:2356
+729:2:2357
+730:2:2368
+731:2:2369
+732:2:2370
+733:2:2381
+734:2:2386
+735:2:2387
+736:0:2654
+737:2:2402
+738:0:2654
+739:2:2403
+740:2:2407
+741:2:2408
+742:2:2416
+743:2:2417
+744:2:2421
+745:2:2422
+746:2:2430
+747:2:2435
+748:2:2439
+749:2:2440
+750:2:2447
+751:2:2448
+752:2:2459
+753:2:2460
+754:2:2461
+755:2:2472
+756:2:2477
+757:2:2478
+758:0:2654
+759:2:2493
+760:0:2654
+761:2:2498
+762:2:2502
+763:2:2503
+764:2:2511
+765:2:2512
+766:2:2516
+767:2:2517
+768:2:2525
+769:2:2530
+770:2:2534
+771:2:2535
+772:2:2542
+773:2:2543
+774:2:2554
+775:2:2555
+776:2:2556
+777:2:2567
+778:2:2572
+779:2:2573
+780:0:2654
+781:2:2588
+782:0:2654
+783:2:2590
+784:0:2654
+785:2:2591
+786:0:2654
+787:2:423
+788:0:2654
+789:2:424
+790:2:428
+791:2:429
+792:2:437
+793:2:438
+794:2:442
+795:2:443
+796:2:451
+797:2:456
+798:2:460
+799:2:461
+800:2:468
+801:2:469
+802:2:480
+803:2:481
+804:2:482
+805:2:493
+806:2:498
+807:2:499
+808:0:2654
+809:2:511
+810:0:2654
+811:2:513
+812:2:514
+813:0:2654
+814:2:518
+815:2:522
+816:2:523
+817:2:531
+818:2:532
+819:2:536
+820:2:537
+821:2:545
+822:2:550
+823:2:551
+824:2:562
+825:2:563
+826:2:574
+827:2:575
+828:2:576
+829:2:587
+830:2:592
+831:2:593
+832:0:2654
+833:2:605
+834:0:2654
+835:2:607
+836:0:2654
+837:2:608
+838:0:2654
+839:2:618
+840:0:2654
+841:2:619
+842:2:623
+843:2:624
+844:2:632
+845:2:633
+846:2:637
+847:2:638
+848:2:646
+849:2:651
+850:2:655
+851:2:656
+852:2:663
+853:2:664
+854:2:675
+855:2:676
+856:2:677
+857:2:688
+858:2:693
+859:2:694
+860:0:2654
+861:2:709
+862:0:2654
+863:2:710
+864:2:714
+865:2:715
+866:2:723
+867:2:724
+868:2:728
+869:2:729
+870:2:737
+871:2:742
+872:2:746
+873:2:747
+874:2:754
+875:2:755
+876:2:766
+877:2:767
+878:2:768
+879:2:779
+880:2:784
+881:2:785
+882:0:2654
+883:2:800
+884:0:2654
+885:2:805
+886:2:809
+887:2:810
+888:2:818
+889:2:819
+890:2:823
+891:2:824
+892:2:832
+893:2:837
+894:2:841
+895:2:842
+896:2:849
+897:2:850
+898:2:861
+899:2:862
+900:2:863
+901:2:874
+902:2:879
+903:2:880
+904:0:2654
+905:2:895
+906:0:2654
+907:2:897
+908:0:2654
+909:2:898
+910:2:902
+911:2:903
+912:2:911
+913:2:912
+914:2:916
+915:2:917
+916:2:925
+917:2:930
+918:2:934
+919:2:935
+920:2:942
+921:2:943
+922:2:954
+923:2:955
+924:2:956
+925:2:967
+926:2:972
+927:2:973
+928:0:2654
+929:2:985
+930:0:2654
+931:2:987
+932:0:2654
+933:2:990
+934:2:991
+935:2:1003
+936:2:1004
+937:2:1008
+938:2:1009
+939:2:1017
+940:2:1022
+941:2:1026
+942:2:1027
+943:2:1034
+944:2:1035
+945:2:1046
+946:2:1047
+947:2:1048
+948:2:1059
+949:2:1064
+950:2:1065
+951:0:2654
+952:2:1077
+953:0:2654
+954:2:1079
+955:0:2654
+956:2:1080
+957:0:2654
+958:2:1081
+959:0:2654
+960:2:1082
+961:0:2654
+962:2:1083
+963:2:1087
+964:2:1088
+965:2:1096
+966:2:1097
+967:2:1101
+968:2:1102
+969:2:1110
+970:2:1115
+971:2:1119
+972:2:1120
+973:2:1127
+974:2:1128
+975:2:1139
+976:2:1140
+977:2:1141
+978:2:1152
+979:2:1157
+980:2:1158
+981:0:2654
+982:2:1170
+983:0:2654
+984:2:1451
+985:0:2654
+986:2:1549
+987:0:2654
+988:2:1550
+989:0:2654
+990:2:1554
+991:0:2654
+992:2:1560
+993:2:1564
+994:2:1565
+995:2:1573
+996:2:1574
+997:2:1578
+998:2:1579
+999:2:1587
+1000:2:1592
+1001:2:1596
+1002:2:1597
+1003:2:1604
+1004:2:1605
+1005:2:1616
+1006:2:1617
+1007:2:1618
+1008:2:1629
+1009:2:1634
+1010:2:1635
+1011:0:2654
+1012:2:1647
+1013:0:2654
+1014:2:1649
+1015:0:2654
+1016:2:1650
+1017:2:1654
+1018:2:1655
+1019:2:1663
+1020:2:1664
+1021:2:1668
+1022:2:1669
+1023:2:1677
+1024:2:1682
+1025:2:1686
+1026:2:1687
+1027:2:1694
+1028:2:1695
+1029:2:1706
+1030:2:1707
+1031:2:1708
+1032:2:1719
+1033:2:1724
+1034:2:1725
+1035:0:2654
+1036:2:1737
+1037:0:2654
+1038:2:1739
+1039:0:2654
+1040:2:1742
+1041:2:1743
+1042:2:1755
+1043:2:1756
+1044:2:1760
+1045:2:1761
+1046:2:1769
+1047:2:1774
+1048:2:1778
+1049:2:1779
+1050:2:1786
+1051:2:1787
+1052:2:1798
+1053:2:1799
+1054:2:1800
+1055:2:1811
+1056:2:1816
+1057:2:1817
+1058:0:2654
+1059:2:1829
+1060:0:2654
+1061:2:1831
+1062:0:2654
+1063:2:1832
+1064:0:2654
+1065:2:1833
+1066:0:2654
+1067:2:1834
+1068:0:2654
+1069:2:1835
+1070:2:1839
+1071:2:1840
+1072:2:1848
+1073:2:1849
+1074:2:1853
+1075:2:1854
+1076:2:1862
+1077:2:1867
+1078:2:1871
+1079:2:1872
+1080:2:1879
+1081:2:1880
+1082:2:1891
+1083:2:1892
+1084:2:1893
+1085:2:1904
+1086:2:1909
+1087:2:1910
+1088:0:2654
+1089:2:1922
+1090:0:2654
+1091:2:2203
+1092:0:2654
+1093:2:2301
+1094:0:2654
+1095:2:2302
+1096:0:2654
+1097:2:2306
+1098:0:2654
+1099:2:2312
+1100:2:2316
+1101:2:2317
+1102:2:2325
+1103:2:2326
+1104:2:2330
+1105:2:2331
+1106:2:2339
+1107:2:2344
+1108:2:2348
+1109:2:2349
+1110:2:2356
+1111:2:2357
+1112:2:2368
+1113:2:2369
+1114:2:2370
+1115:2:2381
+1116:2:2386
+1117:2:2387
+1118:0:2654
+1119:2:2402
+1120:0:2654
+1121:2:2403
+1122:2:2407
+1123:2:2408
+1124:2:2416
+1125:2:2417
+1126:2:2421
+1127:2:2422
+1128:2:2430
+1129:2:2435
+1130:2:2439
+1131:2:2440
+1132:2:2447
+1133:2:2448
+1134:2:2459
+1135:2:2460
+1136:2:2461
+1137:2:2472
+1138:2:2477
+1139:2:2478
+1140:0:2654
+1141:2:2493
+1142:0:2654
+1143:2:2498
+1144:2:2502
+1145:2:2503
+1146:2:2511
+1147:2:2512
+1148:2:2516
+1149:2:2517
+1150:2:2525
+1151:2:2530
+1152:2:2534
+1153:2:2535
+1154:2:2542
+1155:2:2543
+1156:2:2554
+1157:2:2555
+1158:2:2556
+1159:2:2567
+1160:2:2572
+1161:2:2573
+1162:0:2654
+1163:2:2588
+1164:0:2654
+1165:2:2590
+1166:0:2654
+1167:2:2591
+1168:0:2654
+1169:2:423
+1170:0:2654
+1171:2:424
+1172:2:428
+1173:2:429
+1174:2:437
+1175:2:438
+1176:2:442
+1177:2:443
+1178:2:451
+1179:2:456
+1180:2:460
+1181:2:461
+1182:2:468
+1183:2:469
+1184:2:480
+1185:2:481
+1186:2:482
+1187:2:493
+1188:2:498
+1189:2:499
+1190:0:2654
+1191:2:511
+1192:0:2654
+1193:2:513
+1194:2:514
+1195:0:2654
+1196:2:518
+1197:2:522
+1198:2:523
+1199:2:531
+1200:2:532
+1201:2:536
+1202:2:537
+1203:2:545
+1204:2:550
+1205:2:551
+1206:2:562
+1207:2:563
+1208:2:574
+1209:2:575
+1210:2:576
+1211:2:587
+1212:2:592
+1213:2:593
+1214:0:2654
+1215:2:605
+1216:0:2654
+1217:2:607
+1218:0:2654
+1219:2:608
+1220:0:2654
+1221:2:618
+1222:0:2654
+1223:2:619
+1224:2:623
+1225:2:624
+1226:2:632
+1227:2:633
+1228:2:637
+1229:2:638
+1230:2:646
+1231:2:651
+1232:2:655
+1233:2:656
+1234:2:663
+1235:2:664
+1236:2:675
+1237:2:676
+1238:2:677
+1239:2:688
+1240:2:693
+1241:2:694
+1242:0:2654
+1243:2:709
+1244:0:2654
+1245:2:710
+1246:2:714
+1247:2:715
+1248:2:723
+1249:2:724
+1250:2:728
+1251:2:729
+1252:2:737
+1253:2:742
+1254:2:746
+1255:2:747
+1256:2:754
+1257:2:755
+1258:2:766
+1259:2:767
+1260:2:768
+1261:2:779
+1262:2:784
+1263:2:785
+1264:0:2654
+1265:2:800
+1266:0:2654
+1267:2:805
+1268:2:809
+1269:2:810
+1270:2:818
+1271:2:819
+1272:2:823
+1273:2:824
+1274:2:832
+1275:2:837
+1276:2:841
+1277:2:842
+1278:2:849
+1279:2:850
+1280:2:861
+1281:2:862
+1282:2:863
+1283:2:874
+1284:2:879
+1285:2:880
+1286:0:2654
+1287:2:895
+1288:0:2654
+1289:2:897
+1290:0:2654
+1291:2:898
+1292:2:902
+1293:2:903
+1294:2:911
+1295:2:912
+1296:2:916
+1297:2:917
+1298:2:925
+1299:2:930
+1300:2:934
+1301:2:935
+1302:2:942
+1303:2:943
+1304:2:954
+1305:2:955
+1306:2:956
+1307:2:967
+1308:2:972
+1309:2:973
+1310:0:2654
+1311:2:985
+1312:0:2654
+1313:2:987
+1314:0:2654
+1315:2:990
+1316:2:991
+1317:2:1003
+1318:2:1004
+1319:2:1008
+1320:2:1009
+1321:2:1017
+1322:2:1022
+1323:2:1026
+1324:2:1027
+1325:2:1034
+1326:2:1035
+1327:2:1046
+1328:2:1047
+1329:2:1048
+1330:2:1059
+1331:2:1064
+1332:2:1065
+1333:0:2654
+1334:2:1077
+1335:0:2654
+1336:2:1079
+1337:0:2654
+1338:2:1080
+1339:0:2654
+1340:2:1081
+1341:0:2654
+1342:2:1082
+1343:0:2654
+1344:2:1083
+1345:2:1087
+1346:2:1088
+1347:2:1096
+1348:2:1097
+1349:2:1101
+1350:2:1102
+1351:2:1110
+1352:2:1115
+1353:2:1119
+1354:2:1120
+1355:2:1127
+1356:2:1128
+1357:2:1139
+1358:2:1140
+1359:2:1141
+1360:2:1152
+1361:2:1157
+1362:2:1158
+1363:0:2654
+1364:2:1170
+1365:0:2654
+1366:2:1451
+1367:0:2654
+1368:2:1549
+1369:0:2654
+1370:2:1550
+1371:0:2654
+1372:2:1554
+1373:0:2654
+1374:2:1560
+1375:2:1564
+1376:2:1565
+1377:2:1573
+1378:2:1574
+1379:2:1578
+1380:2:1579
+1381:2:1587
+1382:2:1592
+1383:2:1596
+1384:2:1597
+1385:2:1604
+1386:2:1605
+1387:2:1616
+1388:2:1617
+1389:2:1618
+1390:2:1629
+1391:2:1634
+1392:2:1635
+1393:0:2654
+1394:2:1647
+1395:0:2654
+1396:2:1649
+1397:0:2654
+1398:2:1650
+1399:2:1654
+1400:2:1655
+1401:2:1663
+1402:2:1664
+1403:2:1668
+1404:2:1669
+1405:2:1677
+1406:2:1682
+1407:2:1686
+1408:2:1687
+1409:2:1694
+1410:2:1695
+1411:2:1706
+1412:2:1707
+1413:2:1708
+1414:2:1719
+1415:2:1724
+1416:2:1725
+1417:0:2654
+1418:2:1737
+1419:0:2654
+1420:2:1739
+1421:0:2654
+1422:2:1742
+1423:2:1743
+1424:2:1755
+1425:2:1756
+1426:2:1760
+1427:2:1761
+1428:2:1769
+1429:2:1774
+1430:2:1778
+1431:2:1779
+1432:2:1786
+1433:2:1787
+1434:2:1798
+1435:2:1799
+1436:2:1800
+1437:2:1811
+1438:2:1816
+1439:2:1817
+1440:0:2654
+1441:2:1829
+1442:0:2654
+1443:2:1831
+1444:0:2654
+1445:2:1832
+1446:0:2654
+1447:2:1833
+1448:0:2654
+1449:2:1834
+1450:0:2654
+1451:2:1835
+1452:2:1839
+1453:2:1840
+1454:2:1848
+1455:2:1849
+1456:2:1853
+1457:2:1854
+1458:2:1862
+1459:2:1867
+1460:2:1871
+1461:2:1872
+1462:2:1879
+1463:2:1880
+1464:2:1891
+1465:2:1892
+1466:2:1893
+1467:2:1904
+1468:2:1909
+1469:2:1910
+1470:0:2654
+1471:2:1922
+1472:0:2654
+1473:2:2203
+1474:0:2654
+1475:2:2301
+1476:0:2654
+1477:2:2302
+1478:0:2654
+1479:2:2306
+1480:0:2654
+1481:2:2312
+1482:2:2316
+1483:2:2317
+1484:2:2325
+1485:2:2326
+1486:2:2330
+1487:2:2331
+1488:2:2339
+1489:2:2344
+1490:2:2348
+1491:2:2349
+1492:2:2356
+1493:2:2357
+1494:2:2368
+1495:2:2369
+1496:2:2370
+1497:2:2381
+1498:2:2386
+1499:2:2387
+1500:0:2654
+1501:2:2402
+1502:0:2654
+1503:2:2403
+1504:2:2407
+1505:2:2408
+1506:2:2416
+1507:2:2417
+1508:2:2421
+1509:2:2422
+1510:2:2430
+1511:2:2435
+1512:2:2439
+1513:2:2440
+1514:2:2447
+1515:2:2448
+1516:2:2459
+1517:2:2460
+1518:2:2461
+1519:2:2472
+1520:2:2477
+1521:2:2478
+1522:0:2654
+1523:2:2493
+1524:0:2654
+1525:2:2498
+1526:2:2502
+1527:2:2503
+1528:2:2511
+1529:2:2512
+1530:2:2516
+1531:2:2517
+1532:2:2525
+1533:2:2530
+1534:2:2534
+1535:2:2535
+1536:2:2542
+1537:2:2543
+1538:2:2554
+1539:2:2555
+1540:2:2556
+1541:2:2567
+1542:2:2572
+1543:2:2573
+1544:0:2654
+1545:2:2588
+1546:0:2654
+1547:2:2590
+1548:0:2654
+1549:2:2591
+1550:0:2654
+1551:2:423
+1552:0:2654
+1553:2:424
+1554:2:428
+1555:2:429
+1556:2:437
+1557:2:438
+1558:2:442
+1559:2:443
+1560:2:451
+1561:2:456
+1562:2:460
+1563:2:461
+1564:2:468
+1565:2:469
+1566:2:480
+1567:2:481
+1568:2:482
+1569:2:493
+1570:2:498
+1571:2:499
+1572:0:2654
+1573:2:511
+1574:0:2654
+1575:2:513
+1576:2:514
+1577:0:2654
+1578:2:518
+1579:2:522
+1580:2:523
+1581:2:531
+1582:2:532
+1583:2:536
+1584:2:537
+1585:2:545
+1586:2:558
+1587:2:559
+1588:2:562
+1589:2:563
+1590:2:574
+1591:2:575
+1592:2:576
+1593:2:587
+1594:2:592
+1595:2:595
+1596:2:596
+1597:0:2654
+1598:2:605
+1599:0:2654
+1600:2:607
+1601:0:2654
+1602:2:608
+1603:0:2654
+1604:2:618
+1605:0:2654
+1606:2:619
+1607:2:623
+1608:2:624
+1609:2:632
+1610:2:633
+1611:2:637
+1612:2:638
+1613:2:646
+1614:2:659
+1615:2:660
+1616:2:663
+1617:2:664
+1618:2:675
+1619:2:676
+1620:2:677
+1621:2:688
+1622:2:693
+1623:2:696
+1624:2:697
+1625:0:2654
+1626:2:709
+1627:0:2654
+1628:2:710
+1629:2:714
+1630:2:715
+1631:2:723
+1632:2:724
+1633:2:728
+1634:2:729
+1635:2:737
+1636:2:750
+1637:2:751
+1638:2:754
+1639:2:755
+1640:2:766
+1641:2:767
+1642:2:768
+1643:2:779
+1644:2:784
+1645:2:787
+1646:2:788
+1647:0:2654
+1648:2:800
+1649:0:2654
+1650:2:805
+1651:2:809
+1652:2:810
+1653:2:818
+1654:2:819
+1655:2:823
+1656:2:824
+1657:2:832
+1658:2:845
+1659:2:846
+1660:2:849
+1661:2:850
+1662:2:861
+1663:2:862
+1664:2:863
+1665:2:874
+1666:2:879
+1667:2:882
+1668:2:883
+1669:0:2654
+1670:2:895
+1671:0:2654
+1672:2:897
+1673:0:2654
+1674:2:898
+1675:2:902
+1676:2:903
+1677:2:911
+1678:2:912
+1679:2:916
+1680:2:917
+1681:2:925
+1682:2:938
+1683:2:939
+1684:2:942
+1685:2:943
+1686:2:954
+1687:2:955
+1688:2:956
+1689:2:967
+1690:2:972
+1691:2:975
+1692:2:976
+1693:0:2654
+1694:2:985
+1695:0:2654
+1696:2:987
+1697:0:2654
+1698:2:990
+1699:2:991
+1700:2:1003
+1701:2:1004
+1702:2:1008
+1703:2:1009
+1704:2:1017
+1705:2:1030
+1706:2:1031
+1707:2:1034
+1708:2:1035
+1709:2:1046
+1710:2:1047
+1711:2:1048
+1712:2:1059
+1713:2:1064
+1714:2:1067
+1715:2:1068
+1716:0:2654
+1717:2:1077
+1718:0:2654
+1719:2:1079
+1720:0:2654
+1721:2:1080
+1722:0:2654
+1723:2:1081
+1724:0:2654
+1725:2:1082
+1726:0:2654
+1727:2:1083
+1728:2:1087
+1729:2:1088
+1730:2:1096
+1731:2:1097
+1732:2:1101
+1733:2:1102
+1734:2:1110
+1735:2:1123
+1736:2:1124
+1737:2:1127
+1738:2:1128
+1739:2:1139
+1740:2:1140
+1741:2:1141
+1742:2:1152
+1743:2:1157
+1744:2:1160
+1745:2:1161
+1746:0:2654
+1747:2:1170
+1748:0:2654
+1749:2:1451
+1750:0:2654
+1751:2:1549
+1752:0:2654
+1753:2:1550
+1754:0:2654
+1755:2:1554
+1756:0:2654
+1757:2:1560
+1758:2:1564
+1759:2:1565
+1760:2:1573
+1761:2:1574
+1762:2:1578
+1763:2:1579
+1764:2:1587
+1765:2:1600
+1766:2:1601
+1767:2:1604
+1768:2:1605
+1769:2:1616
+1770:2:1617
+1771:2:1618
+1772:2:1629
+1773:2:1634
+1774:2:1637
+1775:2:1638
+1776:0:2654
+1777:2:1647
+1778:0:2654
+1779:2:1649
+1780:0:2654
+1781:2:1650
+1782:2:1654
+1783:2:1655
+1784:2:1663
+1785:2:1664
+1786:2:1668
+1787:2:1669
+1788:2:1677
+1789:2:1690
+1790:2:1691
+1791:2:1694
+1792:2:1695
+1793:2:1706
+1794:2:1707
+1795:2:1708
+1796:2:1719
+1797:2:1724
+1798:2:1727
+1799:2:1728
+1800:0:2654
+1801:2:1737
+1802:0:2654
+1803:2:1739
+1804:0:2654
+1805:2:1742
+1806:2:1743
+1807:2:1755
+1808:2:1756
+1809:2:1760
+1810:2:1761
+1811:2:1769
+1812:2:1782
+1813:2:1783
+1814:2:1786
+1815:2:1787
+1816:2:1798
+1817:2:1799
+1818:2:1800
+1819:2:1811
+1820:2:1816
+1821:2:1819
+1822:2:1820
+1823:0:2654
+1824:2:1829
+1825:0:2654
+1826:2:1831
+1827:0:2654
+1828:2:1832
+1829:0:2654
+1830:2:1833
+1831:0:2654
+1832:2:1834
+1833:0:2654
+1834:2:1835
+1835:2:1839
+1836:2:1840
+1837:2:1848
+1838:2:1849
+1839:2:1853
+1840:2:1854
+1841:2:1862
+1842:2:1875
+1843:2:1876
+1844:2:1879
+1845:2:1880
+1846:2:1891
+1847:2:1892
+1848:2:1893
+1849:2:1904
+1850:2:1909
+1851:2:1912
+1852:2:1913
+1853:0:2654
+1854:2:1922
+1855:0:2654
+1856:2:2203
+1857:0:2654
+1858:2:2301
+1859:0:2654
+1860:2:2302
+1861:0:2654
+1862:2:2306
+1863:0:2654
+1864:2:2312
+1865:2:2316
+1866:2:2317
+1867:2:2325
+1868:2:2326
+1869:2:2330
+1870:2:2331
+1871:2:2339
+1872:2:2352
+1873:2:2353
+1874:2:2356
+1875:2:2357
+1876:2:2368
+1877:2:2369
+1878:2:2370
+1879:2:2381
+1880:2:2386
+1881:2:2389
+1882:2:2390
+1883:0:2654
+1884:2:2402
+1885:0:2654
+1886:2:2403
+1887:2:2407
+1888:2:2408
+1889:2:2416
+1890:2:2417
+1891:2:2421
+1892:2:2422
+1893:2:2430
+1894:2:2443
+1895:2:2444
+1896:2:2447
+1897:2:2448
+1898:2:2459
+1899:2:2460
+1900:2:2461
+1901:2:2472
+1902:2:2477
+1903:2:2480
+1904:2:2481
+1905:0:2654
+1906:2:2493
+1907:0:2654
+1908:2:2498
+1909:2:2502
+1910:2:2503
+1911:2:2511
+1912:2:2512
+1913:2:2516
+1914:2:2517
+1915:2:2525
+1916:2:2538
+1917:2:2539
+1918:2:2542
+1919:2:2543
+1920:2:2554
+1921:2:2555
+1922:2:2556
+1923:2:2567
+1924:2:2572
+1925:2:2575
+1926:2:2576
+1927:0:2654
+1928:2:2588
+1929:0:2654
+1930:2:2590
+1931:0:2654
+1932:2:2591
+1933:0:2654
+1934:2:2594
+1935:0:2654
+1936:2:2599
+1937:0:2654
+1938:1:2
+1939:0:2654
+1940:2:2600
+1941:0:2654
+1942:1:8
+1943:0:2654
+1944:2:2599
+1945:0:2654
+1946:1:9
+1947:0:2654
+1948:2:2600
+1949:0:2654
+1950:1:10
+1951:0:2654
+1952:2:2599
+1953:0:2654
+1954:1:11
+1955:0:2654
+1956:2:2600
+1957:0:2654
+1958:1:12
+1959:1:16
+1960:1:17
+1961:1:25
+1962:1:26
+1963:1:30
+1964:1:31
+1965:1:39
+1966:1:44
+1967:1:48
+1968:1:49
+1969:1:56
+1970:1:57
+1971:1:68
+1972:1:69
+1973:1:70
+1974:1:81
+1975:1:86
+1976:1:87
+1977:0:2654
+1978:2:2599
+1979:0:2654
+1980:1:99
+1981:0:2654
+1982:2:2600
+1983:0:2654
+1984:1:101
+1985:0:2654
+1986:2:2599
+1987:0:2654
+1988:1:102
+1989:1:106
+1990:1:107
+1991:1:115
+1992:1:116
+1993:1:120
+1994:1:121
+1995:1:129
+1996:1:134
+1997:1:138
+1998:1:139
+1999:1:146
+2000:1:147
+2001:1:158
+2002:1:159
+2003:1:160
+2004:1:171
+2005:1:176
+2006:1:177
+2007:0:2654
+2008:2:2600
+2009:0:2654
+2010:1:189
+2011:0:2654
+2012:2:2599
+2013:0:2654
+2014:1:191
+2015:0:2654
+2016:2:2600
+2017:0:2654
+2018:1:192
+2019:0:2654
+2020:2:2599
+2021:0:2654
+2022:1:193
+2023:1:197
+2024:1:198
+2025:1:206
+2026:1:207
+2027:1:211
+2028:1:212
+2029:1:220
+2030:1:225
+2031:1:229
+2032:1:230
+2033:1:237
+2034:1:238
+2035:1:249
+2036:1:250
+2037:1:251
+2038:1:262
+2039:1:267
+2040:1:268
+2041:0:2654
+2042:2:2600
+2043:0:2654
+2044:1:280
+2045:0:2654
+2046:2:2599
+2047:0:2654
+2048:1:282
+2049:0:2654
+2050:2:2600
+2051:0:2654
+2052:1:291
+2053:0:2654
+2054:2:2599
+2055:0:2654
+2056:1:293
+2057:0:2654
+2058:2:2600
+2059:0:2654
+2060:1:11
+2061:0:2654
+2062:2:2599
+2063:0:2654
+2064:1:12
+2065:1:16
+2066:1:17
+2067:1:25
+2068:1:26
+2069:1:27
+2070:1:39
+2071:1:44
+2072:1:48
+2073:1:49
+2074:1:56
+2075:1:57
+2076:1:68
+2077:1:69
+2078:1:70
+2079:1:81
+2080:1:86
+2081:1:87
+2082:0:2654
+2083:2:2600
+2084:0:2654
+2085:1:99
+2086:0:2654
+2087:2:2599
+2088:0:2654
+2089:1:101
+2090:0:2654
+2091:2:2600
+2092:0:2654
+2093:1:102
+2094:1:106
+2095:1:107
+2096:1:115
+2097:1:116
+2098:1:120
+2099:1:121
+2100:1:129
+2101:1:134
+2102:1:138
+2103:1:139
+2104:1:146
+2105:1:147
+2106:1:158
+2107:1:159
+2108:1:160
+2109:1:171
+2110:1:176
+2111:1:177
+2112:0:2654
+2113:2:2599
+2114:0:2654
+2115:1:189
+2116:0:2654
+2117:2:2600
+2118:0:2654
+2119:1:285
+2120:0:2654
+2121:2:2599
+2122:0:2654
+2123:1:286
+2124:0:2654
+2125:2:2600
+2126:0:2654
+2127:1:291
+2128:0:2654
+2129:2:2599
+2130:0:2654
+2131:1:293
+2132:0:2654
+2133:2:2600
+2134:0:2654
+2135:1:296
+2136:0:2654
+2137:2:2599
+2138:0:2654
+2139:1:301
+2140:0:2654
+2141:2:2600
+2142:0:2654
+2143:1:302
+2144:0:2652
+2145:2:2599
+2146:0:2658
+2147:2:779