X-Git-Url: https://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Furcu-nosched-model%2Fresult-signal-over-reader%2Furcu_free_no_mb.spin.input.trail;fp=formal-model%2Furcu-nosched-model%2Fresult-signal-over-reader%2Furcu_free_no_mb.spin.input.trail;h=d437aad29d928d36ccb12d71e6ae6980a15310a9;hb=06e8b2a87f862183a26e0005bf04221633f49d0c;hp=0000000000000000000000000000000000000000;hpb=8322221dc666e720badeb06bc780a1f8e69020a0;p=urcu.git

diff --git a/formal-model/urcu-nosched-model/result-signal-over-reader/urcu_free_no_mb.spin.input.trail b/formal-model/urcu-nosched-model/result-signal-over-reader/urcu_free_no_mb.spin.input.trail
new file mode 100644
index 0000000..d437aad
--- /dev/null
+++ b/formal-model/urcu-nosched-model/result-signal-over-reader/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,2144 @@
+-2:4:-2
+-4:-4:-4
+1:0:3107
+2:4:3059
+3:4:3062
+4:4:3062
+5:4:3065
+6:4:3073
+7:4:3073
+8:4:3076
+9:4:3082
+10:4:3086
+11:4:3086
+12:4:3089
+13:4:3097
+14:4:3101
+15:4:3102
+16:0:3107
+17:4:3104
+18:0:3107
+19:3:869
+20:0:3107
+21:3:875
+22:0:3107
+23:3:876
+24:0:3107
+25:3:877
+26:3:881
+27:3:882
+28:3:890
+29:3:891
+30:3:895
+31:3:896
+32:3:904
+33:3:909
+34:3:913
+35:3:914
+36:3:921
+37:3:922
+38:3:933
+39:3:934
+40:3:935
+41:3:946
+42:3:951
+43:3:952
+44:0:3107
+45:3:964
+46:0:3107
+47:3:966
+48:3:967
+49:0:3107
+50:3:971
+51:3:975
+52:3:976
+53:3:984
+54:3:985
+55:3:989
+56:3:990
+57:3:998
+58:3:1003
+59:3:1004
+60:3:1015
+61:3:1016
+62:3:1027
+63:3:1028
+64:3:1029
+65:3:1040
+66:3:1045
+67:3:1046
+68:0:3107
+69:3:1058
+70:0:3107
+71:3:1060
+72:0:3107
+73:3:1061
+74:0:3107
+75:3:1071
+76:0:3107
+77:3:1072
+78:3:1076
+79:3:1077
+80:3:1085
+81:3:1086
+82:3:1090
+83:3:1091
+84:3:1099
+85:3:1104
+86:3:1108
+87:3:1109
+88:3:1116
+89:3:1117
+90:3:1128
+91:3:1129
+92:3:1130
+93:3:1141
+94:3:1146
+95:3:1147
+96:0:3107
+97:3:1162
+98:0:3107
+99:3:1163
+100:3:1167
+101:3:1168
+102:3:1176
+103:3:1177
+104:3:1181
+105:3:1182
+106:3:1190
+107:3:1195
+108:3:1199
+109:3:1200
+110:3:1207
+111:3:1208
+112:3:1219
+113:3:1220
+114:3:1221
+115:3:1232
+116:3:1237
+117:3:1238
+118:0:3107
+119:3:1253
+120:0:3107
+121:3:1258
+122:3:1262
+123:3:1263
+124:3:1271
+125:3:1272
+126:3:1276
+127:3:1277
+128:3:1285
+129:3:1290
+130:3:1294
+131:3:1295
+132:3:1302
+133:3:1303
+134:3:1314
+135:3:1315
+136:3:1316
+137:3:1327
+138:3:1332
+139:3:1333
+140:0:3107
+141:3:1348
+142:0:3107
+143:3:1350
+144:0:3107
+145:3:1351
+146:3:1355
+147:3:1356
+148:3:1364
+149:3:1365
+150:3:1369
+151:3:1370
+152:3:1378
+153:3:1383
+154:3:1387
+155:3:1388
+156:3:1395
+157:3:1396
+158:3:1407
+159:3:1408
+160:3:1409
+161:3:1420
+162:3:1425
+163:3:1426
+164:0:3107
+165:3:1438
+166:0:3107
+167:3:1440
+168:0:3107
+169:3:1443
+170:3:1444
+171:3:1456
+172:3:1457
+173:3:1461
+174:3:1462
+175:3:1470
+176:3:1475
+177:3:1479
+178:3:1480
+179:3:1487
+180:3:1488
+181:3:1499
+182:3:1500
+183:3:1501
+184:3:1512
+185:3:1517
+186:3:1518
+187:0:3107
+188:3:1530
+189:0:3107
+190:3:1532
+191:0:3107
+192:3:1533
+193:0:3107
+194:3:1534
+195:0:3107
+196:3:1535
+197:0:3107
+198:3:1536
+199:3:1540
+200:3:1541
+201:3:1549
+202:3:1550
+203:3:1554
+204:3:1555
+205:3:1563
+206:3:1568
+207:3:1572
+208:3:1573
+209:3:1580
+210:3:1581
+211:3:1592
+212:3:1593
+213:3:1594
+214:3:1605
+215:3:1610
+216:3:1611
+217:0:3107
+218:3:1623
+219:0:3107
+220:3:1904
+221:0:3107
+222:3:2002
+223:0:3107
+224:3:2003
+225:0:3107
+226:3:2007
+227:0:3107
+228:3:2013
+229:3:2017
+230:3:2018
+231:3:2026
+232:3:2027
+233:3:2031
+234:3:2032
+235:3:2040
+236:3:2045
+237:3:2049
+238:3:2050
+239:3:2057
+240:3:2058
+241:3:2069
+242:3:2070
+243:3:2071
+244:3:2082
+245:3:2087
+246:3:2088
+247:0:3107
+248:3:2100
+249:0:3107
+250:3:2102
+251:0:3107
+252:3:2103
+253:3:2107
+254:3:2108
+255:3:2116
+256:3:2117
+257:3:2121
+258:3:2122
+259:3:2130
+260:3:2135
+261:3:2139
+262:3:2140
+263:3:2147
+264:3:2148
+265:3:2159
+266:3:2160
+267:3:2161
+268:3:2172
+269:3:2177
+270:3:2178
+271:0:3107
+272:3:2190
+273:0:3107
+274:3:2192
+275:0:3107
+276:3:2195
+277:3:2196
+278:3:2208
+279:3:2209
+280:3:2213
+281:3:2214
+282:3:2222
+283:3:2227
+284:3:2231
+285:3:2232
+286:3:2239
+287:3:2240
+288:3:2251
+289:3:2252
+290:3:2253
+291:3:2264
+292:3:2269
+293:3:2270
+294:0:3107
+295:3:2282
+296:0:3107
+297:3:2284
+298:0:3107
+299:3:2285
+300:0:3107
+301:3:2286
+302:0:3107
+303:3:2287
+304:0:3107
+305:3:2288
+306:3:2292
+307:3:2293
+308:3:2301
+309:3:2302
+310:3:2306
+311:3:2307
+312:3:2315
+313:3:2320
+314:3:2324
+315:3:2325
+316:3:2332
+317:3:2333
+318:3:2344
+319:3:2345
+320:3:2346
+321:3:2357
+322:3:2362
+323:3:2363
+324:0:3107
+325:3:2375
+326:0:3107
+327:3:2656
+328:0:3107
+329:3:2754
+330:0:3107
+331:3:2755
+332:0:3107
+333:3:2759
+334:0:3107
+335:3:2765
+336:3:2769
+337:3:2770
+338:3:2778
+339:3:2779
+340:3:2783
+341:3:2784
+342:3:2792
+343:3:2797
+344:3:2801
+345:3:2802
+346:3:2809
+347:3:2810
+348:3:2821
+349:3:2822
+350:3:2823
+351:3:2834
+352:3:2839
+353:3:2840
+354:0:3107
+355:3:2855
+356:0:3107
+357:3:2856
+358:3:2860
+359:3:2861
+360:3:2869
+361:3:2870
+362:3:2874
+363:3:2875
+364:3:2883
+365:3:2888
+366:3:2892
+367:3:2893
+368:3:2900
+369:3:2901
+370:3:2912
+371:3:2913
+372:3:2914
+373:3:2925
+374:3:2930
+375:3:2931
+376:0:3107
+377:3:2946
+378:0:3107
+379:3:2951
+380:3:2955
+381:3:2956
+382:3:2964
+383:3:2965
+384:3:2969
+385:3:2970
+386:3:2978
+387:3:2983
+388:3:2987
+389:3:2988
+390:3:2995
+391:3:2996
+392:3:3007
+393:3:3008
+394:3:3009
+395:3:3020
+396:3:3025
+397:3:3026
+398:0:3107
+399:3:3041
+400:0:3107
+401:3:3043
+402:0:3107
+403:3:3044
+404:0:3107
+405:3:876
+406:0:3107
+407:3:877
+408:3:881
+409:3:882
+410:3:890
+411:3:891
+412:3:895
+413:3:896
+414:3:904
+415:3:909
+416:3:913
+417:3:914
+418:3:921
+419:3:922
+420:3:933
+421:3:934
+422:3:935
+423:3:946
+424:3:951
+425:3:952
+426:0:3107
+427:3:964
+428:0:3107
+429:3:966
+430:3:967
+431:0:3107
+432:3:971
+433:3:975
+434:3:976
+435:3:984
+436:3:985
+437:3:989
+438:3:990
+439:3:998
+440:3:1003
+441:3:1004
+442:3:1015
+443:3:1016
+444:3:1027
+445:3:1028
+446:3:1029
+447:3:1040
+448:3:1045
+449:3:1046
+450:0:3107
+451:3:1058
+452:0:3107
+453:3:1060
+454:0:3107
+455:3:1061
+456:0:3107
+457:3:1071
+458:0:3107
+459:3:1072
+460:3:1076
+461:3:1077
+462:3:1085
+463:3:1086
+464:3:1090
+465:3:1091
+466:3:1099
+467:3:1104
+468:3:1108
+469:3:1109
+470:3:1116
+471:3:1117
+472:3:1128
+473:3:1129
+474:3:1130
+475:3:1141
+476:3:1146
+477:3:1147
+478:0:3107
+479:3:1162
+480:0:3107
+481:3:1163
+482:3:1167
+483:3:1168
+484:3:1176
+485:3:1177
+486:3:1181
+487:3:1182
+488:3:1190
+489:3:1195
+490:3:1199
+491:3:1200
+492:3:1207
+493:3:1208
+494:3:1219
+495:3:1220
+496:3:1221
+497:3:1232
+498:3:1237
+499:3:1238
+500:0:3107
+501:3:1253
+502:0:3107
+503:3:1258
+504:3:1262
+505:3:1263
+506:3:1271
+507:3:1272
+508:3:1276
+509:3:1277
+510:3:1285
+511:3:1290
+512:3:1294
+513:3:1295
+514:3:1302
+515:3:1303
+516:3:1314
+517:3:1315
+518:3:1316
+519:3:1327
+520:3:1332
+521:3:1333
+522:0:3107
+523:3:1348
+524:0:3107
+525:3:1350
+526:0:3107
+527:3:1351
+528:3:1355
+529:3:1356
+530:3:1364
+531:3:1365
+532:3:1369
+533:3:1370
+534:3:1378
+535:3:1383
+536:3:1387
+537:3:1388
+538:3:1395
+539:3:1396
+540:3:1407
+541:3:1408
+542:3:1409
+543:3:1420
+544:3:1425
+545:3:1426
+546:0:3107
+547:3:1438
+548:0:3107
+549:3:1440
+550:0:3107
+551:3:1443
+552:3:1444
+553:3:1456
+554:3:1457
+555:3:1461
+556:3:1462
+557:3:1470
+558:3:1475
+559:3:1479
+560:3:1480
+561:3:1487
+562:3:1488
+563:3:1499
+564:3:1500
+565:3:1501
+566:3:1512
+567:3:1517
+568:3:1518
+569:0:3107
+570:3:1530
+571:0:3107
+572:3:1532
+573:0:3107
+574:3:1533
+575:0:3107
+576:3:1534
+577:0:3107
+578:3:1535
+579:0:3107
+580:3:1536
+581:3:1540
+582:3:1541
+583:3:1549
+584:3:1550
+585:3:1554
+586:3:1555
+587:3:1563
+588:3:1568
+589:3:1572
+590:3:1573
+591:3:1580
+592:3:1581
+593:3:1592
+594:3:1593
+595:3:1594
+596:3:1605
+597:3:1610
+598:3:1611
+599:0:3107
+600:3:1623
+601:0:3107
+602:3:1904
+603:0:3107
+604:3:2002
+605:0:3107
+606:3:2003
+607:0:3107
+608:3:2007
+609:0:3107
+610:3:2013
+611:3:2017
+612:3:2018
+613:3:2026
+614:3:2027
+615:3:2031
+616:3:2032
+617:3:2040
+618:3:2045
+619:3:2049
+620:3:2050
+621:3:2057
+622:3:2058
+623:3:2069
+624:3:2070
+625:3:2071
+626:3:2082
+627:3:2087
+628:3:2088
+629:0:3107
+630:3:2100
+631:0:3107
+632:3:2102
+633:0:3107
+634:3:2103
+635:3:2107
+636:3:2108
+637:3:2116
+638:3:2117
+639:3:2121
+640:3:2122
+641:3:2130
+642:3:2135
+643:3:2139
+644:3:2140
+645:3:2147
+646:3:2148
+647:3:2159
+648:3:2160
+649:3:2161
+650:3:2172
+651:3:2177
+652:3:2178
+653:0:3107
+654:3:2190
+655:0:3107
+656:3:2192
+657:0:3107
+658:3:2195
+659:3:2196
+660:3:2208
+661:3:2209
+662:3:2213
+663:3:2214
+664:3:2222
+665:3:2227
+666:3:2231
+667:3:2232
+668:3:2239
+669:3:2240
+670:3:2251
+671:3:2252
+672:3:2253
+673:3:2264
+674:3:2269
+675:3:2270
+676:0:3107
+677:3:2282
+678:0:3107
+679:3:2284
+680:0:3107
+681:3:2285
+682:0:3107
+683:3:2286
+684:0:3107
+685:3:2287
+686:0:3107
+687:3:2288
+688:3:2292
+689:3:2293
+690:3:2301
+691:3:2302
+692:3:2306
+693:3:2307
+694:3:2315
+695:3:2320
+696:3:2324
+697:3:2325
+698:3:2332
+699:3:2333
+700:3:2344
+701:3:2345
+702:3:2346
+703:3:2357
+704:3:2362
+705:3:2363
+706:0:3107
+707:3:2375
+708:0:3107
+709:3:2656
+710:0:3107
+711:3:2754
+712:0:3107
+713:3:2755
+714:0:3107
+715:3:2759
+716:0:3107
+717:3:2765
+718:3:2769
+719:3:2770
+720:3:2778
+721:3:2779
+722:3:2783
+723:3:2784
+724:3:2792
+725:3:2797
+726:3:2801
+727:3:2802
+728:3:2809
+729:3:2810
+730:3:2821
+731:3:2822
+732:3:2823
+733:3:2834
+734:3:2839
+735:3:2840
+736:0:3107
+737:3:2855
+738:0:3107
+739:3:2856
+740:3:2860
+741:3:2861
+742:3:2869
+743:3:2870
+744:3:2874
+745:3:2875
+746:3:2883
+747:3:2888
+748:3:2892
+749:3:2893
+750:3:2900
+751:3:2901
+752:3:2912
+753:3:2913
+754:3:2914
+755:3:2925
+756:3:2930
+757:3:2931
+758:0:3107
+759:3:2946
+760:0:3107
+761:3:2951
+762:3:2955
+763:3:2956
+764:3:2964
+765:3:2965
+766:3:2969
+767:3:2970
+768:3:2978
+769:3:2983
+770:3:2987
+771:3:2988
+772:3:2995
+773:3:2996
+774:3:3007
+775:3:3008
+776:3:3009
+777:3:3020
+778:3:3025
+779:3:3026
+780:0:3107
+781:3:3041
+782:0:3107
+783:3:3043
+784:0:3107
+785:3:3044
+786:0:3107
+787:3:876
+788:0:3107
+789:3:877
+790:3:881
+791:3:882
+792:3:890
+793:3:891
+794:3:895
+795:3:896
+796:3:904
+797:3:909
+798:3:913
+799:3:914
+800:3:921
+801:3:922
+802:3:933
+803:3:934
+804:3:935
+805:3:946
+806:3:951
+807:3:952
+808:0:3107
+809:3:964
+810:0:3107
+811:3:966
+812:3:967
+813:0:3107
+814:3:971
+815:3:975
+816:3:976
+817:3:984
+818:3:985
+819:3:989
+820:3:990
+821:3:998
+822:3:1003
+823:3:1004
+824:3:1015
+825:3:1016
+826:3:1027
+827:3:1028
+828:3:1029
+829:3:1040
+830:3:1045
+831:3:1046
+832:0:3107
+833:3:1058
+834:0:3107
+835:3:1060
+836:0:3107
+837:3:1061
+838:0:3107
+839:3:1071
+840:0:3107
+841:3:1072
+842:3:1076
+843:3:1077
+844:3:1085
+845:3:1086
+846:3:1090
+847:3:1091
+848:3:1099
+849:3:1104
+850:3:1108
+851:3:1109
+852:3:1116
+853:3:1117
+854:3:1128
+855:3:1129
+856:3:1130
+857:3:1141
+858:3:1146
+859:3:1147
+860:0:3107
+861:3:1162
+862:0:3107
+863:3:1163
+864:3:1167
+865:3:1168
+866:3:1176
+867:3:1177
+868:3:1181
+869:3:1182
+870:3:1190
+871:3:1195
+872:3:1199
+873:3:1200
+874:3:1207
+875:3:1208
+876:3:1219
+877:3:1220
+878:3:1221
+879:3:1232
+880:3:1237
+881:3:1238
+882:0:3107
+883:3:1253
+884:0:3107
+885:3:1258
+886:3:1262
+887:3:1263
+888:3:1271
+889:3:1272
+890:3:1276
+891:3:1277
+892:3:1285
+893:3:1290
+894:3:1294
+895:3:1295
+896:3:1302
+897:3:1303
+898:3:1314
+899:3:1315
+900:3:1316
+901:3:1327
+902:3:1332
+903:3:1333
+904:0:3107
+905:3:1348
+906:0:3107
+907:3:1350
+908:0:3107
+909:3:1351
+910:3:1355
+911:3:1356
+912:3:1364
+913:3:1365
+914:3:1369
+915:3:1370
+916:3:1378
+917:3:1383
+918:3:1387
+919:3:1388
+920:3:1395
+921:3:1396
+922:3:1407
+923:3:1408
+924:3:1409
+925:3:1420
+926:3:1425
+927:3:1426
+928:0:3107
+929:3:1438
+930:0:3107
+931:3:1440
+932:0:3107
+933:3:1443
+934:3:1444
+935:3:1456
+936:3:1457
+937:3:1461
+938:3:1462
+939:3:1470
+940:3:1475
+941:3:1479
+942:3:1480
+943:3:1487
+944:3:1488
+945:3:1499
+946:3:1500
+947:3:1501
+948:3:1512
+949:3:1517
+950:3:1518
+951:0:3107
+952:3:1530
+953:0:3107
+954:3:1532
+955:0:3107
+956:3:1533
+957:0:3107
+958:3:1534
+959:0:3107
+960:3:1535
+961:0:3107
+962:3:1536
+963:3:1540
+964:3:1541
+965:3:1549
+966:3:1550
+967:3:1554
+968:3:1555
+969:3:1563
+970:3:1568
+971:3:1572
+972:3:1573
+973:3:1580
+974:3:1581
+975:3:1592
+976:3:1593
+977:3:1594
+978:3:1605
+979:3:1610
+980:3:1611
+981:0:3107
+982:3:1623
+983:0:3107
+984:3:1904
+985:0:3107
+986:3:2002
+987:0:3107
+988:3:2003
+989:0:3107
+990:3:2007
+991:0:3107
+992:3:2013
+993:3:2017
+994:3:2018
+995:3:2026
+996:3:2027
+997:3:2031
+998:3:2032
+999:3:2040
+1000:3:2045
+1001:3:2049
+1002:3:2050
+1003:3:2057
+1004:3:2058
+1005:3:2069
+1006:3:2070
+1007:3:2071
+1008:3:2082
+1009:3:2087
+1010:3:2088
+1011:0:3107
+1012:3:2100
+1013:0:3107
+1014:3:2102
+1015:0:3107
+1016:3:2103
+1017:3:2107
+1018:3:2108
+1019:3:2116
+1020:3:2117
+1021:3:2121
+1022:3:2122
+1023:3:2130
+1024:3:2135
+1025:3:2139
+1026:3:2140
+1027:3:2147
+1028:3:2148
+1029:3:2159
+1030:3:2160
+1031:3:2161
+1032:3:2172
+1033:3:2177
+1034:3:2178
+1035:0:3107
+1036:3:2190
+1037:0:3107
+1038:3:2192
+1039:0:3107
+1040:3:2195
+1041:3:2196
+1042:3:2208
+1043:3:2209
+1044:3:2213
+1045:3:2214
+1046:3:2222
+1047:3:2227
+1048:3:2231
+1049:3:2232
+1050:3:2239
+1051:3:2240
+1052:3:2251
+1053:3:2252
+1054:3:2253
+1055:3:2264
+1056:3:2269
+1057:3:2270
+1058:0:3107
+1059:3:2282
+1060:0:3107
+1061:3:2284
+1062:0:3107
+1063:3:2285
+1064:0:3107
+1065:3:2286
+1066:0:3107
+1067:3:2287
+1068:0:3107
+1069:3:2288
+1070:3:2292
+1071:3:2293
+1072:3:2301
+1073:3:2302
+1074:3:2306
+1075:3:2307
+1076:3:2315
+1077:3:2320
+1078:3:2324
+1079:3:2325
+1080:3:2332
+1081:3:2333
+1082:3:2344
+1083:3:2345
+1084:3:2346
+1085:3:2357
+1086:3:2362
+1087:3:2363
+1088:0:3107
+1089:3:2375
+1090:0:3107
+1091:3:2656
+1092:0:3107
+1093:3:2754
+1094:0:3107
+1095:3:2755
+1096:0:3107
+1097:3:2759
+1098:0:3107
+1099:3:2765
+1100:3:2769
+1101:3:2770
+1102:3:2778
+1103:3:2779
+1104:3:2783
+1105:3:2784
+1106:3:2792
+1107:3:2797
+1108:3:2801
+1109:3:2802
+1110:3:2809
+1111:3:2810
+1112:3:2821
+1113:3:2822
+1114:3:2823
+1115:3:2834
+1116:3:2839
+1117:3:2840
+1118:0:3107
+1119:3:2855
+1120:0:3107
+1121:3:2856
+1122:3:2860
+1123:3:2861
+1124:3:2869
+1125:3:2870
+1126:3:2874
+1127:3:2875
+1128:3:2883
+1129:3:2888
+1130:3:2892
+1131:3:2893
+1132:3:2900
+1133:3:2901
+1134:3:2912
+1135:3:2913
+1136:3:2914
+1137:3:2925
+1138:3:2930
+1139:3:2931
+1140:0:3107
+1141:3:2946
+1142:0:3107
+1143:3:2951
+1144:3:2955
+1145:3:2956
+1146:3:2964
+1147:3:2965
+1148:3:2969
+1149:3:2970
+1150:3:2978
+1151:3:2983
+1152:3:2987
+1153:3:2988
+1154:3:2995
+1155:3:2996
+1156:3:3007
+1157:3:3008
+1158:3:3009
+1159:3:3020
+1160:3:3025
+1161:3:3026
+1162:0:3107
+1163:3:3041
+1164:0:3107
+1165:3:3043
+1166:0:3107
+1167:3:3044
+1168:0:3107
+1169:3:876
+1170:0:3107
+1171:3:877
+1172:3:881
+1173:3:882
+1174:3:890
+1175:3:891
+1176:3:895
+1177:3:896
+1178:3:904
+1179:3:909
+1180:3:913
+1181:3:914
+1182:3:921
+1183:3:922
+1184:3:933
+1185:3:934
+1186:3:935
+1187:3:946
+1188:3:951
+1189:3:952
+1190:0:3107
+1191:3:964
+1192:0:3107
+1193:3:966
+1194:3:967
+1195:0:3107
+1196:3:971
+1197:3:975
+1198:3:976
+1199:3:984
+1200:3:985
+1201:3:989
+1202:3:990
+1203:3:998
+1204:3:1003
+1205:3:1004
+1206:3:1015
+1207:3:1016
+1208:3:1027
+1209:3:1028
+1210:3:1029
+1211:3:1040
+1212:3:1045
+1213:3:1046
+1214:0:3107
+1215:3:1058
+1216:0:3107
+1217:3:1060
+1218:0:3107
+1219:3:1061
+1220:0:3107
+1221:3:1071
+1222:0:3107
+1223:3:1072
+1224:3:1076
+1225:3:1077
+1226:3:1085
+1227:3:1086
+1228:3:1090
+1229:3:1091
+1230:3:1099
+1231:3:1104
+1232:3:1108
+1233:3:1109
+1234:3:1116
+1235:3:1117
+1236:3:1128
+1237:3:1129
+1238:3:1130
+1239:3:1141
+1240:3:1146
+1241:3:1147
+1242:0:3107
+1243:3:1162
+1244:0:3107
+1245:3:1163
+1246:3:1167
+1247:3:1168
+1248:3:1176
+1249:3:1177
+1250:3:1181
+1251:3:1182
+1252:3:1190
+1253:3:1195
+1254:3:1199
+1255:3:1200
+1256:3:1207
+1257:3:1208
+1258:3:1219
+1259:3:1220
+1260:3:1221
+1261:3:1232
+1262:3:1237
+1263:3:1238
+1264:0:3107
+1265:3:1253
+1266:0:3107
+1267:3:1258
+1268:3:1262
+1269:3:1263
+1270:3:1271
+1271:3:1272
+1272:3:1276
+1273:3:1277
+1274:3:1285
+1275:3:1290
+1276:3:1294
+1277:3:1295
+1278:3:1302
+1279:3:1303
+1280:3:1314
+1281:3:1315
+1282:3:1316
+1283:3:1327
+1284:3:1332
+1285:3:1333
+1286:0:3107
+1287:3:1348
+1288:0:3107
+1289:3:1350
+1290:0:3107
+1291:3:1351
+1292:3:1355
+1293:3:1356
+1294:3:1364
+1295:3:1365
+1296:3:1369
+1297:3:1370
+1298:3:1378
+1299:3:1383
+1300:3:1387
+1301:3:1388
+1302:3:1395
+1303:3:1396
+1304:3:1407
+1305:3:1408
+1306:3:1409
+1307:3:1420
+1308:3:1425
+1309:3:1426
+1310:0:3107
+1311:3:1438
+1312:0:3107
+1313:3:1440
+1314:0:3107
+1315:3:1443
+1316:3:1444
+1317:3:1456
+1318:3:1457
+1319:3:1461
+1320:3:1462
+1321:3:1470
+1322:3:1475
+1323:3:1479
+1324:3:1480
+1325:3:1487
+1326:3:1488
+1327:3:1499
+1328:3:1500
+1329:3:1501
+1330:3:1512
+1331:3:1517
+1332:3:1518
+1333:0:3107
+1334:3:1530
+1335:0:3107
+1336:3:1532
+1337:0:3107
+1338:3:1533
+1339:0:3107
+1340:3:1534
+1341:0:3107
+1342:3:1535
+1343:0:3107
+1344:3:1536
+1345:3:1540
+1346:3:1541
+1347:3:1549
+1348:3:1550
+1349:3:1554
+1350:3:1555
+1351:3:1563
+1352:3:1568
+1353:3:1572
+1354:3:1573
+1355:3:1580
+1356:3:1581
+1357:3:1592
+1358:3:1593
+1359:3:1594
+1360:3:1605
+1361:3:1610
+1362:3:1611
+1363:0:3107
+1364:3:1623
+1365:0:3107
+1366:3:1904
+1367:0:3107
+1368:3:2002
+1369:0:3107
+1370:3:2003
+1371:0:3107
+1372:3:2007
+1373:0:3107
+1374:3:2013
+1375:3:2017
+1376:3:2018
+1377:3:2026
+1378:3:2027
+1379:3:2031
+1380:3:2032
+1381:3:2040
+1382:3:2045
+1383:3:2049
+1384:3:2050
+1385:3:2057
+1386:3:2058
+1387:3:2069
+1388:3:2070
+1389:3:2071
+1390:3:2082
+1391:3:2087
+1392:3:2088
+1393:0:3107
+1394:3:2100
+1395:0:3107
+1396:3:2102
+1397:0:3107
+1398:3:2103
+1399:3:2107
+1400:3:2108
+1401:3:2116
+1402:3:2117
+1403:3:2121
+1404:3:2122
+1405:3:2130
+1406:3:2135
+1407:3:2139
+1408:3:2140
+1409:3:2147
+1410:3:2148
+1411:3:2159
+1412:3:2160
+1413:3:2161
+1414:3:2172
+1415:3:2177
+1416:3:2178
+1417:0:3107
+1418:3:2190
+1419:0:3107
+1420:3:2192
+1421:0:3107
+1422:3:2195
+1423:3:2196
+1424:3:2208
+1425:3:2209
+1426:3:2213
+1427:3:2214
+1428:3:2222
+1429:3:2227
+1430:3:2231
+1431:3:2232
+1432:3:2239
+1433:3:2240
+1434:3:2251
+1435:3:2252
+1436:3:2253
+1437:3:2264
+1438:3:2269
+1439:3:2270
+1440:0:3107
+1441:3:2282
+1442:0:3107
+1443:3:2284
+1444:0:3107
+1445:3:2285
+1446:0:3107
+1447:3:2286
+1448:0:3107
+1449:3:2287
+1450:0:3107
+1451:3:2288
+1452:3:2292
+1453:3:2293
+1454:3:2301
+1455:3:2302
+1456:3:2306
+1457:3:2307
+1458:3:2315
+1459:3:2320
+1460:3:2324
+1461:3:2325
+1462:3:2332
+1463:3:2333
+1464:3:2344
+1465:3:2345
+1466:3:2346
+1467:3:2357
+1468:3:2362
+1469:3:2363
+1470:0:3107
+1471:3:2375
+1472:0:3107
+1473:3:2656
+1474:0:3107
+1475:3:2754
+1476:0:3107
+1477:3:2755
+1478:0:3107
+1479:3:2759
+1480:0:3107
+1481:3:2765
+1482:3:2769
+1483:3:2770
+1484:3:2778
+1485:3:2779
+1486:3:2783
+1487:3:2784
+1488:3:2792
+1489:3:2797
+1490:3:2801
+1491:3:2802
+1492:3:2809
+1493:3:2810
+1494:3:2821
+1495:3:2822
+1496:3:2823
+1497:3:2834
+1498:3:2839
+1499:3:2840
+1500:0:3107
+1501:3:2855
+1502:0:3107
+1503:3:2856
+1504:3:2860
+1505:3:2861
+1506:3:2869
+1507:3:2870
+1508:3:2874
+1509:3:2875
+1510:3:2883
+1511:3:2888
+1512:3:2892
+1513:3:2893
+1514:3:2900
+1515:3:2901
+1516:3:2912
+1517:3:2913
+1518:3:2914
+1519:3:2925
+1520:3:2930
+1521:3:2931
+1522:0:3107
+1523:3:2946
+1524:0:3107
+1525:3:2951
+1526:3:2955
+1527:3:2956
+1528:3:2964
+1529:3:2965
+1530:3:2969
+1531:3:2970
+1532:3:2978
+1533:3:2983
+1534:3:2987
+1535:3:2988
+1536:3:2995
+1537:3:2996
+1538:3:3007
+1539:3:3008
+1540:3:3009
+1541:3:3020
+1542:3:3025
+1543:3:3026
+1544:0:3107
+1545:3:3041
+1546:0:3107
+1547:3:3043
+1548:0:3107
+1549:3:3044
+1550:0:3107
+1551:3:876
+1552:0:3107
+1553:3:877
+1554:3:881
+1555:3:882
+1556:3:890
+1557:3:891
+1558:3:895
+1559:3:896
+1560:3:904
+1561:3:909
+1562:3:913
+1563:3:914
+1564:3:921
+1565:3:922
+1566:3:933
+1567:3:934
+1568:3:935
+1569:3:946
+1570:3:951
+1571:3:952
+1572:0:3107
+1573:3:964
+1574:0:3107
+1575:3:966
+1576:3:967
+1577:0:3107
+1578:3:971
+1579:3:975
+1580:3:976
+1581:3:984
+1582:3:985
+1583:3:989
+1584:3:990
+1585:3:998
+1586:3:1011
+1587:3:1012
+1588:3:1015
+1589:3:1016
+1590:3:1027
+1591:3:1028
+1592:3:1029
+1593:3:1040
+1594:3:1045
+1595:3:1048
+1596:3:1049
+1597:0:3107
+1598:3:1058
+1599:0:3107
+1600:3:1060
+1601:0:3107
+1602:3:1061
+1603:0:3107
+1604:3:1071
+1605:0:3107
+1606:3:1072
+1607:3:1076
+1608:3:1077
+1609:3:1085
+1610:3:1086
+1611:3:1090
+1612:3:1091
+1613:3:1099
+1614:3:1112
+1615:3:1113
+1616:3:1116
+1617:3:1117
+1618:3:1128
+1619:3:1129
+1620:3:1130
+1621:3:1141
+1622:3:1146
+1623:3:1149
+1624:3:1150
+1625:0:3107
+1626:3:1162
+1627:0:3107
+1628:3:1163
+1629:3:1167
+1630:3:1168
+1631:3:1176
+1632:3:1177
+1633:3:1181
+1634:3:1182
+1635:3:1190
+1636:3:1203
+1637:3:1204
+1638:3:1207
+1639:3:1208
+1640:3:1219
+1641:3:1220
+1642:3:1221
+1643:3:1232
+1644:3:1237
+1645:3:1240
+1646:3:1241
+1647:0:3107
+1648:3:1253
+1649:0:3107
+1650:3:1258
+1651:3:1262
+1652:3:1263
+1653:3:1271
+1654:3:1272
+1655:3:1276
+1656:3:1277
+1657:3:1285
+1658:3:1298
+1659:3:1299
+1660:3:1302
+1661:3:1303
+1662:3:1314
+1663:3:1315
+1664:3:1316
+1665:3:1327
+1666:3:1332
+1667:3:1335
+1668:3:1336
+1669:0:3107
+1670:3:1348
+1671:0:3107
+1672:3:1350
+1673:0:3107
+1674:3:1351
+1675:3:1355
+1676:3:1356
+1677:3:1364
+1678:3:1365
+1679:3:1369
+1680:3:1370
+1681:3:1378
+1682:3:1391
+1683:3:1392
+1684:3:1395
+1685:3:1396
+1686:3:1407
+1687:3:1408
+1688:3:1409
+1689:3:1420
+1690:3:1425
+1691:3:1428
+1692:3:1429
+1693:0:3107
+1694:3:1438
+1695:0:3107
+1696:3:1440
+1697:0:3107
+1698:3:1443
+1699:3:1444
+1700:3:1456
+1701:3:1457
+1702:3:1461
+1703:3:1462
+1704:3:1470
+1705:3:1483
+1706:3:1484
+1707:3:1487
+1708:3:1488
+1709:3:1499
+1710:3:1500
+1711:3:1501
+1712:3:1512
+1713:3:1517
+1714:3:1520
+1715:3:1521
+1716:0:3107
+1717:3:1530
+1718:0:3107
+1719:3:1532
+1720:0:3107
+1721:3:1533
+1722:0:3107
+1723:3:1534
+1724:0:3107
+1725:3:1535
+1726:0:3107
+1727:3:1536
+1728:3:1540
+1729:3:1541
+1730:3:1549
+1731:3:1550
+1732:3:1554
+1733:3:1555
+1734:3:1563
+1735:3:1576
+1736:3:1577
+1737:3:1580
+1738:3:1581
+1739:3:1592
+1740:3:1593
+1741:3:1594
+1742:3:1605
+1743:3:1610
+1744:3:1613
+1745:3:1614
+1746:0:3107
+1747:3:1623
+1748:0:3107
+1749:3:1904
+1750:0:3107
+1751:3:2002
+1752:0:3107
+1753:3:2003
+1754:0:3107
+1755:3:2007
+1756:0:3107
+1757:3:2013
+1758:3:2017
+1759:3:2018
+1760:3:2026
+1761:3:2027
+1762:3:2031
+1763:3:2032
+1764:3:2040
+1765:3:2053
+1766:3:2054
+1767:3:2057
+1768:3:2058
+1769:3:2069
+1770:3:2070
+1771:3:2071
+1772:3:2082
+1773:3:2087
+1774:3:2090
+1775:3:2091
+1776:0:3107
+1777:3:2100
+1778:0:3107
+1779:3:2102
+1780:0:3107
+1781:3:2103
+1782:3:2107
+1783:3:2108
+1784:3:2116
+1785:3:2117
+1786:3:2121
+1787:3:2122
+1788:3:2130
+1789:3:2143
+1790:3:2144
+1791:3:2147
+1792:3:2148
+1793:3:2159
+1794:3:2160
+1795:3:2161
+1796:3:2172
+1797:3:2177
+1798:3:2180
+1799:3:2181
+1800:0:3107
+1801:3:2190
+1802:0:3107
+1803:3:2192
+1804:0:3107
+1805:3:2195
+1806:3:2196
+1807:3:2208
+1808:3:2209
+1809:3:2213
+1810:3:2214
+1811:3:2222
+1812:3:2235
+1813:3:2236
+1814:3:2239
+1815:3:2240
+1816:3:2251
+1817:3:2252
+1818:3:2253
+1819:3:2264
+1820:3:2269
+1821:3:2272
+1822:3:2273
+1823:0:3107
+1824:3:2282
+1825:0:3107
+1826:3:2284
+1827:0:3107
+1828:3:2285
+1829:0:3107
+1830:3:2286
+1831:0:3107
+1832:3:2287
+1833:0:3107
+1834:3:2288
+1835:3:2292
+1836:3:2293
+1837:3:2301
+1838:3:2302
+1839:3:2306
+1840:3:2307
+1841:3:2315
+1842:3:2328
+1843:3:2329
+1844:3:2332
+1845:3:2333
+1846:3:2344
+1847:3:2345
+1848:3:2346
+1849:3:2357
+1850:3:2362
+1851:3:2365
+1852:3:2366
+1853:0:3107
+1854:3:2375
+1855:0:3107
+1856:3:2656
+1857:0:3107
+1858:3:2754
+1859:0:3107
+1860:3:2755
+1861:0:3107
+1862:3:2759
+1863:0:3107
+1864:3:2765
+1865:3:2769
+1866:3:2770
+1867:3:2778
+1868:3:2779
+1869:3:2783
+1870:3:2784
+1871:3:2792
+1872:3:2805
+1873:3:2806
+1874:3:2809
+1875:3:2810
+1876:3:2821
+1877:3:2822
+1878:3:2823
+1879:3:2834
+1880:3:2839
+1881:3:2842
+1882:3:2843
+1883:0:3107
+1884:3:2855
+1885:0:3107
+1886:3:2856
+1887:3:2860
+1888:3:2861
+1889:3:2869
+1890:3:2870
+1891:3:2874
+1892:3:2875
+1893:3:2883
+1894:3:2896
+1895:3:2897
+1896:3:2900
+1897:3:2901
+1898:3:2912
+1899:3:2913
+1900:3:2914
+1901:3:2925
+1902:3:2930
+1903:3:2933
+1904:3:2934
+1905:0:3107
+1906:3:2946
+1907:0:3107
+1908:3:2951
+1909:3:2955
+1910:3:2956
+1911:3:2964
+1912:3:2965
+1913:3:2969
+1914:3:2970
+1915:3:2978
+1916:3:2991
+1917:3:2992
+1918:3:2995
+1919:3:2996
+1920:3:3007
+1921:3:3008
+1922:3:3009
+1923:3:3020
+1924:3:3025
+1925:3:3028
+1926:3:3029
+1927:0:3107
+1928:3:3041
+1929:0:3107
+1930:3:3043
+1931:0:3107
+1932:3:3044
+1933:0:3107
+1934:3:3047
+1935:0:3107
+1936:3:3052
+1937:0:3107
+1938:2:458
+1939:0:3107
+1940:3:3053
+1941:0:3107
+1942:2:464
+1943:0:3107
+1944:3:3052
+1945:0:3107
+1946:2:465
+1947:0:3107
+1948:3:3053
+1949:0:3107
+1950:2:466
+1951:0:3107
+1952:3:3052
+1953:0:3107
+1954:2:467
+1955:0:3107
+1956:3:3053
+1957:0:3107
+1958:1:2
+1959:0:3107
+1960:3:3052
+1961:0:3107
+1962:2:468
+1963:0:3107
+1964:3:3053
+1965:0:3107
+1966:1:8
+1967:0:3107
+1968:3:3052
+1969:0:3107
+1970:2:467
+1971:0:3107
+1972:3:3053
+1973:0:3107
+1974:1:9
+1975:0:3107
+1976:3:3052
+1977:0:3107
+1978:2:468
+1979:0:3107
+1980:3:3053
+1981:0:3107
+1982:1:10
+1983:0:3107
+1984:3:3052
+1985:0:3107
+1986:2:467
+1987:0:3107
+1988:3:3053
+1989:0:3107
+1990:1:11
+1991:0:3107
+1992:3:3052
+1993:0:3107
+1994:2:468
+1995:0:3107
+1996:3:3053
+1997:0:3107
+1998:1:12
+1999:1:16
+2000:1:17
+2001:1:25
+2002:1:26
+2003:1:30
+2004:1:31
+2005:1:39
+2006:1:44
+2007:1:48
+2008:1:49
+2009:1:56
+2010:1:57
+2011:1:68
+2012:1:69
+2013:1:70
+2014:1:81
+2015:1:86
+2016:1:87
+2017:0:3107
+2018:3:3052
+2019:0:3107
+2020:2:467
+2021:0:3107
+2022:3:3053
+2023:0:3107
+2024:1:99
+2025:0:3107
+2026:3:3052
+2027:0:3107
+2028:2:468
+2029:0:3107
+2030:3:3053
+2031:0:3107
+2032:2:469
+2033:0:3107
+2034:3:3052
+2035:0:3107
+2036:2:475
+2037:0:3107
+2038:3:3053
+2039:0:3107
+2040:2:476
+2041:0:3107
+2042:3:3052
+2043:0:3107
+2044:2:477
+2045:2:481
+2046:2:482
+2047:2:490
+2048:2:491
+2049:2:495
+2050:2:496
+2051:2:504
+2052:2:509
+2053:2:513
+2054:2:514
+2055:2:521
+2056:2:522
+2057:2:533
+2058:2:534
+2059:2:535
+2060:2:546
+2061:2:551
+2062:2:552
+2063:0:3107
+2064:3:3053
+2065:0:3107
+2066:2:564
+2067:0:3107
+2068:3:3052
+2069:0:3107
+2070:2:565
+2071:2:569
+2072:2:570
+2073:2:578
+2074:2:579
+2075:2:583
+2076:2:584
+2077:2:592
+2078:2:597
+2079:2:601
+2080:2:602
+2081:2:609
+2082:2:610
+2083:2:621
+2084:2:622
+2085:2:623
+2086:2:634
+2087:2:639
+2088:2:640
+2089:0:3107
+2090:3:3053
+2091:0:3107
+2092:2:652
+2093:0:3107
+2094:3:3052
+2095:0:3107
+2096:2:653
+2097:0:3107
+2098:3:3053
+2099:0:3107
+2100:2:654
+2101:2:658
+2102:2:659
+2103:2:667
+2104:2:668
+2105:2:672
+2106:2:673
+2107:2:681
+2108:2:686
+2109:2:690
+2110:2:691
+2111:2:698
+2112:2:699
+2113:2:710
+2114:2:711
+2115:2:712
+2116:2:723
+2117:2:728
+2118:2:729
+2119:0:3107
+2120:3:3052
+2121:0:3107
+2122:2:741
+2123:0:3107
+2124:3:3053
+2125:0:3107
+2126:2:750
+2127:0:3107
+2128:3:3052
+2129:0:3107
+2130:2:753
+2131:0:3107
+2132:3:3053
+2133:0:3107
+2134:2:758
+2135:0:3107
+2136:3:3052
+2137:0:3107
+2138:2:759
+2139:0:3105
+2140:3:3053
+2141:0:3111
+2142:2:647