Add nosched model results (for signal readers)

[urcu.git] / formal-model / urcu-nosched-model / result-standard-execution-nest / urcu_free_no_wmb.spin.input.trail

diff --git a/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_wmb.spin.input.trail b/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_wmb.spin.input.trail
new file mode 100644 (file)
index 0000000..f73a838
--- /dev/null
+++ b/formal-model/urcu-nosched-model/result-standard-execution-nest/urcu_free_no_wmb.spin.input.trail
@@ -0,0 +1,1885 @@
+-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:11
+1366:0:1946
+1367:1:12
+1368:1:16
+1369:1:17
+1370:1:25
+1371:1:26
+1372:1:27
+1373:1:39
+1374:1:44
+1375:1:48
+1376:1:49
+1377:1:56
+1378:1:57
+1379:1:68
+1380:1:69
+1381:1:70
+1382:1:81
+1383:1:93
+1384:1:94
+1385:0:1946
+1386:1:99
+1387:0:1946
+1388:1:101
+1389:0:1946
+1390:1:102
+1391:1:106
+1392:1:107
+1393:1:115
+1394:1:116
+1395:1:120
+1396:1:121
+1397:1:129
+1398:1:134
+1399:1:138
+1400:1:139
+1401:1:146
+1402:1:147
+1403:1:158
+1404:1:159
+1405:1:160
+1406:1:171
+1407:1:183
+1408:1:184
+1409:0:1946
+1410:1:189
+1411:0:1946
+1412:1:285
+1413:0:1946
+1414:1:286
+1415:0:1946
+1416:1:291
+1417:0:1946
+1418:1:293
+1419:0:1946
+1420:1:296
+1421:0:1946
+1422:1:301
+1423:0:1946
+1424:1:302
+1425:0:1946
+1426:1:303
+1427:0:1946
+1428:1:304
+1429:0:1946
+1430:1:305
+1431:0:1946
+1432:1:306
+1433:0:1946
+1434:1:308
+1435:0:1946
+1436:1:310
+1437:0:1946
+1438:1:311
+1439:1:315
+1440:1:316
+1441:1:324
+1442:1:325
+1443:1:326
+1444:1:338
+1445:1:343
+1446:1:347
+1447:1:348
+1448:1:355
+1449:1:356
+1450:1:367
+1451:1:368
+1452:1:369
+1453:1:380
+1454:1:392
+1455:1:393
+1456:0:1946
+1457:1:398
+1458:0:1946
+1459:1:400
+1460:0:1946
+1461:1:305
+1462:0:1946
+1463:1:306
+1464:0:1946
+1465:1:308
+1466:0:1946
+1467:1:310
+1468:0:1946
+1469:1:311
+1470:1:315
+1471:1:316
+1472:1:324
+1473:1:325
+1474:1:326
+1475:1:338
+1476:1:343
+1477:1:347
+1478:1:348
+1479:1:355
+1480:1:356
+1481:1:367
+1482:1:368
+1483:1:369
+1484:1:380
+1485:1:392
+1486:1:393
+1487:0:1946
+1488:1:398
+1489:0:1946
+1490:1:400
+1491:0:1946
+1492:1:404
+1493:0:1946
+1494:1:9
+1495:0:1946
+1496:1:10
+1497:0:1946
+1498:1:11
+1499:0:1946
+1500:1:12
+1501:1:16
+1502:1:17
+1503:1:25
+1504:1:26
+1505:1:27
+1506:1:39
+1507:1:44
+1508:1:48
+1509:1:49
+1510:1:56
+1511:1:57
+1512:1:68
+1513:1:69
+1514:1:70
+1515:1:81
+1516:1:93
+1517:1:94
+1518:0:1946
+1519:1:99
+1520:0:1946
+1521:1:101
+1522:0:1946
+1523:1:102
+1524:1:106
+1525:1:107
+1526:1:115
+1527:1:116
+1528:1:120
+1529:1:121
+1530:1:129
+1531:1:134
+1532:1:138
+1533:1:139
+1534:1:146
+1535:1:147
+1536:1:158
+1537:1:159
+1538:1:160
+1539:1:171
+1540:1:183
+1541:1:184
+1542:0:1946
+1543:1:189
+1544:0:1946
+1545:1:191
+1546:0:1946
+1547:1:192
+1548:0:1946
+1549:1:193
+1550:1:197
+1551:1:198
+1552:1:206
+1553:1:207
+1554:1:211
+1555:1:212
+1556:1:220
+1557:1:225
+1558:1:229
+1559:1:230
+1560:1:237
+1561:1:238
+1562:1:249
+1563:1:250
+1564:1:251
+1565:1:262
+1566:1:274
+1567:1:275
+1568:0:1946
+1569:1:280
+1570:0:1946
+1571:1:282
+1572:0:1946
+1573:1:291
+1574:0:1946
+1575:1:293
+1576:0:1946
+1577:1:11
+1578:0:1946
+1579:1:12
+1580:1:16
+1581:1:17
+1582:1:25
+1583:1:34
+1584:1:35
+1585:1:39
+1586:1:44
+1587:1:48
+1588:1:49
+1589:1:56
+1590:1:57
+1591:1:68
+1592:1:69
+1593:1:72
+1594:1:73
+1595:1:81
+1596:1:93
+1597:1:94
+1598:0:1946
+1599:1:99
+1600:0:1946
+1601:1:101
+1602:0:1946
+1603:1:102
+1604:1:106
+1605:1:107
+1606:1:115
+1607:1:124
+1608:1:125
+1609:1:129
+1610:1:134
+1611:1:138
+1612:1:139
+1613:1:146
+1614:1:147
+1615:1:158
+1616:1:159
+1617:1:162
+1618:1:163
+1619:1:171
+1620:1:183
+1621:1:184
+1622:0:1946
+1623:1:189
+1624:0:1946
+1625:1:285
+1626:0:1946
+1627:1:286
+1628:0:1946
+1629:1:291
+1630:0:1946
+1631:1:293
+1632:0:1946
+1633:1:296
+1634:0:1946
+1635:1:301
+1636:0:1946
+1637:2:651
+1638:2:658
+1639:2:661
+1640:2:662
+1641:2:666
+1642:2:671
+1643:0:1946
+1644:2:682
+1645:0:1946
+1646:2:687
+1647:2:694
+1648:2:695
+1649:2:702
+1650:2:707
+1651:0:1946
+1652:2:718
+1653:0:1946
+1654:2:720
+1655:0:1946
+1656:2:721
+1657:2:725
+1658:2:726
+1659:2:734
+1660:2:735
+1661:2:739
+1662:2:740
+1663:2:748
+1664:2:753
+1665:2:757
+1666:2:758
+1667:2:765
+1668:2:766
+1669:2:777
+1670:2:778
+1671:2:779
+1672:2:790
+1673:2:795
+1674:2:796
+1675:0:1946
+1676:2:808
+1677:0:1946
+1678:2:810
+1679:0:1946
+1680:2:813
+1681:2:814
+1682:2:826
+1683:2:827
+1684:2:831
+1685:2:832
+1686:2:840
+1687:2:845
+1688:2:849
+1689:2:850
+1690:2:857
+1691:2:858
+1692:2:869
+1693:2:870
+1694:2:871
+1695:2:882
+1696:2:887
+1697:2:888
+1698:0:1946
+1699:2:900
+1700:0:1946
+1701:2:902
+1702:0:1946
+1703:2:903
+1704:0:1946
+1705:2:904
+1706:0:1946
+1707:2:905
+1708:0:1946
+1709:2:906
+1710:2:910
+1711:2:911
+1712:2:919
+1713:2:920
+1714:2:924
+1715:2:925
+1716:2:933
+1717:2:938
+1718:2:942
+1719:2:943
+1720:2:950
+1721:2:951
+1722:2:962
+1723:2:963
+1724:2:964
+1725:2:975
+1726:2:980
+1727:2:981
+1728:0:1946
+1729:2:993
+1730:0:1946
+1731:2:1097
+1732:0:1946
+1733:2:1195
+1734:0:1946
+1735:2:1196
+1736:0:1946
+1737:2:1200
+1738:0:1946
+1739:2:1206
+1740:2:1210
+1741:2:1211
+1742:2:1219
+1743:2:1220
+1744:2:1224
+1745:2:1225
+1746:2:1233
+1747:2:1238
+1748:2:1242
+1749:2:1243
+1750:2:1250
+1751:2:1251
+1752:2:1262
+1753:2:1263
+1754:2:1264
+1755:2:1275
+1756:2:1280
+1757:2:1281
+1758:0:1946
+1759:2:1293
+1760:0:1946
+1761:2:1295
+1762:0:1946
+1763:2:1296
+1764:2:1300
+1765:2:1301
+1766:2:1309
+1767:2:1310
+1768:2:1314
+1769:2:1315
+1770:2:1323
+1771:2:1328
+1772:2:1332
+1773:2:1333
+1774:2:1340
+1775:2:1341
+1776:2:1352
+1777:2:1353
+1778:2:1354
+1779:2:1365
+1780:2:1370
+1781:2:1371
+1782:0:1946
+1783:2:1383
+1784:0:1946
+1785:2:1385
+1786:0:1946
+1787:2:1388
+1788:2:1389
+1789:2:1401
+1790:2:1402
+1791:2:1406
+1792:2:1407
+1793:2:1415
+1794:2:1420
+1795:2:1424
+1796:2:1425
+1797:2:1432
+1798:2:1433
+1799:2:1444
+1800:2:1445
+1801:2:1446
+1802:2:1457
+1803:2:1462
+1804:2:1463
+1805:0:1946
+1806:2:1475
+1807:0:1946
+1808:2:1477
+1809:0:1946
+1810:2:1478
+1811:0:1946
+1812:2:1479
+1813:0:1946
+1814:2:1480
+1815:0:1946
+1816:2:1481
+1817:2:1485
+1818:2:1486
+1819:2:1494
+1820:2:1495
+1821:2:1499
+1822:2:1500
+1823:2:1508
+1824:2:1513
+1825:2:1517
+1826:2:1518
+1827:2:1525
+1828:2:1526
+1829:2:1537
+1830:2:1538
+1831:2:1539
+1832:2:1550
+1833:2:1555
+1834:2:1556
+1835:0:1946
+1836:2:1568
+1837:0:1946
+1838:2:1672
+1839:0:1946
+1840:2:1770
+1841:0:1946
+1842:2:1771
+1843:0:1946
+1844:2:1775
+1845:0:1946
+1846:2:1781
+1847:2:1788
+1848:2:1789
+1849:2:1796
+1850:2:1801
+1851:0:1946
+1852:2:1812
+1853:0:1946
+1854:2:1813
+1855:2:1820
+1856:2:1823
+1857:2:1824
+1858:2:1828
+1859:2:1833
+1860:0:1946
+1861:2:1844
+1862:0:1946
+1863:2:1849
+1864:2:1856
+1865:2:1857
+1866:2:1864
+1867:2:1869
+1868:0:1946
+1869:2:1880
+1870:0:1946
+1871:2:1882
+1872:0:1946
+1873:2:1883
+1874:0:1946
+1875:2:1886
+1876:0:1946
+1877:2:1891
+1878:0:1946
+1879:1:302
+1880:0:1944
+1881:2:1892
+1882:0:1950
+1883:1:143