ctmc 
 
module fpta_4000 
s:[1..1888] init 1;
[]s=1 -> 4.449000*21/45:(s'=2) +  4.449000 * 20/45:(s'=3) +  4.449000 * 2/45:(s'=4) +  4.449000 * 2/45:(s'=5);
[]s=2 -> 5.114831*9/20:(s'=6) +  5.114831 * 7/20:(s'=7) +  5.114831 * 1/20:(s'=8) +  5.114831 * 3/20:(s'=9);
[]s=3 -> 7.370112*6/19:(s'=10) +  7.370112 * 4/19:(s'=11) +  7.370112 * 3/19:(s'=12) +  7.370112 * 6/19:(s'=13);
[]s=4 -> 2.312005*1/2:(s'=14) +  2.312005 * 1/2:(s'=15);
[]s=5 -> 28.053245*1/2:(s'=16) +  28.053245 * 1/2:(s'=17);
[]s=6 -> 4.095063*4/8:(s'=18) +  4.095063 * 1/8:(s'=19) +  4.095063 * 3/8:(s'=20);
[]s=7 -> 4.899038*1/6:(s'=21) +  4.899038 * 2/6:(s'=22) +  4.899038 * 2/6:(s'=23) +  4.899038 * 1/6:(s'=24);
[]s=8 -> 110.402084*1/1:(s'=25);
[]s=9 -> 3.715262*2/2:(s'=26);
[]s=10 -> 5.140366*2/6:(s'=27) +  5.140366 * 2/6:(s'=28) +  5.140366 * 1/6:(s'=29) +  5.140366 * 1/6:(s'=30);
[]s=11 -> 4.360852*1/3:(s'=31) +  4.360852 * 1/3:(s'=32) +  4.360852 * 1/3:(s'=33);
[]s=12 -> 8.382019*1/3:(s'=34) +  8.382019 * 1/3:(s'=35) +  8.382019 * 1/3:(s'=36);
[]s=13 -> 3.864688*5/6:(s'=37) +  3.864688 * 1/6:(s'=38);
[]s=14 -> 2.959631*1/1:(s'=39);
[]s=15 -> 1.867135*1/1:(s'=40);
[]s=16 -> 92.353158*1/1:(s'=41);
[]s=17 -> 21.129141*1/1:(s'=42);
[]s=18 -> 8.599598*1/4:(s'=43) +  8.599598 * 1/4:(s'=44) +  8.599598 * 2/4:(s'=45);
[]s=19 -> 3.967309*1/1:(s'=46);
[]s=20 -> 2.739163*2/2:(s'=47);
[]s=21 -> 2.985699*1/1:(s'=48);
[]s=22 -> 4.048337*1/2:(s'=49) +  4.048337 * 1/2:(s'=50);
[]s=23 -> 12.301863*1/2:(s'=51) +  12.301863 * 1/2:(s'=52);
[]s=24 -> 11.286936*1/1:(s'=53);
[]s=25 -> 6.745363*1/1:(s'=54);
[]s=26 -> 8.815971*1/2:(s'=55) +  8.815971 * 1/2:(s'=56);
[]s=27 -> 24.095515*1/2:(s'=57) +  24.095515 * 1/2:(s'=58);
[]s=28 -> 4.557470*1/2:(s'=59) +  4.557470 * 1/2:(s'=60);
[]s=29 -> 87.305745*1/1:(s'=61);
[]s=30 -> 5.094763*1/1:(s'=62);
[]s=31 -> 3.277829*1/1:(s'=63);
[]s=32 -> 535.475234*1/1:(s'=64);
[]s=33 -> 3.794634*1/1:(s'=65);
[]s=34 -> 5.088023*1/1:(s'=66);
[]s=35 -> 4.973640*1/1:(s'=67);
[]s=36 -> 4.530422*1/1:(s'=68);
[]s=37 -> 4.502452*1/5:(s'=69) +  4.502452 * 2/5:(s'=70) +  4.502452 * 1/5:(s'=71) +  4.502452 * 1/5:(s'=72);
[]s=38 -> 4.764854*1/1:(s'=73);
[]s=39 -> 59.616072*1/1:(s'=74);
[]s=40 -> 6.253127*1/1:(s'=75);
[]s=41 -> 28.197609*1/1:(s'=76);
[]s=42 -> 2.260449*1/1:(s'=77);
[]s=43 -> 1 :(s'=43);
[]s=44 -> 148.431818*1/1:(s'=78);
[]s=45 -> 5.772122*2/2:(s'=79);
[]s=46 -> 14.497586*1/1:(s'=80);
[]s=47 -> 3.306605*2/2:(s'=81);
[]s=48 -> 5.918210*1/1:(s'=82);
[]s=49 -> 93.049223*1/1:(s'=83);
[]s=50 -> 16.613227*1/1:(s'=84);
[]s=51 -> 3.928038*1/1:(s'=85);
[]s=52 -> 5.347594*1/1:(s'=86);
[]s=53 -> 69.425160*1/1:(s'=87);
[]s=54 -> 43.410314*1/1:(s'=88);
[]s=55 -> 9.217439*1/1:(s'=89);
[]s=56 -> 16.341204*1/1:(s'=90);
[]s=57 -> 1 :(s'=57);
[]s=58 -> 2.776081*1/1:(s'=91);
[]s=59 -> 46.948357*1/1:(s'=92);
[]s=60 -> 29.609451*1/1:(s'=93);
[]s=61 -> 11.490027*1/1:(s'=94);
[]s=62 -> 1.605111*1/1:(s'=95);
[]s=63 -> 6.323511*1/1:(s'=96);
[]s=64 -> 1 :(s'=64);
[]s=65 -> 17.949777*1/1:(s'=97);
[]s=66 -> 6.146659*1/1:(s'=98);
[]s=67 -> 187.223845*1/1:(s'=99);
[]s=68 -> 7.584376*1/1:(s'=100);
[]s=69 -> 11.639276*1/1:(s'=101);
[]s=70 -> 3.801855*1/2:(s'=102) +  3.801855 * 1/2:(s'=103);
[]s=71 -> 11.880718*1/1:(s'=104);
[]s=72 -> 4.950005*1/1:(s'=105);
[]s=73 -> 9.697440*1/1:(s'=106);
[]s=74 -> 2.406913*1/1:(s'=107);
[]s=75 -> 5.904233*1/1:(s'=108);
[]s=76 -> 11.866901*1/1:(s'=109);
[]s=77 -> 7.390983*1/1:(s'=110);
[]s=78 -> 4.176935*1/1:(s'=111);
[]s=79 -> 6.173792*1/2:(s'=112) +  6.173792 * 1/2:(s'=113);
[]s=80 -> 31.871494*1/1:(s'=114);
[]s=81 -> 10.131918*1/2:(s'=115) +  10.131918 * 1/2:(s'=116);
[]s=82 -> 2.891594*1/1:(s'=117);
[]s=83 -> 342.829716*1/1:(s'=118);
[]s=84 -> 1.752941*1/1:(s'=119);
[]s=85 -> 4.734176*1/1:(s'=120);
[]s=86 -> 4.539059*1/1:(s'=121);
[]s=87 -> 1.279656*1/1:(s'=122);
[]s=88 -> 8.413967*1/1:(s'=123);
[]s=89 -> 42.389047*1/1:(s'=124);
[]s=90 -> 3.364172*1/1:(s'=125);
[]s=91 -> 3.678093*1/1:(s'=126);
[]s=92 -> 8.973439*1/1:(s'=127);
[]s=93 -> 18.580108*1/1:(s'=128);
[]s=94 -> 6.427975*1/1:(s'=129);
[]s=95 -> 35.968635*1/1:(s'=130);
[]s=96 -> 68.979789*1/1:(s'=131);
[]s=97 -> 16.827934*1/1:(s'=132);
[]s=98 -> 63.143272*1/1:(s'=133);
[]s=99 -> 12.846370*1/1:(s'=134);
[]s=100 -> 17.532172*1/1:(s'=135);
[]s=101 -> 3.081949*1/1:(s'=136);
[]s=102 -> 3.991857*1/1:(s'=137);
[]s=103 -> 2.788856*1/1:(s'=138);
[]s=104 -> 31.766201*1/1:(s'=139);
[]s=105 -> 1.768566*1/1:(s'=140);
[]s=106 -> 34.039077*1/1:(s'=141);
[]s=107 -> 6.925208*1/1:(s'=142);
[]s=108 -> 14.793337*1/1:(s'=143);
[]s=109 -> 1.345044*1/1:(s'=144);
[]s=110 -> 2.595919*1/1:(s'=145);
[]s=111 -> 12.274005*1/1:(s'=146);
[]s=112 -> 5.482456*1/1:(s'=147);
[]s=113 -> 84.445195*1/1:(s'=148);
[]s=114 -> 39.619651*1/1:(s'=149);
[]s=115 -> 5.462988*1/1:(s'=150);
[]s=116 -> 3.943684*1/1:(s'=151);
[]s=117 -> 3.576154*1/1:(s'=152);
[]s=118 -> 1.741159*1/1:(s'=153);
[]s=119 -> 2.638383*1/1:(s'=154);
[]s=120 -> 27.276943*1/1:(s'=155);
[]s=121 -> 2.284148*1/1:(s'=156);
[]s=122 -> 30.333364*1/1:(s'=157);
[]s=123 -> 7.816164*1/1:(s'=158);
[]s=124 -> 9.928515*1/1:(s'=159);
[]s=125 -> 0.566412*1/1:(s'=160);
[]s=126 -> 2.738226*1/1:(s'=161);
[]s=127 -> 2.697817*1/1:(s'=162);
[]s=128 -> 27.873787*1/1:(s'=163);
[]s=129 -> 15.139129*1/1:(s'=164);
[]s=130 -> 7.708317*1/1:(s'=165);
[]s=131 -> 16.748735*1/1:(s'=166);
[]s=132 -> 2.229804*1/1:(s'=167);
[]s=133 -> 3.583972*1/1:(s'=168);
[]s=134 -> 2.895110*1/1:(s'=169);
[]s=135 -> 8.409722*1/1:(s'=170);
[]s=136 -> 29.485478*1/1:(s'=171);
[]s=137 -> 2.862377*1/1:(s'=172);
[]s=138 -> 3.811411*1/1:(s'=173);
[]s=139 -> 2.338689*1/1:(s'=174);
[]s=140 -> 27.394258*1/1:(s'=175);
[]s=141 -> 3.713055*1/1:(s'=176);
[]s=142 -> 10.014822*1/1:(s'=177);
[]s=143 -> 16.561501*1/1:(s'=178);
[]s=144 -> 2.179504*1/1:(s'=179);
[]s=145 -> 10.697704*1/1:(s'=180);
[]s=146 -> 75.454614*1/1:(s'=181);
[]s=147 -> 4.936809*1/1:(s'=182);
[]s=148 -> 16.007684*1/1:(s'=183);
[]s=149 -> 3.822338*1/1:(s'=184);
[]s=150 -> 5.098399*1/1:(s'=185);
[]s=151 -> 88.012674*1/1:(s'=186);
[]s=152 -> 5.104124*1/1:(s'=187);
[]s=153 -> 106.970177*1/1:(s'=188);
[]s=154 -> 11.404589*1/1:(s'=189);
[]s=155 -> 53.450211*1/1:(s'=190);
[]s=156 -> 1.840976*1/1:(s'=191);
[]s=157 -> 9.236169*1/1:(s'=192);
[]s=158 -> 2.031818*1/1:(s'=193);
[]s=159 -> 32.071841*1/1:(s'=194);
[]s=160 -> 2.110862*1/1:(s'=195);
[]s=161 -> 7.157684*1/1:(s'=196);
[]s=162 -> 182.391887*1/1:(s'=197);
[]s=163 -> 5.314908*1/1:(s'=198);
[]s=164 -> 23.104293*1/1:(s'=199);
[]s=165 -> 12.089706*1/1:(s'=200);
[]s=166 -> 1.166072*1/1:(s'=201);
[]s=167 -> 1.284307*1/1:(s'=202);
[]s=168 -> 27.104678*1/1:(s'=203);
[]s=169 -> 1.689789*1/1:(s'=204);
[]s=170 -> 1.875152*1/1:(s'=205);
[]s=171 -> 3.043399*1/1:(s'=206);
[]s=172 -> 9.433072*1/1:(s'=207);
[]s=173 -> 7.007708*1/1:(s'=208);
[]s=174 -> 16.939104*1/1:(s'=209);
[]s=175 -> 14.827775*1/1:(s'=210);
[]s=176 -> 46.490005*1/1:(s'=211);
[]s=177 -> 1.984600*1/1:(s'=212);
[]s=178 -> 3.196114*1/1:(s'=213);
[]s=179 -> 2.555911*1/1:(s'=214);
[]s=180 -> 5.267594*1/1:(s'=215);
[]s=181 -> 53.679747*1/1:(s'=216);
[]s=182 -> 8.988764*1/1:(s'=217);
[]s=183 -> 2.307710*1/1:(s'=218);
[]s=184 -> 31.077133*1/1:(s'=219);
[]s=185 -> 69.449267*1/1:(s'=220);
[]s=186 -> 39.065552*1/1:(s'=221);
[]s=187 -> 3.972668*1/1:(s'=222);
[]s=188 -> 7.411800*1/1:(s'=223);
[]s=189 -> 24.121379*1/1:(s'=224);
[]s=190 -> 1.907487*1/1:(s'=225);
[]s=191 -> 2.344721*1/1:(s'=226);
[]s=192 -> 62.637018*1/1:(s'=227);
[]s=193 -> 3.316530*1/1:(s'=228);
[]s=194 -> 1.727653*1/1:(s'=229);
[]s=195 -> 1.685403*1/1:(s'=230);
[]s=196 -> 104.690117*1/1:(s'=231);
[]s=197 -> 8.616975*1/1:(s'=232);
[]s=198 -> 19.293845*1/1:(s'=233);
[]s=199 -> 18.168935*1/1:(s'=234);
[]s=200 -> 2.179266*1/1:(s'=235);
[]s=201 -> 2.698036*1/1:(s'=236);
[]s=202 -> 7.912644*1/1:(s'=237);
[]s=203 -> 1.995809*1/1:(s'=238);
[]s=204 -> 3.388567*1/1:(s'=239);
[]s=205 -> 1 :(s'=205);
[]s=206 -> 3.697815*1/1:(s'=240);
[]s=207 -> 4317.602867*1/1:(s'=241);
[]s=208 -> 4.794783*1/1:(s'=242);
[]s=209 -> 4.086470*1/1:(s'=243);
[]s=210 -> 4.341408*1/1:(s'=244);
[]s=211 -> 16.245370*1/1:(s'=245);
[]s=212 -> 12.263619*1/1:(s'=246);
[]s=213 -> 13.544630*1/1:(s'=247);
[]s=214 -> 5.068424*1/1:(s'=248);
[]s=215 -> 8.552125*1/1:(s'=249);
[]s=216 -> 14.167316*1/1:(s'=250);
[]s=217 -> 0.932749*1/1:(s'=251);
[]s=218 -> 9.929501*1/1:(s'=252);
[]s=219 -> 2.362056*1/1:(s'=253);
[]s=220 -> 5.382421*1/1:(s'=254);
[]s=221 -> 40.748136*1/1:(s'=255);
[]s=222 -> 200.260338*1/1:(s'=256);
[]s=223 -> 14.257200*1/1:(s'=257);
[]s=224 -> 9.620935*1/1:(s'=258);
[]s=225 -> 2.617938*1/1:(s'=259);
[]s=226 -> 2.687666*1/1:(s'=260);
[]s=227 -> 9.515653*1/1:(s'=261);
[]s=228 -> 2.272417*1/1:(s'=262);
[]s=229 -> 25.655498*1/1:(s'=263);
[]s=230 -> 7.573463*1/1:(s'=264);
[]s=231 -> 7.714264*1/1:(s'=265);
[]s=232 -> 3.448276*1/1:(s'=266);
[]s=233 -> 144.544180*1/1:(s'=267);
[]s=234 -> 53.163211*1/1:(s'=268);
[]s=235 -> 1.282249*1/1:(s'=269);
[]s=236 -> 3.035915*1/1:(s'=270);
[]s=237 -> 6.487609*1/1:(s'=271);
[]s=238 -> 1 :(s'=238);
[]s=239 -> 12.172262*1/1:(s'=272);
[]s=240 -> 46.257748*1/1:(s'=273);
[]s=241 -> 1.965757*1/1:(s'=274);
[]s=242 -> 2.038279*1/1:(s'=275);
[]s=243 -> 1.822789*1/1:(s'=276);
[]s=244 -> 4.188482*1/1:(s'=277);
[]s=245 -> 6.559958*1/1:(s'=278);
[]s=246 -> 63.869196*1/1:(s'=279);
[]s=247 -> 11.266463*1/1:(s'=280);
[]s=248 -> 15.966534*1/1:(s'=281);
[]s=249 -> 2.094197*1/1:(s'=282);
[]s=250 -> 2.598685*1/1:(s'=283);
[]s=251 -> 1 :(s'=251);
[]s=252 -> 4.194983*1/1:(s'=284);
[]s=253 -> 13.466381*1/1:(s'=285);
[]s=254 -> 6.452445*1/1:(s'=286);
[]s=255 -> 11.131395*1/1:(s'=287);
[]s=256 -> 4.162331*1/1:(s'=288);
[]s=257 -> 635.081926*1/1:(s'=289);
[]s=258 -> 12.980270*1/1:(s'=290);
[]s=259 -> 6.040106*1/1:(s'=291);
[]s=260 -> 6.495615*1/1:(s'=292);
[]s=261 -> 36.481704*1/1:(s'=293);
[]s=262 -> 12.136659*1/1:(s'=294);
[]s=263 -> 113.869278*1/1:(s'=295);
[]s=264 -> 1.663257*1/1:(s'=296);
[]s=265 -> 10.518455*1/1:(s'=297);
[]s=266 -> 7.327081*1/1:(s'=298);
[]s=267 -> 8.045700*1/1:(s'=299);
[]s=268 -> 17.981731*1/1:(s'=300);
[]s=269 -> 42.538710*1/1:(s'=301);
[]s=270 -> 13.959072*1/1:(s'=302);
[]s=271 -> 125.838398*1/1:(s'=303);
[]s=272 -> 7.019514*1/1:(s'=304);
[]s=273 -> 9.160026*1/1:(s'=305);
[]s=274 -> 10.634564*1/1:(s'=306);
[]s=275 -> 51.840332*1/1:(s'=307);
[]s=276 -> 3.035638*1/1:(s'=308);
[]s=277 -> 5.839416*1/1:(s'=309);
[]s=278 -> 16.664167*1/1:(s'=310);
[]s=279 -> 54.285869*1/1:(s'=311);
[]s=280 -> 9.160026*1/1:(s'=312);
[]s=281 -> 62.908908*1/1:(s'=313);
[]s=282 -> 3.258178*1/1:(s'=314);
[]s=283 -> 8.041817*1/1:(s'=315);
[]s=284 -> 24.156340*1/1:(s'=316);
[]s=285 -> 1.880406*1/1:(s'=317);
[]s=286 -> 9.187799*1/1:(s'=318);
[]s=287 -> 3.122853*1/1:(s'=319);
[]s=288 -> 1.549835*1/1:(s'=320);
[]s=289 -> 11.046672*1/1:(s'=321);
[]s=290 -> 1 :(s'=290);
[]s=291 -> 10.978877*1/1:(s'=322);
[]s=292 -> 1 :(s'=292);
[]s=293 -> 36.786345*1/1:(s'=323);
[]s=294 -> 1.819141*1/1:(s'=324);
[]s=295 -> 15.147613*1/1:(s'=325);
[]s=296 -> 5.621451*1/1:(s'=326);
[]s=297 -> 23.140649*1/1:(s'=327);
[]s=298 -> 2.082769*1/1:(s'=328);
[]s=299 -> 4.939491*1/1:(s'=329);
[]s=300 -> 9.209799*1/1:(s'=330);
[]s=301 -> 1.087796*1/1:(s'=331);
[]s=302 -> 2.693748*1/1:(s'=332);
[]s=303 -> 4.788355*1/1:(s'=333);
[]s=304 -> 25.310048*1/1:(s'=334);
[]s=305 -> 3.029110*1/1:(s'=335);
[]s=306 -> 4.276977*1/1:(s'=336);
[]s=307 -> 1 :(s'=307);
[]s=308 -> 2.354437*1/1:(s'=337);
[]s=309 -> 116.063138*1/1:(s'=338);
[]s=310 -> 8.599192*1/1:(s'=339);
[]s=311 -> 10.308322*1/1:(s'=340);
[]s=312 -> 12.147864*1/1:(s'=341);
[]s=313 -> 36.974044*1/1:(s'=342);
[]s=314 -> 6.436663*1/1:(s'=343);
[]s=315 -> 17.769880*1/1:(s'=344);
[]s=316 -> 11.066721*1/1:(s'=345);
[]s=317 -> 3.339344*1/1:(s'=346);
[]s=318 -> 4.977601*1/1:(s'=347);
[]s=319 -> 4.711425*1/1:(s'=348);
[]s=320 -> 3.221234*1/1:(s'=349);
[]s=321 -> 965.250965*1/1:(s'=350);
[]s=322 -> 4.565168*1/1:(s'=351);
[]s=323 -> 1.783231*1/1:(s'=352);
[]s=324 -> 8.404068*1/1:(s'=353);
[]s=325 -> 1.222539*1/1:(s'=354);
[]s=326 -> 2.512563*1/1:(s'=355);
[]s=327 -> 5.543545*1/1:(s'=356);
[]s=328 -> 18.913603*1/1:(s'=357);
[]s=329 -> 3.934839*1/1:(s'=358);
[]s=330 -> 32.863387*1/1:(s'=359);
[]s=331 -> 1.863377*1/1:(s'=360);
[]s=332 -> 31.348945*1/1:(s'=361);
[]s=333 -> 16.443582*1/1:(s'=362);
[]s=334 -> 144.164925*1/1:(s'=363);
[]s=335 -> 29.263725*1/1:(s'=364);
[]s=336 -> 1.723989*1/1:(s'=365);
[]s=337 -> 38.138825*1/1:(s'=366);
[]s=338 -> 1.610410*1/1:(s'=367);
[]s=339 -> 4.411116*1/1:(s'=368);
[]s=340 -> 32.684011*1/1:(s'=369);
[]s=341 -> 1.525902*1/1:(s'=370);
[]s=342 -> 5.250722*1/1:(s'=371);
[]s=343 -> 4.107451*1/1:(s'=372);
[]s=344 -> 1501.704435*1/1:(s'=373);
[]s=345 -> 8.094544*1/1:(s'=374);
[]s=346 -> 27.716186*1/1:(s'=375);
[]s=347 -> 3.835827*1/1:(s'=376);
[]s=348 -> 39.261877*1/1:(s'=377);
[]s=349 -> 22.255358*1/1:(s'=378);
[]s=350 -> 10.764958*1/1:(s'=379);
[]s=351 -> 8.233841*1/1:(s'=380);
[]s=352 -> 20.618557*1/1:(s'=381);
[]s=353 -> 4.802843*1/1:(s'=382);
[]s=354 -> 0.876962*1/1:(s'=383);
[]s=355 -> 48.132461*1/1:(s'=384);
[]s=356 -> 1 :(s'=356);
[]s=357 -> 2.691355*1/1:(s'=385);
[]s=358 -> 14.717786*1/1:(s'=386);
[]s=359 -> 5.838393*1/1:(s'=387);
[]s=360 -> 2.274588*1/1:(s'=388);
[]s=361 -> 21.629104*1/1:(s'=389);
[]s=362 -> 1.738193*1/1:(s'=390);
[]s=363 -> 4.843319*1/1:(s'=391);
[]s=364 -> 2.032644*1/1:(s'=392);
[]s=365 -> 6.680919*1/1:(s'=393);
[]s=366 -> 113.560227*1/1:(s'=394);
[]s=367 -> 1.936446*1/1:(s'=395);
[]s=368 -> 3.759540*1/1:(s'=396);
[]s=369 -> 11.169565*1/1:(s'=397);
[]s=370 -> 7.177205*1/1:(s'=398);
[]s=371 -> 14.372772*1/1:(s'=399);
[]s=372 -> 1.081104*1/1:(s'=400);
[]s=373 -> 1 :(s'=373);
[]s=374 -> 3.277292*1/1:(s'=401);
[]s=375 -> 6.698821*1/1:(s'=402);
[]s=376 -> 99.206349*1/1:(s'=403);
[]s=377 -> 6.768648*1/1:(s'=404);
[]s=378 -> 11.040574*1/1:(s'=405);
[]s=379 -> 5.829544*1/1:(s'=406);
[]s=380 -> 98.823994*1/1:(s'=407);
[]s=381 -> 26.852125*1/1:(s'=408);
[]s=382 -> 9.150805*1/1:(s'=409);
[]s=383 -> 2.656536*1/1:(s'=410);
[]s=384 -> 17.438920*1/1:(s'=411);
[]s=385 -> 1607.975559*1/1:(s'=412);
[]s=386 -> 14.677822*1/1:(s'=413);
[]s=387 -> 20.771452*1/1:(s'=414);
[]s=388 -> 18.745899*1/1:(s'=415);
[]s=389 -> 4.782172*1/1:(s'=416);
[]s=390 -> 9.983029*1/1:(s'=417);
[]s=391 -> 30.370213*1/1:(s'=418);
[]s=392 -> 67.244973*1/1:(s'=419);
[]s=393 -> 6.546216*1/1:(s'=420);
[]s=394 -> 1.909199*1/1:(s'=421);
[]s=395 -> 1 :(s'=395);
[]s=396 -> 2.195824*1/1:(s'=422);
[]s=397 -> 26.335194*1/1:(s'=423);
[]s=398 -> 0.720461*1/1:(s'=424);
[]s=399 -> 17.778410*1/1:(s'=425);
[]s=400 -> 7.038288*1/1:(s'=426);
[]s=401 -> 27.298537*1/1:(s'=427);
[]s=402 -> 3.693581*1/1:(s'=428);
[]s=403 -> 18.654628*1/1:(s'=429);
[]s=404 -> 17.322316*1/1:(s'=430);
[]s=405 -> 12.084300*1/1:(s'=431);
[]s=406 -> 72.700836*1/1:(s'=432);
[]s=407 -> 11.021834*1/1:(s'=433);
[]s=408 -> 3.382721*1/1:(s'=434);
[]s=409 -> 6.174745*1/1:(s'=435);
[]s=410 -> 4.804920*1/1:(s'=436);
[]s=411 -> 62.664494*1/1:(s'=437);
[]s=412 -> 18.381677*1/1:(s'=438);
[]s=413 -> 1.124379*1/1:(s'=439);
[]s=414 -> 6.091618*1/1:(s'=440);
[]s=415 -> 10.812447*1/1:(s'=441);
[]s=416 -> 9.542895*1/1:(s'=442);
[]s=417 -> 1.473210*1/1:(s'=443);
[]s=418 -> 1.543734*1/1:(s'=444);
[]s=419 -> 1.306233*1/1:(s'=445);
[]s=420 -> 7.867821*1/1:(s'=446);
[]s=421 -> 24.806509*1/1:(s'=447);
[]s=422 -> 16.256462*1/1:(s'=448);
[]s=423 -> 11.440731*1/1:(s'=449);
[]s=424 -> 1.300306*1/1:(s'=450);
[]s=425 -> 4.986536*1/1:(s'=451);
[]s=426 -> 4.075644*1/1:(s'=452);
[]s=427 -> 3.231749*1/1:(s'=453);
[]s=428 -> 40.901468*1/1:(s'=454);
[]s=429 -> 4.456129*1/1:(s'=455);
[]s=430 -> 4.120992*1/1:(s'=456);
[]s=431 -> 2.054780*1/1:(s'=457);
[]s=432 -> 2.483978*1/1:(s'=458);
[]s=433 -> 6.471235*1/1:(s'=459);
[]s=434 -> 13.788729*1/1:(s'=460);
[]s=435 -> 2.555127*1/1:(s'=461);
[]s=436 -> 5.639522*1/1:(s'=462);
[]s=437 -> 6.110229*1/1:(s'=463);
[]s=438 -> 4.143704*1/1:(s'=464);
[]s=439 -> 5.200208*1/1:(s'=465);
[]s=440 -> 14.019936*1/1:(s'=466);
[]s=441 -> 13.646102*1/1:(s'=467);
[]s=442 -> 20.350020*1/1:(s'=468);
[]s=443 -> 11.444004*1/1:(s'=469);
[]s=444 -> 1.546671*1/1:(s'=470);
[]s=445 -> 5.992689*1/1:(s'=471);
[]s=446 -> 23.685457*1/1:(s'=472);
[]s=447 -> 1.039458*1/1:(s'=473);
[]s=448 -> 4.456328*1/1:(s'=474);
[]s=449 -> 301.195747*1/1:(s'=475);
[]s=450 -> 13.455690*1/1:(s'=476);
[]s=451 -> 27.762354*1/1:(s'=477);
[]s=452 -> 1305.397820*1/1:(s'=478);
[]s=453 -> 1.312870*1/1:(s'=479);
[]s=454 -> 5.850006*1/1:(s'=480);
[]s=455 -> 9.887285*1/1:(s'=481);
[]s=456 -> 3.208934*1/1:(s'=482);
[]s=457 -> 4.945354*1/1:(s'=483);
[]s=458 -> 95.785441*1/1:(s'=484);
[]s=459 -> 3.240966*1/1:(s'=485);
[]s=460 -> 15.205888*1/1:(s'=486);
[]s=461 -> 264.137986*1/1:(s'=487);
[]s=462 -> 28.011989*1/1:(s'=488);
[]s=463 -> 17.269666*1/1:(s'=489);
[]s=464 -> 2.461599*1/1:(s'=490);
[]s=465 -> 7.245327*1/1:(s'=491);
[]s=466 -> 19.045442*1/1:(s'=492);
[]s=467 -> 7.498500*1/1:(s'=493);
[]s=468 -> 1 :(s'=468);
[]s=469 -> 3.382721*1/1:(s'=494);
[]s=470 -> 5.663156*1/1:(s'=495);
[]s=471 -> 2.408710*1/1:(s'=496);
[]s=472 -> 5.455537*1/1:(s'=497);
[]s=473 -> 3.267867*1/1:(s'=498);
[]s=474 -> 2.150676*1/1:(s'=499);
[]s=475 -> 12.058217*1/1:(s'=500);
[]s=476 -> 81.162243*1/1:(s'=501);
[]s=477 -> 3.752909*1/1:(s'=502);
[]s=478 -> 4.856727*1/1:(s'=503);
[]s=479 -> 632.511069*1/1:(s'=504);
[]s=480 -> 4.483099*1/1:(s'=505);
[]s=481 -> 35.806359*1/1:(s'=506);
[]s=482 -> 5.117969*1/1:(s'=507);
[]s=483 -> 1.442981*1/1:(s'=508);
[]s=484 -> 118.756383*1/1:(s'=509);
[]s=485 -> 5.765018*1/1:(s'=510);
[]s=486 -> 1.880265*1/1:(s'=511);
[]s=487 -> 3.479834*1/1:(s'=512);
[]s=488 -> 15.671770*1/1:(s'=513);
[]s=489 -> 7.346459*1/1:(s'=514);
[]s=490 -> 1 :(s'=490);
[]s=491 -> 4.845666*1/1:(s'=515);
[]s=492 -> 2.454470*1/1:(s'=516);
[]s=493 -> 3.326348*1/1:(s'=517);
[]s=494 -> 1.312836*1/1:(s'=518);
[]s=495 -> 2.004249*1/1:(s'=519);
[]s=496 -> 1.935359*1/1:(s'=520);
[]s=497 -> 90.843023*1/1:(s'=521);
[]s=498 -> 1 :(s'=498);
[]s=499 -> 12.322555*1/1:(s'=522);
[]s=500 -> 20.347950*1/1:(s'=523);
[]s=501 -> 8.649771*1/1:(s'=524);
[]s=502 -> 4.451963*1/1:(s'=525);
[]s=503 -> 11.727041*1/1:(s'=526);
[]s=504 -> 4.579803*1/1:(s'=527);
[]s=505 -> 5.468066*1/1:(s'=528);
[]s=506 -> 24.109166*1/1:(s'=529);
[]s=507 -> 13.173842*1/1:(s'=530);
[]s=508 -> 10.289124*1/1:(s'=531);
[]s=509 -> 11.611030*1/1:(s'=532);
[]s=510 -> 1.969434*1/1:(s'=533);
[]s=511 -> 5.571031*1/1:(s'=534);
[]s=512 -> 12.081526*1/1:(s'=535);
[]s=513 -> 8.422471*1/1:(s'=536);
[]s=514 -> 4.724781*1/1:(s'=537);
[]s=515 -> 2.647674*1/1:(s'=538);
[]s=516 -> 4.044980*1/1:(s'=539);
[]s=517 -> 3.981209*1/1:(s'=540);
[]s=518 -> 2.840183*1/1:(s'=541);
[]s=519 -> 2.554605*1/1:(s'=542);
[]s=520 -> 2.648165*1/1:(s'=543);
[]s=521 -> 5.728689*1/1:(s'=544);
[]s=522 -> 6.573325*1/1:(s'=545);
[]s=523 -> 3.470294*1/1:(s'=546);
[]s=524 -> 4.349717*1/1:(s'=547);
[]s=525 -> 11.337740*1/1:(s'=548);
[]s=526 -> 1 :(s'=526);
[]s=527 -> 12.348728*1/1:(s'=549);
[]s=528 -> 8.309789*1/1:(s'=550);
[]s=529 -> 11.956431*1/1:(s'=551);
[]s=530 -> 1.566661*1/1:(s'=552);
[]s=531 -> 2.050063*1/1:(s'=553);
[]s=532 -> 4.660049*1/1:(s'=554);
[]s=533 -> 5.700929*1/1:(s'=555);
[]s=534 -> 2.436350*1/1:(s'=556);
[]s=535 -> 10.149708*1/1:(s'=557);
[]s=536 -> 1.310255*1/1:(s'=558);
[]s=537 -> 96.655712*1/1:(s'=559);
[]s=538 -> 2.702703*1/1:(s'=560);
[]s=539 -> 3.732040*1/1:(s'=561);
[]s=540 -> 8.069722*1/1:(s'=562);
[]s=541 -> 2.008516*1/1:(s'=563);
[]s=542 -> 10.580779*1/1:(s'=564);
[]s=543 -> 8.265829*1/1:(s'=565);
[]s=544 -> 5.713306*1/1:(s'=566);
[]s=545 -> 9.491268*1/1:(s'=567);
[]s=546 -> 1.104875*1/1:(s'=568);
[]s=547 -> 2.669087*1/1:(s'=569);
[]s=548 -> 2.048677*1/1:(s'=570);
[]s=549 -> 1.283746*1/1:(s'=571);
[]s=550 -> 53.307746*1/1:(s'=572);
[]s=551 -> 15.137524*1/1:(s'=573);
[]s=552 -> 8.757334*1/1:(s'=574);
[]s=553 -> 9.421519*1/1:(s'=575);
[]s=554 -> 11.114075*1/1:(s'=576);
[]s=555 -> 7.009673*1/1:(s'=577);
[]s=556 -> 20.144233*1/1:(s'=578);
[]s=557 -> 17.481906*1/1:(s'=579);
[]s=558 -> 1 :(s'=558);
[]s=559 -> 3.682563*1/1:(s'=580);
[]s=560 -> 22.324418*1/1:(s'=581);
[]s=561 -> 0.834376*1/1:(s'=582);
[]s=562 -> 9.065361*1/1:(s'=583);
[]s=563 -> 4.890454*1/1:(s'=584);
[]s=564 -> 42.071606*1/1:(s'=585);
[]s=565 -> 1 :(s'=565);
[]s=566 -> 1.945942*1/1:(s'=586);
[]s=567 -> 52.388935*1/1:(s'=587);
[]s=568 -> 5.364807*1/1:(s'=588);
[]s=569 -> 5.203726*1/1:(s'=589);
[]s=570 -> 2.218672*1/1:(s'=590);
[]s=571 -> 5.060473*1/1:(s'=591);
[]s=572 -> 9.208103*1/1:(s'=592);
[]s=573 -> 18.724838*1/1:(s'=593);
[]s=574 -> 5.499643*1/1:(s'=594);
[]s=575 -> 1.883452*1/1:(s'=595);
[]s=576 -> 31.982601*1/1:(s'=596);
[]s=577 -> 14.984416*1/1:(s'=597);
[]s=578 -> 18.430122*1/1:(s'=598);
[]s=579 -> 3.582047*1/1:(s'=599);
[]s=580 -> 2.051745*1/1:(s'=600);
[]s=581 -> 6.235969*1/1:(s'=601);
[]s=582 -> 8.735913*1/1:(s'=602);
[]s=583 -> 7.235890*1/1:(s'=603);
[]s=584 -> 24.925224*1/1:(s'=604);
[]s=585 -> 4.829052*1/1:(s'=605);
[]s=586 -> 20.574015*1/1:(s'=606);
[]s=587 -> 0.865876*1/1:(s'=607);
[]s=588 -> 3.217814*1/1:(s'=608);
[]s=589 -> 2.426537*1/1:(s'=609);
[]s=590 -> 12.426528*1/1:(s'=610);
[]s=591 -> 3.297609*1/1:(s'=611);
[]s=592 -> 1.455011*1/1:(s'=612);
[]s=593 -> 7.679312*1/1:(s'=613);
[]s=594 -> 4.433607*1/1:(s'=614);
[]s=595 -> 2.788622*1/1:(s'=615);
[]s=596 -> 9.220839*1/1:(s'=616);
[]s=597 -> 93.624192*1/1:(s'=617);
[]s=598 -> 17.411896*1/1:(s'=618);
[]s=599 -> 28.152361*1/1:(s'=619);
[]s=600 -> 15.941844*1/1:(s'=620);
[]s=601 -> 1.775316*1/1:(s'=621);
[]s=602 -> 16.256726*1/1:(s'=622);
[]s=603 -> 11.495839*1/1:(s'=623);
[]s=604 -> 9.634840*1/1:(s'=624);
[]s=605 -> 1.838675*1/1:(s'=625);
[]s=606 -> 22.046341*1/1:(s'=626);
[]s=607 -> 22.905309*1/1:(s'=627);
[]s=608 -> 2.797751*1/1:(s'=628);
[]s=609 -> 1 :(s'=609);
[]s=610 -> 5.247416*1/1:(s'=629);
[]s=611 -> 4.676831*1/1:(s'=630);
[]s=612 -> 63.139285*1/1:(s'=631);
[]s=613 -> 14.917358*1/1:(s'=632);
[]s=614 -> 3.220197*1/1:(s'=633);
[]s=615 -> 14.320698*1/1:(s'=634);
[]s=616 -> 9.934433*1/1:(s'=635);
[]s=617 -> 16.724366*1/1:(s'=636);
[]s=618 -> 3.348065*1/1:(s'=637);
[]s=619 -> 4.251158*1/1:(s'=638);
[]s=620 -> 55.114638*1/1:(s'=639);
[]s=621 -> 2.612330*1/1:(s'=640);
[]s=622 -> 4.474273*1/1:(s'=641);
[]s=623 -> 54.719562*1/1:(s'=642);
[]s=624 -> 26.572423*1/1:(s'=643);
[]s=625 -> 25.116793*1/1:(s'=644);
[]s=626 -> 2.014220*1/1:(s'=645);
[]s=627 -> 38.684720*1/1:(s'=646);
[]s=628 -> 1.285611*1/1:(s'=647);
[]s=629 -> 2.128611*1/1:(s'=648);
[]s=630 -> 3.232584*1/1:(s'=649);
[]s=631 -> 510.777403*1/1:(s'=650);
[]s=632 -> 11.742602*1/1:(s'=651);
[]s=633 -> 13.873089*1/1:(s'=652);
[]s=634 -> 2.196740*1/1:(s'=653);
[]s=635 -> 15.729206*1/1:(s'=654);
[]s=636 -> 5.762692*1/1:(s'=655);
[]s=637 -> 6.452029*1/1:(s'=656);
[]s=638 -> 1.037937*1/1:(s'=657);
[]s=639 -> 7.397544*1/1:(s'=658);
[]s=640 -> 15.515182*1/1:(s'=659);
[]s=641 -> 9.568462*1/1:(s'=660);
[]s=642 -> 4.978344*1/1:(s'=661);
[]s=643 -> 4.086136*1/1:(s'=662);
[]s=644 -> 56.198719*1/1:(s'=663);
[]s=645 -> 58.958788*1/1:(s'=664);
[]s=646 -> 2.948896*1/1:(s'=665);
[]s=647 -> 4.926594*1/1:(s'=666);
[]s=648 -> 7.586678*1/1:(s'=667);
[]s=649 -> 3.886665*1/1:(s'=668);
[]s=650 -> 13.506943*1/1:(s'=669);
[]s=651 -> 1.991159*1/1:(s'=670);
[]s=652 -> 3.299350*1/1:(s'=671);
[]s=653 -> 109.277675*1/1:(s'=672);
[]s=654 -> 4.686694*1/1:(s'=673);
[]s=655 -> 2.969297*1/1:(s'=674);
[]s=656 -> 1.444690*1/1:(s'=675);
[]s=657 -> 3.542833*1/1:(s'=676);
[]s=658 -> 2.861230*1/1:(s'=677);
[]s=659 -> 2.697381*1/1:(s'=678);
[]s=660 -> 1.876278*1/1:(s'=679);
[]s=661 -> 11.984516*1/1:(s'=680);
[]s=662 -> 9.463424*1/1:(s'=681);
[]s=663 -> 9.767533*1/1:(s'=682);
[]s=664 -> 3.528582*1/1:(s'=683);
[]s=665 -> 1.912558*1/1:(s'=684);
[]s=666 -> 2.942994*1/1:(s'=685);
[]s=667 -> 11.561095*1/1:(s'=686);
[]s=668 -> 3.574109*1/1:(s'=687);
[]s=669 -> 3.619385*1/1:(s'=688);
[]s=670 -> 4.096514*1/1:(s'=689);
[]s=671 -> 80.115366*1/1:(s'=690);
[]s=672 -> 1.478546*1/1:(s'=691);
[]s=673 -> 2.989179*1/1:(s'=692);
[]s=674 -> 0.975705*1/1:(s'=693);
[]s=675 -> 23.598820*1/1:(s'=694);
[]s=676 -> 8.884940*1/1:(s'=695);
[]s=677 -> 1.891074*1/1:(s'=696);
[]s=678 -> 3.979308*1/1:(s'=697);
[]s=679 -> 25.806452*1/1:(s'=698);
[]s=680 -> 322.674325*1/1:(s'=699);
[]s=681 -> 1.437587*1/1:(s'=700);
[]s=682 -> 14.796402*1/1:(s'=701);
[]s=683 -> 8.568246*1/1:(s'=702);
[]s=684 -> 1.900852*1/1:(s'=703);
[]s=685 -> 6.617696*1/1:(s'=704);
[]s=686 -> 11.324131*1/1:(s'=705);
[]s=687 -> 0.680365*1/1:(s'=706);
[]s=688 -> 7.640587*1/1:(s'=707);
[]s=689 -> 8.484643*1/1:(s'=708);
[]s=690 -> 5.331627*1/1:(s'=709);
[]s=691 -> 254.731640*1/1:(s'=710);
[]s=692 -> 1.512356*1/1:(s'=711);
[]s=693 -> 1.861989*1/1:(s'=712);
[]s=694 -> 3.691399*1/1:(s'=713);
[]s=695 -> 12.016775*1/1:(s'=714);
[]s=696 -> 11.238607*1/1:(s'=715);
[]s=697 -> 8.318084*1/1:(s'=716);
[]s=698 -> 6.515082*1/1:(s'=717);
[]s=699 -> 16.160310*1/1:(s'=718);
[]s=700 -> 325.987743*1/1:(s'=719);
[]s=701 -> 1.983458*1/1:(s'=720);
[]s=702 -> 4.195511*1/1:(s'=721);
[]s=703 -> 4.355021*1/1:(s'=722);
[]s=704 -> 12.961595*1/1:(s'=723);
[]s=705 -> 7.202535*1/1:(s'=724);
[]s=706 -> 4.358818*1/1:(s'=725);
[]s=707 -> 3.798093*1/1:(s'=726);
[]s=708 -> 3.200102*1/1:(s'=727);
[]s=709 -> 13.634380*1/1:(s'=728);
[]s=710 -> 27.052617*1/1:(s'=729);
[]s=711 -> 15.382012*1/1:(s'=730);
[]s=712 -> 1.537563*1/1:(s'=731);
[]s=713 -> 2.477210*1/1:(s'=732);
[]s=714 -> 26.666667*1/1:(s'=733);
[]s=715 -> 4.587156*1/1:(s'=734);
[]s=716 -> 13.343296*1/1:(s'=735);
[]s=717 -> 10.585147*1/1:(s'=736);
[]s=718 -> 1.115922*1/1:(s'=737);
[]s=719 -> 60.056453*1/1:(s'=738);
[]s=720 -> 6.658233*1/1:(s'=739);
[]s=721 -> 3.761095*1/1:(s'=740);
[]s=722 -> 14.337740*1/1:(s'=741);
[]s=723 -> 3548.993860*1/1:(s'=742);
[]s=724 -> 7.459903*1/1:(s'=743);
[]s=725 -> 10.572613*1/1:(s'=744);
[]s=726 -> 2.238038*1/1:(s'=745);
[]s=727 -> 8.185316*1/1:(s'=746);
[]s=728 -> 58.685446*1/1:(s'=747);
[]s=729 -> 11.265955*1/1:(s'=748);
[]s=730 -> 2.271643*1/1:(s'=749);
[]s=731 -> 2.093233*1/1:(s'=750);
[]s=732 -> 13.056705*1/1:(s'=751);
[]s=733 -> 7.688168*1/1:(s'=752);
[]s=734 -> 1 :(s'=734);
[]s=735 -> 7.162811*1/1:(s'=753);
[]s=736 -> 1.535721*1/1:(s'=754);
[]s=737 -> 6.575919*1/1:(s'=755);
[]s=738 -> 1.611370*1/1:(s'=756);
[]s=739 -> 6.888001*1/1:(s'=757);
[]s=740 -> 12.895405*1/1:(s'=758);
[]s=741 -> 13.766141*1/1:(s'=759);
[]s=742 -> 3.849411*1/1:(s'=760);
[]s=743 -> 68.932240*1/1:(s'=761);
[]s=744 -> 2.393490*1/1:(s'=762);
[]s=745 -> 45.751933*1/1:(s'=763);
[]s=746 -> 3.135091*1/1:(s'=764);
[]s=747 -> 1.158695*1/1:(s'=765);
[]s=748 -> 5.858574*1/1:(s'=766);
[]s=749 -> 3.441275*1/1:(s'=767);
[]s=750 -> 1.245935*1/1:(s'=768);
[]s=751 -> 2.595111*1/1:(s'=769);
[]s=752 -> 8.643789*1/1:(s'=770);
[]s=753 -> 10.344471*1/1:(s'=771);
[]s=754 -> 9.419744*1/1:(s'=772);
[]s=755 -> 5.161024*1/1:(s'=773);
[]s=756 -> 59.428300*1/1:(s'=774);
[]s=757 -> 6.928566*1/1:(s'=775);
[]s=758 -> 6.178560*1/1:(s'=776);
[]s=759 -> 5.408036*1/1:(s'=777);
[]s=760 -> 2.762278*1/1:(s'=778);
[]s=761 -> 22.698899*1/1:(s'=779);
[]s=762 -> 1.011787*1/1:(s'=780);
[]s=763 -> 6.036096*1/1:(s'=781);
[]s=764 -> 117.072714*1/1:(s'=782);
[]s=765 -> 30.205093*1/1:(s'=783);
[]s=766 -> 6.053635*1/1:(s'=784);
[]s=767 -> 37.688916*1/1:(s'=785);
[]s=768 -> 8.886519*1/1:(s'=786);
[]s=769 -> 14.894251*1/1:(s'=787);
[]s=770 -> 52.037259*1/1:(s'=788);
[]s=771 -> 3.116041*1/1:(s'=789);
[]s=772 -> 3.288933*1/1:(s'=790);
[]s=773 -> 3.575131*1/1:(s'=791);
[]s=774 -> 3.665824*1/1:(s'=792);
[]s=775 -> 60.081711*1/1:(s'=793);
[]s=776 -> 26.873774*1/1:(s'=794);
[]s=777 -> 271.392515*1/1:(s'=795);
[]s=778 -> 9.623713*1/1:(s'=796);
[]s=779 -> 14.994302*1/1:(s'=797);
[]s=780 -> 3.500910*1/1:(s'=798);
[]s=781 -> 6.518480*1/1:(s'=799);
[]s=782 -> 278.877796*1/1:(s'=800);
[]s=783 -> 6.436249*1/1:(s'=801);
[]s=784 -> 3.020692*1/1:(s'=802);
[]s=785 -> 1.501772*1/1:(s'=803);
[]s=786 -> 68.404132*1/1:(s'=804);
[]s=787 -> 12.917894*1/1:(s'=805);
[]s=788 -> 7.377352*1/1:(s'=806);
[]s=789 -> 2.106194*1/1:(s'=807);
[]s=790 -> 12.685365*1/1:(s'=808);
[]s=791 -> 2.512689*1/1:(s'=809);
[]s=792 -> 10.387560*1/1:(s'=810);
[]s=793 -> 3.837446*1/1:(s'=811);
[]s=794 -> 20.538942*1/1:(s'=812);
[]s=795 -> 2.539167*1/1:(s'=813);
[]s=796 -> 5.675047*1/1:(s'=814);
[]s=797 -> 5.958410*1/1:(s'=815);
[]s=798 -> 3.971879*1/1:(s'=816);
[]s=799 -> 7.922047*1/1:(s'=817);
[]s=800 -> 2.774233*1/1:(s'=818);
[]s=801 -> 1.811430*1/1:(s'=819);
[]s=802 -> 2.349734*1/1:(s'=820);
[]s=803 -> 2.539812*1/1:(s'=821);
[]s=804 -> 4.123201*1/1:(s'=822);
[]s=805 -> 5.088800*1/1:(s'=823);
[]s=806 -> 16.258841*1/1:(s'=824);
[]s=807 -> 4.831151*1/1:(s'=825);
[]s=808 -> 1.692964*1/1:(s'=826);
[]s=809 -> 9.673051*1/1:(s'=827);
[]s=810 -> 31.446541*1/1:(s'=828);
[]s=811 -> 3.753895*1/1:(s'=829);
[]s=812 -> 5.421523*1/1:(s'=830);
[]s=813 -> 2.352941*1/1:(s'=831);
[]s=814 -> 3.207904*1/1:(s'=832);
[]s=815 -> 0.975419*1/1:(s'=833);
[]s=816 -> 13.154260*1/1:(s'=834);
[]s=817 -> 94.616331*1/1:(s'=835);
[]s=818 -> 1.805282*1/1:(s'=836);
[]s=819 -> 120.863448*1/1:(s'=837);
[]s=820 -> 3.045995*1/1:(s'=838);
[]s=821 -> 12.555716*1/1:(s'=839);
[]s=822 -> 5.991612*1/1:(s'=840);
[]s=823 -> 2.607426*1/1:(s'=841);
[]s=824 -> 2.653857*1/1:(s'=842);
[]s=825 -> 2.594572*1/1:(s'=843);
[]s=826 -> 2.790490*1/1:(s'=844);
[]s=827 -> 4.336890*1/1:(s'=845);
[]s=828 -> 12.906557*1/1:(s'=846);
[]s=829 -> 15.980312*1/1:(s'=847);
[]s=830 -> 4.885914*1/1:(s'=848);
[]s=831 -> 1.146027*1/1:(s'=849);
[]s=832 -> 1.984954*1/1:(s'=850);
[]s=833 -> 2.817457*1/1:(s'=851);
[]s=834 -> 3.858471*1/1:(s'=852);
[]s=835 -> 1.631295*1/1:(s'=853);
[]s=836 -> 47.869794*1/1:(s'=854);
[]s=837 -> 10.287642*1/1:(s'=855);
[]s=838 -> 5.631899*1/1:(s'=856);
[]s=839 -> 1.896310*1/1:(s'=857);
[]s=840 -> 5.598791*1/1:(s'=858);
[]s=841 -> 11.117535*1/1:(s'=859);
[]s=842 -> 10.939602*1/1:(s'=860);
[]s=843 -> 3.053155*1/1:(s'=861);
[]s=844 -> 3.005801*1/1:(s'=862);
[]s=845 -> 1.997244*1/1:(s'=863);
[]s=846 -> 11.279425*1/1:(s'=864);
[]s=847 -> 1.714619*1/1:(s'=865);
[]s=848 -> 4.045798*1/1:(s'=866);
[]s=849 -> 1.816233*1/1:(s'=867);
[]s=850 -> 3.665555*1/1:(s'=868);
[]s=851 -> 1 :(s'=851);
[]s=852 -> 1.174053*1/1:(s'=869);
[]s=853 -> 1.160375*1/1:(s'=870);
[]s=854 -> 449.498809*1/1:(s'=871);
[]s=855 -> 27.835769*1/1:(s'=872);
[]s=856 -> 0.979048*1/1:(s'=873);
[]s=857 -> 1.972348*1/1:(s'=874);
[]s=858 -> 1.401404*1/1:(s'=875);
[]s=859 -> 12.341261*1/1:(s'=876);
[]s=860 -> 13.951866*1/1:(s'=877);
[]s=861 -> 3.614806*1/1:(s'=878);
[]s=862 -> 11.997457*1/1:(s'=879);
[]s=863 -> 18.584942*1/1:(s'=880);
[]s=864 -> 3.500420*1/1:(s'=881);
[]s=865 -> 3.331335*1/1:(s'=882);
[]s=866 -> 2.681109*1/1:(s'=883);
[]s=867 -> 10.489547*1/1:(s'=884);
[]s=868 -> 48.706834*1/1:(s'=885);
[]s=869 -> 1.037657*1/1:(s'=886);
[]s=870 -> 8.788118*1/1:(s'=887);
[]s=871 -> 12.408949*1/1:(s'=888);
[]s=872 -> 15.963985*1/1:(s'=889);
[]s=873 -> 1.762860*1/1:(s'=890);
[]s=874 -> 6.627344*1/1:(s'=891);
[]s=875 -> 11.784948*1/1:(s'=892);
[]s=876 -> 4.097857*1/1:(s'=893);
[]s=877 -> 3.133127*1/1:(s'=894);
[]s=878 -> 5.688929*1/1:(s'=895);
[]s=879 -> 3.371317*1/1:(s'=896);
[]s=880 -> 33.821490*1/1:(s'=897);
[]s=881 -> 4.875433*1/1:(s'=898);
[]s=882 -> 14.499688*1/1:(s'=899);
[]s=883 -> 17.451398*1/1:(s'=900);
[]s=884 -> 1.730763*1/1:(s'=901);
[]s=885 -> 4.505925*1/1:(s'=902);
[]s=886 -> 17.250004*1/1:(s'=903);
[]s=887 -> 3.265626*1/1:(s'=904);
[]s=888 -> 9.141603*1/1:(s'=905);
[]s=889 -> 2.496131*1/1:(s'=906);
[]s=890 -> 3.936853*1/1:(s'=907);
[]s=891 -> 1.267186*1/1:(s'=908);
[]s=892 -> 2.834949*1/1:(s'=909);
[]s=893 -> 10.158266*1/1:(s'=910);
[]s=894 -> 4.217096*1/1:(s'=911);
[]s=895 -> 22.284123*1/1:(s'=912);
[]s=896 -> 2.694328*1/1:(s'=913);
[]s=897 -> 44.764761*1/1:(s'=914);
[]s=898 -> 9.505703*1/1:(s'=915);
[]s=899 -> 30.866103*1/1:(s'=916);
[]s=900 -> 2.716579*1/1:(s'=917);
[]s=901 -> 30.964546*1/1:(s'=918);
[]s=902 -> 10.283517*1/1:(s'=919);
[]s=903 -> 50.438818*1/1:(s'=920);
[]s=904 -> 4.668098*1/1:(s'=921);
[]s=905 -> 10.611656*1/1:(s'=922);
[]s=906 -> 10.223485*1/1:(s'=923);
[]s=907 -> 2.608310*1/1:(s'=924);
[]s=908 -> 1.474470*1/1:(s'=925);
[]s=909 -> 3.668917*1/1:(s'=926);
[]s=910 -> 1.756574*1/1:(s'=927);
[]s=911 -> 4.070667*1/1:(s'=928);
[]s=912 -> 2.596661*1/1:(s'=929);
[]s=913 -> 16.418744*1/1:(s'=930);
[]s=914 -> 2.634907*1/1:(s'=931);
[]s=915 -> 2.806545*1/1:(s'=932);
[]s=916 -> 24.884907*1/1:(s'=933);
[]s=917 -> 5.167425*1/1:(s'=934);
[]s=918 -> 14.146873*1/1:(s'=935);
[]s=919 -> 5.545697*1/1:(s'=936);
[]s=920 -> 93.755860*1/1:(s'=937);
[]s=921 -> 91.390971*1/1:(s'=938);
[]s=922 -> 1.418943*1/1:(s'=939);
[]s=923 -> 5.166891*1/1:(s'=940);
[]s=924 -> 6.062076*1/1:(s'=941);
[]s=925 -> 1 :(s'=925);
[]s=926 -> 7.104796*1/1:(s'=942);
[]s=927 -> 2.903600*1/1:(s'=943);
[]s=928 -> 7.901391*1/1:(s'=944);
[]s=929 -> 44.861155*1/1:(s'=945);
[]s=930 -> 26.660979*1/1:(s'=946);
[]s=931 -> 3.178134*1/1:(s'=947);
[]s=932 -> 8.847209*1/1:(s'=948);
[]s=933 -> 10.273269*1/1:(s'=949);
[]s=934 -> 16.661391*1/1:(s'=950);
[]s=935 -> 3.070687*1/1:(s'=951);
[]s=936 -> 11.552413*1/1:(s'=952);
[]s=937 -> 60.960741*1/1:(s'=953);
[]s=938 -> 35.192680*1/1:(s'=954);
[]s=939 -> 2.969562*1/1:(s'=955);
[]s=940 -> 3.235513*1/1:(s'=956);
[]s=941 -> 165.686356*1/1:(s'=957);
[]s=942 -> 5.596911*1/1:(s'=958);
[]s=943 -> 1.472776*1/1:(s'=959);
[]s=944 -> 4.962533*1/1:(s'=960);
[]s=945 -> 47.662171*1/1:(s'=961);
[]s=946 -> 2.429602*1/1:(s'=962);
[]s=947 -> 5.275375*1/1:(s'=963);
[]s=948 -> 0.873591*1/1:(s'=964);
[]s=949 -> 10.355183*1/1:(s'=965);
[]s=950 -> 63.207130*1/1:(s'=966);
[]s=951 -> 1.574580*1/1:(s'=967);
[]s=952 -> 4.490951*1/1:(s'=968);
[]s=953 -> 7.857311*1/1:(s'=969);
[]s=954 -> 3.236560*1/1:(s'=970);
[]s=955 -> 5.739540*1/1:(s'=971);
[]s=956 -> 15.751256*1/1:(s'=972);
[]s=957 -> 100.118139*1/1:(s'=973);
[]s=958 -> 4.100209*1/1:(s'=974);
[]s=959 -> 47.524000*1/1:(s'=975);
[]s=960 -> 1 :(s'=960);
[]s=961 -> 1.393223*1/1:(s'=976);
[]s=962 -> 3.353454*1/1:(s'=977);
[]s=963 -> 14.244203*1/1:(s'=978);
[]s=964 -> 30.036344*1/1:(s'=979);
[]s=965 -> 24.389054*1/1:(s'=980);
[]s=966 -> 13.323740*1/1:(s'=981);
[]s=967 -> 1.860742*1/1:(s'=982);
[]s=968 -> 4.039262*1/1:(s'=983);
[]s=969 -> 4.401990*1/1:(s'=984);
[]s=970 -> 13.570546*1/1:(s'=985);
[]s=971 -> 8.288438*1/1:(s'=986);
[]s=972 -> 2.748536*1/1:(s'=987);
[]s=973 -> 8.588852*1/1:(s'=988);
[]s=974 -> 11.063293*1/1:(s'=989);
[]s=975 -> 3.786731*1/1:(s'=990);
[]s=976 -> 5.831924*1/1:(s'=991);
[]s=977 -> 1.879417*1/1:(s'=992);
[]s=978 -> 5.398402*1/1:(s'=993);
[]s=979 -> 22.641851*1/1:(s'=994);
[]s=980 -> 10.570378*1/1:(s'=995);
[]s=981 -> 11.601063*1/1:(s'=996);
[]s=982 -> 2.660140*1/1:(s'=997);
[]s=983 -> 3.292289*1/1:(s'=998);
[]s=984 -> 8.038585*1/1:(s'=999);
[]s=985 -> 21.280671*1/1:(s'=1000);
[]s=986 -> 3.275038*1/1:(s'=1001);
[]s=987 -> 0.999600*1/1:(s'=1002);
[]s=988 -> 4.303667*1/1:(s'=1003);
[]s=989 -> 4.446618*1/1:(s'=1004);
[]s=990 -> 1.902515*1/1:(s'=1005);
[]s=991 -> 16.917611*1/1:(s'=1006);
[]s=992 -> 9.389671*1/1:(s'=1007);
[]s=993 -> 2.067312*1/1:(s'=1008);
[]s=994 -> 3.922338*1/1:(s'=1009);
[]s=995 -> 29.211579*1/1:(s'=1010);
[]s=996 -> 65.436461*1/1:(s'=1011);
[]s=997 -> 5.541394*1/1:(s'=1012);
[]s=998 -> 15.418536*1/1:(s'=1013);
[]s=999 -> 10.365702*1/1:(s'=1014);
[]s=1000 -> 4.653760*1/1:(s'=1015);
[]s=1001 -> 5.364807*1/1:(s'=1016);
[]s=1002 -> 2.090825*1/1:(s'=1017);
[]s=1003 -> 10.198774*1/1:(s'=1018);
[]s=1004 -> 779.362481*1/1:(s'=1019);
[]s=1005 -> 4.828585*1/1:(s'=1020);
[]s=1006 -> 37.978049*1/1:(s'=1021);
[]s=1007 -> 1.412589*1/1:(s'=1022);
[]s=1008 -> 13.840639*1/1:(s'=1023);
[]s=1009 -> 19.128871*1/1:(s'=1024);
[]s=1010 -> 75.935910*1/1:(s'=1025);
[]s=1011 -> 10.208144*1/1:(s'=1026);
[]s=1012 -> 4.602356*1/1:(s'=1027);
[]s=1013 -> 1.582253*1/1:(s'=1028);
[]s=1014 -> 8.161267*1/1:(s'=1029);
[]s=1015 -> 4.591790*1/1:(s'=1030);
[]s=1016 -> 10.773888*1/1:(s'=1031);
[]s=1017 -> 0.710530*1/1:(s'=1032);
[]s=1018 -> 13.575152*1/1:(s'=1033);
[]s=1019 -> 1 :(s'=1019);
[]s=1020 -> 10.519450*1/1:(s'=1034);
[]s=1021 -> 19.968051*1/1:(s'=1035);
[]s=1022 -> 1.717800*1/1:(s'=1036);
[]s=1023 -> 4.953192*1/1:(s'=1037);
[]s=1024 -> 3.360102*1/1:(s'=1038);
[]s=1025 -> 1.186606*1/1:(s'=1039);
[]s=1026 -> 2.270715*1/1:(s'=1040);
[]s=1027 -> 141.091484*1/1:(s'=1041);
[]s=1028 -> 8.334722*1/1:(s'=1042);
[]s=1029 -> 3.632533*1/1:(s'=1043);
[]s=1030 -> 29.696502*1/1:(s'=1044);
[]s=1031 -> 15.531809*1/1:(s'=1045);
[]s=1032 -> 5.349024*1/1:(s'=1046);
[]s=1033 -> 16.357777*1/1:(s'=1047);
[]s=1034 -> 1 :(s'=1034);
[]s=1035 -> 0.833681*1/1:(s'=1048);
[]s=1036 -> 166.140555*1/1:(s'=1049);
[]s=1037 -> 5.715919*1/1:(s'=1050);
[]s=1038 -> 15.022233*1/1:(s'=1051);
[]s=1039 -> 8.195378*1/1:(s'=1052);
[]s=1040 -> 13.827625*1/1:(s'=1053);
[]s=1041 -> 55.769338*1/1:(s'=1054);
[]s=1042 -> 15.469340*1/1:(s'=1055);
[]s=1043 -> 6.920894*1/1:(s'=1056);
[]s=1044 -> 2.780713*1/1:(s'=1057);
[]s=1045 -> 10.084508*1/1:(s'=1058);
[]s=1046 -> 1.128936*1/1:(s'=1059);
[]s=1047 -> 1.101722*1/1:(s'=1060);
[]s=1048 -> 6.864831*1/1:(s'=1061);
[]s=1049 -> 7.579777*1/1:(s'=1062);
[]s=1050 -> 4.565168*1/1:(s'=1063);
[]s=1051 -> 5.019324*1/1:(s'=1064);
[]s=1052 -> 34.474437*1/1:(s'=1065);
[]s=1053 -> 7.588981*1/1:(s'=1066);
[]s=1054 -> 13.045293*1/1:(s'=1067);
[]s=1055 -> 0.853170*1/1:(s'=1068);
[]s=1056 -> 7.869678*1/1:(s'=1069);
[]s=1057 -> 2.037199*1/1:(s'=1070);
[]s=1058 -> 25.433644*1/1:(s'=1071);
[]s=1059 -> 3.087849*1/1:(s'=1072);
[]s=1060 -> 4.186728*1/1:(s'=1073);
[]s=1061 -> 25.072082*1/1:(s'=1074);
[]s=1062 -> 3.133421*1/1:(s'=1075);
[]s=1063 -> 16.818029*1/1:(s'=1076);
[]s=1064 -> 43.542628*1/1:(s'=1077);
[]s=1065 -> 24.673690*1/1:(s'=1078);
[]s=1066 -> 8.244023*1/1:(s'=1079);
[]s=1067 -> 4.403928*1/1:(s'=1080);
[]s=1068 -> 5.079494*1/1:(s'=1081);
[]s=1069 -> 21.899089*1/1:(s'=1082);
[]s=1070 -> 3.703841*1/1:(s'=1083);
[]s=1071 -> 2.967623*1/1:(s'=1084);
[]s=1072 -> 17.083212*1/1:(s'=1085);
[]s=1073 -> 1.781261*1/1:(s'=1086);
[]s=1074 -> 1.861331*1/1:(s'=1087);
[]s=1075 -> 2.263007*1/1:(s'=1088);
[]s=1076 -> 1.954614*1/1:(s'=1089);
[]s=1077 -> 3.310162*1/1:(s'=1090);
[]s=1078 -> 3.604123*1/1:(s'=1091);
[]s=1079 -> 8.491848*1/1:(s'=1092);
[]s=1080 -> 3.364964*1/1:(s'=1093);
[]s=1081 -> 8.904720*1/1:(s'=1094);
[]s=1082 -> 7.945967*1/1:(s'=1095);
[]s=1083 -> 8.261049*1/1:(s'=1096);
[]s=1084 -> 2.068595*1/1:(s'=1097);
[]s=1085 -> 22.869689*1/1:(s'=1098);
[]s=1086 -> 3.831271*1/1:(s'=1099);
[]s=1087 -> 8.652016*1/1:(s'=1100);
[]s=1088 -> 1.159259*1/1:(s'=1101);
[]s=1089 -> 3.626999*1/1:(s'=1102);
[]s=1090 -> 25.453065*1/1:(s'=1103);
[]s=1091 -> 26.149260*1/1:(s'=1104);
[]s=1092 -> 3.396162*1/1:(s'=1105);
[]s=1093 -> 3.248019*1/1:(s'=1106);
[]s=1094 -> 6.276282*1/1:(s'=1107);
[]s=1095 -> 88.035919*1/1:(s'=1108);
[]s=1096 -> 3.392706*1/1:(s'=1109);
[]s=1097 -> 30.054398*1/1:(s'=1110);
[]s=1098 -> 3.035362*1/1:(s'=1111);
[]s=1099 -> 33.794059*1/1:(s'=1112);
[]s=1100 -> 23.949228*1/1:(s'=1113);
[]s=1101 -> 4.439118*1/1:(s'=1114);
[]s=1102 -> 7.694083*1/1:(s'=1115);
[]s=1103 -> 6.744908*1/1:(s'=1116);
[]s=1104 -> 199.912039*1/1:(s'=1117);
[]s=1105 -> 3.493206*1/1:(s'=1118);
[]s=1106 -> 4.738214*1/1:(s'=1119);
[]s=1107 -> 4.407811*1/1:(s'=1120);
[]s=1108 -> 4.640371*1/1:(s'=1121);
[]s=1109 -> 20.913502*1/1:(s'=1122);
[]s=1110 -> 5.848295*1/1:(s'=1123);
[]s=1111 -> 3.662333*1/1:(s'=1124);
[]s=1112 -> 14.438974*1/1:(s'=1125);
[]s=1113 -> 4.925866*1/1:(s'=1126);
[]s=1114 -> 21.826436*1/1:(s'=1127);
[]s=1115 -> 1.878569*1/1:(s'=1128);
[]s=1116 -> 6.100909*1/1:(s'=1129);
[]s=1117 -> 16.178088*1/1:(s'=1130);
[]s=1118 -> 11.279425*1/1:(s'=1131);
[]s=1119 -> 5.661873*1/1:(s'=1132);
[]s=1120 -> 3.357395*1/1:(s'=1133);
[]s=1121 -> 20.182042*1/1:(s'=1134);
[]s=1122 -> 6.164088*1/1:(s'=1135);
[]s=1123 -> 11.480661*1/1:(s'=1136);
[]s=1124 -> 5.499038*1/1:(s'=1137);
[]s=1125 -> 3.730230*1/1:(s'=1138);
[]s=1126 -> 39.215686*1/1:(s'=1139);
[]s=1127 -> 20.566822*1/1:(s'=1140);
[]s=1128 -> 6.844627*1/1:(s'=1141);
[]s=1129 -> 13.857709*1/1:(s'=1142);
[]s=1130 -> 4.424779*1/1:(s'=1143);
[]s=1131 -> 1.298313*1/1:(s'=1144);
[]s=1132 -> 8.425310*1/1:(s'=1145);
[]s=1133 -> 18.953394*1/1:(s'=1146);
[]s=1134 -> 3.260834*1/1:(s'=1147);
[]s=1135 -> 5.224115*1/1:(s'=1148);
[]s=1136 -> 6.697475*1/1:(s'=1149);
[]s=1137 -> 2.907737*1/1:(s'=1150);
[]s=1138 -> 0.699545*1/1:(s'=1151);
[]s=1139 -> 17.413715*1/1:(s'=1152);
[]s=1140 -> 19.062869*1/1:(s'=1153);
[]s=1141 -> 5.094763*1/1:(s'=1154);
[]s=1142 -> 1.584962*1/1:(s'=1155);
[]s=1143 -> 4.278990*1/1:(s'=1156);
[]s=1144 -> 9.747539*1/1:(s'=1157);
[]s=1145 -> 1.749230*1/1:(s'=1158);
[]s=1146 -> 6.121075*1/1:(s'=1159);
[]s=1147 -> 20.273695*1/1:(s'=1160);
[]s=1148 -> 1.877617*1/1:(s'=1161);
[]s=1149 -> 3.535318*1/1:(s'=1162);
[]s=1150 -> 1 :(s'=1150);
[]s=1151 -> 1.672856*1/1:(s'=1163);
[]s=1152 -> 14.360595*1/1:(s'=1164);
[]s=1153 -> 2.888671*1/1:(s'=1165);
[]s=1154 -> 10.611431*1/1:(s'=1166);
[]s=1155 -> 7.072636*1/1:(s'=1167);
[]s=1156 -> 1.714384*1/1:(s'=1168);
[]s=1157 -> 9.632983*1/1:(s'=1169);
[]s=1158 -> 73.142188*1/1:(s'=1170);
[]s=1159 -> 5.506305*1/1:(s'=1171);
[]s=1160 -> 9.519277*1/1:(s'=1172);
[]s=1161 -> 2.037448*1/1:(s'=1173);
[]s=1162 -> 8.224361*1/1:(s'=1174);
[]s=1163 -> 6.744453*1/1:(s'=1175);
[]s=1164 -> 1.413527*1/1:(s'=1176);
[]s=1165 -> 5.117445*1/1:(s'=1177);
[]s=1166 -> 22.553508*1/1:(s'=1178);
[]s=1167 -> 5.799119*1/1:(s'=1179);
[]s=1168 -> 40.482552*1/1:(s'=1180);
[]s=1169 -> 4.749466*1/1:(s'=1181);
[]s=1170 -> 10.607941*1/1:(s'=1182);
[]s=1171 -> 8.095855*1/1:(s'=1183);
[]s=1172 -> 1.124518*1/1:(s'=1184);
[]s=1173 -> 4.434393*1/1:(s'=1185);
[]s=1174 -> 14.056394*1/1:(s'=1186);
[]s=1175 -> 8.218277*1/1:(s'=1187);
[]s=1176 -> 25.599672*1/1:(s'=1188);
[]s=1177 -> 1.625778*1/1:(s'=1189);
[]s=1178 -> 6.009615*1/1:(s'=1190);
[]s=1179 -> 5.089577*1/1:(s'=1191);
[]s=1180 -> 1.240418*1/1:(s'=1192);
[]s=1181 -> 2.737326*1/1:(s'=1193);
[]s=1182 -> 19.599004*1/1:(s'=1194);
[]s=1183 -> 4.161638*1/1:(s'=1195);
[]s=1184 -> 5.830564*1/1:(s'=1196);
[]s=1185 -> 2.358824*1/1:(s'=1197);
[]s=1186 -> 2.734482*1/1:(s'=1198);
[]s=1187 -> 1.568972*1/1:(s'=1199);
[]s=1188 -> 6.025185*1/1:(s'=1200);
[]s=1189 -> 2.664109*1/1:(s'=1201);
[]s=1190 -> 80.083287*1/1:(s'=1202);
[]s=1191 -> 92.980009*1/1:(s'=1203);
[]s=1192 -> 5.003753*1/1:(s'=1204);
[]s=1193 -> 7.626020*1/1:(s'=1205);
[]s=1194 -> 13.366661*1/1:(s'=1206);
[]s=1195 -> 3.062787*1/1:(s'=1207);
[]s=1196 -> 4.692853*1/1:(s'=1208);
[]s=1197 -> 9.806806*1/1:(s'=1209);
[]s=1198 -> 20.245374*1/1:(s'=1210);
[]s=1199 -> 1.971065*1/1:(s'=1211);
[]s=1200 -> 4.754886*1/1:(s'=1212);
[]s=1201 -> 8.635579*1/1:(s'=1213);
[]s=1202 -> 1.868879*1/1:(s'=1214);
[]s=1203 -> 7.625438*1/1:(s'=1215);
[]s=1204 -> 5.629997*1/1:(s'=1216);
[]s=1205 -> 7.520493*1/1:(s'=1217);
[]s=1206 -> 3.992494*1/1:(s'=1218);
[]s=1207 -> 23.583793*1/1:(s'=1219);
[]s=1208 -> 6.437492*1/1:(s'=1220);
[]s=1209 -> 22.300522*1/1:(s'=1221);
[]s=1210 -> 5.974786*1/1:(s'=1222);
[]s=1211 -> 2.676660*1/1:(s'=1223);
[]s=1212 -> 29.732703*1/1:(s'=1224);
[]s=1213 -> 3.214917*1/1:(s'=1225);
[]s=1214 -> 5.149861*1/1:(s'=1226);
[]s=1215 -> 2.060921*1/1:(s'=1227);
[]s=1216 -> 60.694343*1/1:(s'=1228);
[]s=1217 -> 2.420780*1/1:(s'=1229);
[]s=1218 -> 13.036280*1/1:(s'=1230);
[]s=1219 -> 3.919878*1/1:(s'=1231);
[]s=1220 -> 101.070335*1/1:(s'=1232);
[]s=1221 -> 0.917852*1/1:(s'=1233);
[]s=1222 -> 25.828447*1/1:(s'=1234);
[]s=1223 -> 3.873267*1/1:(s'=1235);
[]s=1224 -> 93.519125*1/1:(s'=1236);
[]s=1225 -> 466.483183*1/1:(s'=1237);
[]s=1226 -> 4.253690*1/1:(s'=1238);
[]s=1227 -> 3.243804*1/1:(s'=1239);
[]s=1228 -> 10.455111*1/1:(s'=1240);
[]s=1229 -> 1.893294*1/1:(s'=1241);
[]s=1230 -> 10.723746*1/1:(s'=1242);
[]s=1231 -> 4.994257*1/1:(s'=1243);
[]s=1232 -> 5.217301*1/1:(s'=1244);
[]s=1233 -> 1 :(s'=1233);
[]s=1234 -> 8.210181*1/1:(s'=1245);
[]s=1235 -> 1 :(s'=1235);
[]s=1236 -> 38.264330*1/1:(s'=1246);
[]s=1237 -> 5.374321*1/1:(s'=1247);
[]s=1238 -> 3.976459*1/1:(s'=1248);
[]s=1239 -> 3.669455*1/1:(s'=1249);
[]s=1240 -> 12.182197*1/1:(s'=1250);
[]s=1241 -> 3.009057*1/1:(s'=1251);
[]s=1242 -> 1.814915*1/1:(s'=1252);
[]s=1243 -> 4.947556*1/1:(s'=1253);
[]s=1244 -> 10.029990*1/1:(s'=1254);
[]s=1245 -> 15.891682*1/1:(s'=1255);
[]s=1246 -> 170.392585*1/1:(s'=1256);
[]s=1247 -> 15.364051*1/1:(s'=1257);
[]s=1248 -> 10.305029*1/1:(s'=1258);
[]s=1249 -> 28.865027*1/1:(s'=1259);
[]s=1250 -> 8.030194*1/1:(s'=1260);
[]s=1251 -> 1.888752*1/1:(s'=1261);
[]s=1252 -> 2.022081*1/1:(s'=1262);
[]s=1253 -> 8.934155*1/1:(s'=1263);
[]s=1254 -> 7.539772*1/1:(s'=1264);
[]s=1255 -> 18.331806*1/1:(s'=1265);
[]s=1256 -> 5.620820*1/1:(s'=1266);
[]s=1257 -> 6.045218*1/1:(s'=1267);
[]s=1258 -> 2.564103*1/1:(s'=1268);
[]s=1259 -> 30.975096*1/1:(s'=1269);
[]s=1260 -> 4.611483*1/1:(s'=1270);
[]s=1261 -> 26.366441*1/1:(s'=1271);
[]s=1262 -> 2.833423*1/1:(s'=1272);
[]s=1263 -> 1.883984*1/1:(s'=1273);
[]s=1264 -> 8.254912*1/1:(s'=1274);
[]s=1265 -> 2.985877*1/1:(s'=1275);
[]s=1266 -> 4.297933*1/1:(s'=1276);
[]s=1267 -> 4.631989*1/1:(s'=1277);
[]s=1268 -> 12.876310*1/1:(s'=1278);
[]s=1269 -> 6.531679*1/1:(s'=1279);
[]s=1270 -> 19.138756*1/1:(s'=1280);
[]s=1271 -> 3.716505*1/1:(s'=1281);
[]s=1272 -> 30.726686*1/1:(s'=1282);
[]s=1273 -> 8.093889*1/1:(s'=1283);
[]s=1274 -> 4.876384*1/1:(s'=1284);
[]s=1275 -> 4.587787*1/1:(s'=1285);
[]s=1276 -> 32.220647*1/1:(s'=1286);
[]s=1277 -> 4.379626*1/1:(s'=1287);
[]s=1278 -> 5.431535*1/1:(s'=1288);
[]s=1279 -> 12.973366*1/1:(s'=1289);
[]s=1280 -> 2.382143*1/1:(s'=1290);
[]s=1281 -> 8.230453*1/1:(s'=1291);
[]s=1282 -> 5.267871*1/1:(s'=1292);
[]s=1283 -> 1.499588*1/1:(s'=1293);
[]s=1284 -> 1.939789*1/1:(s'=1294);
[]s=1285 -> 26.510432*1/1:(s'=1295);
[]s=1286 -> 5.480053*1/1:(s'=1296);
[]s=1287 -> 33.017466*1/1:(s'=1297);
[]s=1288 -> 7.013115*1/1:(s'=1298);
[]s=1289 -> 69.218523*1/1:(s'=1299);
[]s=1290 -> 8.192021*1/1:(s'=1300);
[]s=1291 -> 30.349935*1/1:(s'=1301);
[]s=1292 -> 160.020483*1/1:(s'=1302);
[]s=1293 -> 14.386212*1/1:(s'=1303);
[]s=1294 -> 9.515653*1/1:(s'=1304);
[]s=1295 -> 3.350420*1/1:(s'=1305);
[]s=1296 -> 56.497175*1/1:(s'=1306);
[]s=1297 -> 8.512087*1/1:(s'=1307);
[]s=1298 -> 4.546488*1/1:(s'=1308);
[]s=1299 -> 6.255082*1/1:(s'=1309);
[]s=1300 -> 4.187605*1/1:(s'=1310);
[]s=1301 -> 7.192175*1/1:(s'=1311);
[]s=1302 -> 9.938382*1/1:(s'=1312);
[]s=1303 -> 2.921926*1/1:(s'=1313);
[]s=1304 -> 2.269375*1/1:(s'=1314);
[]s=1305 -> 3.702058*1/1:(s'=1315);
[]s=1306 -> 2.705042*1/1:(s'=1316);
[]s=1307 -> 6.099421*1/1:(s'=1317);
[]s=1308 -> 4.281372*1/1:(s'=1318);
[]s=1309 -> 10.398577*1/1:(s'=1319);
[]s=1310 -> 9.584052*1/1:(s'=1320);
[]s=1311 -> 4.705439*1/1:(s'=1321);
[]s=1312 -> 8.258320*1/1:(s'=1322);
[]s=1313 -> 37.704547*1/1:(s'=1323);
[]s=1314 -> 7.118958*1/1:(s'=1324);
[]s=1315 -> 2.910954*1/1:(s'=1325);
[]s=1316 -> 4.989024*1/1:(s'=1326);
[]s=1317 -> 8.840170*1/1:(s'=1327);
[]s=1318 -> 2.724350*1/1:(s'=1328);
[]s=1319 -> 5.122688*1/1:(s'=1329);
[]s=1320 -> 2.551216*1/1:(s'=1330);
[]s=1321 -> 2.554213*1/1:(s'=1331);
[]s=1322 -> 326.936280*1/1:(s'=1332);
[]s=1323 -> 4.521000*1/1:(s'=1333);
[]s=1324 -> 12.981281*1/1:(s'=1334);
[]s=1325 -> 18.751172*1/1:(s'=1335);
[]s=1326 -> 30.165913*1/1:(s'=1336);
[]s=1327 -> 4.459905*1/1:(s'=1337);
[]s=1328 -> 12.487357*1/1:(s'=1338);
[]s=1329 -> 2.626395*1/1:(s'=1339);
[]s=1330 -> 5.103082*1/1:(s'=1340);
[]s=1331 -> 7.410701*1/1:(s'=1341);
[]s=1332 -> 12.411722*1/1:(s'=1342);
[]s=1333 -> 29.502006*1/1:(s'=1343);
[]s=1334 -> 83.668005*1/1:(s'=1344);
[]s=1335 -> 3.518773*1/1:(s'=1345);
[]s=1336 -> 10.033713*1/1:(s'=1346);
[]s=1337 -> 6.163328*1/1:(s'=1347);
[]s=1338 -> 7.075639*1/1:(s'=1348);
[]s=1339 -> 1.822789*1/1:(s'=1349);
[]s=1340 -> 4.374262*1/1:(s'=1350);
[]s=1341 -> 8.533151*1/1:(s'=1351);
[]s=1342 -> 52.061641*1/1:(s'=1352);
[]s=1343 -> 9.766579*1/1:(s'=1353);
[]s=1344 -> 10.220351*1/1:(s'=1354);
[]s=1345 -> 1.838573*1/1:(s'=1355);
[]s=1346 -> 17.315717*1/1:(s'=1356);
[]s=1347 -> 4.204861*1/1:(s'=1357);
[]s=1348 -> 3.776150*1/1:(s'=1358);
[]s=1349 -> 9.111617*1/1:(s'=1359);
[]s=1350 -> 3.547231*1/1:(s'=1360);
[]s=1351 -> 70.821530*1/1:(s'=1361);
[]s=1352 -> 52.449386*1/1:(s'=1362);
[]s=1353 -> 1.888182*1/1:(s'=1363);
[]s=1354 -> 3.260090*1/1:(s'=1364);
[]s=1355 -> 6.437906*1/1:(s'=1365);
[]s=1356 -> 3.246121*1/1:(s'=1366);
[]s=1357 -> 3.130870*1/1:(s'=1367);
[]s=1358 -> 20.530087*1/1:(s'=1368);
[]s=1359 -> 5.000750*1/1:(s'=1369);
[]s=1360 -> 1.314371*1/1:(s'=1370);
[]s=1361 -> 3.037575*1/1:(s'=1371);
[]s=1362 -> 12.694705*1/1:(s'=1372);
[]s=1363 -> 8.873902*1/1:(s'=1373);
[]s=1364 -> 1.546910*1/1:(s'=1374);
[]s=1365 -> 3.753895*1/1:(s'=1375);
[]s=1366 -> 5.716246*1/1:(s'=1376);
[]s=1367 -> 7.664597*1/1:(s'=1377);
[]s=1368 -> 4.105090*1/1:(s'=1378);
[]s=1369 -> 73.953557*1/1:(s'=1379);
[]s=1370 -> 2.312620*1/1:(s'=1380);
[]s=1371 -> 13.815590*1/1:(s'=1381);
[]s=1372 -> 9.928515*1/1:(s'=1382);
[]s=1373 -> 1.108697*1/1:(s'=1383);
[]s=1374 -> 10.917507*1/1:(s'=1384);
[]s=1375 -> 2.853148*1/1:(s'=1385);
[]s=1376 -> 62.511721*1/1:(s'=1386);
[]s=1377 -> 7.821666*1/1:(s'=1387);
[]s=1378 -> 6.015761*1/1:(s'=1388);
[]s=1379 -> 1.018434*1/1:(s'=1389);
[]s=1380 -> 81.866558*1/1:(s'=1390);
[]s=1381 -> 7.388253*1/1:(s'=1391);
[]s=1382 -> 1.976910*1/1:(s'=1392);
[]s=1383 -> 5.122426*1/1:(s'=1393);
[]s=1384 -> 4.320588*1/1:(s'=1394);
[]s=1385 -> 16.687805*1/1:(s'=1395);
[]s=1386 -> 5.878895*1/1:(s'=1396);
[]s=1387 -> 268.492415*1/1:(s'=1397);
[]s=1388 -> 15.844596*1/1:(s'=1398);
[]s=1389 -> 107.339903*1/1:(s'=1399);
[]s=1390 -> 2.405465*1/1:(s'=1400);
[]s=1391 -> 2.266032*1/1:(s'=1401);
[]s=1392 -> 9.615385*1/1:(s'=1402);
[]s=1393 -> 2.004731*1/1:(s'=1403);
[]s=1394 -> 17.825630*1/1:(s'=1404);
[]s=1395 -> 20.195900*1/1:(s'=1405);
[]s=1396 -> 13.598227*1/1:(s'=1406);
[]s=1397 -> 6.961364*1/1:(s'=1407);
[]s=1398 -> 36.695901*1/1:(s'=1408);
[]s=1399 -> 2.018367*1/1:(s'=1409);
[]s=1400 -> 11.762077*1/1:(s'=1410);
[]s=1401 -> 10.578652*1/1:(s'=1411);
[]s=1402 -> 9.447331*1/1:(s'=1412);
[]s=1403 -> 0.973520*1/1:(s'=1413);
[]s=1404 -> 111.180290*1/1:(s'=1414);
[]s=1405 -> 7.203054*1/1:(s'=1415);
[]s=1406 -> 1.088293*1/1:(s'=1416);
[]s=1407 -> 35.069262*1/1:(s'=1417);
[]s=1408 -> 5.217573*1/1:(s'=1418);
[]s=1409 -> 8.481045*1/1:(s'=1419);
[]s=1410 -> 4.788584*1/1:(s'=1420);
[]s=1411 -> 4.097857*1/1:(s'=1421);
[]s=1412 -> 23.037759*1/1:(s'=1422);
[]s=1413 -> 1.666611*1/1:(s'=1423);
[]s=1414 -> 1.428633*1/1:(s'=1424);
[]s=1415 -> 2.752698*1/1:(s'=1425);
[]s=1416 -> 3.540324*1/1:(s'=1426);
[]s=1417 -> 2.544335*1/1:(s'=1427);
[]s=1418 -> 3.296305*1/1:(s'=1428);
[]s=1419 -> 22.354361*1/1:(s'=1429);
[]s=1420 -> 3.284719*1/1:(s'=1430);
[]s=1421 -> 0.808865*1/1:(s'=1431);
[]s=1422 -> 2.316155*1/1:(s'=1432);
[]s=1423 -> 34.430519*1/1:(s'=1433);
[]s=1424 -> 40.316078*1/1:(s'=1434);
[]s=1425 -> 8.877053*1/1:(s'=1435);
[]s=1426 -> 17.308824*1/1:(s'=1436);
[]s=1427 -> 925.069380*1/1:(s'=1437);
[]s=1428 -> 3.185221*1/1:(s'=1438);
[]s=1429 -> 15.066367*1/1:(s'=1439);
[]s=1430 -> 4.289820*1/1:(s'=1440);
[]s=1431 -> 36.730946*1/1:(s'=1441);
[]s=1432 -> 11.160963*1/1:(s'=1442);
[]s=1433 -> 6.707808*1/1:(s'=1443);
[]s=1434 -> 6.750827*1/1:(s'=1444);
[]s=1435 -> 5.329922*1/1:(s'=1445);
[]s=1436 -> 6.070171*1/1:(s'=1446);
[]s=1437 -> 3.523112*1/1:(s'=1447);
[]s=1438 -> 7.005254*1/1:(s'=1448);
[]s=1439 -> 0.899928*1/1:(s'=1449);
[]s=1440 -> 17.119770*1/1:(s'=1450);
[]s=1441 -> 5.002752*1/1:(s'=1451);
[]s=1442 -> 1.993422*1/1:(s'=1452);
[]s=1443 -> 0.852297*1/1:(s'=1453);
[]s=1444 -> 3.436544*1/1:(s'=1454);
[]s=1445 -> 9.566632*1/1:(s'=1455);
[]s=1446 -> 5.396363*1/1:(s'=1456);
[]s=1447 -> 14.665552*1/1:(s'=1457);
[]s=1448 -> 13.228563*1/1:(s'=1458);
[]s=1449 -> 15.479637*1/1:(s'=1459);
[]s=1450 -> 20.982836*1/1:(s'=1460);
[]s=1451 -> 4.953438*1/1:(s'=1461);
[]s=1452 -> 3.214297*1/1:(s'=1462);
[]s=1453 -> 4.929265*1/1:(s'=1463);
[]s=1454 -> 1.158923*1/1:(s'=1464);
[]s=1455 -> 81.746097*1/1:(s'=1465);
[]s=1456 -> 4.321708*1/1:(s'=1466);
[]s=1457 -> 3.136173*1/1:(s'=1467);
[]s=1458 -> 0.914829*1/1:(s'=1468);
[]s=1459 -> 22.394410*1/1:(s'=1469);
[]s=1460 -> 40.723245*1/1:(s'=1470);
[]s=1461 -> 725.952813*1/1:(s'=1471);
[]s=1462 -> 1.744257*1/1:(s'=1472);
[]s=1463 -> 420.079815*1/1:(s'=1473);
[]s=1464 -> 7.832080*1/1:(s'=1474);
[]s=1465 -> 7.716645*1/1:(s'=1475);
[]s=1466 -> 1.742737*1/1:(s'=1476);
[]s=1467 -> 15.788310*1/1:(s'=1477);
[]s=1468 -> 0.906947*1/1:(s'=1478);
[]s=1469 -> 14.630792*1/1:(s'=1479);
[]s=1470 -> 2.195052*1/1:(s'=1480);
[]s=1471 -> 4.209817*1/1:(s'=1481);
[]s=1472 -> 4.802613*1/1:(s'=1482);
[]s=1473 -> 2.746347*1/1:(s'=1483);
[]s=1474 -> 7.897647*1/1:(s'=1484);
[]s=1475 -> 1.583907*1/1:(s'=1485);
[]s=1476 -> 1.920492*1/1:(s'=1486);
[]s=1477 -> 16.638658*1/1:(s'=1487);
[]s=1478 -> 43.850033*1/1:(s'=1488);
[]s=1479 -> 8.400538*1/1:(s'=1489);
[]s=1480 -> 2.228611*1/1:(s'=1490);
[]s=1481 -> 2.685717*1/1:(s'=1491);
[]s=1482 -> 2.819999*1/1:(s'=1492);
[]s=1483 -> 4.323763*1/1:(s'=1493);
[]s=1484 -> 1 :(s'=1484);
[]s=1485 -> 1.877159*1/1:(s'=1494);
[]s=1486 -> 6.495194*1/1:(s'=1495);
[]s=1487 -> 28.460838*1/1:(s'=1496);
[]s=1488 -> 2.783035*1/1:(s'=1497);
[]s=1489 -> 2.847705*1/1:(s'=1498);
[]s=1490 -> 21.717413*1/1:(s'=1499);
[]s=1491 -> 1.402879*1/1:(s'=1500);
[]s=1492 -> 9.711566*1/1:(s'=1501);
[]s=1493 -> 4.677487*1/1:(s'=1502);
[]s=1494 -> 6.271952*1/1:(s'=1503);
[]s=1495 -> 1.030322*1/1:(s'=1504);
[]s=1496 -> 4.752852*1/1:(s'=1505);
[]s=1497 -> 7.899518*1/1:(s'=1506);
[]s=1498 -> 3.003725*1/1:(s'=1507);
[]s=1499 -> 4.968203*1/1:(s'=1508);
[]s=1500 -> 12.567235*1/1:(s'=1509);
[]s=1501 -> 14.307789*1/1:(s'=1510);
[]s=1502 -> 3.969199*1/1:(s'=1511);
[]s=1503 -> 21162.229653*1/1:(s'=1512);
[]s=1504 -> 16.661668*1/1:(s'=1513);
[]s=1505 -> 7.898894*1/1:(s'=1514);
[]s=1506 -> 6.356471*1/1:(s'=1515);
[]s=1507 -> 21.491511*1/1:(s'=1516);
[]s=1508 -> 64.470376*1/1:(s'=1517);
[]s=1509 -> 13.105473*1/1:(s'=1518);
[]s=1510 -> 4.468275*1/1:(s'=1519);
[]s=1511 -> 3.018048*1/1:(s'=1520);
[]s=1512 -> 3.103566*1/1:(s'=1521);
[]s=1513 -> 2.159687*1/1:(s'=1522);
[]s=1514 -> 31.986694*1/1:(s'=1523);
[]s=1515 -> 210.044319*1/1:(s'=1524);
[]s=1516 -> 0.984058*1/1:(s'=1525);
[]s=1517 -> 22.743296*1/1:(s'=1526);
[]s=1518 -> 12.139016*1/1:(s'=1527);
[]s=1519 -> 5.077431*1/1:(s'=1528);
[]s=1520 -> 1.566367*1/1:(s'=1529);
[]s=1521 -> 3.361006*1/1:(s'=1530);
[]s=1522 -> 20.799534*1/1:(s'=1531);
[]s=1523 -> 23.896576*1/1:(s'=1532);
[]s=1524 -> 1.058672*1/1:(s'=1533);
[]s=1525 -> 2.749141*1/1:(s'=1534);
[]s=1526 -> 1 :(s'=1526);
[]s=1527 -> 2.668873*1/1:(s'=1535);
[]s=1528 -> 2.053683*1/1:(s'=1536);
[]s=1529 -> 4.316671*1/1:(s'=1537);
[]s=1530 -> 1.871047*1/1:(s'=1538);
[]s=1531 -> 2.372704*1/1:(s'=1539);
[]s=1532 -> 1.587932*1/1:(s'=1540);
[]s=1533 -> 17.075628*1/1:(s'=1541);
[]s=1534 -> 7.631840*1/1:(s'=1542);
[]s=1535 -> 8.679802*1/1:(s'=1543);
[]s=1536 -> 1.076415*1/1:(s'=1544);
[]s=1537 -> 3.949447*1/1:(s'=1545);
[]s=1538 -> 3.131459*1/1:(s'=1546);
[]s=1539 -> 25.265285*1/1:(s'=1547);
[]s=1540 -> 1.038012*1/1:(s'=1548);
[]s=1541 -> 3.835974*1/1:(s'=1549);
[]s=1542 -> 15.868986*1/1:(s'=1550);
[]s=1543 -> 9.017133*1/1:(s'=1551);
[]s=1544 -> 7.379529*1/1:(s'=1552);
[]s=1545 -> 1.792950*1/1:(s'=1553);
[]s=1546 -> 4.844257*1/1:(s'=1554);
[]s=1547 -> 21.879923*1/1:(s'=1555);
[]s=1548 -> 1.793819*1/1:(s'=1556);
[]s=1549 -> 5.392289*1/1:(s'=1557);
[]s=1550 -> 1.778632*1/1:(s'=1558);
[]s=1551 -> 18.694035*1/1:(s'=1559);
[]s=1552 -> 5.652272*1/1:(s'=1560);
[]s=1553 -> 4.513043*1/1:(s'=1561);
[]s=1554 -> 12.593190*1/1:(s'=1562);
[]s=1555 -> 16.404469*1/1:(s'=1563);
[]s=1556 -> 35.343182*1/1:(s'=1564);
[]s=1557 -> 6.134969*1/1:(s'=1565);
[]s=1558 -> 122.806371*1/1:(s'=1566);
[]s=1559 -> 3.588474*1/1:(s'=1567);
[]s=1560 -> 4.515284*1/1:(s'=1568);
[]s=1561 -> 4.432231*1/1:(s'=1569);
[]s=1562 -> 1.640824*1/1:(s'=1570);
[]s=1563 -> 26.334501*1/1:(s'=1571);
[]s=1564 -> 113.308028*1/1:(s'=1572);
[]s=1565 -> 2.455916*1/1:(s'=1573);
[]s=1566 -> 27.489897*1/1:(s'=1574);
[]s=1567 -> 4.286878*1/1:(s'=1575);
[]s=1568 -> 1 :(s'=1568);
[]s=1569 -> 1.734816*1/1:(s'=1576);
[]s=1570 -> 3.975511*1/1:(s'=1577);
[]s=1571 -> 15.628174*1/1:(s'=1578);
[]s=1572 -> 6.205014*1/1:(s'=1579);
[]s=1573 -> 4.015258*1/1:(s'=1580);
[]s=1574 -> 14.271239*1/1:(s'=1581);
[]s=1575 -> 3.451132*1/1:(s'=1582);
[]s=1576 -> 0.704126*1/1:(s'=1583);
[]s=1577 -> 354.748306*1/1:(s'=1584);
[]s=1578 -> 2.183025*1/1:(s'=1585);
[]s=1579 -> 35.525241*1/1:(s'=1586);
[]s=1580 -> 3.078060*1/1:(s'=1587);
[]s=1581 -> 11.778147*1/1:(s'=1588);
[]s=1582 -> 1.589623*1/1:(s'=1589);
[]s=1583 -> 0.846382*1/1:(s'=1590);
[]s=1584 -> 8.181298*1/1:(s'=1591);
[]s=1585 -> 2.609263*1/1:(s'=1592);
[]s=1586 -> 2.589801*1/1:(s'=1593);
[]s=1587 -> 28.123857*1/1:(s'=1594);
[]s=1588 -> 2.295684*1/1:(s'=1595);
[]s=1589 -> 57.152655*1/1:(s'=1596);
[]s=1590 -> 2.488800*1/1:(s'=1597);
[]s=1591 -> 2.047041*1/1:(s'=1598);
[]s=1592 -> 9.303191*1/1:(s'=1599);
[]s=1593 -> 13.756861*1/1:(s'=1600);
[]s=1594 -> 1.386963*1/1:(s'=1601);
[]s=1595 -> 1.227009*1/1:(s'=1602);
[]s=1596 -> 1.597980*1/1:(s'=1603);
[]s=1597 -> 3.603733*1/1:(s'=1604);
[]s=1598 -> 1.070893*1/1:(s'=1605);
[]s=1599 -> 2.819045*1/1:(s'=1606);
[]s=1600 -> 3.299241*1/1:(s'=1607);
[]s=1601 -> 6.616382*1/1:(s'=1608);
[]s=1602 -> 25.744664*1/1:(s'=1609);
[]s=1603 -> 6.190800*1/1:(s'=1610);
[]s=1604 -> 4.978096*1/1:(s'=1611);
[]s=1605 -> 7.742335*1/1:(s'=1612);
[]s=1606 -> 1 :(s'=1606);
[]s=1607 -> 1.634441*1/1:(s'=1613);
[]s=1608 -> 5.464182*1/1:(s'=1614);
[]s=1609 -> 3.844823*1/1:(s'=1615);
[]s=1610 -> 1.991516*1/1:(s'=1616);
[]s=1611 -> 1.784694*1/1:(s'=1617);
[]s=1612 -> 10.371615*1/1:(s'=1618);
[]s=1613 -> 2.843979*1/1:(s'=1619);
[]s=1614 -> 18.866857*1/1:(s'=1620);
[]s=1615 -> 2.270611*1/1:(s'=1621);
[]s=1616 -> 1.245966*1/1:(s'=1622);
[]s=1617 -> 4.954665*1/1:(s'=1623);
[]s=1618 -> 12.418658*1/1:(s'=1624);
[]s=1619 -> 1.243085*1/1:(s'=1625);
[]s=1620 -> 3.090808*1/1:(s'=1626);
[]s=1621 -> 6.079397*1/1:(s'=1627);
[]s=1622 -> 16.050849*1/1:(s'=1628);
[]s=1623 -> 1.515312*1/1:(s'=1629);
[]s=1624 -> 0.973710*1/1:(s'=1630);
[]s=1625 -> 17.864161*1/1:(s'=1631);
[]s=1626 -> 20.873341*1/1:(s'=1632);
[]s=1627 -> 13.437609*1/1:(s'=1633);
[]s=1628 -> 26.063386*1/1:(s'=1634);
[]s=1629 -> 5.883391*1/1:(s'=1635);
[]s=1630 -> 125.911283*1/1:(s'=1636);
[]s=1631 -> 6.516356*1/1:(s'=1637);
[]s=1632 -> 23.389077*1/1:(s'=1638);
[]s=1633 -> 6.530399*1/1:(s'=1639);
[]s=1634 -> 4.465482*1/1:(s'=1640);
[]s=1635 -> 106.423737*1/1:(s'=1641);
[]s=1636 -> 30.428432*1/1:(s'=1642);
[]s=1637 -> 2.119273*1/1:(s'=1643);
[]s=1638 -> 1.581378*1/1:(s'=1644);
[]s=1639 -> 1.148435*1/1:(s'=1645);
[]s=1640 -> 3.189182*1/1:(s'=1646);
[]s=1641 -> 4.329942*1/1:(s'=1647);
[]s=1642 -> 434.593655*1/1:(s'=1648);
[]s=1643 -> 2.564497*1/1:(s'=1649);
[]s=1644 -> 11.386539*1/1:(s'=1650);
[]s=1645 -> 0.991670*1/1:(s'=1651);
[]s=1646 -> 12.121653*1/1:(s'=1652);
[]s=1647 -> 5.934014*1/1:(s'=1653);
[]s=1648 -> 11.583459*1/1:(s'=1654);
[]s=1649 -> 1.408193*1/1:(s'=1655);
[]s=1650 -> 1.721052*1/1:(s'=1656);
[]s=1651 -> 2.169197*1/1:(s'=1657);
[]s=1652 -> 4.953928*1/1:(s'=1658);
[]s=1653 -> 4.292398*1/1:(s'=1659);
[]s=1654 -> 7.160246*1/1:(s'=1660);
[]s=1655 -> 10.621687*1/1:(s'=1661);
[]s=1656 -> 3.545848*1/1:(s'=1662);
[]s=1657 -> 2.082379*1/1:(s'=1663);
[]s=1658 -> 2.605320*1/1:(s'=1664);
[]s=1659 -> 6.824075*1/1:(s'=1665);
[]s=1660 -> 2.605524*1/1:(s'=1666);
[]s=1661 -> 5.337034*1/1:(s'=1667);
[]s=1662 -> 2.493890*1/1:(s'=1668);
[]s=1663 -> 39.241848*1/1:(s'=1669);
[]s=1664 -> 39.452401*1/1:(s'=1670);
[]s=1665 -> 13.658403*1/1:(s'=1671);
[]s=1666 -> 41.240515*1/1:(s'=1672);
[]s=1667 -> 9.351038*1/1:(s'=1673);
[]s=1668 -> 11.264813*1/1:(s'=1674);
[]s=1669 -> 3.966995*1/1:(s'=1675);
[]s=1670 -> 86.266391*1/1:(s'=1676);
[]s=1671 -> 5.069451*1/1:(s'=1677);
[]s=1672 -> 4.706990*1/1:(s'=1678);
[]s=1673 -> 61.580147*1/1:(s'=1679);
[]s=1674 -> 14.824478*1/1:(s'=1680);
[]s=1675 -> 37.210687*1/1:(s'=1681);
[]s=1676 -> 7.917030*1/1:(s'=1682);
[]s=1677 -> 2.350176*1/1:(s'=1683);
[]s=1678 -> 10.422529*1/1:(s'=1684);
[]s=1679 -> 152.376309*1/1:(s'=1685);
[]s=1680 -> 34.268874*1/1:(s'=1686);
[]s=1681 -> 186.094983*1/1:(s'=1687);
[]s=1682 -> 2.556629*1/1:(s'=1688);
[]s=1683 -> 1.338384*1/1:(s'=1689);
[]s=1684 -> 1.697447*1/1:(s'=1690);
[]s=1685 -> 1 :(s'=1685);
[]s=1686 -> 12.707288*1/1:(s'=1691);
[]s=1687 -> 1 :(s'=1687);
[]s=1688 -> 4.634779*1/1:(s'=1692);
[]s=1689 -> 2.239943*1/1:(s'=1693);
[]s=1690 -> 18.532246*1/1:(s'=1694);
[]s=1691 -> 6.494350*1/1:(s'=1695);
[]s=1692 -> 4.826255*1/1:(s'=1696);
[]s=1693 -> 2.510923*1/1:(s'=1697);
[]s=1694 -> 22.662376*1/1:(s'=1698);
[]s=1695 -> 8.197393*1/1:(s'=1699);
[]s=1696 -> 12.122535*1/1:(s'=1700);
[]s=1697 -> 33.928208*1/1:(s'=1701);
[]s=1698 -> 11.460793*1/1:(s'=1702);
[]s=1699 -> 4.059430*1/1:(s'=1703);
[]s=1700 -> 3.360441*1/1:(s'=1704);
[]s=1701 -> 1.091393*1/1:(s'=1705);
[]s=1702 -> 2.304094*1/1:(s'=1706);
[]s=1703 -> 10.947267*1/1:(s'=1707);
[]s=1704 -> 8.848774*1/1:(s'=1708);
[]s=1705 -> 6.125574*1/1:(s'=1709);
[]s=1706 -> 16.440608*1/1:(s'=1710);
[]s=1707 -> 7.481110*1/1:(s'=1711);
[]s=1708 -> 15.278839*1/1:(s'=1712);
[]s=1709 -> 19.506105*1/1:(s'=1713);
[]s=1710 -> 1.902443*1/1:(s'=1714);
[]s=1711 -> 25.986851*1/1:(s'=1715);
[]s=1712 -> 4.390972*1/1:(s'=1716);
[]s=1713 -> 35.114825*1/1:(s'=1717);
[]s=1714 -> 1.661544*1/1:(s'=1718);
[]s=1715 -> 15.129509*1/1:(s'=1719);
[]s=1716 -> 3.014681*1/1:(s'=1720);
[]s=1717 -> 15.700559*1/1:(s'=1721);
[]s=1718 -> 2.763042*1/1:(s'=1722);
[]s=1719 -> 2.502628*1/1:(s'=1723);
[]s=1720 -> 7.026913*1/1:(s'=1724);
[]s=1721 -> 4.609782*1/1:(s'=1725);
[]s=1722 -> 2.916302*1/1:(s'=1726);
[]s=1723 -> 2.061261*1/1:(s'=1727);
[]s=1724 -> 2.131015*1/1:(s'=1728);
[]s=1725 -> 9.744689*1/1:(s'=1729);
[]s=1726 -> 3.640733*1/1:(s'=1730);
[]s=1727 -> 3.364738*1/1:(s'=1731);
[]s=1728 -> 0.584966*1/1:(s'=1732);
[]s=1729 -> 2.159501*1/1:(s'=1733);
[]s=1730 -> 1.992588*1/1:(s'=1734);
[]s=1731 -> 4.071495*1/1:(s'=1735);
[]s=1732 -> 7.859781*1/1:(s'=1736);
[]s=1733 -> 1.345714*1/1:(s'=1737);
[]s=1734 -> 28.588582*1/1:(s'=1738);
[]s=1735 -> 14.718653*1/1:(s'=1739);
[]s=1736 -> 2.823104*1/1:(s'=1740);
[]s=1737 -> 6.040836*1/1:(s'=1741);
[]s=1738 -> 1.978787*1/1:(s'=1742);
[]s=1739 -> 3.391095*1/1:(s'=1743);
[]s=1740 -> 1.640178*1/1:(s'=1744);
[]s=1741 -> 1.721793*1/1:(s'=1745);
[]s=1742 -> 3.560112*1/1:(s'=1746);
[]s=1743 -> 14.421898*1/1:(s'=1747);
[]s=1744 -> 2.700221*1/1:(s'=1748);
[]s=1745 -> 1.706339*1/1:(s'=1749);
[]s=1746 -> 7.017051*1/1:(s'=1750);
[]s=1747 -> 3.323805*1/1:(s'=1751);
[]s=1748 -> 3.542205*1/1:(s'=1752);
[]s=1749 -> 6.626466*1/1:(s'=1753);
[]s=1750 -> 8.856611*1/1:(s'=1754);
[]s=1751 -> 2.367929*1/1:(s'=1755);
[]s=1752 -> 2.406797*1/1:(s'=1756);
[]s=1753 -> 14.947460*1/1:(s'=1757);
[]s=1754 -> 29.897154*1/1:(s'=1758);
[]s=1755 -> 13.785308*1/1:(s'=1759);
[]s=1756 -> 8.401243*1/1:(s'=1760);
[]s=1757 -> 1.461860*1/1:(s'=1761);
[]s=1758 -> 20.169016*1/1:(s'=1762);
[]s=1759 -> 18.025813*1/1:(s'=1763);
[]s=1760 -> 19.530869*1/1:(s'=1764);
[]s=1761 -> 6.804110*1/1:(s'=1765);
[]s=1762 -> 7.782707*1/1:(s'=1766);
[]s=1763 -> 7.038288*1/1:(s'=1767);
[]s=1764 -> 7.722604*1/1:(s'=1768);
[]s=1765 -> 7.533524*1/1:(s'=1769);
[]s=1766 -> 12.782820*1/1:(s'=1770);
[]s=1767 -> 10.250628*1/1:(s'=1771);
[]s=1768 -> 23.953243*1/1:(s'=1772);
[]s=1769 -> 3.818834*1/1:(s'=1773);
[]s=1770 -> 107.820199*1/1:(s'=1774);
[]s=1771 -> 3.140999*1/1:(s'=1775);
[]s=1772 -> 4.371011*1/1:(s'=1776);
[]s=1773 -> 4.508973*1/1:(s'=1777);
[]s=1774 -> 8.967001*1/1:(s'=1778);
[]s=1775 -> 4.416961*1/1:(s'=1779);
[]s=1776 -> 3.688948*1/1:(s'=1780);
[]s=1777 -> 7.731560*1/1:(s'=1781);
[]s=1778 -> 4.345370*1/1:(s'=1782);
[]s=1779 -> 4.663744*1/1:(s'=1783);
[]s=1780 -> 3.753895*1/1:(s'=1784);
[]s=1781 -> 4.882336*1/1:(s'=1785);
[]s=1782 -> 1.762518*1/1:(s'=1786);
[]s=1783 -> 14.515895*1/1:(s'=1787);
[]s=1784 -> 9.828976*1/1:(s'=1788);
[]s=1785 -> 4.510600*1/1:(s'=1789);
[]s=1786 -> 8.950148*1/1:(s'=1790);
[]s=1787 -> 4.197096*1/1:(s'=1791);
[]s=1788 -> 4.634350*1/1:(s'=1792);
[]s=1789 -> 2.507963*1/1:(s'=1793);
[]s=1790 -> 68.889501*1/1:(s'=1794);
[]s=1791 -> 1.372401*1/1:(s'=1795);
[]s=1792 -> 5.585968*1/1:(s'=1796);
[]s=1793 -> 2.438549*1/1:(s'=1797);
[]s=1794 -> 13.414536*1/1:(s'=1798);
[]s=1795 -> 18.520919*1/1:(s'=1799);
[]s=1796 -> 11.869436*1/1:(s'=1800);
[]s=1797 -> 9.590486*1/1:(s'=1801);
[]s=1798 -> 3.403328*1/1:(s'=1802);
[]s=1799 -> 5.413599*1/1:(s'=1803);
[]s=1800 -> 12.562183*1/1:(s'=1804);
[]s=1801 -> 0.733138*1/1:(s'=1805);
[]s=1802 -> 5.786702*1/1:(s'=1806);
[]s=1803 -> 25.133206*1/1:(s'=1807);
[]s=1804 -> 35.401990*1/1:(s'=1808);
[]s=1805 -> 0.947688*1/1:(s'=1809);
[]s=1806 -> 1.038875*1/1:(s'=1810);
[]s=1807 -> 2.000720*1/1:(s'=1811);
[]s=1808 -> 4.802151*1/1:(s'=1812);
[]s=1809 -> 1.598951*1/1:(s'=1813);
[]s=1810 -> 1.846483*1/1:(s'=1814);
[]s=1811 -> 13.504936*1/1:(s'=1815);
[]s=1812 -> 18.749063*1/1:(s'=1816);
[]s=1813 -> 247.121040*1/1:(s'=1817);
[]s=1814 -> 2.758621*1/1:(s'=1818);
[]s=1815 -> 20.042490*1/1:(s'=1819);
[]s=1816 -> 4.428698*1/1:(s'=1820);
[]s=1817 -> 3.585257*1/1:(s'=1821);
[]s=1818 -> 15.937271*1/1:(s'=1822);
[]s=1819 -> 184.692671*1/1:(s'=1823);
[]s=1820 -> 3.427475*1/1:(s'=1824);
[]s=1821 -> 2.412196*1/1:(s'=1825);
[]s=1822 -> 2.085027*1/1:(s'=1826);
[]s=1823 -> 0.569249*1/1:(s'=1827);
[]s=1824 -> 2.733137*1/1:(s'=1828);
[]s=1825 -> 5.633485*1/1:(s'=1829);
[]s=1826 -> 2.138534*1/1:(s'=1830);
[]s=1827 -> 17.346355*1/1:(s'=1831);
[]s=1828 -> 3.774012*1/1:(s'=1832);
[]s=1829 -> 2.729332*1/1:(s'=1833);
[]s=1830 -> 34.910106*1/1:(s'=1834);
[]s=1831 -> 17.433144*1/1:(s'=1835);
[]s=1832 -> 1.798885*1/1:(s'=1836);
[]s=1833 -> 10.474275*1/1:(s'=1837);
[]s=1834 -> 6.705559*1/1:(s'=1838);
[]s=1835 -> 30.788177*1/1:(s'=1839);
[]s=1836 -> 1.269374*1/1:(s'=1840);
[]s=1837 -> 12.794432*1/1:(s'=1841);
[]s=1838 -> 1 :(s'=1838);
[]s=1839 -> 7.297140*1/1:(s'=1842);
[]s=1840 -> 50.528018*1/1:(s'=1843);
[]s=1841 -> 26.172529*1/1:(s'=1844);
[]s=1842 -> 3.738737*1/1:(s'=1845);
[]s=1843 -> 26.857895*1/1:(s'=1846);
[]s=1844 -> 1.467739*1/1:(s'=1847);
[]s=1845 -> 9.509319*1/1:(s'=1848);
[]s=1846 -> 8.536794*1/1:(s'=1849);
[]s=1847 -> 4.629201*1/1:(s'=1850);
[]s=1848 -> 34.973595*1/1:(s'=1851);
[]s=1849 -> 2.660777*1/1:(s'=1852);
[]s=1850 -> 5.305321*1/1:(s'=1853);
[]s=1851 -> 3.090044*1/1:(s'=1854);
[]s=1852 -> 3.161056*1/1:(s'=1855);
[]s=1853 -> 8.448087*1/1:(s'=1856);
[]s=1854 -> 3.045438*1/1:(s'=1857);
[]s=1855 -> 4.552283*1/1:(s'=1858);
[]s=1856 -> 10.897401*1/1:(s'=1859);
[]s=1857 -> 130.636986*1/1:(s'=1860);
[]s=1858 -> 8.187326*1/1:(s'=1861);
[]s=1859 -> 1.096131*1/1:(s'=1862);
[]s=1860 -> 6.545359*1/1:(s'=1863);
[]s=1861 -> 1.714060*1/1:(s'=1864);
[]s=1862 -> 11.077632*1/1:(s'=1865);
[]s=1863 -> 7.898894*1/1:(s'=1866);
[]s=1864 -> 8.822232*1/1:(s'=1867);
[]s=1865 -> 3.466805*1/1:(s'=1868);
[]s=1866 -> 3.228306*1/1:(s'=1869);
[]s=1867 -> 19.425019*1/1:(s'=1870);
[]s=1868 -> 2.243360*1/1:(s'=1871);
[]s=1869 -> 14.166714*1/1:(s'=1872);
[]s=1870 -> 3.276647*1/1:(s'=1873);
[]s=1871 -> 11.434191*1/1:(s'=1874);
[]s=1872 -> 9.490367*1/1:(s'=1875);
[]s=1873 -> 53.078556*1/1:(s'=1876);
[]s=1874 -> 494.902504*1/1:(s'=1877);
[]s=1875 -> 10.141268*1/1:(s'=1878);
[]s=1876 -> 1.198021*1/1:(s'=1879);
[]s=1877 -> 4.067521*1/1:(s'=1880);
[]s=1878 -> 1 :(s'=1878);
[]s=1879 -> 9.371193*1/1:(s'=1881);
[]s=1880 -> 0.974659*1/1:(s'=1882);
[]s=1881 -> 2.255198*1/1:(s'=1883);
[]s=1882 -> 24.554339*1/1:(s'=1884);
[]s=1883 -> 1 :(s'=1883);
[]s=1884 -> 2.889839*1/1:(s'=1885);
[]s=1885 -> 1.624616*1/1:(s'=1886);
[]s=1886 -> 5.070223*1/1:(s'=1887);
[]s=1887 -> 39.902638*1/1:(s'=1888);
[]s=1888 -> 1 :(s'=1888);
endmodule

label "o_00002" = s=963;
label "o_00004" = s=1021;
label "o_00010" = s=1241 | s=1631 | s=1643;
label "o_00011" = s=1052 | s=1078 | s=1637;
label "o_00012" = s=1039;
label "o_00013" = s=1735;
label "o_00102" = s=948 | s=1210 | s=1234 | s=1635 | s=1813 | s=1829 | s=1837;
label "o_00103" = s=1024 | s=1222 | s=1689 | s=1817 | s=1825 | s=1841;
label "o_00104" = s=1683 | s=1821;
label "o_00110" = s=1053 | s=1072 | s=1079 | s=1150;
label "o_00111" = s=872 | s=1301 | s=1361 | s=1549 | s=1682 | s=1740;
label "o_00112" = s=504 | s=855 | s=889 | s=1198 | s=1291 | s=1311 | s=1351 | s=1712 | s=1728 | s=1736 | s=1833;
label "o_00113" = s=906 | s=1236 | s=1275 | s=1321 | s=1341 | s=1732;
label "o_00114" = s=923;
label "o_01000" = s=840;
label "o_01001" = s=596;
label "o_01002" = s=978;
label "o_01010" = s=858 | s=1076 | s=1251;
label "o_01011" = s=616 | s=834 | s=909 | s=942 | s=1063 | s=1091 | s=1138 | s=1261;
label "o_01012" = s=926 | s=958 | s=1050 | s=1125 | s=1271 | s=1727;
label "o_01013" = s=196 | s=265 | s=1037 | s=1731;
label "o_01014" = s=231;
label "o_01100" = s=786 | s=822 | s=1124 | s=1221 | s=1696;
label "o_01101" = s=841 | s=1551 | s=1562 | s=1623 | s=1698 | s=1706 | s=1722 | s=1805;
label "o_01102" = s=932 | s=1017 | s=1345 | s=1543 | s=1629 | s=1702 | s=1718 | s=1809;
label "o_01103" = s=734 | s=1355 | s=1820 | s=1844;
label "o_01104" = s=1847;
label "o_01110" = s=768 | s=803 | s=839 | s=1040 | s=1059 | s=1085 | s=1092 | s=1111 | s=1137 | s=1459 | s=1479 | s=1583 | s=1692 | s=1700 | s=1818;
label "o_01111" = s=301 | s=516 | s=635 | s=785 | s=821 | s=823 | s=827 | s=852 | s=891 | s=898 | s=921 | s=1046 | s=1131 | s=1151 | s=1409 | s=1449 | s=1538 | s=1545 | s=1554 | s=1559 | s=1561 | s=1590 | s=1617 | s=1688 | s=1704 | s=1814 | s=1822;
label "o_01112" = s=182 | s=331 | s=492 | s=539 | s=654 | s=699 | s=767 | s=809 | s=837 | s=908 | s=915 | s=938 | s=1002 | s=1032 | s=1112 | s=1136 | s=1281 | s=1335 | s=1419 | s=1475 | s=1535 | s=1537 | s=1567 | s=1708 | s=1810 | s=1826;
label "o_01113" = s=147 | s=561 | s=673 | s=680 | s=711 | s=749 | s=920 | s=925 | s=954 | s=985 | s=987 | s=1285 | s=1305 | s=1325 | s=1405 | s=1465 | s=1509 | s=1527 | s=1798 | s=1806;
label "o_01114" = s=692 | s=730 | s=970 | s=1295 | s=1315 | s=1455 | s=1500 | s=1518 | s=1802;
label "o_10000" = s=1619;
label "o_10001" = s=897 | s=1613 | s=1750;
label "o_10002" = s=914 | s=947;
label "o_10003" = s=931 | s=991;
label "o_10004" = s=1006 | s=1035;
label "o_10010" = s=565 | s=706 | s=1102 | s=1205 | s=1229 | s=1625 | s=1649;
label "o_10011" = s=488 | s=536 | s=880 | s=1065;
label "o_10012" = s=462 | s=513 | s=558 | s=1025 | s=1248 | s=1743;
label "o_10013" = s=945 | s=976 | s=1010 | s=1061 | s=1087 | s=1113 | s=1238 | s=1739;
label "o_10014" = s=1048;
label "o_10100" = s=563 | s=1467 | s=1523;
label "o_10101" = s=1477 | s=1480 | s=1514 | s=1532 | s=1738;
label "o_10102" = s=964 | s=994 | s=1174 | s=1245 | s=1444 | s=1484 | s=1487 | s=1505 | s=1641 | s=1767;
label "o_10103" = s=481 | s=979 | s=1009 | s=1038 | s=1064 | s=1255 | s=1360 | s=1454 | s=1474 | s=1496 | s=1647 | s=1659 | s=1671 | s=1693;
label "o_10104" = s=1051 | s=1464 | s=1653 | s=1677 | s=1697;
label "o_10110" = s=687 | s=1066 | s=1109 | s=1193 | s=1658;
label "o_10111" = s=372 | s=426 | s=453 | s=668 | s=863 | s=1069 | s=1095 | s=1181 | s=1371 | s=1490 | s=1541 | s=1557 | s=1664 | s=1676 | s=1744;
label "o_10112" = s=343 | s=400 | s=452 | s=479 | s=498 | s=527 | s=571 | s=691 | s=949 | s=1082 | s=1108 | s=1162 | s=1164 | s=1186 | s=1212 | s=1256 | s=1381 | s=1434 | s=1565 | s=1670 | s=1716 | s=1724;
label "o_10113" = s=314 | s=473 | s=478 | s=549 | s=826 | s=829 | s=899 | s=933 | s=956 | s=1018 | s=1126 | s=1152 | s=1176 | s=1224 | s=1246 | s=1265 | s=1266 | s=1331 | s=1881;
label "o_10114" = s=811 | s=940 | s=1033 | s=1400 | s=1780;
label "o_11000" = s=1675 | s=1687;
label "o_11001" = s=576 | s=846 | s=1666 | s=1746 | s=1754;
label "o_11002" = s=756 | s=993 | s=1313 | s=1660 | s=1758;
label "o_11003" = s=1008 | s=1654 | s=1762;
label "o_11004" = s=1648;
label "o_11010" = s=315 | s=725 | s=815 | s=851 | s=875 | s=1089 | s=1403 | s=1443;
label "o_11011" = s=283 | s=344 | s=554 | s=744 | s=816 | s=864 | s=892 | s=960 | s=989 | s=1104 | s=1130 | s=1293 | s=1327 | s=1433 | s=1524 | s=1711;
label "o_11012" = s=373 | s=762 | s=798 | s=974 | s=1004 | s=1263 | s=1283 | s=1303 | s=1317 | s=1578 | s=1707 | s=1715 | s=1723;
label "o_11013" = s=161 | s=297 | s=601 | s=682 | s=780 | s=1019 | s=1023 | s=1253 | s=1273 | s=1695 | s=1703 | s=1719 | s=1766 | s=1774 | s=1790;
label "o_11014" = s=621 | s=625 | s=1699 | s=1770 | s=1778 | s=1786;
label "o_11100" = s=541 | s=804 | s=1209 | s=1233 | s=1498 | s=1595 | s=1633 | s=1669 | s=1730;
label "o_11101" = s=287 | s=348 | s=467 | s=608 | s=859 | s=1148 | s=1175 | s=1197 | s=1199 | s=1570 | s=1663 | s=1694 | s=1710 | s=1726 | s=1734 | s=1742 | s=1775 | s=1777 | s=1801 | s=1832 | s=1869 | s=1875;
label "o_11102" = s=181 | s=319 | s=493 | s=588 | s=628 | s=696 | s=704 | s=738 | s=876 | s=1187 | s=1211 | s=1235 | s=1709 | s=1714 | s=1771 | s=1828 | s=1836 | s=1878;
label "o_11103" = s=78 | s=224 | s=246 | s=307 | s=308 | s=517 | s=647 | s=681 | s=715 | s=760 | s=1223 | s=1365 | s=1705 | s=1816 | s=1824 | s=1853;
label "o_11104" = s=212 | s=276 | s=540 | s=585 | s=1282 | s=1701 | s=1850;
label "o_11110" = s=509 | s=518 | s=556 | s=713 | s=750 | s=787 | s=853 | s=857 | s=1026 | s=1044 | s=1096 | s=1098 | s=1105 | s=1122 | s=1469 | s=1488 | s=1489 | s=1576 | s=1639 | s=1652;
label "o_11111" = s=250 | s=269 | s=321 | s=532 | s=656 | s=694 | s=737 | s=800 | s=805 | s=835 | s=845 | s=869 | s=870 | s=874 | s=881 | s=904 | s=944 | s=1030 | s=1118 | s=1135 | s=1143 | s=1144 | s=1163 | s=1169 | s=1354 | s=1399 | s=1439 | s=1497 | s=1499 | s=1517 | s=1520 | s=1530 | s=1533 | s=1546 | s=1553 | s=1569 | s=1580 | s=1597 | s=1611 | s=1634 | s=1646 | s=1781 | s=1789 | s=1834 | s=1880 | s=1886;
label "o_11112" = s=216 | s=217 | s=235 | s=354 | s=360 | s=457 | s=466 | s=603 | s=672 | s=675 | s=710 | s=717 | s=718 | s=754 | s=755 | s=782 | s=791 | s=819 | s=886 | s=893 | s=927 | s=928 | s=1015 | s=1016 | s=1071 | s=1099 | s=1123 | s=1149 | s=1156 | s=1344 | s=1385 | s=1411 | s=1429 | s=1451 | s=1471 | s=1485 | s=1503 | s=1526 | s=1529 | s=1573 | s=1575 | s=1587 | s=1604 | s=1628 | s=1830 | s=1838;
label "o_11113" = s=112 | s=200 | s=251 | s=325 | s=431 | s=447 | s=487 | s=490 | s=582 | s=583 | s=615 | s=623 | s=653 | s=661 | s=729 | s=736 | s=772 | s=773 | s=808 | s=903 | s=910 | s=911 | s=937 | s=943 | s=972 | s=1000 | s=1280 | s=1375 | s=1395 | s=1415 | s=1421 | s=1435 | s=1461 | s=1481 | s=1494 | s=1582 | s=1622 | s=1794;
label "o_11114" = s=177 | s=421 | s=461 | s=562 | s=564 | s=605 | s=642 | s=790 | s=793 | s=1272 | s=1425 | s=1445 | s=1491 | s=1589 | s=1616;
label "o_20000" = s=468 | s=1447 | s=1572;
label "o_20001" = s=1564 | s=1607;
label "o_20010" = s=543 | s=1115 | s=1217 | s=1402 | s=1437 | s=1442 | s=1458 | s=1655;
label "o_20011" = s=1128 | s=1154 | s=1178 | s=1412 | s=1432;
label "o_20012" = s=436 | s=446 | s=497 | s=572 | s=1134 | s=1166 | s=1190 | s=1258 | s=1747;
label "o_20013" = s=420 | s=929 | s=961 | s=995 | s=1074 | s=1100 | s=1147 | s=1202 | s=1207 | s=1226 | s=1368 | s=1751;
label "o_20014" = s=912 | s=1214 | s=1219;
label "o_20100" = s=584 | s=1457 | s=1548 | s=1609 | s=1621;
label "o_20101" = s=604 | s=1470 | s=1540 | s=1556 | s=1612;
label "o_20102" = s=620 | s=624 | s=1116 | s=1142 | s=1460 | s=1608 | s=1725 | s=1741 | s=1757 | s=1763;
label "o_20103" = s=455 | s=506 | s=643 | s=671 | s=1077 | s=1129 | s=1350 | s=1370 | s=1665 | s=1721;
label "o_20110" = s=630;
label "o_20111" = s=392 | s=427 | s=611 | s=649 | s=1056 | s=1414 | s=1591 | s=1748;
label "o_20112" = s=159 | s=364 | s=401 | s=418 | s=591 | s=783 | s=794 | s=865 | s=965 | s=1043 | s=1121 | s=1200 | s=1324 | s=1330 | s=1391 | s=1424 | s=1430 | s=1450 | s=1720 | s=1737 | s=1759;
label "o_20113" = s=57 | s=194 | s=263 | s=282 | s=503 | s=652 | s=844 | s=847 | s=882 | s=916 | s=980 | s=1003 | s=1060 | s=1139 | s=1188 | s=1276 | s=1296 | s=1314 | s=1340 | s=1380 | s=1420 | s=1755 | s=1764 | s=1788 | s=1873 | s=1879 | s=1883;
label "o_20114" = s=229 | s=526 | s=862 | s=1047 | s=1204 | s=1228 | s=1250 | s=1390 | s=1410 | s=1768 | s=1776 | s=1784;
label "o_21000" = s=399 | s=502 | s=1579 | s=1681;
label "o_21001" = s=371 | s=425 | s=828 | s=1672;
label "o_21002" = s=253 | s=342 | s=528 | s=774 | s=810 | s=1298 | s=1323 | s=1343;
label "o_21003" = s=285 | s=792 | s=1308 | s=1333 | s=1686;
label "o_21004" = s=317 | s=1642;
label "o_21010" = s=797 | s=833 | s=1392 | s=1393 | s=1413 | s=1448 | s=1453 | s=1468 | s=1473 | s=1661;
label "o_21011" = s=1117 | s=1337 | s=1357 | s=1383 | s=1423 | s=1438 | s=1463 | s=1515;
label "o_21012" = s=410 | s=550 | s=1307 | s=1373 | s=1428 | s=1571 | s=1585;
label "o_21013" = s=126 | s=143 | s=280 | s=327 | s=581 | s=663 | s=701 | s=739 | s=1243 | s=1378 | s=1418 | s=1592 | s=1606 | s=1691;
label "o_21014" = s=91 | s=640 | s=644 | s=720 | s=895 | s=1231 | s=1388 | s=1408 | s=1782;
label "o_21100" = s=569 | s=1507 | s=1525 | s=1574 | s=1588 | s=1602 | s=1627 | s=1651;
label "o_21101" = s=114 | s=134 | s=255 | s=266 | s=377 | s=441 | s=546 | s=1161 | s=1185 | s=1577 | s=1581 | s=1618 | s=1657 | s=1690 | s=1773 | s=1779 | s=1795 | s=1797 | s=1803 | s=1811 | s=1866 | s=1868 | s=1872;
label "o_21102" = s=80 | s=146 | s=169 | s=219 | s=298 | s=357 | s=412 | s=523 | s=568 | s=677 | s=685 | s=719 | s=723 | s=1173 | s=1225 | s=1601 | s=1614 | s=1624 | s=1626 | s=1713 | s=1769 | s=1783 | s=1791 | s=1799 | s=1840 | s=1863 | s=1871;
label "o_21103" = s=44 | s=46 | s=76 | s=111 | s=189 | s=254 | s=258 | s=275 | s=279 | s=328 | s=337 | s=385 | s=438 | s=662 | s=666 | s=700 | s=742 | s=778 | s=1213 | s=1237 | s=1630 | s=1717 | s=1796 | s=1812 | s=1856 | s=1860;
label "o_21104" = s=19 | s=41 | s=154 | s=243 | s=290 | s=1292 | s=1636 | s=1800 | s=1808;
label "o_21110" = s=484 | s=494 | s=501 | s=534 | s=578 | s=589 | s=617 | s=655 | s=731 | s=732 | s=769 | s=1011 | s=1057 | s=1083 | s=1239 | s=1319 | s=1382 | s=1478 | s=1502 | s=1568 | s=1645 | s=1884;
label "o_21111" = s=179 | s=245 | s=289 | s=349 | s=350 | s=359 | s=408 | s=415 | s=458 | s=508 | s=598 | s=609 | s=637 | s=674 | s=751 | s=817 | s=818 | s=831 | s=866 | s=887 | s=900 | s=957 | s=996 | s=1045 | s=1157 | s=1287 | s=1289 | s=1309 | s=1329 | s=1346 | s=1364 | s=1384 | s=1389 | s=1506 | s=1508 | s=1511 | s=1521 | s=1584 | s=1640 | s=1785 | s=1793 | s=1877 | s=1882 | s=1885 | s=1887;
label "o_21112" = s=43 | s=48 | s=144 | s=257 | s=320 | s=335 | s=378 | s=379 | s=381 | s=383 | s=387 | s=388 | s=391 | s=432 | s=434 | s=440 | s=444 | s=483 | s=531 | s=535 | s=545 | s=575 | s=657 | s=698 | s=764 | s=801 | s=812 | s=836 | s=848 | s=971 | s=973 | s=1001 | s=1031 | s=1058 | s=1084 | s=1086 | s=1094 | s=1110 | s=1168 | s=1277 | s=1297 | s=1300 | s=1320 | s=1334 | s=1336 | s=1374 | s=1401 | s=1441 | s=1512 | s=1594 | s=1849 | s=1874 | s=1888;
label "o_21113" = s=18 | s=21 | s=27 | s=79 | s=81 | s=107 | s=109 | s=158 | s=165 | s=225 | s=228 | s=291 | s=294 | s=295 | s=353 | s=366 | s=405 | s=409 | s=464 | s=470 | s=512 | s=519 | s=552 | s=557 | s=567 | s=595 | s=602 | s=634 | s=679 | s=748 | s=757 | s=894 | s=953 | s=959 | s=988 | s=1073 | s=1097 | s=1107 | s=1159 | s=1180 | s=1247 | s=1270 | s=1290 | s=1306 | s=1326 | s=1431 | s=1603 | s=1792 | s=1876;
label "o_21114" = s=6 | s=45 | s=58 | s=69 | s=74 | s=115 | s=130 | s=142 | s=190 | s=193 | s=259 | s=394 | s=435 | s=495 | s=542 | s=574 | s=587 | s=775 | s=1146 | s=1192 | s=1260 | s=1262 | s=1316 | s=1596 | s=1610;
label "o_30000" = s=442;
label "o_30001" = s=416 | s=1600;
label "o_30002" = s=1278;
label "o_30003" = s=1348;
label "o_30010" = s=520 | s=761 | s=1407 | s=1427 | s=1452;
label "o_30011" = s=544 | s=612 | s=667 | s=702 | s=743 | s=1141 | s=1422;
label "o_30012" = s=472 | s=521 | s=592 | s=686 | s=1268;
label "o_30013" = s=393 | s=1160 | s=1184 | s=1195 | s=1232 | s=1338 | s=1358;
label "o_30014" = s=1172;
label "o_30100" = s=1615 | s=1823 | s=1831;
label "o_30101" = s=389 | s=1605 | s=1749;
label "o_30102" = s=403 | s=551 | s=593 | s=600 | s=639 | s=1103 | s=1155 | s=1729 | s=1745 | s=1753 | s=1761;
label "o_30103" = s=429 | s=529 | s=573 | s=690 | s=1090;
label "o_30104" = s=86 | s=709;
label "o_30110" = s=445 | s=1462;
label "o_30111" = s=180 | s=302 | s=419 | s=721 | s=758 | s=1404 | s=1472 | s=1598 | s=1752;
label "o_30112" = s=63 | s=124 | s=145 | s=201 | s=215 | s=323 | s=374 | s=580 | s=765 | s=776 | s=952 | s=983 | s=1029 | s=1294 | s=1440 | s=1733 | s=1756;
label "o_30113" = s=96 | s=102 | s=166 | s=249 | s=284 | s=345 | s=514 | s=633 | s=747 | s=896 | s=936 | s=1284 | s=1286 | s=1304 | s=1760 | s=1870;
label "o_30114" = s=137 | s=728 | s=879 | s=885 | s=919 | s=1216 | s=1240 | s=1772 | s=1861 | s=1867;
label "o_31000" = s=477 | s=525 | s=1586;
label "o_31001" = s=281 | s=451 | s=480 | s=982 | s=1593 | s=1678;
label "o_31002" = s=313 | s=454 | s=505 | s=997 | s=1288 | s=1353;
label "o_31003" = s=428 | s=1318 | s=1680;
label "o_31004" = s=346 | s=402;
label "o_31010" = s=548 | s=650 | s=779 | s=1377 | s=1397 | s=1483 | s=1667 | s=1679;
label "o_31011" = s=163 | s=248 | s=570 | s=631 | s=648 | s=935 | s=967 | s=1347 | s=1367 | s=1387 | s=1685;
label "o_31012" = s=198 | s=213 | s=341 | s=386 | s=439 | s=491 | s=538 | s=629 | s=735 | s=771 | s=1067 | s=1363 | s=1547 | s=1563;
label "o_31013" = s=108 | s=178 | s=247 | s=299 | s=312 | s=356 | s=358 | s=465 | s=560 | s=753 | s=789 | s=1183 | s=1220 | s=1328 | s=1539 | s=1599;
label "o_31014" = s=14 | s=75 | s=329 | s=659 | s=807 | s=843 | s=878 | s=1398;
label "o_31100" = s=547 | s=1062 | s=1516 | s=1534 | s=1550 | s=1566 | s=1819;
label "o_31101" = s=99 | s=149 | s=221 | s=232 | s=234 | s=309 | s=404 | s=632 | s=670 | s=708 | s=1049 | s=1528 | s=1638 | s=1650 | s=1684 | s=1807 | s=1815 | s=1865;
label "o_31102" = s=184 | s=186 | s=204 | s=318 | s=338 | s=397 | s=433 | s=500 | s=613 | s=658 | s=727 | s=1007 | s=1036 | s=1114 | s=1140 | s=1620 | s=1632 | s=1765 | s=1787 | s=1843 | s=1862;
label "o_31103" = s=34 | s=151 | s=174 | s=220 | s=239 | s=242 | s=286 | s=303 | s=311 | s=368 | s=407 | s=423 | s=475 | s=796 | s=1201 | s=1312 | s=1857 | s=1859;
label "o_31104" = s=8 | s=16 | s=52 | s=71 | s=119 | s=135 | s=139 | s=209 | s=449 | s=814 | s=1302 | s=1804;
label "o_31110" = s=162 | s=469 | s=476 | s=511 | s=524 | s=597 | s=636 | s=712 | s=867 | s=901 | s=1070 | s=1075 | s=1227 | s=1249 | s=1369 | s=1372 | s=1493 | s=1542 | s=1560;
label "o_31111" = s=49 | s=59 | s=118 | s=127 | s=128 | s=188 | s=197 | s=211 | s=214 | s=278 | s=330 | s=486 | s=577 | s=618 | s=693 | s=695 | s=799 | s=813 | s=849 | s=873 | s=883 | s=905 | s=917 | s=918 | s=939 | s=941 | s=946 | s=950 | s=981 | s=1013 | s=1088 | s=1279 | s=1299 | s=1339 | s=1356 | s=1359 | s=1362 | s=1376 | s=1379 | s=1394 | s=1482 | s=1501 | s=1513 | s=1536;
label "o_31112" = s=22 | s=28 | s=31 | s=82 | s=89 | s=92 | s=106 | s=110 | s=148 | s=152 | s=153 | s=171 | s=173 | s=176 | s=223 | s=227 | s=240 | s=288 | s=305 | s=310 | s=352 | s=363 | s=406 | s=414 | s=460 | s=507 | s=522 | s=553 | s=638 | s=676 | s=714 | s=746 | s=752 | s=788 | s=795 | s=830 | s=854 | s=856 | s=888 | s=890 | s=924 | s=930 | s=934 | s=955 | s=962 | s=984 | s=986 | s=990 | s=992 | s=998 | s=1014 | s=1020 | s=1028 | s=1055 | s=1081 | s=1101 | s=1267 | s=1310 | s=1349 | s=1352 | s=1366 | s=1386 | s=1406 | s=1466 | s=1522 | s=1846 | s=1852;
label "o_31113" = s=7 | s=10 | s=47 | s=50 | s=51 | s=55 | s=61 | s=68 | s=70 | s=113 | s=116 | s=120 | s=123 | s=136 | s=141 | s=183 | s=185 | s=187 | s=192 | s=208 | s=256 | s=262 | s=272 | s=273 | s=322 | s=324 | s=334 | s=339 | s=380 | s=382 | s=396 | s=448 | s=530 | s=579 | s=614 | s=619 | s=622 | s=627 | s=660 | s=665 | s=741 | s=766 | s=770 | s=806 | s=838 | s=877 | s=913 | s=969 | s=975 | s=977 | s=1042 | s=1120 | s=1171 | s=1194 | s=1242 | s=1257 | s=1396 | s=1416 | s=1436 | s=1456 | s=1531 | s=1855;
label "o_31114" = s=2 | s=20 | s=23 | s=26 | s=29 | s=37 | s=39 | s=84 | s=95 | s=100 | s=101 | s=150 | s=155 | s=168 | s=222 | s=304 | s=422 | s=594 | s=607 | s=646 | s=820 | s=824 | s=1133 | s=1182 | s=1206 | s=1230 | s=1252 | s=1858;
label "o_40001" = s=626;
label "o_40002" = s=645;
label "o_40010" = s=496 | s=586 | s=1417;
label "o_40011" = s=566 | s=606 | s=683 | s=724;
label "o_40012" = s=336 | s=664 | s=705;
label "o_40013" = s=241 | s=306 | s=365 | s=1196 | s=1244;
label "o_40014" = s=207 | s=274;
label "o_40100" = s=1827 | s=1835;
label "o_40101" = s=361 | s=1179;
label "o_40102" = s=376 | s=1167;
label "o_40104" = s=121 | s=205 | s=850;
label "o_40110" = s=471 | s=707 | s=1839;
label "o_40111" = s=270 | s=332 | s=740 | s=1191 | s=1842;
label "o_40112" = s=236 | s=293 | s=559 | s=968 | s=1264;
label "o_40113" = s=131 | s=191 | s=252 | s=316 | s=437 | s=489 | s=537 | s=1254 | s=1274;
label "o_40114" = s=156 | s=172 | s=226 | s=411 | s=463 | s=868 | s=902 | s=1864;
label "o_41001" = s=1027 | s=1662;
label "o_41002" = s=1012 | s=1041 | s=1668;
label "o_41003" = s=1674;
label "o_41004" = s=375;
label "o_41010" = s=424 | s=669 | s=1673;
label "o_41011" = s=398 | s=590 | s=951;
label "o_41012" = s=233 | s=370 | s=413 | s=515 | s=610 | s=716 | s=1054 | s=1080 | s=1555;
label "o_41013" = s=15 | s=267 | s=697 | s=1208;
label "o_41014" = s=4 | s=40 | s=678 | s=825 | s=861;
label "o_41100" = s=417 | s=1558;
label "o_41101" = s=67 | s=199 | s=268 | s=277 | s=390 | s=395 | s=430 | s=485 | s=651 | s=689 | s=763 | s=1519 | s=1644 | s=1656;
label "o_41102" = s=32 | s=35 | s=164 | s=167 | s=347 | s=362 | s=367 | s=369 | s=456 | s=459 | s=1022 | s=1127 | s=1153 | s=1486 | s=1851;
label "o_41103" = s=12 | s=64 | s=66 | s=125 | s=202 | s=271 | s=333 | s=340 | s=1165 | s=1189 | s=1322 | s=1854;
label "o_41104" = s=5 | s=25 | s=90 | s=98 | s=104 | s=160 | s=170 | s=237 | s=292 | s=832;
label "o_41110" = s=443 | s=450 | s=688 | s=726 | s=884 | s=1215 | s=1259 | s=1552;
label "o_41111" = s=83 | s=93 | s=97 | s=244 | s=296 | s=300 | s=510 | s=555 | s=745 | s=781 | s=922 | s=966 | s=1106 | s=1132 | s=1203 | s=1269 | s=1492 | s=1504 | s=1510 | s=1544 | s=1845;
label "o_41112" = s=11 | s=60 | s=65 | s=73 | s=77 | s=117 | s=129 | s=132 | s=138 | s=140 | s=206 | s=210 | s=261 | s=264 | s=326 | s=482 | s=499 | s=533 | s=733 | s=777 | s=871 | s=907 | s=999 | s=1005 | s=1034 | s=1068 | s=1093 | s=1119 | s=1145 | s=1342 | s=1476 | s=1495 | s=1848;
label "o_41113" = s=3 | s=24 | s=30 | s=33 | s=36 | s=38 | s=42 | s=85 | s=87 | s=88 | s=94 | s=103 | s=105 | s=157 | s=175 | s=218 | s=230 | s=238 | s=351 | s=355 | s=474 | s=599 | s=641 | s=684 | s=722 | s=759 | s=784 | s=860 | s=1158 | s=1177 | s=1332 | s=1426 | s=1446;
label "o_41114" = s=1 | s=9 | s=13 | s=17 | s=53 | s=54 | s=56 | s=62 | s=72 | s=122 | s=133 | s=195 | s=203 | s=260 | s=384 | s=703 | s=802 | s=842 | s=1170 | s=1218;
label "o_minimum" = s=1 | s=2 | s=3 | s=4 | s=5 | s=6 | s=7 | s=8 | s=9 | s=10 | s=11 | s=12 | s=13 | s=14 | s=15 | s=16 | s=17 | s=18 | s=20 | s=21 | s=22 | s=23 | s=24 | s=25 | s=26 | s=27 | s=28 | s=29 | s=30 | s=31 | s=32 | s=33 | s=34 | s=35 | s=36 | s=37 | s=38 | s=39 | s=40 | s=42 | s=43 | s=45 | s=47 | s=48 | s=49 | s=50 | s=51 | s=52 | s=53 | s=54 | s=55 | s=56 | s=57 | s=58 | s=59 | s=60 | s=61 | s=62 | s=64 | s=65 | s=66 | s=67 | s=68 | s=69 | s=70 | s=71 | s=72 | s=73 | s=74 | s=75 | s=77 | s=79 | s=81 | s=82 | s=83 | s=84 | s=85 | s=87 | s=88 | s=89 | s=90 | s=91 | s=92 | s=93 | s=94 | s=95 | s=96 | s=97 | s=98 | s=99 | s=100 | s=101 | s=102 | s=103 | s=104 | s=105 | s=106 | s=107 | s=108 | s=109 | s=110 | s=112 | s=113 | s=115 | s=116 | s=117 | s=118 | s=119 | s=120 | s=122 | s=123 | s=125 | s=126 | s=127 | s=128 | s=129 | s=130 | s=131 | s=132 | s=133 | s=135 | s=136 | s=137 | s=138 | s=139 | s=140 | s=141 | s=142 | s=143 | s=144 | s=147 | s=148 | s=149 | s=150 | s=151 | s=152 | s=153 | s=155 | s=156 | s=157 | s=158 | s=160 | s=161 | s=162 | s=163 | s=164 | s=165 | s=166 | s=167 | s=168 | s=170 | s=171 | s=172 | s=173 | s=174 | s=175 | s=176 | s=177 | s=178 | s=179 | s=183 | s=184 | s=185 | s=186 | s=187 | s=188 | s=190 | s=191 | s=192 | s=193 | s=194 | s=195 | s=196 | s=197 | s=198 | s=199 | s=200 | s=202 | s=203 | s=204 | s=206 | s=207 | s=208 | s=209 | s=210 | s=211 | s=213 | s=214 | s=216 | s=217 | s=218 | s=220 | s=221 | s=222 | s=223 | s=225 | s=226 | s=227 | s=228 | s=229 | s=230 | s=231 | s=232 | s=233 | s=234 | s=235 | s=237 | s=238 | s=239 | s=240 | s=241 | s=242 | s=244 | s=245 | s=247 | s=248 | s=249 | s=251 | s=252 | s=256 | s=257 | s=259 | s=260 | s=261 | s=262 | s=263 | s=264 | s=265 | s=267 | s=268 | s=271 | s=272 | s=273 | s=274 | s=277 | s=278 | s=280 | s=281 | s=282 | s=284 | s=286 | s=288 | s=289 | s=291 | s=292 | s=294 | s=295 | s=296 | s=297 | s=299 | s=300 | s=303 | s=304 | s=305 | s=306 | s=309 | s=310 | s=311 | s=312 | s=313 | s=314 | s=316 | s=318 | s=320 | s=322 | s=324 | s=325 | s=326 | s=327 | s=329 | s=330 | s=333 | s=334 | s=335 | s=338 | s=339 | s=340 | s=341 | s=345 | s=346 | s=347 | s=349 | s=350 | s=351 | s=352 | s=353 | s=354 | s=355 | s=356 | s=358 | s=359 | s=360 | s=362 | s=363 | s=365 | s=366 | s=367 | s=368 | s=369 | s=370 | s=375 | s=378 | s=379 | s=380 | s=381 | s=382 | s=383 | s=384 | s=386 | s=387 | s=388 | s=390 | s=391 | s=393 | s=394 | s=395 | s=396 | s=397 | s=398 | s=402 | s=404 | s=405 | s=406 | s=407 | s=408 | s=409 | s=411 | s=413 | s=414 | s=415 | s=417 | s=420 | s=421 | s=422 | s=423 | s=424 | s=428 | s=430 | s=431 | s=432 | s=433 | s=434 | s=435 | s=437 | s=439 | s=440 | s=443 | s=444 | s=447 | s=448 | s=449 | s=450 | s=451 | s=454 | s=456 | s=457 | s=458 | s=459 | s=460 | s=461 | s=463 | s=464 | s=465 | s=466 | s=469 | s=470 | s=473 | s=474 | s=475 | s=476 | s=477 | s=478 | s=480 | s=482 | s=483 | s=485 | s=486 | s=487 | s=489 | s=490 | s=491 | s=495 | s=499 | s=500 | s=503 | s=505 | s=507 | s=508 | s=510 | s=511 | s=512 | s=514 | s=515 | s=519 | s=522 | s=524 | s=525 | s=526 | s=530 | s=531 | s=533 | s=535 | s=537 | s=538 | s=542 | s=545 | s=547 | s=548 | s=549 | s=552 | s=553 | s=555 | s=557 | s=560 | s=561 | s=562 | s=564 | s=567 | s=570 | s=574 | s=575 | s=577 | s=579 | s=581 | s=582 | s=583 | s=587 | s=590 | s=594 | s=595 | s=597 | s=598 | s=599 | s=601 | s=602 | s=603 | s=605 | s=607 | s=609 | s=610 | s=613 | s=614 | s=615 | s=618 | s=619 | s=621 | s=622 | s=623 | s=625 | s=627 | s=629 | s=631 | s=632 | s=633 | s=634 | s=636 | s=637 | s=638 | s=640 | s=641 | s=642 | s=644 | s=646 | s=648 | s=650 | s=651 | s=652 | s=653 | s=657 | s=658 | s=659 | s=660 | s=661 | s=663 | s=665 | s=669 | s=670 | s=672 | s=673 | s=674 | s=675 | s=676 | s=678 | s=679 | s=680 | s=682 | s=684 | s=688 | s=689 | s=692 | s=693 | s=695 | s=697 | s=698 | s=701 | s=703 | s=708 | s=710 | s=711 | s=712 | s=714 | s=716 | s=717 | s=718 | s=720 | s=722 | s=726 | s=727 | s=728 | s=729 | s=730 | s=733 | s=735 | s=736 | s=739 | s=741 | s=745 | s=746 | s=747 | s=748 | s=749 | s=751 | s=752 | s=753 | s=754 | s=755 | s=757 | s=759 | s=763 | s=764 | s=766 | s=770 | s=771 | s=772 | s=773 | s=775 | s=777 | s=779 | s=780 | s=781 | s=782 | s=784 | s=788 | s=789 | s=790 | s=791 | s=793 | s=795 | s=796 | s=799 | s=801 | s=802 | s=806 | s=807 | s=808 | s=811 | s=812 | s=813 | s=814 | s=817 | s=818 | s=819 | s=820 | s=824 | s=825 | s=826 | s=829 | s=830 | s=831 | s=832 | s=836 | s=838 | s=842 | s=843 | s=844 | s=847 | s=848 | s=849 | s=854 | s=856 | s=860 | s=861 | s=862 | s=866 | s=867 | s=868 | s=871 | s=873 | s=877 | s=878 | s=879 | s=882 | s=883 | s=884 | s=885 | s=886 | s=887 | s=888 | s=890 | s=893 | s=894 | s=895 | s=896 | s=899 | s=900 | s=901 | s=902 | s=903 | s=905 | s=906 | s=907 | s=910 | s=911 | s=912 | s=913 | s=916 | s=917 | s=918 | s=919 | s=920 | s=922 | s=923 | s=924 | s=925 | s=927 | s=928 | s=929 | s=930 | s=933 | s=934 | s=935 | s=936 | s=937 | s=939 | s=940 | s=941 | s=943 | s=945 | s=946 | s=950 | s=951 | s=953 | s=954 | s=955 | s=956 | s=957 | s=959 | s=961 | s=962 | s=966 | s=967 | s=969 | s=970 | s=971 | s=972 | s=973 | s=975 | s=976 | s=977 | s=980 | s=981 | s=982 | s=984 | s=985 | s=986 | s=987 | s=988 | s=990 | s=992 | s=995 | s=996 | s=997 | s=998 | s=999 | s=1000 | s=1001 | s=1003 | s=1005 | s=1007 | s=1010 | s=1012 | s=1013 | s=1014 | s=1015 | s=1016 | s=1018 | s=1019 | s=1020 | s=1022 | s=1023 | s=1027 | s=1028 | s=1031 | s=1033 | s=1034 | s=1036 | s=1037 | s=1041 | s=1042 | s=1045 | s=1047 | s=1048 | s=1049 | s=1054 | s=1055 | s=1058 | s=1060 | s=1061 | s=1062 | s=1067 | s=1068 | s=1070 | s=1071 | s=1073 | s=1074 | s=1075 | s=1080 | s=1081 | s=1084 | s=1086 | s=1087 | s=1088 | s=1093 | s=1094 | s=1097 | s=1099 | s=1100 | s=1101 | s=1106 | s=1107 | s=1110 | s=1113 | s=1114 | s=1119 | s=1120 | s=1123 | s=1126 | s=1127 | s=1132 | s=1133 | s=1139 | s=1140 | s=1145 | s=1146 | s=1147 | s=1149 | s=1152 | s=1153 | s=1156 | s=1157 | s=1158 | s=1159 | s=1160 | s=1165 | s=1168 | s=1170 | s=1171 | s=1172 | s=1176 | s=1177 | s=1180 | s=1182 | s=1183 | s=1184 | s=1188 | s=1189 | s=1192 | s=1194 | s=1195 | s=1196 | s=1201 | s=1202 | s=1203 | s=1204 | s=1206 | s=1207 | s=1208 | s=1214 | s=1215 | s=1216 | s=1218 | s=1219 | s=1220 | s=1224 | s=1226 | s=1227 | s=1228 | s=1230 | s=1231 | s=1232 | s=1236 | s=1238 | s=1240 | s=1242 | s=1243 | s=1244 | s=1246 | s=1247 | s=1249 | s=1250 | s=1252 | s=1253 | s=1254 | s=1257 | s=1259 | s=1260 | s=1262 | s=1265 | s=1266 | s=1267 | s=1269 | s=1270 | s=1272 | s=1273 | s=1274 | s=1275 | s=1276 | s=1277 | s=1279 | s=1280 | s=1284 | s=1285 | s=1286 | s=1287 | s=1288 | s=1289 | s=1290 | s=1295 | s=1296 | s=1297 | s=1299 | s=1300 | s=1302 | s=1304 | s=1305 | s=1306 | s=1309 | s=1310 | s=1312 | s=1314 | s=1315 | s=1316 | s=1318 | s=1320 | s=1321 | s=1322 | s=1325 | s=1326 | s=1328 | s=1329 | s=1331 | s=1332 | s=1334 | s=1336 | s=1338 | s=1339 | s=1340 | s=1341 | s=1342 | s=1344 | s=1346 | s=1347 | s=1349 | s=1352 | s=1353 | s=1356 | s=1358 | s=1359 | s=1362 | s=1363 | s=1364 | s=1366 | s=1367 | s=1368 | s=1369 | s=1372 | s=1374 | s=1375 | s=1376 | s=1377 | s=1378 | s=1379 | s=1380 | s=1384 | s=1385 | s=1386 | s=1387 | s=1388 | s=1389 | s=1390 | s=1394 | s=1395 | s=1396 | s=1397 | s=1398 | s=1400 | s=1401 | s=1405 | s=1406 | s=1408 | s=1410 | s=1411 | s=1415 | s=1416 | s=1418 | s=1420 | s=1421 | s=1425 | s=1426 | s=1429 | s=1431 | s=1435 | s=1436 | s=1441 | s=1445 | s=1446 | s=1451 | s=1455 | s=1456 | s=1461 | s=1465 | s=1466 | s=1471 | s=1476 | s=1481 | s=1482 | s=1483 | s=1485 | s=1486 | s=1491 | s=1492 | s=1493 | s=1494 | s=1495 | s=1500 | s=1501 | s=1503 | s=1504 | s=1506 | s=1508 | s=1509 | s=1510 | s=1511 | s=1512 | s=1513 | s=1516 | s=1518 | s=1519 | s=1521 | s=1522 | s=1526 | s=1527 | s=1528 | s=1529 | s=1531 | s=1534 | s=1536 | s=1539 | s=1542 | s=1544 | s=1547 | s=1550 | s=1552 | s=1555 | s=1558 | s=1560 | s=1563 | s=1566 | s=1573 | s=1575 | s=1582 | s=1584 | s=1586 | s=1587 | s=1589 | s=1592 | s=1593 | s=1594 | s=1596 | s=1599 | s=1603 | s=1604 | s=1606 | s=1610 | s=1616 | s=1620 | s=1622 | s=1628 | s=1632 | s=1638 | s=1640 | s=1644 | s=1650 | s=1656 | s=1662 | s=1667 | s=1668 | s=1673 | s=1674 | s=1678 | s=1679 | s=1680 | s=1684 | s=1685 | s=1691 | s=1695 | s=1699 | s=1703 | s=1719 | s=1731 | s=1732 | s=1735 | s=1739 | s=1751 | s=1755 | s=1760 | s=1764 | s=1765 | s=1766 | s=1768 | s=1770 | s=1772 | s=1774 | s=1776 | s=1778 | s=1780 | s=1782 | s=1784 | s=1785 | s=1786 | s=1787 | s=1788 | s=1790 | s=1792 | s=1793 | s=1794 | s=1798 | s=1802 | s=1804 | s=1806 | s=1807 | s=1815 | s=1819 | s=1830 | s=1838 | s=1843 | s=1845 | s=1846 | s=1848 | s=1849 | s=1851 | s=1852 | s=1854 | s=1855 | s=1857 | s=1858 | s=1859 | s=1861 | s=1862 | s=1864 | s=1865 | s=1867 | s=1870 | s=1873 | s=1874 | s=1876 | s=1877 | s=1879 | s=1881 | s=1882 | s=1883 | s=1885 | s=1887 | s=1888;
label "o_premium" = s=1 | s=2 | s=3 | s=4 | s=5 | s=6 | s=7 | s=9 | s=10 | s=11 | s=12 | s=13 | s=14 | s=15 | s=17 | s=18 | s=20 | s=21 | s=22 | s=23 | s=24 | s=25 | s=26 | s=27 | s=28 | s=29 | s=30 | s=31 | s=32 | s=33 | s=35 | s=36 | s=37 | s=38 | s=39 | s=40 | s=42 | s=43 | s=45 | s=47 | s=48 | s=49 | s=50 | s=51 | s=53 | s=54 | s=55 | s=56 | s=58 | s=59 | s=60 | s=61 | s=62 | s=64 | s=65 | s=66 | s=67 | s=68 | s=69 | s=70 | s=72 | s=73 | s=74 | s=75 | s=77 | s=79 | s=81 | s=82 | s=83 | s=84 | s=85 | s=87 | s=88 | s=89 | s=90 | s=91 | s=92 | s=93 | s=94 | s=95 | s=97 | s=98 | s=100 | s=101 | s=103 | s=104 | s=105 | s=106 | s=107 | s=109 | s=110 | s=112 | s=113 | s=115 | s=116 | s=117 | s=118 | s=120 | s=122 | s=123 | s=125 | s=127 | s=128 | s=129 | s=130 | s=132 | s=133 | s=136 | s=137 | s=138 | s=140 | s=141 | s=142 | s=144 | s=148 | s=150 | s=152 | s=153 | s=155 | s=156 | s=157 | s=158 | s=160 | s=164 | s=165 | s=167 | s=168 | s=170 | s=171 | s=172 | s=173 | s=175 | s=176 | s=177 | s=183 | s=185 | s=187 | s=188 | s=190 | s=192 | s=193 | s=195 | s=197 | s=199 | s=200 | s=202 | s=203 | s=206 | s=207 | s=208 | s=210 | s=211 | s=214 | s=218 | s=222 | s=223 | s=225 | s=226 | s=227 | s=228 | s=229 | s=230 | s=231 | s=233 | s=237 | s=238 | s=240 | s=244 | s=251 | s=256 | s=257 | s=259 | s=260 | s=261 | s=262 | s=264 | s=267 | s=268 | s=271 | s=272 | s=273 | s=274 | s=277 | s=278 | s=288 | s=291 | s=292 | s=294 | s=295 | s=296 | s=300 | s=304 | s=305 | s=310 | s=320 | s=322 | s=324 | s=325 | s=326 | s=329 | s=330 | s=333 | s=334 | s=335 | s=339 | s=340 | s=347 | s=351 | s=352 | s=353 | s=355 | s=362 | s=363 | s=366 | s=367 | s=369 | s=370 | s=375 | s=378 | s=379 | s=380 | s=381 | s=382 | s=383 | s=384 | s=387 | s=388 | s=390 | s=391 | s=394 | s=395 | s=396 | s=398 | s=405 | s=406 | s=409 | s=411 | s=413 | s=414 | s=417 | s=421 | s=422 | s=424 | s=430 | s=431 | s=432 | s=434 | s=435 | s=440 | s=443 | s=444 | s=447 | s=448 | s=450 | s=456 | s=459 | s=460 | s=461 | s=463 | s=464 | s=470 | s=474 | s=482 | s=483 | s=485 | s=486 | s=487 | s=490 | s=495 | s=499 | s=507 | s=510 | s=512 | s=515 | s=519 | s=522 | s=526 | s=530 | s=531 | s=533 | s=535 | s=542 | s=545 | s=552 | s=553 | s=555 | s=557 | s=562 | s=564 | s=567 | s=574 | s=575 | s=577 | s=579 | s=582 | s=583 | s=587 | s=590 | s=594 | s=595 | s=599 | s=602 | s=605 | s=607 | s=610 | s=614 | s=615 | s=618 | s=619 | s=621 | s=622 | s=623 | s=625 | s=627 | s=634 | s=638 | s=640 | s=641 | s=642 | s=644 | s=646 | s=651 | s=653 | s=657 | s=659 | s=660 | s=661 | s=665 | s=669 | s=676 | s=678 | s=679 | s=684 | s=688 | s=689 | s=692 | s=693 | s=695 | s=697 | s=698 | s=703 | s=714 | s=716 | s=720 | s=722 | s=726 | s=728 | s=729 | s=730 | s=733 | s=736 | s=741 | s=745 | s=746 | s=748 | s=752 | s=757 | s=759 | s=763 | s=764 | s=766 | s=770 | s=772 | s=773 | s=775 | s=777 | s=781 | s=784 | s=788 | s=790 | s=793 | s=795 | s=799 | s=801 | s=802 | s=806 | s=807 | s=808 | s=811 | s=812 | s=813 | s=820 | s=824 | s=825 | s=830 | s=832 | s=836 | s=838 | s=842 | s=843 | s=848 | s=849 | s=854 | s=856 | s=860 | s=861 | s=862 | s=868 | s=871 | s=873 | s=877 | s=878 | s=879 | s=883 | s=884 | s=885 | s=888 | s=890 | s=894 | s=895 | s=902 | s=903 | s=905 | s=907 | s=910 | s=911 | s=912 | s=913 | s=917 | s=918 | s=919 | s=922 | s=923 | s=924 | s=930 | s=934 | s=937 | s=939 | s=940 | s=941 | s=943 | s=946 | s=950 | s=951 | s=953 | s=955 | s=959 | s=962 | s=966 | s=969 | s=970 | s=971 | s=972 | s=973 | s=975 | s=977 | s=981 | s=984 | s=986 | s=988 | s=990 | s=992 | s=998 | s=999 | s=1000 | s=1001 | s=1005 | s=1012 | s=1013 | s=1014 | s=1020 | s=1022 | s=1027 | s=1028 | s=1031 | s=1033 | s=1034 | s=1041 | s=1042 | s=1047 | s=1048 | s=1054 | s=1055 | s=1058 | s=1068 | s=1073 | s=1080 | s=1081 | s=1084 | s=1086 | s=1088 | s=1093 | s=1094 | s=1097 | s=1101 | s=1106 | s=1107 | s=1110 | s=1119 | s=1120 | s=1127 | s=1132 | s=1133 | s=1145 | s=1146 | s=1153 | s=1158 | s=1159 | s=1165 | s=1168 | s=1170 | s=1171 | s=1172 | s=1177 | s=1180 | s=1182 | s=1189 | s=1192 | s=1194 | s=1203 | s=1204 | s=1206 | s=1208 | s=1214 | s=1215 | s=1216 | s=1218 | s=1219 | s=1228 | s=1230 | s=1231 | s=1240 | s=1242 | s=1247 | s=1250 | s=1252 | s=1257 | s=1259 | s=1260 | s=1262 | s=1267 | s=1269 | s=1270 | s=1272 | s=1277 | s=1279 | s=1280 | s=1290 | s=1295 | s=1297 | s=1299 | s=1300 | s=1306 | s=1310 | s=1315 | s=1316 | s=1320 | s=1322 | s=1326 | s=1332 | s=1334 | s=1336 | s=1339 | s=1342 | s=1349 | s=1352 | s=1356 | s=1359 | s=1362 | s=1366 | s=1374 | s=1375 | s=1376 | s=1379 | s=1386 | s=1388 | s=1390 | s=1394 | s=1395 | s=1396 | s=1398 | s=1400 | s=1401 | s=1406 | s=1408 | s=1410 | s=1415 | s=1416 | s=1421 | s=1425 | s=1426 | s=1431 | s=1435 | s=1436 | s=1441 | s=1445 | s=1446 | s=1455 | s=1456 | s=1461 | s=1466 | s=1476 | s=1481 | s=1482 | s=1486 | s=1491 | s=1492 | s=1494 | s=1495 | s=1500 | s=1501 | s=1504 | s=1510 | s=1512 | s=1513 | s=1518 | s=1519 | s=1522 | s=1531 | s=1536 | s=1544 | s=1552 | s=1555 | s=1558 | s=1582 | s=1589 | s=1594 | s=1596 | s=1603 | s=1610 | s=1616 | s=1622 | s=1644 | s=1656 | s=1662 | s=1668 | s=1673 | s=1674 | s=1699 | s=1768 | s=1770 | s=1772 | s=1776 | s=1778 | s=1780 | s=1782 | s=1784 | s=1786 | s=1792 | s=1794 | s=1802 | s=1845 | s=1846 | s=1848 | s=1849 | s=1851 | s=1852 | s=1854 | s=1855 | s=1858 | s=1861 | s=1864 | s=1867 | s=1874 | s=1876 | s=1888;
