From 098c9c1cb9b97e4e555810729ca7378d5179c4d5 Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Wed, 28 May 2025 15:01:15 +0100 Subject: [PATCH] example: iterative majority --- examples/iterated-majority/README.md | 58 ++++++++++ examples/iterated-majority/generate_models.py | 75 +++++++++++++ examples/iterated-majority/nfa-3.png | Bin 0 -> 72218 bytes examples/iterated-majority/run_benchmarks.py | 101 ++++++++++++++++++ 4 files changed, 234 insertions(+) create mode 100644 examples/iterated-majority/README.md create mode 100755 examples/iterated-majority/generate_models.py create mode 100644 examples/iterated-majority/nfa-3.png create mode 100755 examples/iterated-majority/run_benchmarks.py diff --git a/examples/iterated-majority/README.md b/examples/iterated-majority/README.md new file mode 100644 index 0000000..214abfb --- /dev/null +++ b/examples/iterated-majority/README.md @@ -0,0 +1,58 @@ + +# A family of uncontrollable NFAs + +Each automaton in this family is a chain of diamonds where after a split, controller can move a majority of the population into the target and moves the rest to the next round. The last round is a bad sink. + +![nfa for N=3](nfa-3.png) + +All of these models are **not** congrollable for arbitrary number of processes, but in the size-$n$ chain one can control $\le 2^n$ tokens. + +## Generate model files + +Starting in shepherd's main directory, run the python script to generate 10 models. + +```console +./generate_models.py 10 +nfa-10.dot nfa-2.dot nfa-4.dot nfa-6.dot nfa-8.dot generate_models.py +nfa-1.dot nfa-3.dot nfa-5.dot nfa-7.dot nfa-9.dot +``` + +## Solve them using prism + +This assumes the `schaeppert` binary is in your PATH, which can be done by running `cargo install --path .` + +```console +schaeppert -f dot nfa-3.dot iterate tmp/ +n=1 -> 1.000 +n=2 -> 1.000 +n=3 -> 1.000 +n=4 -> 1.000 +n=5 -> 1.000 +n=6 -> 1.000 +n=7 -> 1.000 +n=8 -> 0.949 +The value is less than 1.0, stopping the search. +The 8-fold power of this NFA is not controllable. +``` + + +## Solve them using shepherd + + +```console +shepherd -f dot nfa-2.dot + +Maximal winning strategy; +Answer: + NO (uncontrollable) + +States: ( 1a , 0a , T , 1 , 0b , 2 , 1b , 0 ) + Play action 'a' in the downward-closure of + ( ω , ω , ω , 1 , 1 , _ , _ , 1 ) + ( ω , ω , ω , _ , 1 , _ , _ , 3 ) + + +Play action 'b' in the downward-closure of + ( _ , 1 , ω , 1 , ω , _ , ω , 1 ) + ( _ , 1 , ω , _ , ω , _ , ω , 3 ) +``` diff --git a/examples/iterated-majority/generate_models.py b/examples/iterated-majority/generate_models.py new file mode 100755 index 0000000..3d6c1f3 --- /dev/null +++ b/examples/iterated-majority/generate_models.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 +""" +generate_models.py + +This script generates DOT files representing a family of NFA (nondeterministic finite automaton) models. +For each integer i from 1 to n (inclusive), it creates a file named 'nfa-i.dot' describing an NFA with a specific structure: +- States 0 through i, plus a target state T. +- Initial transitions from state 0 to each state 1..i+1 labeled 'a'. +- For each state j in 1..i+1, transitions from j to T labeled 'a{k}' for every k in 1..i+1 where k != j. + +Usage: + python generate_models.py +Where is a positive integer. + + +Note: All of these models are not congrollable for arbitrary number of processes, but the n-fold product of the size-m model is controllable by playing action "a", then "aj" if node "j" if none of the n processes reside in node j. +""" +import sys +def generate_model_file(n): + filename = f"nfa-{n}.dot" + with open(filename, "w") as f: + f.write('digraph NFA {\n') + f.write(' init [label=" ",shape=none,height=0,width=0];\n') + # States 0..N + for i in range(n): + f.write( + f' s{i} [label="{i}", shape=circle];\n' + f' s{i}a [label="{i}a", shape=circle];\n' + f' s{i}b [label="{i}b", shape=circle];\n' + ) + # Sink + f.write(f' s{n} [label="{n}", shape=circle];\n') + # Target state T + f.write(' T [label="T", shape=doublecircle];\n\n') + # Initial arrow + f.write(' init -> s0;\n') + # Transitions from 0 to 1..N + for i in range(n): + f.write( + f' s{i} -> s{i}a [label="a"];\n' + f' s{i} -> s{i}b [label="a"];\n' + f' s{i} -> s{i}a [label="b"];\n' + f' s{i} -> s{i}b [label="b"];\n' + + f' s{i}a -> T [label="a"];\n' + f' s{i}a -> s{i+1} [label="b"];\n' + f' s{i}b -> T [label="b"];\n' + f' s{i}b -> s{i+1} [label="a"];\n' + ) + + # Good and bad sink + f.write( + ' T -> T [label="a"];\n' + ' T -> T [label="b"];\n' + f' s{n} -> s{n} [label="a"];\n' + f' s{n} -> s{n} [label="b"];\n' + ) + f.write('}\n') + +def main(): + if len(sys.argv) != 2: + print("Usage: python generate_models.py ") + sys.exit(1) + try: + n = int(sys.argv[1]) + if n < 1: + raise ValueError + except ValueError: + print("n must be a positive integer") + sys.exit(1) + for i in range(1, n + 1): + generate_model_file(i) + +if __name__ == "__main__": + main() diff --git a/examples/iterated-majority/nfa-3.png b/examples/iterated-majority/nfa-3.png new file mode 100644 index 0000000000000000000000000000000000000000..dd5e21a9a0fbc58e6bc662970ea65fe9b16fd1f3 GIT binary patch literal 72218 zcmdRWi9gm|_w`lEOcFv$lu}d(p$wstO2`lyGh|4H2Fer}l37V4Qv*|_Zy|0f9-8!Fr`CIWd`f}VO*Kv;r`}Ysga+)#vuqf876sDIuuf@Ny zt@EYg^I_S=#*F_+R+nN?qzzZ>QK02hrvLx^FSvcXJXbb*czC!)HCmAuAugXh?a(iMp~;S)gVQPM)7u& zhOTaPTaH=clP5C`e}jU8OziFVJx%A{h&8#b86)M$zkB!Y&V|C)uVtQ`j9%@fu(dj! zdmXn9zmK3m&e@>WtaE(>^-=cUhZ-IoeE#A^gqe0QHIvYK#d~+}+@arbD&|jXqQHq0 zC+PjC6R_ffS#%qAG)uiqe)7bx_U_K#>Kc8AD^z`0QY>w3?)>@l$L8Cb)vKDCnoQ20 zFF$cAnDXzF9>&KT=OqewDNqg`JctiUA|I5uBA1t(l;j;Mzx<&34mZueCwiN0_@?*Q z_cta%hqblYKgP)_)!*MUzxPCR<8xL%<$3p|$!ZpQUv&))uZIset)-$Np`dDC?n9TF zndx&@_z9mt2nm{dI;N(4m%hLDy?2l8%C8PC#YC2cg@ppQ`Kg1(A=}1}&5~d1YkYi+ zcHO$_`QJm1Kbi#0EiH>LuULMFDQj=%{`Kn@r-%vVqMhA@XlPhaP*D2yE7$$|_lKL)Ht6Ts_(nvqZr`yZ$-b+&roO(S!hcHwpa-G z2r?rCS~7GiT3XmYJUmc6J^E#G^jV1$2P5TE^6?FB^8-;X6WyzxoOg-)yqRRsjd=9A=`Y4P)}MD=8EcOmciMjC>Q%>y?!(&!1bP<7ONQR? zbbcZ+`Rh(#U}MUOjZ)Imd|S8P9CxyLd3980ZgFv&sOb9dZ=CUi*B?K{+fU7YckVL9 zx2UM89UX1Wn&12M==mH@H8nN$GiQ`eo@DGAsM+-W@>ZW3T{SgkkCng9Zi{2D=r=Kz z$_v%mwLM>zlanLmIwOo9+iWP!qS!xD&FlHjk7-j_TpTlkvAF*FvsF~o3c?(oR;v!{ zqB6{{53Fp_R#wwGjeRS4Y^W znYf#~Jt&t(by&qSm1)D{FAp^&daf+TzRW|Eid0RMto(h}KJ!t2g$EhzY_28K&cBqK z{{A%NVCz0Ja%_E)^cb0>=E$W>dm|zux<^LZyYt_j7gc*C<9mP4xg>0Ci`;&3aUWmb zwMma3Yn(mX)?G{~MX0a#q99PZlVvRwaI(V#`}@sBsy=0%dqw>!GA=Hpyj<}?Oib%s zVL$+#GXHwyqc8YH1!H60qeqWo`v(8-FE%%8S=rc>x3v|N*}Zj}XDyYNZRcQrZA25cN0ipP%m-_1|&3>Vz9Cu{OI-q2>zvE{cZg?UMQTQ}?2xlnf0Y z;irB{m|Ix1%*_XG+?PI9z4p|p53l?*%#_L7G1%GJv2EOVx#@mf+?LGD%!%$Ys(X=< z+KWM=e#yz(Us`{r-mzmx>>nBj*MY~3B%?Z&O+OEckLSg*J52T0+I;Kl?G3womr7n< zo_5XZhK2f%A9e2(CKM3J5zb&{W>(}fspur1kZAcajtR9w*r0#~FH2dz9@SgFuS9uq zW^D4qfi8!p(~*DvT=6}drDpW+YfLX)LjHOGbR#Oe2j!`)p2=k%`<24^9|My@0_f0UgZ2;j=I^7C83p)o(-9thH;_D4?hzU%Ex{>k{Zz7$fH{ z<9+LvU`^JhJPZXRv{y==j6Qo-~ngx3D=A-&y4%t zj2GW3DUsj#IY?-ezETVe|NaB^o$r?Be>=|n)SH`|>mG{tyr0=2d1Y9gEZs;;#;4ZS z!9q>zyE{)GH8k>gtNx+T%9z zh^3$Hc?<`gf4z(MT&`70kvO5Eaud%?5>=v-|CAxKJz17mmp{Yni;9Xw&cCBAc>S7R zKwvGhhx<^SeT5%W#cBD!KGK&5w+afXgtW8@OG|U15)6NN#;cR1U+FAelvId(%*4+T zm~-j7jIiNrHcLxODbM9Y1_lN;?n_BW0>iMc$M5b)EGXbS^HeR;G|!$?U_K?k1bmB> z%S3{CTI0GF|G#5&d`wfrjoVOCxuW(NS2d-a$T2Bfotl=`Quqk9RO#3;ns~P;)eJsW7(y#MkgO4f7Pz@`L|fM1s2U}taXmWyP= z;p+d3q`KJS&-(xY|NHlEv-$aXrymFQ@4x%u(ZMKdTiaZ~P7x#<4p!E3r^}aZzaQ1p z;|dH2F#SFB@d65t#cHpc*Iiw6aq^3&IgvrCLN?dO9I$WLBIj09sjDHWJB$deIXEyh zWL9@?7cB!r1yE+qeEa*n$-xhsgpG@No~k`6|GPNL$3pw*t*i4{ef=ctEXmF>;?}DZ z)o-H&6y2Dn58WcGsH#fOx?zKcfk6~z-6-6e@3iB z8(UCw?)&Sj43CcnD;_^ihvi*!?AWnRo5??aeEj^V^XQhLqOR^noOEAg4Zy_4H_rA2g@t_L;%vZ=M|5;JUcN+yxNzf!%+H@cyMO)+0=iV% z%2G3TZg)@yDWGYMsKXEP^Cd4|y=s9lDr%kTtz_82Mz5!?9@g=V1o#Ge--~#<>0jsQ z3=eVAxVly&? z?(Z`W@nzV^FDF;r`B!KYIm;>{RnHOgnZ_ksfU7E_j6G_dk5dTJKdYx_imrmm<^oc{ z+@H^<3GfpKfNZT6t?C{d3m*OQtPff0s*KL@M&S1_Pt-HB-gg0Q1&-TRQ&F++;M{V^ z3IF!Wp2m#v^V8Gz4x8(4qQrV*AsKn)c&bBr zkDWcsSrxpg+W9yuii#5OR?pyIYj-}j*W0whujRTG9R)pAj^~O8_C<1z{wNn3hbb>W zRKLJL1_Ch(3Zxi0MQ)Bqq|*WQBilHI# zTwkb&ghVAk86RtaRK|(Me-Bdk;e+qfr#lG%=Hj9|bLLF(i3nB}777Cc!=GQ@ALdH> zD)Jo--4guPb+&cXg^7vj=eJku=;-M1Y4ZR3kX5^dh2NEWQB97t2)%pv4mH(hJR%vP z){EzjHImSpoSv@42RNW=-PqiPgFq@bAjDC9eeUX(UDOC?IT6G+=fP{jVq#(rgYUVn z41e+(kFa6m;tJTf�z<&?R2Z-Ne#T=h>#u+8q0g7&mO#@IFQ&u%eEQ24|g@rHa$C zAvOR(zlMh9i%ke$@tQSjN*f#3Ka#oHTV&^@a5G@T&hsnFf2WJ>6SA{IP_MV~^CunV z`|o0A>g7_q&ipLH0yjQA%?p&9k(9*m;yuLng+^KVyloV%5N(!g!jhF8io?pzj)JzH{pqm5lSRAUsG-N(pK*Nd;(C^=@4_ch%9+D^pN!XBc&73ADCybpjdl*_$U3OS z9ST4%$h^C6BLX3~IYQtBK;*41kHz3|O&hzeVs|SPmP3aQ^|wBai!*wA!R9Y%U`R(T zq?6g5Am)MAxQP~z#8k4fd=Q;TV7}eADMPiawbaz-(er}|a2or96N$p4avE9S9Lbc} zZjcDA6Xh<-X!EUo3=9qVI0Dyi*g)l_Q0gq5=QL2q-uCq?A0OYU{QP{Uu{TLctL@rf zmU*vbm;gu>FL;ZHNk1srQeqb`W)DT=Ir#Q zV6OdsxevQ@FMO=>qM`|ljI2EF>W1)1UcWv-`Rq%p^*ERAq=2T|JcnFZP$lL-7|icYQ6qbonJFAy@@Hl* zx<=%Tf&QwOC@Q2oNAIF2%yC)$(Gpp-+e=gR`#ASoGNO=>U&T*Q%gV~We;`V=Q!TbT zg&M~Wn8FNu5WAFc`jHGfP%{cdk@-1PJEY{D^B<8{H+6(&k|$A7K6Z>G>ba4OXLI;C zw7lUDA2Mv*xRLw?0=KB8cWB5TM4i)AoFY=bshQasyUIdr*ZHq6EJVb`m9Jd6a%=EP zgak4QcL2aEP@~^x0f_-V&|lzHm}0)&79u>#*W8^KM)zZVdJy!2d-qaPhDSz{j7vO3 z#Kd}&-Sq&hlh+Fh2~~i+i5xsN?8!h&TY7U9m5GT-sq-$%a-pdE@FzaBHxdO|j(t^$ zsj0Lm^}PvV^Z$MmC{@YSG|^y3Mqd-^3d{QSd|!TubzVTx5fl{cHup#dL@YygDl04F z(b{1=<<1n&!oOkt`t=|(e9(cLKRhdZ6t#t)pFiyWeQF@MKcipP0kPk@f1e|?WjP+Z zo0^ef_U`t2)YBmI#gr3K&)pZV9r9S>%+k;E#-5|^-5wRwo^MAQYa~OH{+jTJv1!@( z&dyG<*BTlcs{okNKCa`Dy4l@r(%;`tVCTf_tUt2W$>MW{pCWOd6qJ?MP&4zKwflx- zE^1N7_8>ai6fuGZ=iNH_CCY^h7iu}Bx=^}NYMJn$wfUbusSE49SOaovuK(`oiG^uf zmm4>F{dqmY&KV-ZNjdhe0o)S!HsUJx_U&72aUhz9w2#Hh3%1Hfj+o-eaUQtD!@q4? zV}|a&SUGq79bFk}oP5e@78fq;$LT6BFHg4{|NiCxHYGKG42=aN<=m@Fj}D#4)BtV) zEEGO;C|0xzY-Kek#nQr}Qkg&8Tpj=pL|e4NRuj}Or?fr$_Jsmn<^bp&&zI! z1dtWAX->8I7W?Q?BA6Z&q3ie0K1RhW2jN3S&6t|+{%5#RU1Po^eg}>O&Y+j59~BLA zO^PIr3nQ0Ua{HMROw#dNwrpwf`;d-GklkK#?xmF%a%c}&Q#6hjsfrI*G|JK_-s?ck zPsIM_b-u{S5nWzhvniu)*AuNj zKOscs?e*KZugEPA<-d#JNZY}i4x9%? z-6FR*8^&aesG4Xz#(SK}ca?&sW<+y74%6zJ20J%sfs9Voc+A4Wax*C@iTcrLtmD~p z=e9{o=Icv=J4-}7w9K43d2-FxE_~JUimoE9b=c0+aS2NP%q{uazDKmQ?wQX~Q9^j6 z`RD8J?E^(dvu?|~ZA5u zXlQ77UtaEg^+%I$T575YJ^}e`$E<$kdC~o%qNafydu%4=4_z5%Iisy@f&86`!p2DX zmS?+hw4-o;ZhpRHRaF&QJJR^*7#Ijw+v`0RddbSer`k|cLu>3l&5m&1Ij!g6A%`~S zHbBLLhYu@CO9`j|`@M#8WwezEs}N=T_RN!$WuP9z!@{`{WC0O3xy8M4 z9uGl~Ich~-L@7+_|1&)u9u-yX%r!oZ-j8IhL`##bJ;uhy{R0CME+b>W`aPgcTH;(Z zwf=pB1)V>#IEZ(f{f~ABUK?vK`}(!8Oz8xc^cbWV5K+?UC$9nOYdF=hGOt>-ic|Ew zavs;&$N-#vTW za!*9$xl#3|O`DXowId0k>dMT_OwUC&U>G&$^_3sx&bwk!J#GPNeX?ls>3qa$me)4H5;dv^p&QmqmkGBKBwCy9ppE*m#@X2!2gy0#+Quebu#9pOI*_%vA0wCd z&z~1j9(#ci2&N#d(7xh1#ld|BEzNRfjCeOBe&8+ArM!Rto^5%4`4!|0!ZOB6U;gy^ zsx2gz#|a4(bf*#Hbj@yi2@S^1z48P-lH81Znuu5pI=blxf`Z-RB)wO3~#?(_xjE54~Nc+V|9#$zI*wS4)&zJ2>h z1n%FTTa{m5U*GfNN3C5MlQLA6H`9mZ|K|k|ECh2$KsIE8n!37jbkYMP z2^RVn#6cv=i7cf9Q^ii|+S-)>0iu^Wq@ri)pFS&D<~FMe3YQrgcXhJuEV>@yjxQB) z>Q{+wX=A}Bh_43PB&{QIT1r(px?J-u%qz>bdZ$h?{au)@xWg`F-oCR7+BUw{cdy}V ztv5EVU3bqRyZROv%iZ*h6Fl>dPvB-Jdc{Vl=!!@N1e}l2sA_BH=~Spf4k5Z9x+`$O zQ1XF}_}SRl6i%OBhbZ*Q&fbeCH!(F`b@?)($aqRu{^kj@(VLo^`+#83-6Uh33I30T zo15O&*0z6WNNGFk+u6FqN=j7m?lW9yS_J4ck3jBG+1B*TSpH|{+f4xU5xl#+6x917 zl^~F*#Y%Z0tHvI5W(KLbdg7x-kFoEc8XJ51Y>9ItIXqg#bTumJWW_r9o1*APw-!3F1XdDV@Y;B1Fe)Ar zQQNm~eW0_BqD?imwhqA3zs+^8;*2|V-J9gM9XqIz?F*a+=x=(qM%IA2Lo#?@@|554 z@@1k&3w$=e*io<^KXW@IqzYu?DhlCO6BGGhR7l9k2t-><&V}d7-ve=S?l@NTkhiY< zXj+R7$-&vVI^poGIoB1h^@`jnyUsijNmQ@V($@Z}YwTXhyyZ|0DL9npKn}Uao_`}j z`rWx(eC=09t=~G{hS=EH2k2*HZ~QUAlUm}rVqZQRhGIgMiQdc?)a`5aaKIXoqLSAdFC%)r+^fHp+{eaYXMOiw#l`Q9YmS(M=pipkwibk*mXT2d3VS(N zb%F71f-le>@5gFi10AzB=CP@O;ypbiMQ{KYLB_j9Y3{>Am@6iRRRT@{@sZa6NpU|c z3_MPrBpT}{iHT+4&p&;7l1?fX+{!QV%yQ6Qq(BNzYAAu-`$>eAP7>RrNq+{x;fzj zK_<9Gow0{H;e{&0vw1VL(;8>#0_X89ASXm^TZJ=?-o{`~BuFU%biWeQY<%GM{DFE5Pl14P^PXIsK_j%fuoF~@-Q?Mqp~i4fL* zNxQtftjfzsnLvtuj4arxWJW4!cvF++63!CXCi|KXM}5s9Q=%cwG$>@{4_Ep1*Z%u! zc6f8<@FN4AuY^gdf+$xFu{Ho%LWcJ=7K8OGnp&LwNvOjUhIdX9Q2{ll9KqM$ZV%i5 z&zV2ElgG%$PGjfpBPWoO4sRFlRk{1Wq*;=be~yijjE@!>vGE?9#o?_i-H>3MM)!lf zhlH+j;sgkT&Hb&<4iTG7TkeH*5GY1oWFG)stE>lm8b3DmpO29L4E`bIz99bM#f$#d zA)M)+U%xtsy;o75s6D!aW|(jH?sT>4#tu~c2z*3`&8n&qR)E_&`~g8|AhvVPYH+BHF^eD@=-?#$b$wS0&r|l;IK+ZN9XJd z^MK}Jw8wMMOC2CPsV#VH#CH+a5$Esjbz=$(JNsJD$`Ic#HyIf=WE2JQNVB2_AAR(T zU;N5yX2sh-+1c4e(Kmw-l2dEn5TN|Nwe^0U^=Cg=Ry1GyMW(W(v>~uE#^UeZt)PgY zfmB=YjAz;;`Hu_ zvfhUc(#+brkCNlC6s05a?T^(*B4`;!L6Zqav(M=F|{ zSkVlDj}aStidJRUu3dyg-Z{2wdah|>^+8iWI1Pz)7yb@TuTeVO^YA(52>j7i(icKzxq+4m!m;i~L2 z@B+k813v-lA#M>^N z1X6zS(bE^z0bUv490~=o12jiyUpDfr-$)&RFj8Gd?-TtQ%{kx^VTOAYAA?Tbsgr*!ve_f2Do z1~cU-K%a+U3w>(0tc%rnHgvVS)T`$G`*%Qa;aGYAa!M(PJkYI7#FXT^M@B}*BnTdm z0v%5)Lbd}_bECr%n6ke7 z9vL4GMc|k~UDf>TD^exp{xk38OSV$^m2>G#ubmL$4u5rD0+&JSc7(Lr*4CzyzrV`i zSBErmP+4cE(MSP|cxiUpXKX?41?MhMe)+rEluv)sHf$J$OgVuboj5mva9hf!L2q8Y z@gh|cC^I1?MSIlu-akT|09`P54egs?D!q8|;sk7i-Kb#^V_?aS03zySp4I5nE=Rp~ zoa{YPTXKYdy~q5(MoQ_*@~nKr2vz?EW}r^NUAqn=b?+Q&87R{Ep1={H-0~z3&3|NV zy(bF7Rhf9`gST0UgozGE+V(Vl7!uj7sHlx-*?f`vd*N4-0{>aO`0L=wXt5(N#?hxb zg082m1cf8=Hi0iC4h-Ty+;rfQ36!H)xwJJDln!qw;bh;C@k=?CASLV!&21ehnn56< z%vXeLJ_zoJ2K_CxZFm!m#A08%%{%=W`?e8z`=Wy#(X{F1mvPuelMgWx#A2{T z-s8RX8|{5B|GLh6S}87_?$XnHTU5ldWeW~3n-w5hzkpN~C)(iWj(tZ@K9Y(2oWGI< zMd|hH*R)Jbm1t?DZC^dEn?#tu(RC`2nfF}?^Xvs3ZIFRY~#*I zScC+eXh_|uzio`_MnDBUfA#9v-5saQJEM?}(SAt1*_Cx0>Jb&pf&ehh3!Fp+Al?ti zJ@b2&206`$*pYW2$D+2Pg6cnpue&Ea-K4HhZHLM2+^91Th5SktR0W6W5$%R}PhD{| z8eqmsA>|D;8KZoXt{y&x(|iBco-;Dq0%2LyV`)xi^D)9P5>5=vA*2H!K(RdMaU&Q= zY6m=&B4OU)B(4v~7l$o2vazk{j^Fra#G3%PL>S14e*g(0_?lZ0_#h${z+N@bJ`NU; z7{wnQbgs)Y)-wz0!N-(>ZB2aoRQIXbF4QglmBp@=2_UJXuG15M{rEJ+C*zXM$xxMu zLiYT|w2j)3e(yI#Z`i$iKA;g^H&i#dBC|#Vukt~JK&1fJFz|+_0r|ePxtWb{?`W!o zXO{`@hsf;3f4xI>8R(S%0^bu(Alwpu0CmmN4mUn}u~_6cc$F0g- z>>M0PpkN)YUDH`uTo)wDxaANhqN)-BZX=uWG80@bkpXF$nXAAOUC&C9<20L?nkpwI z5)`EcwO5Lm1`yl^B!BVii?uY&Jf&EIxxG&hlko;n0H%1*BKQ`FsREd&^4_j9Qjh3# zjUcQC0}a99o?!ahK@?*R3xf~siJR#Slp9dhC!oF)`_fo@9-4}dllpQm)6VL;)6Hgf?l7{0fFdVQqgj&D3IhU9AU2$-(j3M9S{rqxs_lInet(zBn z%oK^P0{T2EC9#Ez8NYa$xYxLtaoxIgFtUdSE(%;B`xFHSEO@!w%KY!Ds*=!Kx<&ml z0%#*78n{oK6HqB1oR3Sqc3+f);@H#OeG}VUW5Hj#KzK_mSWj=SH~z?B^7eiLQ@={s zwX@+^5T_Vy3gOYwuuhHNi;1Df_YD8|!6z(y()8AgX-@d)HqT+FTQ~Vu% zsOHFQJ~+F~JW{1!-|YLxVPS2QE?yL-l){w;>7=hPDMn!X_5@Jj5duda!bak`@}6-&hKHYvnpHiAHdV!G2FmOG=g)W3GBR=z zJ}&^RI!9cW=0q<$J70*2iTR0haqq}RT|&*9*VWavK^`TXNxa9xuKL>Ap1e5ti=IQ3 zB3&fRqhdy$TDE;S+9yw(2qc{{prF>`$?dE;+8H{cSRYF}yAQDX3w~(_*7*95*buia zhXVrb$QSb#cEXitJ2;5gwxqL@|Nn-b0rZH|SP5EhyN-fzH25M&yx?%83ulaZ;gm4J zb6$iuK(lPZ9t&y)yma!&5np2X_+H?s^yF$}R8%hPy}1Z-F~Gt6^Of{)T<)&li}Ygs z9u!9#*y;!A>AOce-yZz-*7eo<6{n2>%0D65zi(=a0HdA*7Wg^pbM#ED@AKy(r0FGo zePw=)tPp9Zep(XYq-h58@)HFoGdbBOHwG2J+M)~A|6HMy!2bRF$zg%W!MD!W&DtiD=Ya!fv2=SfGizh%`&Qs8?;^!Sb%GuFmE4Tne8a`xXWMrWKB;8FYNl zk;7&3S`_|3y5x-j%0CYRRmyEn1UQWtnu4~-lD>Et3!`G%sUvWb#z@-HgD4=5#aq-&y=MCBZ_tH=t<%6Mgk!}I z8$zu905zY!eDN0CI3ORUX_$Ior3cLqq zCQ!-Ca3m%mT3T6IIq2)|F=U@=6yozSh9M#~HT5Q5GEUwz1hWf7azWn%g1HJP4s#B~ zz6y2o_;PzoV`JGdUiURvQ6fx$7$Y-YFNIiWMQoY{LHa89Je_KLeN{+q@#lWwv(FWF z1TuhvD*y0-3DnV5IUPZ^Bvc~^Lc|t1l-EKH%su7hboHt)Ob&#X(|ZVigVneEJ;n2b zoA3!YbFUTVV{8Wcj2Wn~v#+o0g3YW3r4cUjsuvdZbHj0{HT_C|;6H)!n^0V9 zrR?7%k}?Cchza?_Em>gqoGd_d?g;W z*YFNN0~zljws*X+D#Uj1`DNek8k27}0b>^oZiR7^1@!J^4_Q3H%pn3yR*p9cX=(DRuDR8BD~P3vJ)7oGt$V)$$#>)BdUE2;>Q%1qbkn z&>~FdCVIri&ul@R4Tm)!&0FEj38X%nUZg(QbHfe%?xka-ft-9~t-IFp;6R9t6*d13 zz&D(|3Qzvl-bD<6Y44Xi1PEF~!w>EPtgCNUR#wNt%bXl9l=qYV_sM)2WL?4xfN1l_ z|Gi)6C3+_?d%xUE$SyTBNj55Je535m{;ysgVCIz*zMEfPS0@5L50T=r%F{8cw7Jkr zLh({8hyp%)c)-5yDlDw%|Iplr!p-8)ehG~!Cc6A!n97Jq$yx(;D1wOJo8QVuGBpl?KJc|$`;Za#ZBej9#0!h8Pjw*elY z+^J*Oz_kmeRM^g9ec_7Z^JCt82amB;MuuBbQZn{sMh!8BLR+f6Y83#E`sgnZsJDZI z2Q2W|c+E>)#ldJiBvK!NX260{K*C5l|KfRlb+k&u_s%J3K!6@j?!?m&c62XBKGM_E zF@M&dMNRO{=;*dXhl)Dw;BO-&n9IVSU1&to_ncnfBi)IcTT#aX=DU)^8R+P|kX|9$ zxMUoLAO|-VtZK?{Lp))kg&IzX6G&TEMw$cq=-K08Xa%?hLBSWbOu)rERaI3O{mMqe zG})o!Vn0YvuU7pQk~Thy3~C}jPr}Yro2ppZiWUVTf8kq3M1;yVj`i!kK$!YIP(5E0 z#s`us#fu-sNR)K}f*t^i@SAQ?-e5Z);{fGt z(Z7MYBm^vE1H##1dV)(gbq-V~&Nv^_Hk{I>IY(bk&Gg=Z0beAS5@-Hm^#7OwAa9NQ zrv&gkpp|$&7t3@0e3F5Y-@o;FjnPk|Vz)H)&pNKxuS2BX0LCMG@;68j=x}6`3O?O; z;62%U(~oJ82YdPQPu5TRNutW5U06*)#oYaI ziY*R>bok>*`SPv+G*;OoGzge}l9Gat>+$zpR- zd<|nQ-lZF)BIPEOyvLp^%fn464DcA!0hY!IX@84_1en=x7KJ z9ebqb^1dywNMLfAbZ9VJfD9-@6C55Nzi+l38YuBIA};tavI&F4vGLBgju5_4@U^}{ z`d>#h5V)GapfVAY70$>#*AI7+oyR-j-$A|+8}la-KIq0BQh)wj zeX3aD$`x_QX~9U=8vw4!Z0o!8IUTlFuwFnh@Kl)E+lPYSf;UA3g8z&)0e0Ss zjASPsU*O!@x0Xj5A&QY%!NJeY$dpYrgmwm1)uMCcb8BlAw%PRJMMgAWV9k4wpb4=9 zS&?s+n-~|7zbYCUmby98`Yz$j<6HG1{r9u*VAZ{Iz+z_+m?8pyTPMB&S zgsU-rk8^VJ^HGs7RRnI4oORih?HIzcsOKP54Vg6oQijG3o_SS5!-gJ-cWGyyinvUe zFm9G%19Sl-x<0h*=jW&SExpqVg75v~!F35>@QF&Jdg6pdD;YTmR)Nk$F#%wXumh1= zf#lnmc4jBa78i!6O@fYRb9NqxT&qji2k4iCEl2Bm3xlQLKYlluLAgkQ5m8ZF#qBm& zT@8>B^RGKraI#glY35zK1*?_$Icz7z1U^H!uzl49*Gzo8(mBP-!QlrC1GCdQIM#ge zE=W!jP%WIZnPj??Q$5_pQo5i)C!;HaM|rrPEsP7e%4#5*`IwZ83T4QRvgLo|*znK&aFGZHe< z=@@VJ%M(KO3mZ_9k0Re9eC5$+h3_vE;Q(UBOLuACMDb?4CBeLC4gkgCdrGXAf9a9Q4bzv&15va*= zyi+#%%nu$IA_Yp1ANBrZY!K<^P=`~Ee8POuQQDu`25 zkt1|}@fSQ%j?;kZ&yKr!pd+Ilw-flM;0^2%Y*OBV4Lto z+lfK*v@*N)uU{KCoR~H-F}VpTp{DN%{q_K^U??K< ztnii^&tCg>;E0|gTV3&fAJ!z{{Yk>LYP4p?)hC%M+L)?jt|?iX@A_I>9BC-wYaVc~ zDelsDxf1!M5uwOmV{xt@-%i7ZyJg*_S+~ydKF87TLvE6Z>MC#j#nhXx=Ht`fb-wSc!L3j8)Rnfjas&hf002`x9n*B&s$40sb0@jX!qd~cs6a^1JueN( z%S)jqQ%Zqw32_dbZY^X?=!vjW_?>?NfF@ zq@Y0i-S~LeX%w|OqCRU~c5u?<^TAM%ULLLeMn&uwE#jASQ|5 zum92+Zg}tzv&p^c)K^EE6MGd@j@<3KJg1M!!)b=naTI3S9VZ{$oE`6~XBWb|z>-bo z#>vDU-mbnSE|VB0P%nifEU%lODu+hWrdg@(W;Q+_L~hhrd+V-6cx-GC1~~bEm_b%4 zLyM^I(9zRy6x@U<_z`Iq%|@I%?{+|0Q=%=mFOPC>n7iKsw)o!B8b&S%5lIFll-X78)fU?tsGRC8lEhU!xQ=Qydnoj=$480Vl?;OJ=ed znIL!uhVZ$;JUA!*ooEcg)_3nv@!52b_9mpI1wfYGf__?Px}8+N?r~^BK1j%*(i^kR9l*k3pb%rW z+_6IjI_OuLFNcN0sE%|fH75PZOhB=@G;05SadC0=w>PfBWc#=o9Gt5^%FV{iPy+hV zBsYSy0?*om;rS=qPVB@Dib1YIGNQjA`K(B|)BB<6>?$!!=F z2aR8KJ$ovtS6vbj)^jC`3IW@!;Ni$ZyXGvCHr`QtL;~v%dd2qevmUhTWb&A3yN7hI zqle%_VFzvF_B2U{JhiNFKot*d&tZ)ElCf9ZD}d>$ZE!Il^uahCPEn0ScBH`mB5w7G zf<+e;WQOak9F%Cvok`eMJumy8sp8}iK1%`mgDd3G-NjySFa?xu+_6$5{O$}4VV1F% zzMVoe2m}NNS7Kd*kwSaXp%C{R+}{}ar-8hU-V6pq64qeN+TOYzz&YCrHzINt6&2O{ zczIr2S=4+MIGLDK0>>oWj$;l5gM&EaI>XG*Uev_j=i0DAsq!$jcDhy>w3|}SyCeHG zxv{i@ZBQ&RQ>2){ zSJ=LL`J4-?Zr4uA;6bZ%@q2fZ-?(WvB!EX0w5&ID41QTC$N_UsFtT5IO_e+1}|vJS=B;Q`62h?DgE@{k(b zC+z4ueIGsAJmiS43dDnTBhrEF*Fq->fc%2DTi1r2%64ybd^^-)$%PSQmY7fg zLlt>Qf*iYDlCR8HdSx88=EnUr+t6Je#nx*)RohG)z7|w($RGj^7nxoobL+_XeOOeA z+&c9J@Jk>YG_wNK1>lqKyRxD1jsnDfY?2lfIDrcdv0j)fhfwK&8gYJBQIid|gOIf z$lFtPpnTk=IH3iwtc?_*r5_>6|o{AayF1$gB8F^_Uf&V3;PNFCPtp#$p%G{ix= z6})*v3>bKN4BH75uPnQEPK6)KvuUBY84YAz3Vk>CZa`6rq;_(751`3WWagfsA>G~> zDvO7p{>V%=nt-%1eXph7t>e*c>`byc{K{*|;2i`vFkN9U|j4 zqXh|y3!Tpe`QhDnut&iB0eACLrC2nniTs8?$#I!H-`3tf^+;_!;f$U`tYsWS~l=Fa)yZ1M!N5I#`g%qHq`^#OJ zU-;m>J0)E|Z#V8=2*l^Jf7MiKLAGkt(&5s8WEPkF^l2Z&-v_vaZ09$ADvXM;g60GN z@f_|Iwf3b505dQb0XX80o%#G49}iz!SXh85qd$2MQbkQEv`;8ci2Se)JDg6Uky>>W zh+=G(AwaqOu-_30q(XB3VI^R1Do#@W&nJYbY>y2R)j$QMh7rmSj1Xb!E{y^tk(DFx z29mB*m|-os<^^4Vpg8px_^Y>a1kS4|W%Y-84Ga#}eJ4wj{Eo8%hShGkQ;)ksM|lU* zq7hePskJZO#}4$Op3I?Av26(ynx|o1{{vs@LqlXW0|Op(3-~2C3t8wRfA48S-;Tz4 zD~QcqlLZLEum64)L={DDrRv!wY$DnfhF^y_lefU>=qZD>4)=t3WBY$UQjI2QA3lk` zgG^}}j$xbea4uo7vF~dY#EtQK%{DfI?En4DA3uJGh=_C_3>L%nN6HxH@3K}oCCHXO z@Wjil&e*l0a%I!MS8GW+Q2c3~K0gB%TP2|0-FA))wGtEM=dCv0$S0a&qM|()pSj7o zEzPZu+^yYvkSS>gLW^GjWeC=w%hwnmzmRobU_(scx&Hfiz_pa_E0K<%z_&tZfC-;c zid$9i@9GHohVzv83(pR@&M-1@i+8^?)bt=5rHV7A7|bo<0HU&?9VXJXW|=kdAcq_{ zs3@TA$(1bdX*ss<-Bm&!fC@;|pvWbBT-=<4hli1YA<(;X9bXE7-fhMkGd~0144DL82|&f&aUIar+p3<8k+5EREG$-p{t zDI4ZkND*>-s@P0R4v9GKRRIN!d8Dv$E!FAezpiA42jky5?K9oUZV9Iu_{47Cx#JCH zml$awXa?M6YGC_;t1-ObOFU$|(jtce z*XM8>+jF#J2%L#W%o_Xoi#Kdljtr0%yU(A| z$8}LK>1B)2d=@^J&xj0LiHQ#NH`nZnKl9n#!8WYy14#)NC#mZY@EqaiCL;@gDf=d4 zz&dUd6r_cuQjSSd7v6+USRTl=Z8&+4!MPO;DmIhwr9fe-KriIEG)beAZ4dydF$pzI z)9@Q63<+!_Bo}H6Y@ckgc9Zvo^}I3QYl{05u;POPG@2gR0d{?yQ%q{m!aM{(-CeS> zTmhAVzKT7$1x*(qW*^WIv2LOyu-|jkfRzZ`?@jD22@TwZvU`stiO4W|w85}JBmt!p z9+Ko3@}D*>=@yrAk)jG*CizLO106%s7!YWm$Y>JKb|c_nti0zI7y-b2h zA4f05XCSGe58A$d3gHS%7#@S6jl=F$fr}r3ItUl~=>ZE2{Z%{3g;gc_{n#8NZbtQ1no0-GX)9Xm~VIP5WLzbAyoj% z>S>w+YQJ|Riz6Zm*;rXu!<2%&+lTk0cU=+#PfTpGKxBRZxXoVx@fcBv{|;VC!!1Q+ z>Dn2oA}mIq9#HMlB3Y@Ipj+{FcSV zj4-U6DRh6RQmIhsb#D`b-T^Z;0NJF^=z~cnRVOP(@%&#H5aC@vMA&Iy$$B?;1V&nA z84%RJk-?-)YgSE5^5`VJzzf+8T9a6@0p`=5e^>e3)C9Tl4th{xRT4A)$f;y*o~$KH zgU%8e@5K{Um1qH`w7fqz|4aFND=35+u5?y5^&} zSAl}y&TpR8*VAh>6DVhh$x?3CL?R?3k_hP@7_LZaV%tK@=osuSM}Y=?Z#;Mn_?&#P zR<=Rmzh4Imn()5CtUN}{JGfQ?^$bkPb4~gRth*?#_awwOXoI^Md#o*Y4`2%Xi6~7u z1Mp=Y>*mc&xWfVJST`~voZ%WS7{uYhr37nW)PUhVw1et9f)P+GO>6vvXC|m(n#3@V zsBLvh@sdfBMCwjdqT$@MsSoE_brd7H&=Rd2*5K~J!K&jA0b-~qKr;&Iv$`2NOaMqO z(C&bN8PD)#``$1*?0mi$axQNpg$*Tf{t+ed{^rmQwG*91Rr(J`+ zpeFV>J)oFdczQj&;Vvl+J9LSvf%TjfF#X|u@o3Br`e8;zE?!vB`YT8Cz;{Eyldkt- zvHo;XASr@q!x$nrYf3(T_RX~{O*34!%LyA$Dbl=@yy+MwX^DH{M+}-G&@-yXWNDI| z$ZeD8OUW%BXK~ksrkOFE`z6Z@Ld1%IDsZ{e17ZRCFQLy8pkDu+4G;u$OVWhmK7rvk z6Qp+#1R3R$AB7sA*b%t{O^6u?eEI;~TC?r4W2#>64*bRyEuPzTpv{>f7KvVL6Cn~n znr{#462U9!y3ayzM1-~<1qq6`(#X)+6P=x5^i~E176b54!-{BkF$YVtM8fdMKtvg| zzpCS+lv3~q1bYwx+T)&8F_Kg9`YBI^CS9 zw_#=JcWBd-j6saz@Dc|Cpwx-HGd6ky&z!O~9{ZjA68-QY)trF=tp*1o+UWRpRwCs5 zAEwR(D(AIbzwl~)%*Vc&vOsgb=}tu@^Lz-)~tE+=FytJc-+#JkQYi{ zy-F>b1Yz9B@pBonfvlxtLZYeJN=pbk{I$fUNtMP%tLN)@qBBU#7vy|QETX2<7~z%{JA zyma&0w{|kq+-zXKZQHgmip{-5CDH#jtZ#L3_xFu2)m~l>ZzFvy#C&6HhYSZz$>i}` ze=)lDgY#R)y=YpvdGjwaN%T7;sN!Sc|0Js(WHwXO-*NM@5C2hJ?jS4`<=blhjFZ>% zZy->wh{DO=%uP+LFyL5YrnkSFk;<@x-1sH z1VVor-abVX;Y2yz+}>bZJOn;;;YFB1)ByI8LuTIUA`{Mb&?SMViY!Y>f?Dwt;dWUDf9YG#|)iCPf3NZKk*Gm(UZ$BBnCKJ)8#!Ff#zxm zvg_&N(-7iZ5C(w2fSm4Q{0A$|d_NJv7L8}4Uzv;EYRY&y^o+H;dk28Iiy)Ef=>7{o z7^t`51*=gb4yUp;fr6Nqc>_yh5nDw>Ah>7<9veZA=#BK;cl{1@CHTA~67l&Y@FrBX3q3o2@aI4_M6x>4HHwV;KeQ?`9x@#*8ort3wlj*6mr_^>r} zB;pCY@@H*VB3#3+UAsQm6FEP)^pL*TQs9%r5(Rh6l)rx#q$6P_}{^#1$B zFvwyoX_||bnC9)1t*L)&Nfy71lU zg*l{opSl0E183i6_~CPh2>CeTTD0 zAMMd=qtH_-95;#-;kazNuXp^!27 z^l~~vhT&7L{nCm1WpkpB05HIWGD}XMlzjP%zJbABO78xsGa24p#j7#N&1!dv^w?6- zXvpSr7bpMCpCi_26#q{PumTSlfapDmiS^LeiUZGzA74+S5=N(Tv7PY?)A=#I58mTC zg}VN|NFaPur1l5X&aC*cEOF(A952BPNs>4_b^r8L6d`BN?xht-+BM_{c#X8?3>vRO zL_yo!EHgGHMt@=9t!@YV+x>aLEB*A72Ryzec%w>}#z^3XGk3;EoQt4V=eS*Eq=AZbJ>U3{ByC8~B8SUpHDl03? zyn&OG6Tx=Vn$B4shX4Kfc6@NfDmvK)HRoDfrEvjcX|16#;mz#s*7>6z>CCZS-y5KJ zLXy3DY<&FJf-mJaj$Zi{h=%ETY3W5`PBysAB>wU}$nyQ`&*0dKrKNBDkwB(a?@-Cf zd@vn-93lzs!Zfa9Ba4Cri}9~M+gDeX+B9DEg9^|0>|?se6EtI{xt2Gw-4G?7ICaVw z((3w^E9*YJxxbYO-}8vKmE@ybCp9=YoiKp96Eex+rj>=e8(5O@3J=o9)1&NMka0y ztHhj}Hz+d&FUC29@o61IluIQk?D6#CTaIY_Vw)SB22Lt=rD!lv0n-CunXnY+XH?v^t&J zqM)Re$}iEM{)&{po{qx{@Tlp=oS5%D`sX{zkX>cf(-8!#fSnpT`g`;2L)uX0%E$rT zn!09~=~^`APe862tsQkS+r(wtpF^P! zO({0_d~eFqVPLlEnj0KyjrYMV`eepZWi$Y#4S-_C-B%lg=19@O{nD`F3V4i$HMFhH z(eioa<6?hAieamLjFGxUw{@+C?=2hpY!TW@oUJZix@0rWv<&Fu`SZqn%ecPP~q~Fpxk<>wfIPq@7pBYl#y9Itc%rsydH{ z<*dG<5636a0CP2J8nQS*#4c2-O_8dH=8Wr-=%~!h4!M60a7KWbi!oS!6Aek|$@iG@ z0a<#&R)U(QTYGieaP;Whxb>H4yE!0IvF~@fwbmbhP1&bF*VI3<_Sw}o5gi9=(3D6! zTk+QT;oTgo?ix=ynslj3l}mT0Y~Q}!`mRuhM9q|`7c$Mp>xU#CSAF@`_F)1_1f?xfBiV1;?w}dcauHC3n!te>&4L&S0 zypYd|`9KjTXWv(axrCEoE>n0`K$F*N_PRsuS~L`q&`Ydwgeqg{Pw;-~_}7}|ejf{Ft-5i3BVzaYTe|A#Q-AK?@;I>DNV*4j2$IFb z=WkB{uWY137no&x-#Kn^4;=NGZ?Zxe9zJz?M4}MMQ)Zzhxa{R0ewWc##>BTwaA*@M z2WxLy+OL8fne;#c)E?PVe(?$x8&I6pM;IeWVvn|GmmeV$lGj4)oWB=MAunmz1RnYq(WFSZiL;R9itp>t z)BxVu(3rq7&>7jHwXLMPTWB}jIwx_>(jQ;V#j29QzEaLO1-*bNGNd?bRx_rA+O=!9$0^BP1T)lk@*Q}8 zI>a~}x&+gK)+xd#SHe1A@Z*0hK5-6nKAS;iQSm-`{dxn@{@|ywo?Jbyr#GQngf9Yg zlA>fJg*E~w!UhWb5H+YBdn|0Vl93J>1Qw)*kIwx(8q3xK4j&K_I^>nU$%-Nk}qGR|3Xka2wB%V^V3%{cs*oke}w5ex60o_}i zT^BD!(;uys8y<$E=x$)J_L{rPS&n=L?D?HNRt;nr3vS>F3aX1l-1W;>j!awG11rm- z3pUo)_Xq-UJbkgo7beDG%$V4LD_z8OUwmsaZ#x>(KQ~wW`Sbgke?}t;%9D=_3N;C~ zCytK{dFu;DA%k)WIm~Oca3?Ebx8|iAwQlJ$M!8c`)}+0^mmb_CG<(fnBr#X1@9$G{ zf>`we^8JI;mJx!9QRM! z)!RiyxE3)GGLUQL6gVyf6~8nUf6ShJSoOlG$7ce=?%%t|>FB-a>&Kayw@cOd<^HZ( zGj`for~>TMLW|@WXaGRIUw%-AwQKnAnGyug0^<+UwIU{v490&4YqKv1oh33Yp(WLt z%F+$c>dKv}Vs^=$f|R(JlN0)Rs%}DJnd6x6^m8)Jj-XJ`C+g><%SU#{Bm(e=OoIwM zg2WKBta4-OK=6Ek3XyF9>#huJz2i8ugr2{C{+NUvA0=Bbmmp?|K|`Hedk-Ei&mw6H zNJ{w7rh=wg2s+SEffHNY zf>&(H2$$F-a;bt23@hI5w<15h7@kO(2ZKbU6CkcjT(;u-ypj_nEna>Yk18AO@sVY% zcrG%LY6>RIAlww+W;U6m8ep-OBtzp52ZKTs&RWH8K$m=?o2f3wux&PD$40)7wl9W5 zNnjS{KZdTjEIp4u%5A%wKT445o`=Jfp|_%(f*V z2aIN7@FDz?)_?`dV*EXD=RE#Z7Lm1xvjDYf^S1D0Crko)kPYU|o5#>v$omEBH20S6 zNk&aj1^=pL88qogh7)7GGGJDT(Nig`QqY0%y8Qc~n#y``JMCpYy?U2%K*@$VqL^9R2cz`boq51qE zkb_W)|NC8AsRChfJ?ZBj4;noxhQUZt(}GPI^_vk7ht0%fx~GlR!ig~9-GP^(X{8qoJ{_oj#`&OABQjzRUq*~5GjAJ;epoUxKUO+Wy>QfalX^^< zhyc1~OlV4LBNe}Ak|`MIL;9WUG=9Q0Kc1lQtg`7Lb9}wZrLC3$n^4ZhyA2uhH6FNh z1-qu?`$0}TgC2(8Pl=*C+)LNe&N8U~3+1vG8zmsD z8z{&bqoMoJ%|`w2ye zr9P94g^=Pc9Q_^JFg3o4X&PL0F7nHNmqSfuw;9Wn+&jr01!lp8MR!+OFXKASN8Hp2 zb`=BF_crFUheLv86%>qq`&oaBjAc^Jit_eRz&&7UF{hQ!5gWXh@=^vG_-}W+9d_*c zo%7TfBP3)<4Im*SZZE>g8dH>-dgw!*ot*5-JCub%LKO9?0!bE+V~XRzN1rJYrRozq z^_&&|;$Kfrn?Ha4P)EmB6;&7d`dn!R6O}Mw^j1)5#|9NQc88HRev3osrneJ7MX|tr zcuKjDaMHLX?IUXK79i#Jkw2tA;s^t-R~#;&dlepuGM*7Vnfh^k^9{wH04z`8)|PyE z*KvB4!!7QsAT#K>n??>7w%ojxmR1DH_4yeaZHRw+_U)5teE(aW+EO2_HhOFRQ2|OIy&T}LKR#idPCV}kM!Wd&B%K6NR+4c8%7obs+!No#sh^x z=!wsOd9qc9x?%pEX+V^L&(FRV8u9=zBOMjqWc%m+PXm8_2Pzg3O_bYzVXA`n0j2t3N(cOxp zf&E7JEgb4;ggLIjYd-cLyDlCz?OiiiSQ^vPKFMI7_TzyUoCD81|jbhpx20}0mv>n{-Nq1_^ zs9T*EKAYG6Xw&IlV#!Zk)X2LtZJH!7e8t6g0Q5gVbp-Vx6)yE*#s0xgmK;ZaAg^;j zpU9p_8t7){|3GiVQINxwkZabb&t(KutZmqL(rf##22SdYE4ZDLW;l9iw-WDCWk&N@ z6gEAlUd{KFN7hfD*{Z~fH;6uk)~ib6G4fuxxQp;-f|vtCDRx&>9Y{{L){TNv58gV7 z52LW$eQ?j=GH}6qL-jYg_L$rJ0Fg(LRr|CrT?MLx@Y{Vy))E|Z5Vw6;ba~&T?rYIB ziXKArGF;JaFLIuB{&2OtZ*#s3TOr^qo*pi^^(-&H*Rr7e!or@_Za?RJnfm3?Gq$@O zRXwl2_bhRuKd|$ov%du8L8xIuFxUM%nRYdxQ?DL9T2P=T9O<{&c18O5(2Dmc_l8et zhA2rSpDAOijn> z46ksH*tn5_I9x>b7oX0l`tZT{AywIBta@J&NcDh>CC58 zF{!P{Vvb5AxiHz7&X*DMO&MJG!PS-2C;l~eGDiShaLb7@F{k1R zYkWIJan#u&z~|zaU34iaE{8NgWJ8H*0_Q1y_M2gp24F(pvu10Ck6iTHeDND-`>lWF z>(%d>>mDko>bd@Ns8eMc0K7#sBlyJl$G5Gl{pHH>2EQynH%G)hj{Y<$!~l`wFx#3x zatFc&6w0w*e^BcV&v^f2Su+*-5{apoE(PCSlyvjhG#k+e-|m~#;~7;N2L}%>wX-j( zfF4oVcbYeA`nqKxrRH!Uk!0qooolT_*REy%SkjZKSTpFRCQ#l+rrnM-ul@VGYIP4% z;VN#qO!(47SMOY(jcBbkP-Mk|27_i=3>cu>uU}gRl*ccd?aR!74Qd$~o+1_INUp%t zDim;-XHYw4_%z|Cfgh`m=Pcy4-8}8@oiJdb{mb;2w~SHH5(B%~56`h`0ae!o<*{K^ z%E*Q6{|sfsXUu_F`F=7G0=&r?TXM~+{pa_OTZ-$+jvbP;{rRMqDF|g1D%9Va_s;$Q zq75oeb!i4acCP%%%a`FCBkF|szqHhPz`+7amYq^=^N9;T8hy<^PN2x%DHn_wry!Vy z3RyYPc4YyR2z-$olEBhyRyQ-|{@av`jd}a-_s;7y_mu510GkrZLu7RHZsh|z7E03> zVantZpG`n(j%e&Py*{)8l3iql>1StMr^K>7wiE&_0F4!gPhCMM*6)|5!5*O8du&_xKy+X)P`^~|jncg7}SfFN1k_>6JCec#^ zRPJm#9eDQ`LR=YJr{NSaom5NhNfn~61HUrrzhP*{$&4D(xaWc-IlnRu+q$(4UF15B z(6${PROE(=z0>X?bzh&a@COwNa>F$w8AMZ&?-%4h<2s-+%MwZn^%8ZT7s`hv4C
;_X6-cBQ|97arYIs8+Cb6-j@UIZCi=KENL}V-5_1K@|;* z31+IKP!S=E(9knW;hZ+5qe$|kq8*lFwGn5P*353cpl3-xuf(|%$&uu5&6@z5z zEY7*ed_Y7#MNGlUe#r>a%<&BrA~}Q~kwX3Gl=D)U(Fz+XrSy;P z4UQtfG8N4RGVwH^NvuUCxP2$w?gO;gK475{NQ@|TLlc4zkK%5wr3er~Dedni7Bb0y zL&qsaz55hKT|LhTiQ%$s)uyXU>fCgq=mhJpEuW0!Q|-FX-VGl`y$%S)YwF=bLr?06opuq$xS znqqJx*qPgG-*}eK&SEo`3}_Gu8PHhy)8kz-Uo?;;^oCZ;8xB!+Ba$)G0h|mpHk8jD z$VBTA;B0P9L_JTIQB32#muk-{IfgNrY)J&i*zjW+cpxN%d2cf_FZmXEd0|*D8+PxE zgCOxRN3+k2EO4;xxZq)6dQ z3j@Wm`>&O_DRtQf!toh1Z8OGul7W(>f1=yzKhr%%KGL=vtE}zoBT`!@Ev5Vwl#y9< z)UR!?KkjE{W{vdQlc{nc>OrsZ)Ied56GZ4RU7WjzQq3cw4hMTq1O<|vp|zV%FZ}R) z^n&+~IueBL9rxW(e3!Cb1c!9lmt+`>St90A`wti(mU+nARv$e0vfo3r|FWJ{iaQSO z6QVDFM&ufjfAIC+!-1@RwAW3xv0;jlvgO1jXP4g+(+%8{YXk4Jwa-~CGvR0gtuZ7O z-!{M$CJ_X7#k@z*T7oGns)A7u^7qA;kgDMMz=ef_+0sO|6K4UQI+=W2@*+VYWk`yT zBC;jqQ1ybQ^b>g%J&v}qaWnW8g`m(BM&hf;>T+Cy*enx5-iO~Q%9zt{Sx0;}wG|_W zSvk8Gz8g1LFgc$1Wf!Mm%SEzDQ=N;6js5a@?B(E0bG1GNOw=MdNl+9V822ULp3N1G zlvN}}S;URN5~Cq1Ho=#1{en-GwG5bR*6n%4oyTb6QBin{Mw-HhOz^DoopMwQ^{}Qr zk*Q#`B&4A8`@47U*wPZpb;eiO(^+EO}K6RKLg`LP~RKFg&6HIwsXPnO? zx|-0{#te9~ZgbGd!o)QQ>4)OHIqJjHw{PCaZ))^Mk_YUd7$u`2E8I2s&`CW9ebsP} z^KFEBv1!y+L!&XgW!$c@O#bTNR88z_dVQ1yCb5z%5mks)J#>eQ+iWBviJLPUh5PLt z`$wa;ojR#7F}rTqts&DW81xh=B^IhVc+^V5BxoQQsWrMf7bVrUOK0l&$&honR)7_LVuV4h;*_ z>(wjmdX5f91~JUUp?|CoWS_X`nnAt9m~d%DY0n*^&L=bCv++ zC9iJYLY5<--}MBGHiUz+fgRD+#mMJ@Rt!FJWKP_Qp&(A|XtbKMUOtt03E&?h%GaO+ z4OXFzoa3xzbnN(b=dWANHn$%_+0N~gMuKS7NEYPTEBJ~fb-%J@%WbcpnXvQ(s(07j z+eP+mumZyHAq#mg=h5s)g<~HE!crqFVB`w!hdsAO*b+zI>T>E5aIQ6GN5O`Pg-#vQD!=xIy4E7>Ye2T5s9Gg^Ln$^{T8_jnc z&B^|YnosPhVPIA!+AMT#jgHdgz<>{5*WDtpTpK+8r9-O8yJI*NeE3H=+1+^Rj!N`D$`JHnnEe3m?&Y26&T1-aqM&2Ak2SVNbxIaDwycsosT0(O&OrM`RFP(7va~^fc&8t zO5iL4Lpt-|B$E%Q$opS8x&SjzFj1kb#HR+mys>`IZ7Kcj0Gkgy32dr>fps}k@~&L{ zla|qTm@WxVGQ>xNDm)OG;p)FfkM}Kgz=bVs%6W`j8No&cs-`)1+>Gm1ePvQBEiEm- zd&Xg9-qc0({dlJHaWJ9Weqs@uZIUWS*D%c?`fZHEo-)dof1 zV#orFP1aG!;tc5Uz)m*zk)=c|4(+a4C_Z14O+{D*Dfawf}}A-TFLtTqG-pn6ei2i;Q~F!Hv5% zvPr)7jW0^e&5XCBLC`hc$8yvsPoAtoY$wU4rhMB}&pC5siZ{PFL$`0~L&QNc48w40 zc1})G(OsISW;B+9Zxdm~4}h+uF|c@HnQ>Fx1fFxSE;2#Mmf3JdjxqAti^7S88P5lr z$LM|eqNJxT+h93C-LvAYj!iMotU?DRrSA8kXZOAns|c66WO&v(6a?JVoQF)~w_ zI5Fhp72QjNrHjWPL}M9~FmswK2GWLhwdj@)sM%hDVzf82nXU*jrx8D=MVQtVDvHBU zR-?LWv^`hB^B1!cY%q>d9hV~i9rx=yq&q9nlzIvVbb`vOIUZ9#?UDp0J$mBWCzWeK*uhxETRiQ_7V>s zbgg_Z)@;(d0-dOtJxVHk_T%Rs)3BypFtcKWb@(4&!5-9?&ikojL3}r>_j^f!;+?#2|2- zS8>|Z&VmVXxMXun+|lI_lQQj2XkZb*x?%b&2Vu#wmY4lhAk4J1d5LM9wlT@4gZ2!c z@B0Bdn>kgDWk(M4x7bB8mcRA&R8oDzmotjK-)~+^0hP`|Oo}Iw%$w!aa$$WsEfzZq zRw~q^HHM3}8awv=j`ufK`oy4xdGU#IPQA9rNcEfENyqPl(Ih@z#v+1HN>mXBapea6 zk?dBT=liVo=bl|QjiOj`hwQ4YS{RyIS!}0RB|BYtD%`j*$8N(Q9Js$2-i2`)^0gf9 zjIN=3y@`K2`cwgED6*5L^hU`Bu%aaSoC;0UL;}Q9a#7;uLZz{&H<+GuFSM80f3VuP8n=u_aYzFyl&m;VNR_UV72~5QT#$e9e}LWrD|<%ppYRRst^mVRZk& zgEA%rtq8p`9WR7DM1AF_Pd#qyo(|$Wim@PHV=d6{@(<^kK1Syu9zUG$wSasM>f+Wy z%_N*_=vQz71j2M|t`8Y>)<%i{};UQ=K{<}92=OSp-(268`1d%z4 zW51`YU8f!m)V@_4urv7F=$mOh)QA0iIWNCvv|3z=wiBaB{rK+#i zq6>GSw_Wq(>&L%tMQ5}t%*#_k^K@A-4l0RmJ$kuV<*ZH_K&WomIY&oVckjJRu7a6J z>yOSN7pwl5*sVs1lJ!U)^-!9WA*Ihb>hGu~Yuhjv*-^>&X-=ffWfQRsr6!f{^J5gU zF6HjoKR8D1D(+z5g`u5#G*VI$&k`9;KmiyXyTJ(arr@F4lFwZ~UOlX+{^ET6y&Dz8|64n+i0WZPW7R=dz$iQG&wMr#=V7=o&%WSoDB!v4Yhu{S9P znWC0;%2_O|XxFaWU?ms4Xh#h0w)fVH+pdL4Xy;fF^m1?*qiuj2N+6*;`n7bpPEQXF zplX!Io$%Brj=NAPrfynqV<9Cv;Mm+T;> zLk7F+OgX^mi*qVFgfMkj$<3pO%RPQB2|m7S-VJ8{rOPA0$_eC3;kQ{vCzAB8$SsOt zv~dfGbW!+amJ03yH^~DEL6-Cc7R$av#Lpq03kMpdzW(#u4TawD_%-UobLuNkXw^J; zT#@$nNnVlZ({eP7>-TjW7rnQgepI&!-7hx1dSga&Ppdw125GcjyY8peZKSBYs;U%2`sb($_Nw8qSGK{B_$<=%Z|!|?WQ(H1AOWY z2-q{fqn}E^FsLAZwtvWc-JnilVWwCm`aTRfsA^td%L@_)7c84Uas&7!m+(xbEG`+9 z#Z&-yI--1wQi_G+X%%xNi)>ET&`bl8}7@JN%X7{c=nY5t2A{n6zy`N)K!U>V1u3O$v1 zl$TKwUunMZ#g*0B3sWqvw5R$wxbUO6+v0|S>qXxIW08ncycS`z@f|^sB^lsvF?dg2K2|G47w!Cxt$M^4keKy5whh)J_5C{g7SRHGZOq-^INs>6b zgTGt3yZ=3=ieH0_&i${>!wOlzRIJr4VQqYH0>+F@qwJi^O+jRYl_P{74NQOvR01zs z4V*}9mrNuvU8GDXC+ke$sZbVfx_kc5#V9=)5&Svi;~@EL6AvU{tmpAISx>DgP~Wfn zF{6I@@+Dnt+e5U;_J91fN8Wg`*0aqZvo4!DAq@dIcT4-i zZ~r^D!#1)QH7g6mHc_`Pdksr|vdQCLVRbK@11IK$j?T^vci+fkeCoAJecAPdNm6Qr zrezX4&q$A9*adOI+BV)#E*3{=0v8G_+ z+yHPnDJ?`-L{PY6$hg7EQzc_|XIFekWc{E(_m~EM`YC1@bF!8ERMg(_^cqtt<&kN{ z`$Q^k1ih<}4T*V!>`liV6B$&uUcE+O3s0JD!~z>N4Gk|;liDHDGj6wBK7jb*{Q6M{ zYk3fBm(*zOz7fU;<9e}{>F$8{^J;qW07tw?Xb}3^G4P2A!ewBqX3QFk+mKkcJzoB$ zBl^y7Im8u5jp&8y?&O10hpIcRT)DEc_Pf!C7D1Mskv2jh z(2$JS*Wq*cj>_S%w12B|2h-& z>nZr60@(vBuO+k#L=PA&X4*($j5mtiEweZ&-~U`1& zM+D2-Au^v{bK%#wAs!c2bmY3JUgc1Y3*0lmv!9BVHts&q`*b5Rl`8_vipEPfvWHLs zM;;2_inXiB(rO>+=omlPJYx!j!$>y`{tby7V>ezxZ|qgfrvO4_hcyIC(2q}doeFML zd`R~zF+yRbgTWm2L+p|<4}Skh%gIMB>#~$b`p8P8MUWd5qmk+z$==ui1f!Rsy@`Yu z@n(CCYC&zu#Hr!|I_XS6(y$Nn)!ioSmGsfw461a{@~_b@-Zjy{6=fWH889MebQ!Q7 z$swJ8?4+Qh1e2SGU3+KvI(9o{op-9cAWdj*Rnb;}2q`@bFp`lV8Fhw&;c<-cS{lEs zjpcxfy5KNL=FLElR?+tpn(xJqZ`3I=j5*h#oFD%C&69Q|KMINbFAKPOG7vih=X(Z7 z@5egnL4t~5A5)F~7!!p*BXo~G+obbO9zNf|={eb08el;}Q&aOZ65OEMoAYPDHVo3W zMlbEH^@-N+o~rOUCqp$xW{Q7S^KO`{C+W*1pIFdPlttvI>&?wx45%Du;$V;%s6tpx z8)K-drR8y7In7j7GC&>5@C>upYlwcOC>R7*CQd-fXKnV9+$g@*!zT1JFEHmQPHvLD!_n?c;bo;H8~=2e{s!J6q(-XIAjPu zNhX`K;M}iU&J`W&l3+&*yKn@gGVT57QRdBb+3~w-)heT0g@Q`eT=dFBeLig80WB4> zJWVV%INEwuKOM%;$sSQqmwoNRX)e~}JvBZ4nqiMe=;IGpSyVNdGpg@9rj}w}>|Zc` zcJ_#_`wcz9;)A2@?CgfpbFlMAKV1tiUYQS(<#Y_!nP~jA^4HHLXnbWndeSJ<(WiL7 zo0I2vT(;0Y96-&_S36loMxcZ%ul2fM^7V-G;ei$wap~K4>(0%-8@kEU z9lEaoYGz~5YMSC{3^_#P-no6d0a*rMsr^P{TkTddI}y?<{BngZA))RA5)#$`k`MEG zeE!e2TqBNtF1q1%kvE=Ju_c=XW}OS}R8Yz>7@gW=w_TUL{MiHKq3CWsd#;U-*L>;^ z!z(T(G8v8QYD8Y!ef%J<-{F_%t{+|VU)5sQgpw+E+brs{Y-ll=%pW`ChjZ-`G9_F` zy8;(Cx28NHTkrKV`KkZP7Q>4l`!Ut58lh?4RNga%>Y+hhn*?_2-aUGfYx5b)c9hor z%YSux=!<-euxsljI#ZBaxUCxYlsqXd9amlp-?SInJK|aWRV;L1)8Af@p@^LCy_j5~ zaun@2tc-qan6czpsdn_`JptvIs2byV0)L@YnI7mj8e}>u$|LJn>@m&u?M*d4Tv)fG zlGu4@WS`P~djI=L=rr*c;XgMAM-o;tmpE=db!y?hfS`P;yFJOtQoHAR{oE$25!fJ) z&V`a9alXP&MHMgD`W%^T?pF8^9Q=rPBBx-pX-Udyu_yqTDV6zAa&;yDTT%(lF{5Cq zx6H&^fPZ?K+WCH)DP!@YuTNn@I$i{qc301J!Z3yMALA;h8@tz~1% zrx9qMkye=kw!5|bkj{V*7$8IADu%}M+6j~=Bne62VEJsL|IS(u%cP#sWVa3*n7ib>FznX+V7VF{0gE}6bs`c@6uA68xnY`I zk6aK#5#jvKQ!Oz+lij@ZB{x%c+#wN*`%(9)nOZz!Pe=0;)IO!+LqyrNFVg%-OCBXt zXkvWHKEs};&fQu&cg;Qt4=b!O#sPN=gBZAoVN{K+9&%80Q za#z*7B_b){IEY#ZnYM}MjwU=`NlhHLiLd${OTHBnd6e|J(_oegu|AaXGHJeBv>{`m1j%v7+KZ36YETHw-IkP@gzFBB4hsh-1w&&^xQHbm_ZIot6D z(^c?$5aVS*)UR8HDOa%BJJV zHpD>WF+A48GdFiBdu%QVHO?S#A)u0YB)(v8k@V5%c6BJ%z(Z}2(oDMPGkbOfgog*> z5s)h1@8`n4w(8uuCFq5igit2=E=(#qFuLYh>nOX1iUrSxmi7slr$Wn>!?V8$po7fN zlQSqUlYs{nriU`hWp5@U<>Fu=gPH6?v72nelM*Wvz$DmsXRolY#W56JSM|!G8j#Vq zMY#tGatiq%=3^91-*J5=%Vcr#+3(joquk{poFX`wRC7{(^-r9Ql~p~tpOn-xr^i6{aBcy|EbrxzTppzCBqCK1f3o@W zY%=MV9z>ZK%t}^~4FNzRT^W`7t$k+5pnj$Mr~+Jv&OJIN(QzF(h_KBxAR!PcNG(fW zytwz`L!14f*cyVtBi?JFHE2mI94Bk=Z64?3ls#z^1h9;tkS`qh|KZDI*0b=ftwz7n zzyJKw^Py9_FwXDsRUX?f5hg_=GYw}v(Lb;|E&`l3@Mw^8TOoNNOQZ;;Mv(oMax5_| z#AWEHm8pZhz4R?XU;bT;@q!f*ig>ez3~!&5IK^gjg+b5)>v-K}S8^x5auXq|n1+jm z1M*6Y1sW3C@5PpQVizJS=A_@?{)I55O*s=x1}LLWymuzBE7O}Yvjf5)`x*HzYjMjV zq@qq)OQICs9$A*`VMSfxPaVbjq^!ciqsLwMbdT;s3r+u$lc8ptsHe2PyY`9a66zRw zR;GEOjlW3Ib3eAY8!&0P_6nLJCHTL%MRA~HXA90q1nP?!hi!W=e&=zLKR|(g zv}$RmNF}iDNs}gdiWUk~T9WZ^_zN?7Wy&{JT7GVbw)=u z^2yf{jS5?s_fWUdRLB~Yhg;fB=trHTxusf$a=fb(7T^cpAtyvIM?c!D}dK-PT& zk_zPRUDcvP9ImlBJgq0b=yDPO-Z^UGnt8@_E%A&s!J4G>5OVSPM@kA(Oj=bfk*5sV zPs9wLdFxh=`kxk{ndR=5$T80Bh)(v^U*A2eHcFHcV$*}|uIPbeu_hldxYZhT^s>T_ z*>CUjk9IIzMpoa0>$bUNua?ghLEU@oWdGKj_7T#~hP$Pa#t zKQ%v#H?EYJ**@{MnECU2tw^qzY|&H$M}B%jFN~+Omvz}&!Y8yjX-{N4nKH_opBBa$%v_fK01Y?Jt95c62~$XO9nkwd)}VU*C@SSeKe=4e9sxPr zjRq@)kY}cN%=SCf#9En{r35xkLE5kX7%(a9PruwhuBttC>#geIy0mv(@%nk)MF#K@ z>|SW?c9Jx9bK1|hPdim8*R z*V7ik!O4ixn>S*0Xq&T))hDYS^veo=3Dn?m-9qteR(98xMNxcY&$n}f$XH?>$4B01 zlzydtS;@$b0~TZfC1`f+#q24siUGUw=~M55&&EwX(#3X=;b`S)?)Lk@8KW9aG7aM* zd*??RPCDjk6}&AVUsVi^^f)#E$Sk$2Ewej>0|vg%!%Eg8g8<1t6Ci-j}5raZYlb;-zR zVg=HV`D}AVn%fkP_mfPh2mHv;cIz9jWcjcS+z?i0pab$96 z%cz|8Na51|DA45TT%;4#wRq(=p}yr9`)eC46rCL$s=ZXC@ikLDKj1F;0~MN9|M^4T zO*E+Y%eX5;YbIw0yc`dzLO#5;zrgCwj!NeJx^?T;C;UQ_^>1`d0|}eC+|wuT-?yZ{ z7@1V6M%x4a(NBs{Oe06>T3p_m{>jkz{E8o%faa<<_2xWFY_j{FRyVbtdQrwFX+6Z2 z7AP1KIKyzY1U++ebt-h-Mu*HFabctK9p-FTbptN!wX6smd9LXXG+toyw-Uj zF-#KGSE%0Z+Twp{FS@agTGPaolyxNVYdP{=3Mm`#R^Ld} zO+0r_OXw-0n*J7JHpD;>5IYtwJHI4Er*8~1J3mr|3XZQX`@mHdS8SLDjomTQsb{ zdQ`vCHamjP)%~)4&)IF)7?e}|HH9)a>(jM$+L%{VmQ)Y>xAf*Cf$l6^aUO_LJV`hS zO;We?EHel?zU=5p8tgW=)Cw=XP}gK-36rE)(uZF?mXL!z#?6~IRVVNKIF&8JuY6Uq z@@{Pz6c>EBU+FiFP2zlY+phcZe2XALL>zjA~Mv#&A_Oexx!dR5kqBBOM9bel20 zd<&(KueWN@p@6a<`n+VaWy_3%1zJ9}U#y~rwCiBOT1pu~OwCwe4v0rlbeZ@jyPyE7 zy`h$YkvO=XM(3R&1;nO>>DgIF+JmKblDsMiDqUqMns>^wnIB7S*)THW=H5n%tel)i zvU*$0DcEfL9d1uHdysLR%Lkip)asHn){W^OCb=ih%$|7nM(`XzGbPtw%N?J!%5H^b zS=Ptm8M#0IDRn>>;-tQAR7!O^AFB;*s~IjZ$+sNTd3%7~BgsvtDiA#>EB5Z$GZfy| zxN}-ciZ)rUi{c8vp=QFLw6H!9rXj7Yscf!r*A5N(MS<8_@r)ibCKBQ*IOyBkznpG% z6+GWTYJ94sa_@yd2HnfOdw1J{H}|4i=?=Nja->WTvYWgxqj{VzkX_t5K#i+y=|K0oT-UtA#9lnqG( z#4z)%1!n?f{u5G$j9;;^tX|MR(J?!B_84#6&$36?GpA1neLiLWw#uYWpN0xXG%j4! zB;$&=f}-=hwf_G8EMy*zcoI5Ep&)o!gJP8biOsodfxNGHWRVklhn)@TG<*D3iz}D7 z;ZsclCT@z19I;}BCC!k>+cUICA`!q@aqKA#_HpDt`h0v99HC$rypB~jDpv9l+IOn` zwIf5bck5n#Z*#f$z1~@?>Is8a30`WH)@Jd~hJKwa?Cf{T)@>SGAs%@}+yV zYi}WXZf2fJCWO+hJ)!>*Y#RGL*K*wp;CA#aady4brG3FXRFvbdN?vbBgMv%@y#2I` z_2frWJIFe-rlH~~H=h9_8I&Lt9j?|~x$>9MuRAO`=Vhqt#YS7ste)8>lOgf}EBV&r zpAKGH!x3#}YpcQy7LS%g%P+M~`@!BC7q^a}RU(uawLi9LS-_U4sByj>YaGN{^E5LP zz>;AHkKKK!NM`xA$^0tM z`v3n`nPQ@sJ2dzawU{`j%A6+_jNAZW^AP&w&r3&$x`t*ClzIDR-PZK~(pBI$b0c=^ zrp`k)v3*|Axx$S(-uehdq&Jv&)Z-$h7YN*Hkdi)=Hqh%JsFrO3gqurHhiDw|mmLoJ z#$!!9d^iG}O>7WwGC4T=)?)Sv(i=HA?>^bOUn$jyXu*utd_iqQ;-7HH* z01c$qgjJsPG1-8F%RL>6B4Y8oe=btUigk@Jk(^sbM_19qve3%-vEJOwiO$Yl{FmPX zS`{Lc0kwrc2i<#q+d^sSH{R#E+@5P;p!Inj&%gmTw#c#I>q9W?M_4IyB(tySgtRha z8BX=TiyxP~9!!*Ls1Vmv{r&3)lURo1&wY#Jb)SRONC9F`;>)CE7mBC8EEtm^$2yT^8?rd|; zXVN*V)T4~KUioxob>35%jh*dqu+4%(D#Sito2t*VH0srB-pO_ut+#CjO1yL?U`sph z0F0)tscHI@_ggEDZ()L&nLpp;lf$Hq*>m%o)@8l5$O4z`cFZ;BnaZRRdmhL9s?zMx z;qIT2>jrI$QQVJT3`omI92@{6+n}=Qn5wG*rhy`Hq2sV{9rKlDY2UIP!Gj{TR;7-v z5sGVl_n`$+zOjh6Eu@d9dtqBsGqcpit|NCbF!_BR~;{db?jUw1n`bYB6_FcF=x*-Vw)v0I^B zb2AbK0IqeA{_#+V?t49@Co8w!dbag*rAJ7-v@rXPXW4xHF~1%IwFLXlkRUN~$8Hpxj-uMSa^yJG)gBZ!l9n$q63~ z>4Onp%|DgbL`S+75HJdyp~}QcOL5=<{+E4wlue4w*yu9nz>L!92i5x7H2tS%t1M`v z#izQg#T)fUv~6HLG87{G`mVtp_{Fl~_F;f#2!5$_v$C+44P&LiAkyWbIsnCsl%f%k zf?Mh`cNjH7j8YHuI z(%NaSjQ9|rKxY%K|AnnV=IgUN3y?wUG|7-KV*aIsc?;3Bomx@(adBMycm*t*jDnX;JRrOSm2(kM zg(00lt{E`#TL$Wh+1dSoGc(GIl|fgp)NgUt`Y}oa5qD5c3ms0eCzLOeiu@DHLanEj zH}Sb;fHVOt>)_|poD7&rf3}9ieS0oyQ!fg}-E(w~vR)g&+vO*wEw!f}g~;Ytrp9s? z9^csgzpkrDJ5XRb*>((nT#9a8VL7F;EPRaV?2Vd*yN5)It`t0>(O>DF6zQ>zIxi!W8Uv3w9geSrUW-qf3EO%#&c{# z<8Z(3Jo1JL;T*w7`-_D(bA*6LGWV!HdQ_cb)jwxW+_^E?<58P^M~-ZSikQ%0PB%kC zF_5QSh)tQ2(TW}-((6p)-_NXPP^bR$6(p41M|Qq?@uE+kpx~=45TgaE7u0FXQ_(kg6@Z)C0|q2zU5d70vVlItJW)aV_lgi->w z-n?_?sDCj71!40tYa8=l;{$Z!^{=>Rw@F>Wb;yeCA31_<0z@16((!ir)H{h%X4cLZ z<0*OhEDRK`DSd(-77Uco7{s#78Q^imj z+f1I^k%m)JwX=)M>m(GK^$D;gpWRXZ@Ki;s&n(cy^DF!IJORcI=_8}1MVt;~J#6P) zO=Twym3v_=N>$$Tx$4KfU~$?302fni7#Q&mGh6wgETE2_BR<9jb54X-g1Q4aJon&A zDW#NzUH+EwJP%&>sobYkOJs$CP_3&QD9MIf1QOrh7#!m{{O#u61jPhYovw+AV^7;= zzw{Z;VOpvNf=-%!=8zx~#qn%X#_aaEOv^<>4(G)&giEvrxESZ*5h31Y`}b>GShS}V zk=!U0Iaj0%cY-XTXBb(?Sb4eeC4}g8vDf>#LIFBdi960P>XY5BZX7*KH|qNG*k}Xg zCGN9O4PlXu1cV*jyYn_F35!8zDE zIyzceL5Cd9p8N2~$my>}lr?8=sw*XJSH%??Q%VcDrY?g9C8Q7Hy1;@)v4EpB zFa8!4BpX?CCk4$UrH_!Vm^s0RPN_wZ!^hG6W%$nD#W86^5Y6ztqQ*R2L&Z{jruNyG z`l%oh)PdpF8Pq9~5E{jh-e!)P0ohV{DRclTN`qIgUZHdeV;pZQ^6p*C_g#T$vm?c~ zyK&8ci8CK`*C975+Q3=_K;0ZHU-9up>o`3BN~@Om5R|)^o4fd(>9B#FFs|sR9-5^V z0mqiTetj*Yd7(`~;!l&ADiINL*du;y=4}IxxKIf6xjEom>?5klvGs3}hzJrrg)RPb zviOaj172~toEkAce*wYt`UEKquzQrsg4&8JH(64KD2j`Vw--$^mW>!xrDD&VlA0<~gn(1g=PGd# zlpR{k%!)(0*bqM0SdQIvF4}Q%kYF`kM`k^&SSM=i_G&$+9JZ=|Nu5r~XSMC*L~^th zCQ;HA5*FyF_HZFa%{c5>N2)M!+$7$WGOJnQ=6%eH zh$td|Lhn-wpLWc7RDbwzKi0)qzGYo)d-1v0_;CNda10QvRooZ$A6+IplmVoq!UG=@ zvA>Mja2JjzA2emtf;T*tP!OblF(fElep`#@a&+p2O-SHHWX9+8a(CJ|Km9k&RkUYd zA&*LYO=T||z;42Twz7>HS;kOg6zoQtkD+mfen~THWl8=p!QUVM`q7ykm0214-8h{W z0a*d7lyH&PVNP()NOLb=-{A$Ttq*qn)He)x^dh!an10Xq_m2umw!KZwE=%N*elXH% z=iuP&?zEG0D=xbJ9CMyt^c;(+!*EWgqC@Nw0wfFYazEC&#ZmLpebR=20ODmM9{Mus zK*F-OZ=**cs@?Zx@R2)-v4`{ARnJsC{v$Sq z?o2C!p!LLIL82*hN`@mxMtJw6I3X_ zAp83D=5(b#?qh<}nFnEbMts2#X7F2qOe}j26(*qgs+KUZSf7C8r`~yLc;-4mhjcnY zX6S)X_<3_ck;?D2fhaoeF6k89J)L{nPE%71Sm_tnFdEG)^FuQQ`hqKsr}hcsG=Km4 zIt~9zE0*-_PaLT$(hOP%Qc0QfQp4YJ09cz2sXIS)-$3MH$rRbKwQ`dt6v_Hvp(u`o z`#dy2Sw}lWbVL=kW$Le3!$d}Bl5u>~fG(nIUG)CZMw&(n<~BS%A24U3A3#;_#b&o- z|Dd?JaH+H7{(S}FK=BREV{mA|<>?#YkV0Pv-O&=VP#80=ee_E`^BjCaytyONDg!V) z3=q~K^aWNYO98GQ425C?Urj znfL>m8ToG>Gf=h0@bm^Hu-hdLYbFEU;;$4#-qp4%L-xaWN@eGyUrimkj(%*?PK!sQ$JPMqQ%)pB@8_-ZDx@r3FywGYP z`aij;#*Ovg`S^Kz-+nO(k2JI!EGMWB!Nb;(u$mg#Q|pOp0xjmj;|V8ef+-(nEqHYH z7RgQ|8_@nv*J>^P-vY1buTXiY-oZ(SDt%IxM*9ig)fTg!RraV z|5@wd?)2@bS40Ywa4)WK(QmNmk*2R z`9Cc{ZR5D;=!Q&Rg;$hjPj4RdJ%O^p!rx8nAqbgkxUR8tZ>6e&7eP&G%>=CEYji2?#b2S@r}D!TN0j_AH5JALaw1 z=Z|oL*dWy$|5v*b-M-lrjkZtws`c%62_g2CrX|-)xpDOD(J!Wb=4}y&Wqa~j>iBXC zpy}B-ya<8EO_LlZmT}?*kGSw^$|l}`!*c5Zz@?xCC$o0(fMhtIKF_zcsu<5Qj7ggip?PxBa>_ru$E%gdmBEolGQvHyWvE)4{Z36ySM~o$WTIm6eqK zl;s{zXNl|DyLVH{O(F8YuaN?68aJ4(6MS>?tHwtNRf^6VN2(_D_pdLzGT?qUre%J8 zbt0{!nUCG6yvuo8f6`}0yz;uVZk9M#5Q%(}eq)JNeqFDDFuCkf%kaFo#%=1hgoNfO zqsVhlc~7_mEsv>)8`N#M$AD?xZBKWZ@Qw}6UWnBx9jQul+D=V7bjbZ}I`w}81sf>Z zm)I(o7SH`NtLH}p2{!Qjoa{Dfk}_UcMw(qVF1f7T$;w0qXH8g-g4p|<{gA^HnRQ6|uI~)@ zM23&HnyosjPUUse$;R^#+T_5Lfy@lA81reEM}|*X;Gvtc(YD>+O|X)x8=T3=_*s@< zMSOuWt1RgE*ptr8Wv;=NZaf{V?Pp$gpSMfzFq${(E~=&(2Fs~d#P|aVfzh8| z*Zq1;qZV`bGk~X*zuYypS*-ot2y0Vx>(1Ftd=TU7+@~ux!4}XR_x@bFeuVFh-9z%& zkC3`NSB7UkotL_jzakX|ol|2J!g*9!vSh`=$$Je7Q&up`*4Bue+1(*-Z&^-^kBzDO zxb4qeHP^rFyCi&j@RHF3#_zaK3!XWSy{xBXU|(Khu%BY989ao{)|`${$}IjX=oURM&4~Gcd6SuA znRYVBX(BqR_LD{@ z^NY3;iYG5dZ~W85b^W2Lrl-==Wdc*L$?1H~H5^C#_8m*M>Da7&0&chD=l3(kfhVkh zhiA{3b3b-m3%>2mCNIz0a8SmgKlc8&hhHBh>_@~Rt@ru)T`r0)kWX>KY^0yBZzE#d zga@GxJJ3k8;51_E^DI7q+l17Cc$PCX{D=G6QBiSm;iytfR1et((&UQ?mdpa%ZkgW# zSWPn2B31Y0<6K;X8I+Jcq1s_9hDxk6`nKWkQ}?qUJcy5PprjKbmf!^L>F(=C5tMaY z14YBg?n>E(Jm%w*>G9+qJ!9iTxq$}za~No^f^AH{^?h`_mPJ6FJO)AbLnpss4Hh}TWm3498yTV zQx|pH*1S5Dw*UW{I`6oi_c#21!ZAWfiDZ4aGspD6^8isZ_Rx5e=nn zq%w0*85xnXvWkxFD0}vM-p=>;`2D_reIEz)`Mlq+*FCQ5y04otnrmj|8+ibVgnyjI zpckAu^h>68xxWf5-FckF9@o?q+v*(H!k`6x*%Z8kvR=vzs6-l?7y!~WZpPcrUAWMM zkXHmea3{vasEjJ*vVHIq{7=Y3zOVHk>_0w+&5%7>SXucYX=&Ip>^4$Bss|6R18wCw3KTfZh29J36(4@(>Mr zhse*xM&(6CjfVgH&=xR99E`{L_#FZAz|OuYNIh~Tb@A(^u$)4%Ec!qvPqmvi+U{-~*ydl3~#``a~ z=#=>)lr{-PCl~d##y*G*8i_#ZNH_wPRE*}Fi`tzwrJAcLO(}DZA_1Ltb=Swc{dA8- zUQDtAb=;LDAA=!{d&-J5T3!p-UtvE+H@!)fBiIUh z74!M?b4P!ev6CMQuGbq%1RG6njE-iF%J?lr!&exK08k6QS>syTRlAtZz;m6>43IePR)sUJELj;65E!@y^D#ge@w2rl?k!UkBL3!bi?C(G>>ja=g3VT}hE11Y z<^1lZ%6_v#_x)x6(xnhB)FQ9W6t6;3ynMarGINqS15hA zyeph9DFFGMBOr-&P>Vs13b%X+2gGZ6cLpu4)8$FDpv$5_Dk%>CtBi`^YSnv!p5WPZ z$&)1#< zMorBMG+ZFgi`0>KVl0`49fO>#sUim)2sGk+zV3N^JG%juKLrL>z06?o7~~T@4u8qH zMku(%IlmL5-H)H!#?;g_2heN3<%RzDw3=!QwO>?Oxf@1&JNIrYVNEsB>7v#1(rwYv z)&OCSr2Ibp`gN=S_5EN`P|jJhX*dV*MtQmJkOi;1(imht7um{s@Ku-xJwP{a>$S;! zOijC^{8f$o_t~?NSkHImqinF%)nVy;QEBPs*#>=OCTBfhC|uFB!TtOF)Ab(`kuU9; zm9z6!(2s5WrtJ`x|AD1Io}P%h$!FaOvE2Z^0!_Wr!uj{rZ{IqiLAM3MyU1}1x7FQd z{}!}i3u4FQ#?b+%8JKbKgs(8_MKgF`b#nLxpq zrn#4ln^lM9N?-JXBE#Z)n1kF zW9|g=D6R1^(p4RQtM=o^?#O#w(g$B`h_ubh({rcjD^;teELvwfXVi0wJlUX&g=Kr% zY!G?N`d>d$J%;|zE(=g?H4~=)PqxpS7Z_G{df3~aBVgC!ufjXuN0lai^zc!;K1|cm z(9jU`RGJh(32dT!0voQPM?P_OcNqWWH@JaijTlp7T}kJ*MuvI81zXfNx-XYqhEh1w zz>w`XQw6%qsD#k#L-Vty;E6;X`K`mZJ;A9e-IYyJW#IiL(t%23mS< ztPi>>VL_O@67Gf!Xu+)nbr*RT^R3Fwn{UNXpQ{IPB!eSpjxG7`^6iB9CNd3L@3yD3nB+O02wk_XHPi!vTW4y;eR1*c zwrp5DjGo8hAH2J#tXlPjSS~tuZViw|TSffOF`N)oLc4`vWX$Pk$+KPY@ndrH^1@S7 zQ*&2Zxp%-=po6J@l$FoPlP9-Rz}V~N_dLRsutXr@#+?|Qwu}tzRCJXMi>}I-Vxs+@ zP>?>qeXt82H`l4UmK1pCtDPgeaYG6@6o%R%_pSLa*u_Y7!*%;qe4Cu2DdL=-x7}P_ z&3VxDs?c-R;8?@Q@2zAx1r5-an3!9>OCGQaLh1&V!c05W7}C)$2<0kY;Yv}5O=l=S5|Edmi; z0CrtCH27^Do=DX^ew@-`{2wv{^q4q(=j6hJuJ3a~bY-$V?Hboj_VQvyP8+!o;p z_M=%(7h>>+qJNLx*%~FNd>lw^o|L`U$_S*V;LFNAoi(azD6;E8ICwFTkdW+paNi=$ zMn?b0u)NKH*|LxY1V-q9h8f2;QhT89)6MCV*$aW+83qX-K70s7@u!hy@+Ia?WnP`~ zqpxP{-bNnL6k6Uy>y5v1?x+zDWG=2ZE6&rOZokWXhs;Z(s4e1BUimU`XfJV6S^4X0 z*vI!N9@$Rd%oD#gGUKY#?y-m#xw7gj4oY=q$;Jj?uBttXLeogl0 zFEwG(iO_=G(p25f8h6=aE33R1pg5ed4`Nj^5Q`Ka>e{s0wgZXQyWymV$snU2&H8%^ z&nJWDOaL0^#bxc_jdzhbIU65SJ~4U}kl0pKxgEkUbw_m~mxW-^@3eNNHY$DkZCjV| zpUgt2T9~ay_17WN?wQsw7bmAxbb~jXEjzL3umyJm&Amy*Qiah!XFeQF6}2jl3s=~d zQ~Dg28jt2W<=e)pAc21+&=HzykuT@h*s8IEfH?=2D#RS#G5=asx9TTzQ(4`SqdMn3 z;G~Gifh5)f4!H(h4lzT;--32t^1SYf#)ta1Iq0__DCkLf%VJhr&^o~)x2kl}wTH`1 zNKL))+|>HAeV5@4vAe)cm7+FswprXXlD%k8YUVohqEutyWpj$CEU!Fet8Z_Tbk6~N z2$Oy-Tj}=o>t|#X2X#CO;6uhEla_s~@F>@6{|`A^m&Q?^o`DeC$SqO-jkeL}tmdY`__aklz`6FJz2z76r(IkG&&nL)<$D%t?gv}|$x1ta zxY=Gbbofx7sjM8YQ=1}&_J{EoM)|0kk&z)nFh*GgJbvn=b>KSwWTgIn?q2>cyEOsv z!_{V0-qpAqVVPvjC%r`ih6PzKCKqe*zNt?1w%$RqDbA>Lo_KiZZ`Im1joO%69?HpQ ze93fYWZZ-iBBZRV$kz%_V0Z>f++U@|J61$d{FgZwPNy+BgQ#FKr2rMx;fxUVAc;(9 z5vUKr8N%4DMPchZC-B6vW9_9d!DGv}dR`|ienqqc#JPrTTjMubO%CigVeEh=z{Vg@ z*N551do#~30Rbzfi{DP`9q)*|^Y0stu|J~;ZmO)jZCqzN@mxj^FquU=@M`@i5{tkU z#jr0w#kLWi9~3tI%92vj=d4)@r6kgRh7W90{Nj2BBG(g;6~4^^5!#)YZt+Mja5p-O zHNZOHHBpSHUM*IGIFX>mx8UqtMxZza3Ye$Q6}>cdd`rgK&SQ{N;V=*C(2Ao!=xEQ~ zMxwlfyyG+}jcX$AD2#0X zo%;F5uXh(#JaB4s|H0jg<$snAeaUwDM{C2(g8u#U^Zj^ml9@cRFus9Fpm!X@PsHcs zzPTSvRg73!T+OUJhkaAVZKq~ng0eH7P9u!$bHsRL3!`fzNQ1qG9P>ll0;M---s4q^ zj4Z6F6XXnw6*|6wKoc|3AEEY}C2<~LWBT|_RrhUj_~)seJ(o8o(MtsO_0;;4;$7 z?#t6Y%IkKW%#zY8{$@lgWA24D9X2{+W`GgLfxpLY`I~tlT4~!WqE+&Izn3CvbR*-;TN9V0R8d}tUpmkP<>f>)TFX+ zvJD0Wyv;J=r++Z}*FIwbJEhSoexz^mfwyQEozYkfd)1kqBaw$;Z@0BtM@{(>F%RzI zZcNfVOi-BX?A)?L-*vc8RR(5Mw=;TsYUt>G7)VaIg*hZ!My&R~`NiNFjP_aB&K@^r zdT&SOQ^m=esa4qGlEFoY$ZH4~sm%^N} zc^Dm5cpVKCs0cSk$!Z;^#D}sC=q7EuW4`RAmD@+BB}tHLnO5-;O@Y)ADEty}RiVxm zEGo-5`P-molm7ZV>{rQ;~mVC58cGPRq=@u{^C|8=^`gRmC zf!p9PN=k8^5+8N3MF0#&d?d0DmzgVJA9wWkQ&B2_)u=wW4Gi?EtMvOhM?>N%-o+N z-iezQjfJR@cuST%G-od_!)|%;{{(3iE`M>&8*vGyPKESk9Qf8Wv4T4bQA1c13@tx- zSK%$!FQh(H;|@tZ(U~c>AQ)jNGT=C4bY#`Gg}v1P7foA|Kydvu={s;>D!IyQ(jx>o z_o)1>?(&%|6*CB<6%#ws^$5IDYWJb)Sseh}sHmyFzFX*VKhi|p(o|m!dcu#K&qWw> z>*|#&x(eOaO{t{ps_&y8Xr?fpbb5lj%kWFQz;N&O_zV5D=fJ|iz$DVLooBR(MeEr>>?}{_-9N$q*YHeHJ_>@89n}`{EN0f`l6yQNuXNwRF<^Efxc2*rM-s|E3ns z@7l_oKc$u1_=ES&7(P3E?)b|3pRtN9nVFdzTvzO(tEdh<{sB6o;>8jQ1g~TB5~JJ> zk3oyiy2tCkF|VZ7c!Rr;uo*Ymz`-Q*Xv{f0;MsKs;Q14=(^5ZQX2fpZoSX*lwADuM zVwOO*kmFMlf;j?%bTdy)$1TZJHh5sTq=VS*)JSVj&kop6Wt^HrZ-wdqd4OD_xFZ;v zQ56c&C9+C@1H~%v&DxB>sai32=mq4ML0uyJdAt2%jbFpO5e$oSbI(H|A?v?)vJFffOqZw ziY(YOD}TrT)dCd!DGL~wvh`sl1?VX%pSBz!%nq6;zI^-U-a!x8 zb-ehMpczrubLZ>}kKdmhnuaL4NbK}TIupRJ0zZdw#4RWrY5PUlu1530% z$buGy1j)=e4LE`Z5ACb0$n!Rix2^p`96^{O!(ERd{wi!t+y;E@HM3)y0X6j$^FUDRbtoZoStqdG=$dHp`HhHe>McC=K+T5HnBN@+e!&h(a9tl%iC#a+!J2q~@ z3hr40b3TIl0c;U^pz`rL>|>qsd9=N~j!Kv%$eL=~z07G)33O{<&d5W2?flo<(Yzw| za@*t(TWW?d8ZXS~V*(77V=c_w_CCPtl2LO~ggR7QryQ8MJR87~1yd#F>O=4#WX(i* zRPcnq{Ap;mBO7G`o`9xV8JMiJv~8J{6*|0f#%gqQ>S}AX!2}zalX~~j2#!S+oQ5#A zsA^ssH-z`n@Az|)hZ?*5u5$-6mvxA=(%FSJmDYYM(I^k^OI%s4czfLt;FMKVq)=7c zKMhcB)=V2TrR373^qe=mt?gjS>6w`~2R>S6i7jJS@{d1b^-2kFoY$$slYd>Q)78;g zqi|ZZ=$O@4diT*hwMMJ3cC#S#>rw9oVv2>$I ztz=&(-IeSFv86@NyO#JdB>)F{fIS_Ka7ihw-KN}Q#jOtyTwef~yP@-+nz&oAH$*-4 z<^uQ+9-#=BVAKoY5#CN&NWCeB?czcs%qB=z^evX8oF%s53)2AO1(B>%STXa|@SXOg zE$pjBX@facB*0?rcB7Gzk&&`h78S->atldMWN8Qql$Pz-G5gM;#Q9yuU0YWF^Robu zWV418LW(m)cIqjW$A$I_Sn$YF1zFs)n!=GfU2WQ_hfH6K5!Z$dSrx&^9R+g$#_if| zYTXEw0L)Lx#4K`)b3gvRxLf2{KqVrmV{+|7_c!x33jIr~$XksPY-<0VHLs>bok*8N zqrGB*M*!h2IVI&|%6zloy8%l4AzV2;b}cR&G)D$MgodDEaOVEgr-!kw$=N33=>_U$ zI|ql2pzJ6HmC0=sd%8aD_m^G&ZlYKa7QKEw8--?oKhL_Hwv80-jO^gz*|V#u9$Zsp zz;7#~oj?CwS-(AJaE%`77j}FZu-ay}L7v{=!MhaKK}lu??*SdT;!<`w5}lZfhey56 z?V0847*?+XN9Rb~BVtqr`u;J*;N4)9=4Xh?ja%pp_~jq9neDiL6+NldT~IJq+YSL4wo=ZdMZ@H7&b|;}4itxZ zCqhe~dF&cs-9cPz0*+7kMiqQFM#qDy-I&d1gS1rWhO=(@Er?S4^h|60diXg%;va9W z4^OHbzhKa*eH>2@&oTOH+o*5;z;DBOPhcHGsb#lsr{aRYX|{psKd1=u9M4^-35*Vm z8_b^QtnBP`WVj%(MxcgIpFFVy`pcz2&#$@Iws@Wj7peydK7VR?1de!`@DfT1ctbg1 z@)$Chx=mLl?0tpJ{PGz7V%yCZGH-rU8jvCr^HS@`mrK5T%*)=+E|GedqRVFr7D=h|H*^{j!ww&Y(3Z{`^;MU| z-DBax&zcqN%uAm?^_Wf&oK@NN>j^M0A+rqv#r3cpEh-MaYMPo}uY!9{Y8_Fx0p{*gvtMU8WB>wcyPztJ7(W+-zmwT1l2m-C*j@ z@O8)RB!B8JHeY!4hZD?CaSdnh*v3zvdyN@+;Cb7VKz6!Z;cpD#Lv!>aIT+~cuWui! z&4E|~m{qw=jWLa&uHRaZ&Dy`;Mlj3q_IqkSecCV6h5DPr!xJ&VX&qLm4MfC&OUcUW z*-p){3!j$DJ_CUOI9F80ws(A?%_KT~CU1GL&#C$wt)iyzbou7T`5H;>kV*^db}~M^ zZxA6X5R#I?w|g9f%0M;s;y@LvE~n2KR_c%JAVf-^7GvM+ZHVJ)0%2%7MUmgknKv(P z?Pg$T_%d_HyYE`a#vNJ|UMKZo5WAWNv5jId;4>LGlEoEcAa06!w@~`>ls?fBUT4J@Ix>ggW>nD*b!#mYb+R;8OEP+F(k5}ebxX^Y}2D!kNN>);|j=ij2 z{}(LLAT7tdO{)v5wovm|Znm`QGT;$+>x)j|!F@?d7x5LuLGkYsAG!ov)y6e!;|wnD zM@>!SQ|EwF4f*GJ<;OurmSIs}#=v#-dPjkSm_DWr; zQqU^|fd+m0Y$c>l8HFF()V`I41#I+9?^fjfOJhI zLGQ-8ASK!BE0fOsu|X{>FHZ($Ih;g`zxvCv6?rDhLcK3S&y)1rv)7^uONC%}-@7jk z40;=cGC^)5#E6x?S{WgbR!!Crjr+O7$wlp^nLx!*gD+4raY{GBmFV`09mP!ImY2(E zCZL9A=Au`iEzsCWFEhyyEdZ^u4K3sc#(K*5a|0S>B*(G9v2{U`Yiu8UnE(dI8!0oG=NFH!U|VY@H5v2$lIK%onaPpOUs7Tm6#Q-!{0GCHy0ATXeDAwj2z9G zj^W#?%EE5`#P{0<(-9z|h)$)l6P%g0;$q%UPzhnDV9eY7tMRK3a~j}TXK5CsX3SV| zl{;E|Z%rnZ4dUmB&#N)bonjr9E6@;Pb-YztiH;g851Ptp<70AE_Z_;1NJ&9#7rYeu zy(nKxafW*P2CV`pW`HLm2OwvO%mD0h*1_hCQ_(|+K7a;U1lC+o`2{qjz@suBBd)Yj zQIzPdXh>uXo_F*gaw-BWT#FbL^tiVvCZ-+odD-U6%tzt<`&!6B#ghV8ED=Oeu)cq$ zt{ftzCvCQ8Kx?8QMi@&|Ojd+?&jW9VAKpjaJ%$He$PyCPqT1?^xN>{YMOm>zGhR(@ zqx+s_9oApASrV>T5e_3KgBjV2H0 zuK2kmpw}J=VltBPOY`(A$2-pQOuyWgJHMO8?iE)5`bTccWpXAg%G`({Eyp7h1 z89qK1483s*P468G*f$|q-w?j-15+nuOu*thWGxpPAwt`*1*p|s=pFTSb=Ls|801ZQ zy17#kp&=!(bl0{$dmL!HqeHV|ny63$xbBFW);<(CMz7yr70a`5pI{=u%9N( zA3sG;q)4OTmtT}){9=^l;XMu8+@LSB?b_OQ){(CaFUh^mo><^DXE605+vCC~&Fj2* zBu!C&VEzh?QKopqxL^hgP8`lZwBd;Ag?g{QT;oC!ET54AVOZvL8d0$UqDJZd+3qFP zy~l|aRZp5d1R{&<)F`YlJz&?rCm14i@%t7@uxuN9+3jNSI@2o3PBks9(G6CwLTjw9 z)8b2Ww#iy@nD16r-ekZmoiYbWea~O2(a*frbCKOT>~wjn%Y4b-w>FOOze>;ioQtN$ z5|mBn=+u*FbDhBk_teddj*7a@P!1Wx;q9bi#!FSJvMD80pV7b;TaKF0D;D}qr=PLR zYEGVPu7KsTeLWvz89PW!VRMhW%4@2JG)Zdpsx!4U z*UWBRD>0{^qggUm*LC5%L0Zx;!vdE$+>Tx4q@N6o=7stD;zf%j9zXBEP{L~+m#jx`~)$<1NRc#Rj zx&FOkIfvLiV~ZQrDK$)YdTDBfB-m}Y85zr*mOaC**O4jKHY*eBKZo=@cH6$h(8l!^`udeZHH&D8cbb58pIWUYw$KU%*sr!pHBc%#lV0MJru3flQL zg}uf34;^Jkpvh%*_ptG74fM*2~Y zB+rUYoKS?G-8CH0)sBt6Hlkw6mOqK3^MN9GojthNef#uDgrfeqeWz(Xs3Whc9J$J_ zK>;EgD*H8=oH!w25a1XpG$U9g8&q+O-Z$p%scbAL zcfMymi_wcUnZ%mI!Qp$>_}5PhF%Q_&@J85G7eIszhrs=$*VwcWU_y_V?FF#ic{DpI z5P_E;1)Ka3MH&#pe0WLak4%naEcdptwyrqwhDdxJRNRh25XH=;M~~uveS2jBHkF7x z!|UqisIfd@`NhCCTj_hk3#)LgUHcrU-Sor?sHynTO~-YiR@2t@xq0X zFEpMm_twv+e($aQ04bCI_P9$^lr{iK{&6AU%8*;j?dXOCK9d`*kW9iuQN0mX`)W)< z&rVue{#s`#<3?h6+m$Xs7y*vlW!<{8W5;$tc$(AlX^ffYF;JTe@AW2b+*hl`d{NH_ z;f@q&K$hv$Yt?%#zSc)8hgj6glTts#Mu_MIJC9H3HT&Ty&;4)M>u#5OwQ8R0rV%4B zhi$QV$r4pX-G>i9p2p7qT0h+(v@ymImr6<^P$temv=Qi;Xrdaf-?#5J_+i_zW4Ftg zQhK-DLl(|Su{>1c$d6wQf$6*LT(TZT!gWZl;^xvz6u+=`)z>Yl(kel>)JpQhM7GM* zKTX;TpmvicL^>bL!yQ{{_V0>uPVJyvV&%@=yT@`T{dmTbte3ody!y*Gbll;S@;P@G zzd5@t)1xd@-&}S3DdpTb$Foe@U%q-Z1tDUkUaF*q=l~iuYIFvF zTp-m3VTEUTP_;N~9j<+D=&#f!kvAv5cAZ64k5})%E@O?GH(NJUYp9G-f0`g+mYPbSJL(J<1pPsYlb0!g9h72BM&B*;IhGj>$y{rWoO zRx*f8U>3oc&}qz=!gSfc^>Qt5R(!3*OC4pc>U5u?`g(gx8=a(9i(|nP&8c;hGc!j4 zzV2rj%_}K?xK)8|8@eG~2a0tck{h%A?okEhy*hs+UZ z@11b4KO*ZXY;*elplydf5d1fhAxgo_YT2 zM8>}T`|INO>s7EMuRQ2N)XJ|+fo!83w!;E~JZ4Zaz}0p$#*g8XKIH|pt}(gCEX!6@ zF~P*YGL04Vucou^I8FQH?&$FPYH@K$`_Qkmmh$AY^MZh$<=DVnY;39^qHq&-7-~O^ zU0pXM3|e0`zO)C!-AjIc%ezv^SY9&k8HTVw{zpiAw=Ldn=r7whUQjEksj6B~PieHO zh-%d-diuwoUmgb@uU3=P#VotwPvuE0li>;zv8FwcC&8Y$G6aHhCgwA(F*wh;bFb4B z&YBftMvqR0@&f(q0saqkmt|O792-_Q7+WeAPuPR!~(?Lf~@3m6k3m%6>3QribsjvuJ|k8jE6ymrbVss)X}l$BLfVqWC$H&j!p z2~rukNsBAzd)n~C09+xr0O^*GHP77A1qTgnmQyKj8gcivF;N!#89ZsT%VtJKMCkYK zeW;}OByf|Q++1)}OCCfj<(=)H*~gSq%#X*(s$Y5Bv|1PPqm)G&NkNB?bL4CTL;p)m zz>^JKZGY_F@F|9#LeNcGCFR@Ls_ufAa+|%kuYyW*Tx!v3!_)dvm(9fJ1m457`qEU{ zO@uao^#1YY8C!<2d?5*0x0}9)`%)mIPC^Hf4~wQU9;6)<^nT1gyQ<%R?avhG;^7g> z#g>c9rfUtJ|9dAY?}x?im-6H6`EgcU09hx3LMQ*$Z4#U)-%(u)un)H)VsB6lLh?R* zXAuBDo;Qdo#fFOBEgDkLBPTm^=8OX3gbDODgo@lQ|3->KDk?#1gq2c&)|AYe%RKIk zJBPFZ?1df>nFJOKAo`Rx@uv>b+=?WRP8msX5@Ygb!lHCRsuT)_8|k|th9c|x_vy15 z+6!*Vn@%VZ$JW$f7&l!dj8Xh^Dhcrg zp)QblOmT*W&-guSU}~zaNZ7ZpAygW^O^hsRa;5q7BM^;D_Vv{r=5K#|JDwz#pcul< zVYby3wTjphA?Q&k$R0LO(c;m74xA+x7ppHMs3Ac(S5~GEU3U?h@woE3jAnk)hs?E}-Prpc41Uo-aHbc$#chKo9>8)=mcenHCb}nlC|Y60cQ; z>tt^N2xs1MU-h~XW^ppf1P+4f(Wkqg@tu~P;vzx?=aeP6XsfsQ=U;?bnau19_wo<0 zCF%#+N&sFXCc+yvO))dgE5Dc7j1J~l@T+#$_Wl_O(;xzUrW0*=qVO;cH8f)F4=!a( z6JEGIe=T$}D^u#IP;{7UXEnmr>AFTg-_}TmDe@i@QhAZBV^DKi;>(oTFRkb{)+Eb@6J-d{fa2nKT`NVin7!Y+ER0Y-tt|A8iVh z3FdjzeN+8ZDmY(n?-7i`e_*z#48kZKxV`Av`xmM4E4JOU(dRBD10M4bJnmH7q>U9$ z#h(ia+>54jKLJqrBMq=My+!q&lZKi5vM?#w6ROh5&{?nL(&h{h5c6Q6+jK!s)=fd$ zFmN75Y(Y{I|4~bRJP-|GC|ds!RwV%3M!x#~Oj#@%RO7M>iBVMa?fi~rWq zJ(#V;~TBMQtS+`WDV<_ zxi!08-J-vZcV_Z2S&9b4GgN_Wg*##xJOg2x;j^y8=hWVLl~=xjnkkXDLsE}lZh`<9 zd~Vc+BmG*eWhX0;$74ua9L4HiFHoF8$Ap;C0>@fBePresOo|N(9%-4`*)0(zFsLOX zA#iI5f!A!`zI~9PoqO*VYtdN98qaaWaWJ{n#BmvRWOg~muW}aZ^|gdXHdA{hP0;*w zE6usv4?r=~jG41${qVH3uc7l>KRbI_P#0J~@l9jh4MQaAm3y7^fq;|>dsnwyPh=wm zND{;s;SBI1VhKXS)~}6n@G1de3e~m@oy^M>!}WmLYHKE_6c8P;ewBt9Hi^HnAu(EF z^+)>s($dm{Wp#We1q&gMyWUe0BQipFHF!QwDr;f1$(n2#o0vEUAXK)tBbh=L_=LMu zJ;@i!kQELhg?oN0yCZPDzUjs;g*AbF*eWQ0z>9C+*S9Hy#mUuC>RV9-Ve)GKV`$3M zx!i6GGM2xqhu1Z__2vxz9K%FMX6Aa$y_?e=wWczNOnBNpntPF_iW*;}j{Hn(FRxv9 zenCpfG8LkQ$hO6G+bzLrHrj0QzPXVyN&}Im{A4KL?Vd{wGe+{|anwTbBGv~Nvm_M# z;I9%&&XbW-7EGeHK`ri$Z=>n2h@K<$)lki8NcVz-DgX~MQDgF)X52pT`|T2jMvc~K z&_&Mz1Kn^DNbow)=;o>X70mbrftn_F9g$};Q%mYEWqA}g8cEhVvJfg!&$|(ILHMwx zwKnM1YUy_MnosRCG{AL%(KKsrzSYE^}abK0z(OJj#_R1SW2ddm}5E}-3M`7sBASL29{PC_T5}50NEKd}>XBtWY>p|!9Rv0ME>A_?nAX<5-Im_w^ ztea!~>v|@lhN55O=UZ}`YneasI$Eel<^fFKqQ5<*;L_TX*H>@cIDGEcOHL#E;DoPdRP@$~PU;nBK4pyz=0k7eM2vp>C!@x@ z;BWI7OJZff2z&{)E$K)LmBM7U-OtnTW#uRuMWs`){CfycEyd&}Ef*}IE;tGK}E75#4{g_I{1JY5|Y)`a_F7j>!ZVaBd4 zF?!K=D|rdcR+V>)VcvH%Vi)1yA?9f2{A_=nEd2&J)J*Y)?KO^XxE5Ra0d0OhT9?by z;p4bZ=wWQkX1*+HibyW`%P&@jzY2{*-kO1#Sx~X)ef|Yk3p~*H{^{i%sg+0KV1r4c zcEteVkztlrbYp6c^St>pRr3z{6f0BfF&8u1XV7Zz_8YX!RLOe5-;#h=Wz>dEL59wq z+0imA-sIOpv?sD~?mpWM5vZhpx4g8IR#G{?`>3Vcn?&Co|Mf%@zskh5Ya7Crh|TZl z9lezly`hzBA6;(NqD7PmHh=^!+FFsuwo!S4jCo5i6Vbk*8nF@v{27Q@X9GO)sifh4h-cWo`2 zp+QSO^^~D%PI0YnH-*?XI({>z(m}@RJPiscaW8d@SlLo_@8eYj`;U4^+3m3-Av&z! z(zcS<*+Z*)GEI9vQiEK47(4@TGWFhZ-B54Yt1h#nR9rHKDxw0U7Zh$08rijrP7SUU zzc8se`Q-tgZUdSs7+X9zc8H;2()B-^tTuP@d!CwG#iV&&o;7+UuV zDI?B|+E;yrV_nWbPv@NljQ%T~>G9?eL>nU|jD0sDaEVQE_`#1EQtrVMo*`r4)0P&yVPFy?zif&zFm2Pi&jJbsflM^}=p zX5Gt8cf1$g6k`j9Hda|J=6r|rzFOC;l(2Ry-FN^CdD1@^jraO=zOkIPQ74uydhxed zw@LdUstD3V?-t!w+=v+xQ_@vOGRBU9b2~HoxSo2w8vaL?35eA|_z9ZT;1&D1yM+%Q zPCR#n7p3Z+Wa-kT^bTc%xkF!61-^}&nDJmnTOBAw}M1DQo4fY?$7dby#d9%-j^XG4Q ze&-g7JqUxT?n%qg9;ki;zh5mLfz*-=Go=MBt+U}2#H~1?<#(@RN7rd{fw9S(swTJT zN@qPh)xlv`{}J3vp0^4o7bhLNp-ZR!rc~jJYzWv4=dY6)Xd-iFSz~;@ToN^$$BKAm z%7snJmRU77oN6c&WX_f1=e#%xmB(=Z=9fxmL=(vrs|~8KVXr2__L5b^bX5#e#k&_B zI>}Tv%}8cRPo2Jk+laGd1PcPBnxShE<5p-z#{HCB-!?6|Oi~x0aH_j15(NVV!rRJj zJw8tOg^89H7W2s8vd0`>f>n@g)MB+SD~uFpX!Ckczox}Tg-jdIaqsKu#3hcj&_pzZ zz!p3^rN@OCmNrvtR>J|aDJEX4mtpEM>tM<&#+Lf`@BjGiTiI^yjXpz0 zC+0a2jbuoNZ$%hAgViR{2C3e@V~!4Smi(ar&5#sTwEkU_ls!Ff{$3#E$zY)V8=Yei zX@Uc@iZ}1r=ysnPFPo=Q|0cz@(o7_zq<+#hJ7$g^J4LmDlA#S1qi{Fjt+tP;4fwE~ zRqgbZEzx1~VpGfhn2z}id=@vW71Qu*D3WB1f-U4B$245pK6CQ&ihu@{#dfm68P!|cdN2yjFoT@^*WH+(TSt?ajAS^JJ1Z*mW9 z;Fpr9XVP^$Wi^vZ0K+Wy!=#WPE~hx;%lxuZ0+D=Fl+nI|Hp|B~B#RQ)940IfRW+Sw zrQ7UTtrfDWhV{%AbZLQ0Wtj(6L^ptas?4bS_uQP7iYGo(D1g1rGGB9tPjqZTFL*NW zj&SNjaX27zHwi0j(_?5RVDDxE#ktbbRsd#wOXo(h6|Ww}sT65c)~qXkawX#fKd zXKMnb`V9}9nmh1up_Vg$)IDhl!5%ZAb@W``97{%+lr~>zSlHV%Cmj*%nZiQLe=c=d z-Ky#qs_Gf{at(Mol550;=V)e<=A8v&;-$-Iw2H$F!lo%)6YR1Y6CNai{jhm1vZ1jJv5PlV@q#u9) zQnEJ4MscF={_Bq?fyYf3DA$AmNQ}-U0p5r<@({h*Zg73ArK8kYk_>-bWQ`k!Mj5b{zEe5CKlCDSS6 zivc*-z?|Bam1(^Mv0k#&@Z}ZbkiA=aP3K#UJH5;dAS`3UZFgOvJpiLic0by%#C8`GY>CYA zic6$b`vZONbwoDSDy&T#wCU?O)%lLz$7>cG`_D=^7s#<)I~{gpip44cP)a0{MK!ON zYikO@cmr)c6Bj;@&#ZRY*kY` z%!9y+p&w(AIOAQ&SIElnI@Zf@7%q67GM-x z5{R}Yg}o^kIOt*r0Cgf4fU{Yv=Z*widITENFB73?1S5rdH~i&!lqYDjv!Uyuh`>Qj z6p~TIah=ZQP??jXwK>vs5KqaGC{&7TfKg>pv3T=~>@%N%8W&i=T@xbte*)RS}8=HDV{>zXj_;vSoTMUjAD0L}2K!x`Np`v1yJWl52 zY-Y`R-D7DE1(P*tzPRcrA*HKM?Rj&OF``Y`1d8kp%{g)Vpou%r4(| zN`Hm^Ofx=;2o=cVKI849S+}^CoJ@h@wqzKhGe!_Bcoc4%zU%4gUiAEU+kr)oFq=0i zce|HF-+f4LWv$R3Jov;pQ&?s_UQPq^p`8z|`H5OkX#Z24M}$--eQ8_Pgus?J_?!5 z>2;l_3a5imL2uLx!>EQe=sbUuGJw?o2`!7rE6#v%mkJB_xtn|@)M`>YF4`KmcJ100 zZW(D2z(M}k6O=@vr+&>~cLA*OPGD!|M335hCSk-`jalQ}e(<7q2|ax?oq9!;no;s$ zq^`mDAGPl7VQU^mFpI^YuwI>NUO}mI>A{0Nm~p0LIa)h}uU{{rf}&itro?wH1))%W zBAm$n_dDhB`lYHEUvG(-pk5MLXVyd~iL=2NND7Vabr??1o7icL#3=$g@Q;{Db%XhgYv|1g3vM z^B6d{o_itVF%o-;FP93ItC#gaSWB3^ghBK=i^L)`>!U{@@wS?Goou~3!bG(umpU;~Iors2Fpf+D8PWn(w$ zfsgikb}FmK3l|tjKUZw#D?(gglI`~jC}#YKpweygadMe`Nq;at#3u*B9XUGl*oJ=| zZ2D;d9>pRHqFC@~-*{|db-%BHaYzc5tHE?wfYhQmPFq?3ORaO~iK*)*k~e5??b)9x z?7s{KP$pX+IR3`%&}AMYX{n6+Y}C?u+RcXuXKV=lxb&ubb=+ssPJd)|!98)=#=RUD zxR!i{RbYBjvN0}9(^g3BOj$~_XiNxVB$t9)jHEH9vpr=JNQ1Ylzuy|N-xQE4!qxQe zH(W37gtThT)W*Ev;9^3)(SuNzy`NM%znf|`w59a$P^+46(#kC_vFb6qLkae=GG~+9KXG? zk+w_KPohr%eu_WksQD>|Dn)E8nBiDM!-=;`qJ2=d#jRz_uZ;+aD8-|r9gkj|K$d)Z z9WDh9t`>T;3t%zmT4XlwEC9u#S|33MGQ4%w>&$Dk_+Z9RSmeYa06&4*WH?>ye(0_e z_w9S{`MDRHLdo2RIV3-rNg)aRHb8(yUGb^FEiLU2!)FN=)_-a1h`S-8hzrOb7+I!x z5^O{G1I#}-Wfc#*u|O6I^gLKaz^@;R1+}A?5T|G^E3{eykW6Y1mqd#VC1z<(+ASfO zSa26kI2Ry~9HXRQR#P^JvoS5j0>vGw3&7)}o-^6f`{A|R1v+o+ZM(qn!F?3CHN=$0d xM=M{Q|6>sX1u2h=|7-on?;puec70s0G^uD=)sRKGn-%=e&f3xHfW_oB{|B!P+ztQ$ literal 0 HcmV?d00001 diff --git a/examples/iterated-majority/run_benchmarks.py b/examples/iterated-majority/run_benchmarks.py new file mode 100755 index 0000000..f2543df --- /dev/null +++ b/examples/iterated-majority/run_benchmarks.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +import os +import shutil +import subprocess +import sys +import time +import csv +import matplotlib.pyplot as plt + +# Constants +COMMANDS = [ + "schaeppert -vv -f dot nfa-{n}.dot iterate tmp/", + # "schaeppert -f dot nfa-{n}.dot iterate tmp/", + #"shepherd -vv -f dot nfa-{n}.dot", + "shepherd -f dot nfa-{n}.dot", +] +TIMEOUT = 60 # seconds +TMP_DIR = "tmp" +LOGFILE_TEMPLATE = "log_{cmd_idx}_n{n}.txt" + +def ensure_empty_tmp(): + if os.path.exists(TMP_DIR): + shutil.rmtree(TMP_DIR) + os.makedirs(TMP_DIR) + +def run_command(cmd, logfile, timeout): + start = time.time() + try: + proc = subprocess.run( + cmd, + shell=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + timeout=timeout + ) + elapsed = time.time() - start + with open(logfile, 'wb') as f: + f.write(b'=== STDOUT ===\n') + f.write(proc.stdout) + f.write(b'\n=== STDERR ===\n') + f.write(proc.stderr) + return elapsed + except subprocess.TimeoutExpired as e: + with open(logfile, 'wb') as f: + f.write(b'=== STDOUT ===\n') + f.write((e.stdout or b'')) + f.write(b'\n=== STDERR ===\n') + f.write((e.stderr or b'')) + f.write(b'\n=== TIMEOUT ===\n') + return None + +def main(): + if len(sys.argv) != 2: + print(f"Usage: {sys.argv[0]} N", file=sys.stderr) + sys.exit(1) + try: + N = int(sys.argv[1]) + except ValueError: + print("N must be an integer", file=sys.stderr) + sys.exit(1) + + ensure_empty_tmp() + results = [] + for n in range(1, N + 1): + row = {'n': n} + for cmd_idx, cmd_template in enumerate(COMMANDS): + cmd = cmd_template.format(n=n) + logfile = LOGFILE_TEMPLATE.format(cmd_idx=cmd_idx, n=n) + print(f"Running command {cmd_idx+1} for n={n}: {cmd_template}") + t = run_command(cmd, logfile, TIMEOUT) + if t is None: + break + row[f'cmd{cmd_idx+1}_time'] = t + else: + results.append(row) + continue + break + + # Write CSV to stdout + fieldnames = ['n'] + [f'cmd{i+1}_time' for i in range(len(COMMANDS))] + writer = csv.DictWriter(sys.stdout, fieldnames=fieldnames) + writer.writeheader() + for row in results: + writer.writerow(row) + + # Plotting + ns = [row['n'] for row in results] + for cmd_idx, cmd_template in enumerate(COMMANDS): + times = [row.get(f'cmd{cmd_idx+1}_time') for row in results] + plt.plot(ns, times, label=cmd_template) + plt.xlabel('n') + plt.ylabel('Wallclock time (s)') + plt.legend() + plt.title('Command Running Times') + plt.grid(True) + plt.tight_layout() + plt.savefig("benchmark_results.png") + plt.show() + +if __name__ == '__main__': + main()