userspace-rcu formal model removal

[urcu.git] / formal-model / urcu / result-signal-over-writer / testmerge / urcu_free_no_rmb.spin.input.trail

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