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

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