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

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