X-Git-Url: https://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu%2Fresult-signal-over-writer%2Ftestmerge%2Furcu_free_no_rmb.spin.input.trail;fp=formal-model%2Furcu%2Fresult-signal-over-writer%2Ftestmerge%2Furcu_free_no_rmb.spin.input.trail;h=0aacf1a8c35d7e4c66dc42a230caa5f1ff1c3187;hb=8baf2c9506f8e4bbac913c7ea2a8b2e9a3cd0932;hp=0000000000000000000000000000000000000000;hpb=fa5b67244cb2c3733d2c0195d3ad239d97ec2dc3;p=urcu.git

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