X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2Fresult-standard-execution-nonest%2Furcu_free_no_wmb.spin.input.trail;fp=formal-model%2Furcu%2Fresult-standard-execution-nonest%2Furcu_free_no_wmb.spin.input.trail;h=fe987f06ebac7d458655a212c2d7cb945b8c0437;hb=8baf2c9506f8e4bbac913c7ea2a8b2e9a3cd0932;hp=0000000000000000000000000000000000000000;hpb=fa5b67244cb2c3733d2c0195d3ad239d97ec2dc3;p=urcu.git

diff --git a/formal-model/urcu/result-standard-execution-nonest/urcu_free_no_wmb.spin.input.trail b/formal-model/urcu/result-standard-execution-nonest/urcu_free_no_wmb.spin.input.trail
new file mode 100644
index 0000000..fe987f0
--- /dev/null
+++ b/formal-model/urcu/result-standard-execution-nonest/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1617 @@
+-2:3:-2
+-4:-4:-4
+1:0:1946
+2:3:1898
+3:3:1901
+4:3:1901
+5:3:1904
+6:3:1912
+7:3:1912
+8:3:1915
+9:3:1921
+10:3:1925
+11:3:1925
+12:3:1928
+13:3:1936
+14:3:1940
+15:3:1941
+16:0:1946
+17:3:1943
+18:0:1946
+19:2:416
+20:0:1946
+21:2:422
+22:0:1946
+23:2:423
+24:0:1946
+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:1946
+45:2:511
+46:0:1946
+47:2:513
+48:2:514
+49:0:1946
+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:1946
+69:2:605
+70:0:1946
+71:2:607
+72:0:1946
+73:2:608
+74:0:1946
+75:2:618
+76:0:1946
+77:2:619
+78:2:626
+79:2:627
+80:2:634
+81:2:639
+82:0:1946
+83:2:650
+84:0:1946
+85:2:651
+86:2:658
+87:2:659
+88:2:666
+89:2:671
+90:0:1946
+91:2:682
+92:0:1946
+93:2:687
+94:2:694
+95:2:695
+96:2:702
+97:2:707
+98:0:1946
+99:2:718
+100:0:1946
+101:2:720
+102:0:1946
+103:2:721
+104:2:725
+105:2:726
+106:2:734
+107:2:735
+108:2:739
+109:2:740
+110:2:748
+111:2:753
+112:2:757
+113:2:758
+114:2:765
+115:2:766
+116:2:777
+117:2:778
+118:2:779
+119:2:790
+120:2:795
+121:2:796
+122:0:1946
+123:2:808
+124:0:1946
+125:2:810
+126:0:1946
+127:2:813
+128:2:814
+129:2:826
+130:2:827
+131:2:831
+132:2:832
+133:2:840
+134:2:845
+135:2:849
+136:2:850
+137:2:857
+138:2:858
+139:2:869
+140:2:870
+141:2:871
+142:2:882
+143:2:887
+144:2:888
+145:0:1946
+146:2:900
+147:0:1946
+148:2:902
+149:0:1946
+150:2:903
+151:0:1946
+152:2:904
+153:0:1946
+154:2:905
+155:0:1946
+156:2:906
+157:2:910
+158:2:911
+159:2:919
+160:2:920
+161:2:924
+162:2:925
+163:2:933
+164:2:938
+165:2:942
+166:2:943
+167:2:950
+168:2:951
+169:2:962
+170:2:963
+171:2:964
+172:2:975
+173:2:980
+174:2:981
+175:0:1946
+176:2:993
+177:0:1946
+178:2:1097
+179:0:1946
+180:2:1195
+181:0:1946
+182:2:1196
+183:0:1946
+184:2:1200
+185:0:1946
+186:2:1206
+187:2:1210
+188:2:1211
+189:2:1219
+190:2:1220
+191:2:1224
+192:2:1225
+193:2:1233
+194:2:1238
+195:2:1242
+196:2:1243
+197:2:1250
+198:2:1251
+199:2:1262
+200:2:1263
+201:2:1264
+202:2:1275
+203:2:1280
+204:2:1281
+205:0:1946
+206:2:1293
+207:0:1946
+208:2:1295
+209:0:1946
+210:2:1296
+211:2:1300
+212:2:1301
+213:2:1309
+214:2:1310
+215:2:1314
+216:2:1315
+217:2:1323
+218:2:1328
+219:2:1332
+220:2:1333
+221:2:1340
+222:2:1341
+223:2:1352
+224:2:1353
+225:2:1354
+226:2:1365
+227:2:1370
+228:2:1371
+229:0:1946
+230:2:1383
+231:0:1946
+232:2:1385
+233:0:1946
+234:2:1388
+235:2:1389
+236:2:1401
+237:2:1402
+238:2:1406
+239:2:1407
+240:2:1415
+241:2:1420
+242:2:1424
+243:2:1425
+244:2:1432
+245:2:1433
+246:2:1444
+247:2:1445
+248:2:1446
+249:2:1457
+250:2:1462
+251:2:1463
+252:0:1946
+253:2:1475
+254:0:1946
+255:2:1477
+256:0:1946
+257:2:1478
+258:0:1946
+259:2:1479
+260:0:1946
+261:2:1480
+262:0:1946
+263:2:1481
+264:2:1485
+265:2:1486
+266:2:1494
+267:2:1495
+268:2:1499
+269:2:1500
+270:2:1508
+271:2:1513
+272:2:1517
+273:2:1518
+274:2:1525
+275:2:1526
+276:2:1537
+277:2:1538
+278:2:1539
+279:2:1550
+280:2:1555
+281:2:1556
+282:0:1946
+283:2:1568
+284:0:1946
+285:2:1672
+286:0:1946
+287:2:1770
+288:0:1946
+289:2:1771
+290:0:1946
+291:2:1775
+292:0:1946
+293:2:1781
+294:2:1788
+295:2:1789
+296:2:1796
+297:2:1801
+298:0:1946
+299:2:1812
+300:0:1946
+301:2:1813
+302:2:1820
+303:2:1821
+304:2:1828
+305:2:1833
+306:0:1946
+307:2:1844
+308:0:1946
+309:2:1849
+310:2:1856
+311:2:1857
+312:2:1864
+313:2:1869
+314:0:1946
+315:2:1880
+316:0:1946
+317:2:1882
+318:0:1946
+319:2:1883
+320:0:1946
+321:2:423
+322:0:1946
+323:2:424
+324:2:428
+325:2:429
+326:2:437
+327:2:438
+328:2:442
+329:2:443
+330:2:451
+331:2:456
+332:2:460
+333:2:461
+334:2:468
+335:2:469
+336:2:480
+337:2:481
+338:2:482
+339:2:493
+340:2:498
+341:2:499
+342:0:1946
+343:2:511
+344:0:1946
+345:2:513
+346:2:514
+347:0:1946
+348:2:518
+349:2:522
+350:2:523
+351:2:531
+352:2:532
+353:2:536
+354:2:537
+355:2:545
+356:2:550
+357:2:551
+358:2:562
+359:2:563
+360:2:574
+361:2:575
+362:2:576
+363:2:587
+364:2:592
+365:2:593
+366:0:1946
+367:2:605
+368:0:1946
+369:2:607
+370:0:1946
+371:2:608
+372:0:1946
+373:2:618
+374:0:1946
+375:2:619
+376:2:626
+377:2:627
+378:2:634
+379:2:639
+380:0:1946
+381:2:650
+382:0:1946
+383:2:651
+384:2:658
+385:2:659
+386:2:666
+387:2:671
+388:0:1946
+389:2:682
+390:0:1946
+391:2:687
+392:2:694
+393:2:695
+394:2:702
+395:2:707
+396:0:1946
+397:2:718
+398:0:1946
+399:2:720
+400:0:1946
+401:2:721
+402:2:725
+403:2:726
+404:2:734
+405:2:735
+406:2:739
+407:2:740
+408:2:748
+409:2:753
+410:2:757
+411:2:758
+412:2:765
+413:2:766
+414:2:777
+415:2:778
+416:2:779
+417:2:790
+418:2:795
+419:2:796
+420:0:1946
+421:2:808
+422:0:1946
+423:2:810
+424:0:1946
+425:2:813
+426:2:814
+427:2:826
+428:2:827
+429:2:831
+430:2:832
+431:2:840
+432:2:845
+433:2:849
+434:2:850
+435:2:857
+436:2:858
+437:2:869
+438:2:870
+439:2:871
+440:2:882
+441:2:887
+442:2:888
+443:0:1946
+444:2:900
+445:0:1946
+446:2:902
+447:0:1946
+448:2:903
+449:0:1946
+450:2:904
+451:0:1946
+452:2:905
+453:0:1946
+454:2:906
+455:2:910
+456:2:911
+457:2:919
+458:2:920
+459:2:924
+460:2:925
+461:2:933
+462:2:938
+463:2:942
+464:2:943
+465:2:950
+466:2:951
+467:2:962
+468:2:963
+469:2:964
+470:2:975
+471:2:980
+472:2:981
+473:0:1946
+474:2:993
+475:0:1946
+476:2:1097
+477:0:1946
+478:2:1195
+479:0:1946
+480:2:1196
+481:0:1946
+482:2:1200
+483:0:1946
+484:2:1206
+485:2:1210
+486:2:1211
+487:2:1219
+488:2:1220
+489:2:1224
+490:2:1225
+491:2:1233
+492:2:1238
+493:2:1242
+494:2:1243
+495:2:1250
+496:2:1251
+497:2:1262
+498:2:1263
+499:2:1264
+500:2:1275
+501:2:1280
+502:2:1281
+503:0:1946
+504:2:1293
+505:0:1946
+506:2:1295
+507:0:1946
+508:2:1296
+509:2:1300
+510:2:1301
+511:2:1309
+512:2:1310
+513:2:1314
+514:2:1315
+515:2:1323
+516:2:1328
+517:2:1332
+518:2:1333
+519:2:1340
+520:2:1341
+521:2:1352
+522:2:1353
+523:2:1354
+524:2:1365
+525:2:1370
+526:2:1371
+527:0:1946
+528:2:1383
+529:0:1946
+530:2:1385
+531:0:1946
+532:2:1388
+533:2:1389
+534:2:1401
+535:2:1402
+536:2:1406
+537:2:1407
+538:2:1415
+539:2:1420
+540:2:1424
+541:2:1425
+542:2:1432
+543:2:1433
+544:2:1444
+545:2:1445
+546:2:1446
+547:2:1457
+548:2:1462
+549:2:1463
+550:0:1946
+551:2:1475
+552:0:1946
+553:2:1477
+554:0:1946
+555:2:1478
+556:0:1946
+557:2:1479
+558:0:1946
+559:2:1480
+560:0:1946
+561:2:1481
+562:2:1485
+563:2:1486
+564:2:1494
+565:2:1495
+566:2:1499
+567:2:1500
+568:2:1508
+569:2:1513
+570:2:1517
+571:2:1518
+572:2:1525
+573:2:1526
+574:2:1537
+575:2:1538
+576:2:1539
+577:2:1550
+578:2:1555
+579:2:1556
+580:0:1946
+581:2:1568
+582:0:1946
+583:2:1672
+584:0:1946
+585:2:1770
+586:0:1946
+587:2:1771
+588:0:1946
+589:2:1775
+590:0:1946
+591:2:1781
+592:2:1788
+593:2:1789
+594:2:1796
+595:2:1801
+596:0:1946
+597:2:1812
+598:0:1946
+599:2:1813
+600:2:1820
+601:2:1821
+602:2:1828
+603:2:1833
+604:0:1946
+605:2:1844
+606:0:1946
+607:2:1849
+608:2:1856
+609:2:1857
+610:2:1864
+611:2:1869
+612:0:1946
+613:2:1880
+614:0:1946
+615:2:1882
+616:0:1946
+617:2:1883
+618:0:1946
+619:2:423
+620:0:1946
+621:2:424
+622:2:428
+623:2:429
+624:2:437
+625:2:438
+626:2:442
+627:2:443
+628:2:451
+629:2:456
+630:2:460
+631:2:461
+632:2:468
+633:2:469
+634:2:480
+635:2:481
+636:2:482
+637:2:493
+638:2:498
+639:2:499
+640:0:1946
+641:2:511
+642:0:1946
+643:2:513
+644:2:514
+645:0:1946
+646:2:518
+647:2:522
+648:2:523
+649:2:531
+650:2:532
+651:2:536
+652:2:537
+653:2:545
+654:2:550
+655:2:551
+656:2:562
+657:2:563
+658:2:574
+659:2:575
+660:2:576
+661:2:587
+662:2:592
+663:2:593
+664:0:1946
+665:2:605
+666:0:1946
+667:2:607
+668:0:1946
+669:2:608
+670:0:1946
+671:2:618
+672:0:1946
+673:2:619
+674:2:626
+675:2:627
+676:2:634
+677:2:639
+678:0:1946
+679:2:650
+680:0:1946
+681:2:651
+682:2:658
+683:2:659
+684:2:666
+685:2:671
+686:0:1946
+687:2:682
+688:0:1946
+689:2:687
+690:2:694
+691:2:695
+692:2:702
+693:2:707
+694:0:1946
+695:2:718
+696:0:1946
+697:2:720
+698:0:1946
+699:2:721
+700:2:725
+701:2:726
+702:2:734
+703:2:735
+704:2:739
+705:2:740
+706:2:748
+707:2:753
+708:2:757
+709:2:758
+710:2:765
+711:2:766
+712:2:777
+713:2:778
+714:2:779
+715:2:790
+716:2:795
+717:2:796
+718:0:1946
+719:2:808
+720:0:1946
+721:2:810
+722:0:1946
+723:2:813
+724:2:814
+725:2:826
+726:2:827
+727:2:831
+728:2:832
+729:2:840
+730:2:845
+731:2:849
+732:2:850
+733:2:857
+734:2:858
+735:2:869
+736:2:870
+737:2:871
+738:2:882
+739:2:887
+740:2:888
+741:0:1946
+742:2:900
+743:0:1946
+744:2:902
+745:0:1946
+746:2:903
+747:0:1946
+748:2:904
+749:0:1946
+750:2:905
+751:0:1946
+752:2:906
+753:2:910
+754:2:911
+755:2:919
+756:2:920
+757:2:924
+758:2:925
+759:2:933
+760:2:938
+761:2:942
+762:2:943
+763:2:950
+764:2:951
+765:2:962
+766:2:963
+767:2:964
+768:2:975
+769:2:980
+770:2:981
+771:0:1946
+772:2:993
+773:0:1946
+774:2:1097
+775:0:1946
+776:2:1195
+777:0:1946
+778:2:1196
+779:0:1946
+780:2:1200
+781:0:1946
+782:2:1206
+783:2:1210
+784:2:1211
+785:2:1219
+786:2:1220
+787:2:1224
+788:2:1225
+789:2:1233
+790:2:1238
+791:2:1242
+792:2:1243
+793:2:1250
+794:2:1251
+795:2:1262
+796:2:1263
+797:2:1264
+798:2:1275
+799:2:1280
+800:2:1281
+801:0:1946
+802:2:1293
+803:0:1946
+804:2:1295
+805:0:1946
+806:2:1296
+807:2:1300
+808:2:1301
+809:2:1309
+810:2:1310
+811:2:1314
+812:2:1315
+813:2:1323
+814:2:1328
+815:2:1332
+816:2:1333
+817:2:1340
+818:2:1341
+819:2:1352
+820:2:1353
+821:2:1354
+822:2:1365
+823:2:1370
+824:2:1371
+825:0:1946
+826:2:1383
+827:0:1946
+828:2:1385
+829:0:1946
+830:2:1388
+831:2:1389
+832:2:1401
+833:2:1402
+834:2:1406
+835:2:1407
+836:2:1415
+837:2:1420
+838:2:1424
+839:2:1425
+840:2:1432
+841:2:1433
+842:2:1444
+843:2:1445
+844:2:1446
+845:2:1457
+846:2:1462
+847:2:1463
+848:0:1946
+849:2:1475
+850:0:1946
+851:2:1477
+852:0:1946
+853:2:1478
+854:0:1946
+855:2:1479
+856:0:1946
+857:2:1480
+858:0:1946
+859:2:1481
+860:2:1485
+861:2:1486
+862:2:1494
+863:2:1495
+864:2:1499
+865:2:1500
+866:2:1508
+867:2:1513
+868:2:1517
+869:2:1518
+870:2:1525
+871:2:1526
+872:2:1537
+873:2:1538
+874:2:1539
+875:2:1550
+876:2:1555
+877:2:1556
+878:0:1946
+879:2:1568
+880:0:1946
+881:2:1672
+882:0:1946
+883:2:1770
+884:0:1946
+885:2:1771
+886:0:1946
+887:2:1775
+888:0:1946
+889:2:1781
+890:2:1788
+891:2:1789
+892:2:1796
+893:2:1801
+894:0:1946
+895:2:1812
+896:0:1946
+897:2:1813
+898:2:1820
+899:2:1821
+900:2:1828
+901:2:1833
+902:0:1946
+903:2:1844
+904:0:1946
+905:2:1849
+906:2:1856
+907:2:1857
+908:2:1864
+909:2:1869
+910:0:1946
+911:2:1880
+912:0:1946
+913:2:1882
+914:0:1946
+915:2:1883
+916:0:1946
+917:2:423
+918:0:1946
+919:2:424
+920:2:428
+921:2:429
+922:2:437
+923:2:438
+924:2:442
+925:2:443
+926:2:451
+927:2:456
+928:2:460
+929:2:461
+930:2:468
+931:2:469
+932:2:480
+933:2:481
+934:2:482
+935:2:493
+936:2:498
+937:2:499
+938:0:1946
+939:2:511
+940:0:1946
+941:2:513
+942:2:514
+943:0:1946
+944:2:518
+945:2:522
+946:2:523
+947:2:531
+948:2:532
+949:2:536
+950:2:537
+951:2:545
+952:2:550
+953:2:551
+954:2:562
+955:2:563
+956:2:574
+957:2:575
+958:2:576
+959:2:587
+960:2:592
+961:2:593
+962:0:1946
+963:2:605
+964:0:1946
+965:2:607
+966:0:1946
+967:2:608
+968:0:1946
+969:2:618
+970:0:1946
+971:2:619
+972:2:626
+973:2:627
+974:2:634
+975:2:639
+976:0:1946
+977:2:650
+978:0:1946
+979:2:651
+980:2:658
+981:2:659
+982:2:666
+983:2:671
+984:0:1946
+985:2:682
+986:0:1946
+987:2:687
+988:2:694
+989:2:695
+990:2:702
+991:2:707
+992:0:1946
+993:2:718
+994:0:1946
+995:2:720
+996:0:1946
+997:2:721
+998:2:725
+999:2:726
+1000:2:734
+1001:2:735
+1002:2:739
+1003:2:740
+1004:2:748
+1005:2:753
+1006:2:757
+1007:2:758
+1008:2:765
+1009:2:766
+1010:2:777
+1011:2:778
+1012:2:779
+1013:2:790
+1014:2:795
+1015:2:796
+1016:0:1946
+1017:2:808
+1018:0:1946
+1019:2:810
+1020:0:1946
+1021:2:813
+1022:2:814
+1023:2:826
+1024:2:827
+1025:2:831
+1026:2:832
+1027:2:840
+1028:2:845
+1029:2:849
+1030:2:850
+1031:2:857
+1032:2:858
+1033:2:869
+1034:2:870
+1035:2:871
+1036:2:882
+1037:2:887
+1038:2:888
+1039:0:1946
+1040:2:900
+1041:0:1946
+1042:2:902
+1043:0:1946
+1044:2:903
+1045:0:1946
+1046:2:904
+1047:0:1946
+1048:2:905
+1049:0:1946
+1050:2:906
+1051:2:910
+1052:2:911
+1053:2:919
+1054:2:920
+1055:2:924
+1056:2:925
+1057:2:933
+1058:2:938
+1059:2:942
+1060:2:943
+1061:2:950
+1062:2:951
+1063:2:962
+1064:2:963
+1065:2:964
+1066:2:975
+1067:2:980
+1068:2:981
+1069:0:1946
+1070:2:993
+1071:0:1946
+1072:2:1097
+1073:0:1946
+1074:2:1195
+1075:0:1946
+1076:2:1196
+1077:0:1946
+1078:2:1200
+1079:0:1946
+1080:2:1206
+1081:2:1210
+1082:2:1211
+1083:2:1219
+1084:2:1220
+1085:2:1224
+1086:2:1225
+1087:2:1233
+1088:2:1238
+1089:2:1242
+1090:2:1243
+1091:2:1250
+1092:2:1251
+1093:2:1262
+1094:2:1263
+1095:2:1264
+1096:2:1275
+1097:2:1280
+1098:2:1281
+1099:0:1946
+1100:2:1293
+1101:0:1946
+1102:2:1295
+1103:0:1946
+1104:2:1296
+1105:2:1300
+1106:2:1301
+1107:2:1309
+1108:2:1310
+1109:2:1314
+1110:2:1315
+1111:2:1323
+1112:2:1328
+1113:2:1332
+1114:2:1333
+1115:2:1340
+1116:2:1341
+1117:2:1352
+1118:2:1353
+1119:2:1354
+1120:2:1365
+1121:2:1370
+1122:2:1371
+1123:0:1946
+1124:2:1383
+1125:0:1946
+1126:2:1385
+1127:0:1946
+1128:2:1388
+1129:2:1389
+1130:2:1401
+1131:2:1402
+1132:2:1406
+1133:2:1407
+1134:2:1415
+1135:2:1420
+1136:2:1424
+1137:2:1425
+1138:2:1432
+1139:2:1433
+1140:2:1444
+1141:2:1445
+1142:2:1446
+1143:2:1457
+1144:2:1462
+1145:2:1463
+1146:0:1946
+1147:2:1475
+1148:0:1946
+1149:2:1477
+1150:0:1946
+1151:2:1478
+1152:0:1946
+1153:2:1479
+1154:0:1946
+1155:2:1480
+1156:0:1946
+1157:2:1481
+1158:2:1485
+1159:2:1486
+1160:2:1494
+1161:2:1495
+1162:2:1499
+1163:2:1500
+1164:2:1508
+1165:2:1513
+1166:2:1517
+1167:2:1518
+1168:2:1525
+1169:2:1526
+1170:2:1537
+1171:2:1538
+1172:2:1539
+1173:2:1550
+1174:2:1555
+1175:2:1556
+1176:0:1946
+1177:2:1568
+1178:0:1946
+1179:2:1672
+1180:0:1946
+1181:2:1770
+1182:0:1946
+1183:2:1771
+1184:0:1946
+1185:2:1775
+1186:0:1946
+1187:2:1781
+1188:2:1788
+1189:2:1789
+1190:2:1796
+1191:2:1801
+1192:0:1946
+1193:2:1812
+1194:0:1946
+1195:2:1813
+1196:2:1820
+1197:2:1821
+1198:2:1828
+1199:2:1833
+1200:0:1946
+1201:2:1844
+1202:0:1946
+1203:2:1849
+1204:2:1856
+1205:2:1857
+1206:2:1864
+1207:2:1869
+1208:0:1946
+1209:2:1880
+1210:0:1946
+1211:2:1882
+1212:0:1946
+1213:2:1883
+1214:0:1946
+1215:2:423
+1216:0:1946
+1217:2:424
+1218:2:428
+1219:2:429
+1220:2:437
+1221:2:438
+1222:2:442
+1223:2:443
+1224:2:451
+1225:2:456
+1226:2:460
+1227:2:461
+1228:2:468
+1229:2:469
+1230:2:480
+1231:2:481
+1232:2:482
+1233:2:493
+1234:2:498
+1235:2:499
+1236:0:1946
+1237:2:511
+1238:0:1946
+1239:2:513
+1240:2:514
+1241:0:1946
+1242:2:518
+1243:2:522
+1244:2:523
+1245:2:531
+1246:2:532
+1247:2:536
+1248:2:537
+1249:2:545
+1250:2:550
+1251:2:551
+1252:2:562
+1253:2:563
+1254:2:574
+1255:2:575
+1256:2:576
+1257:2:587
+1258:2:592
+1259:2:593
+1260:0:1946
+1261:2:605
+1262:0:1946
+1263:2:607
+1264:0:1946
+1265:2:608
+1266:0:1946
+1267:2:618
+1268:0:1946
+1269:2:619
+1270:2:626
+1271:2:627
+1272:2:634
+1273:2:639
+1274:0:1946
+1275:2:650
+1276:0:1946
+1277:1:2
+1278:0:1946
+1279:1:8
+1280:0:1946
+1281:1:9
+1282:0:1946
+1283:1:10
+1284:0:1946
+1285:1:11
+1286:0:1946
+1287:1:12
+1288:1:16
+1289:1:17
+1290:1:25
+1291:1:26
+1292:1:30
+1293:1:31
+1294:1:39
+1295:1:44
+1296:1:48
+1297:1:49
+1298:1:56
+1299:1:57
+1300:1:68
+1301:1:69
+1302:1:70
+1303:1:81
+1304:1:93
+1305:1:94
+1306:0:1946
+1307:1:99
+1308:0:1946
+1309:1:101
+1310:0:1946
+1311:1:102
+1312:1:106
+1313:1:107
+1314:1:115
+1315:1:116
+1316:1:120
+1317:1:121
+1318:1:129
+1319:1:134
+1320:1:138
+1321:1:139
+1322:1:146
+1323:1:147
+1324:1:158
+1325:1:159
+1326:1:160
+1327:1:171
+1328:1:183
+1329:1:184
+1330:0:1946
+1331:1:189
+1332:0:1946
+1333:1:191
+1334:0:1946
+1335:1:192
+1336:0:1946
+1337:1:193
+1338:1:197
+1339:1:198
+1340:1:206
+1341:1:207
+1342:1:211
+1343:1:212
+1344:1:220
+1345:1:225
+1346:1:229
+1347:1:230
+1348:1:237
+1349:1:238
+1350:1:249
+1351:1:250
+1352:1:251
+1353:1:262
+1354:1:274
+1355:1:275
+1356:0:1946
+1357:1:280
+1358:0:1946
+1359:1:282
+1360:0:1946
+1361:1:291
+1362:0:1946
+1363:1:293
+1364:0:1946
+1365:1:296
+1366:0:1946
+1367:1:301
+1368:0:1946
+1369:2:651
+1370:2:658
+1371:2:661
+1372:2:662
+1373:2:666
+1374:2:671
+1375:0:1946
+1376:2:682
+1377:0:1946
+1378:2:687
+1379:2:694
+1380:2:695
+1381:2:702
+1382:2:707
+1383:0:1946
+1384:2:718
+1385:0:1946
+1386:2:720
+1387:0:1946
+1388:2:721
+1389:2:725
+1390:2:726
+1391:2:734
+1392:2:735
+1393:2:739
+1394:2:740
+1395:2:748
+1396:2:753
+1397:2:757
+1398:2:758
+1399:2:765
+1400:2:766
+1401:2:777
+1402:2:778
+1403:2:779
+1404:2:790
+1405:2:795
+1406:2:796
+1407:0:1946
+1408:2:808
+1409:0:1946
+1410:2:810
+1411:0:1946
+1412:2:813
+1413:2:814
+1414:2:826
+1415:2:827
+1416:2:831
+1417:2:832
+1418:2:840
+1419:2:845
+1420:2:849
+1421:2:850
+1422:2:857
+1423:2:858
+1424:2:869
+1425:2:870
+1426:2:871
+1427:2:882
+1428:2:887
+1429:2:888
+1430:0:1946
+1431:2:900
+1432:0:1946
+1433:2:902
+1434:0:1946
+1435:2:903
+1436:0:1946
+1437:2:904
+1438:0:1946
+1439:2:905
+1440:0:1946
+1441:2:906
+1442:2:910
+1443:2:911
+1444:2:919
+1445:2:920
+1446:2:924
+1447:2:925
+1448:2:933
+1449:2:938
+1450:2:942
+1451:2:943
+1452:2:950
+1453:2:951
+1454:2:962
+1455:2:963
+1456:2:964
+1457:2:975
+1458:2:980
+1459:2:981
+1460:0:1946
+1461:2:993
+1462:0:1946
+1463:2:1097
+1464:0:1946
+1465:2:1195
+1466:0:1946
+1467:2:1196
+1468:0:1946
+1469:2:1200
+1470:0:1946
+1471:2:1206
+1472:2:1210
+1473:2:1211
+1474:2:1219
+1475:2:1220
+1476:2:1224
+1477:2:1225
+1478:2:1233
+1479:2:1238
+1480:2:1242
+1481:2:1243
+1482:2:1250
+1483:2:1251
+1484:2:1262
+1485:2:1263
+1486:2:1264
+1487:2:1275
+1488:2:1280
+1489:2:1281
+1490:0:1946
+1491:2:1293
+1492:0:1946
+1493:2:1295
+1494:0:1946
+1495:2:1296
+1496:2:1300
+1497:2:1301
+1498:2:1309
+1499:2:1310
+1500:2:1314
+1501:2:1315
+1502:2:1323
+1503:2:1328
+1504:2:1332
+1505:2:1333
+1506:2:1340
+1507:2:1341
+1508:2:1352
+1509:2:1353
+1510:2:1354
+1511:2:1365
+1512:2:1370
+1513:2:1371
+1514:0:1946
+1515:2:1383
+1516:0:1946
+1517:2:1385
+1518:0:1946
+1519:2:1388
+1520:2:1389
+1521:2:1401
+1522:2:1402
+1523:2:1406
+1524:2:1407
+1525:2:1415
+1526:2:1420
+1527:2:1424
+1528:2:1425
+1529:2:1432
+1530:2:1433
+1531:2:1444
+1532:2:1445
+1533:2:1446
+1534:2:1457
+1535:2:1462
+1536:2:1463
+1537:0:1946
+1538:2:1475
+1539:0:1946
+1540:2:1477
+1541:0:1946
+1542:2:1478
+1543:0:1946
+1544:2:1479
+1545:0:1946
+1546:2:1480
+1547:0:1946
+1548:2:1481
+1549:2:1485
+1550:2:1486
+1551:2:1494
+1552:2:1495
+1553:2:1499
+1554:2:1500
+1555:2:1508
+1556:2:1513
+1557:2:1517
+1558:2:1518
+1559:2:1525
+1560:2:1526
+1561:2:1537
+1562:2:1538
+1563:2:1539
+1564:2:1550
+1565:2:1555
+1566:2:1556
+1567:0:1946
+1568:2:1568
+1569:0:1946
+1570:2:1672
+1571:0:1946
+1572:2:1770
+1573:0:1946
+1574:2:1771
+1575:0:1946
+1576:2:1775
+1577:0:1946
+1578:2:1781
+1579:2:1788
+1580:2:1789
+1581:2:1796
+1582:2:1801
+1583:0:1946
+1584:2:1812
+1585:0:1946
+1586:2:1813
+1587:2:1820
+1588:2:1823
+1589:2:1824
+1590:2:1828
+1591:2:1833
+1592:0:1946
+1593:2:1844
+1594:0:1946
+1595:2:1849
+1596:2:1856
+1597:2:1857
+1598:2:1864
+1599:2:1869
+1600:0:1946
+1601:2:1880
+1602:0:1946
+1603:2:1882
+1604:0:1946
+1605:2:1883
+1606:0:1946
+1607:2:1886
+1608:0:1946
+1609:2:1891
+1610:0:1946
+1611:1:302
+1612:0:1944
+1613:2:1892
+1614:0:1950
+1615:1:244