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

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