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

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