Add nosched model results (for signal readers)

[urcu.git] / formal-model / urcu-nosched-model / result-signal-over-writer / testmerge / urcu_free.spin.input.trail

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