From a02107c9bd034c6840e3f82fc83e65f78232dffd Mon Sep 17 00:00:00 2001 From: Georgii Skorokhod <64529579+gskorokhod@users.noreply.github.com> Date: Sat, 18 Nov 2023 17:17:59 +0000 Subject: [PATCH] Revert "Initial implementation for the CNF format" --- conjure_oxide/src/ast.rs | 2 - conjure_oxide/src/lib.rs | 1 - conjure_oxide/src/solvers/kissat.rs | 113 ---------------------------- conjure_oxide/src/solvers/mod.rs | 1 - solvers/chuffed/libwrapper.a | Bin 21756 -> 22668 bytes solvers/chuffed/wrapper.o | Bin 20184 -> 21096 bytes 6 files changed, 117 deletions(-) delete mode 100644 conjure_oxide/src/solvers/kissat.rs delete mode 100644 conjure_oxide/src/solvers/mod.rs diff --git a/conjure_oxide/src/ast.rs b/conjure_oxide/src/ast.rs index 8bfd3bf0f..90f583f13 100644 --- a/conjure_oxide/src/ast.rs +++ b/conjure_oxide/src/ast.rs @@ -45,6 +45,4 @@ pub enum Expression { Sum(Vec), Eq(Box, Box), Geq(Box, Box), - Not(Box), - Or(Vec), } diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index 1ddc3a670..851c0bc27 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -1,2 +1 @@ pub mod ast; -mod solvers; \ No newline at end of file diff --git a/conjure_oxide/src/solvers/kissat.rs b/conjure_oxide/src/solvers/kissat.rs deleted file mode 100644 index c3002d661..000000000 --- a/conjure_oxide/src/solvers/kissat.rs +++ /dev/null @@ -1,113 +0,0 @@ -use crate::ast::{DecisionVariable, Domain, Expression, Model, Name}; -use std::collections::HashMap; -use String; - -type CNF = Vec>; -type Error = String; - -/// Loop over variable names and assign indices to them for the CNF format. If a variable is not boolean, raise error. -fn make_indices(vars: &HashMap) -> Result, Error> { - let mut ans: HashMap<&Name, i32> = HashMap::new(); - let mut next_index = 1; - - for name in vars.keys() { - let variable: &DecisionVariable = vars.get(name).unwrap(); - match variable.domain { - Domain::BoolDomain => { - ans.insert(name, next_index); - next_index += 1; - } - _ => { - return Err(String::from( - "Could not convert (Model -> CNF):\ - all variables must belong to domain BoolDomain!", - )) - } - } - } - - return Ok(ans); -} - -/// Convert a single expression into a row of the CNF format -fn convert_expression( - expression: &Expression, - symbol_table: &HashMap<&Name, i32>, -) -> Result, Error> { - let mut ans: Vec = vec![]; - - match expression { - Expression::Reference(name) => match symbol_table.get(&name) { - // If it's a variable, just get its index - None => { - let str_name = match name { - Name::UserName(s_name) => s_name.clone(), - Name::MachineName(i_name) => i_name.to_string(), - }; - return Err(format!("Variable with name {str_name} not found!")); - } - Some(ind) => { - ans.push(*ind); - } - }, - Expression::Not(var_box) => { - let expr = var_box.as_ref(); - match expr { - // Expression inside the Not() - Expression::Reference(_) => { - // If it's a variable, get its index by calling - // convert_expression again, and add a - - let ret = convert_expression(expr, symbol_table)?; - let ind = *ret.first().unwrap(); - ans.push(-ind); - } - _ => { - return Err(String::from( - "Expected Model to be in CNF form,\ - expression inside Not must always be a Reference!", - )) - } - } - } - Expression::Or(expressions) => { - // If it's an Or, we just need to convert expressions inside it and flatten the result - for expr in expressions { - let ret = convert_expression(expr, symbol_table)?; - for ind in ret { - ans.push(ind); - } - } - } - _ => { - return Err(String::from( - "Expected Model to be in CNF form,\ - only Reference, Not(Reference) and Or(...) allowed!", - )) - } - } - - return Ok(ans); -} - -/// Expects Model to be in the Conjunctive Normal Form: -/// - All variables must be boolean -/// - Expressions must be Reference, Not(Reference), or Or(Reference1, Not(Reference2), ...) -impl TryFrom for CNF { - type Error = Error; - fn try_from(conjure_model: Model) -> Result { - let mut ans: Vec> = vec![]; - let constraints = conjure_model.constraints; - let variables = conjure_model.variables; - - let names_to_indices: HashMap<&Name, i32> = make_indices(&variables)?; - - for expression in constraints.iter() { - match convert_expression(expression, &names_to_indices) { - Ok(row) => ans.push(row), - Err(msg) => return Err(format!("Could not convert (Model -> CNF): {msg}")), - } - } - - return Ok(ans); - } -} diff --git a/conjure_oxide/src/solvers/mod.rs b/conjure_oxide/src/solvers/mod.rs deleted file mode 100644 index 7b58d4848..000000000 --- a/conjure_oxide/src/solvers/mod.rs +++ /dev/null @@ -1 +0,0 @@ -pub mod kissat; \ No newline at end of file diff --git a/solvers/chuffed/libwrapper.a b/solvers/chuffed/libwrapper.a index ece196ecc03d730161311c1d0e5e2ee2b05e7518..2b9638b4f30630f504e1715597b4e53d8defbe83 100644 GIT binary patch literal 22668 zcmeHO4{%(?d0*)nEQrA>g~kCVIm@vv2V3YQOR^jTXUS)uu@D#Aavj&^?sPg?XHGih zbh2e)6@xJG^}>vrA%Ubcv6B)+OFPMQLI~xLs7Vc-PRF#+xP@sHhIBMVO&p-qlX{|l z-|qLlw{PEj*lK8}lj+XAx4XaZ@BV%J_Vz7VpDLvLZo2%2kUNB%TU*!Gw=}jihC=m{ zq~AlK@R~Jiltl7!Aw-K1mrVb<0hG@1M zX)+U5nKeV%eFF#pq47YfK*`RgTz5X7LlKmq9LPYfrI_zPqNIew?R}|%flO}8KyMz{ z_wV2DgNJRrac8Qqu|YbuV<%>$LkNb+Q%u*ZbZc87HIVMh4(tQXSdJY#9S8-TT)QSt z%$=y7@wIK>@y=}KAP~8X4i>htt<75oiXhjL9om!~$@C~k7;WB{0b)*p;f9UF{r!jH zg?x7|)88~$fC~4cgu_FbVmg(}b*IvIMB|$d#2XJ}(p%zWDH_F+xRte}dV0W#p{T(M zoZ*&%%)vwtT22fq(^xaDg9(y}yH)vUXdFyv9+~{U{Rbps56Bd zyJZJTs5UjkTA_wj2ZK~jr5sgG*NV1>wZ_`EJ+Wm+LbjQ*sWEaNZb5s{*S2(I>!VTV zaopBfSuF-RY>?eWu{*P?a%c!qu{9Uk8~lCU>edRw{?3f*tZqVfM2&cF*=PiAp+UQ2 zi(?gPZO3-Tx4ZC8dysMEIDpcqap15&SV#>HW(swAn&|cUy`izbu`#6X;rjY!oY@<~ z^{vfvf=^z4SF~eOWkm%{^D0z`n}m~NREUXICmoT=h)9cW$-4~lD6@j%T8dXv{7H(h zr+5{_t0`Sa@eL5y!xe_Bfv`r1*HF3%;$}+214*oPrg#Iz zZ4|dtyb$MqlupJ< zKT<_2or#tAo^#k1p)r7_V@F>rLIIgg#p7<~T3|j?8h)kJbsDPROzi&XlvV}huG8gP zUqP_+x3;5_MV0WaYh&Pu2E@P_sy@dK)?jJ$d};XH*y#C+g-5S|QE~U^x!GAE79PbR z@)Wkov)H=NVM-S3DI7W`hSX>AX7ahQ=TKH^Id+MpplUsjpqAh8Bm&>Zn{owHj)^jk zGA;k#jvXf%b%SHkP8(pk)~};>VS$(#v=M7<1+7yWfBcn!4<- zOV#D**|8}LI`KJ(o}ap;^!&mn+N`muuV41!u{Nt5odIW&`ux;P}a#vtpeplUSlsTa_C)*0zAU z6iyp7AHZxgHo1UDCk$Jhf5s+Zf>4@TPcD35(miOoXE4jXlfxfTo%jUQx-k%?ubKs; zG?HA7SE(50x>K`%2Tt1cttMfd0AV67#jET(wY6Ft3KO8sk4flkpj4%xsTY6_TSjt5s@w=YFo1R{G7kr#R7lScmWGZDbur27%s^lrx&wOouI;6q_^@FAH-cQM`naO4TwODV zK8R)Us596j;es=aVQh1I`?^r==FYB_p>Vjau`V2HsBdTpha1A7+HIMhP%Kp>!s<1! z@VuJDEAHGTDn_a+u3Ip_Y8;+8ivhfzW&0JE?ga+OB5gh55Tp*K-{#Qw zD6+T;W2WEg&<_(G7iBhmt3!X7=*x6^(xE?1^dS4M6a7kEev2c2p6DOZ={p?yVtn#K z2rNI*N0EukS2-dTECy%~(Lb!yw>kO`6MeZ(PdW65FChOk(eZu4w%_f@zfN>qf7|rR z&9;B%iM~#!N5`x|;6VQuS0X{J@g4a#TYf#!mm(9F|8~dz9-?2T(|0=b!$iMUr*}E@ zhl&1ioxaKM_3=7I^LFVSu6arD1P z^jhrGTnEb-etjtf^0h?22GX|vxU!E>P(XL)iJ!wd-Wx0- zOXDF}VyOp1z_NRUL%sr%m71O!BH^5dIOlnuN3td4j7pqNWU10S0Hm-!Dl{C+gJA<) zh;yD}d{;-DhL%l78B6YbV9FgVQR@aMX9?UH@diuaPKi6DAzPu<4>h;=Ea9Bz_%6cn zS%!h}`yq{b7D&{=F>49jnehfojT{%@tB^xIvOmkTB0oa-Z>X$YKi?r-j!~H=28b+y zyFc#m3}jLNB7(Ubn6(7%5_y9qca8jT+(GgNOUUvAn^8JvzT&iJSdk&=U#3vA27JCEC0oAeLwk zz&8fqn*#7y0FFCs-e3vbaq|XC$Q6KxUj4m-8~QSYo%E*~a$<;J175jnY4QaB9>~ zOZ-v|QOShF^--wsgA%{Y!#^hR%RTs)B>o`}enR3rD>>xvN}Oj62Y*H4`mC>L|0;34 zwn#?S<8L_%D78}Jas}(6wMjhW!Z>4zJ)CsKmOb0KVCYxWh;A5gZ~Y^SWzW`b0ZY(B z+6@E0x4o2}`39%TTEg3oir?Fg3ir07!oBUNaBn**9G~XiUYvV?qt z@WJKE-Ur7Op*L9Kqh1gYOMENnk7OWY&&%E8g1RhHU2vim#b1K!_T$-60f!O z@QUqV0DiB;o%Irr{Bemp>m}|`O`em)SuKOu2vy|j)rJ}Yr&y|kI|zYoy=W6AHV zmzEO$e@fh0FY(B!gN1R8wqD|qwi=!zS3%7+lRS@vUBK^GuG;}e{x0I@_9_wnIRk%& z@DqfyKR+b=X~LrvzYTbewjSg0wE!LoXtzQ>_tbx{D1v*%HQG9jdv*))^SVU7y8}P& zDc6XNWKGyBq#@$(BK>{DF#)(=Jv<}zY_j!CQ0iX-_^*LSSB>D&;MlDL+)w|Fl7EA( zU+xJ&ZchOIIf=L1{9F&eFL7^q9|hdc?&FewldXr#^{T|3^(xE$EI`kDlHXa!E+LHz z;8E>Y56b{wVz-8{--qe|582*0i4Bt9S+BA`alkq4a0_ur@^7;tXeJr%3E-cQ{M^fh z;1$64kRRqaGrRzJjkfMxK@6`VzsU^wHv;(IkvRTCuEKIo@S%tF;2@l(=xFXgl*{jH zz{4UPE&ZAPuAxj1o{-sI>9upwLLrYQuoP`mDmNrK*COYR!m!LV=j>!lE@AUP+Sb*Q z&L#$ib2-%1(tRLNB+<2y?q#Jd*#pe9CY(qN6;s759{K91I;4#GIQ|Lugx z17wu8kF5Za50DuLd79q;AP*~bALMbNjtkNDCjWyx-h(-&gBum_YjqT`C#Q}zIu%6c zqCU_Qfjf5Et&E+<&cIPLZgM^ec)|05iPX?grci|bpT%)u9PshVlb2XBFX0Vm-F4XG{j17;IL@5k2e|eG*Z*-ZgMA3-jc*%+PQ@ zPSKslJoG))9&+*VR98Tf*GLIwf z><%ojnk4fb>u{kJ0V#A0^+X=;9slZ*f-eEn+V4UePTVa0RB#cpLe!)1@PZ)@bf;!2;uBM?+lG< zda#GHpJRp|uAgIuo)E}jxL?yV26@)=MUDS)$*FD+YB<(Ih-my@HTwCdgkf|-)Bk6X zXZ?>7juGm?3&Z1v{(1$A?`V2-KcCR}bwB??!%;WunbdII&mU;|bwB@6<3~La^5>s5 z{)YkMa&h}0?~sP`&MDT<2wePbb2X$fApaq_SWgJj7!cRTwXO&En*8(}2AuWqzLsg1 z_kU17{ujvnyfcXW_rS&ac^?4zKdbTcjtSy}8qRhR@7M6_A&tSr^?JA$=4cOgh)KnyPq5lS##L;0kJ&!;p-M<|W_3n-1zaY`f3WkhHaZx9gY zXAb74@CE^K*S{?2I0VGG?3fQ}_%#Snh-f&E9V8_+ocA^nKceA07a@LJ!+B0Xd{V=C z4nTZL!+CEOajsnSzeWP;7D505MoVQ%-69&kOv95JzFfnPX!r^ZKd#}JG=ie7tZ)iBrbtv{X z8je2k|MfE(z7`oN;66JBV^*W7gOC37Yi!x<5VG&OVz>4O;ObK zq>3p~*F7{OBv8knq1F}hiiB){x;{!}R<&ygq6qT=KJ}|zVxnbuOP;NrGiE_^nzie~E_RAiK$h{;t*=JkHpTYS8 z)hVCfYTdqcI*}PkX9kN2=p^tiY-@PGjR~7cZ71+1fc=$d0Nt<3 z-8-t@%D=b`3wMQkWK{pKyRzGB{+=?xX}PnZ^s6xeJ(WIx_MlGhqAuh}sBbT6SfL8F zd10#1zs%H`J({^NcIWgN0}jm@2)Jnve=!tNheTaE-`}4ZfLUN5U(D3Ok@nTFv!A|$ ze9!bHdJ8GorK;Ok$PW){bIz}l+zRuX-zkX*Ddlxj67slirRmU)gXCjA^8Is=kNe2u zyT`@a-{m8Zb#}4xNgsK954u?SJ|Fp;=OEAR%WJwM$QI`ye;9Z%=OI|um}ee55dgZwKb zueaal=OF*OkNmMY$iL|$Uz&sbjE{VD4)X8%$dAuK{=AR;ra8#ZqxT8D{Ws4+p7(oo z`Pdxf7yH=XG6#8H-|PJc-yP<`g@NOs`MaL%>+;{!ol3{(5}uKRO5bK_C0LZ^3ps4zfQ&^7{OJi;sK=Fl4>nokIA`g>Fe9db z=qLXRlIMMU)?v!O1_VF
A)K8QK~{v*KtRWu&gW84ClX+ITU{{^zo=Wa=j$38wM{p!D-Hskd6$9*!> z{yhQqe@XUne$<0m{?P#YNwPmq!bylf1(#|64+HFPny&r^Z_HmyOexCN*PxAPD z)PpJiUV!|4B+uuMS%)dV900U$;>Stee10IW9`OHfKmWf?@@sTvNSk){2FSlj^5*l? zl*j+I{p`O-@;K+}!Ib}6fP4)#bX*sPv?>1;0Q~yzS?WLf{J#<8&HnRTfc*k7PF%qL zQvvp?Xwy1L@)&P|%e0T*7x>lRwU;Tu3zh$;0rvaIzFz*AkNvA);pJz4KiN0?ADDB6 zh5-3HNq&io+uMHINxsrhe4OObXFYKJG1dw4e(isR%0EtwNr-VSW_hlcY=He~vR_N` z9I-s-djjlN*DH=BF=E^a7t6E#qXG7-@edsc%%^gWJm-%D*dHYOF=9+Y9EZ!a|K$Mt zwPc@`F{DNH6*~io#{=Z+NxoWVhBVt}_|X9WpCtb&5=juiQ}8U$^>Q-6euV6Qhz(K9 z@(llo@UK_8U(%m zc0t~>|6v$BR{{=dT;Vv`XMQGfp5v=PUXDLzpg2bMxtvMBcf-YUj4uUYEI<1RNf{={ zJ`H1rB`;=B2E!_nS2^eYLy~t8m0~%@H;}y9u4hO-W()xKpXJwsJp4q20g97U{j+-DYNYW5>JNk4!*H~%G&itS^3|ApL`q_ OyAZZv;k01Z-+uw?coD<^ literal 21756 zcmeHP4{#jSd0**lEE|Irpyi(_XJL#8Aas%?S&lJh$!DLjY%aEBz_mG@PAB_7x>N2> zvP|t@5M+E+NHi&#CK;xMHc6QYok^#Gp{W5mOk+qh)TBwqB}}7w$c!?m#Ysuyww}1( z@9p>PzJ0fgrG~aMnZD89d++!CeQ)3UcK7XDtyq^Tr1!61a(mdDB5jS0%}tTjtDC~% zMn%$p!(pPVwk3L(SeDghSqo==Q;+2C+<~FQsFmEkee3G(Y_60Z&Bj!H+3 zKvR{7U0Ges?#lrnLi1>U{TxM`fZXi$W z4?OUI4<2#w=3S}6#wO)d_bybFLjWV}Daws@xxJ&1%BA;bbNfg$+R?qsg&^qGIyG@- z-VXJGujwF+hdYSgLcVP<&MT!XGA+$J9Z|wbSKq0vu$dOGOF5O zkA~-#u54p0MuSw&byjtYL5>(?Z&RG{@97*F&=oFpHu?Ly)vJ{v#X}i;uzCsEF*`_9 zD3*D?h39$q7PsNlYu!5q->KmT3aR1YOrasqfnJaAk;X;}?#^#3B70L~WQ`r*dzU;M z>)KRZRYhUmPF2==%dH7&S*Kdua#R(gR=<^2ysM}VnVUGT=lo{QKg#(noZm|MZCq~P z{C3J4>4?zL#8@-stGNvGtz4!HlC_4*?Ub*j<70HJW9$yf*K_$!%A;J~z0q<=eQto%6dnPf-4GF7KdxCzrb^@8R+;&hMf8UM}B9c~89j zlk(x&6R~sWDZRVs&BL?fv2#`9hi9#kf1QY(+xsdw29~`yH4tC+N&MudZ0wa<5~pjl zWyMe6m$GOLa+@37t(E~Ud%5GFG-<&k$L zV(-Mi5I;V>AYT3!S(}MhofK>F2`gSE`*31foi=D zP^)iv5x`&J$94rJ*TjTUQvSA!{P($RBdTp)Ba`-!o0g5URXZ9?1hfd`1Btye(h*SXd*UC&VqV; zdXbPGRwUK-o|$rD0kzHXT%A*p;;PLyE&)KBbT*4Uyg2|+yXPwH;ghzr73w=(xz36{ zwN0W$<&GLJaI|Bo5sY+UT`956qh$yx94#mojZZC=xl5B8(P?~&!iViw`>V^IoN}kM z6BM_nfw1JgX3m@JM00oT$;yte1vC zdH#IW(iJqTTNcKxy_C!71!uWuw!DqPqv)zdk%lfQwM#T`mhz-fb4zhXYrJ!dFDFDh z5nX`UtQ7LqMWkt3kcJt$aDn691-NPv-^_&79y@pFXDG%eqBZfyrzlKI#Tf@g6n$=N zSK*qPLBTq9QqB!^%BgZSA*Uvw=M;^6Rf#T87n_j7rzRT(=tRwl*sSs?3Pw1A$(#OO z{P^jRx+Z=5l^UX}7)lWyM6&13Y;~~;jmKuuo>OSg?4jo;Cq3iiLv6d92_vSFbs7@z z{(aYbJG`QK|MyAVm-@J&-KKh}n>#z#hU<6s?2LuGvbmA5o5PXjhNgxH-JLcyH?~Kb z!oOR{jAo13d@kJA-kND`9q3=38EDQlx3;foZf|WL=v$NS?~k;%v<|eiL{g1ytNZp^ z7RG3p4qWOsZ|||Ht*R+txKbfiaec8}wXWd2>Y*K0)mUxSwM!S(OcL{Q!f_zg;b+68 zwV$f)yyT+2#6VTh)&ZxabO`-!m%hg)TbCgh`Zkw-i0Qa_bLd-L`cq85QK$F1^kYm9 zvi~;IFV*F@xbo+iezi{TcInHx(*oPi^uxM*^_WtyoUlDizfz~~aP=QzI-Vb#_NQF> zQx}jw#&kS)IP!h2{M$^&{klW1-t72y?gH}5t08DvLH?~{`dTo_`HhW-hRK3zKhyC% z;n1r)9Q%iueuGZG-}V0~reCYmce(UqOut5__qg=8nSQ-a-|f=RF+He#%R>Ik3os_Pjyr|fc`nebkF&t{=*al{VAs7S<#UvdYb8gs~$>pshPV-F^6RSt|S@` zr2TXt2IxAfwSHcpi1xFl!;^RWX(iKx=J7_RNTbZ#gZAO*XcI2SXP68N$FzD2{~7xi>ly3n4o&0Q`w-~i8rOGTBY?5pH}M= zj7weehZ)B;3rX-Ns0=+z73$)shAgbqRHl%nM!1LYC8|M>8h5H}lfT0FN9?N8uYbX~ znoFw843vc|tOj}0OH_sas~DDcpc=BUYE+p*Y8A;3$BI&A3R&9XmPQWY)rU_CS?xY3 z{J|=eH@!|(_#b9i`soLZHySvqAqy*5l__N1Spl9V1p1>)5&fu!)Tm~HmW8Yit>zX( zR;OFhN+D~bR&$FXE9O?TQpnn*)!bspQddG3;8MtnS6~1_7FOLVQ^@M71PKXQSdFVp zAq%T>-t;e2McjCaC$x%tgk48<;IHw7znH~36(3)aG*tdQ#!yg-d=~;WB$&{2K~KwDhLGQTXLvkZSKJ{I@Fb|4{gESKzg(U(_9) zht{renWZji2jO*EoRoRLTjA=;ub5@rW))uVD3Ay~8i0>0+>M_S|39m6H-4&nVAA>} zg}d=h-TM;$Yykd(!ri!6$DVyl;cmQA_rOGZD**qw!rgc!J@_laS6B(wN{`oE!tG3* z7T<*ba)n16es%9gwd)C&K6HpwSf%*gxF>qn5Wd3N;jl`NZw}zUPvLHylrxtJz(1kz zHb=kA*vAR?^Yae^`2S4dZoCz{F9zVRE8LC4(m!u0+>NX1o}Iiqqi{E_N`zWS7fL@r zFDJZCi>o(q3vW|+htpnlPfWF5g?Bo*x>u*#tu((bqceba8c5gMnf3btb|(o3e-HCX zyZ)N--!t&{7=MOw@n`WuThB4ZC4#RcyiSYTGEdhtf0c>{_B$Sk?o|BJTht!bmu3EX z=2!RbMEk7bm(guGBmOJQ-^2X-SWqbdDa6do)QSn!{YtbV3?_SqLb_L;5cATX`z2bMT zcXdo$uW*@#ZvWpy_zJ7rQ6Uk$m+-KIx`m?RzsCW@hervQvO}c8*AzeQqU}VdPo-}J z@V}+_?_(}{9^ukY!B4T$O#c?3$C8(#>EU5|aoW{7bZ{`guL*C4yV`~_Lp{YzKVFCL zEOkZNhqIY<=0LWXNvhWpg^@J&c7W7O8w&F2R4HFbrV9IPu$8ud;SY9Gv&l0CWp z%z#si6$*Lm(6DKnQiDasxdxowg%MS09dwFqgGq;n%8stKbT*kA861SBw!YD1iAC2? zc|er5Wk-c+btIWAmQtlG-t}io+01Z8TcyQ*>FqB5buyy%mvGtH6+*;{{UsZj$#{$3 z^1*NM#ftYWz6W)EigmX5zs0Y7D{pJ~joK;HKWOiIa{Gh#KzyhhhPrn-XBmUWsnE8Q z%2RG{SaO+UqlY6Uo1A2$&;_>-B~!&>rck08lf_Ij_W%5EZ6=~|L&pDq?~uM7>(|&j zl-xHqmZbeI#e9yUT#2?UHR9Y>%-VnrMXmO3r3&^rZ&b2f@5vp=Qe@qcDUJ*wsBbqS z)&JCXq=7<4nXB-Bo_msp)RoQcIN2vR*R4s(^jIo6JW`qpQH_y{e#pm z%Bxf8d@mh>*YbTXaNVD4HT(gMzeB?ZHT*6OPiXi74bN-%goY1m_#bLG))2+d zX9MuR)bN7F|6RtH5Ei0C(wiFpMgm3uw84-5K>A4l|N91ijm>WTdjNk8-z$ngOPT)? z#$iwQ=SmIVLNxL7I>wQqU83iv0RGzyep!iW3*f)Q;FooZdl(o0<-UB6re~|>XP==* z`UmSNNTMgKYL=DL^xR9Bw7017KgPVs#xxxL5C%x;u!irpA@%#HrvGt5ME_C7kwK4~ zcdXYSiJy&j)p}CXqx<5r^H z0Y9Me>+L$I;kurOG#s)>&;uT^I{}aqaI6Ul9%NVIL>2KKrbCjPf8d`Kka8L4CLU%U z6R!`z8v}6NpNE+T*@xwisDz(KG`+grM}$eEgJ1VYSb#sO@#%WTg-Of7j}Y=2$B{78 zP-RFVQ3J2zdas6KEJ`}U1?Z496F^VnhZ1nPcA-9nA4Xzzu00 zqJ%7r0;i~k-yk66y&Aq!!;fhADh+>H!zH$WJf-0>M}SXjIEu19ECC7_4p|2d<03~% za9IbA8u&9do7HRJ#~43i;IiKPw1LaI?%y(wF_>c=$fgZ`S=ark#_ztZv8);dDoXJG zqpD>8)N8oJc2MFPeyhg6U&G~^1@ci1Z_xOk({T5#jAeaS!zD&RY*xc1<^x~45WjB! z%lpJz4P55C)lfV*R7&+xUMkr6ekm0)gQ*63b}3m6{i#yQYUnE#t%gG0u7J=WpQ|Z0 zs(C(Ib3iPu&}t5Sx+akO&6*(2mumvZ7i;)_t-*1HY`7n$REvgK9P+}>vJi==#iRhTj~9-pT2b=K`7AE^Gq|6rx&7k*v04EA z!k?@K2nK$**03*~PG-i^nc-5B1{XaMI~qP{dBS0`7ZqeF!1vHN@8CPz^qmoH@+Xcy~kw6dRmkn8($BMtOPA}xTGh*wS2%>Lv+ zAw|nj4f_iDkzqR`{d&LmQ@s0#kBTT`a-Wl;`UW~UJUV%heB4LAV;=GeANkeukjFD5 zlI}mAU*_t6FN7)S@^~(qtNeZ??UiqthrFCzxtBx#W4&Uo_7C~k$34beyvZSY98$ zSkIj6`9I?$-#ZWavp(_|LvyunRoM!3|JTh!zQ#u$b8@csW&KvSk7w(-%3sCy_3^)c z9`Y-FMjv@Rv&>b#%g6t1^N_#SM;_~GbG6^^Bad~H zxyldwwEvNL$dCEh$GXH^?LX#Yf80ktOc+?PHm0Xfv;5!VflW&cI|!cP;ZxK>?85X) zJD2CR6jfKyA@k`fo2+&WLMJ~qGD`1Wq@fOC7fkzjHiS-7zL(__hJ3A2$1@&u8qHMu zxxk8RzMf3`xF!L+$WZWAwlDjuM29KAIY9nJmN)%1%viXl_}PDr*GJx zKg{{}OTzr@pJw~3h^{Bo{?Cc%XMc?CH?lDL4|C15e<>OFvtPpj=|b&aOu~NlpY>@! zcE_6bZwas;X8ZbD9-3mde^r3}DWCS^{@=8Z_rCO3F@EA~zY9jSWZJ(Y!2TJw-^;Qo z%5nd0+D`@8e{zoP-xFXz!HazQ`A4iY?H>-Xe~j&~V*e#G+mGv{-}yh{V;}eLru{Dl z*gwto@ywtn(?0g?``Q1xkA2)fn)dN;Bj~T<{4ZZ*TgCN3Pp19n1ME+;{Ye&1QI7jZ z)BXjGpy6x6qBB-}qU#*cQA{ z`|;g`pZyu1_9GUX_U{U?|7o^wjz6>i9|(|tiskFUze5P7lxQh@zN zwl93F#*vpgzAy2!e}?VHnGyE8=`iiT5nw;g_W3qS%&D>JRH*PyfP8}G&G94lMaPc= z{9nT_#~PUt{@+7~$VSDgoU}-mg~4Scc;_II&;z~ zr;{ubs~CiduNP+23<)HqiJg=nTG~mb6GA9IL``bwbULPm#w|>vFr=d?YT^K;p41cd z``!J1-`ltEz1nK?M|b>gcR%0n=lk8=x4UoO_sRFfI@_zOssyJhaf@(jj0!Q??3AOj z7!?`OEp=Bw9XYEgucv%9<)5VdQ?jsmGZ5Ww@}_nc^l+0Dz`(vjmmMzJE(jc<=ZLmg#30Y?|}Rc zDkmWS43&3Mz6 zzgLM}Ja8H{dKdqEsyDv)_wZ+6N?|Y50(}N95kG^!kVR`SSK|2iY;C+eb|GFKJ|C}i z!4-q@KgP>vBxm9kX?UJm(uQdu1a4-^!*5q&Z^s{rzc{@hUj8faHWRNp%iiJ@5if&( zjbDzvUx~f1TCoe7QKR*zd^%qKvFcj+T)cANf}^$sodGlxKmJAuI>>4&pKvSJgYvoZ z@N4C+voHkb;t$5AwIQf|Ar1}EfH*XUhR^YXBUm20SRTGG zK6bHc@$su+RopvvVQx-{#m8}pJcIY-dAz$XU`clC8C*IhhSKNp$JBFUFCbT1IdO%Q zplQ91pjO}dGy*@sAJr5rIW8)=%C!3bR!2FI{c;aSsS#F>d>KG{PNf$S7KA43(U%xt(DGUsi#7K6ar%=2p(>L7Po9(%2BwZZ33Dnm@ zA>1c&L+!cIY)}1axwfQTn06Ij7O*7B!|#{Ro`{`?`S;*;V)0Y4^Hn%uFO+L1)Y^gj z2}^H$y6X7U;xE&3Q`oB)pmE$@umdLKWWR8NxiB9>u%IhlvoLk$oCODN=3a4e%U$Qo zx6ihfV>4i71>D4sD^ulH@BInZDz*2%1p_pF)!&qBE3xzA(-utP3y{4yeMR}j#ZR?Z zg5wHRwXtIjYa8;(+gR2j}&3QDqS<>!~*D>-Ew)8)oR3cE1WkBZILP!wH#=} zfbqLrwo8xuPF`T_bmO`zj;V5qJu0`^9?5i+FXyvc>&pdFHmRY>A1j%u@8L%qI06vKR`h^;x$bB(hUNRn=#lD=wzRVu|!Ni1XZv0yN z&GXFIfxtUV2W;j0b}Qw^haLO>k=DWH>(`RzmSTD!)0Z1KNOP0cw7!UC_h>TME8&tm zjNxrtYwPAv{k9!lt3#1UcwIOWYHVn1j6@nEq57TKo=`kpBEj1AaPYj2=v8;`6jh_O zRW~kLSTg}noTY%{g{cmIwq8^FKy~ZYR~`TbsG@8O;*g{bmfzvX_baiu7IT*0?#Pdl z91mr-e7hrml;kUPdCHMLOY$K9Z<72Po!{Z`FOvKtx_q}IUy4s&NP+z)`4}p3|Efo& zfu#WLC;5kU`A*0FQIfCJ_`YfL4?6r$kR0FF zYs3CybNIt2{v5jAMZ1nvPHgK#?kUVHFm?Zf!-N$~%{>vn<$2rYoU@fmg4YWT) za@W1m)=G_hFA&0SE`@+!Px9-bY}-#L{|E&oY|aAl3pmGnlO<$tJOWEB_h1NE_Ka}E zS3|K{vr|VR+|v-}I`8u+wuIbKNz=(J)q4kk5{^fehGTy)ZG{VQu5*s>>WI_QvgOFJ zWaI-&?qrF2H$XK@U}VIbEP;^{cgjGuN*f=#-QshEbDi^h2*+m`CdMCxGTK=rQ3uDW zB``AMO_o|YF2UEJhIZt9mSrV=jPT!7ReOBCOSoL4vP=q)SpuU!?(`f~(f$&GxgS`y z1V)Lx$&yhcKO7@S-ed{+p6d}<0wYWA^a@n5Jt2a*->(ziVBlD_L^Gl8%n}%(a;LYT ziuR)fvwf^u0;5>oWI>G1FInPNKN##p18|(}-eiduF9?VwS_AO50K7c_j|bowVe=+S zV8qRvEFn(-9)Tq=8s|-xNO(a&EU_~H$Eck*S)$7W{tOV@m!6{yL+;n4WeMCpyvdT0 zKR5m{;G>A~A%`{==`Nk1d;D>XzFlM>fgp~4SK{3?(B zxWs?MgMV4#AM)U*B+k2%BmSPmdDn38*Cej*`bze164ytIIC30++c7|;)e@H{SeL9t z;vpBt6-(^rqAR!T-OdHWyrP@vh5`4EKdM;vZtW&mf*#Ut81%jOOW9dyXsW6uy!TP* zd+(#dz4uY!-utLBh&S4n;6oWpjS0biy)2YJNf0s8wSzQH!lcdj=8FG{@0 z*5@bj1AzOr^PvF!Nr^k>rOjmVd5JscrEP@&LxBCCNPXwLw4C(+OXALXiC0b-4#sub zd5KrrT6m6J3nRCY_`DMKg1%qB?gSk5yGWn!SDEn78~AgCpCX*w^CQBaB|Jv?yMWhe z=P_Pii{O!feyikjPknnu3dV}-v~wEI>?YFZbBTO+2Yrkw*NHarChQZ^5b1Z3{XWu| z1l(^No|AUkZ99`x`qu#c>*3K=CwMhDe#3zK*}qxpZ?)~qm;luF2jHKVc&n|?nVtVtQ~eTMTCg2SsvU=f?gc`NF}*9G08?(Ceng?^)O!jbYD4UcY4U5B>5{cHO^Z7z1T`Cll>Eb~JZp8jJ(4UDbrY0( z*=SR4gq7AulF6Y`x|GW#a|5|jE}hTa4Yk5RGCk0f?8y#+fsCv-7jkwG$}A z-N}w*a$lrrAbU93Gu+>QBso|tbmz1EI66Dlb>>Q~8)CU`tZc}47Ycc-Vl5JB?Mn{~ zWb+*Zy#)Xd9Xcd&{1VW%Atvcg^dA(IL6CBJQwx~elgl0k03D&#Cj5>IP)BF3Ar=Ec zVx#)9i>-$CjASz%453&Vb)oEB={ijSb%z?;xhvVRI~j9~YKm;ZZXf{zhx-%K;r8{r z;UjWpBuD;nlp1N2%&)`llLjpw?6>bmA~eiF=G2?J;)a z5gV6d-zXckdyo7igJXs_B;pKzTZ1h3{kTP&`%t5?4;kB3 z#1Okj$6hM#Z3dec8rRqE4riFKx@SkEAqk43>F(S}q!G$Pxnw2}i!xa{GMI&# z)my-&w0jrrJO(4u1Z+Qb-A%G*sE~x`N>5&ni@jf{+a#NrE@em6!@`lO-Zl z5T)|~9Fs)_F8QZ(@E0>B4KHi>*EIZuhJR1Pzo6l7Y50VO|A&Sj*YH|8FPrVTQNzEa z>9=V3LmGaYhT}T~_e;gyRQJXe?Q z{Q`ijUqxp^)@RO@gkxRTzuwTVAqO`E=&Sgh5Nv-D>4yXKH)%M|4Q}Txgky$nVmt8w z{T+rrN4E9`=-+ARbDUz7aBe?GhQ>5IBU(Gh4LdwOCk#6w;9z=Cvoj8L?(dg0{U@cS z`gvHxaU4P<<8Rg2&Oajzvs0S=KZiQof1Gg4&<Nfx9h5Pl{t>v? zP6*1F5ZBkWZUjqzwH&02lXnE6L6FaD)i) zZ)o~@zfNhmZs(gC-V0?+Xy;pSvEScE5E9~fxEK%e%j>ubbRUC@6W<@izs(@zJP%Dg zL^>v3AAmOm;Cg!=CmqawUF~6$*v?7KuI~2L5xwS%IR zhI4Ea@nag!dlBL%HJtYZ#HTcz_W;DFHJoF!i1XlL`|Bj2enJR9!fd%Lsh_BZuh8(6 zhOgA{V;a6n!%u2B7CCM_W#Ak+n>KKqLo(3@h+@1>DOAS&vB>zdghvg1jsvF*oa4O} z!g2n8g=}DU($MF4?-QDSy{7-NroURlXEgki8eW471roNOpAlHE*Kpq35sz#5S_CNN zH9X89%7-z?Xy3Mkre%5F>%6Pqt@X(R| zQo0-RQc>l7TqxA*r+@yDr2zS*<4Xa=z$jDrU?!8yj%Kohr6f!eco()U7?B58 zV8T{%2MO#zP=MTLY~2QAu)sZdo`8aHz~T}dW!Ij{Zl@gD2xzp7Y$*F`O~6d0n5PGI zW*1F6hoRyhw5-sC3SO8d^iYVd?6J(9u_vd`*f}z1Az;uRJ~0&2M?^SN=9+r3xP`7KR74J?H;Y+z$Jj-(N{Y$ta(jQc%ZpD{Y5% z9>kCP@cZY%Px$ch-Q#lo@Acv1m|ZSE<-^DKpv&d=`S5R@2cPdRpXpM-EzN^}6m&7^ z_b&?d%WePtNQT5`z7&+V!gaa)M?e>o-u@P-UoQWTCELw!od^FrKK!-=wNyi4&n`Lus@9(?up zsP6SYHV=Nn$NyvV;P3b8KgJ)p-<$`HUyqOf$LGNx^zn~z3--%-kpEHQ>-+a@KKu}1 zsCp$_dio;qe~B+KS|Zp+@Le9;615Rkn5tKKA2l=u)n#z;d|IN!^#3iKI3K~{0q!6J zl$-w70FE~4HPhCfAb!F|RH4?WW1J9e^7jW8GoSyiigD9FKGP91hDm&r{NtXZCzFqR zil6@(;+yR?{p=6mUm*Sp-8qy^K7MQQ^Z(H+6p`l-n=#veZva0+d_Bg5HcUQ#^YZf_ zCB7a*LcZC4ToZo$&l0~5Nm?@fe;Z^tR8hllJp~zfo~A&D=Nc64cfBzZa|61A*Rm3 z-+zpgnf~t!@c%3FkNcyZ%>IuB_)n4l2_mN;|1?~t|33=w-@Z^0m#fVFHT`3p5dL}Y z-y!1T^HEPG|APSj1H|XQKV};yeAOQ;VMPERR4b#;J=Uj>-~@W_`enoUVi=$k$-dk zfjd`f4B+2Q{ADg}@BQ0F{A$DSN#bLh^~B@H*bd)PBlD3JCaD@XY6NIUV3XO8!5@ zjwok7!#^gz`To#J{8g+-xiL+}KL@mb#;5&zzy|y0_T&F!@mqf-^1t#D{yzxtzXT6! zko57}3w6`~hhgzt12~v*rIX~J^;yVu&aVZ&Tz{-Ud7S)nKU0A3gNu2LF9$OApW6vV znI_3UEn|kIE>@6(X$|pJ&H4Qi@f}2!n8)~5;+yyN9P#7E0^s&De+%&8pNKL*d5Zdf zo(47r_?>VupZkyPF?|ChLbdoS#3Piap`3@ynWH|=TlFvS2*<5VNfNOI)-JR?M=}x&j z$uhNrjUeNzLZfNPG|4cnX_J(h(3x}^7@8W8!!(98Lrt1wT*5S}hs-F0TAY+LZtIEr z{q}v|dwYBD#ZsG@?(lARf8XETxBKmT-;;SF+OxSP5U`{Kta~lDC#YqeX?5EX)r?qa zE2Vf>Qy((7bKSu88m>Ri^&MQ_N%dXaZshuIs+;Hv)78va3)O464fAc>Zl`)3w>zj_ zPuC~t+Q8U7RNu?(`>2j^dn4DKTz7FD<$5#MTeyx<-OcU$sou)%9;&x-dpp+;a2==m zlic1x^-ga0Qr*YxU0gp%^+Vi#nCiY*`6uPWbEl#gE>ihm$vcPVCZZPt6Nl%l(SM(e zUfBBvI0l!0I6W9!{%QQ=rfux?Iuf6y%Zi=CFIACR)HXRbF;^EWA3h%|kDiN7_R$rk z_77v_Q%Yv)Ev0yYTuO(jAVg+n%cJj4M&FNpA$D?RQLOwevNjtFoEB@bNh?++`m(CaNPVFBZ9L%Ke z9!nOAcN66vS- z+0(cM5~=HgowvgN*WGT0UqoYbJXiM= zq?j7BjY|N~Hl594FK-S2H17FISMbT$*$T~_u3TruoZ2QaqHdz_OLJt6LYxti4pr>IG-H zZ?3$J!lUS_Lz9*+DYaX)aF+3=PI~7@k-K-Sy=_1m!El9&G9bDk} zU=dC&;+vhcI-(a2{S3|6WTZCs^fZNO={W0vh@#Jp?J8W;Feq3@Ps_cbNjX!lA>_;? z^qirUuR4)M>aYnqd}^~%fR5Lmiq0vYB4C6Q*u1Il#ZI0Lsx#@^uh$Y?#ZZdyAd)?I zXRE_1I1!!0c+OxvbBA7}2ODD+hA*JIN8*`c3`h%VU339!cn(nd!JQf z1*U=Fq(TXBf2rNIuH`!L_zo*DUKhA&*^=5RVqQTwE|hxwY`m)OGc{dTUbdGQs0-Q# z;8c_jp+Df#_t<3XYScpC=F$%_9S?5~eXC1DWKS^jmfMBd-6? zG5sc;zRRVbVETlduNgnn{rua*^eB|b{M1C01DKyf zOs}|qG=JD)pg+fSyem5LL{BjtaNzNHkJ`CQ6mwAa?<%6np4Zy#@BI^Js?`F*Z@n(25qbm%qqMh_A66w_bS=`_xoKXY}w@N0BnuHIz2 zUo4qrdcAH#i)FP4m{hL7o{)PLyet3@LIgDko!Sn4v+W-szXElOte;)RVKvkODkwKNVB32TF8`Cm!O5rNo7eg(CPf)P|mA z3UzUGgBCJ1)g@@D6<$I367`@*tvl7W$zNgoV|Le>*S}(1?IqP_2C9M&s34#6yQ$#xho*K2Y0Rnp52M|ImIul+j3U? zSD3$#`S-J)cM12J{|}WO_gr|9`LCxC?8U!@@OtgMh%_T_`A0&LG z)$6E`2;NV4$U)skQSm?M0OG@wgiG5YQsZliA5YPCq1&g*H+=ZtRs0V#7rl>g>!;wS zSZS93@X=!(C?rQlGKI#}$cUBL-P1OFa45g8Ig57taAvr#m`RUOXJ@G=+%b~Pq%sGx z#Y{qdmMDy-N=#}=4h`i~$x^w%Q^!!Yl<3Q)GlNbqS}5cTPH%H^ zsHiyCfwQ+Tsyb~$PP2U|;qXw~(bb;HCUT=gL(tSdFqSB>=sIc-iqiJ%m@uskClbX{ zvXo6Fvbk(2n;gnMPQ83Ck<6tN=}eInq*T9&hP|cdfzFLRBr!UW=uRYdhud?R1BvwL z@bJOJNFhHklo`h4Y;WnwmbzM_*#UG~hX(TbA#~9Thr9MCbGgh=cWy9G;G>T|s&FI% zH?>BUxSRYV23sLfrM<3`)a}Y<4iErC(CT2Kq8(q3h^MsX#?li$YzWh}{*9?%0{=?oCA1s7*%JkUKCOSNgZE?WM0&sj)1Z!z?xPEU76A z+nu#VS}HuW7W$?oqvV++5p7;chI;L#d=I8sQ7Y%S*_q=?JnZ0V?wgfUy}MLK7WWW0 zB_fA-L!Ex->1!th5X6+&m)kPGg;TX(hxSi%Bkxh>qc0Be^YAn7poKO=IZXHfOmPyb~pmB)ZiHVneKhCe;3ZK&>IWMK^Wd_;`XsdoiD* zC|4r0O|E`-wMM(bp4+?4wpbMnyp4(9nqJ%WzTANwY0@25-nU!pb&@C03gp9M$-IG$Yv{{=uQ!1vN6cpX3I0@wYyNy8u2_&YUx zNW<^f@VJH_(D1y5PipvxhX1jKBZnw{zTkuZwT2fo{_iq=IblJ%q`af?Zz53i&lvoe z50szy@PB0R*V^pXfBNv(^0T7&vyAz#WE}Q%f3DN;ZlZ~wH#3e3;}Si$`|#go@JlA9 z-G~1kgJ1F#4>B(P%X9f2P0v=%&jCY^%n$M@D558%dX|;b^gKkEjJK%qKgGPL#x)%C z5CTZ$u!irpA@%#DrvGU|ME^0yQ9+N~cjRkO#Lp(XYdx#!(f$0Q#;^PNCmIg@qUX;w zT=x@s9~AhZ`zhbn#GeS5sGQXJ5kq8La(|!)Z+(JGrVo0y(N#wm%C&Z-?BeZC_(K{V z*Kl1AvNm3NKB@6bUdyyA`5*Y%tMTI-5(@b7b|?Df{T=+9=@LKj_mwEX@wP0utanpS zhBa1{G?ZJCuZFakc!~H zV|ShWhTt0*mrNY&K0=rHvythhKazn0en8{b$8}J{bv=)3IAl?v2RveT5+D`e$O#GV zXIJ7xfOrqnB}MK(@J|a!wXAa!4>6C4H~8R9KDh4B6U>9^H|3A0gr7$=y}I3_!lco` zulpk`z@OCkbUhQoq}AX@2zis^NQi0ZGNh1*f!A}tU&FB$r5xb~bV$ww&~f}w0WN13 z`qTKK0$lbi`ZM^U0$k1_1;BAC!1b>PAq|(k2EK@f%bEe+ui-ZW;BrL6C07a3aSfLk z1$fkXEYp5$q!3_0)|WSz#$xRR0NkiaKyl$x7nu|80u>eb|8do_e;PDgVml}?4Zl<4->>0vW`TT6!y7gJ7d71d zDq~sS)o_VX5S!C*iTS{nEyk}q|METYP6L($%T8#t6qSaW)+Z_-ZRWgARH;RpV+x1kG10uCTuaK0s6Ufa(3F73V1d#k5vQmwX zD`dk>Nja>Q2`ElXRS4N>C%mwFz)0g%!tM*5diAX&;^oi-cG5ybQ^}-CDTl0HT>WU( zu1Fe5ODCM%0rGNlO@~j8@?F*3q0?X_EuUmlpmp$Y=79jt15Bc>AkeBBref*zTfc$9> z`+F83|DK2Z-UZ0dvb?^2k^_amiM(Jbyw0Q`{{a{to~vUI{CGcQTp~G19cF)VcN&LA#|GZ z{VX3h3fx^YXvn!++#I%>DOE!o2LCW&5j%t{2n(&xz<|f1K?%u`uQjd(E_e6&d%k zU&{gMQsZAr!d~`Y@EAY-I@Yv*hmZXb+t+h>7>YUm)jsy8J;smcf73p``_g|^>nFzc zdtg*6ru}<-?4M)%{VbcL8qe>h{iKimXXiQoJwEp1oaEE*KVqe6|FDn!6KsDq`!AI_ zew>qD_y358eLTOL_P^+3|18_bJA+-fwu9?5ElOt-5h)oA!U(8A3M}6d>OXS7=t3LLd*uL95_y@I|Ms!p&-SknLtKlzz}L~_;TfOQ zRFn~xH~FP6_0=S==D$Lk{>F~|7eC?uZn{KH@LNeZK)8%k)Qq!zj9D+>MUnbWmbX#& z_a9i^MeLTy3BG~kaa0)F&pOTWreET}$oH~+Q(ivq$BYGJ%0EEz^q&z!kbz~9V!EKZKTVTN0>41Jweu)75F8Z2-sa`-npy3J$T8F O@W