X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-nosched-model%2Fresult-signal-over-writer%2Ftestmerge%2Furcu_free_no_mb.spin.input.trail;fp=formal-model%2Furcu-nosched-model%2Fresult-signal-over-writer%2Ftestmerge%2Furcu_free_no_mb.spin.input.trail;h=3d2a95edcf089970f69f6a0fe0ac51b9fee73363;hp=0000000000000000000000000000000000000000;hb=06e8b2a87f862183a26e0005bf04221633f49d0c;hpb=8322221dc666e720badeb06bc780a1f8e69020a0

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