userspace-rcu formal model removal

[urcu.git] / formal-model / urcu / result-standard-execution-nonest / urcu_free_no_wmb.spin.input.trail

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