Add verif results

[urcu.git] / formal-model / urcu-controldataflow-alpha-ipi-progress-minimal / urcu_free_no_mb.spin.input.trail

diff --git a/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_mb.spin.input.trail b/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_mb.spin.input.trail
new file mode 100644 (file)
index 0000000..37c6ecd
--- /dev/null
+++ b/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,1249 @@
+-2:3:-2
+-4:-4:-4
+1:0:2890
+2:2:1138
+3:2:1143
+4:2:1147
+5:2:1155
+6:2:1159
+7:2:1163
+8:0:2890
+9:1:0
+10:1:5
+11:1:9
+12:1:17
+13:1:21
+14:1:25
+15:0:2890
+16:3:2862
+17:3:2865
+18:3:2870
+19:3:2877
+20:3:2880
+21:3:2884
+22:3:2885
+23:0:2890
+24:3:2887
+25:0:2890
+26:2:1167
+27:0:2890
+28:2:1173
+29:0:2890
+30:2:1174
+31:0:2890
+32:2:1176
+33:0:2890
+34:2:1177
+35:0:2890
+36:2:1178
+37:0:2890
+38:2:1179
+39:0:2890
+40:2:1180
+41:2:1181
+42:2:1185
+43:2:1186
+44:2:1194
+45:2:1195
+46:2:1199
+47:2:1200
+48:2:1208
+49:2:1213
+50:2:1217
+51:2:1218
+52:2:1226
+53:2:1227
+54:2:1231
+55:2:1232
+56:2:1226
+57:2:1227
+58:2:1231
+59:2:1232
+60:2:1240
+61:2:1245
+62:2:1246
+63:2:1257
+64:2:1258
+65:2:1259
+66:2:1270
+67:2:1275
+68:2:1276
+69:2:1287
+70:2:1288
+71:2:1289
+72:2:1287
+73:2:1288
+74:2:1289
+75:2:1300
+76:2:1308
+77:0:2890
+78:2:1179
+79:0:2890
+80:2:1312
+81:2:1316
+82:2:1317
+83:2:1321
+84:2:1325
+85:2:1326
+86:2:1330
+87:2:1338
+88:2:1339
+89:2:1343
+90:2:1347
+91:2:1348
+92:2:1343
+93:2:1344
+94:2:1352
+95:0:2890
+96:2:1179
+97:0:2890
+98:2:1360
+99:2:1361
+100:2:1362
+101:0:2890
+102:2:1179
+103:0:2890
+104:2:1370
+105:0:2890
+106:2:1179
+107:0:2890
+108:2:1373
+109:2:1374
+110:2:1378
+111:2:1379
+112:2:1387
+113:2:1388
+114:2:1392
+115:2:1393
+116:2:1401
+117:2:1406
+118:2:1407
+119:2:1419
+120:2:1420
+121:2:1424
+122:2:1425
+123:2:1419
+124:2:1420
+125:2:1424
+126:2:1425
+127:2:1433
+128:2:1438
+129:2:1439
+130:2:1450
+131:2:1451
+132:2:1452
+133:2:1463
+134:2:1468
+135:2:1469
+136:2:1480
+137:2:1481
+138:2:1482
+139:2:1480
+140:2:1481
+141:2:1482
+142:2:1493
+143:2:1500
+144:0:2890
+145:2:1179
+146:0:2890
+147:2:1504
+148:2:1505
+149:2:1506
+150:2:1518
+151:2:1519
+152:2:1523
+153:2:1524
+154:2:1532
+155:2:1537
+156:2:1541
+157:2:1542
+158:2:1550
+159:2:1551
+160:2:1555
+161:2:1556
+162:2:1550
+163:2:1551
+164:2:1555
+165:2:1556
+166:2:1564
+167:2:1569
+168:2:1570
+169:2:1581
+170:2:1582
+171:2:1583
+172:2:1594
+173:2:1599
+174:2:1600
+175:2:1611
+176:2:1612
+177:2:1613
+178:2:1611
+179:2:1612
+180:2:1613
+181:2:1624
+182:2:1635
+183:2:1636
+184:0:2890
+185:2:1179
+186:0:2890
+187:2:1643
+188:2:1644
+189:2:1648
+190:2:1649
+191:2:1657
+192:2:1658
+193:2:1662
+194:2:1663
+195:2:1671
+196:2:1676
+197:2:1680
+198:2:1681
+199:2:1689
+200:2:1690
+201:2:1694
+202:2:1695
+203:2:1689
+204:2:1690
+205:2:1694
+206:2:1695
+207:2:1703
+208:2:1708
+209:2:1709
+210:2:1720
+211:2:1721
+212:2:1722
+213:2:1733
+214:2:1738
+215:2:1739
+216:2:1750
+217:2:1751
+218:2:1752
+219:2:1750
+220:2:1751
+221:2:1752
+222:2:1763
+223:0:2890
+224:2:1179
+225:0:2890
+226:2:1772
+227:2:1773
+228:2:1777
+229:2:1778
+230:2:1786
+231:2:1787
+232:2:1791
+233:2:1792
+234:2:1800
+235:2:1805
+236:2:1809
+237:2:1810
+238:2:1818
+239:2:1819
+240:2:1823
+241:2:1824
+242:2:1818
+243:2:1819
+244:2:1823
+245:2:1824
+246:2:1832
+247:2:1837
+248:2:1838
+249:2:1849
+250:2:1850
+251:2:1851
+252:2:1862
+253:2:1867
+254:2:1868
+255:2:1879
+256:2:1880
+257:2:1881
+258:2:1879
+259:2:1880
+260:2:1881
+261:2:1892
+262:2:1899
+263:0:2890
+264:2:1179
+265:0:2890
+266:2:1903
+267:2:1904
+268:2:1905
+269:2:1917
+270:2:1918
+271:2:1922
+272:2:1923
+273:2:1931
+274:2:1936
+275:2:1940
+276:2:1941
+277:2:1949
+278:2:1950
+279:2:1954
+280:2:1955
+281:2:1949
+282:2:1950
+283:2:1954
+284:2:1955
+285:2:1963
+286:2:1968
+287:2:1969
+288:2:1980
+289:2:1981
+290:2:1982
+291:2:1993
+292:2:1998
+293:2:1999
+294:2:2010
+295:2:2011
+296:2:2012
+297:2:2010
+298:2:2011
+299:2:2012
+300:2:2023
+301:2:2033
+302:2:2034
+303:0:2890
+304:2:1179
+305:0:2890
+306:2:2043
+307:2:2044
+308:0:2890
+309:2:1179
+310:0:2890
+311:2:2048
+312:0:2890
+313:2:2056
+314:0:2890
+315:2:1174
+316:0:2890
+317:2:1176
+318:0:2890
+319:2:1177
+320:0:2890
+321:2:1178
+322:0:2890
+323:2:1179
+324:0:2890
+325:2:1180
+326:2:1181
+327:2:1185
+328:2:1186
+329:2:1194
+330:2:1195
+331:2:1199
+332:2:1200
+333:2:1208
+334:2:1213
+335:2:1217
+336:2:1218
+337:2:1226
+338:2:1227
+339:2:1228
+340:2:1226
+341:2:1227
+342:2:1231
+343:2:1232
+344:2:1240
+345:2:1245
+346:2:1246
+347:2:1257
+348:2:1258
+349:2:1259
+350:2:1270
+351:2:1275
+352:2:1276
+353:2:1287
+354:2:1288
+355:2:1289
+356:2:1287
+357:2:1288
+358:2:1289
+359:2:1300
+360:2:1308
+361:0:2890
+362:2:1179
+363:0:2890
+364:2:1312
+365:2:1316
+366:2:1317
+367:2:1321
+368:2:1325
+369:2:1326
+370:2:1330
+371:2:1338
+372:2:1339
+373:2:1343
+374:2:1344
+375:2:1343
+376:2:1347
+377:2:1348
+378:2:1352
+379:0:2890
+380:2:1179
+381:0:2890
+382:2:1360
+383:2:1361
+384:2:1362
+385:0:2890
+386:2:1179
+387:0:2890
+388:2:1370
+389:0:2890
+390:2:1179
+391:0:2890
+392:2:1373
+393:2:1374
+394:2:1378
+395:2:1379
+396:2:1387
+397:2:1388
+398:2:1392
+399:2:1393
+400:2:1401
+401:2:1406
+402:2:1407
+403:2:1419
+404:2:1420
+405:2:1424
+406:2:1425
+407:2:1419
+408:2:1420
+409:2:1424
+410:2:1425
+411:2:1433
+412:2:1438
+413:2:1439
+414:2:1450
+415:2:1451
+416:2:1452
+417:2:1463
+418:2:1468
+419:2:1469
+420:2:1480
+421:2:1481
+422:2:1482
+423:2:1480
+424:2:1481
+425:2:1482
+426:2:1493
+427:2:1500
+428:0:2890
+429:2:1179
+430:0:2890
+431:2:1504
+432:2:1505
+433:2:1506
+434:2:1518
+435:2:1519
+436:2:1523
+437:2:1524
+438:2:1532
+439:2:1537
+440:2:1541
+441:2:1542
+442:2:1550
+443:2:1551
+444:2:1555
+445:2:1556
+446:2:1550
+447:2:1551
+448:2:1555
+449:2:1556
+450:2:1564
+451:2:1569
+452:2:1570
+453:2:1581
+454:2:1582
+455:2:1583
+456:2:1594
+457:2:1599
+458:2:1600
+459:2:1611
+460:2:1612
+461:2:1613
+462:2:1611
+463:2:1612
+464:2:1613
+465:2:1624
+466:2:1635
+467:2:1636
+468:0:2890
+469:2:1179
+470:0:2890
+471:2:1643
+472:2:1644
+473:2:1648
+474:2:1649
+475:2:1657
+476:2:1658
+477:2:1662
+478:2:1663
+479:2:1671
+480:2:1676
+481:2:1680
+482:2:1681
+483:2:1689
+484:2:1690
+485:2:1694
+486:2:1695
+487:2:1689
+488:2:1690
+489:2:1694
+490:2:1695
+491:2:1703
+492:2:1708
+493:2:1709
+494:2:1720
+495:2:1721
+496:2:1722
+497:2:1733
+498:2:1738
+499:2:1739
+500:2:1750
+501:2:1751
+502:2:1752
+503:2:1750
+504:2:1751
+505:2:1752
+506:2:1763
+507:0:2890
+508:2:1179
+509:0:2890
+510:2:1772
+511:2:1773
+512:2:1777
+513:2:1778
+514:2:1786
+515:2:1787
+516:2:1791
+517:2:1792
+518:2:1800
+519:2:1805
+520:2:1809
+521:2:1810
+522:2:1818
+523:2:1819
+524:2:1823
+525:2:1824
+526:2:1818
+527:2:1819
+528:2:1823
+529:2:1824
+530:2:1832
+531:2:1837
+532:2:1838
+533:2:1849
+534:2:1850
+535:2:1851
+536:2:1862
+537:2:1867
+538:2:1868
+539:2:1879
+540:2:1880
+541:2:1881
+542:2:1879
+543:2:1880
+544:2:1881
+545:2:1892
+546:2:1899
+547:0:2890
+548:2:1179
+549:0:2890
+550:2:1903
+551:2:1904
+552:2:1905
+553:2:1917
+554:2:1918
+555:2:1922
+556:2:1923
+557:2:1931
+558:2:1936
+559:2:1940
+560:2:1941
+561:2:1949
+562:2:1950
+563:2:1954
+564:2:1955
+565:2:1949
+566:2:1950
+567:2:1954
+568:2:1955
+569:2:1963
+570:2:1968
+571:2:1969
+572:2:1980
+573:2:1981
+574:2:1982
+575:2:1993
+576:2:1998
+577:2:1999
+578:2:2010
+579:2:2011
+580:2:2012
+581:2:2010
+582:2:2011
+583:2:2012
+584:2:2023
+585:2:2033
+586:2:2034
+587:0:2890
+588:2:1179
+589:0:2890
+590:2:2043
+591:2:2044
+592:0:2890
+593:2:1179
+594:0:2890
+595:2:2048
+596:0:2890
+597:2:2056
+598:0:2890
+599:2:1174
+600:0:2890
+601:2:1176
+602:0:2890
+603:2:1177
+604:0:2890
+605:2:1178
+606:0:2890
+607:2:1179
+608:0:2890
+609:2:1180
+610:2:1181
+611:2:1185
+612:2:1186
+613:2:1194
+614:2:1195
+615:2:1199
+616:2:1200
+617:2:1208
+618:2:1213
+619:2:1217
+620:2:1218
+621:2:1226
+622:2:1227
+623:2:1231
+624:2:1232
+625:2:1226
+626:2:1227
+627:2:1228
+628:2:1240
+629:2:1245
+630:2:1246
+631:2:1257
+632:2:1258
+633:2:1259
+634:2:1270
+635:2:1275
+636:2:1276
+637:2:1287
+638:2:1288
+639:2:1289
+640:2:1287
+641:2:1288
+642:2:1289
+643:2:1300
+644:2:1308
+645:0:2890
+646:2:1179
+647:0:2890
+648:2:1312
+649:2:1316
+650:2:1317
+651:2:1321
+652:2:1325
+653:2:1326
+654:2:1330
+655:2:1338
+656:2:1339
+657:2:1343
+658:2:1347
+659:2:1348
+660:2:1343
+661:2:1344
+662:2:1352
+663:0:2890
+664:2:1179
+665:0:2890
+666:2:1360
+667:2:1361
+668:2:1362
+669:0:2890
+670:2:1179
+671:0:2890
+672:2:1370
+673:0:2890
+674:2:1179
+675:0:2890
+676:2:1373
+677:2:1374
+678:2:1378
+679:2:1379
+680:2:1387
+681:2:1388
+682:2:1392
+683:2:1393
+684:2:1401
+685:2:1406
+686:2:1407
+687:2:1419
+688:2:1420
+689:2:1424
+690:2:1425
+691:2:1419
+692:2:1420
+693:2:1424
+694:2:1425
+695:2:1433
+696:2:1438
+697:2:1439
+698:2:1450
+699:2:1451
+700:2:1452
+701:2:1463
+702:2:1468
+703:2:1469
+704:2:1480
+705:2:1481
+706:2:1482
+707:2:1480
+708:2:1481
+709:2:1482
+710:2:1493
+711:2:1500
+712:0:2890
+713:2:1179
+714:0:2890
+715:2:1504
+716:2:1505
+717:2:1506
+718:2:1518
+719:2:1519
+720:2:1523
+721:2:1524
+722:2:1532
+723:2:1537
+724:2:1541
+725:2:1542
+726:2:1550
+727:2:1551
+728:2:1555
+729:2:1556
+730:2:1550
+731:2:1551
+732:2:1555
+733:2:1556
+734:2:1564
+735:2:1569
+736:2:1570
+737:2:1581
+738:2:1582
+739:2:1583
+740:2:1594
+741:2:1599
+742:2:1600
+743:2:1611
+744:2:1612
+745:2:1613
+746:2:1611
+747:2:1612
+748:2:1613
+749:2:1624
+750:2:1635
+751:2:1636
+752:0:2890
+753:2:1179
+754:0:2890
+755:2:1643
+756:2:1644
+757:2:1648
+758:2:1649
+759:2:1657
+760:2:1658
+761:2:1662
+762:2:1663
+763:2:1671
+764:2:1676
+765:2:1680
+766:2:1681
+767:2:1689
+768:2:1690
+769:2:1694
+770:2:1695
+771:2:1689
+772:2:1690
+773:2:1694
+774:2:1695
+775:2:1703
+776:2:1708
+777:2:1709
+778:2:1720
+779:2:1721
+780:2:1722
+781:2:1733
+782:2:1738
+783:2:1739
+784:2:1750
+785:2:1751
+786:2:1752
+787:2:1750
+788:2:1751
+789:2:1752
+790:2:1763
+791:0:2890
+792:2:1179
+793:0:2890
+794:2:1903
+795:2:1904
+796:2:1908
+797:2:1909
+798:2:1917
+799:2:1918
+800:2:1922
+801:2:1923
+802:2:1931
+803:2:1936
+804:2:1940
+805:2:1941
+806:2:1949
+807:2:1950
+808:2:1954
+809:2:1955
+810:2:1949
+811:2:1950
+812:2:1954
+813:2:1955
+814:2:1963
+815:2:1968
+816:2:1969
+817:2:1980
+818:2:1981
+819:2:1982
+820:2:1993
+821:2:1998
+822:2:1999
+823:2:2010
+824:2:2011
+825:2:2012
+826:2:2010
+827:2:2011
+828:2:2012
+829:2:2023
+830:2:2033
+831:2:2034
+832:0:2890
+833:2:1179
+834:0:2890
+835:2:2043
+836:2:2044
+837:0:2890
+838:2:1179
+839:0:2890
+840:2:1772
+841:2:1773
+842:2:1777
+843:2:1778
+844:2:1786
+845:2:1787
+846:2:1791
+847:2:1792
+848:2:1800
+849:2:1805
+850:2:1809
+851:2:1810
+852:2:1818
+853:2:1819
+854:2:1820
+855:2:1818
+856:2:1819
+857:2:1823
+858:2:1824
+859:2:1832
+860:2:1837
+861:2:1838
+862:2:1849
+863:2:1850
+864:2:1851
+865:2:1862
+866:2:1867
+867:2:1868
+868:2:1879
+869:2:1880
+870:2:1881
+871:2:1879
+872:2:1880
+873:2:1881
+874:2:1892
+875:2:1899
+876:0:2890
+877:2:1179
+878:0:2890
+879:2:2048
+880:0:2890
+881:2:2056
+882:0:2890
+883:2:2057
+884:0:2890
+885:2:2062
+886:0:2890
+887:1:29
+888:0:2890
+889:2:2063
+890:0:2890
+891:1:35
+892:0:2890
+893:2:2062
+894:0:2890
+895:1:36
+896:0:2890
+897:2:2063
+898:0:2890
+899:1:37
+900:0:2890
+901:2:2062
+902:0:2890
+903:1:38
+904:0:2890
+905:2:2063
+906:0:2890
+907:1:39
+908:0:2890
+909:2:2062
+910:0:2890
+911:1:40
+912:0:2890
+913:2:2063
+914:0:2890
+915:1:41
+916:0:2890
+917:2:2062
+918:0:2890
+919:1:42
+920:0:2890
+921:2:2063
+922:0:2890
+923:1:43
+924:0:2890
+925:2:2062
+926:0:2890
+927:1:44
+928:0:2890
+929:2:2063
+930:0:2890
+931:1:145
+932:0:2890
+933:2:2062
+934:0:2890
+935:1:147
+936:0:2890
+937:2:2063
+938:0:2890
+939:1:46
+940:0:2890
+941:2:2062
+942:0:2890
+943:1:153
+944:1:154
+945:1:158
+946:1:159
+947:1:167
+948:1:168
+949:1:172
+950:1:173
+951:1:181
+952:1:186
+953:1:190
+954:1:191
+955:1:199
+956:1:200
+957:1:204
+958:1:205
+959:1:199
+960:1:200
+961:1:204
+962:1:205
+963:1:213
+964:1:218
+965:1:219
+966:1:230
+967:1:231
+968:1:232
+969:1:243
+970:1:255
+971:1:256
+972:1:260
+973:1:261
+974:1:262
+975:1:260
+976:1:261
+977:1:262
+978:1:273
+979:0:2890
+980:2:2063
+981:0:2890
+982:1:42
+983:0:2890
+984:2:2062
+985:0:2890
+986:1:43
+987:0:2890
+988:2:2063
+989:0:2890
+990:1:44
+991:0:2890
+992:2:2062
+993:0:2890
+994:1:145
+995:0:2890
+996:2:2063
+997:0:2890
+998:1:147
+999:0:2890
+1000:2:2062
+1001:0:2890
+1002:1:46
+1003:0:2890
+1004:2:2063
+1005:0:2890
+1006:1:282
+1007:1:283
+1008:0:2890
+1009:2:2062
+1010:0:2890
+1011:1:42
+1012:0:2890
+1013:2:2063
+1014:0:2890
+1015:1:43
+1016:0:2890
+1017:2:2062
+1018:0:2890
+1019:1:44
+1020:0:2890
+1021:2:2063
+1022:0:2890
+1023:1:145
+1024:0:2890
+1025:2:2062
+1026:0:2890
+1027:1:147
+1028:0:2890
+1029:2:2063
+1030:0:2890
+1031:1:46
+1032:0:2890
+1033:2:2062
+1034:0:2890
+1035:1:289
+1036:1:290
+1037:1:294
+1038:1:295
+1039:1:303
+1040:1:304
+1041:1:308
+1042:1:309
+1043:1:317
+1044:1:322
+1045:1:326
+1046:1:327
+1047:1:335
+1048:1:336
+1049:1:340
+1050:1:341
+1051:1:335
+1052:1:336
+1053:1:340
+1054:1:341
+1055:1:349
+1056:1:354
+1057:1:355
+1058:1:366
+1059:1:367
+1060:1:368
+1061:1:379
+1062:1:391
+1063:1:392
+1064:1:396
+1065:1:397
+1066:1:398
+1067:1:396
+1068:1:397
+1069:1:398
+1070:1:409
+1071:0:2890
+1072:2:2063
+1073:0:2890
+1074:1:42
+1075:0:2890
+1076:2:2062
+1077:0:2890
+1078:1:43
+1079:0:2890
+1080:2:2063
+1081:0:2890
+1082:1:44
+1083:0:2890
+1084:2:2062
+1085:0:2890
+1086:1:145
+1087:0:2890
+1088:2:2063
+1089:0:2890
+1090:1:147
+1091:0:2890
+1092:2:2062
+1093:0:2890
+1094:1:46
+1095:0:2890
+1096:2:2063
+1097:0:2890
+1098:1:418
+1099:1:419
+1100:1:423
+1101:1:424
+1102:1:432
+1103:1:433
+1104:1:437
+1105:1:438
+1106:1:446
+1107:1:451
+1108:1:455
+1109:1:456
+1110:1:464
+1111:1:465
+1112:1:469
+1113:1:470
+1114:1:464
+1115:1:465
+1116:1:469
+1117:1:470
+1118:1:478
+1119:1:483
+1120:1:484
+1121:1:495
+1122:1:496
+1123:1:497
+1124:1:508
+1125:1:520
+1126:1:521
+1127:1:525
+1128:1:526
+1129:1:527
+1130:1:525
+1131:1:526
+1132:1:527
+1133:1:538
+1134:1:545
+1135:0:2890
+1136:2:2062
+1137:0:2890
+1138:1:42
+1139:0:2890
+1140:2:2063
+1141:0:2890
+1142:1:43
+1143:0:2890
+1144:2:2062
+1145:0:2890
+1146:1:44
+1147:0:2890
+1148:2:2063
+1149:0:2890
+1150:1:145
+1151:0:2890
+1152:2:2062
+1153:0:2890
+1154:1:147
+1155:0:2890
+1156:2:2063
+1157:0:2890
+1158:1:46
+1159:0:2890
+1160:2:2062
+1161:0:2890
+1162:1:683
+1163:1:684
+1164:1:688
+1165:1:689
+1166:1:697
+1167:1:698
+1168:1:699
+1169:1:711
+1170:1:716
+1171:1:720
+1172:1:721
+1173:1:729
+1174:1:730
+1175:1:734
+1176:1:735
+1177:1:729
+1178:1:730
+1179:1:734
+1180:1:735
+1181:1:743
+1182:1:748
+1183:1:749
+1184:1:760
+1185:1:761
+1186:1:762
+1187:1:773
+1188:1:785
+1189:1:786
+1190:1:790
+1191:1:791
+1192:1:792
+1193:1:790
+1194:1:791
+1195:1:792
+1196:1:803
+1197:0:2890
+1198:2:2063
+1199:0:2890
+1200:1:42
+1201:0:2890
+1202:2:2062
+1203:0:2890
+1204:1:43
+1205:0:2890
+1206:2:2063
+1207:0:2890
+1208:1:44
+1209:0:2890
+1210:2:2062
+1211:0:2890
+1212:1:145
+1213:0:2890
+1214:2:2063
+1215:0:2890
+1216:1:147
+1217:0:2890
+1218:2:2062
+1219:0:2890
+1220:1:46
+1221:0:2890
+1222:2:2063
+1223:0:2890
+1224:1:812
+1225:0:2890
+1226:2:2062
+1227:0:2890
+1228:1:1089
+1229:1:1096
+1230:1:1097
+1231:1:1104
+1232:1:1109
+1233:1:1116
+1234:1:1117
+1235:1:1116
+1236:1:1117
+1237:1:1124
+1238:1:1128
+1239:0:2890
+1240:2:2063
+1241:0:2890
+1242:1:814
+1243:1:815
+1244:0:2888
+1245:2:2062
+1246:0:2894
+1247:1:1049