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

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