From 3616626a91adda7c7ab815aa176b95873cb0f778 Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:03:34 +0500 Subject: [PATCH 1/6] Add `tla/.gitignore` Copy from https://github.com/tlaplus/Examples/blob/37236893f14527b4fc9f3963891eb2316c3de62e/.gitignore. --- tla/.gitignore | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 tla/.gitignore diff --git a/tla/.gitignore b/tla/.gitignore new file mode 100644 index 0000000..c53ad62 --- /dev/null +++ b/tla/.gitignore @@ -0,0 +1,50 @@ +## Ignore all files by default +* + +## Don't ignore TLA+ files +!*.tla + +## Don't ignore TLC model config and results +!*.cfg +!*.out ## Usually .out files are small + +## Don't ignore Toolbox model metadata +!*.launch + +## Don't ignore Toolbox spec metadata +!.project +!*.prefs + +## Don't ignore PDFs +!*.pdf + +## Don't ignore all folders +!*/ + +## Ignore TLAPS cache folder +## See https://github.com/tlaplus/tlapm/issues/16 +__tlacache__ +.tlacache + +## Don't ignore CI files +!.github/** + +## Don't ignore READMEs +!*.md + +## Ignore Python artifacts +__pycache__ +pyvenv.cfg + +## Ignore directories used for local CI testing +deps/ +tree-sitter-tlaplus/ + +# Ignore TTrace specs +*_TTrace_*.tla + +## Ignore tools/ folder created by .devcontainer.json +tools/ + +# Ignore directory created by Apalache +_apalache-out From 50d7458b6e57c11ffeb0b17550469b137bd8479f Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:05:38 +0500 Subject: [PATCH 2/6] Don't ignore Graphviz `*.dot` files --- tla/.gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tla/.gitignore b/tla/.gitignore index c53ad62..3c62655 100644 --- a/tla/.gitignore +++ b/tla/.gitignore @@ -48,3 +48,6 @@ tools/ # Ignore directory created by Apalache _apalache-out + +## Don't ignore Graphviz files +!*.dot From 1d9fa5d245fe1a11d87c0e554c36cb6341e6d5d3 Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:06:02 +0500 Subject: [PATCH 3/6] Add SPIN state machine TLA+ specification --- tla/spin/spin.cfg | 3 +++ tla/spin/spin.dot | 23 +++++++++++++++++++++++ tla/spin/spin.tla | 23 +++++++++++++++++++++++ 3 files changed, 49 insertions(+) create mode 100644 tla/spin/spin.cfg create mode 100644 tla/spin/spin.dot create mode 100644 tla/spin/spin.tla diff --git a/tla/spin/spin.cfg b/tla/spin/spin.cfg new file mode 100644 index 0000000..5ee969c --- /dev/null +++ b/tla/spin/spin.cfg @@ -0,0 +1,3 @@ +PROPERTY AlwaysValidState + +SPECIFICATION Spec diff --git a/tla/spin/spin.dot b/tla/spin/spin.dot new file mode 100644 index 0000000..3afbc17 --- /dev/null +++ b/tla/spin/spin.dot @@ -0,0 +1,23 @@ +strict digraph DiskGraph { +node [shape=box,style=rounded] +edge [colorscheme="paired12"] +nodesep=0.35; +subgraph cluster_graph { +color="white"; +-8857019723714639812 [label="state = \"operational\"",style = filled] +-8857019723714639812 -> 4466091959303920822 [label="",color="2",fontcolor="2"]; +4466091959303920822 [label="state = \"fastChainFinalityProved\"",tooltip="state = \"fastChainFinalityProved\""]; +-8857019723714639812 -> 5376352793141087770 [label="",color="2",fontcolor="2"]; +5376352793141087770 [label="state = \"fastChainFinalityNotProved\"",tooltip="state = \"fastChainFinalityNotProved\""]; +4466091959303920822 -> -8857019723714639812 [label="",color="2",fontcolor="2"]; +5376352793141087770 -> -3097599280067440227 [label="",color="2",fontcolor="2"]; +-3097599280067440227 [label="state = \"recovery\"",tooltip="state = \"recovery\""]; +-3097599280067440227 -> -1367225398818136591 [label="",color="2",fontcolor="2"]; +-1367225398818136591 [label="state = \"recoveryEnded\"",tooltip="state = \"recoveryEnded\""]; +-1367225398818136591 -> -8857019723714639812 [label="",color="2",fontcolor="2"]; +{rank = same; -8857019723714639812;} +{rank = same; 4466091959303920822;5376352793141087770;} +{rank = same; -3097599280067440227;} +{rank = same; -1367225398818136591;} +} +} \ No newline at end of file diff --git a/tla/spin/spin.tla b/tla/spin/spin.tla new file mode 100644 index 0000000..3c98d71 --- /dev/null +++ b/tla/spin/spin.tla @@ -0,0 +1,23 @@ +---- MODULE spin ---- +VARIABLE state + +ValidState == state \in {"operational", "recovery", "fastChainFinalityProved", "fastChainFinalityNotProved", "recoveryEnded"} + +AlwaysValidState == [] ValidState + +Init == state = "operational" + +Trans(a, b) == + /\ state = a + /\ state' = b + +Next == + \/ Trans("operational", "fastChainFinalityProved") + \/ Trans("operational", "fastChainFinalityNotProved") + \/ Trans("fastChainFinalityProved", "operational") + \/ Trans("fastChainFinalityNotProved", "recovery") + \/ Trans("recovery", "recoveryEnded") + \/ Trans("recoveryEnded", "operational") + +Spec == Init /\ [][Next]_state +==== From e737cf3aab50c37d85aad5f886192e7587c18b8b Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:07:17 +0500 Subject: [PATCH 4/6] Vscode settings for TLA+ --- .vscode/settings.json | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 .vscode/settings.json diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..3374f75 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,8 @@ +{ + "tlaplus.tlc.modelChecker.options": "-dump dot,colorize ${modelName}.dot -deadlock", + "[tlaplus]": { + "editor.codeActionsOnSave": { + "source": "explicit" + } + } +} From 448101c1cac8f3cb27f2b3d7d972e78479c86afb Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:15:10 +0500 Subject: [PATCH 5/6] Add `spin.pdf` --- tla/spin/spin.pdf | Bin 0 -> 93558 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 tla/spin/spin.pdf diff --git a/tla/spin/spin.pdf b/tla/spin/spin.pdf new file mode 100644 index 0000000000000000000000000000000000000000..6965ed1db4e95c054d67207838eb1280e309bdc5 GIT binary patch literal 93558 zcma%>Q*$i-c1~>Dwrv|H#*Xcr*tTukwr!hpr)IvYshaz6`>Fc}^mJ7w>@O@c5F4y9-TY6ZLRAcvm@oPi`rvtpbvV^*BTM)RVSrB)S zLT=zuu90MwOU7KHrx+)W{m{e&j?hS%EV~o`&0HJ>%uG|b2(Zrk|elO3&BJW|2D6 z3Vph1qa+rXR1BdYKWAD}I&nisd*ZJ+8R)uXU_VNvMDl9rL@`ElVkb1SWT=W^8;s0# z(Jzm-HCgipw|g6xJ4RMRzTz%Bbh8?hVG-6;h4Gpds87H**_tfK&3>$!nqpbT9)T(S ztzU`GUqXapnir!+B_5c^7gvuPt?Ma!__fHVU>k|K)o<96&rUsU*~U6gy>e_A?zuOO z{B_vYgL({hL+qBiN;Ki?zQ}idEBz2*A&pp?(x--JOs%KE9whu_LUx3L(${vV@2^=` z+uoV?t7g4gt`PNWk9cL5r?#;rvm+m*BIThf6#;@QvGDK%+u2mF<-R6#VKG zPkgYhrQ(~(J;M1NBxSt~K8%^Y>Hq!gf3^SpcV_ng@AynaOl+*I|G@w=5eF9w*MHW3 zVd6iPh?9$r?SIOLm?lWpEMHXiSR!keKtt$=9Xz+P2L!J(QW2dhc7)*l-Q$B4 z5Ly!&9NODEkdIGbmyZt!n5}InBO2aET#)}X*2M{e2npGbn37{qpkgb#7}7;bd59>` z65k#WKnSQe9IUqtjF3>!KThGxfn-4rBo9h>kO+uQ-=7-=*pnK0VO|OJoKpbF51Gx6)E>ka8$OT#!>_>kPvlQFROlNi z78nF+ww@rA1J(e6A!LvUF!w}87bOE42T-v8*Pp<>o3Tv~Bpk4yAX^7$za<0^%E@zJ z!B)DT_>(~AQ`fM5KMv@x>=U;cX{d0Jg>~#m!FJTI8U^GN2=HBm9o)CqZ*JoF z9H?EtJbXCd`p<2sp+RuVVE=Y6!DX~xlI;wrACtzg0-ymO;{stH5TG&|pbKy}pdbE$ zxlQnouz$a;?=7%?2AD;#eK#%0Wdc(OUY`MZ0jq z_t{^Mk;Y+=q~@;Z!Y<-#Mp1{f}h2EZ`8M+jPi^B;4e|# z@9^6%lHd$u+p9s6&bwEhy@n91XD3qlZ*hj;udX2-CD_USSFb)B+L;^q5z@<@pE>kj zjZjY^;toc%wS9%@FDs6ZZU;v!kcudmuPE*6u&DrqJYQ|refGr0O zgy&JZpOLxE?2lWNBqT$!qt^#$s3;&odwU{>z|G8Fv4K|MwryporAtIBQ2#C{vI}-F z$ITjnK7@1eyU&ziF<`+ths9h;IH0C)$nP3NsCUdGNTB@RzyTnlD}y_Bj2{L{1R(BT z$Q^qSq<02NFrbca*d6u#dj^k8m~Y6hTK#?kd;8YGHo3?fu!K8)S?w2ixLq#` z%p_``Y*C?0VJv}QvoH(CI{`hO4fdh2WrD6Qa~}jYSdp?)4YvUWbK5Y7?^oWb>ELIC zwd1~aYLupag8UeNRjNLP)`7D|WJY{3QBt;<@$#i>-JB8gWvoD(*Y5M2^rIOGD^P58 zx<`V=Ns9OHWu zq9bAoF=HV0j)Nua7A8+9FOeB^CoK_`RS{=k?o!kAPe0V3il${ch{|nQhN4)%Lt^>G z9seuQm?5g795Wd$~Bas_2S#??Uv%>H+^KO zH@o96HmqdUS{m%@kmGV&nj0H5nOxF6M&Wli!22M!A^pb;OIQiWy%1^x3NDjbO_<6;+sBK0gPlD>h*4(Bk)K^_BoW2iMV?& zS=Mdn>`w1#Yx2idslPLqBFk=sbyT!dd#|Q+2lLy;0UW;=Nr$e<6>SaVVFET;uSMpG z5l-R34%dtZpc#QR4pe?6scOIBl8ch}X6?(l6_zwyw=w~4W5>`cwa64G)Y}q z{b!fdL06h4nAySKdrcQ9GV;&a<$`=9Mv;_2b?hvFiL_88CGE$gcXoTO(NUeeBlWci z4`R3ap*zBJ9n|C5e}#rzF_d?5SS89$yX!?}cq!^usE)B1`F%$fkr+kV{7=MmjAqu& zQBz1R@k;r?+o?F=0KhVLPN{}pNr7U4j^YS;t(5@wD;koJ`8m(`wwRtf*7mV>i=+p<08ip~ zeZ4>t4kl~K%`AZsYL*@Cb`aKFbeu+jLP=IrP#*{y;(We{WFEm;xs%pe;Zo64cvYIn ztR3aT<(Tuy0`g*JLhNAAiX1;ex$;?e*nqe`<-7Y>4*8-gy7grj6NXEejazN*=VDS% z{fj3T`>&FX$I%v5-eEhLHYAKK$D*U5k@O=HxmB;XXqvE$pE~Kd0d1!=xd2YQS2b1V zob1<=l|}^Lq6mA7MJ*n!`(4YbF$}(YSpL@!V05J0?>-O7X7aaY`OWuM@yw z%iw0mEu#k}#kyc|ZEF~c<%C&&y@DH$=3c-z^0m^zJK&R*NtuSt%EW15)-5u|65hJJ z>-gc7A#9LYL}s{a#?uw90`?s;>*BVHAH(-xRj}9v9$-GBIu090I7QmF6i>6VPu)0f zwujt%wMkAv7Qj}=b8(pD>>P(TyvS=*F)TX10B^QsW=GeXdO35Z2ql6lUtco8M*(zo zoBn3C3ffsePk8_3plz9^4!XPUS~aetgkA0kg0%*Rca_}8RsqdxiK9-)2xr!Sk~D(T zRq8&5{g1xXqiH%|a!9<2n$gRn#;*Ce;Gz9Juc3cE*Xh;hblh@wKl&C{6~l&CX}cRY zH@#|(qL%jN4ZlXZW!i`t5i^jI!xK$o7iImMm9of&dbD7B4I%~pwYJ6&Pnq#mqJG0}UR-Yl4Z3Y4*h}}x^Tj1sy@`3rV{gv= zOk(FaD=jQ>IATo^U(6XLyZdYz!D*!LUoHK83ysJlfrsO_Zl+oLSpEy>*j)xfy=gz8 zA7RmKnwR-AdJx7L2B#-ZioF@Q3vs^;X$y9BcbYqKE4J#X@x6dFfBE58)`x$-p$MCJ zc+6ek*qWOeSCDJ}V-*|u@6Fk%p>GCNAZf_P2O0+sX&4G=`QRr_HU_KfdtLO792@_- z*n;~^LY8rHzg^IZTWa68r4Zf3GZTpXpXmpbI!W!ucbD*fHVaEL!p6L z11M66$+5Er6NrCzRdzuJpTirZF{6be|MgGbz<83INmp~CXyP$)sSWskcM|H7XjZcj zQr>N8cpgW#t4omk)d#VFB&Ku{5CR8eP6zqZiSvsd!#Q6Hl*c za_!@&F&t{L!l~yxx6QlX-(zVTE=?VveDatl~NXXI8DS<6!V~HFnpnKSK2ss-mmm zj5wd+EfO&&uh6F5D>HGcZ%U(_vR7S_d@uHR~XFEfvc5e1J97S7c+sa4g* z85sCDqkR~6o$lzm*U_d{COKfUz6+(|e@Y4kjM2A@enh7^rI7V?gIPdLxLYTP@Xho4 zJU$-M(oNW}cVx}V1=ACGn3;5o-NLNLu4!#VO{FrHKV}rG`>rj`${(sG9)S_iBHj$x zRY3M%80y|jByAHQG_t+^RaPu7lvh+(i};iXVm+Q^!E0$UjzijPBZanRd~GH`OB5Ax zFU%{d)5q4ttyKR>=SMS%pc_fu8ssmE&j&a%sAMFxG&0QMFc868_-t^om zr1Z}H(IEIcD=K5+D*T64@P=D7=Ny^cPHbScN3lRVE{6UDx@fLj?iYS_CC?ht^%4%| z-aE#}+{+}#hQ zKbQ17nj4kR;;V1=I)zfWQs-3GHUZGgOYZ2F2(v)vTHCvgplns>898MZ<5yGE+1sET zZnN6*gYZOr!vC#nvlPWMGDCR@GH?)mrRyB%oK|s`P3g?^$_<7^CPeI@D6xqeWzD9s zb0!F2H-Est|J)7MvB#+DZGV{UuBzQ8>E8&x_5kn9HDSlzm)^ihQIkNn%C#SYoh=y( zC3J>Id;cSC^KJyT#Rs&APj!2X=`^1DZs%5HOdijKwbaO$8^nm8MY`FG4CBD!)Iet1 zu27gMo$cOaG=QiJos|G>fFZGfKTp*>Zy^-LK?`Wx&fsaA>JPrX>5^I3#UN*3!tA>k z*$6MYUEq)n|2FS38A8FO8FwQRwmW389JgAapAY|`&+p#2N7WBYbdA&%WhT+3I6 z2Ba{e=s}fC5*T4Ac=wzemhg;T^Y}dh&uusmGD@7ymj3zbo;REkvbWv+xyN zhErG!%$8h%=`YIb1Vyh*5C5QgSE7`M!1{I3Oar$Jj>mkJ7H^UFJw)w?>`!DhU@Omb z>}-R0o8e|t<>lTi+>2fDUsWQ`cMN&?O=;ri58wKb%v*vx}u)WGg0~QlCj`-U>2BWW8?d!&rCttEsZm zZHI`!vt1phRf=1?pLR1RqD7jq>LhV~)h`LI`ab+OvXfROP5PXwdUO;?mF!+I4jCcn zoqC+$GincX#R563g-b%kHqQ`r;%=9ItMb7zEj`e+DQZ#`kmLzHX73Guxfe=Z>KqFT z_`yYqAWkBYuWY&Q3M_rknV&om82`~r?-)i1tAkOncM|*hT9qN)d%{pp&YgJM&POpY)hG)CQi^eYokgp#88>_laD%t`6$gnt;~|Fkf3o ze|{YeE!h+NEB&PNCD+%LB!#KoKbnbyBqq8&>p-)`zin!aC{%mt)HLHV0%sbyS`G_X zUfb}q&91+VjJ4dn=zvR>!s%OzswCP|@XGQ_i|4EKNX_`efv@8`P`*~htF}S&c~HX` z;J^-XW`wic)+HDndvb1Lg{*{GxP}lAmYA4=yqjCao;Y$CW4xTs3S##Ns!hlyqx6vq zW{CWAphx6gl~y3}orLK7;PO3)07pjN;>3BaQU8_|mL|caqwyadkx%m&?~T z*iIn3ea8`fWGqlCy3A~GxbhR!EPrDHQ;XcLR>kEL@a7fl2W5BP97l0aCVhHcD!LK8 zp5566t(iLVAe|*QIxTPR%A3Pzjv!^X09v=7!eWQ$9=zbZNy}gUeZVcA_%~U8bCqU! zMBZyD>}0ygqx3IUeM2c4k#ieBY@+NwMnj#lFIZR>w zLT~c#qc9XO@1!@#W04ys9&f*h4}%m0KX+gx_|-z(+FlXl`Cu8U9vu>!suf+^wSC?i z`ssj*KBxM~7K+63MhuuyU2QX5I^5B%(ew5OhgpjU$NO$S^HNfN_`($ES{v277>X_( zyZKa$_E-LLaWRm`PdUdmy?Xw^4lS4EY3Qb{QUmY2g?bg_{!C?DX*Asb$BdCX#1i{Y zYIPvBgS-tHpBug;L&s6-i$XI$oK>OON%F#JZZm3NdEqV#oOivZXr}bh#A}o-cB7s8 z_Ji)<*Ht+kY!$(e_1tBBse)>2#VA+PMvnlXDzS$l(V(=^ZRV5g(UJu~7im}J<8JkZ zUosYd_oTy?x+64nY@!a`AO^#$V^J~?i`bTZOF`1o8;0qb7|l2jZVD$z?A9respNM5%D|9q%iyEl3A0vRAkIb!3`zNq<1W_vGp){qViIv$5+dS zwq&i|BE^X<`-?PD-Y1v*dW|^iHt~M9tvIy+GeZi=nRqX$CKVFN7&PE(gI82%Axu1H zHKg80yrJqLgOT8i?_a-0I=IUtRc>WsDvWc#*0d@9*GiJR1!?z1HjSgSz%j>2g9hiZ zD1T(G^Jfjt-oT(TrU5UW$huIJ8O_3|ruS}k&d_veg# zy*=Ltp_WB3m52NE@!_une8v8F)LNH=4A#Oa6+lpuy`{d+XyZi4W0!Ay?sqh!`-GQT zv=eD^i8%2c%3&}w*6sKHTb-j4L)1t|!hw%LKh^h(sl0U)Nrx`j=ulc-ej5vVZw+ep zytC*&pA!Z(K>lTKeX=n9kFRLjR@+m|>fYj84n~Bdu?6Zn2L)}RmFAU`O6OTgI^ahd z;nM;hk?l?_8*gTvcbDfRimaNT?$hKrZYiG?zz%w0&Mr;3WE1^rWV*d)3zmF_jQ6ZL5cRS z`d)gS6ff8Hu?I{h^gvOkUSWEw*|-)THzwa#7FATOvBBCxY|mbLNbclbostQ8@kDO$ z=I68wFd;7kyJC)hc$`TY+2R=@h^Fbnx#(s;KVCXKr=+B}E8)f5rfr&vORYiETlo22 zS-B)LN`G!YM!4%j3Ry%92vFnocogCLt-!=ege2L--f=0QOjBvxoWSp}&|}M=Wlv(v2^@Usj+NJB zOrP(tI+AGJvY(vDC=yeUMaJpeB-t0XvYITVHG^Ot5PJLp#ku)sR|F#U$V4|c&)FqB zMk<<-WTC&uuP@$;mCmSf^@#XpPq~lb{YcNN`=Z#dV-K3%%Fr-hnzI>sgO5C2?FoC7 zc$@9^p$<$z+ICh=zoWN6&s^Y3@fBaBCMJijHfMWJn%i^10%FJ-fNwD=eF+(wcq@oq zY-z-9Kklld`LBWk>lrGjdwH8uE7A-e;4Ce^n^d-nr(xqpz2o!2*Y{W|HKO*Jn(9>L zUJ~P3=ZPVqnbFQ*fQh8P`54+4cJNob3Vov@_T*ICN7>^cIpik3Uc&8y!o%}~%2MRT z<1!?tD2-)CMIN5(sAPhj7f2D=xxs`#v48Y>!?#SD{?N|9I?YPX@ZQtt7*wA~;n9Bk zlR;edxJ$i7;Mlv|z933rXf89Yo=x?r;R&wT0oG_;PJ?*F_UR1$U(`^3$tx~MaHzFc;2+{waC8--^Av@%u<&|))ES8*>2k}%&KbEsG&C!Y5}~sjaB5fQ zJoU*--PazOG?r3QRacEEvN4X%N3V1SvCRPt5j8 zS!9};8}L0+bA(MEA?J|6oB$$(GfVw>Q1ET$=;?~}Cd9}q^(^yXx9IA6;IHVcxGR)5ex?cU z@ACDO^u;Vq`Fs&h!Y`+L<-#{RHJSujgE-Q`jjJzC`n@XXjgj*U5#ne0Tq-MkEY~jC zDF~ll{WYaqss|Q$6>Lmj@erk$dh8udi7z9W=DWeOwq|wy**8q>piX^bbX+L{GlAS$ zK8rP0L^L?caCRBxKXY!#PA-iIRIX<>6!I*_vjK0e?=7#a-Akai)zmpA-7w!~pHF&v z-FoBt@!##e{Syk^nAOSJBG^aKbX?L*acV`Ymm5Z%R{O~%m@L;i6gT00;08OU$v<^B z=%EjKY9pBWm_?Hl5>4L$JehH(Px{M$|jpgwl+Bzitb(h8X9UrAAnX02UVjb@e^8rj!Uw zr1BWOO~H85A)_XM<9f7cLmhCd*M7`@B<;H2zs4F<2$GMwFEc)kCtsoGeioK9HXRrc8ROxk3`h3jS;k ziE=}e54O(g$gd@8*PAMmYl5WKJj0%4GcW+3`K=x&bkY(hsx)(dVcX7fZG^HzWo@4y zHQNMA`^j4vdFz04ji+{o<18C^8U43dV>`=|%@JWM*D;oTE*(ZVe;2;?QarAEM`QL@ zK^jdBzsZSAsfka$4d!Uea?yA4xp9P4K)Lx}n4Kw$bO4!u1>^;<7;1c9aU(7OhLDLP(c-k;a~`X(K`6oP`s80Bi*R z6yGHK08Pzn``zg}$3I0DB3f!*JQl=&o^nX16jUtS9$LKHA*6020zUYd zy(8&^Goxa@F~ZI7iGkA)I@<{*Te28OYy$KPk`0t(7^XpuYu)N8mC{zt+>yn58%b~o z-H&jc`)y*{j``ZrzJpL*J#2i|#lv8!D;q~L3__qKigW$p(_A{&dmZWuWcU=ZXuWiF zdp^M1a@Tf6YRz6jkf52WAAqaz2ePp)6wdD3arw`B-6zWq%l4>3@s0{ZU4L;Xy#@lr zt!Kb=P$>gsCE+oDu0_&3z8}45l1kPz4-EHFdh=9#z%o znMLrYOl3KoPj;+!(9E*EYZ4u8Mg|DeamyeiBn@3Ig8WI7n~0g`x-6e5!XWk89I4?1+o__!2!?-B5n_K-J!xfroo+c$C0pdE=dIaFL%^{>>=zZ*-o zi^c_2(VCB5>x_y_#MJRB{f>;-yh91%5Mz7?DRn-x=E}_AGvamsI3(NotF&d`Y6m8K z9W+=g&8Zhxu~ADVPv8G4M}YYYX&b8H``;Khod2D1!@|Y!AF+m+h>eSd=|AiLHE!5B zIa&V4#*I6;>Z0$aK;Y7U@y@CQgkxIV-5n-6acjgMd2>xXj7U$~ovNHhAST;ABf+MS7p?`<|jbI%X z5-k;MN+NiGe*sba)NZV06|ExvMT`p=4iu>CJS7-HUv=onn^D3Hy@zmiZ=9e$Cm|9o zDJl6I4PMznKp)AzBHA2Kq`Qy@67@j-ji3rEUPRyLHz{~+7c44P#z-6EeNa79+IX*FzKC-X&&(s=)DE25fBH`LEz9gds;#E9ls(ih@@g0={^)% zEYd-Uv#4P}@P(iXzHc5fM8L;&)$gVd(%Y%CzoF4x@4|Nkze2F+H%#cjz9k|Y+HsgD z7if0;4OCu2Ne|-=CIeJ(0p2Wr{tYK9F~J4AScixaSeQYzNI(Ylh#;lWfWYJao+cSY z9O?-1_N)aOmx4%}Iebzf&c+~Uz`!BU>32D4Jrw8u&bR0f?J9i8ixBu19T%}uto*47 zriQokKPY2x1bDluU$_3=ndTU@*g$*ijeI5Mt1q8CY&5Gz%EG z;T%>Tsu7$h(gL*58!*^j-VPKI!DR>(%$vfX067pAoQvqdy&%>Ab_B>5506lc;|Cq; zOPtsTNVO2yTR=eG<7}^d3s^8$fzl1&*X_627&%#|B4xu1#83PuRY?u~8Ws)-1r;17 zLfYToFusjdG13w0!y-pV@hF%7hg2Q%I2a;_g6B5XQOWQ1>KhWQ%MWV+^2>r*gcZ00 zis-gC!5%abs2|#3@0VrAFXZdj5Rh~1C-&jzUUYtZ^D{Z~xw-#aFTxjp1MuU8ntL8V zwKVkq6A%2nTZ0k4yTvBRNz%>xvsn=ohH{n{==?`e8;X`54&}F6;(#@w2WnJDl6UKv z!xnHkJp+9jD@tsi?==t%c8 zq@rfkwUr3CoyTf6kYt~p%wF)Wde6tLvO3)`D!cHE7x=X2F)WX5+)?mR2v_;LoQ|5p z>Dl6L#7l0Ndp$xX$1)EZ<)VhL&TNY~Pxr#PAumlXaY~?KpV8NA-MLfxcE^}xBYiI3 zgx%t-O=jZh{9ld^>>M)#-uy@jNWm4i8i30uAx!z;8@GEZtmjdI$rfdWah^6?Z^pb)h1=KAP@sM%-*L!~Z>W zQ-X`0f6BqO!^Zr(D8nE!`XT4QS(_)+Fkm&jkeUZ^a|*p9pD^z&fa~OlwiqxDk<6;#=nIbNRFhvh=Y=Xw{R70Gth|qX^z1LiWt$NU_TfTi1Oa?URB4UlSMI~iGwi`t&=#6us7h!s5!4N-`76UH`pE!Yen0@^vw zzn8%Mp}-wl7Zd?1*~xvnudZ}HDa4;i^hNY83r81#%K28boo0lYM}JiWhR;q5XOnNa zV|jvXg5@=})hkHN*9jN&qU&Xn)MHjIae_wacu069c-DhB{Hbd``n(XvnT~OkeES&Uu7$3vKEB&`X}~^0+B`y&>{EOc{os zsht{TQa_plbEl@$n_YsP#A4OcV7;2>s9fYlDVjt?%aB5 z?t!@S>SUg3|6t62wnep{26dME*0+%&J9giLYfC&I zu-!nrj}Lp2N8&qCwRG9GT0nr}%V~mqs_TgQ%&fJmEs$+F1PTb?|tHo83Q1W`>XzXya>rR8#6ct8p;rB{toA0j-FCM;GnMhY-KwO;5e}m5t z;s6sZJ0GK$_ij9|NW<+fbXq}p${#^&^{R&F=vAucZaQrRJHO_=pJBH^h)YZ2DBIjL z)P^uMQ1WBl&t`bUzHzM?x{ zfsf1xg_pHJTB1l&$oU3nr1gSmD?Kv{@BX1P_pj!6XGISqG=SN}gOTPXe0e;bg3nvm zqLL!T_k<+1fosu|n94tEp#D7M#5Sy0D_|tnnrYS9C_=b62o^*G~ls-(C*?{ZLW^%^J;Po#jscW|BrTIBnB4QnqB?*k3O zyCdq~kZ77o+cbD>9A(@@3L{!C9oZDB+K6U@9cddfARk8vj#Zg{Xyy>ly{il~;2k2};Or_!KN{o)B} zM1CUfRjs1&cZVqH3pUH(9Ax=+&n~IR>Ne{_5oC#RqCrmsg1cAKmDpjq!~gv7P^kW0 z!4X6Q+qIYfk$BDN@Kbq`%4yb3{VlRfR^0ZUU(Nh^PtJ=cmm{vp!sTKNz3hVjvA-Dk z!`P*(w|mUCdT?^X%TYlta>93CYGQg2rp5EubR`Q$}DCK2#l7 zCDSRi(#Wu~Hu)H#V=3Ge$%Z#$rOU}bOn?*t6;UQRG##Z*wBCSaQ~TPTnsn@3JUg0_ z)_fO*Aq6wZ8$Zze8dlj$m|&8+7cY0PFU zSxL!ctD3#&rNd026kzOq*dNqG));-!oh6nhl=O)#npsWA=5>*}7{hpZ&G#7*rP$7y zjT;q}6*rv=VH}L}Q)@d9Ibtv&7vwh4LuzG z410Lwt!)#)TTvu;@1whJIV7`TMC$VC#mge`6Kansm>CCe)0Mi`XHQ$N;Q~1Twup$L zgqPx2_&d;4Yk2iIccvPtbYSr$r@r3g9*8)7h5hV6Mb7pFugjuZsmsK+mMLg2uc$y( zqE~Y1+ep~$WAz?}^~rqqEpq_2Ie8!sM0aQKP@ku+VHSjo_A1M4o^w>qnyXdY-}eR%S`N1}XV$dx)G_ zPE?Na)}xFCzWh=&;W3+)%X7Oe_6m&2B;Yj1*m`XypthE89Cx7Vq!v2)b z9YR5GLOHi(jIG;zJl>w!AZV4Cv({xFR!L3kC-3P}*HMh^jJiq4yMA2O@Y~K$#NPBc zEgG#$`mTlsR}{FhsZpuDjV$AK_}C^^HM(9hy^%O_893x1jXQ8!(j(kJ8Q{lP|afXUGMI~Q75?g<@J5%Z%Irt_XQ+Xias+X^Vdt-9$2iKtBvUG9bNI{ zAknRS%^TIFl8s@UBEd-RNWo6o%k5Vip)sV<9O`}6XnT{0p02!9k@s?JSDPB0zNHgL z6iaMHKUDeFPZ-eLayzufx-O_dIj0j*@{KH4OXd7=`C}Le*{cDF%O`2fl2_tNcu~Cn zt^4G9EimcK--;=&GW^q!aP;6drMsy=vTSb7R=qGuOcm+?TXE|;3qAq-Jk~3<;8rnp z9rwz`N!#2x5vho5K-!__E^u_URF#zZE19@_^6gf5F(Evmn)ucC@lfqS4;OK{7(cVa zmP_vw4AkI*p`}&z>A~B3e#&{*t|c|Q=e|{;W|LzhIw#^kEz{Mq!To;HM=X&7CFpB} z{buXW3>0yu-<2e$O#GV{+3fp0Ewv}J?+@qUn)C^Lrmw{6fPJ`x&lV{g;844svCh9` z&p+%4>MX`I35${ zQmJm5Q>a;b_L@Ft40VzQms^ah`!F4|e%6kky{GH*;%c!T8svH}yK64ewJTKV){4T8?*3>0tmfm)mZi#F5jYdf}xB{l|95T{dc)@`2gZXLh zoFI%tN;`>6b!LIIR+^3wQCv|Hn>#C}vWcGSGynLEc1fM?XBNj`;+N5w^2Y8sbb#;9 zT4pI}Bt|OLUcsj3p|WI8prb*e(>GaDtr?)1-NDAH!a=Xm{M&Q89dt*87`4TgPY4eI zOFj6*35iEb$t3VID1}+0mEO+}zWPTvE1|axdmCBaB&q8DK`QjKwM`2Xmkx3*gpV@J z#mNm7^Y%);H#>bTnR@o><9>U3*p6)hS7D}$=ODvfPvJZqC5ag}wgggbZ8SrjEO^qX z;kw1Q%6X$88F|(wd5h=5W*_cJrc|_5`o+D5lroaP26n&ybtkGW{E58(h;&i8L}4pd zECuvrY(-poo@+2fW8k*;hFt4QnWTDH4l@Yb-n)5z)AUZnjrJPK^&t_~9;cz7+UeWL z89+lx_p+GeJoNlDvPbSZQJ=ZsoO;8%Rw1xCqG!rbr&Fu$sQ&rGSkCVve(vacm@Uw* z8`y0pjmw^P*HN0Sj7}Q(E4AF*ObBSCD zvr&H4yNark1qgNAu@m+g25tusCa<6R-0e&0W z(WRShICCTYslNf1g`@TlX}Oz!Ig5YW;e( zqza39pk9fMW?mOTig2z2*M5_u;3;Nj!QB9dT;=IiS)RxJ!XRx{h~@b4gGk*OJXJjj zr*V#F51yIhM13}$MP-Fob5?(HbhiX;JBnsx*CtBUUbQtB(FD!@6qY&Ua^ zdgKlBp5}7zMP57s5{<{hH64su>0>&*dSq?T1#I^iw#;wVY zz9Eqb47w!NE0d~x@-YOi#9;&DGz-m7#`}e@{b2DbV`Y=S1Cy#qRBj!qMh!ox8@!jZ zz}8CK2^sXI@1i6&6C4I1k+!>Ns7T7=f@W~R9u#jZtkU$MZm?-9Fa_3s7^K7!7=a7? zA}dOp@OJAywIrE&*w}-_rrmhUEmfa}L76qld_)LdxWJ&qz@&{!F$#)zW-CC=_h77` zBX~6~k)Ryd3{DiX2V2L1<6tlI(Wg_kGCj0ZmV=szUiq$?&gz;tCbIxwVBNb==$Inx zO%kufW=+-9H;EuGqiI|1*rrvS9Jbb4nnIqa@m1Ax|ewBSsnGr>{=o znPd>rT6f%(3A5`#T$lfaa(AA})cW5wq+l#`4Py^dqAhx}_+vSrH) zF%5tgQ@0*2PpTUnK3M<*mPXI5^b+&`J{4>!m1<8C!%396y1`hZ^klwY1PucA#?X;; zQNJ@t-%-07l^y{At-go1z7NBeyXz~OLBOaDK3g$_-Y$vIFQEH8BHol1lFsm%EDIP% zB;hc4R**Y({;d;a>oKQqG11FU56rcoL?d|?<$jY_J(!-Ff8RlPZAx9p(!k}i@y_As zJR{&p?x8gG9=ptNgwQ#$P=y*AZG;(+P!W9MBYG{FzW7+>^n6q&EQsX4v%L5Ll?Tjx zW=t9BU<)7X5ndvk-@Fx)4}8d!@@T6%S|H}O3FuUkbCvB#-b0?Nf|tMaGX^?0|TaW zlAbHFV|4W<{Fo#VC2RCr*U}*2C-E&<;5Vw4Wj$jnZhH-#*Q<8sruwOnf z#ieZManIl5O^V3`vx{1kdb;$rh8a~-TT3?I)t;zw`l@+ukCnHF_q{O7O__yjuFxs8ygY=|6ECp)2YYxR;?k8wD~ z9WT(m+Vt9>j$?YBG`A5#b&q#(HmaWJt6exDJ{=5jCzLk^k(WJNn0^+O+nDV30=kV) zY$cbPZ}yX7`Ce6=^&500b`GVzw>}vB(U>wSel@yzwAdU6o;ayEzOWX^@6zh~ha9(5 zS<%iGaq?Ej!rY6S6?cxp00FVLl!aFAqu+%xfk0`W1}sclDr~;JRR{Yo=535K>OA;T zgPv%e>PEtXwiHc`?iruxtVP}5xd!(JgsGqmGK zb351hJ;wk#CQ+;wbp_lcph}L-gS6MG0+1uW#}0K!AeXOJGM1?t9Zr67JRcoi&6?)$iHNLjUhX8n+HIyw&M2mk>jG+>?tU?4#5fCG#C zF^Lk406go#m*5Kep%p~?2<<|uogmQdNtXH%L)%a4hyw=GkO7cTefz#AaS0A#1chw- z9Rk2Gjv*XJwk)8-0G|+A6d)!(^$9sha1<%f8Tt6+<>mG28?otu&I!iHVekH7F2D{1 zc8CRFBk(s(1_9(Nn0H-FdO~V}UBrtQ>{a2lVxE2p2ms)|f)<1}?2$oSJ8(fDhIHU3 zl_fweI)pcSayB3K*&=aw%uuz|xM7y&L z8R}{Qo8yEzxr7cW*!#0zM}-m*v?uG`?|$wth&cO@uiwOL!uxJ7{L%H!?)%IE!n)gp zR1f|#3<&%D8NeW*2tYuA@FJi92lm`#|-hD1i6j z8^R3!Aw6~m@DKo@F5z#VKjjCzNQ4j|^}!oO0Bi{06ghYKXBZepzuF@#_>j*)8Gwvi zz<>e#{{Hzi3{QWB`wVw}Gk!1V^J^#eE z1poF9S_BvRFTBC)qqgw^5qxlKPceU|HjLr}IecNl$@TRbTM{u;hXQc?5VmtFKv+b- z2mH*c{2o928o$j_{9=#)aubTWV_cMDhB5kGTicmVJvhMGXNI^_Qe2x^~%N) z^oFbbJ5yKpANv|8s2EHT%r@YwTl0_(N}+B7w+)4qnnU}RuMt>3IZPO+a0}wC0{&H~ z0Pw}E-vvXl$rnU3*EU0ncWKamnVH@?m4Hp6E5A65-UJ4K7?GfENJiNa2_XP|1T(a2 z0=-@dn7zYLVg(FzfHEHc0A3);x5nZk0)Tv2B%4o&pmo2OKlu~8ZGF3Mw{SnD2qPQ< zI@^q~AJB*>pm&BZoBT`&eWyX1RCoTMC?Ma0zmTtWLN?op7^D~I%M7YNq`z7?2odN* zX%0pxhSYc$DtKD{Uvek4c0;T34ey9^ zu&(4Qt2JwHh+3PR$KrUkQ@eIr3(GqO#nWBYq(YY?X6A!=8o(G&`t8Fs8*LZF|76}P z@I1Y}O1gJRgu%mwOE7=dVyNajBYxNqK^=W&%{=n+V%}$ZR?Xh7NDK-YOUcGN3vBTA zoltkCl}NFkXeaP*^WCTtC(dR_PJKINowD6x`CCz{uw&^hE1k^q&I4#oNP&d>-L)mx zmZG4pCTbO8vQ|u4(G*QCoB+WSJX^)OGBv+|ht0mq)mxB_g6ru8f}$wtWyCO_*5D%M^%J!4X$>aTR}if* z^{g(Tp7?5LU5vD#yG=7}5Zq=i)WIz)jkUFdaJ^FE=p-k3m{;jN0- zRSoM*Z~E*0{1oqe^FC$V90U78!{m#pVR9den%#?NQv((OJxp@gm)FP`OAA(dHOqSx z5!ulcUzx{xmr{{YLM@GJ7d~a{;-;V8?S5Dckf8I|T^KV#eJqcyDsNWQk2Nb{ziBU- z&UXSs{kwi>y2~f+OMs~QtkAOP)PnNz zEE=Y)0Z_=*kEW8TF(!qZAMFvCGt=m5Fb4l{vvxajWK=5!!;t)zCSH1DnRF3NVayEb z7?HYj(9itmul`9Il_Vwojfi!7jum|x6;$l-%E2eVZKea}ez(EkPukDObE4vLVkhM1 zyiaJpJ!KrH2NN|^cf{k?a}#j3%xS1x>L0Waea-h9-AWbo*yg35;1X9UqN*DjoyMUsUqpIaNWnRX?;l~6 z-3F!=63B)&2PfHPex+&LC)qukVF5U3^eiFG!Wb$#e2fSFr!q5)ZkT#g1J-=!Z8)a7 z8ePOCq$dL=>1HmaifPZ*@1CceBHv-QEHn;r{igClucAatAfHX#(|u|l@o%H0uQpHz z*v#{d)BzfS$2*8q(T<;jNUYl?tmjv{88SPn(pjsXJqb=_&C;0o5SXVOWt`TcrL{rr zx8?xhFnZ|_)h1011M^+EUA0FNh3RZor8;!^ z66a20AeNnnR;ACWj!|-RQ5fi5`HIfpthSoWHj6!}CuRHo92M)@4QMHCxeIzP@_`A;qXoc{Z#RbGCw>ZL}Lb<3TWoQe&m#^_)tfa zQs-w_u`?$HSouT15>eOB=A?_cozq=r`H{ToEvt1Q!BI_9HT`&iikUF(OPd8Q*L}`4 zqB>*f`5-))x1{x&NayD;F4e7=yE7OE9sRsjFBj2^F(SkTpoH^L7}=|&(gbSbu_s0_ z#~0q~u$=fh`D#`ndud zykcRAZxvjxe&@!iNLN;Sxb7gvxd=miPU76#b4p+Z!MMnB)X3YEZ}^~N8%~1W7Y^_R zUE;*@H6=HdA))7}W-Wtx!F()WyeO)7OkWaOv(W-EZi>^nj3lKGS=zX4bb?DCP71f4iHJmtVF;wS>lFAVql)l=Jwg`vy^jnV*F|#V@_l(e?0aYf(krPwK|+IeZHUxrz`1Nh z32jR5a#JDnU-*|`GUC*{z;Rnk@U-54IsnmV+@}D?TkwcE^Ix#GynU_ubWXNTn`f`x z54X;q-mHpCHucWP>DUlMlL{ZUvG$;){!xh{PE)RjWBy7zS_pPbUFV;<*w#c1AACuz>u z_qM%`jhm+=j=1tNtW93?QNQQ&!m5;S$L=(%faGXuoLH`h8;4#sUiPokta>4+Mah?D z_jDPA$;|iKv2>afYq30ly04?hF7M35_hqp|D)jvbu2)Cg6d*J={$(;Vm!K_i3=!cB z>+VuQ+EfwmNEb0R!W+)&bV*HFu~6%KFG#J~=b3Ck&+}`HImw3nyhCYw5B8g+>ttkd z@Sw|tw*!?QQdFHSBN;fANFt-rpZ-|L7t+wFki4xb)8J%pHh!mAHfzEB;SF$F)aqtg z1@ec=F;9rqT|Du|le}oCui<0Y?Mx!hxC4HQB29ofr*UpRPLtT#>gfe%&mC;f*LkhK zJ8RtRha*be65Duff2Ba=OU}VDZlX`6<*QRHI1i7t4MQbB&9T@SA)V@%{Y=G$o(*_6 zw7hko%I*l6EWa#SCSmxS?Z*mOfl6du-lbb3iQjhR&F#|#%_D@-tCc$Wk>V3K2J_ob zf6S;8AMbws>G$2QArj5V#*r==Vn#BX$zVwpw9)SzbPh)Nb02If3WRKF&l?@ET|Z?# zK1|LKa&^|)3JDS;d5$O3m)u-QF^nE>KQonUhe|aSI8B7ViEr%<2}T)is`%#HYv`g! z$X7bVAmz6i5~C^b5kap2BK!}~X7ml1_h)jp= zvoSCq?pBQaR)K3zMAH1wu_AdGxoB_7Kyy}UQxjCS6G40(%vgaU%c%s+f^PM-Si?bC3;{$#OcueE{`L0ec` zmBuOQPyR~fgI4v5zd zXb^BNog{fM;$DqhW@v-@Wte;%R49YRy285Y6S{B#8`iiK{ug5O9{9>LoQfX_5it9Kvx9HK9o=dTS63Ul+hDga%vji%+V1%ItE(&7ENfz#NuaRsj9o9z4V3KG;#QP;25v7rCoEha2(^4@ zi@MzD@7{x~n#Esg9t@(-y+de_+2=@Ye zO=TugPuIbPH>UI1ee{p^C{ubi{MIgk^cqQ^@Z5D)y+Vw0^_o*V&YXO_8a0Nty|X~u z(^(qx&*Us_?JqY5NSBUq`&<}}8I%0HUfUcG(*WHW-GHg0ok6L}y3&^mP*=Ey6^%gW zp?<{bEY=*(H{!)9-&cHXds4+EX&x@^s^lfaG%EjAa9Zc|myLQ5qX9ei&K8kAf1$5y z*sl=CeurMb1Ho5F$E==~UgVCe9>!C8hJgshpA|+MPb@6X23>y&(c!6HKGc@u>3GzG zyK+1x{e3;7Wt&`emGA4C#jL<5Q8?LR;lxPw*55k$s#$mtu1M-kNL9LsJ)D4?yJSW} z(Vt?NKlZVC9e~^K+Dm3qVB}f2kkMP%1&y~J#=9oC7!&f>nhUcf?5=S%;D+KV5IobN7`5J@24ZCNQ9X^q4ta{J&+A|YyE9JayDf=hs+Z_iS*c2+)rJH9-lSK;HkbzoVnFUG2h z@1TtZSWqT`+d(X#VE1fa&!Bra-rd5Y`3-86Ch#~Ct;tCF4)gL^>-VbM?W+Ez3rE+# zfr67(3qLZAf}DlqWUiKUqxGfRN;tuk@@}TJE%-Li6ny;MUje7!MqYb_hjd8 z$9LuVsIvm-O`@UwYQHQl*A3jQO`XtT-W6O8zpdDB&NUXqCDYdsMk( zvfGcV>z--NJ9S?oY%-R`9$k+|QVwe8E4&M(Jjn(ULs&{#on(!)HI*Qjha?t1CyDu% z94%|et*Z8^kA0ODc3nj5PHt!!BmD-lJB|I3t91L8%bZ~)^1g_+u5&unxA=@c6k~*6 zuEK@ezVxllS9O)XKU?xieK{C&;s6ZKLkpMS$t;+^?W7af>3U{t`1@IZ_b+xY`b+)d zf*UA@?O5l%ERPBLg8AGrJSWHI&Q`8brC2#@e<$fTv(m94RVQ>*#r?(n!g7@h-H^uWA;iNwR^H+LTx}Ej3$k zSW;ou3?$l%^Af*6OoUvdp{pZND*t%5A1Cl#z_}mpxO8${I<8K5$w4&?P^D5=wuXQc z4AX1jcK9|C7ok9Ei4;7)IY1?H5;I;{wHTgsYNQ*cX1>}%BCZ#`qYn6?45ymK{28ab zXAg}b^U-wc)=p1Zwtna$e-w&qF^lSRqT+!@DfIBRMZkZ(l-y`C8c1^i9eP>6)|I>1 z{gt&~86`1_U5hL7Zux8nVU&k;?jgjAQwr`FJvHpd^^LfyHdj6gu*i$g-djKV(_V8y zjOt~g_--Wla)x;N!9L9dwCPyP?IrS618%`nV8nC3gIDLMBr;4w6Q-GD%|sZjE#vb*`Y^cuCxL$0^h)LEM(a@& z>=XHc1F$~ScdEDVMWTbgXkiJ&^7a*^>V7U}8sqqq)>`~EWvn1|O<0RkyIj6v=M~h393eSkeCiL zCbPNtn2+>APN$1TVW$eVNt*LzoE>KiMpq~*8eO!~w-5OQE-n&cQ-uaxqomU5ftu4q zr}ZCYXH0u-n~OcMR;(ekce{$2L)ik%`*i2xJ2hMC@j5vMf{$PoFOEUZN>;X0Mo(0R ziimQBOWHz+lx@F7{8={@%ViDB)^S_^Dt%96Gsots4p%;|n5-?+NMW*#X=q(tx1xy# zvGZ78k=@*^bS6nx!>O7Z&Y`noStoB1aVkW~k&$xjV6!nCaqdsfvFjdTh*%f&RdRC> zS$>OW%A}I6*=i)+TQu~9E=B#Gwv|5kBwizFsuO@2~P^T!0Y zHh3b~C09NLyYg`<3b$V#AcNZ>T@6K#hYsg7ev@4r_A=&d09H?N=CM)_yE$npHF03+ z?>j&lXV26DW#z@{$&kp8ZmYV4sY_e7*@S2|YljBGMk4eR?wOZz&5yqYz3{r4LN}^- zUeNQHeFIt&uzrFn&ulA357URK^G@4PnXAb$RFi7!I9FP3dOdAxr_KCO42ITvmH44m%022SRH+0QCd#)MrJD()qldZ zMvb$EzOr;K9z8l>H>~2%kFgjCbu-Fy zaQ|zaUfQ!9w|=$X0pHrU%5~jmMqIUN3bj%sl%DUZLWLF0ZvGWo)reo^$isE~MrPyB z8x*xqKWeG8xgx=!+pV{J-w(Tl#;MB3E$?K$23qXjF~0>2?XCp-3L4TcL19J%_c!40 zZQh)s487e^F0wa|uYUOt!?oM7UCT_rZC{G(iBplp^E6g;10~cwfivq z1OfUQIr<_vAVB}N82vhhbVdLl_1P&<2Vl_)V8R6xKm^F|$>q^0U~7|Hr1;YU;-uvO z_%Sjf-t6uJV2VdTFCoDI{|QWNK@eYxOfvuvVB12167>2Z1`Q9PMLH*$89lwZnSpi_ zxf{^6!E<&3-YS&P4nP9|baV{X0Q75y_5gDW`Lc^i2Y{Gs2qpT-Xx?9uaIc3331H$7 zpe1Agq3T0519b!}m;tk(t^iufC8+10sr1Kb1N7I04aiUb-Tg0hcq#OT)eya`(X3{w~B#A|?n;={q)eG1_9pcDJ<`vw6)F=PNS7q@jc z2x)W*F)Gjtb}yq?c;EAHMObcwuhf9)B8J z!Un3V{hJMrFNVsYgSk3|QjUHe1TrChTGj;;00bHO^*5Ub5dN(MdUCHun! z3GhGh0uyIM1KNAb-WwqxOd!1o|NWJH+$H?Q?({c(=ZE;of2L^T;`kEd^y~ix2IUsQ z<@p^@^l=p}YO4birv!M(ul-2icTx@35Y)x}MOGCGQp8FKT<7@uL@I;;{R2KE1sv7X z^evpq@3yTEG<4sv%QK0XI^aG%`|z^8|S6A1-au<;10F{lgSH=T^%M-J{N5ah23 z`IET5usjS}TD6-jj{8~nZI38SfQKL*)Na{!Tx`%;xp(pig$d@K7ppif-v|4RB8PX& znU1z9ZL}pa^YGMXny#EV6ezba?CKeZeC~N-eY+h7-$odFpCzl#$3JbafcbR}1)P^udt5%KaX+>;v z+3o#EuF1)D8cdUt0T857la~?ETai!iD91y$S2k@UKr9tnj#k0;Jtein)Z^Hl)FSM1 z){g)-bS6FFgFpNk%O4orvk27Z9R5MH`$eNc@GNrAO#JL z#BMB14V9bMG@7cR6HD>xXR4k^3P(;VL*ey%MC{06i*D9X{+Whwe(+jdDDEXPCrZQE znX{^xsj$!ONTA*5p!jD4z8Sp9PL06UwNApT$HxX+O^7gFL^=IK?iXlpY+<;!)lcUn zhd!od-;3#fjIDT+MO+c}B%q*Rdgv_a=FQ#9#QTB7HXSy%KJmI@k0Zl338mb(F@eLZ zYr|JE+F;8ZWH;S8Ht}Dg=F3ZXP+3PoDsvC}=W~%_-Fjm^4U}Wcdp_)!WmGg0IqZ8` zvs7~Q+){;W}>?{L&nD=yL}-kTdcK^FIf*OT%> zO_>`dZgp$X!Wew1MS(Wi#}9A?s)oSs9gnh-tsB^^$hWx^+?6?EzCeye$}P}PW9C?w zU+Yh*apU(oekU3oY4nsh>%2Bc0J_~$Cb!ikiM&Evh#Nb8 zwfYJISS`gv9IL2GCRTKi7bS2qjST)l{lY~^J8SfYVg(qE`~{W9j!IOlhHgI3fyavU zz65iDAjS_7PF;GpGOpTRiCF+Wk9vy_+l8`>p~o6oPBW$(jW^^li^Jv%g8q94q~%29 zTGTB~I=87pv|(=e$IRWkqg@g7R#x{YF(gi>X-m7N{1-pF!b!@m?cFEeCCBcO=I zhnt5BP5wfPM=0m$)gjdC%W~0<4lKYA+{lO0$>4oLk1xuC=#u9RPQ7`U1y| z#!o!R9tUxp4{2jNW*g?o77E6R;E+jmQpp&rSe2-?Ncnyx2Zg&%& zv^W8hI~J{$dH3Jcx$u~F&~;G!O)(xs_R{sW5H`+EZYx}KOB3<(un&mK9eQWcG5f^~ zW46oA!1$}6+*a#ZeC}79Dj2j>5i+ltykKTK=Ot0=f8`?^)lN+S);y18VrJuIP&ru zZ!xlI?WJR|h-q%RTv9+E1Jo;ei5?p2VF-W3sm#L{p<EAK3ief zSTnHIb>zxQ8r8sPn&FSK+=D8SyiQydl`o+~be;kkOU5&!rY+|Ntc#=@dTlLTYsgu7 zv|}N6otCkbpa`4Vs&_?qQKg@!5OL0^n@-AkC?*XiiX%zVnC`8Z-k!-No*XiL;5+FW zw0~mM1Oy@F)V&Wx@>UKHgZB5vSC>b5$j~>ft;e$E`^F&E!PdauEx5 zW*453CsG=*rpBT#CkG8qzt!{}3_(_6$f>)zAad8&WBPqsRe3mbZ#Z-vVDi45iXkiJ z&>1#HN3`)GmgwuQyg6i!5Jb0bDMzvU9+}Bow>!9|=xX_761&`WP@Yg(rMWI5cHm#u z8X5U4z{OZJpXntuM%SWZkXmr8xMl@*lqd9BBtaDE{h zPn-z_(2LL7_+d}CQ*czVjz2*;cC;e;A_rv!MDYXf=Awtfz|Yg_Q08?{NS=L_@Ybju zXe)+xvbe3-ci@lay2C+IWgvX~CZfLP*v3S+{eAbs(_x7!W;558&1AjaS{Q#4epNw{ z^a3fYb+&p*^z9|0rOu|n=aw|h<6XqzIScrqm~QI#Y=nr9P&O!eC3XoxE`nnJb`|HQ z8OvfhZ+F=3*aeM}bmmC}-RyGa9JB7V?Uva#ics%v#&R?nw5c~)bW8+AfLsSx#f!aV z?#uGQU#2)$W@4ImvK~nIFNZbt_DHv#PtH%pir0`rqsWYV!V zax~>YO41O)6od^QwUtMz(+CDNf8DLD$7Pz)P+>foE-4z-cnt7DT z)3#mC$b1<8$eBv>)@yyYUvK@81p^|nyj^l2KEF&wrkO`^dx~D})d*&;BxEkyJ1u@~ zP7iy^^_*9jeP;$X*7bzc+bt$h>EJw zv=s5qxVJ}v-+I~~!AP8%NzUE{--G@Io6({ok9+BD({7Nc6_HpnpnrnAZCzx(;dgD9 zWG~g1G(347(<&Ewd}{FVwgErd$2t*g@yvF;I+qOo!%e7P5Z>z8X+Pvl68GT&P&d5k zfxAsaxkL=d9YugG+RC=;k1~WhPPNQ7dX~mZgSkDWZ_eM6D(?ngV|-hx#X5PP6+Uh>Tvyr z8h0B+&B9}^z64BF-GP-XN*3=ML(F#G#|j|)d$hQ*W9q$XZCr$79*8bCzUSIVDmRY6 zUM@qDaDs3@_}0iHt(GeC(aq%EC>g~$1dV3xqH6{+@G{zLz^_A@%UNw3Gd_Nrk#j~5 ztkv@Iy;;+QPyTIp!CpmNl{45Gna$ns?Ym&mJ*>dvegUFayQrwArlDk)UCrL8W7VaqRSBD-3cA!Je*cNo(cmH$}>*z)0=|UWLBBLGU;2 z^h*EhSJk0BE=NH>*@Z)h_NKGzKx-@-Wj@Cx%lxu};y@tckGJUIl0W1d2C%6mUS?3C zsT$*xeq+W5Z*OK)NFWicN*riC3{%g4+t+7!6v$R0@TXlQeMauDa}c<@hpK+>wRFd? z3U_9h@lX-C=D&JHl)nMXj|;&5JLEJm0YJ8N1r%zm_l6gv7!wPMm-cb3r;rtB(%JYT zxyjznWqHcn`Vy9p%>yN8GIMR)YJdy3tfy-d2E4MbY_1{3j}O<&cR&+Cuz#B`AFyUb zJT|VgajGO6B310p+d;qenzXGXayf@!=_a~~FZS6D$jO)d{Ch-szS%at+l_|o_*F!h z3k@d#)r76)do0x|B%*9~9RzNho%+vs-!s`A-*0ieLbRN_S8V{fh9 zMw;i}<{U>e3`gfH_Iz!dS3|qn>x0Tt$q>ZC&WuUER^{N%Z#`m~rJfiQhcK#juavWb zM|82YB z_te$gZACqu+z1^?AOU(8^li?>Gdruuh`Ozn%7tF7f*R^yjg zS|^OI!@hrwSr}Xx$sVf*1*b(<>&hBwh;IzQ!rPdz4CWSn)`;VkJQjv8%ZM`t=^E8W zOT@p<1bvKb0o=$vGYh`6AG_jT-Q=u}y$h6=54kLp1HI%Q=zA}oxX_5FQUl8PDqe3j zCk5xCp0$ZTzKR6?Xz5p^FywOu(B5`W(uO(@6R`{N4+U>cJkAi?mt%2Y39Xt3NJy*Isj8D-og9*;N;=meFoZQVmp(y~JFQ-P%5NGWgFj z8g^;qiQh3O8}G45q{=VQ=+(6z&ls$tJ*E%7a|-*k>%bw+t=T*JUXF{;bfQ|0;l#Zs zk6>W$Oxb0aj|!!O`}a9dw+vkrXmp zt;5Q}K5-4{v$KSi-Hzoq#4XHTjdz7Iae5q+Ru+d)z-JkmKQ+>*XHa)~i%o?ZhwXyv zGBW)Zh0d}mmY!I>+br@*KI=<(KPDFh7TM5qd7h2j`t+ja02%0O{o>@EFm!vmafA_r z+;h;L+w1knN?Kdu8YI(TOokSkn`!IbnfJJw>2GZ~nRm||&G8?qisl;+Pl{Q~3t<5Z zNM0_LI@P_?$Dv=zSLQy9t1%XndG3zcJ7*|T-ATU>KK0tW3E>(NDHWxp8;g7#I%i-O zHaHd`hKF0fjkbTKVvG^4_cr7t2h^)Jv|(=(O{&ph_edj?9tW~r11cAP95|EpzRgT9 zKxU0K_k0RmPc52AcP+z6dOO4_E%JboI`7=TPbUZ`n{sjel9{pVdUJ?sNfCFzOX;Z} zLy*>2Pm1E@_d`$zq+YplbV58o^36|U?>SFpR{su8YNL`hySOolcMb!9b1vT?;#FLy z)=+ZQWG$oD9FCXRyt#qy|CkQaR>^JM$`1gl=qOdRIG49o!}(RmX2X9cxLQBy2lKdw ziPW=B1uKmPJRkXX-_Q5h$T+p^AZ1x9Wwdc(HWT4itXR=7hvG?jwYMz1^NyvPk{Sla z6%%*8p0kWfovKh&(~-_?$20PBz{kB*m^2e=yi{58$d+rS3>WS!;poMm5`DL(hKeKS z?#5Q(;5=m*GczI^l61bTld?t3>yE=+*Db<;@`}vtSBL-sSI4=cZ$fbVTpw3_b`4CoW@tKTyo{YiXha34;u9V!{6nKxXk zPk21oIS}dQaSYIK^8G9mJ2V%~4&F*Y!*SlKj>r1i!3U-|qcqesR8-D{dfY+dq8*%G z;iy~bF}0n*q3T$F#V$FgAt+(Lt{}@T^gJOQP4(HRU7?+Q^`+oYyLyZ-ai>^azN=b6 z(%nQIp@z79P+C+LFW=Y4eS8fflPjQse=bU+FvfAts^`)nKb%R?1nwQrtG!yVh=@?u z_jO6tU#SMlKEJ2M+Ho$%j0jit;fogMVd|Ej(QJ4$3I3;J|F(7-dyA|cM2}mH=po{v z`;aOfzfMOE%13?bfpK>TqeCmioH1o0Kne*mmvZ<^ZlQIZM-H)pc3zo*9zNcZuB%i( zHLFZS{nyc1ZmJNgQ5JKe%h2_RQgZZH~k zHHwz&L{goSUVfto$cH6!W%hu?Z#fRdl?Zz<0<|s)Yes;Ko0dX%m)nMoClbUkp#-rw zKVd4ak}-ZL&mU(A
&#KndHSECmx5)TT(muIQBU`#ZOCGb$XJ)LpjhiR}H3)*o;x!knis=XakaF^M4>` zEdPm|u`{y%FLK7g#Q8rvc>i~D#>vdV^8ZcFT0s?bHj(ILAm9Llqyzd%$M)a^gF8O~ zfMJ+`2lvpnfckR@AkkO^f%{1ja`x!@w^@%8oo9GYw?2PWZNJoSZ=%9)a3GMcP0`1OCO^5GcOziD2k}507x-V zuA+u1fSq50gl(=7;4i;UQTvRBq4vAm+j} z1^XcCex>?}%)$jYq8%JPJvWDjfb-D6EvWeeq~H!F{7X{xC20Wu z)yxTCCwJ4k_>KC_jR^7~&M-Csb#ep~6CvA45+!~eLJin2h<=_BJE#*7<(O}?X)C^h- z;4M&~03iV#zzr~fx8|zNkG|mW80Kei{Co3jE;v7)c?#3uaSm(^-U!(5ZScVnv^^LQ zq78d(_H;MyS4?AT3&1)8703XxB~+l{XZ*(iZ1XD;e+D1!9s~mz|7a8z;OFQ2+w7x& z!5U*}{u2KKUwq1xgu0l%?(M5C?bl68dXNW@4+m%q01nTOKtMwSgJ6sv=I-;B1&d%z z-}H-G1;TWIpZt&^rHOWbVI^+44@o*mYT87{ux-RIh_VVDd~VdIm~>;h1+vO{{GSs|K#wbSTqMsw(KL+5pX2T<&`Lwm! zVgsE31=1SUUUOco}deV_(%_V zh*N!AmZ@Com6J{>dGH9*-NQVt8l#U-qHkz~hPT@+RNaqphyCReEz(?z=Uy*Z{O`pvZ8+afPg+W86wF zv{hciR38`Jlyfz^5o5>-e{%e1szk!Rn z>qt#@)7Dnzq7A1UQkAz?PG&R88Tp$iQbi+b5#_UhZ&0tI-E7kE2Ut7MH6J3cHQ2c3 zVpY2jfNyHB6Lsc>y^QSyckZ)xI%?S;3$z&JQs%1z>Ff&2aD|aXB5~EYjBa1c^0X1ZXF7EV zlqrFy2}F*#5+)a}_lKOBgX$m$LTzAU4xwzPob%8+>%5O9c`^c%>?q>MLwtQFIvVTo zr=7}kOM2X{JfUg3F`(Nk2iG{0=V1;a^vP$`MbZswxIPsm;^x_G(;IZdHfFO_qksRn zo!B-dPbax^=<)QG^M0T8S5yyG<*hfI6*HYSXg1(~I8+&^^A#7c({-i+S7huqkYNBR zW%SgPi!w=q{gkXHhI~W4n&u=C^dY(DN*SJ%m3)Z$(!)+ey;UD_vz@zz?E@Kr-~OEe zK8TgP01EnD5p9@)?1eRplt+cTA58X54BF7mthGcPU|Qp|w`@VbY8XWB}ja0h<3(cXL z5~K`=b?&~Wrfd#Ky=wZ**%&CrTGTc|yBe)$)L#wIe?!4Qj@RB$3JOCoZ#={W@#LP} zk|$a#;4%88zS};yr#kkJ$%N~Jz8ceXf1cQ=c5>W>o|M}D1n`y0Qbno#N$R+*lD!_F;v zK4S+&Y+WePW3dd0ulLcpi?p8#9*iP(VJ8Vql^IQ6ARYFDd1@bxJ;(z~75DOx?8T08 z3zmDkBWOcrZmQ}aMosn0`kSBswTfUa6iQo`!>ki8k7W(Q{6gEduj*QYm@%V+`;wih z1s(*Gm;A!nsXHH5Zc&|Erozh{p7`x68r1wid`HT0f@hbdn2E|I!|7HM1bNQ8iSW}K z*O}l54Q;Qvol6!dGY^BCuR@xD#fM}}JLkfnkc)lX?7HfVNEwDBk3OtTL-E*SfAFv_ z?$-)I7V}YacJTM;Orhch&!@2}`HcyeGGL(^OcxPd65*xApi!S>_iPh6bS(_Rt99Y} z!%??GtIEgtS01arU4_sm$?Rz46K7{4;3~y7x;Hc})rQor=`yfUb6>fr?|Tmoh^sN?iiwT?jd zY~=>{h#Hf#)dU~a>^_oOBcF>`ec&d7F_wpCF(NwFCW|$O;pZ;;q*bn8o1cC^UVRO? zJRT;s{`DdZ;Ltugph7CU$kfw)U74Yl zO^H5?61($tui6G77)OeYHVm z|GnBAZkh`(`o-grjH%u864Bs-1bJDuPA>4o8?nMrGoM2x_1Id)_>kC}^C(;WjUK#y ziyWGti1YX6(lZH(#yd5Qr+8{i_l)(}G|TS;rKK=P>R#imknkj}_Ol7JnE!-!OSd|t zbfuzci3J+PsO?e;sE-}d;Nghdi( zL3Tp@&rI87Z6zVGdu6QR+0RQ0sa_#eX7N_f?BaZBYdH|iLf z%mZcr)?BNV1rxrA$a@PoHbE~UMGFA;t_lw@aN1PCk;>^dHai33%XP13D z&gbB7BrJBk_#x47T#dhHkO%uLT$(QLw0`^BhHTAasa)Wo?oob1BCqR1g#RHa>|h?g z6v=R{47$!SxfUOqpH6;{v*UC7Vxa2nap*89v1;&AW6k)g=$sq{Sd=pdGqqLCSbBUeQI z2Ycz=)y1}OSQ;&0TMKj5eb>^OZ^in^7b6wG8E)B##wbo>dJbwvMI>36tjgwim16Bu z8=9F*2#44r5SdKi{R<4Wj_xpWMIuVw--Qpu3fv{KAk8svvQaHIL;jp@=^2`d9Q%oU zuDhE$EzFU#{5UK2CoEDaCGGt(6G$UP`1`_v-?hW<8IYAWwa2_uNd^7V(Kb=}Xpo%; zqw4BmoRthhI+bCvzPW-<4*WN?SXE?2|8l!nL1w%P=z&k0gcyBIWZkeO^ApeuGwi>MY$Fr0ooZ;cUHJ022}!iuat+^q@kaq$L42m5y{ec z!A-E>-h_x!tf$#134B{Nr8J|tHAS(r4MU7{!X8y`pQubnnpa!1e+KIx$o!<54kdxB68WpfioTC);U*SV8;hZ*ZTYYf9oD+TiKZ{Y}O2t z3ikpiwQ3x~zZ|uH!F$ctQ*`X^Tok!*8POk92CSx@of^t+-}Azo4H=ZFAjsXuy&5G! z&J=!2+<>y+u?L$?4BJOblX4rpIf@oA;_==HVfK`zNT_5A9J0=?kQ5eb+w3k>Y#k*O;C?8&AnSQ_Qq2%-XL1+K zOk5=LOJJa=NI96CnIHA>XX?1%!uOBh4kYSWxtN%>Wl!Uh5|eW2QqNaV=3sX;m8)uH znWIPue436h#%IVxD^Y7{`4MX4QI3f`3?O4=DOTHG$){29lTho*MM!B+XCcdx6Fi{v z2Aswj@EBN^VBx}rW8UZnuuz5UDQq_JKrI@xe@Q-`D%W;pEz2dD$q;Hv{^ z58Xm8{yn>BfI4|PY(7aJ*l6Fkwfwg)m8S?UaMHFK2DQ-=G|j!jB_LnSz4*4 zSv6z1pIW`SQL^;$=1@NJ#8&np%`6Rc55aTFmqLmrnPXpg!mOkf&#d`18wH=D;max0 z)DEqQSzb|3NxVa~TgJ&t$lSkgT}+%Ntx(T#ecL&%A_n;YtVN7}L%*E0sQz)rJzVRz z{#No1p7n1TiIkQ5SKkp$vGEpU&)DrHfYI(s*)NO9~*vNevZ_ye5kt zpE58OE{)&<1MSHfoc}Om!dhJN_rwme89Ge(i)ax?MHj&Fm*iJB4fP@ zwyA~jhvuMin*(ofRO^s+7h&?R2j6EN!0y`pt}fiXMd(47EnW_EZ^SCW2d;iO$WMxP zvqZF-Q-uOA!G^}<_o+c9Wr(lN+Z@i@C{x%IShjBpamEGECw#1R@j%wh4P)!~Mj&Y< zqYf-x{c>{DKenJ8tx9el2otg^ObzeJ5HsuA2Q=+{`1bwjlas88xi_gO$x|Xs&sI)! zUmWxH+IC(ndc^a=vFI zpsQ)QT!c0ZUBAS^>xE5~R!jp&Uqo%I4#PX*1LZMTIN8PU)#m-Y3nY8F2VIAv5Src; zZlB<8F-onJecj!xQ{&F$78E-Km913Yw z*B#2y=_Tq1dSes!Ve5OLKFfT!YOM*dhtpVEMvgrl-a`j#KzPa>D!OqL`u29kX#>7D zYp%Ry^et0*(YK2^cWUMh2k)nXWGIR>7pt7H|L(fv&dQiZZiMs`S;nj_MSMf<8OBiM zj=&q6TjILy*BOY|ibBC`QqpTBytrbC;hmLP4}XAD^x;{Rlkj`@NgjcbDbdsUUx5~_ zzmC}@+QwX#mgJ%hO<}~u$tlm7Sp(;Ax}HC05AMml4NP!s_S?)^O+`Qk-Hv0EH$g0) zE)4NGvWyLu;7@ZV=(Ck~)qIv>XvV>G#jVeQ`+0Y&oLcXNLQ$z9Z(D^?T<{ml4$Jmd z)Zzw=J-^n(cU#1Tb?OOkAY5BKqKrJP8tll18=aUp4oAB&>amxMfipt2BtuY}Tl8 z{?^rmyN!eVI=92t7)%N=?~8tIR^lMaVV9xD%X8h{>)y!Oy+OK*8XSMSkkqh8J-G9c zm!@!fn*|u+%3(}xarqm$ij_Pwnin++D`~gGe~sY=08GBQ0Eic0V_+8aj`vO9)UA7@ zW-%T&rycTJDaVyt{N{Wk@`bWj$+$%~@y{sfgSM-rChb0!ZTj(I3U?4EogZe$rHxZj@qJY@IQmvrK}sUIzG?l8$)Zdv>ryjJtQ z>@_GpW{Z4$J+8*fbz>nPPI3qWpSb?qg98PDH!N161Btm76+#lg zBjmeyT5);Rt`sBiQ^#+_8f`r>#hPIaSPV$eGAW5ggwXr)N6QJz{qQuggg=ZcQ?M>Q z?6R9g{L=MS$LIaft*la~g!cw(4&so*#majD ztV1tW1~x-&EOYBK&*;{UKXf6ezlih|v*x}8JT#`Hkss8DRmt-FeKsbYjfG;fYCCCl z9<}2ez+?d5?@CG_-S#E6#~)zDMWmXoYzQ3)%aX%5Z3^cCM#TNeA0Z$m}+CG^z zB!uy1rqRHWmrm@_z!&Vz9r&F674In{{}f7ZA%Bf@0dAhgq-8zsK%x`7;#vC#4C2P@ zGwwFShNQn(+Rj4WdcnL!o8MkV1UPIFCrbhbUE&Y+4LByh=OcuR9t9R@#CxlfANfRFuvUm&Yb=w}HUrK|NDhEmO-r+_FzVRCG z!1~wOr|`VA!Eovt8<+#R7Spm`>U*F`=J&)EU1OZQZI<2*T$j5l%|pb(SBnIl!VxdI8qt*)USG$hC?j{Ierk1KNFb89ILtFwXuPzjBiWjmt56$sr(9hANe= zzD_7O5Llw;usrzA{$;U!nZ%=9&W0F}e|?y~_ixr=UmOXB;5>$8BVBYnt>p4L+tPtq zDijlCS{Xi+e??kYNu)T%s@TFe#L<$qtRL z|5f{A9Uimn&N37ec2eeR*yTq~sAgo~;JL-Bh6$qvbO2${2rCZ%>jNNjr2#FMK#W#Nv?V-x3%^BSg0$O1kUoaT;* zdJ%^Y$jXu8yWe8O6fEL#wkCq~ zFdn;eg*8om8;USqRx}l51tX>Gouf3ES)6sSOm9TH7)ZlYRcuDdI@9Fo=g_v-`!YjO zgqAVR=X_VDo>@g+%2Fqf;wd8wh=<=LtsD zLj$E!&^%I<*%CQWQ~aIrTwK>FLUTjuyy#l&jr5+f{F1f8jF+Q#t79<}R>t4)>E_S* zJR7^$S%l6z{JQ?T$A*rs!74uG&bg6X-`pJk%Es88RhZ@U^N(00Z^A$f*Lc6rlkq#I@`96=b-|&nxEh|*sdDs!q+E}*)46TOKkaLPjEJ_24> zyE>}ZTQYdvjy}c&X6QU|s3^m)u=nZvKwq2uS@#|dzD&LH#x<=`>ZF=E>sEuchDoWK z9Ix2&qv+WTb*)QiWFk5d_pQRJUhs=}uwM>r>fh$Q`1=D6POJ!|1o#X`a#PP9bQ>-) z3iU&CGv^?VGxw8?BDdmB(X2l2ez<5c`V5A4r=H>+eG|M~6vPGCk)Mv|m(#ek*~3Y% zJ9)YkpW-m%|ilu#Sb2L&INHv3em zFP=TX)C=`fleOdl2)Whi?@oACX!$kuAR366h@N(oGq0d|fVxPd@`b^3&PP#Y>-4?5 zMs2wp`WJ$?Qd{x&EhpDkPdEdM?^SY6KWd^c#wOc!wtHY8b5vJgS6cYX`Y2Xs)9w-A zzD>+@ryfh^eb~K3X7m?{4njAqKn+d$vE(1R+k0@C;q`c#oI!IZGZ@X$o69%7$dw~_ z7}k?n?M0ug&Iukzt#0;jr343sAB-fQ31CVgemPR&`KI?{p|*ZGE!lJ(W24SeUtipV z;M|9^qKiBZ^XUl@OBBnTdV8@=QCS~xL9leKgn~zP9uc%sKOt?cl{)A2vZM~S*K;rrT0gqz) zPk0my`+oybOayGK9RGd#-*^-|D?7*k8ISS+S4q-dpqm%1e8h|2_C`GGd7)#4M1X)y zob^s1o9BiIdL$wc<(kiWqyw5SmJ}BN{VW=F?)~w3sdc@X&>HW`^E7*&$~AXu9GoaN zAESm3+6Y$NWgw{|$m1Z;i-z;eLA z2pp}1aDQ+N=ink#{P_HW*adI`0wE>+>*?18e5gBcjgXHElW!aD0@PLL2C^;)80J6# z68-q54iPIZCsDj1?B_>MPtV7#4uZeAr5Kh3z6&bI1qjm*QQt+50rINKBry69^|OqH zk4G&a0U6{jZ2;jq;IYve99RJW1qfsafdU;K1L6`+;0lgGWd-Q8GtkgKq2-(C7T_BP zP9R?XHqXJo+aENj-;a9(FwjArojV;KXk8G|A-ON7 z3>U=8JdWs7ZVN7-s1CkfSoO7x4`dd1KTPD7kYHAy_5KGcn9J<9Mvr)X4i!d-=+Sqt z9Mm2hSnm9?_p_jbjbPw$6Evj7DwXegiW zr{Kqqv9GhDurrM5B`@)Zk&2?f2hguuC=ozUk`XWm_m!F8S1m9)A6S$O4d(DEei{cV0vb@xKJa7T@#FT^SMjNy z{8Kjj!%d6|Px086b3i}%W7y^#D&YIgpfK?yP*^H}9h(Wd>aQ$2;2%@Vh5>Tt@b$aW zIuFMRd(R-AT<8fZ`U)cQJxB%2e-S3=2?_C; z2Fq$9fWAl@Bp~_F1{s}M;D1vE13W0$7bYvA0%LG;ZFdqJe$Hw|3U!MtB1;N!`K3Jt z;K%o?82B9`Sit~r^l#nyv8pKuK=j++*nxux55SG-xANED;=k6hea95d?}{_}Pw()j z7efT#L%Dx04e1kq!_&OO!?^#%d{aB-hj(#P{q7VMRK9zEeM|rZ_Y4Sh|K;RRpxS(s z_1I92;i*BtS*CbC*AjOL^3+eJNVNSf$xA|$OFdsi2Gv$TU6SbB7SbF(%;u+E*;`6~ zIjGH!Phn}{A<1;w2^(az|DJ7Yq7!EThLAhppv%SU5p+r}mzOuOj<6ihwc&FAQt8(A z_;@-Q%z_(k4L#)RM^*318~_HTavfFaGN+U?M(X!|NDzD&~R`$kG#Cr zCeNG{3QDs?N|+RkuSW@CA(*K>h9ljt-7gu6pu~`LNqKbE&`IwB!?ScB{Q?=L>d{Yhe2;T_0jai@9!SaJ*F{To;%!5x{a&zI|JfArFcZ zEl+z~xt$fRk&qVFC;Q~~Q+#vf>LIL%hxx6O0@}jm7h9hVo346!yh8hObiuqK>wRo) zDzo#hV)g0k=OJssSM%lQ$I%0+v4}>uRn)mAk7H}SY+JD6wjXr8@w=Jz_=eS=y;qVl zVIH3LDib^zyAppx1|{wHC3+4mOB}>jT_3PX^hq|UX^7Dftnt8oz2F< zx??M7{9T5FdZyLPW&In!=&SC^-FsS~O=eqBaDpjnUp`Yx*9dMyb+;$vvTC(sD>s7*X8M{s!Ng90Nm9G$9{3DyT(r z3MLm+hpFOpB_CNe0^Ckq022Az&Dbw2v4h)m;F1s5^uTBv;!ur!{suJG?I%@9g&S)@ z`s<@%iff|qwpO{xYLw&wri4_hSU|2+Meg}PBR6fm)3i@miR#`+1f=Hsz^mzrsj261S9Y9BPJ<2YJ41NA5)>3oCF50 zkqZ`C0WF%&`7R~ru^6)8#KzMBj6%#Qaz*z-nY+O)&~~&`_gFnQdBN0!)+7-ncrI+! zONY}hy~l8a4++C4OsEeN9`m$#f%C~SIw6M0B7X-jK3%nO5C7Wd;r2I9`{qtM^i?5qm|ay`6lIr{pm) zmw?DXIE6y9R)Jh{@m+(1b={&$Zm@t9NZ_DI9|v=}dJvyd`BRb(>f33%HQ=^_S^R3r= zOEzk}AW;XJ81Z)qZ}j^E?sT~|BD${SMDPYw2dA-s(wR8LOe3Do+Zxo7Ir?LU44shU zCOJkbetLbMj-NkwYd!N9#x|A}@63HFt=q-rVx$OACRX1Y+T0Wx-uB6VY|J z_Qrl(o|!LYT~%k#cjF4X1nmC+*I z4u>OO)q1_Np#`jS^%p3MA+|OvS>Eb7*$|d3)l*Gfdx^OxgX8=htm3A^$;>$rqe#CO zW9~0oDF@hAef7yR3?S-9X1NXK-MhLsQUtu$F6rFXmPu7r%oAD{*80vm`U%d0ZiJD< z=kikz56DD|SXlZ1CEQB+5T-IbJZuo`R6DY5Z>lOOCa18@;q~b5jn*q+#&@oQ+Ty=n!BfCUW0`!KAU|3mXq28#{SB!uZG4Yzt$4V zSJBp5dO;E^hWFh3 zGA}yXJn*>{I5Aj+8ye8rtee(Zf|sot3>*vJbg(Q0T|EqRdcVT1uQQ}QXEgf9t>C-X z@b+wg-jrzZU7Pk$b?=RjUg9h1fZu~@n|~iphGNS2R94XrU}U;mb68^jdMEFst~0-E zRs1&v+^z;}E=qGwxqRbwj$_AM6$!eF?oY@uJU-cCg)o&?CgXvgHF(vhJJhgd!{ptF zRivc_i3-2ulFv%|pzAo(#2NoxFmXAmN5_O@SPDyVd|G@iSrfxi_lcMh%$y|}` zAWc&YV>6cO3jCMD3V13{Px(2 zdkaTJ(B?gV{F-mpT1EWx{LK?!PRp9&6qg_3bHR{T0%y*w7v-h4xvAik$#Y5ZXuGY) zJBiPtmO4#QO4^ZzccNfyBrhlb^iu^cIO7&ek34t9%~bMFhI6Z9<6G#(dvTw%-EJKX z;PvdcqE}~lI|uC)<-)4YbIrH)BfxdoEFOdo%xuVQtl`V1x78U1d-g%x>m!aFM}!YM zQAY7efQ#m$3?9sXR-;UsYS=NVT)%TM$%;7k1hwVM8gq_L-JX9!aAMG6)db~94Zm1= zopICgyHD;RHItFT9A!mCcrh;b=ttF=BH?=Qy*|88qy)fNv5Oh}m3j`1>sVzgXqh^0 z`PPQeMVKz#=!)v)2s6aN5kcxKhtJd0-~roOJhlFpG~)s)_6Bb87o9+Gx*I4hGV+D- z-=rWaXnQjQp#Fr@(#oTCw0z;t$jwGd#`#U-dziekWw)gs19dUwDVkX22gIXW_x@0} zAHtS-#%F#!pUhd{y^KX-mUau2y6D-;dJ4=8vHOf)Q})kbXDea)Y?!T z?gkUEttNbjn0oUm?yPuT(u)LH!x|~4wBy1@LK~FG_EGjLLEho2a?yATx>4y`Os~oO z*makM>fYbio=(l8R+PltsSwhd234V$uc8HAYf_1`7}L8u;o%~5{H&19 z47oA2XyU#P^P&>o{%HFdk zLOKIy>I~?(+>JR|zVx!NGU@f54k3wT5l0FYo{tL}zj;M1SK)UcTt|c*x;`mN+AD>J zKLUbS^91HKq+mI58ULW8Z$yN*B+Jo1k-9lg&fUDq5h3f+sw#Blq2DZ>yUF=cNpu=( z<$E_O`VE}$#++y>bY_JTc4=Z>rlimm8Xg8`psUuyBvf7-C5~ntJDcPVLxqn2nLVSw z%}0J%U&(Jr32LAhJF?E0D8zCx8oY3+4=PmRf3D!8I@ zJ6^wuksLJpNdAx_6fCA-;F_L9%pg$r=v~dUk(sSHI$uCGXCk%^*iVt#exUB$b8IrDR7TS-__8H z?6Xmh&C+`jYc&j}&|~lXoclkurx!!>K{F<-x8BAmDe!@LE_L~v=8YkU)4UJff@b!U zctgG9-F44pMwWA>b7CJ*{kRUH4+sdpD7B4KvOntgTK2t-R4^mv6d6ol;$EfF3+VxM#^AoXMQA^$YuCZ{Lak553R#` z@VV+!f;a7UY!u#}Yo{SJyc4IqcyrRtWq4B9?rDT(;{xs$=_A68ec?0_N3BhEC^enI z&2;Ust>YWt*{bJo^blZNw4VADtj|g72&tUKCk)pIfNiwY^|ooKT@cjewEVS}aDSda z>U1AmR7UWr_s?2ym;zm!Q>w0 zRDvQ{x6D)@wz;)lVGS~#ZGW#KVeyB%C_otZM}&)JKKbv0hEiq00&vY_>1qrjpk=9%X!sS?4u)`)fO zqf?&aLvK0NB)ea#Ue*25t5jTvsxu8yP*~K!R5wG~nF4ndOo+XXmbj z+tvw#`ibnH(DmMLFA7s`>E16*KOprh!>@}p>tn0O=b&-eiyA9nKUqCPV6f%mB+bPT z9uIm=6)E%i#bh*jSqqabIY%F|g{<*MH4W8bZQ(BPcT}PVdNlfbRaW%J>~kR3bJ{G1 zrEuHl!XQ+~xEKl_^-`Q`yB%MaoKz%lT&Gbrkf)kz8jiAoZMUY@DI;tH2lOloloR3E zgL#8QS6o8$aG);c_VBRw+bDwlo_FP$mY#nP1kk^pwXXg;LF$mtG(Xj&7L2f4aHQnB}e91j`m316X@0b4$9wtM( z3At(z9>3~+dQ8}Uok|d2gThPdQVWWQLu-f5U=?k6*;8GvN;~{mrKPUkt#LT|{;Dw5 zNmq*y)<^P6hG@*kRfzFxBVzm~-{lqjxO4*3JUqILls))PL94o)5D#J28a2~t%snri zXbZZ>&>pGS(VO^?NTi%}44U|qRR^^slwR7JPuH1xJf;6I5Hp{=YO8n5y{+5XF-Ixr z)f6AKmbM(XFuKw-9(kpGOuT5a{AGQF&0*{e&Ks@Xj)O$(-th$eSX*09mZ`#-NgGLQ zj8O#~nDhX+ImcSDn$8!*{q3cmRNM&@$R<+a>7P|~mhN zd2fJJNuWdQNP;pT;qv=d<30j$jNUl_;^8gkFmO0n6s9C1=gef-ji!AqRToOUF{>?h-N+qL1{}jJ z-W;cm;wRC<`3si9!*0Etlo7z0yQ8YU=0~v+BcmzN&&INh3;c}C1x?whh2~p1i<$=M z$oO@wq@u7K%V(rEjrV*U- zYA=OW`e(OQWQTCU_UYxaFw_|TK9AKahSy#q5kz65@iYt(nc*+6JZ#v@JZD>FmB+(F|M|u_a8uktVoFJN zlz^u2h9<~uKey#U7ZYPs`?MK%r;DSwzB8w*`0?>eX9!PYXE2fEt3f?T4#zY1%j=GH z2Bf397V7oN`UQ0$#A(kMvE)l$(tkJ$vG#lwic>!%M3YR6nVkTwANwl~^_oIgL6($R z)N@lL$%XZlqdx9JFpRNOF72)9!b_yt`Mu6;ddi!EQ~9IKI_6Pzmo{Kt&KolRsG~4XyDE(2NLR&KgJ1j8QT1_Uvh)1S zU>BjS6sEsmRndu2Vw8CtLj=~RJ`JtTlpPs26vj+b_vFtYLuHkNo=wW8=wa@$^|h!d z^P^H?Ns1j6LlDpDqs*yk#xmHaIDwW_4!`pNet~)rZbdu^yo=Miq)36m8>Y#+l|J(J zW(DfjE6{!n z2|Y2YWA(DS=^eey8~L5VNqm~Pb>Og?mn~@~`5G?pJW2=*En}p{4P)HakPA zd;pkU7&Dv1>+e>VMleMKhiTaWX_YPATjrhR2A|Xq?DU&s4B?|+uJaBkL15+x`e+hX zj0dR)Z+uFe%EC(noTi`5>+{nHY3My3+zi;Nh()A`Ru+=ngyaZzAs`OJo64(0vYMVrlIupY+l|M5%zO51Laphl(+yqb z#2}-f(g14R8P=N992oVXe)-F4XZ)gG&X7-ccT)xY(EGXww|5@8{KG#PAxTCnAH7X8 zpV2<1?l@7~J6m>3P}-R?UI*p7i1Mtrb?9DcKo0QNK&g-d@&*!;gg^{<;OCT8vmKMX z1=U2ckksTmLPm_vFtx1|I3SpQ@OrB%@^tVf1bX1G_+YTOk9&U5ZW{Z18;dZXDU~4^ zKS zU>sM+55rn8HL)K+;9NUWc{0S3?q(X~23D7SPdBPI40B;nj?PhsZ!+*5#_bTk@-B>b#COFf`(Tw^3Ek=m-RL-n!NM}~ z*{pFaEHN%6UZgR0={~y~%3aZr8%IMs9QTxYU`Hfd|R1*|)ma$uu4Qs6Rc@~~;24y@P@dF$I!Kb9*9Qy%cjXV*MFX8T~g}L=s zVc+Ir!S!R=m)UQYd`tnZi;awWsfUNQV^?IiN604`Pe+d-9p-D3SK`s*?1*=P-9dH9 zw_X|8D?C^hkNppyslmY->sPAaqY9-L3P9t*V_QTU&QPBWJg<8!Q4s4of1a*R!ls<>CS(int z&Gj3IS_G){kn)gf|LEn>!{U2$b5f1bn2y2mY+$rdIG->#H`pzaNb8 zhkbdR{si@1=R~Jf!LF^5;xP9e?oUEzUdzUS##@9iP}dv52XMn|26)FG`|TN-yiRX! z_N<6x4kYkkYH#D%# z)ol)#HO4HtoG*U*%#Q8 zz|8^_*%ZW{;u8Lv=J9}lf(v(L$XP0f4r)w%!I}={_NfV_05%1Gr&Kp=U!o z1rmO3_WksO0J8POkMPWXL~sGUv{Og&I`D=uPT<4^051K2V1a|Wv#7NW)D%bo+c^1U zm2k68L4!X5OFsbDz~8yB0K@R_?p=LLeOLp#eNh7l5QB4&FfSnkwgAfv;1mMVk~#QC zft~OGLp6SY18{T@F1)L-FwOwlg@AqJ;K0cyt^fus1AUJ=1QO}U6QMhx$G1^Lx9ZrB zl+=SYhlsJU3LF!mrz<{C3?wK)d~Wi)d08#t#G8BD{^-jL?I}<6NNTlm{p1emP1Gu? zd-Ncfz*p71-uVd z7o74F*`wEEqXY~25@_PgMWYc1!j6#MQWXQ`(ylYlaq(v0(d+GiU9b)iwFS36TB0W z(LvmPnPb~BT;5;+{Zy!iY7+y%f6GMimHNwGKC1)h_)ibOzM9j^f@rlU0Ic|n*pU$s z0SNL7{Ol zg<%W)WvT#Mf;zaq-PKS*#jpj@?1Isl@g>sr1zzQGjtfB^0<u>k=fwYlF)rz+_%(#J5+v(J zeW(H3FZvfdeqlnq`3Qw)k|2kMe{@YH4n#X>inw=H2)q9t9gle&)IuPloGeP)YrB5J z95I@An5&t(09UN*Z->Oly))cj>ce=ax0r&`6_+0tGN5#+9l^cbzthRD+vL-zL4ai; zHY|>*-Uox=9&gOZILh3RV#<9(pjxA^d$j4@Hm#Ws9S*?tBPu+`MAL>MqEcrqbO)o_ zPL1?NpR=TVmUf(1@nOD2pu$FRr&&iA{NA3dG151Ac{kJN*HWlleoyTOJr#iCiuE@n>jKnJ2Qej5ylmYN zcM&=~%O^0aBiV$fm+MZ$Q50&!O8A)2)Tgnp!>EpiZami5%A4!n@kXi8{&sPoTDRfQ z2epn@(r- zPi|?BBL?Ff-n$$$BMbpz==l?St(PVpF1eTxC+<2Ow=M zzsN5S1KMuSO**5XhjQY+?X)V~oHLKko0L#Pj#^UM;{wH$50*;z(O_mkeug(z-SsQp z)M{{gs)hG1t4glY9NGL6zPx{w$@sAcRMEuAH>0m~Z>WKa9NBJPZ=23drfaqbvC`j` zq+1Dr40*K{4qr%Pw++~7*YixFSmFAM2|Xf?%kr_Vu*qX-F!j#EyTa5ZEHzA6s99U5 zswWklY|fx0%td3(hE04~#KzGP^z~%}m0l_%a&62tSllvM6Ruc0&{~yroc$1Kbqf7vw@%m={Ux1lnBXfYaX-rOtH2^<(JI+ z+@?Z>-Bch1{SOVUQ&}39zGxaX9l>Uec+nhzx`)7UBsNZk^rwP6-mIroo{p}jU`hnG zrPwD1Vg+AgZuN9^gdDcK47MJ?H#O9FsZsB+M?9F=i^DOILh4^Rf+rriW-bo4YNg05>$2GT2A{ zYxvF`+j@{Yb!{yRbl!D|i4`PTXc8G@eFRBWMg*dj?TD}g?MsF}2e>*W92yC+4NkH_ zR`-miVkBxp9PWUnTn^tp)WdrlSF2(=H@&@4=@I`@OPE0E^!1$8Fr6k~krjq<=m7Zf z$dYVA*TDgAjW{E{E&;aJMZG(q%+OeY_wsgWtZ5BLRPJ=CgLfjqHgM^&j|9{6ROcp1 z$@|0-8k&pJTWehx*6#Ul@C0dhNp9$8yw@!nL(G%z#C@FY0?h zk+YE;fGWEEfrH!G#IMsI*{KeO>zzb6c({fHUGxD2k18F}U`0S@hlteE9EC@`3#YDm zY@gp~q%%W9rE-|H52o6GZ}*C!7tlg5}fm;2nl#RTH2MYAk zitZ)ajn__k%lDziUQkz};Lhr;1}q%7R4%v_-5~bkh)${*7g|qctk^5+DRiZY`?Ztk zhC@g47->wgwszUev!MrPc8Db5Mt?(i&97-SY!WWx{u-aBAiQYg@wTYci8Kverb)WC zTF;c%9>cl>IM3)Hl-sA+Pi~_zS@Q2+)pwQ)ni`-tU{$-m>#ZM>XHokadlI|4+LFbN z+BBjApXP_leCK0RL?&&C^^c|;%4H;(F;M=Y$>n@C(*bAkZSKE~9=Eltd5H_jncx1i z>=1$z>l|@j?36^VmPDL<83QO-zF^tH_^{qnPk3UDbz^wDbXhSoNRZL-nCV-_^31X! zQ)v2A2t22#_eaBZu^OWah@d{kV@402s6L=iiS>1-pQ364lEhRtHW2bU$V zofCvDb}-`VO8UHL-w#wmkzf@Ni2~0pc5;x}8s&!~J7_bbM}&txrYn$X%j>&n`Y6LM z88Q)8`rcZP$|Zgz|P4@O;A{6mPWho<})C5|*-{nF)o(?s=;*U|jl8Fm%n6TE~ zy3+U#dj3klE6uk0aMJcMHK6RFZSVap1Hd<6n(%vTu`DIie>Oa-88yR6^&d?WMdP2K zQW2wuZpmhX6489@uag)$a^>jk<8lAy{XK7m+yr_~%LoH#%ln~s8h4lk#utNLwBkO{ ziZ$>l+)t;yco;o2C3CKj)p4j*^H6XN#m#wTSi1??q|nKG{dvDBe7z#mYv-+tL|X^6 zeLs*JDk#hweUG!e)Ip2awKn<>$5e}oQ$#|XZ+A4~7J%5pfCtu6d(h1hAd`+^20 z6X1&~{qPg`NRl#^wdRHM5{$(cxJU!z0{he#B5gfn)RBE z!!6jLtlL^@U}G34)W_rK?r0V~eI!-qBNonrAA>^tBel#Y+2X>dqk(rV)?!^tn-Iq8 zwe{VEn`Fx&S0M3@@B3r?`eBQhxq|e2Q?MT=Xl$|K;+}E@`s_~xX^D4b$`dZ?ksj4faNJ z?i$9S3qE#9zT3*A_e0DIIXJDbD&PGKbp?;qxeSPx7=7w-P^qxF_4 z4-SPSQ>^O>i&a_IY5!oB3lW>44;}&U?GeJQ&bjVWTuKm)xjQoQ3fKJnnU#!+^>B=h52{giK z3M*i|-oXp8u1)ePg*M>?0B^g`-ZwYv3iEO%^p17gtk$$HdGg7t+MZNSlj$G^pJO;7 zo*>x9tgE4#X~4&xeFpGk(AQY!6cfU0S>qa%rmUifED)RUUF5_enISd`6yr0yX-r8+ zcu5djY)(FDf zlXzkpk_I!V7&Z3)F>=VR^7z}A zhD3SEg=~siHcflo8$Joyek);$@caB`D%Lh#7FiTQM0zbN%s$m=s-}J_>7DML6I`YE z2*abn&l#<5s-I~2D9)`72s9%@8fjVeOs>MQ-AS_+6cX(Yx?~hfJCm;J*v343d)RYM zi%djE{)+eMkR%}iHmzj?FRJ|`bwN=Q|5$4YVRK#bD*fI_U$01z?xt04n@QlIfG;M=Yk z^^NNFx`}rFy^_~gE&WA0|jv;q67Ts_0Bq`9mq zBxN1u1Cb7U=IS=z&B91PchnfNPr!JZzPGtR!8&>gKIC2Xqo&*X6QR?2LcUZ&FZt5h z{?ZQ%1h`Q`CT22EZ{cI zYEHjI5(A!VZyr4$W3=9bkrD~x8NDdn46%josZ9JiQ3fTI;U=I*=Si*Q_H9p9hV{TWXONa zkP5!CMcJYfh00S#(mSP;A=WZXSfVg`7LK}NsmYW4iXv65N=kvz&bkw&HVERQ047}< zLPA1WOVsc;SRryjX{j<0_TW+Fqj*J+Om1*FV)i)cCU(OVp<^lsVe5vfK~gN%`@W<6 zWoGnj`IjoOEGQk_ddF&KB6Xf_$39rp8)_os_!Jw1^7~_{ps}muwq2U%R+IxcDDy(o zQ61JQOs>Pd`7r@qU`pZe?$7yth6eyp;-fh!1fuXi)Vq!jFL>W!#Fph|GiInP{b^g8 zW^B`|1G*B#Niy06OT?^c(;1VnA1}wbN_`?b))Yyl>cxiYJ(j1CN`0R&Lvmjv{*9k0 zuEIb;O{tJB7xv%er|gIT6#AE^gf+;K6mB4+Bc)>H@K!>ilfbn?k7u($BVbPHF z%noNj;ld(Dfm`Rmd}Z_~tIH1vGdpV2yg**KV=s~k!QwzK&~OT@(Z_1m)YcO@&MQJG z9?zo9CL~SC=Y-`O*n(RvOWj8IYd101$gg)m5tR{SbWxWldMR-0VSH*OjVoy722fcd z*`7$4Aip~Z{%3Quoonx|fOS=oc4pcm_a%~#3mpHg=BX-t$xV9~FY4=j+cVwq;+pg9 zZxs*16_vZ>yN{8dn8l%Y_c~dmWvb0VpbDL3)fOs4)53S;ZG4RyjZ4w?=5E$#7L4^< z4#SBQE^-%vGTjnkcMv0}9whZscJ} z$Uf(764VCcEHrlK(0MW2lZUJV@TpOxyc1d0YxTrN%%0!6OU2_5Ha&^DpA21bb|Nk_Nh2cL< z)7aSlkGGkT@xS2b8JU>bIR7_b2}LhzVeM?l2#W!`|G)@7;jN)RVMt9**~% zZr%Q_dfH8EGWS%us;If#UKkWFuN)==3R?e(L{P&Zr$>*Y_#-Q%7m^0vKQuHuGBgx6 zFkTKH${F-yG^Wo2(jhc}pf>Nvc(f(3Qg4>k&3ctl4(I?{?#Th{{tnnJSlCT3;^7Y9 z&BH_VODMP{0{F0!t55JJ2s$6i0aSnyBPfDQu6(G4UJ(2qH0zQr}rM;9v{jHrJvFvdrk5WFGyW1}lLU@q*8zE(W-6X);{ zDug3A&n?`Xk^;DSM}YP(QPr==9>A9m2Y@c!&Tr`__eY$t{wjY^jg1W;BC<{xKW>%*L#eD>#+3jjOvK-2!EUxs*EJ+t)p*N0F0y;KR%;Fk-EuKI2&;->#|8rZy&vQeyTALw-+hc<=i==nnlrQbIS1mM zo%_A1+OvcP{9&~A4ip5ia&xo7k3Q}46%7R7-#M)S3GDtwVfN3OLIv`I1LS$d0H_aY zH~MmD5DWyc&ES{zD@^+WuubucXYkj0>=S=mFMEYY03jGx!q6ges`OQD2 zVf!UO1ZcbVo5#m>0{#W{0Nl#=8#q1a{|%hY$o>tO)jW0mMn3|!@A}7~M?d?af6IpY zpnub5xYE1ppsMpD*mW|!{db|#`zQF<>8Ta(=4SSGE|2-aoBnsekI$1Jo_!q6$O6xh z8tq0Md&gIYR_J`>-6vZP!0V3X1ZUb@EMUt?ja*sw>m-_=-&LX1>qYEp8f<`2Z$c?4 zi4ig`X{6InvzlT;(TBS+XPPbSmn2~LnoxN==r&AKEv*8zk9scms9fVUYPI7DhMIEh zGU?VS<5TiLdOAf76;7=DZw!A&J;Larp~6IP$a@3AAh$6SHpqnc)55`M_Erx^F+3|x{sVgE z8*e2E&NUx8G!3XE9JG=OtK=E1(Q>P32IFs;z?g3_(&em<}^>UwNgws zqaRcqvRF9LV^7^Xr0?Y0Ubc&M@&}55jXbku8bXi;9z((>*UVrlvEYYOq@MD2xV+uo ze5Z1BrLLNdhF{JpsF33}XM1eyezEE$t*9>7H2Dx|4oHPidkZfMU;E<2?3bVk9_Sq@ z@u4apNDE%Td&{-G7Clw#BY(KIv(If+0sdkA=HvStE;oi)3boDX!M(PJ`^sBt4rjQG+ijAQTD@5s)LE5?bi}H>Z&t z6kAc-T)U7>@fhimh6H&B(o+48Fsk`tZ?{m!q59 zY+T*wSoWNnx6R_?=RY!Gkr<-6#8t=a52(BBYrDgJKR%6Dk))~pK8_Y!@k)smfU8hp z$0ktKV2}9ESfi!i`9@~?h}lE;r;;l@AGmfcn>sBABB>=dZGy_lqppW{ZDr^n)EAtv{Q7;^li2rV5B0n!3zKpGj6B ziBlPf1mIBsLf9 zOn_hTlp6o(N`^uil_f%JZL=KE*$wPzQfw#p-Ll@4gu3^q(m+z+o;WF=k}b+VkdYZX z7-&dbIN#7;G@5EUJK?`Pr~$EB0abg-@R6YK1Q(JetNym*mTGTLpY~h|pY1pG7smoZ zCIQ2+=ed3`HiUK31(YO(W}T$Ol)RIXCXQK;*dc?CG9!rMR105Ix?C+nyVfWeWMbp@ zhR?Okp$|?qanOc zaLDo!;b0rOvQ^(*O|xzH9dNI;wr!>^B?B6X)Cl3tmfoJvxnP-Y%3OwnJmfJ2xDx6t z$yT9Ww?!egSg6Z_z(f7azQ*mLezD8v5|{O2?>=97-k-D^4$(G-)Tv9)hGJA|#8Q`CSk5Z#}Mjy(Sm3_B};ZK}9|F@UcIbfT}1M`71)wt6W90J zrR#5b{MWK1rScc3`0oVHIfeFrKg`7Jk?RR2VLtH%WAV#;)nWFwiY?n*)1@OG*gxnN zG^$KX?P325WC^1XDLWzZ&vpTvzi-_&XKs2q5hMv{tTS?G3;9zgszf`SRKa*twm#{V zxVS6$wOofV_z?a3i6zvISOKy;ivGTIo+P8wM8)`uN#b|gorS$O;g>#DJ@gS|#Nn!e2KurnC z+?YYI_I6vCoQJ1HgqD1a-JY`HFnitb6EEC}^6-s5#f-dVg`HmYzsG%c@9%7TNloNp ztiXThq&GzL!kJcQ`n)>uPH}qRvNr{_0O-^m72g2-8fi$DlMI@xmV>Fpgmtp+>NLt< zjMX!(Hyo%{yXcG4g(bd&7jjg?1jo)_FYR(EMH(Mg661hqp!HZu?6B;`8XH(cOx#PU zmdt;nH$OGvpt&w3A77}tQPW^}M!rl%Ap-VKs19mU?oNRaB2bJ%dCh1BvgnylWCD46 z;b0y#OP(UV^(lyX;^YSq%a>De>kO}r>;gf~8IH%L7&Om(+_$ONgXmg#(D`%yRaJ?; zy1R~#&ktDD9NYEf$*L30851J6sg2{a_-t8f`hqpIUafcI%jhn|!f*0uL)OH93d6EQ z9_X%%fY;1Rq?auXJlLlco{Ld+tS37{Ni$g_*>Q6^fh_G%VnGZ0QXTI-CJGIrU(~x{T;;TV5<4<{rh2?cI!2D;ZrJQ8Qw zwP*6oEgY2XhS#O5vK9`*?$u@8nAMgrc;-p+fMG9POx|YLNtIdb4iP@AvWSVk>p)6~7p2Q8*3V zo0WfvhHf%uzT>|NZ*!cw;Z5>mwKB*L-3KNb6V0`3X{QVI$2O7%-feg9yLclp{w-Dx zC(Jih^(=!i>+XaG?zZ~t@?$dnt|efv3T+BA8~AT7<;u4cLS*pN-O06m`Prfn^Q|>b zt_(6zt9QaUutk4(;WGB{do5Hh_2zad?kdmra=mTJ6h)gSetqszdEK6sykZXC-Sau} z84k{4a7|K)B?U^KMm!m0z&13~eNHycNkTJw29^v1kE_L5xTRckoNLzi4c;qNr}ZJ< zW3sDtDu&-iy|P?FEKN7n~%-GjUB<_a;%gmZ(je_B38nW|v z&TH1i@aTz1JQlZuDA?|$-Lb3d8&|>ozB{k#xVSS$t(WjcJ2b*gy0~dwyN-18ESj}w zu*bwo3u#D(!hHN_Qdhc+Wp=W$_UW$oQT4Ml!JyUw!^_A=c$Mtu*jF^g->|Z~AlVJg zPtPlT(=NV>RTo{G`T7v)7M{fp?zLr5JRC8)hnN35z#qL{NS9}-}+Q!U!gP1J2PBb2o zga#u^hCt%J4mxeG^-k{2j^~3aVvjDXjTjfm-?d@I98j2HoB7Wql2p1UHAbHRQpq<5 z`C0T>0gE9C+2f7$7v;^ZF=H1bipO@dv|HL~*gf4NmY3o;yg3qsb9@H|j8xf(J?_|V zT}B-{4!_r6v2PS%iuUD>9c38kJnVT7Ud?waN*m3I3D+;j$2L6yv`)VU+e_HNATA!f z6TI_$&V;h;=pnoz0=g*u+PLuIyMpL?h9iJ9x1&ygvd$|hXXo0T`W18r@aS^77!Ovgx)6Z+DRWx}O%kkH1_rnBTEwQWqo{>E0E}@)6ARl@8Iiu-s3! z17J)JVxjL>R`$#hFnUM8NDUkG$#gfbjen3_FMisC0ABQ}u@So0XrMu>rb-)2zg19Y zg#&RXcj@B-ukV&OF4qcdIv#pCz2}kuj}pg5fdOA~zw>8i&Tb16nQ8@W+dj4)rKY7v zmvuX7S~Hsr3BK(q=i>aLq8Jgo1oFF!jT0uOVT71HnLN|6dUtVO^O203F#iaXB6qBA zeMDlY&9Z2r*8fvrkA${HGX6fWDH^`Qw*A@!X%{f+nciK6BTBH>q)A`MNtV&;WjwPE zmpqpW4joc)XE%pjk56flluW+PP!Wj&?mq9o1unN^v$=IGb^fg~997elRNq!r};uV+bBY=T_`0eCKWwFvr3N)Ql1$J_REf^cXf`w@ zaN0$UgF#7aCBd!LtKu15V}U_m9Diq{JA?KTp0nrtm;=D`zLJm8RIg^_e*)@yx_YjN zLpjy8-9WQokvZm&Afu{M20(}^P)=20O?3k&8?)a66|R~bi=IR_cb%6w5l975cSg** zdknl?7eOH_gM54XR1nMR`--pPk6pF&K-FLuQ|EMw@!^6s^CP|&{ZjWVij~vRpDToJ zaH?HH9Uzi*4+`fm{A~X^Tro*#mrHsjy!-6&UCh!(y9F=j{}JJ^t=(CVP5b@z5YsIh1c-M&?U0I@@`$ogF)_H+{Yg1Ew~$I?p8e5 z|AU~WPi}iQP_t(3m9R8kmkEWV1i)7>v^U~7crDWz^n24Tvscd80?kOTI9{gk3X?=_ zTj5^N1g_46*!wwiZveci0+A2hU>r>Itn`~xQc;60Tq$ok%$NWAA7Yuqs!KU!kG&A5 zCb>hR%kd55SrPJYQnWzSewYY&H!Cw%qxkF4QgqGxnH}TY0V1!y?!PE}lz(%Y9T!Pf&e@|ggQ_@7mcOYE7_tDI1{gL&T5jpn+6~lez#=@{=tCB7f*E0zz`js(n1@6Ut zuB-Q!LJOM3oeuLw=t&%j9Kdl^!hCd!9VFAVKea|gY>q(n*G^S*E&SgZfOgpf0@j*? zO)7L9q9#^U0d|H4)%^UU;-2P-$URvo?h)m>@gdbmK_#Tw)ekNbas!L(&$G%pb;Pt~ z9F98vaqnvxO_6y1Xxnx4xn$bMKitrJPA30GE*o%+z?}tgET;z8cB~T< zo~j9unz5j=%tYiXYb){}^dw)>O}Sjc4I(32U6uo9r@A~gs_#43j_@4Kemnu^Efu}s=GY9wgTP^Im{V~dh=YARP7H6-_=RO zlFK!)apT})1hza&H~lnWwa$uIBi@aWL;-ev~HjKE{#y1NYDGi5G7%VAK~?qK}U&iiAfeohz+Ivlmju*8bActGNf(^M%2 zRJ~e6yD!K|Mqr#(Ygk4ftFK)`=MY^ zFYgP{<=>1;!-`h&Qe^-sYl-1Ix0ko(cHxf)VfFQltfR(s3#KELwP<06K=#(Tt?v!o zkL~ZOJ0b!a8nh5nstI%hX(jl*BmYFamvA(?0P1ApV0T&HU}U{H-Gn$Adz@_?vZX60s9Rc zH!cXl-uX*I!0rqNR6H=$d$C(+&u^;;%FK*KRBkwtKWRMeNlpv1MR(Tv>33f^;~G~< z&mqkMkKsI2ck28)LV1G!8baBUb3^DMiFus-X;^Ia(@@G)zj@o_0ZKQ;&t!4w#@$I5 zRK*TqP%x1spdn7qt~RaQ|MNZ|vM)I?&Eds%>c~B&SRG?H7L=KcZ91_OvaYLT(Tbay znM9iLz9f;F@MNxbB4S}gcW(FWESJLfp@P_1<-APM$CGv3cF3I}v_NaB;WXk&DSQW6QfP6VPX*w120ckPENOl#xdnVRKN4b!5^j;(g7b_EtJEO*| z%3swA=EH6H7SNJEg@9&OY`qkI6=ANPPIGTp(HTUzUTbl`CAj2O*1Ea*`Xr2HF+#68 zTmV36zVU_@eOr_6;S>o~_nv&5)-Qv!vpSYpd|3Bvx;zzU6?ug8 zM;#96iVxNBhqKNb>=)49@16Do9pyoJ76+xpa@&?z4n4u;Gh_E@8T}bQkSJ-bIPuTNbsw+q^*| zkuY~_7K-R&(>(89ZcLS1z;jwB7e;$*VILDAvor6cK-C5eGgXudJVQ!C+RGp%l!wgT zBsFl5q+=7EryMo?x1A_fq5B~?MQ7El3B9*hRTzO#A|cL!Dfy!? z>MnB=hHU{wL+WHnLJ_H%uO26+=ZozzIMutnQgs(1ZM#Jg!5R33r;-WyQv|Imi;OEb zsCV#is&H@%^Kh6n`>s~0%B%~4+oK;yg{Vj98h~PIYr^aWNUilew?~e+ymn10`%_p~$Dxw@kyCTI8b%_( z6i{jq4?)$P0D0H?{;ZNwaonzdImw5Z9k?3cu`?bRqIp=%lD1cmRx=%ipp!d&eI`zg<5_5BbZA$0Vl<;YJm7RvyM8~z9X zxN#naSjG@lfLpF~PNB3G7}Hd0-vt@aA_n9i1=p}|=D3PT;qlGD>e$?7{f3^vfPiOh zbC2}PumJxV!O`b(d0t$-WAvHZzQ4W(!}CkQ43(?ZZP8lvNmz8#@g?$@qA^YF%n(yy zw%pOf!k}A)gg6bB^SL~nn%38$lvt_n>vYP_yI1bwGMenrqB54AbTM7mIf<*PD8pAZ z_ZfJfu(Du_6U%gY@!2qH{0D}&B^jPIJ%P&P$jg38UIJzLUtXMUulO@~k-V`YY4L@&x_7(T19Q>j^>Anq8dZ z(>0G?y`fpspray7ulZLSbS!#M5*Kzsl)`s7MH-~~&jYV#ChuiAm`A+$S)X@7Lqjrqqj;`A zgA11x57^VC+;wIq1?-(}7s6iVY zHV=Kd-Xne^1n*8%@##8iv&SsiBFZN^m?AeJ>{)|yFtI&5Qo8q{ac469y3)^b%wG%V zy*xC3w>GCYRISd1{oh)XI34KS+N!2u-KiX!@t2SGnXCVt56r~3tEI@e?51iTYEN^h|VDf{kE^G5p(ZO0hR$1x^;eVV! zR-fjSo-s<$LXcLsb4g{FPBe|u&CI`kVtV#`7&xjI@-!{{jgS!t;8UiCEbooi&BcF^ zh1QWK$zNiAW?OWck~@eaLZ|F1tIIiv-M>B*vZRU^JKdnA$On(BG(j$#iSe>GS$~+x z?ue++qw_hxpc#Y3BxL0F1q`<4`Po?=s3YTaU?zH(S`Em9l6e(`b;BjJQ+nqP{65KC z4UY@AKINdwO96SF*XY;l<&Dk{Lyn2MP6QT$m+tK!y_BA^7scZ7iYKKP3Ep z*&8>?@+c%_{bBnawvQLZT$`ugcFRsTw@zN1I!f|o;;~rwc;`iLoRQdrGFOX(v4zyN zd5Dvp(GP6R5s77j2@#dLX_SEk*R53xl#D~c0-s#!z_KDx*2q{H|)f7tBarJpGT?G6RID}-h^{Bj+S)%q0 zZl0=@HIC#GC^92~#)=w#gkNYFrgLoCgD+83$+O#YmAGD@d4#l~1X7T&Bp7PCa3$t( zUzD+xZMJ?GfXOX>^|OCS+T}15Up{nA0mlXpx3g*YGsNxtI6YTry==ung-rIk}8ZA9=J!65yi#y}gH zKjG1kJPGP^YSgNI^&)PEMSZv&M2CQ`H$2}$Yiw1X#;#XrLajN5!Xjs8(a=%W`J3+tk=0I0+?c?e>E^z?;^{SoM;#gkePP{Da8Lk zmY;2}zwac;m1vjP{Y%p!_fW7pJ3qe5AkIQcIr9&oUj!H+?+CKen)8r9{Y4a?V_Zj21_LXGC=R|!|Tze$3{j!0-J?|=Zwbac&`RK4YzJcyb$;QCZqJ| zcS#}A1?tL>gTC;M#1G&G$59|R>KhRQ6{J2`6s&4QJTt`DC|J4uNOqLnu+uw%6L;uGR_& zblUsqOVM~EjLd%8GjGlRHIw=?sWHCB8`8edm`>#l{Zb5U0rjdOLcCJeWB6rS@YwTL zVEqQ0FhL}_E7Bhfuf^3mfC1!8+^its(aY`1QWDw(7E!HjPn%E9daILs?ZK$!Nbzf) zt8Pr;>!x8vCl<9lTXv$NwNdO+jE*9o2-rY%$eA>UBJbf30u8R zZ}jDkmdZkn(!kZ775mcFN*$|XPSmOGKV;;ofyzOeVbd6 z>ui(@uUdI*^$0K-5&P08I?y1_a;Y1Er6A0bRCi$ch=4%Cs-Nxrz?@X zEy6(tUFrW&c8<-N0BwVfHE}YrGqG{UnAo;$+qP}o$;7s8XJXs7xwG%qZoO6eeAxZi zf1taoPhaQM5;V79EE;&L*MssP-X*8il0NH;x|~Oo%u*MG&yY!P5w7vMOq4$u!3eU= z5kz38cw3zm%a+Ws=sq+>`1V%vWtJ`!2rlQSm5Rr@C0lK$uND5zN*9F(Q2;dS$RaBZ zXfUb$>A&2!Ek3{XIY=mO3emcx++zO>>LGd@lfkQD9p{&xi5a1!uOqgkiL{!Z6(Q)Sb#fRW6H;5oPMBb z!Uiv`@A|R&D`OQp5;l2za|oT;-Hcr0cACz&wyRK0KC$S+I%LplsbMX;Dq&W}09ZBaYnU=voLJM<_uhCM(XBSndq$K7B zZ38M~4wtXan*53K7>s9Br01Z}m2Eg`Bec(mM$z?n^isSyR!4~>?CC|$!(bn^dALwc zvu$kV))N!w9rDX)f|HFIQ&UwHH?F-!&C{uSC>7Ol$4VP>-4LN|e^KEaWh?5j<^(2x@FF@c#PUA#P7;rHGozo=kvK&W$ja@wE79AlBi7Ue73+}b#)c8L znum?%tH6Km?d98WiPdWm%!E%mtZC=H9j3J1JB25@<+c{Ec?#1ER>^|FZCcZnh{+!c zaocaWE3^?_oOYoRerX$R?h)kD)tbTTP@R9rz4T^7J;)SdG2`5?iO3hh{1mWUx^9IE ze`uD?_|~zIxJW$;l<^Zd1td06yDf54&hC}hoosNEK)8JelH=VTvA5BhLB2_@+8qRe` z$B6inLReK3z*Du5pk@FA(4FqY(9>=yavOby}yo$=k}l+X7U$j$GKrWyFO^ck|cXs*JSBo7mMGdRhp{@IlYWv&Y^($7}%Ov6$wCeavmY zpPU#%{1>7hxXJ8|ieu|2+{I2V(}2c9#|fg(eUQHVS}87%7W}MM1es|Za&a&VCpd~q za53J>@5a^D1lpph1V(sZQ*!<=0LqGgmAb&G6c|luDgXwA5@dM-RF`R?Jabptfq2D| zgse!!Zrp%Mf8{>Lg(#{-%1u7diQwE&@}LeyhFt7@l+~70?K062|Fk5J{R(i2X2#v;({U@&A+uuRpPtH*`67X80^VJGQIhHSrYx`VK-vl|5dJORnB)Avj zSTT)K)Hg#K#Xo=6yalXg8<|rs3!3t~9}%-`Inc<|`JtxdXtZc`bctQ&n7o7`e9!&w zn<7*zbN?9sdHi)`3?kb2_k7c30t>TW`V}@KuP-!ysW>I5s(Jl!!Z>?`TG)+;^+!OJ znmO`wbR_*;i>s&zb`LV2Z1~=u6eL~sRV2%Xt59f{pJj(A0iF$`n-1bL0|82N8?LdP za6|je(BO+>&zz&*z%M^lGO##c3hL5)2poEnj+1c@djFg6$5a@I%wjNPTHaP(1qzVDRONS zeZ@jpXSGafI>q@@Q}d9Ta6ZJ4ZM>b9j`%t?dycu_oLB2hkxY5vvDt3>20wuPwtc}H z-zb-`8bx`?CM~K|Qz7a&{Qc`IIxli`fZ;B>yG+oXR$RE}^UzxU&yL`Pki=90aXC37 zC}g56HG;|eSl=PT)6!3v&C2X%2 z?RzvxCZDKpHi`Un^x!)A)%};>ECZ?NSUSZ|tH}mg0?t^fNEDActRuSS1}Pv3+LGwE zo_QZEzIE`{9V<^KeVC2qn0q&8*~WjBtJqJ^J4?8FH5OqSl*T%4Y8QwM0bAi`-=HGr zsFnX=kb(I>4KlDYvHWil*uPE`JLCUZ{dX-GJKO(<7R>FR7EEWE4POWj47Fe8pBcnW zq9yzQ1RNfoWfFOgZgY+*9F;_e1coF}90pY~EpLv9?l$JF^ZK6e`n%@Q=Umt7s^Pi& ziO&n@r1PvfFlK2^l6Mi_7-mU?q6^j^sE_?y<*%|7DoBtBWS>3?GDQj1=o({oZ8a z=K8(k4?716^?3I#25ZZS$-sbwO`QM!eEmakgBLQv+zgVycZY9s0+KP*Q*f3~UTkN% z*Pm|?|ILh90GUGn4D9}6pIv~2u-A7mIbjPo~2ZaTbOFey5MJ{z=jqcbQt66GF} z`ZJP0;lExrh=IVaU)np(yBaapo*VOEAL!{7sK84f^0Yr1JR&4Kt21Pmch?IjO#dw= zGT5`Q;T zH~Q`&?Asy`2Ohzt7q0_21I%&}BDy98`(n=4hY>5$6XNjng2^D(r?e|gUDHF3{_)WA z7yAq{Jg85f3dI2=5-hJ9kzTN8JnPNlw;yzfUmFt|1f)9=F9^jX@(fWr8u~pLq`RPZ zozD{P&w&OS;jU+6bQ?ivK% zNsv(AYVZXN(Cm}X184&i+r*TjeBT>t_`CkjA4M!E4zM7BqCy|P)3b)v_kQ~`ipIyv zZ*NOO1w){SGf2bvXE4Fo3;q%4saDZMMGpLM{A> z*x88@HEMjxqE3hUHu=WjLqGfB0wNxwas(ea!%v~) z`PCA=n%eD6=)vK`?6CT_>1AG|93kPZ0;8p)QJ+04q&M3gd#!BP)tln|=T|QZ^=kuy zoQ_=rAZL2o%k>Y8nAuv6>b~1EQu46-$%}$l1={O2;ILJ*A`aMbfxKn8h5l;@TQ-`a zlbDQ5G7@byKYLrDO0k58?MpIhz)8=-{d`v@=DLKl3!G$c!e>6^W2LqTZ}`!L87U{| z!zJXxZW9%r%aybj>p0E!5tm=7bpUCNbfEQ;7h2{3(4yd?w5ZGW=Wxz4a{ECeRmjm+ z{mfKVmx8#=9O3RY+*WFg;4~c1qi+QkS9wEPhHOC$pZ)aZKA?I|$2Sr#x<7-1U<|jj z-*rcB1X`Dzypw{85zThrIdO|n_@q=1tMoRR&vgqX-N&ZzV-{E`J*aQ9sJrasaC@3N zq^-1+2T=hTgZ!D>6u|LByF81f3WkEz%_R%9g>{B{V~Ec?zs!GB-LG>qtQ6~M;XAT4 z;D^6~E6}--bP#+Y)vaMyNXDtj9=+!{>a(vcxNztm#4(Km5Xl~H8zBz&^=uV5NLSkx z#N$*AF^M*Hp;NEwF}HJr#X*VWDfzv|LU)YrX%WvNfJ9c&y-tz2hzIG|a7%tJIkRwj zjg@^topB2T!7#HWHrTyP(S6~IJe;4h_~8Oh(1zCjKz068p1o+=<9sYxH{H2>Cvr{n zZ4(N#OJO!u2``IrE+A;ERzAxRNvn~2twQby@6;+Fb=GwV$2^-0Cfq2KKG z;!JKZ*9JK|uae}?=U~?Lqpd7@;YmW!D6|JfQgP~dLnO3e^oSkDvn=vZS%brvh#)v@ zp>EAJKPLIoUr8p%GF{{csr#Sha9Ihp5*53HRs`dD^+z9*2TE&i#fVKZ4`Ae{%Gu6j z7av^wtJnLIiTQsnUe{T%YElaWgXzD;pCMWlo+t+NMI(cewSc~SvCwLRU7lQV%1}E@ zHo`Go%rtQyLOVtD=nfS?R(P%E?kMfU=pK1V>f{VGomn^D99-H!aCOM$j&{fNSw{ks}@)w4$wb3`aoN6u$?y~ck*12R2L&}JKj22mwdBa)%oQjRUw9YZo z+x>92Bt6se`(ZYMychI+gZ?~y3)rA;ouk=G77nbG#@&kSe&Y?CBlxwN!$8}@$4jH3 z(CBh{qBcnJx+8q7P{5`r!LX(2l)Oe_dwxdc>m4?u^-8oQ_$_sbbXRL`Kv7&7^1;Xw zlk0}@6n0Dyw7kz9t9epx$csDew?W2jCF(7tfmU0Wm}x@icU)1=K_CpMZ%a=(jhIqR z;V4qJ;<&by89|*s%jWs*m3)_*DWu-??r`WVm3*Y?eFZ#$yf{uuPpz{FmdUv`Kko|v zzE~2qs>`2X7+2c_{Tu6NEUvTP#(w?;W zGP~LM^k>)$Q*)@|n3*d_Q~T(Ot+gY652M?V;ZNZ$|1oG1)0U>P65^<-Y>R^|hXK

