Add nosched model results (for signal readers)

[urcu.git] / formal-model / urcu-nosched-model / result-signal-over-reader / urcu_free_no_wmb.spin.input.trail

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