Add verif results

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

diff --git a/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_rmb.spin.input.trail b/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_rmb.spin.input.trail
new file mode 100644 (file)
index 0000000..931028a
--- /dev/null
+++ b/formal-model/urcu-controldataflow-alpha-ipi-progress-minimal/urcu_free_no_rmb.spin.input.trail
@@ -0,0 +1,1479 @@
+-2:3:-2
+-4:-4:-4
+1:0:2970
+2:2:1220
+3:2:1225
+4:2:1229
+5:2:1237
+6:2:1241
+7:2:1245
+8:0:2970
+9:1:0
+10:1:5
+11:1:9
+12:1:17
+13:1:21
+14:1:25
+15:0:2970
+16:3:2942
+17:3:2945
+18:3:2950
+19:3:2957
+20:3:2960
+21:3:2964
+22:3:2965
+23:0:2970
+24:3:2967
+25:0:2970
+26:2:1249
+27:0:2970
+28:2:1255
+29:0:2970
+30:2:1256
+31:0:2970
+32:2:1258
+33:0:2970
+34:2:1259
+35:0:2970
+36:2:1260
+37:2:1261
+38:2:1265
+39:2:1266
+40:2:1274
+41:2:1275
+42:2:1279
+43:2:1280
+44:2:1288
+45:2:1293
+46:2:1297
+47:2:1298
+48:2:1306
+49:2:1307
+50:2:1311
+51:2:1312
+52:2:1306
+53:2:1307
+54:2:1311
+55:2:1312
+56:2:1320
+57:2:1325
+58:2:1326
+59:2:1337
+60:2:1338
+61:2:1339
+62:2:1350
+63:2:1355
+64:2:1356
+65:2:1367
+66:2:1368
+67:2:1369
+68:2:1367
+69:2:1368
+70:2:1369
+71:2:1380
+72:2:1388
+73:0:2970
+74:2:1259
+75:0:2970
+76:2:1392
+77:2:1396
+78:2:1397
+79:2:1401
+80:2:1405
+81:2:1406
+82:2:1410
+83:2:1418
+84:2:1419
+85:2:1423
+86:2:1427
+87:2:1428
+88:2:1423
+89:2:1424
+90:2:1432
+91:0:2970
+92:2:1259
+93:0:2970
+94:2:1440
+95:2:1441
+96:2:1442
+97:0:2970
+98:2:1259
+99:0:2970
+100:2:1447
+101:0:2970
+102:2:2151
+103:2:2152
+104:2:2156
+105:2:2160
+106:2:2161
+107:2:2165
+108:2:2170
+109:2:2178
+110:2:2182
+111:2:2183
+112:2:2178
+113:2:2182
+114:2:2183
+115:2:2187
+116:2:2194
+117:2:2201
+118:2:2202
+119:2:2209
+120:2:2214
+121:2:2221
+122:2:2222
+123:2:2221
+124:2:2222
+125:2:2229
+126:2:2233
+127:0:2970
+128:2:2238
+129:0:2970
+130:2:2239
+131:0:2970
+132:2:2240
+133:0:2970
+134:2:2241
+135:0:2970
+136:1:29
+137:0:2970
+138:2:2242
+139:0:2970
+140:1:35
+141:0:2970
+142:1:36
+143:0:2970
+144:2:2241
+145:0:2970
+146:1:37
+147:0:2970
+148:2:2242
+149:0:2970
+150:1:38
+151:0:2970
+152:2:2241
+153:0:2970
+154:1:39
+155:0:2970
+156:2:2242
+157:0:2970
+158:1:40
+159:0:2970
+160:1:41
+161:0:2970
+162:2:2241
+163:0:2970
+164:1:42
+165:0:2970
+166:2:2242
+167:0:2970
+168:1:51
+169:0:2970
+170:2:2241
+171:0:2970
+172:1:55
+173:1:56
+174:1:60
+175:1:64
+176:1:65
+177:1:69
+178:1:77
+179:1:78
+180:1:82
+181:1:86
+182:1:87
+183:1:82
+184:1:86
+185:1:87
+186:1:91
+187:1:98
+188:1:105
+189:1:106
+190:1:113
+191:1:118
+192:1:125
+193:1:126
+194:1:125
+195:1:126
+196:1:133
+197:1:137
+198:0:2970
+199:2:2242
+200:0:2970
+201:1:142
+202:0:2970
+203:2:2243
+204:0:2970
+205:2:2248
+206:0:2970
+207:2:2249
+208:0:2970
+209:2:2257
+210:2:2258
+211:2:2262
+212:2:2266
+213:2:2267
+214:2:2271
+215:2:2279
+216:2:2280
+217:2:2284
+218:2:2288
+219:2:2289
+220:2:2284
+221:2:2288
+222:2:2289
+223:2:2293
+224:2:2300
+225:2:2307
+226:2:2308
+227:2:2315
+228:2:2320
+229:2:2327
+230:2:2328
+231:2:2327
+232:2:2328
+233:2:2335
+234:2:2339
+235:0:2970
+236:2:1449
+237:2:2132
+238:0:2970
+239:2:1259
+240:0:2970
+241:2:1450
+242:0:2970
+243:2:1259
+244:0:2970
+245:2:1453
+246:2:1454
+247:2:1458
+248:2:1459
+249:2:1467
+250:2:1468
+251:2:1472
+252:2:1473
+253:2:1481
+254:2:1486
+255:2:1490
+256:2:1491
+257:2:1499
+258:2:1500
+259:2:1504
+260:2:1505
+261:2:1499
+262:2:1500
+263:2:1504
+264:2:1505
+265:2:1513
+266:2:1518
+267:2:1519
+268:2:1530
+269:2:1531
+270:2:1532
+271:2:1543
+272:2:1548
+273:2:1549
+274:2:1560
+275:2:1561
+276:2:1562
+277:2:1560
+278:2:1561
+279:2:1562
+280:2:1573
+281:2:1580
+282:0:2970
+283:2:1259
+284:0:2970
+285:2:1584
+286:2:1585
+287:2:1586
+288:2:1598
+289:2:1599
+290:2:1603
+291:2:1604
+292:2:1612
+293:2:1617
+294:2:1621
+295:2:1622
+296:2:1630
+297:2:1631
+298:2:1635
+299:2:1636
+300:2:1630
+301:2:1631
+302:2:1635
+303:2:1636
+304:2:1644
+305:2:1649
+306:2:1650
+307:2:1661
+308:2:1662
+309:2:1663
+310:2:1674
+311:2:1679
+312:2:1680
+313:2:1691
+314:2:1692
+315:2:1693
+316:2:1691
+317:2:1692
+318:2:1693
+319:2:1704
+320:2:1715
+321:2:1716
+322:0:2970
+323:2:1259
+324:0:2970
+325:2:1723
+326:2:1724
+327:2:1728
+328:2:1729
+329:2:1737
+330:2:1738
+331:2:1742
+332:2:1743
+333:2:1751
+334:2:1756
+335:2:1760
+336:2:1761
+337:2:1769
+338:2:1770
+339:2:1774
+340:2:1775
+341:2:1769
+342:2:1770
+343:2:1774
+344:2:1775
+345:2:1783
+346:2:1788
+347:2:1789
+348:2:1800
+349:2:1801
+350:2:1802
+351:2:1813
+352:2:1818
+353:2:1819
+354:2:1830
+355:2:1831
+356:2:1832
+357:2:1830
+358:2:1831
+359:2:1832
+360:2:1843
+361:0:2970
+362:2:1259
+363:0:2970
+364:2:1852
+365:2:1853
+366:2:1857
+367:2:1858
+368:2:1866
+369:2:1867
+370:2:1871
+371:2:1872
+372:2:1880
+373:2:1885
+374:2:1889
+375:2:1890
+376:2:1898
+377:2:1899
+378:2:1903
+379:2:1904
+380:2:1898
+381:2:1899
+382:2:1903
+383:2:1904
+384:2:1912
+385:2:1917
+386:2:1918
+387:2:1929
+388:2:1930
+389:2:1931
+390:2:1942
+391:2:1947
+392:2:1948
+393:2:1959
+394:2:1960
+395:2:1961
+396:2:1959
+397:2:1960
+398:2:1961
+399:2:1972
+400:2:1979
+401:0:2970
+402:2:1259
+403:0:2970
+404:2:1983
+405:2:1984
+406:2:1985
+407:2:1997
+408:2:1998
+409:2:2002
+410:2:2003
+411:2:2011
+412:2:2016
+413:2:2020
+414:2:2021
+415:2:2029
+416:2:2030
+417:2:2034
+418:2:2035
+419:2:2029
+420:2:2030
+421:2:2034
+422:2:2035
+423:2:2043
+424:2:2048
+425:2:2049
+426:2:2060
+427:2:2061
+428:2:2062
+429:2:2073
+430:2:2078
+431:2:2079
+432:2:2090
+433:2:2091
+434:2:2092
+435:2:2090
+436:2:2091
+437:2:2092
+438:2:2103
+439:2:2113
+440:2:2114
+441:0:2970
+442:2:1259
+443:0:2970
+444:2:2120
+445:0:2970
+446:2:2745
+447:2:2746
+448:2:2750
+449:2:2754
+450:2:2755
+451:2:2759
+452:2:2767
+453:2:2768
+454:2:2772
+455:2:2776
+456:2:2777
+457:2:2772
+458:2:2776
+459:2:2777
+460:2:2781
+461:2:2788
+462:2:2795
+463:2:2796
+464:2:2803
+465:2:2808
+466:2:2815
+467:2:2816
+468:2:2815
+469:2:2816
+470:2:2823
+471:2:2827
+472:0:2970
+473:2:2832
+474:0:2970
+475:2:2833
+476:0:2970
+477:2:2834
+478:0:2970
+479:2:2835
+480:0:2970
+481:1:51
+482:0:2970
+483:2:2836
+484:0:2970
+485:1:55
+486:1:56
+487:1:60
+488:1:64
+489:1:65
+490:1:69
+491:1:77
+492:1:78
+493:1:82
+494:1:86
+495:1:87
+496:1:82
+497:1:86
+498:1:87
+499:1:91
+500:1:98
+501:1:105
+502:1:106
+503:1:113
+504:1:118
+505:1:125
+506:1:126
+507:1:125
+508:1:126
+509:1:133
+510:1:137
+511:0:2970
+512:2:2835
+513:0:2970
+514:1:142
+515:0:2970
+516:2:2836
+517:0:2970
+518:2:2837
+519:0:2970
+520:2:2842
+521:0:2970
+522:2:2843
+523:0:2970
+524:2:2851
+525:2:2852
+526:2:2856
+527:2:2860
+528:2:2861
+529:2:2865
+530:2:2873
+531:2:2874
+532:2:2878
+533:2:2882
+534:2:2883
+535:2:2878
+536:2:2882
+537:2:2883
+538:2:2887
+539:2:2894
+540:2:2901
+541:2:2902
+542:2:2909
+543:2:2914
+544:2:2921
+545:2:2922
+546:2:2921
+547:2:2922
+548:2:2929
+549:2:2933
+550:0:2970
+551:2:2122
+552:2:2132
+553:0:2970
+554:2:1259
+555:0:2970
+556:2:2123
+557:2:2124
+558:0:2970
+559:2:1259
+560:0:2970
+561:2:2128
+562:0:2970
+563:2:2136
+564:0:2970
+565:2:1256
+566:0:2970
+567:2:1258
+568:0:2970
+569:2:1259
+570:0:2970
+571:2:1260
+572:2:1261
+573:2:1265
+574:2:1266
+575:2:1274
+576:2:1275
+577:2:1279
+578:2:1280
+579:2:1288
+580:2:1293
+581:2:1297
+582:2:1298
+583:2:1306
+584:2:1307
+585:2:1308
+586:2:1306
+587:2:1307
+588:2:1311
+589:2:1312
+590:2:1320
+591:2:1325
+592:2:1326
+593:2:1337
+594:2:1338
+595:2:1339
+596:2:1350
+597:2:1355
+598:2:1356
+599:2:1367
+600:2:1368
+601:2:1369
+602:2:1367
+603:2:1368
+604:2:1369
+605:2:1380
+606:2:1388
+607:0:2970
+608:2:1259
+609:0:2970
+610:2:1392
+611:2:1396
+612:2:1397
+613:2:1401
+614:2:1405
+615:2:1406
+616:2:1410
+617:2:1418
+618:2:1419
+619:2:1423
+620:2:1424
+621:2:1423
+622:2:1427
+623:2:1428
+624:2:1432
+625:0:2970
+626:2:1259
+627:0:2970
+628:2:1440
+629:2:1441
+630:2:1442
+631:0:2970
+632:2:1259
+633:0:2970
+634:2:1447
+635:0:2970
+636:2:2151
+637:2:2152
+638:2:2156
+639:2:2160
+640:2:2161
+641:2:2165
+642:2:2170
+643:2:2178
+644:2:2182
+645:2:2183
+646:2:2178
+647:2:2182
+648:2:2183
+649:2:2187
+650:2:2194
+651:2:2201
+652:2:2202
+653:2:2209
+654:2:2214
+655:2:2221
+656:2:2222
+657:2:2221
+658:2:2222
+659:2:2229
+660:2:2233
+661:0:2970
+662:2:2238
+663:0:2970
+664:2:2239
+665:0:2970
+666:2:2240
+667:0:2970
+668:2:2241
+669:0:2970
+670:1:51
+671:0:2970
+672:2:2242
+673:0:2970
+674:1:55
+675:1:56
+676:1:60
+677:1:64
+678:1:65
+679:1:69
+680:1:77
+681:1:78
+682:1:82
+683:1:86
+684:1:87
+685:1:82
+686:1:86
+687:1:87
+688:1:91
+689:1:98
+690:1:105
+691:1:106
+692:1:113
+693:1:118
+694:1:125
+695:1:126
+696:1:125
+697:1:126
+698:1:133
+699:1:137
+700:0:2970
+701:2:2241
+702:0:2970
+703:1:142
+704:0:2970
+705:2:2242
+706:0:2970
+707:2:2243
+708:0:2970
+709:2:2248
+710:0:2970
+711:2:2249
+712:0:2970
+713:2:2257
+714:2:2258
+715:2:2262
+716:2:2266
+717:2:2267
+718:2:2271
+719:2:2279
+720:2:2280
+721:2:2284
+722:2:2288
+723:2:2289
+724:2:2284
+725:2:2288
+726:2:2289
+727:2:2293
+728:2:2300
+729:2:2307
+730:2:2308
+731:2:2315
+732:2:2320
+733:2:2327
+734:2:2328
+735:2:2327
+736:2:2328
+737:2:2335
+738:2:2339
+739:0:2970
+740:2:1449
+741:2:2132
+742:0:2970
+743:2:1259
+744:0:2970
+745:2:1450
+746:0:2970
+747:2:1259
+748:0:2970
+749:2:1453
+750:2:1454
+751:2:1458
+752:2:1459
+753:2:1467
+754:2:1468
+755:2:1472
+756:2:1473
+757:2:1481
+758:2:1486
+759:2:1490
+760:2:1491
+761:2:1499
+762:2:1500
+763:2:1504
+764:2:1505
+765:2:1499
+766:2:1500
+767:2:1504
+768:2:1505
+769:2:1513
+770:2:1518
+771:2:1519
+772:2:1530
+773:2:1531
+774:2:1532
+775:2:1543
+776:2:1548
+777:2:1549
+778:2:1560
+779:2:1561
+780:2:1562
+781:2:1560
+782:2:1561
+783:2:1562
+784:2:1573
+785:2:1580
+786:0:2970
+787:2:1259
+788:0:2970
+789:2:1584
+790:2:1585
+791:2:1586
+792:2:1598
+793:2:1599
+794:2:1603
+795:2:1604
+796:2:1612
+797:2:1617
+798:2:1621
+799:2:1622
+800:2:1630
+801:2:1631
+802:2:1635
+803:2:1636
+804:2:1630
+805:2:1631
+806:2:1635
+807:2:1636
+808:2:1644
+809:2:1649
+810:2:1650
+811:2:1661
+812:2:1662
+813:2:1663
+814:2:1674
+815:2:1679
+816:2:1680
+817:2:1691
+818:2:1692
+819:2:1693
+820:2:1691
+821:2:1692
+822:2:1693
+823:2:1704
+824:2:1715
+825:2:1716
+826:0:2970
+827:2:1259
+828:0:2970
+829:2:1723
+830:2:1724
+831:2:1728
+832:2:1729
+833:2:1737
+834:2:1738
+835:2:1742
+836:2:1743
+837:2:1751
+838:2:1756
+839:2:1760
+840:2:1761
+841:2:1769
+842:2:1770
+843:2:1774
+844:2:1775
+845:2:1769
+846:2:1770
+847:2:1774
+848:2:1775
+849:2:1783
+850:2:1788
+851:2:1789
+852:2:1800
+853:2:1801
+854:2:1802
+855:2:1813
+856:2:1818
+857:2:1819
+858:2:1830
+859:2:1831
+860:2:1832
+861:2:1830
+862:2:1831
+863:2:1832
+864:2:1843
+865:0:2970
+866:2:1259
+867:0:2970
+868:2:1852
+869:2:1853
+870:2:1857
+871:2:1858
+872:2:1866
+873:2:1867
+874:2:1871
+875:2:1872
+876:2:1880
+877:2:1885
+878:2:1889
+879:2:1890
+880:2:1898
+881:2:1899
+882:2:1903
+883:2:1904
+884:2:1898
+885:2:1899
+886:2:1903
+887:2:1904
+888:2:1912
+889:2:1917
+890:2:1918
+891:2:1929
+892:2:1930
+893:2:1931
+894:2:1942
+895:2:1947
+896:2:1948
+897:2:1959
+898:2:1960
+899:2:1961
+900:2:1959
+901:2:1960
+902:2:1961
+903:2:1972
+904:2:1979
+905:0:2970
+906:2:1259
+907:0:2970
+908:2:1983
+909:2:1984
+910:2:1985
+911:2:1997
+912:2:1998
+913:2:2002
+914:2:2003
+915:2:2011
+916:2:2016
+917:2:2020
+918:2:2021
+919:2:2029
+920:2:2030
+921:2:2034
+922:2:2035
+923:2:2029
+924:2:2030
+925:2:2034
+926:2:2035
+927:2:2043
+928:2:2048
+929:2:2049
+930:2:2060
+931:2:2061
+932:2:2062
+933:2:2073
+934:2:2078
+935:2:2079
+936:2:2090
+937:2:2091
+938:2:2092
+939:2:2090
+940:2:2091
+941:2:2092
+942:2:2103
+943:2:2113
+944:2:2114
+945:0:2970
+946:2:1259
+947:0:2970
+948:2:2120
+949:0:2970
+950:2:2745
+951:2:2746
+952:2:2750
+953:2:2754
+954:2:2755
+955:2:2759
+956:2:2767
+957:2:2768
+958:2:2772
+959:2:2776
+960:2:2777
+961:2:2772
+962:2:2776
+963:2:2777
+964:2:2781
+965:2:2788
+966:2:2795
+967:2:2796
+968:2:2803
+969:2:2808
+970:2:2815
+971:2:2816
+972:2:2815
+973:2:2816
+974:2:2823
+975:2:2827
+976:0:2970
+977:2:2832
+978:0:2970
+979:2:2833
+980:0:2970
+981:2:2834
+982:0:2970
+983:2:2835
+984:0:2970
+985:1:51
+986:0:2970
+987:2:2836
+988:0:2970
+989:1:55
+990:1:56
+991:1:60
+992:1:64
+993:1:65
+994:1:69
+995:1:77
+996:1:78
+997:1:82
+998:1:86
+999:1:87
+1000:1:82
+1001:1:86
+1002:1:87
+1003:1:91
+1004:1:98
+1005:1:105
+1006:1:106
+1007:1:113
+1008:1:118
+1009:1:125
+1010:1:126
+1011:1:125
+1012:1:126
+1013:1:133
+1014:1:137
+1015:0:2970
+1016:2:2835
+1017:0:2970
+1018:1:142
+1019:0:2970
+1020:2:2836
+1021:0:2970
+1022:2:2837
+1023:0:2970
+1024:2:2842
+1025:0:2970
+1026:2:2843
+1027:0:2970
+1028:2:2851
+1029:2:2852
+1030:2:2856
+1031:2:2860
+1032:2:2861
+1033:2:2865
+1034:2:2873
+1035:2:2874
+1036:2:2878
+1037:2:2882
+1038:2:2883
+1039:2:2878
+1040:2:2882
+1041:2:2883
+1042:2:2887
+1043:2:2894
+1044:2:2901
+1045:2:2902
+1046:2:2909
+1047:2:2914
+1048:2:2921
+1049:2:2922
+1050:2:2921
+1051:2:2922
+1052:2:2929
+1053:2:2933
+1054:0:2970
+1055:2:2122
+1056:2:2132
+1057:0:2970
+1058:2:1259
+1059:0:2970
+1060:2:2123
+1061:2:2124
+1062:0:2970
+1063:2:1259
+1064:0:2970
+1065:2:2128
+1066:0:2970
+1067:2:2136
+1068:0:2970
+1069:2:1256
+1070:0:2970
+1071:2:1258
+1072:0:2970
+1073:2:1259
+1074:0:2970
+1075:2:1260
+1076:2:1261
+1077:2:1265
+1078:2:1266
+1079:2:1274
+1080:2:1275
+1081:2:1279
+1082:2:1280
+1083:2:1288
+1084:2:1293
+1085:2:1297
+1086:2:1298
+1087:2:1306
+1088:2:1307
+1089:2:1311
+1090:2:1312
+1091:2:1306
+1092:2:1307
+1093:2:1308
+1094:2:1320
+1095:2:1325
+1096:2:1326
+1097:2:1337
+1098:2:1338
+1099:2:1339
+1100:2:1350
+1101:2:1355
+1102:2:1356
+1103:2:1367
+1104:2:1368
+1105:2:1369
+1106:2:1367
+1107:2:1368
+1108:2:1369
+1109:2:1380
+1110:2:1388
+1111:0:2970
+1112:2:1259
+1113:0:2970
+1114:1:143
+1115:0:2970
+1116:1:145
+1117:0:2970
+1118:1:44
+1119:0:2970
+1120:1:151
+1121:1:152
+1122:1:156
+1123:1:157
+1124:1:165
+1125:1:166
+1126:1:170
+1127:1:171
+1128:1:179
+1129:1:184
+1130:1:188
+1131:1:189
+1132:1:197
+1133:1:198
+1134:1:202
+1135:1:203
+1136:1:197
+1137:1:198
+1138:1:202
+1139:1:203
+1140:1:211
+1141:1:216
+1142:1:217
+1143:1:228
+1144:1:229
+1145:1:230
+1146:1:241
+1147:1:246
+1148:1:247
+1149:1:258
+1150:1:259
+1151:1:260
+1152:1:258
+1153:1:259
+1154:1:260
+1155:1:271
+1156:0:2970
+1157:1:40
+1158:0:2970
+1159:1:41
+1160:0:2970
+1161:2:1392
+1162:2:1396
+1163:2:1397
+1164:2:1401
+1165:2:1405
+1166:2:1406
+1167:2:1410
+1168:2:1418
+1169:2:1419
+1170:2:1423
+1171:2:1427
+1172:2:1428
+1173:2:1423
+1174:2:1424
+1175:2:1432
+1176:0:2970
+1177:2:1259
+1178:0:2970
+1179:2:1440
+1180:2:1441
+1181:2:1442
+1182:0:2970
+1183:2:1259
+1184:0:2970
+1185:2:1447
+1186:0:2970
+1187:2:2151
+1188:2:2152
+1189:2:2156
+1190:2:2160
+1191:2:2161
+1192:2:2165
+1193:2:2170
+1194:2:2178
+1195:2:2182
+1196:2:2183
+1197:2:2178
+1198:2:2182
+1199:2:2183
+1200:2:2187
+1201:2:2194
+1202:2:2201
+1203:2:2202
+1204:2:2209
+1205:2:2214
+1206:2:2221
+1207:2:2222
+1208:2:2221
+1209:2:2222
+1210:2:2229
+1211:2:2233
+1212:0:2970
+1213:2:2238
+1214:0:2970
+1215:2:2239
+1216:0:2970
+1217:2:2240
+1218:0:2970
+1219:2:2241
+1220:0:2970
+1221:1:42
+1222:0:2970
+1223:2:2242
+1224:0:2970
+1225:1:143
+1226:0:2970
+1227:1:145
+1228:0:2970
+1229:2:2241
+1230:0:2970
+1231:1:44
+1232:0:2970
+1233:2:2242
+1234:0:2970
+1235:1:280
+1236:1:281
+1237:0:2970
+1238:1:40
+1239:0:2970
+1240:1:41
+1241:0:2970
+1242:2:2241
+1243:0:2970
+1244:1:42
+1245:0:2970
+1246:2:2242
+1247:0:2970
+1248:1:143
+1249:0:2970
+1250:1:145
+1251:0:2970
+1252:2:2241
+1253:0:2970
+1254:1:44
+1255:0:2970
+1256:2:2242
+1257:0:2970
+1258:1:287
+1259:1:288
+1260:1:292
+1261:1:293
+1262:1:301
+1263:1:302
+1264:1:306
+1265:1:307
+1266:1:315
+1267:1:320
+1268:1:324
+1269:1:325
+1270:1:333
+1271:1:334
+1272:1:338
+1273:1:339
+1274:1:333
+1275:1:334
+1276:1:338
+1277:1:339
+1278:1:347
+1279:1:352
+1280:1:353
+1281:1:364
+1282:1:365
+1283:1:366
+1284:1:377
+1285:1:382
+1286:1:383
+1287:1:394
+1288:1:395
+1289:1:396
+1290:1:394
+1291:1:402
+1292:1:403
+1293:1:407
+1294:0:2970
+1295:1:40
+1296:0:2970
+1297:1:41
+1298:0:2970
+1299:2:2241
+1300:0:2970
+1301:1:42
+1302:0:2970
+1303:2:2242
+1304:0:2970
+1305:1:143
+1306:0:2970
+1307:1:145
+1308:0:2970
+1309:2:2241
+1310:0:2970
+1311:1:44
+1312:0:2970
+1313:2:2242
+1314:0:2970
+1315:1:416
+1316:1:417
+1317:1:421
+1318:1:422
+1319:1:430
+1320:1:431
+1321:1:435
+1322:1:436
+1323:1:444
+1324:1:449
+1325:1:453
+1326:1:454
+1327:1:462
+1328:1:463
+1329:1:467
+1330:1:468
+1331:1:462
+1332:1:463
+1333:1:467
+1334:1:468
+1335:1:476
+1336:1:481
+1337:1:482
+1338:1:493
+1339:1:494
+1340:1:495
+1341:1:506
+1342:1:511
+1343:1:512
+1344:1:523
+1345:1:524
+1346:1:525
+1347:1:523
+1348:1:531
+1349:1:532
+1350:1:536
+1351:1:543
+1352:0:2970
+1353:1:40
+1354:0:2970
+1355:1:41
+1356:0:2970
+1357:2:2241
+1358:0:2970
+1359:1:42
+1360:0:2970
+1361:2:2242
+1362:0:2970
+1363:1:143
+1364:0:2970
+1365:1:145
+1366:0:2970
+1367:2:2241
+1368:0:2970
+1369:1:44
+1370:0:2970
+1371:2:2242
+1372:0:2970
+1373:1:681
+1374:1:682
+1375:1:686
+1376:1:687
+1377:1:695
+1378:1:696
+1379:1:697
+1380:1:709
+1381:1:714
+1382:1:718
+1383:1:719
+1384:1:727
+1385:1:728
+1386:1:732
+1387:1:733
+1388:1:727
+1389:1:728
+1390:1:732
+1391:1:733
+1392:1:741
+1393:1:746
+1394:1:747
+1395:1:758
+1396:1:759
+1397:1:760
+1398:1:771
+1399:1:776
+1400:1:777
+1401:1:788
+1402:1:789
+1403:1:790
+1404:1:788
+1405:1:796
+1406:1:797
+1407:1:801
+1408:0:2970
+1409:1:40
+1410:0:2970
+1411:1:41
+1412:0:2970
+1413:2:2241
+1414:0:2970
+1415:1:42
+1416:0:2970
+1417:2:2242
+1418:0:2970
+1419:1:143
+1420:0:2970
+1421:1:145
+1422:0:2970
+1423:2:2241
+1424:0:2970
+1425:1:44
+1426:0:2970
+1427:2:2242
+1428:0:2970
+1429:1:810
+1430:0:2970
+1431:2:2241
+1432:0:2970
+1433:1:1087
+1434:1:1091
+1435:1:1092
+1436:1:1100
+1437:1:1101
+1438:1:1105
+1439:1:1106
+1440:1:1114
+1441:1:1119
+1442:1:1123
+1443:1:1124
+1444:1:1132
+1445:1:1133
+1446:1:1137
+1447:1:1138
+1448:1:1132
+1449:1:1133
+1450:1:1137
+1451:1:1138
+1452:1:1146
+1453:1:1151
+1454:1:1152
+1455:1:1163
+1456:1:1164
+1457:1:1165
+1458:1:1176
+1459:1:1181
+1460:1:1182
+1461:1:1193
+1462:1:1194
+1463:1:1195
+1464:1:1193
+1465:1:1201
+1466:1:1202
+1467:1:1206
+1468:1:1210
+1469:0:2970
+1470:2:2242
+1471:0:2970
+1472:1:812
+1473:1:813
+1474:0:2968
+1475:1:40
+1476:0:2974
+1477:1:1060