xTMspfrSb{@Nt-(iX?G9rOtb3oS3pEiq7V=Pj zEmf*4lM}vyIYhj_hLI|L)!99CM3lI{3y?Xfq8IA-qB>*$r(O$#9m#is(68HhrwO=|~o41$%%a+V%9-e8ZNqQVr>34n#7Q(MqAEMPz z($M$cWelgc74nQzr@|n&vgJ6Sg;uWO2}fn;r~^(gk2`LH_{n6xgV_WG(91d0f9ePE z(jr2*SC3ZaX#T3Ah_5&b?se$K4?%t=-fp!=y{ynSALuOPwM$WD*p-y0Ww^RHOe>rb z10?v%QF%oF%*f8Ww4<`wU;0aHuEz=;*Li)31b|mmh9uMJ#N#UMaLS*hCiq!9X^9u& z$C`Nhax6F)R;D)$p`J4Q6qn7A9gYy0e!0kzi>$Hcv4Y`kO_KX6U*+2ta^$Y<+BT9~-iqxZw)h>`KMRGcSU_b6a`X_upLd(~lnpA}euT|E5^5H@ z=Y1*8-?AbKKu<|vgZ{GlblHny!sgcl zP#F%5UcWb=IDD3z#W75k^fp|{n!mG~P!{aV2t}y8vJF*ak<7!+Osu^q>#irLyzIB& z!mA1M3H=~g-8aY-y3e*^#9v2Q8-1o4LZYAppkd3a(=ER&O=#MnPc!`OSc7a*)cliT z@)I-D=rYS|+Zsv0CN$Ed?%=3QwWPq!4bb3Q@10_bO!PC!%~NPO+!a1W;oY2Iw~-2o zXWR$97}kTNT=qtYPvcf$Cv$T&Tw-@)GedfhTBAa4k(5YanUO~p)uaz_IPcBaTP9MC z-XPoH(KVO5{37fsDQHIJxvhI+?9+-SYPTnoN|S2O8$$B4Q|Kf-&YNp`Vd0YV#`jkm zvFz2)AzaDU_PsvxT|6Z!`-#0M`XVLXgIL4mc&iMp697rZ=-2%v*lSki`x`^g^s}ef zlkqgd#(n%VQWL@Ou_~Aa(76M9zt|f=Th+R;a@dM6@f=n1%6dcosV71WYrylG+Vgg? zzQxO_7!L`~DnI27U(7^QpU^Dauw6vR^~Y^!j%C%n52EE3QM?k>S$)>Ek#*p6uN8D_ zY%^-taQx-$LOcKQLD$VuaryD8Ex(|fsvwe>N46QD?3N1=rK5n?n|X68gCM9)Q^@(Q z8!yvAOK|0Wf$c#Pkj3EHqbsKZc+Hzr#&%V0g;dANtdR1hKWABoY4L4@NHy6A$LZe= zX+$xu3}s60f6$BHVw0tXTl|#@qnWdms9M@&T}f2>P|d$X`XR}B!ITzLk9WH?)WVHe zZRN(Hw$0J*Y4&2Nl@X9;amiQuSWVR(YQ-P?Cc7)D|=+K&ETZ%6a($Vl01;lT-ryz^NKdn}56KFjuBepTi=A z&zK*49C_j&XG`JNfdN2(&as*n4Lrx`Ei=;1BhUL5MChnGZ{D}^X`8jpVlg%-^Y+QS z6uxN*aloQ8D6|xqF}@g>aq1!MiVu2&Ci&D_9@$8xJ})AGhPSWYrSsy6$cE@o*OrwZ z+$Q68m;S-+%9PT98E7y0u6Lpg&5Ek>oovZIUYnD{;K zV2kL-?I!%6r$vf=gA5fueLG?zmhU}4NhpQ~R(Fvj_iPDNT4lkA>y+*sr;mg9@Q`3p zN(S%l9CjMz(Mn8S^hf>$B~J1XH9?Mf>%!UOzQDUe zCAJO^m1B{TW83bZ_B|E6jTXZJ2ePMK<+aMow1V+)DX+xW z={^%T|3H&`D?VtXE2FDrpzTjv5VHU~G$9BRJ+3f%9F86`lb!lSwP?jg7oVze6a2(4 z6*1@c=;)=lbRHz}PTcI%^i`tDx3`HxN@|Zu+jevJN_i9M(W0Q>yRoqN87xteHx`T* z8KrvKO6d*@kFQt7gu3akY~Q$vdEOFG$rKLTk?=eAgoxAeP6*!RGabzN>F&B%Tl`T< zm~H_-6~Z5s6e@+}$eL(`)9)FeBS|eH)7KABCd)^t&`eWpjtk@)MeA}8)}~@|UJnx~ z2)Ut^(+BCRk6RHoKi{Ug=bvqqM0^`r&+2nNUnR;%j5RF<5$1RO=TUlwlv=Q?yj|qt zEY}=@_Qf~{&abZCunX+2<(|Xuav~!qBzG_X8C8d~sadQ%KZp?OE#Y}I>$xll84A6e zr%pg42(jxMJ9@7g8o) zNp@Q^ZwIku#m2Im!YIATES0z))Ab*vl^CMi{cqL-JXsAqugVEza*Ds>lEzX%Z428k z&i$?<@DvQxCq(qCdnMd*10%p1>bSHLHY9u292(Iw{remY@;n7yb#=B~`z;wz&^dEr zJ`Gdo5rvn`8|lnDQoYL4+8-_%YjcF>7T&v(x;#9x3kD=tRqWKYSC^zW$TJKo^xxiZ z_cJ+V7R7iQZ$?fNMHyap^}D!dkMql(B z`?duOul9`dO=98%Ni`I&6B+G2$yE>!5!@b-5(IVn;z87j8X2k|w) zsi`_N4zC%ln;}v9Bjl~ye&c#dQLZw&!?sQsae44;or7v@3{KZo!Z_+XQ+3;;M3bW5 zv42wfsdi3YFx~xdXrE(}e|6}Y&hRvtwuWb=)1?&_g&x#EetbaN(yI!!Bgass*$pnA zjD|u44l+YInns9RjGubQE@d9^`Uq?@h8D8T%~8Y*W!1>GNytlh+7-Gw_iuBUPB)|D z84i|55%MgqRy>}`U!qK$+jKZd%&v@VSoopJ==sMLLMJGO2EXeVivCr`l}$LmO2ykF z0wFEM>Z$c0dMVTnNUVl&=Q9*XGZAL`z}4ioP6iv|4Dd(UoW^U?KDjSJ0^p>yu8AH# z6NYkfta}+sO68$PU2*N9jtaE?`5qT3)FcIhipBAR4+fm%uCDJ2H8cA|T~f-%jz)OB zo9eQ2py5*#|MyPR18+5_sQ=nWRUn*Nq7*!B59^gxCotRHV0xZziM9kQQ~KMc`uWLT zJej~JQvmg}cIMO|83dWY|KB}6sK zRR6Nih|H0<_;2PGz~>{WMpR%6hak0>YyBgW2OWj$mDC~MT{LoBHiMYm#DWBlzDxa^ zd}wmB7&V?-%brr;^6jdC=hFgt!ua~gEe?AjgxnEoYcM`~!OH!K`o5{k0qhwf{d;Oj zC zy0v5iU0ElodAD;qp7IDLW>hB>0!g^-*M)th^^tV-L<8mfalFaC=PsGmwj4zpGda*W z&YiM}8-hc`FEYG1$8%Ag7um_J!xv}jegWV0G*~q0daU9*Bf6*oBh`~nnaObvn-2r; z?8m0(=lRq(bo<+)`%e7r<%HlL9WX5SjG;MFPz{k5RL*cVJ`;8NJuTVk$Q=;T;W423 z@Akx@^#Q55X=Vus{fy4CSTm{N=oxAJVJlhY)6yoxRkB~~YHh!ikuEt&aHa#P*9=@Y zqIh$g@7&eu3jt87l4jyFBrCV>PS9WTCJJ40_T)ciHoAfMO&^We_eEYhVI9aEraNj^ zehhP9>j}IFGYO8vbZCzMMgD%AStWoB8^QEOO>5@69zj}dF%UD|Pi(V5AxpOJx_vc2 zFI%U=W7zSbY+6fk{+B9I=|7+8EOLd#jmRH~uw<8ARM+HjmOQO5_sFk{F|`pd(8P;z z>=yv@T zSD&cmzKwM2O965;co!*J{HV|1_029ht+UbD$uw6gu)XLg$yzo&rm2hbmF?<$?%lp= zcO*m6Ri3p3x;T*%ZC1^|u?SFkChk`^=s+&mS^r4q-!rmPDIwx;ZTT3?HV4ndihLdQ zARsfd);SvV)UudRdKWs5xBRO>F+syqN5PVY)DM-9k#KfHkMy7*B z{npara$pHBAH67*$mKx|0rMouj<-prrELkYz&DaWYr3|0+CXarORiVuYO+5`uo*?7 zI$AqR%%^_AM71!MpGX>vswzV$rp%+W^zGcBRU_8Nvo*RIR^Mek`4P=a(kYC_lq?3= zvApPJnLg-W>?tlW2mz!UuugAU2_`Jp22GUxu3!J3e*llEt5r~$a?fvM8JD_#JRARY zxv&z{)>;nS<~kggdqmV-i&~Gy(O9+_iX%D*L||iU>F8oOchmzoHrO_$#)s2MqTng1 zc%Kz@Wjt!gfZO4)dJpZ_$?xg?K#yIPP{$aim8NC6c zf^2spjau*T5BcU$K0$DU{?T|h%=d#ZLYMp2>BlOkN5@~4LM6^_%uqIBIplK*X5zOQ z&lg+St>S5UXBZW<;yw<>9O)tkKgTmymfC^xv>^#oCG-4Sr)I#m!QzQ=?|{G|!=NWN z`Ukl4!_ldcj`f8)6u7Y1hO~+TTdw0*N911wq_I6ZP448ATdEK$aXd4h`rT8UylE6v z;wgQYe+Pf5tqqg@95d@Mo8HGxX|u20xA>mvpyq?N!wq;aG6ns`1_EcDD$7H?lAlcv z$T`BX$F3Vslt{e1JVkqME?I2W>h7CS3rJz4Ej#7Anb1K-x`PQ|Ah!}j&uS8LZVn2& z`gv8~<1V{4v#^PR%5#qmY>%ei7YgWNXK{Y$RAy^E$6J3s-m3wpSM$lm+&?o-D~&QZ zk@^;&udBSt>GX{qIa2lzI}aP9{I67SlyqmPY(e!&L^QrY`rGVtsYvUs>#7%ssfgr4ZhfyS_;=WcyJgu9lfuGQR;$woJ}pQ?@o z!&VW6X?faq26z|y5g^C zl(+Z3>G*tvJQX;&$H7QLI*URWsKVavavs%lC61u=soFa z;+>>MRU@fI@8eqR%vh=soTg_5){tj7c#Jd{(`#F5GUivjmXWK^Vo2?4|QS9Ut`yBG_H$Z_Ed4R4zFG9Sn+p%t{6+%c8>2z!xP68*?@%f6SV1b zUJFIiJC3m|u$-2Kl&r6hSQAyd?(vs=fwD-lYxy>?k^ZEr2!IhsQJ8keHfM&==wF1w zQJk9VDD2VuP0U@&5XfE-BnTPSYCK_i(Cg8+NKY~w%eNYq>D7?&3Q7RIMq^g;;I6>BAiZ zyu=&^QaI@q%8x(uW|0LnIYt?}g(l<^*0e&!7DOUNHNzx>V7qhDNZT434?Q0mtgle! z5SJH>r|E~39)ZRx8J&zjO)Z&voL0g)vf5zfZ&CQY=RExr!_DYWX%FMcbL&vnGfONL z6{^f_yPa1S7dgk6zrp6$&Nq1~R+ihh=?^YbqT0;)^jF{SCzE8{705L!@2VQxs*z4w zkM8?`?YAXtO2({9HN2SYhho-MGT1=h!E8f@ABHAY%oc@Ql^>t0Fz*g4=pFt+Oyd|Y zO|CVk`+_c0?K=Jsw3+ok(PozaPMZN7fd7-E`tP)vjUB-HU(!6H{|9TH%RkzDxztPq z2Tx2yLUaof$jag@1&<%-%mNP%&jda&Lp-MgCJ9GEGWRb+wMmQ*Hdhpw$Lf1>?ltZ4 z_rG|vhTMji-h2CV_jA+oz<6QN0I5|>vmoUk1$6=#26a67v_+;se^5qse@yrz=(_qd zlDgRNo=YNCABf?f5uy>_(1HX({ss&-@>ox(r2(R#<+iaP!XW-IQ9}RFq`p5PJjOe2 z_;5J5d^-0W&dd&^@+@UAO}Gld-I zzriK4Y#MjJL99O_POPwg*Ox#ay+zm%SJeHjhr9btf3~*AES8o9qHQmDL=!jxi8czB zTQK0J!uU7ZQSgfr4nz3QnI@t3ufrLEb$woaEC_oGd*OZ*%H;`U_GADUxb_v|NogrK zQZ`CyPw$x@Xlnp}82E2@;_pB2XrECq5pVeLK?Ae0(~QZOs3t#Fi11N*!9`qjD=AWO z{qrmRKn-H6PbS>cx#3S?8rmT~WbvUW$1TBYC*Zypj^Rd#a_Xu(tHnq30C%5%+IUPM zlbd+f#$W^b+XHz6G@$yCEP`6S z1H82ju3$i-9E4t8KT7t2G{_KO>ZH5sy>JFm!U11Xz80b@A5GmC{7|Q`>HZ9d(4f6N z)qXx1I@FUmF^&&!>>qAXuf~rD2MEfoU&$W~CE0juXg9k7;h<^k{6yrGFfdVYAim#) zvw_6lg|~$H)RefaM0aY3#)>Q=;c_8mQqck8jOcmaOQlzBVm=XwqO48P!e z8L`qaVZ5nee2IyBp&dDumtg*GYeKyI>rY;o!0cRvK7w1%V9nGF!vuixtsL&p!Ms5; zZ6E}-;U#Y4cWyjhKVC-&6Y-$f&pbfj(4$!Ep=kRllY5N>nYqO4#TVXd9e@V(MS{h= zx4Y(b9^7{Swp~cJzF*N?xFs24`#uK(5JQ#qq3b?%4@C(T)pr{qa8PnTvxU5|E?$}8hfcZs#`z*{MLO$WMI0|mqzDn zDlG+Jvb7Jg78Q!nZo4>9FBsQZwqp(g0%vG!2})caZhz3ZOn2@M3;0TQH8hFrRl3I4 zk$qYhsHCe-Ibva%=vb)a@x_=S@suL@PTC%>)sVhk?GB{7JzA-VdQr#Vh@L9&nT)+Y z8hlO$5CGk_^V3;n%LZ#SFz}P9(wR9>KBc#KaM^|XABfk5LljsqfY^X5-f9AXt^2%B zUWTtQK&Eaep+7TG7yvQS1za-sUhzfG@$N-+#+zr5S#XaLb<2KwiBUEIp#%0JT!lCM ztcaNp=nm(zbzx(}4xdBd)G82vA`1kkXJR>ftqL(nL%VyQH#UKmnwNavv)sbX`8&ZJ za@tKxKNNGdP38+oaNX>DGZ0!AmP&dvl1JAI@_0&GHvx0b(q87B>${)?2!q^1e@En8 z6^s7>&??AiLz!hwBpOKz#{siFEfvtcoD&*rCZ+)X_+kJvZsSgQe@x|U zEkqC}5Vcd0l(+!MD?qOBEx7-%4;yO>(H)%p-oz9ba6oY;C_rHACbXCY@ED?;nDPcP8)sJkG zzpAd4T8$5Fv0j$iin1^DuyV`F?I?Gf`j^PHWl6Ku{<+fFHTb3Y3dC<~VVCuU*B8%% zfF(tdQ<8x(&{TKa<~6!F3PLL}`^I&APKqwsY!0#Dvq<5n!Wmue7Fqne;{+S;KBeCa z!kb6=pihYS00LS{Q@F8&3C$Z1j`wjKy$&wd10fS_%nZf6Nh5B#={*E~>M!xcLly$C zl#a5!h(&u0#p2c`=gX|qovgL|u0iOL1^#{&yB{k@u}$FR0=83lZlKDoh6~ z=n1i_M^n!;m~BdO@WowFZCdbw5SVYjb9a@u4F;9M0vv@?VEmgS%g--I(@==Po4{*XCTfnLaID@9oZSncilKAoc z+B9P?=V%=BrCU;JDoLtTl4d3*lv_NTc8RegZidbW3P+X8J>6b71_U=}!bx!7QLkyt zFVn-Z=i7@6L8Pu6FX`Flcv3&oWpQJ@#ZBb+D-U!BTBpE%V8m6A`oM|CgpC~KWcW>HMbj;LnX>Y2@HUhl4Mr4!NlxH<=Be;)Su8_1yK|r!9LVJ0V~E z=J62r8>jm=wQ^VuCv`Y^;vC=jNeTtLV4L;Z?$>SHDeSQ~fnaCv|E2%tOg^(r%amS| z+My_TOOi%kA3D~&8j(8DPlRhKWW>{9^Y zm&_+~-~wC-uf@DQP(E9@UxYx_B)eqhqJvW|7V?AKR;1ArQ>cfjzruTagl&45FTEtj zq8jUwq=aqx?mUS%7^pB_OH0{IhUWbP$&kTULmpSbRe|!^y|+Gq7UrjH&*fGj-Fc@5 z?gAgvV6ndKE`t;K!o83;XX^*}E{F|n91Nx^I`1SS1=OVq7f=sIQTrl4ljKqQ`0Zx= zQ8SWlveazN3U%JyMbmfRyNwZXfx-tvYb*Yg74x5M{mO>)XWQD!SHXu zabTe{pR9~=d(rv?V~8|;TU^WbCTPMt|D{`{wH5AjXmF!*e52`PgIvqI1)@B^1HxNOsG7^3tYGD8z?<(Gp6N%vm!xBKmAj7Xm~ z5v_-aq@Cp<-aE@#zsu1O&DXmc(h`ke_wxA?KtmFiYOI z(?31B#B}SUAHt>k9_1+*MXhLIAx)pT$8#*J&@Azy-(a#s_F$6{RBqOJqL)d@;6YB( z_vhri_OM3t89{$z1$xtB!N3W&^iYY$KL^353g&5EQyZ)CjK%1#RI*vnXSp`xsO&~SWQYh|wl z556t|8JKM7)*zgY4Ql3De0MhXuCq>~msE~mLl)4I~1V= zBh9gOtDzCneY(W&1dQiO794$}b1eoIYL?iDlzRF;EIQf9qBm$))+rWRjmi#(WH@EywQF1yE< zc-gBQW!lDcGt6_Epp;UE>>YC74DUNww{y{z%*5EVt#L>(;#`TMz^t!DlgIgm7p*P{ zZ{cXHBs<03&6nq9Rk!Ho%o24l$Za5IGpCI4_US5p7ib$QAOG!73QsRT^McmwvN5k} z<(#+3Mt&m0wt3wTtZ79wAKb#}$rxab#|>@(kAsh6suutCy%P@PV@bWe3Xb5GFY1zZ z|E4aZonB3Nr+SmQ#<0pL*;ZN6p4-%e2&e^G2X z)9~pfz~+c9B0wQ1KhK{rTGmFw7xkNGDp9%UcX&tCve$QR7o9>6-T1a|8Y2e9kLC4q za?VjR-WXNp#SDABtA1O^+oc&KEShcUpRxu#8I$vY3r_a`OazU>mVm4mmhO<+2Kr`X`8?fBgkala#VYP);Eew zMpQ~%>MpE#3HEHe+vS@w`Rg9FiUVYdnB1<_x+UJm5-Uz+ubKo(GB+o)vmZM-)|X

A*iP8j}$ld~cgFa6N0lS0(S-*>8-=@su+umW`)xUi#-L?}wovY(4 zGNf;sLLmOy2tvG__2IiBf}QkFifTZXP1Br@PJtFke1=t71A8~157j9H5PWS7RS5*| zv3VtS9j#S@q{NlNwmg5s96DLKh`krxBhX)`|N4<2?^)z^ss!h-G|%|X14;^hcL+Rd zH$4E=5~|v+I<&4#@3765HR{kQpqVJg6ixdZorI?v#kfKlcGthq2Zi3%ea=aPOa-624#L5bS_oA(ApGk)Y}335 z-b)9GySO*5OY+mm-rJiv@MW0jH3JNnHAvW~+h@|~Iv`?9T;fea%OJGG=*EVA2u_1t zvZ7rVBhmU>$iq*^esNRTAW`E!qA2trc-UObtz#K%JQCo090kudFD$O^ry*gJkD-=0 zQ1U2N7LGGr^T-Uv#ZdBL4ej|eorOhw6--WwvL*WNHtVYCZFpJqvc{!;)i@UjNF$%6 zd4n`7%33{#t9=ZnthW9s)$U;V*dAu&r5-}I@={*CD~y`w9iDz~R)6a{wNav{Rk(2gq-J9kq zKGa*yJI6OA2}K{|f8gy`N^+zBr|JE5sL zJ9EqwEc+_ea}P6Pry^_hLmyi=pqhO8m!tkAVVnf9+JqA~IpK&K%=O-e*ZYO5d5z39 zX{c9-49$jBvxfmj!G^^_)rVayLEg&iIy7^kKHfqb14I}BQ%0#mr2sdN4aCLA z+*bMg7D4g~>hd~z>#M`%S9|T&Dy8EinzvorYnU7o09T$)3)T<=pyV9rX{NHEqis-4 zJK6er2>o@&HPPaov&c2n2b~er(MUaK}R!gA-V@ z$O_ATaV>Z1WWv;AG*a=yXI}E#v0rXVqsEGIf3{FwlQz!pm}e7b%=jb%iLk%=(JVGr zj7)fixiNJ_W8V11mLe|1*&?YFm2-KBoMkY2(4{>GyM>`8`nEq<@>%_+^CcA@5g{q3 zd9G`eM{hl+ki*hrx;KB8U2zOxPPN&gH@4Nhlh@Zz8Td?&ZWvum8-d!VHqb-}hr2Bqp&)(29aw;M-udzq;>aib|Qmu@)4BrnZ-N8B5T*5gWq&mhFPB93Z6ylqH1mH_$8(}kUQUzbkAs* zdp&)e%0NXs`lz9bFx?(|F%N1t#VH5M5~un)mcOJ^P+L|>FLp8!S)!t?~=nd^X z#?}(QEeOfUKkb#oQ^StV7z|lJwT*J6PL{H#L8F6iN0;PyMvnDEFXuwDl?u9EX5x9z zQ}$QEp2JWic<7AmN?p=UK7QY=zfFg*-)W>XFx!!VZl;>H@u{|^2zOGWtzbsslgH`! zGfnF{Zo5oZ+%9-stFW>7ws<8>O1#+F!AI=$(B~AeV|Yong{TM|9La8W8oXqvMm>cQ#$@ZOfaPx(dPL-uOH zfPZMA9E?4d@Y4-QBdn$+QIF!*8{)X9FAEr?=k{n8>6Z-%j_+fRoJjAespc3DK&V=- zKz|`C0ohaO{WOXMkj03eEATeZ^(7z~mpEyC=r$+0q04)^R;$c4Oh|s>rwN{oaJ|P- zPc%{Yktiu?HL+f;IXSLJ{~h>uo0c3ej<(7iZ!y{dvi|&eyYuH1)lDSxfHqi6mKtBQIxm&EGJTa9WHI~dKIzB7M`#$9NkNE1I{7*`MExDf^cE% z7LwBddh9jlN1)Z?*3U&kJthn5!;>%9>qev1>P-H(Q%Pgl!HnCEhNhDxZ^&UW50_(O zui4$CMMUUO*9zHNPF^chLpg?T3c4AR2zJBH=M)+Uc~s%L{^PC{s;cAE%w0MYy(clL zS7jtjsA8i&VlJF=i2XVG{4XFUDb$F;`FRB>I)R`#$&%xqg1z&lK;&)s`xruY(csO( ze&sF(u~~|~={8meEyMdouD<6qaKoJfcVL~cfP25<_m`IcERt0I%ISf&b^5ROq#^&# z_6s=p8+j$Ssq=FIAvb&_GR}7HskRf-;7KW1k+OG|IZ*bY^`Jw_ahI;#W4#WR`cSu( zr*_f3rt%NE*Iy+JU7wiM;yGHkoWwTgD}3dhX3rAcZ9Ep1@Xc6g3Pf+r;Dza294Y!9 zS2=HF<=QPc9O$l`@N8a&X0Q{byO`}*=WrX;M0(j$bw91=o-S<=Q9>~lw*cGl15~+{ zSG#WJJt5h4@2sPSKTVr3y$_^<(_~@JFL=_PkDsdCgr9YOI%E%i>YA=A67|Ug;rV2l zB+4k(!Ntf|L{V~=&qUv_b~%&JrF+aQxVCjU(Fwf@J%{F()(B-2hd)6qL(X=%jAvSs z0x1teNfSuFptN!?yyF$_5;4a-jOI|4pjjG$ZajsoE3&VSruVY1KTPRc1XUp=y?=0+$pT`X5Fdlxyq^92eYM+Sc ztj$x|ij$^aA!9tbn3nO`{8b@Yj-RFoxSCCQF&BDE;>#0Jt-)TkU`HLtYFA+;zwHVX zoV76{zYIxPb9rmSUBIhIt-;5YzH5irUx#Yl!-kE?4XF~>9jTh7&5p~DRSeHUfgfHj zQA3es>|kfKGC*ZOinU<&>768R)WtA&Gc+5`Sn%WR^&gn<3OGyRNM`Z257`&(kb6}b zqZorKpr^>Rl#AI9Ce3$eV((2N#{4HIuP-uBzF?V}f zTtJ7PWRc%F*y8-Vtx3t`xCmS6Kx#J!$EU=h&Ho!T5|s4*KY%T^{|jspu`@CKFJSfm zK&)((W$gACk-Lu7+>uh&z=vGL!Bm2ckA?PXZB)t^b%~ia#pCmS;k{iivj}0qK7x2+ z_h9!-c1{k|JYP;OY;H~Un^Ey?%;>z0Pt|XCINjXDyDc6btlciQtu4-<-jHm)SFg1z z@R(+K&$I0(QP{1WxtDDYzGWD1s?9S)UZKPRudXY(RD_BSto@Vh{QpUnhRGu zQf~yESF*B`e!f$1cE~tG{I-k z!2<*f?gV#t3lQ8xa0zY+9^Bo71sGg{yE_aPU?3TL&b%^ zrbjw4wmW$)201;+hBPVzn)1+|`s9yfR@pDouP^Oq^z#NCP%ZH=tyzpaQr8@Eurahd zu)0uJ!t7%FjJq_qJvp`l)WQzp%=p#sE@QLB_J^*uOOKDED6Se)rG9 z6%OUYuYP_%Xcin{J8G{HW~S@^;{lDBQe3k3*{5? zp#}Bq*MP+H&q9BY1<&7Q!OhG4e=Q42T7OKcIgD6{jdr3{t%j5=51zE*lhB8|OEUZt zbwOOY%;lk$Q!MAJeOLZ5wfcJe%l^4E!S_jRHSq^mN6!}*H+4NMZTJPWwdbq^1cfVS z+L-Fy46f$rmuoIhR{GQG1oRmBt9Qm?T{E!M2;Mvy$C6()kS*)!)q+L^yM{zBQasTF9~c_D~#pn8S(}r{>D5 zv%K?;`$z~b3IRaf99$GytaBH`6q%t9@ti_$CX(8!ycc~c?#jm(#$Zl-6f7p77p3YY zRp=UH!;dZ2%xMph^~m!Fk1E;m=98wuva0QgvYPv{`--u+a{_I`?~GNpmxr=WSyjRj z3zLpF+IAp!5D@4qigQNQ{W}|xKw_SEs7{o>9v<4O~W1m3jy*d&>s}V>b zKsQM)8GeZK9(hdYDz=r00Ctiz!X9^e^W~|h`T1$n58vj8J!}oET*v;HxUWn}FS2N0 ziG*mULw(jgOGr8q7m=8>e> zy(0{|YqK*VDiET_u^OC>soii*_b+cD!Mja71uv+lTqUk8tfQ{g_I*@vrJc%h^wroQ zQ(>b6f6%!mb{8e5@++8>d1WD0l%zWPc`Gxp`E3yn)E`>zhBULV-zjMQ?AJK^b)MRZ z3^YKW565Sh_BwB3C26`79yD%`!1hTIKVib>Y2W$rg$?7;<{)Q&{1uz`F${x+Nef>S z*VWqo?qD(_MqF4cXnpJZyv(zEbjQQMoBZaQx#CK;VDJ9@Ku@!}FH^qdnl_ z++XdV(zwsT5J-iiv&;`V7w+A46;u~(hiSbw4u;d4ob^+rVb0FjM@MI6e3Y{M0%R&_ zp6P;ua2!-T}4u>cGEHhp57OzT;s~>-~POiyX!o%Pnb)&ym4P3 zD>M+$WPNArR+n@6(85d1eLu32c=q7IDce*DR8!MPn{ZS~@tN>R25x!{z|8?Izw|Lp z#^Sphk21c@rn6TtqZV2bHp^!)=7N!She=@(s6M!&2J$7~y9g=PC;UxJLUhZ30a`H{ z)={yXP%WMJl}!?;1751C_j4CShXOhVB$CDq9@xx9IH&@&CI03?SSw*}D;;3NneD1- zZLADsshN1$9s26j<>3fjYTm$#a@tg{`cpSK=gFyx52CS`E83QG*I zBfHJZwI1@v?>eDSRzQ`P5)^X~<)e8jI7WvAi4TK3gD8pkbCIv9G&Ne z&kGctaVw-QZ%KbD_ZUC3&UD#1&oviP;5+jeuY|_Sdu3iMY)i9wW!At8er`+uuDbFV z4~E9GdS|j9ohM*q70BKSm{#v+H0rnA<*nOx@q2n-7CSG`qmK#J9p!Z6&(v()zMyQT zQE!a?(BIeoG(vB1h3)jbQ1K6v;r)YTK>vYc;6(KmPE_YiEun7@sUmHWXbHki&Z#yl zY^PMewbHM+#NxdU`irRW+0~|ycfdXzJ}`l;qnUj-vpu_Gv(>N9?T;38L;fNvp@!xk z&3jHxht~%>hkKTnzi9PBe-qV$`Cmj8`0qp|2`4Jpv#aCZMD=v+Up%F_4Cg5Z;Sx+r zJbf`F{D+3s1((Bk#c1WXl&^mB?aMp(IfL56anGfvb1e5)i{BiGXk^zErdhT4tTyxA zr1@C$bHxe;3PQbX?K4SsxWzlJER}-^Qqh&)loaK^I{ReB#lO85$i zGVa0jTIfYMg41A>+&&?MPqBF&;cZaak+90w$A@Za7DS{M*VVto)l8nVyJFYoFt>;? zOE>n5+_OvKEIK3J5^#%%XTLKgW{Xw0<=A-MGv+5PeDsYV4n+VukQqKWK@y-08hha-krK)#8v=73K{_`LzwU1!Jvdb5G>Y}mblF)UDS z7T^Z2VS)v69iUso0n1o;HvQfJ3(iz?fD|}Wh2O_m!o=ztE>R!le~}sLbQm-b=j^d# z`@C7b=$=DXDX?6$eGStEyt`g8$q0dXwI+1>I=qeb{ktf*{(kH%kOzJi?SFS+obBIz zgg_L2$dco19pjW$c}%h$t&}3(pL}FdR(0xV=r13+IBaAZroC?zM1BAMopxq)K1pU| zku28;OyQu``bQ+mtasDMw49)T=2;U1V0$p4=c^Iw5I@@7+sN@|!T|8O58RBCTRt!mcFB@o7Xx|kGEPhlqc^uFniX(wPwW~1 z15XWVjS}bPqoyCvVHUF&+R+*#ciRJ?-QEC~L|fC_i8{{3x*JgEKY0oyce$)1%H(zz zo2to}wa%nE#;7?sYDDt2gQX5tHY63(S^EjrCmKdga%N*g$1ggaYX&I>?9yXlSQm;r zIfOI1C1pw??34tFzIBV@`~V`&-Z9O$FOX%5#Sj4))+;2dL3(f?;6yl^Mnd(#s%gRv@ zu0=p^D_$aSTmxJ?M{H&LPaNoendRYqh5}3z$5j1`TUIq6c ztgM2BJAu5eZH7c4h1~;B^P{9=pI!H~lQ_Ms*0Tjyn79kH^ux|c&s1b%TYmv8NbP7n z^X#-8`D+sOHCCESal#)o1OB^_@Phs`&CK)Rw(M(Egd*&AatYHavtlFXnjrIDAj_Sc zltuMyV1${9)d6m1x!*foIc(waRah!{X>z_6VE9j|MR!r4x==oNtVtDT$63^`hua4-i^= zV0hr)ck6pkXAa$7J>-nw__$H9dht0)5$ZafyOJA+Z=w~ww?NUI>CyY(|h;u=Fn49edZ*i2PT#m3KRT} zzjTItWxdlwPSqA3rCC@6GXbIXPe?@xza{Rh%M>SXJ+>{1gC8AwwMQoIs4(T0!#!N@ zgkAvVS>@+Xxd>$#G>jVOO2Q#9-%`sy?M(f$M%Teax!W;MrPA=caR&7ezn@625LHoT z@%&I%5Zv1lR}fK_z9432T6ugzuRyDy>OdTwL`baFB1V|(U|&H{6r|4AG9jJ>>2wE5 z7AfoG)F&{oekNdN92qS%qzY1NLG57_3o<(<&yublSrOOtncsJqanKP1#Hu*%znpBadq&gq*k~D?O7NqgjJ~h9) zEz_#BtYG23K7%!6R4XS+l~xmht%$*nVT(rNc~X%5tF3tZ4rQ$+ED~CoFAkh>QCf8@ zMr%5y;QWP(w;LE+iqw*)v6_=gB>|SWY!LJ&>j6E#E-l9hJ}u{n)>PgElkC(|(HpEN zhGl2j8x)+l6tCy$WXQJg!h08SeUi?ARf6rP5{Qp1@$C?$PubH||W%4B`_u$#oWAMl*6 z!4d9gwW5||fW_T2@%Ba5kN(5a$9*abf)Q+YMvc$U^({}`QdIX z;{6ylQ|qaGw3g#vI{W1`T&hxLGafzt$x4kmQNEHLWs>kUMmBZFX9Q*h^p3ly2ms&- z;ZuZ5)gRgdeq4S}5pn$T(F#kZx)8F_J|m+0?L7leQFmvDtdhPEc$>I}*_tQoSXmOI z?lQqI5 zHZna%nGv4`48zroqI;*VDq8{u0Z;MpEwyP72tis0g66Ukj#&Jmv1x$#Q_t(O=$%M1DQ_?ccm@Eu<8*I1XyD%)rH+g6d_%@8$e1yCp+ zZ+LXimnb6w*+BPB-cel{7}E3UaO26bRO5rGp&VM|DI0=8eFxc_Oyfa&54MI~u0E_D zFLlfX?8`*74^Pi!kL18ia`fPmMC`DE9yQ=6b#fJo@j>FjZ4$Z$l1wFKp|lxex9%&+ zuGb;9!@8mI|y3VEf3UP+Vwi5_`tWk`muH3;mQ=&US9RsI{a|Odbd0?_b6ia zh@N;)=>qcw%{}G}JpicgggNIPBL}KEH*F=FHeJ4*LMZ@ahjTk46AAF`-=#Zw9c18$ zQ&=_y4E^AXuqQ_OF>9NTP52|CqW7-sA2bc$?E$nmvceP)_*d>hAP*dP|1-AzUmaPzvu&)UX;$Ew%P;CfM_=OHJk^=QxD@Q4jcz){g@i7)&o5V>aZU$7 zVcWNm>EQ_E>(&?1I2VUP&eCpaCYl#NU}B5he+5Z&sqKqv1pOnZlJyHKZr&Uz@~HW) zcEdVYaeoI3_0+Ff6pnY!?1b@D@M6z1e4PuddG=B1#(YM{c+bR70$ulJm^96OGP?L4(S;4e=gC)4tZ*@pME%fM)vzmRnNRQw z{nJo;3Ptk6M4qxEmjz^sbkluGJ|kVDo1#XmJ;erJpz&HfE0hb$){iMeI?ZJemz5{R z0Pl7<=Vi~JJt&WJnBn4^V+d{rG#HZOqaBHjy(6_E$jHl9A6q0@A<-*Ad{2N!k0P5q zA&5|40c;)RSPMe8bCmGt=nH~oE6DyjjpTZn=>XMo7q;BJ&rQ6F*K-%%9lev5TvFhJ z`HcU(la3GNJQ*W841=~nU3~UAbQf-iPPDT~PN&Qzd@fUzmdwpoz0E|AIq*HQQfBXl zm|LMkgLgv~#~j8jP}x0iGxlSS_zzhrU3bizOXfuJPvE#>PExZ zw*LJ5J6{ESV5lccaMz6zNs+*|`qiZY2alvlQzB*s55J-ao9;7f4kl4(f`enso38Jb zy+NM>X+wq~!4f*Jl14|x%F7BMdia5KS;UFHZui0b8ceU&N8tlQ5oQJecEgw1*DcwQ zP)II5r03c9*=;BGX(R;(S{Us!B@|)J0-x3Z*R2_bl5^h^{QQPtMEPvAoE26SixuVX zxH4Tx!v3TU?_NicnuHTi0y$O~cStyOs=^q`sq~atj1jfLG2tCip%TXVDhiOHyn1PtN`kmB4 zgUV2}BZzkq*#Qe{97~W!-hGA8JOSNH_8R-Pr-yP`(|HZ!swDU-{_~Q8mWS{z{0gTv z%Vpy}*ZBBlX=@gzhZHiU_gK{R(4Fjdz0kz>QYd!&Wy&*sZ?g@JERs!cGr}cv`U@eB z*sGL}aOI5O4VAP&BVa-ty>~;o@Tzkmj>fALh8C#uk@siJ<7!pUth`VAX{&EKFc3Jf zw)R~~KX13a55x-v;k+jHb~P?{ZnEYt?4rcE-aST9XA?gm@(V0u|ATnA{%$=Sod3Zz zm2#zBAP9Hyo?wPbnH^WQN|iv=N}2}D`7y3=4-*!vg+w-IwsLIE@6WAt$Tmv&cQJ?pKem_}SBJpYLlYxP|t|Mi+Yc2dWYfL7XNm-~~eyJ3dn2d*ZaYtR?qH6@*QKO8#w4zDy@;8xY za1DMx;5>E9js4MH9r$8+O4P~w969m5WE_D*=K%{All7uN%QYwQCtE6O@$u(tUy&oH z#7-K3r+UtlqIw2C_QN6tZTqAb+FJ2ywuQ_b>!3? zP)s@tpv~h9bZH)b^7aAnRYP1&UqzC*`!cNJSUKKh^D2AtUh4MO%aIus@*e*~=&4GI zmO<-uSu?1~;O9I6Ucs(g@puEwTLz*i0? zW~!!|EMQhn5Gy+u116i8lc}MLJ-h~9{I6R}d%HJ=E~da&Z}`|j>|7vDFb|j=%*h2} z0&%?rfnLJf$=RFyS4~u%3>_RyO@M3?hBnTom~4uw;+m`yt~NGChIV$p`=V-L=?sK_ z{?R99pt`A(GyKs&4puNHn2VR4n~Q^mot67vo&BqeKv_#SQy{!o9Bgk)jVulA7=YFe zhAtM)riMVbe}12vm4g-j(}ez-X8p}c;D7(iSM_i(1+pm^S*f_#VzS8tIXHiBlXY@- z0kU)b&+N@WFb^mDf0w6fHRt8Yq;b8k;Abb7Q7>Gj1yTEVVq#PTFEiITBpKe&g>qIV}4@G<7o zVqNDZCycS@rErS4By>Xi6M{|gE?!KNK%W=pI?Kv{E<-Gb6Oi-J;t>F(b#bBr*2z_= zB)Fyc6v!$f#AeJKq5+vCbae3nB(^N)L&-ZS#=W~8)EqDT(9Ed)62srE8W^Z!Ec$;} zr(qZ3w6;qYx|HYZ5kY(2Gg+oRC zUCD=k(5+y3E)gL(@X$+jhC)*)&~=A$c&UvJ>V48%S5I4N|ir zi49j>HSLd2Z0I5uRgSIgSbX&&S1m{~)>rHyuD5S$FwvEi3p^pB5)90DLXV@^jhCg_ zXd0v*Wwq=%lmGSORl|25hM${KE#t{XE5;qOnxUsEI3~w*YicG8$exI36$-U$@stoI zoiGC`f&`}ISN=HEd9>6KuU!IiOmhAFk^KsoMHE53F?FIQo5A+^66YGJQ?S?{mu?DfdyRs|9F3@>p zKfAy8>*~mcUHbZZc0VO6@QUK0Qpcbs=<;d~n{95{z1RMl1$q+}eS@5JM&i4+?4zJ~ zOXKiG=d!s|X3|aGO}On2VKNFwE7{hvHrq@zgLHwnbh3_CUVYBi5U97olP)A+!X;#g zFI12PU~_x#2el-lpdoa5^NY>p^MF%j;?OWN*+U}H`Y)Nv7;}rh^Kyl`WQCW!zCHFX zCa>}2GBDZdzuV4=53m zI9TZ)OTCW0#jA z7!p5)CLEAtod@`?3tLr!(t6fbs@|XYP#T{Wu@IgFnlp9rGUfH`kCX)g!t*J87}8<1Uw{wqR%^pIU=i4DJS zU$w>e{P^;Wi;O}h%MHpla@*5L7kr{Eq@;cnEQ9vp!Zj)4!xr9fta{|Ag!#nCjotCt z%J8cE2jRi6ljje)T>_;~rWloLd`R4NDb3U;HEYrtS9W*vvn5pnJ}ug0PJ9ZywCCZP zzWyAnCw(DV?cq;W{e)LwXb_!&iZbcz{F+Y`n_2&bji(R^JpAO>XB$;;lbDP6l6!Sl z(?1YEM@lj?dObYG*`_$zX)%WqSfmy3(UX9*7LDEpC*P-)r(%bm@SWTQ=0`m-JRZsM zmUJ>r8~jh)YM^2yNzPTxO5XIX`&qwg^{%>9dIm<1IBSQEEeBE!b>v|!)HFpAWA%I5 zds5ID!K=9ly{xOiJ?Dz zNlxXy#mV6@x&EWjs>}k;Bd95(nrU#?b+Ia`Qw`L*pG%iW)b@ygczU4!2ax#p6&e39 zPfcZ0GfXyVI}=lPpf(7|#jA_Sref)73ctc+(*SCNfgC_EyiD2N-UZ0@d%>Ub@8)Lq zK(60Z^84luP+LGm0?Z>W$}TR!!Oh9TDZ$0fE($+E0VKi61&0kVmxK`TzitA5ima)f zxr+r5%==Hn{%@=jq4*&vkAz4Zw3BQA$<{NJ~hFLK8cJ!$jAE z<&J{I$Zz+$(59qF;8U>AIhVo`0~*2u5>OHm39MSM_BP>rV*@UMBYcUSvg*K1+VUPX zE;=<;95tP&<12UqW@_qZw>&bO`YlmmM@vkS0v9btMvZ5D^wX4j9!B-2jJU$>dgAQo zo35gDe0p?Ml>RM^+-SDO5UyUVb=XA12QGS=^@qh|@4HeFA)$G%pKFxQY>9*a{*Iho Y44quuo#1bUmjevu#-yVYSCGK`AMPXsF8}}l literal 0 HcmV?d00001 From 3b3fe8b790114af6929be60363928b0a32afc11a Mon Sep 17 00:00:00 2001 From: "Alisher A. Khassanov" Date: Thu, 17 Apr 2025 12:53:10 +0500 Subject: [PATCH 6/6] Leader availability spec --- tla/spin/leader.cfg | 1 + tla/spin/leader.dot | 77 +++++++++++++++++++++++++++++++++++++++++++++ tla/spin/leader.tla | 52 ++++++++++++++++++++++++++++++ 3 files changed, 130 insertions(+) create mode 100644 tla/spin/leader.cfg create mode 100644 tla/spin/leader.dot create mode 100644 tla/spin/leader.tla diff --git a/tla/spin/leader.cfg b/tla/spin/leader.cfg new file mode 100644 index 0000000..4d07be4 --- /dev/null +++ b/tla/spin/leader.cfg @@ -0,0 +1 @@ +SPECIFICATION Spec diff --git a/tla/spin/leader.dot b/tla/spin/leader.dot new file mode 100644 index 0000000..412efd4 --- /dev/null +++ b/tla/spin/leader.dot @@ -0,0 +1,77 @@ +strict digraph DiskGraph { +node [shape=box,style=rounded] +edge [colorscheme="paired12"] +nodesep=0.35; +subgraph cluster_graph { +color="white"; +-2129222505383092032 [label="alive = {\"v1\", \"v2\", \"v3\", \"v4\", \"v5\"}",style = filled] +-2129222505383092032 -> -2123624603493679006 [label="",color="2",fontcolor="2"]; +-2123624603493679006 [label="alive = {\"v2\", \"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v2\", \"v3\", \"v4\", \"v5\"}"]; +-2129222505383092032 -> -7765162563257140054 [label="",color="2",fontcolor="2"]; +-7765162563257140054 [label="alive = {\"v1\", \"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v3\", \"v4\", \"v5\"}"]; +-2129222505383092032 -> 6588154810387299395 [label="",color="2",fontcolor="2"]; +6588154810387299395 [label="alive = {\"v1\", \"v2\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v4\", \"v5\"}"]; +-2129222505383092032 -> 2345315966805697744 [label="",color="2",fontcolor="2"]; +2345315966805697744 [label="alive = {\"v1\", \"v2\", \"v3\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\", \"v5\"}"]; +-2129222505383092032 -> -6191826570015327651 [label="",color="2",fontcolor="2"]; +-6191826570015327651 [label="alive = {\"v1\", \"v2\", \"v3\", \"v4\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\", \"v4\"}"]; +-2123624603493679006 -> -2129222505383092032 [label="",color="2",fontcolor="2"]; +-2123624603493679006 -> 1712824352354559804 [label="",color="2",fontcolor="2"]; +1712824352354559804 [label="alive = {\"v3\", \"v4\", \"v5\"}",tooltip="alive = {\"v3\", \"v4\", \"v5\"}"]; +-2123624603493679006 -> -2840532753157167147 [label="",color="2",fontcolor="2"]; +-2840532753157167147 [label="alive = {\"v2\", \"v4\", \"v5\"}",tooltip="alive = {\"v2\", \"v4\", \"v5\"}"]; +-2123624603493679006 -> -6668272953674727610 [label="",color="2",fontcolor="2"]; +-6668272953674727610 [label="alive = {\"v2\", \"v3\", \"v5\"}",tooltip="alive = {\"v2\", \"v3\", \"v5\"}"]; +-2123624603493679006 -> 3020653026633785803 [label="",color="2",fontcolor="2"]; +3020653026633785803 [label="alive = {\"v2\", \"v3\", \"v4\"}",tooltip="alive = {\"v2\", \"v3\", \"v4\"}"]; +-7765162563257140054 -> 1712824352354559804 [label="",color="2",fontcolor="2"]; +-7765162563257140054 -> -2129222505383092032 [label="",color="2",fontcolor="2"]; +-7765162563257140054 -> -3505999373485863089 [label="",color="2",fontcolor="2"]; +-3505999373485863089 [label="alive = {\"v1\", \"v4\", \"v5\"}",tooltip="alive = {\"v1\", \"v4\", \"v5\"}"]; +-7765162563257140054 -> -5424058312653465636 [label="",color="2",fontcolor="2"]; +-5424058312653465636 [label="alive = {\"v1\", \"v3\", \"v5\"}",tooltip="alive = {\"v1\", \"v3\", \"v5\"}"]; +-7765162563257140054 -> 4478782874851559761 [label="",color="2",fontcolor="2"]; +4478782874851559761 [label="alive = {\"v1\", \"v3\", \"v4\"}",tooltip="alive = {\"v1\", \"v3\", \"v4\"}"]; +6588154810387299395 -> -2840532753157167147 [label="",color="2",fontcolor="2"]; +6588154810387299395 -> -3505999373485863089 [label="",color="2",fontcolor="2"]; +6588154810387299395 -> -2129222505383092032 [label="",color="2",fontcolor="2"]; +6588154810387299395 -> 5205351981436691191 [label="",color="2",fontcolor="2"]; +5205351981436691191 [label="alive = {\"v1\", \"v2\", \"v5\"}",tooltip="alive = {\"v1\", \"v2\", \"v5\"}"]; +6588154810387299395 -> -4421643181276218246 [label="",color="2",fontcolor="2"]; +-4421643181276218246 [label="alive = {\"v1\", \"v2\", \"v4\"}",tooltip="alive = {\"v1\", \"v2\", \"v4\"}"]; +2345315966805697744 -> -6668272953674727610 [label="",color="2",fontcolor="2"]; +2345315966805697744 -> -5424058312653465636 [label="",color="2",fontcolor="2"]; +2345315966805697744 -> 5205351981436691191 [label="",color="2",fontcolor="2"]; +2345315966805697744 -> -2129222505383092032 [label="",color="2",fontcolor="2"]; +2345315966805697744 -> -4811665873115766982 [label="",color="2",fontcolor="2"]; +-4811665873115766982 [label="alive = {\"v1\", \"v2\", \"v3\"}",tooltip="alive = {\"v1\", \"v2\", \"v3\"}"]; +-6191826570015327651 -> 3020653026633785803 [label="",color="2",fontcolor="2"]; +-6191826570015327651 -> 4478782874851559761 [label="",color="2",fontcolor="2"]; +-6191826570015327651 -> -4421643181276218246 [label="",color="2",fontcolor="2"]; +-6191826570015327651 -> -4811665873115766982 [label="",color="2",fontcolor="2"]; +-6191826570015327651 -> -2129222505383092032 [label="",color="2",fontcolor="2"]; +1712824352354559804 -> -7765162563257140054 [label="",color="2",fontcolor="2"]; +1712824352354559804 -> -2123624603493679006 [label="",color="2",fontcolor="2"]; +-2840532753157167147 -> 6588154810387299395 [label="",color="2",fontcolor="2"]; +-2840532753157167147 -> -2123624603493679006 [label="",color="2",fontcolor="2"]; +-6668272953674727610 -> 2345315966805697744 [label="",color="2",fontcolor="2"]; +-6668272953674727610 -> -2123624603493679006 [label="",color="2",fontcolor="2"]; +3020653026633785803 -> -6191826570015327651 [label="",color="2",fontcolor="2"]; +3020653026633785803 -> -2123624603493679006 [label="",color="2",fontcolor="2"]; +-3505999373485863089 -> 6588154810387299395 [label="",color="2",fontcolor="2"]; +-3505999373485863089 -> -7765162563257140054 [label="",color="2",fontcolor="2"]; +-5424058312653465636 -> 2345315966805697744 [label="",color="2",fontcolor="2"]; +-5424058312653465636 -> -7765162563257140054 [label="",color="2",fontcolor="2"]; +4478782874851559761 -> -6191826570015327651 [label="",color="2",fontcolor="2"]; +4478782874851559761 -> -7765162563257140054 [label="",color="2",fontcolor="2"]; +5205351981436691191 -> 2345315966805697744 [label="",color="2",fontcolor="2"]; +5205351981436691191 -> 6588154810387299395 [label="",color="2",fontcolor="2"]; +-4421643181276218246 -> -6191826570015327651 [label="",color="2",fontcolor="2"]; +-4421643181276218246 -> 6588154810387299395 [label="",color="2",fontcolor="2"]; +-4811665873115766982 -> -6191826570015327651 [label="",color="2",fontcolor="2"]; +-4811665873115766982 -> 2345315966805697744 [label="",color="2",fontcolor="2"]; +{rank = same; -2129222505383092032;} +{rank = same; 6588154810387299395;-2123624603493679006;-7765162563257140054;-6191826570015327651;2345315966805697744;} +{rank = same; -3505999373485863089;-4811665873115766982;-2840532753157167147;-6668272953674727610;3020653026633785803;4478782874851559761;-4421643181276218246;1712824352354559804;5205351981436691191;-5424058312653465636;} +} +} \ No newline at end of file diff --git a/tla/spin/leader.tla b/tla/spin/leader.tla new file mode 100644 index 0000000..e699516 --- /dev/null +++ b/tla/spin/leader.tla @@ -0,0 +1,52 @@ +---- MODULE leader ---- +EXTENDS Integers, TLC, FiniteSets + +Validators == {"v1", "v2", "v3", "v4", "v5"} +minimumValidatorCount == 3 + +(*--algorithm leaders +variables + alive = Validators; + +process leader = "leader" +begin + Election: + while TRUE do + with l \in Validators do + either + await l \notin alive; + alive := alive \union {l}; + or + await l \in alive; + await Cardinality(alive) > minimumValidatorCount; + alive := alive \ {l}; + end either; + end with; + end while; +end process; + +end algorithm; *) +\* BEGIN TRANSLATION (chksum(pcal) = "696cd7bf" /\ chksum(tla) = "c5d75fd8") +VARIABLE alive + +vars == << alive >> + +ProcSet == {"leader"} + +Init == (* Global variables *) + /\ alive = Validators + +leader == \E l \in Validators: + \/ /\ l \notin alive + /\ alive' = (alive \union {l}) + \/ /\ l \in alive + /\ Cardinality(alive) > minimumValidatorCount + /\ alive' = alive \ {l} + +Next == leader + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION + +====