From 1fc339f0ef2d3cbc3a671625f250b63b9f72213c Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 13 Nov 2023 20:25:25 +0100 Subject: [PATCH] Use `ring` to solve Alive theorems (#134) * Use `ring` to solve Alive theorems * Update mathlib version to new `bitvec-ring` branch * Mark `ring`-solvable theorems with `done` * fix: fix FHE proofs after mathlib bump. --------- Co-authored-by: Siddharth Bhat --- .../FullyHomomorphicEncryption/Basic.lean | 3 +- SSA/Projects/InstCombine/AliveStatements.lean | 25 +++++++++-------- SSA/Projects/InstCombine/TacticAuto.lean | 7 +++-- lake-manifest.json | 26 +++++++++--------- lakefile.lean | 2 +- lakefile.olean | Bin 0 -> 111512 bytes lean-toolchain | 2 +- 7 files changed, 35 insertions(+), 30 deletions(-) create mode 100644 lakefile.olean diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean index 1466a9e91..d7a00b923 100644 --- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean +++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean @@ -304,7 +304,7 @@ theorem sub_modByMonic (a b mod : (ZMod q)[X]) : (a - b) %ₘ mod = a %ₘ mod - ring_nf repeat rw[sub_eq_add_neg] simp[Polynomial.add_modByMonic] - rw[neg_modByMonic] + rw[Polynomial.neg_modByMonic] /-- Representative is an multiplicative homomorphism upto modulo -/ @[simp] @@ -325,6 +325,7 @@ theorem R.representative_mul [Fact (q > 1)] (a b : R q n) : (a * b).representati repeat rw[Polynomial.add_modByMonic] ring_nf repeat rw[sub_modByMonic] + simp have H1 : (-(a' * f q n * (b' /ₘ f q n))) %ₘ f q n = 0 := by rw[Polynomial.dvd_iff_modByMonic_eq_zero (hq := f_monic q n)] diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean index 928b7c5b6..cca5e0bb7 100644 --- a/SSA/Projects/InstCombine/AliveStatements.lean +++ b/SSA/Projects/InstCombine/AliveStatements.lean @@ -1,4 +1,5 @@ import Std.Data.BitVec +import Mathlib.Data.StdBitVec.Lemmas import SSA.Projects.InstCombine.TacticAuto import SSA.Projects.InstCombine.ForStd @@ -27,17 +28,17 @@ theorem bitvec_AddSub_1156 : theorem bitvec_AddSub_1164 : ∀ (w : Nat) (a b : BitVec w), 0 - a + b = b - a := by alive_auto - try sorry + done theorem bitvec_AddSub_1165 : ∀ (w : Nat) (a b : BitVec w), 0 - a + (0 - b) = 0 - (a + b) := by alive_auto - try sorry + done theorem bitvec_AddSub_1176 : ∀ (w : Nat) (a b : BitVec w), a + (0 - b) = a - b := by alive_auto - try sorry + done theorem bitvec_AddSub_1202 : ∀ (w : Nat) (x C : BitVec w), (x ^^^ -1) + C = C - 1 - x @@ -57,12 +58,12 @@ theorem bitvec_AddSub_1309 : theorem bitvec_AddSub_1539 : ∀ (w : Nat) (a x : BitVec w), x - (0 - a) = x + a := by alive_auto - try sorry + done theorem bitvec_AddSub_1539_2 : ∀ (w : Nat) (x C : BitVec w), x - C = x + -C := by alive_auto - try sorry + done theorem bitvec_AddSub_1556: ∀ (y x : BitVec 1), x - y = x ^^^ y @@ -82,17 +83,17 @@ theorem bitvec_AddSub_1564 : theorem bitvec_AddSub_1574 : ∀ (w : Nat) (X C C2 : BitVec w), C - (X + C2) = C - C2 - X := by alive_auto - try sorry + done theorem bitvec_AddSub_1614 : ∀ (w : Nat) (Y X : BitVec w), X - (X + Y) = 0 - Y := by alive_auto - try sorry + done theorem bitvec_AddSub_1619 : ∀ (w : Nat) (Y X : BitVec w), X - Y - X = 0 - Y := by alive_auto - try sorry + done theorem bitvec_AddSub_1624 : ∀ (w : Nat) (A B : BitVec w), (A ||| B) - (A ^^^ B) = A &&& B @@ -362,7 +363,7 @@ theorem bitvec_AndOrXor_2663 : theorem bitvec_152 : ∀ (w : Nat) (x : BitVec w), x * -1 = 0 - x := by alive_auto - try sorry + done theorem bitvec_160: ∀ (x C1 C2 : BitVec 7), x <<< C2 * C1 = x * C1 <<< C2 @@ -372,7 +373,7 @@ theorem bitvec_160: theorem bitvec_229 : ∀ (w : Nat) (X C1 Op1 : BitVec w), (X + C1) * Op1 = X * Op1 + C1 * Op1 := by alive_auto - try sorry + done theorem bitvec_239 : ∀ (w : Nat) (Y X : BitVec w), (0 - X) * (0 - Y) = X * Y @@ -533,5 +534,5 @@ theorem bitvec_InstCombineShift__582 : theorem bitvec_InstCombineShift__724: ∀ (A C2 C1 : BitVec 31), C1 <<< A <<< C2 = C1 <<< C2 <<< A - -:=sorry +:= by alive_auto + try sorry diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 15ec05c71..4cb293013 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -1,7 +1,10 @@ +import Mathlib.Tactic.Ring + macro "alive_auto": tactic => `(tactic| ( - skip; --placeholder, as `simp` will currently timeout sometimes - try simp (config := {decide := false}) + intros + (try simp (config := {decide := false}) [-Std.BitVec.ofNat_eq_ofNat]) + try ring_nf ) ) diff --git a/lake-manifest.json b/lake-manifest.json index 661325826..85785d5e2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,14 +2,6 @@ "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/leanprover-community/mathlib4", - "subDir?": null, - "rev": "9eb5aaff128911772f3564ce032b44a94d5f8ba7", - "opts": {}, - "name": "mathlib", - "inputRev?": "9eb5aaff128911772f3564ce032b44a94d5f8ba7", - "inherited": false}}, - {"git": {"url": "https://github.com/mhuisi/lean4-cli.git", "subDir?": null, "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", @@ -25,10 +17,18 @@ "name": "partax", "inputRev?": "master", "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover-community/mathlib4", + "subDir?": null, + "rev": "3b5350301929a51585dedea497e172a23e4a4485", + "opts": {}, + "name": "mathlib", + "inputRev?": "bitvec-ring", + "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae", + "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227", "opts": {}, "name": "std", "inputRev?": "main", @@ -36,7 +36,7 @@ {"git": {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, - "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", + "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39", "opts": {}, "name": "Qq", "inputRev?": "master", @@ -44,7 +44,7 @@ {"git": {"url": "https://github.com/leanprover-community/aesop", "subDir?": null, - "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a", + "rev": "cb87803274405db79ec578fc07c4730c093efb90", "opts": {}, "name": "aesop", "inputRev?": "master", @@ -52,9 +52,9 @@ {"git": {"url": "https://github.com/leanprover-community/ProofWidgets4", "subDir?": null, - "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037", + "rev": "f1a5c7808b001305ba07d8626f45ee054282f589", "opts": {}, "name": "proofwidgets", - "inputRev?": "v0.0.19", + "inputRev?": "v0.0.21", "inherited": true}}], "name": "SSA"} diff --git a/lakefile.lean b/lakefile.lean index 24263bc58..a851da1b1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -37,7 +37,7 @@ lean_exe mlirnatural { -- NOTE: this must be 'm'mathlib, as indicated from: -- https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "9eb5aaff128911772f3564ce032b44a94d5f8ba7" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "bitvec-ring" require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly" diff --git a/lakefile.olean b/lakefile.olean new file mode 100644 index 0000000000000000000000000000000000000000..d33be72f86dda2f7f37371b7ce0543300848ece2 GIT binary patch literal 111512 zcmbS!2Y3|K_x7g2(gRpxK^GgbfD0l73oJzqMOZ;3h?)%{u#uECBp6V1MZ_qmYXKt` zqM}C8pRpjZuc8?HDwd!EK~N*2Mnw$PZ_eEJ-Q2y|0RL}z9!}<-bKX;KnLGE+%oZ2q z(Av;C_8PBm!5{0W7>P4C!5 zy!KEaZHMzfPDyD_xjNC~YzEGMeY{_NbYs}ICwy0;il2T@zUJ7KyQcak3xe=H;M0%b zPw&(m_SKp}!k4(%o=B5~VI7ku4Of3y|LcAPf%o-~TeI?a4xTSUg2OzMn)$X30#Wd) zfl~*1%M-p8DZ97X=7ryE_&t5l-wS@N?Q#45+8Yd8LUel>Nh)6tTsI+o+mrXaO}-!H z%+tsj$L^YQ{h(>Wm-sr%AJ#!?byfQ)EXXe@$|)@?$tgfdY`&_2yY7g80$+~2;}#Lx zpM3R?qA9$3;536S>^^4e()!~M5HX1_Jz2#?{~ug4yY&5am1mL9e3PGa{axcucWi#1 zeB!em4exc-#FHL)<2mvx4E$rB-W*)@#()XJmw4EINZF1?7UYYFeTbiytbNo0@2?AA zpE~O58y8FA{^UjPXoA-SoYWK*|21#9^3P8z-6?p&_n@3{Z{K{w`BTG5uhSmK8B+Gg z!kkinLH=|RvvKHm5O`DaKCQX(l129TAa<%z&h|C!rDs=p+`&}p*BO31{NpL-jQz3m zal)6l*=B=o zaR*9@i)Usla}pQZMLFyocTRZI!R<$UO*_m#^Sl1H+>QUed(R2v(@(bBp6|A&Jo4q5pw`OGWFi6go%+*$nU!)fHZ+Q+v0J~v(V^8XIcurHSqC;KTW z$0uF~`fCl!u1AbJKHy%p^{GXrw}mdGy^vw=`i|F}Srz$q4f)JFwp{QZje6p>Vi9hXV|e9xeaLrpjLpxvMHM{`zI?!w z!r!m<;1)@B=l&9;hO3h(f+~y!~VYb#Fw(Z@LqTb^;0{=#yjDo8`7SC;y$~7NWARdq#RG# z--ieg4n1BkaND^H?mOkmq1#17_(8+ohh1NF&e(aCmwdKAwy$=N40ZbU9AjS>ML%rn zAL;0O9eVHzRS|l2_d8UJ(&He_dkp^UM9u6gJ+w*1qrApZ1^)hc+JDuMfBx z^Ot9K|NPp&XfI^i+xW+#!%li_mGJk+-arw=Vf&BkO$4|r7y5k@vd2f`b99Z3uZRDT z+>3jEc!oge`s{Bd1&`-H+t>9t`5b@P-v&Io~FOH>Y#4RORi~LM1Ih) z|MWq1@AMn?><;p&Py0Q3uK)4i`CFpb58BVb_&%)urt|We4_HtA1_OV1TGo%RUz*&bOxV~2CuG?B{Pf{JFKIY9dc9)4nXmT;UBAFPq}>bDj~M#Rqn_EB^-b~( zoI9?PMUpV5n?|=S;`d(B2n+a#X z`s|t`$Y*`g|Gv$e0>P)xJDU8Ep`SJ6{SyoFYohm2Y_Igc;lkt2%uh_Vvn=_I82TG8 zIPlR82h0f*pZ>GIp7wce|5KKp8lBH@{AGLS^UvTRoA2Kf&5yfBY<|A@Y+Y(j{k9f; zj5nOmPpeB?bn?n2(fdT&XMbC9_xyEl9zHZWo`ekizh3z4#ri(YSJQv`$M|2maoJan z!LPqbe#Fr4HMQ>N?vut`L_YNy|0`dw{iWfS+zRrUU&jC2)@Q%&I%D}Iv3@f!9^HO#-ie=Gcx5l@2MqmJ+THNPTlXLP5BY4Lw12_274tv*eOUqd zHHQAMHA4@1Z|P8bJhA%YZadMIFljyR(|la-08N8`6`+~8&t?7ic|Q*7!~JC=??Z84 zl?7S_8U}UXKEwlB1KI@Y#=N}>v;owG`Kkvr2pR@;V1DQUtpSaIHi5b^FRB7<0CnLy z9|DbldT@QL0d?WJ;Q{r5R)K~=9T;Cdph3_ur~~7X2egLc6Y|)Eb2s{J0JH|Q2{aY$ z+6x*0tpR1bZNhmf+KCr51j_L6h9J>pvN1ELr<- zAEf%jz@bm9u0P@-UN@4nP)@lO7dHI{6-z(K!FEZ0IpjsgD%+C?VN%NVBZx&)9SI4w znx3^z+@S&IwclL#5k=E1e@%PBb32k9m5^@&r5)$NDlTFO6?-nNT;gEAqMjLty#QnB zk{$~{e`#r8&S@u~JS)G{UpBp8ZgJtsrSoRwm7Of>_5=Is%e1!Lpk`O%ti$=ulP-J_ zkk&eRVuI<9@FY$jpa%qGl8@Iu?syXY`pn95wZBm105`;=a#}vx z`Ccuwu4|ZeWYGq(CwU1O{(SmgZjSKe5Py28KOLmqaXzQCq%5~|bkUsBQF$|S z$_h$RE=2sYbnPPo{C^Tc;jxz-WZ$k@i-=La2wCmO;XG93B^?yy2^lyio|KDUocEFP zzH3BTe!-0M=LPaa5Qm;8Kkyzp@}xf+T?_5zC3svnByA7fl02(}%u#59QwjZA&=LPe zZmPH`f%l8a4TiseZ%(uCeFVcyTy;Tn+))G{B*@!`YQS! z5q_<~KgC;L%(@ePy}^I*hmDu8 zZ3(~G;BUwtHIIE(_%5{jv?Emf|2=i-!|dBqPxO_PvB|io@*RKrJ-YNK`E#S(2YU5)P1VE{eg^E9 zgI}=Rbu90pB`=JFl<`cOH>WhOP^{bjM)O+>oL%iNdVSSXkJ$Hvg2Or`Wg9r#dNjam z?LjFd^}pn&0XPnq%EO*R&zW_oFNxR71UJfg{rY`|=c!%&BQ@|R*$X~n9rnhvVcL+m z1K@MM_4@mL@1v~6kM^q&sHR74P5sqo$uyPCoqD zam(AO^h5Gg2|nA$#WUyJqvwI+7vtCz`KPZDgfzPLSfVX*B=-Ol7xT0EQ#1B8piM{U36WJAopW*_)0`#HN@)oeZ zEuA*=R9qAtCIu&fcItq${>Zb3?YVixd-S8p@T0ox;Lo)08%X|X;NQ65XY z?C&+eD?a?C?csvSTyINmK)Ho&AD+A3%)*}zvB&u{sWlh2kJ94Ffk0l#Nb53GFp?8a z@Wd|b+jXqUQ`!IebRT)lTOWyt#ZS&cIqiP^;;*ZrF8q{o@Y%oDl>HUG=M}yK{7TSc zmwfRW>p}cx&PmySMiduECraWc?bie6&y&{I*RFf(Y4JsHSU04^o0(I9S+*Tdg5x+9 zrwg>~&ih{}{_&+R1V`e{L^m^KbDAq;IOZd za!j`Fii(Dpl+HOjCpV8b9+qDTHNc60etT4>zN;^tmn(P{KiQG4;$C@&hR{q3jFU2ZoZZG zzLF1K`$;*6I=6U6SwWtj4Ljawej9+-+<9W-yP0e4d8Fhc_4wF)?7C*z@sbNU#2&{b zQjSmdeeRf+Yl6s2{y9!~fqUsc-LI-S4qP^}LAq?*lG<8lUqJ-M9S@f=~Z$Oqy~B{j+r1oCmA=RZy0lXr9Bs zyVE~*=$x!09}tPX;S_64L~t6R?>tfEFcnTU&%qN*OQ;T zs{Uuul|%gI_1M{0#l2_2s@{|pzfFA66TchbM>_PVlZkVY;~{?gv~uyA`!Ccp{pNG3 zf zWoYFR7x$B>r^jX2Uy{NVeYuaWg#KR>*VxZisPe=F6GzI$zjDY|gVIh|^Fw6i5PS7n zxh31?byTj$XO-v0EbUr(jE*m9Co8}2`K|reKYVw=xq@%;lQU5s_2ahZ*)1);wcmkw z$@fDZ`U%wMIQq#MpNzX};MR2FR~z^%-#TfL@Z^wst^=RzHJ8kF_T_qw@VOqrd}ZI0 z`xku?ek1gqZWZ4HmCv8bYpL+lQC@@V(U_8Zck`NS;j}qU+v_g_qJBo_>we%hRoBn^ zW>)vLh$A_Ka{Bg|YfxBet2k@G=eo+vzh#$FR{Wq(q>SO*aib@WH=d)GcF_bpu_5iy z)nCPbcK>fy=yoHJbA$i&tG9j4ekA$H1V0n}Ax8~Z#<`jJ#knLY=dQf3nPTk&P09<{ zCM~>Zo+^NsQ@Qo4;PkYeB4F{8Yf;YFM_&5+qx4to(Kk}c^`($SCH`jMNU${i=(GT!?dy0y`%f$KP zb^E;Tri0(^!FT$zgNuG9%6VPgy`-vNyz8nTat#x*L-DSw72r>v^!*I|y4r~Ns=?2h z@JcD$k{v(FdH?av?Dt;c{fCV6=J+GA%Q#wre%}av)`@eV$^-Ky^3q;hD3@~?*Z7@mW>VzkU)LSa}LD1s&`({$s%D45e<&gdvhTQo1XT*&ERVa^u z&fIw2q3nMa#@^}yqqFT#G#=+5)c?GdPdksk#lFa3M$tIX-`!QV&zPGJq{?I9C*_nbAW{{{c+W6u)=hhqvU`5n^xla*B$J<`ou~MHj~{CEfo_;NJaU(jDC%JU_bb%dwG^V`+ANVW0qp z1*aVPm7rhu$X<1m^QKcp#NsE14Zpvue(n*d3qK_t{07k5kG(Bse(V^c;^urJP&M@L z{p>gP9t-@4_8SlIp6E9vr`q$|O5saCWwYJ^0y{7frAY~S>&G8^mHpeeAatIE`)3no6o-*%h?)|~s%--N9 zdr(e$cWfGazpbqFQ+(iad`nw+!Yh=O`U!&1ez)M`QZL5^8BdtEnP>FB#^F-PqE`jI zFzDgmb-OAFd<(zL_^j*BAcYc}r)J=cdS&9%$=gn~=c9YWnUg<1+Qsxdc}`b(I%(Ch zHGf|H`Zr?B;wSr2ZeiNTKUuFuuR9V?1^CR5s}WzvIRb{{VyVkd0aIeg_(N&Q^mtuos(AY!ah2nO4l@og?eO}0%{>nt%h)ZtxAr(hFyzqfRKQNr#TWfC zcVUms!WSIg&yaHbxAx1ob&8bzF*{mI%8m;-9?<1CKCnKa<6~ah@uQsYcMr;}{NL8kYih`^0H4o` zjlBMufycf5-e}>AA8e1LY?rgFeK=lwB!AVwsRMoN^8X&6GW7U9#Nl<4G&;YV(dw}& zyFQwLlR8Z0>C4qahn8Pjb|UepPs({|_MAXouJ)dz2l_tHoe{@@hm8tP5FBa86)3l2 zwU7I{Tz5166n;uI_#E&4YW!$?f=fvVzYcu1^Ivl|)h2>3<0$>=H(}4I4o{0-BlMge z6<^>}_t+%xEnnKqyUgF+3P${kjw>GEyji;Ru8g~`wXc6-pZCIld|Y^dBhX@>>uwd$ z+rDeozy$F3WxszM`(fZr9CY)4RfC_uLPR7#Tqk3GzDXSO3&#QBJBO?IdH;HoJ7JAJ zzOvnsvi(UOIDyvlkO{n(dzRe1g&b&=FFK zVxQM>FZ3Qh`1VT@HNGF^%>TMYe;kwq{=Vv&6D{4pYT&({Kjn!>-aX@P@kDSKGpSW( zAH|?TB(F`-mvhN$+DP>8P(IV)(DRxO{*EnGD>UrA_76_TbiaMT`M$^b-mJSno(lVp z1LY6v$XT&vh@(dRt>?8GdN)6q_EMt852KuUefNdk&nJN|^>vtna*P-mzTDB!g3IT- z9HUg+SI&QXPXhR&cL?;By*&ACN2EnB4e}YFbKY3;zeMPXzh0E{`JVqRJ@U{bjUND? z@iZLw@cYRcKLkFZL=^2fgE0ZTP2KRck%Jp;v|TO6VP&`tZusP;0#!%ztRl1-%IL&YZdJ%$1H7&E znlb)UuO9a^HPGv^<-kq{dRpuG4ZRwiH`3m@8wVWZZmk!Qq4q;S=5$wPjh`zc(U&41702U zd7W^KR{j%1s9Z17v~pSZtWH*P)T3V_FLq77l#AUg;BXy1s;}XTtQ_|BUn>{8d=D$C zcTkJJ*0_`G>k#W#m(qqi6`I2#;}X|9nt(g@m7Ajb?c%qIFS_D)1oEk4V)5NLrwyUv zccxY@e)GMtcz#=DZSEgU95KF_i&>Wc349K?8u*K^e(l4YlUENFyMn{iVa-!IG(+y-o1Xhw$EioTbG(v2{j(FFW4&0m+w7MU z0;T!IMGDFCx8?p1IN3X%dMWAaX@84^#N$UfpL4qN>CGSNepGNI&{Fo5c4noFfV+*>$XuJjnVyKK1i7t zYgs-|vy;HQG{DZXlB2edU3ZJ!N2Pw8UKKa%XYJ;vPSEsI(!r-618(2kPxpiQAZ1=A z6_=Id!V}9*^f?MY@KQeR@W9BY>W&s$;ztPO#D03&Khbf@Dr<8+%6gBI?g~x+IcD;d|z^AQSz_!N%$Gyb3NwTf`vO1T?#?? zS>SU#J8jJcHAyY}WL|&xT>3-V%WU5SLG&x3&*#z)+tVr9za#G5$c+#Fj7{?tG} z0y_J%1IJz7?hN~ud~g0_`{&IPTXINT&CpMqq~c$F#0N*5;cT|eTKq&0%D+5L>AZhz zLi)RZtl1%FZbwo(ANZ_Cjw?;0Ka1`|DNWm6N-gRs2)*wXX6nytM&~7LH&0LN9^E*! z{7H!z_Oh=1?oTUT`w)H;_{8_`x%MK~x#WfGQKan8@;(+bEP3HP%zeJf%jDE6w=DZ6 z)1J;){NyZ@)Al*-b1&25EC-+YsGZyILCWsUk4a_IOZhgb_(7do;2lwrH1_$Kv(6V= z!f!x1=S5d#EPH=l-UhpySmSb3|Jm+OUMLMr4w*N&CabuJFXa-K1LYZ@1D0j16P_Fv zKgEmk8sz!mlG)SPw=AqS`)$kUrTnJd5b&3rXe756(m)`$7eU!K}!DqWF zT{mXD-mbWAL(2AbSy_JW?2(1+y0%HFH|~E|0QambyB>enlZBtq-&&N@hc^d@>@f}e z6hHX&pbx*a+<$Y((A zoQ0$P9HWHqM>*|%FnVE{{(J%RLCSttkn5E%CfcSXFO0Vuc#{VYo3i+VBW(eTpBzCs z<tSq< zL+-5~?C_}!iJp`5d+5EobkDW~jbDLsu9vN@>H9{a#;*pS`CC|C_i7UOa(}?}mP*9s zg?t_8w0>D5J9r&2hv;#=h5eOzX@uVCo9>(1(G#O)ug`Jaqz3bda*W%qsVZ+Xum5OG zCwFT-uA78056gsp7WBGynBAeXtF@kckixCT{Iv@DA?W2r&OEOR>Vew&eG~hw3;K1? z8~E@Go4Qf~RK`E^{zX`F-&BtK1;>TTAGWg$oa<2bJXkBYWZQi1)~i0l+~#w)A>ec! z(EHNlo40NhJ65|&4jX<4U60@cT6Mv%&C(DI@I$%1toJ}1uF5nX|h{#ygRbjS^= z`g$~DlzQMkGw&a^x*uOfzeV2D@GUH`&0=j-R=$&dev2Q`_E!zOL!Wwe{m_Swv#)(p4-u3zkH4mUFo1FH z)lTuO(G%j>Nxek*{lIezZ+O0Ao&ET**vUXSWBhW`>NT_@`D%h6S&(~m_{&F9c5i-o zC%1ff-olAq?<#?F@Ll)aRP(?O(f$@jIp<@iZu|BS-H&qc8$jp0ea&d*UHs(zwIf@_ zdGnPEHt6#N-uIH3iesU0Ysk8fv zBlGCLTu(V31q%lp>(qiZ`D>Q{DMAu&0OgGLk5Afj z8(;V-Y2b%I9Usj)KRGDcwth+t%AFpCf9ZEQ+fsry+t!bO&w0dvJI>nBPUAO$&;7h_ zFM9vc_8LDmN8xh+G4$HAqn#Sx4LX?z4{Sg+J|hz4Qn4r>ZaKb_^;B@rTz3QtscwA9>xy`g{{T zQhK^yj_E2NlRuj<=1RxnW|0uTGEh#x#(aF>6-ryxQv>|Tg52V-rrgvis3gQMwkuMj zeOV8I<l{8fAai%U8=?pfY1InfAE|myMr(D zRqpR{p6kOn6@uPcf49rx?YDA&m+O-um-4>`dVAhE>GGaFMRu({StY*zW^s4{Qq{BJ}x{tEW9M*J$#5arXP7A?*l#W=HREq zwrHErajN&4^;J<77w7Mlz`Od1tN;G{wfPr|AL3^n%4wrp`USTLPY#Qp(g?oyL>1?+ zUBCK+vcfM1-|1KUQ;rI6(dS9&DCc|HOO~$d-!czMa+vQ|WkO!;TXx!fU*YVW!u*1H z6Us_O5QpVYbR4Sy&T)rLI%(`7N7=)m;PHAv%In)q8!vly-n{I*%d(?Og*LL_)&j2{ z^vl4e%g4-bw?_mlesXHQil6IXt7m=lFx(P;iW_|P-{0qZp0fP058->Mk9 zj{)#m58teOzo;dT)^{$zXPy^4xPHCWd+bBv=5>jb*M)rR%YSArC0@3h2yp+oX6*Lo z9;!S^03}|>rLpn$%D;dqwc~Yx&v+l4-eI^NuZQ}Gcg3oryY+Z|;4|LUcg?(7k2eTD zFGFciFZ_<^~kujIBkFMK|0R4^2x8^d@qF`X5a^}vQGhm9e*@G zVfeA+#j;NqcIZ(iLXscXY?U9zyz#2re<6U>cNO$Jko&CS;t?qj5Pl8v?gM{(-GaB< zfiL5Z*>8j;>lS{r&mi=wK!tCOkBPO~xybXoyYy3k9!18}x?~lH=v(7f2WNpgUw2%` z8Yz=Q{N?i@Y2atC+_qM$&t&eO($0o6t~p0(D}68Y_*}&7$#>18tVP@0Unt6-c@X_*;wfO9uSBLAMt`c^&Al#|?4n{yL3)zB@u^-J$C{3RNEHZ`z~P({z8+ zAxzo_=W)K@TIes!pOcRdxaJn*_v4{5_PlS1vP-=t#sR$@+YWN4xT&G2 z=y85SJs0$ zbuMx|#BQ2aE_V4{Z|doGt#+8q-w`4|_3UqB#tF9ba^Nn#WV`;|)ns>%Sig21|I=^u zN7{KM^lCwezMfsE_4|~1l(U`Q{YuYk_x3yy+f6g{<_~#s46j49EBQ3z7M|oY3wmjn z#ro~VIWdGvKK)v`cO08V%^84}B)9qSid$_1X z%Aq69xGk?r4-*|e=UBr}j5hF~v}^JON9=llW5(;# z@I_V*v0JW{OT3=F*cEyHPN3*ZJFJKPuw_}rQYME!E;NFF-_*BGV|`n>X!Cn1)ALK` z=H>Qn`S`PiCw5(PTk>PKf1E!)ecTA!DC}}x<^%uVso%7xUGa-7|7AYW4E^T5%SP?be4-rk z?#ora`uvsGcYo#+4(R!zH@=5+OT77n**+w4X?L}#=PKwkr}a2j8B+gCeKu+3((ZzL zX?N1kOg`+9XQ$MKT>vk)(a(jH}sQjaz zZddYE(=(Po?a(fxi6{Bu`=rgl{d3;9yNMz4)NWrh_7K^`m%un{S zequxPGoYUZTGMw{UflWD848E*)s#d2lfJ8ejywM{;ud?-?(3OP=rfiG&P9%g)MKMo zF8So|$WYJBCx54p{2kS|#Jw(NUZLW7Z*|dg`gPI77hlBhbjbTbiC=+p`YcrZuF}fI zZ~pEL^$fqG^Fn_2D|FP0etjJF4^aMcoX!1USSOC7Qjh$u827_Aje6?Lgn;r&_?|13 zKKB_HTzumDi5lMrKHmqdzw)d1lQe!1eBO_C9Jh5tvc|6hpZk4{f86kXipCFv&wbDn zGW@CSf-U|vfX{Y(XK|Mu?KQq*0ovbjik@@cpLaUJm+J`k2bfpBSLK4<$#<{0xdZ%B zR@M7^+#jGG=N}&EJ#zf3hj;W*Ls7BE=aHz#_xH-7x8ay!!A{=RdfZo_o(pl;KyS*Q zo2Pd6wASOk0`>U)vPSy({o7l*xLfO)_uUTIb6utKI5JW_v8$`Ko_mnu(;oLRvY>ZX z-^B-ZOKq)Z-goo9Aq2g~>gP5YYWDrF**^qX`dtJ1Q62Qze;ijU|8x(e-=%5g((js# zai}t_MbE-&^LY;IeenSq0Jr*2bibk;_}^vB8hc}(274iFUpPbJ;Dmv5$?xTKoVX>Ct6Kjtl+A-e%OhA=Z4SK z9C^cnnEjqi=y9EV-jkoKuDHY)Jxds0jHNhlQ%)a8_O{yM8 z9q^u@_}S&vPHexl=A6(9FeRy{X;+=?3q+Yhx^ z&jGi0fzNv7_xaCz;_GrNj+n!;my&vn!ec%Ec*nhq5->2ybHyfJ0Qh4QdjG>ZA*keu zc_HQAf;EnuVm}OS2}_*xB@Dbz?zyEl)Bjv_zl?J!QqE0UzP1yK<6NZTxO>wU|7l&` zyH9+w>?FHUPJ09U^g4w83g3Ua(qlgI_uxsylKh3h=X|8&DG%L{ z=u!xl++Op+4?F4khyd^BqF&o7W@l{`qTyyHf|;9bHfRQE4gM z29z`3t}V}9Ml7-GSR8A2%B{aHXFIgy+T3>^J%d(kJ5m2U!29j{75`qpyegl5`ccky z@%}K4&ibfaew$<;>6=vhWgUuMT+k752Dr<5amn%2x->px{Kso27U8V)zOz|iuML!FCw&TvbCv9%0 z@yo&IIMI9e8IQKt_?6&uUOd?Q;hRpc!k2t-JRsG_g?RIVdf>g#KJC^AH}!j5ki<`Z ze}~^~S@hA=2GPT3iKuWVm-;$3IbZ&WxBtm=B}@~t^P(N5I~s+{p$zN_H~-uFvB_S`Z4n8cF}bO z@iPoP=6im>p||ioCgC@L&vEGbA)jQV*jcdGjUC5|A?vu})*qW3Zp(A)5Iue$$hB0( z*=yFb+Y`XI)_omE+ma5)#VL(HI9x4y8IaEcy<$ho@>&(Q_<-I1)}_5|+Ec5BaeRH+let%F`8Xz4QpUQN+(9XF}?xPGwv zsJGs1r}16jbN$0})C(`Q*Z3ar`8;F6jVJDOYJ4B~9LI0&P}$T$;|IZK{k>Z^by`R8 zWj&w@^_K?fKpa)j+vrYe?u7g!1@`+%&1m=3%VIl#-oVZor*uwL^``52p~v=CgY#zS zjX&YM)Gk*2>xcN+h;fJW3@7y5H>>;}_xJ1_U7K_*wNB!LUMBA2s&MXy-oa}xIkj6u zYrSTS>$H~!y(;J}`sB$zsgc%tHPEBI3fQfOo} z1wAmXQ(N-lF#L4UKJ?x{!ux#BDrzVydKH+rRfE>z`W=K`x4Tc6a6qWFo(J;$?hw~i zYoT}Hjh+V%47S#5#ypvN{9aKL^j5u-J?@}DYrRI?Z+M|!1DYOEdAX@+Cj{SRpY!8daq{v_s=1o)_P&AA5gCW=Mm@~+G*Phhq_zq zl|#;auGo32itplg(sB-SwbpY(kL@!Z?aTwcYtDc6-@{W|>osEi#tC_@kCj93&@#uy zUUBrQpjUzGRwHN)^wMhXsf|7e53_P#VXk8dOV-D-fY%6p_ITHADsJ6#Ss%;L%4L0w zzrRjBuJ?(ajLTKo3MUd3dJ}#*_`GhscvHEP`-8%-H1LlacUeciXKV43D-vS;+x$tfJ-20kYN1~b z`scP@-*?dLH={h9qj0)ReB$_y8b9q0RnGS}Zhh?5yE|$84Dk6LMemEJF6ylDv%u$j z4Uzjte9QM!?fAh@ouTXuA9s08S53bXeCE&F@zq>Ujz0eby>a*blgVd_S?|(c%yun2=`ZDIPif0y>&1(6VhEM~;@8Thzf^UK z)ie4_va3rhzt7=AUm~XDBl`Rga66ou8~u*C_-*2guJ~OI`9@IoH|KI?k2Zvg-!83O z{BGEb-(uI~3y#?J0f)~e&~8w}7g;&PZlzW(c3qug^I_)8lNifidcZq>DKs_y@cDyg z;5OWJ@HqM){maocR{xvO%I9PB?^OH@&^ddSzod^pStw`weJ3xe7w?1i*8a+gd)$d* zIUdojc#_Y0#8C--#uC9fF@#D!8?|!DXJ{|^6uTy0aKvtUrOE^ED`__qE`EEA{;0Pf2LkfCcfy3-UZmAi-c?7lNjyI5xfcE_E z<16DnXJq70Fr{7`&~x6S{9(O#a8BDorCzeMa;X=eftz)%!V!7NJJ+lDJkenT0@1t+ zpWjX6bN@?^xjiXfz3}@Se4d=&=eX>{dE+G=1+K1FO|@*fo*YsyoQHVtQ*n1HnK*^@B7U3rq9=a4 zAs+yx-yxif91rokS}Pa7!+ZBTr4sWq?ys&Hm9aJv^)G%qS1NzGPB!qC^?z~yRru-P z^L}A&+2yY!Yxdc2SK zKySkA(MKGR8lz^9Bj$YxpK~dP-jXx>Cm$HAW6#6=XHtPC8 z=v9F(+4a{pjwga2MmgKf*Bfi@-rGEz?;|xp@7Sdsu8TL%HscnbB%dDWIUbCSI|JwR zU8v;KtCdSWJx07{J{vm3;y&H&y<%cYyu5Fz0j~Si%iq@X>Fyb;fAUR>Ptx@x&}#x6 z*QsMaJ)fzols@yh_2*Yl-djG|kKEAvXY4^Q#LK4{xA-La48adC^chP9&gr{Q$!C>T zF8K`ZC7*J=G5LZcb{l}h@BPrO;~^El$ng-nXxrm70CsuNtk~?yttWnclv{uEXHdZWC}g&!yeehvVlXT`RZSwSlYK zm3;7bTRAT{V&^kGXv5+shm8B0Mc41JpE(i#M85*|szHxh`a<+MR*B1F*k@dR$k&0= zW+To;j)y(|J<<}d#8qS9nsITTtQPZ&Hzy9MqYd%f2RyceFTTyaR_|{?@VQR+^m^Yq zeVwujd_G70=y^wd$^IpIb9Gey(&p@*&P>K5_QTL`0NwS-uYYOll*#_2SpBRIR#fWx zj%vksftKCkn#DbF!S|p%1M7)1>N~7x4*)xU@OfP>PfCcs&mjJX4F8Y#eb{2%eh~Uq zpl=`g`RooY_{l+MtpEL9E9ADg-EP9rYXF_HA>+1=(3f^&)~~SaaUS_{JQ|Dd!Z{#p zBJCzaE0=atof4~O-rw-|n7RJ7XT`3V=LPwmZY6M+UAL^i-fnpR!}n|4nRi5=dz8Fa z&Q|bLYSzJ(% zmmB>+xaCju`H(E&?fmGhk3Q)&=?zKX-th9|*Inb_RRE_NH0jielxf@V`B3nrUDczU z&l_Dla{X}O$sze^2A|)H>^P$&`o5(2bC?p1{(jD(IG5**j2QJ#u;E&J%QAnP6cY5P|RKKC2{eDs8~C@cP_fnN){U~}@8LDN3Q zPcPOpIDUM2SLI21JFfyB`H2muKd#3aHuzh9SRZ|FSMtLz~PZ+<} zopH$(%#-k42EXIR!xwUVlf0SnN!*gRAnbae&pi2XE^<61Z{=FKF)BhkwZ!tb8U{ zb%>4YuGF>bXixGTfV~iC|Ab@uFfQTOpq$ss18curptXl&m(ku{4V3oQ@gvZ00zGwH zd5$*jC5L*%`nPH3Axm}r)F&0+4SHr?!+Uyr@}ivW^}S!l_SD)_vcrgf+NVG8@i!~K zR{YQpfo=?bdj#8?9Y4x>J-y-mH*Vy*oz%NoKjOR8yBG0BpwBvK!Z~9UD(%r(6I<^! zd$0H8hIX-ed;a^oPavlF&2=F^aIZO_JdO1#ew+BBD}HA}z5u>yDt0rpahy-b&Q?&EWI7r;9FZcW9EvPkUPV z%jcd3ywz`8vc}HSO%xu;}zI?KOTS_-yBQ zjYukTf-mbU{CzY&-^AylYN1z9|JLChLXMb2^!WQ|)Z=qe_0T)=tB)pi492M0>oScV z)ZYn;^0}zgXVm#iTSmUpDbQNa4?V8$^0}x?=w0>fPr03at@ZdlJ3g;caj~)!gx;{K zQJ;13w$|f&XPh_GqMmD^_u%xS*K^&C+L9N(cSb+?9#|9f{(AYB%euL#p{VHby)*Oq znDl3rzaKt4YGbOawI0{wXs;4}`k*)bu8NV|ucx-yr96!Ww6JK=2?@GwmgVOJ2%|F@^zf+%6eoC2r{WtvL zbG*VAy8(kwJuh(hJ*$9*YuQPx(9Xq9je%q4ry@Bve`oYQ zh_MR48RZ;bo}LkkxqnJqtMo&-Zr*up&hwmSNSvmBVpsB83)~Fo(`FXVMUIE$H=vbE z+)YMYZQVC=Uo5opmf^G^aq+$}0^IVg@BGPjA^e&`-xsbfo05<@A-e-hx&KN~r@>Y#< zIk)q+m-b@YHTa?@b{m1i`)Jy6KCkj1ay-PYODh+J|^$;pT6;zfvgW1 zmpBe`pOW9H;67z)#kM~Gmwn1A`1fD^i+}CcJ|*t&>Y=xE*N7+gXP+_%`P3Iw{MTNc zIxgNmrI{berR3cQ{Y>aHe?gox=Rzg#m0G#v-D~9C93LXxW9!9p?}z^oQ`$Ml&t~A} z4*#*3^&;)X#1~!hyB_jsFUI0$;G8yuir-$XT>K90!|#yc_eIT1h7(io-!;H}Cwzgc65&Qt7gjqMY?_jdQG4e2l#@F+wT7_DSfX0pBowyeSbsRtGPeL{S-I!9^5$X zc#apeEBQ3z7M|oY1V6mcXDk&sCx%eTXO&hi`OHX&jaUDD2P>YA-a{3i&zb(ZE_gd_ zNWA=A1INosuBlzO=sU8)=X0tq@V{Do*`xY+=|Oqg5la7tkNtOZeNps%;Flk%__uxZ z>n(hDP4|!c%I$}*x>xrv2>mM1gYF(NxigX?_+gYg`zZXa%_rU3rG+1j-;=HQ*`43& z#rhHb2IxCpQT>$b9x=;k!_t3H-={&L4B_NcbM`vwA80H`Z>AK7Jy6ANVyc#XsQW z=WpyD$3N~%cYOWzIWh4=zY28OfXBb#bD0)?G(PTIFI#ZZQe8g`y#~<0DPKOsd7iEx z-PgY7@-4c)<5lIi3)KI^WgQNP<3IPk1Mhp*>G~e%`9R0d(fLB^wWJ@jt~8R(jz{9 zpY@;r$CS7E!mspev;T>z^y>!nQxEjnXM8wkj3O`nx*X+lF8w-Uj+197KNUYQIn@{^ z#~=Oh2f~v>;%!sq<0Y5S5?eg0;~CwY*(1%T&%M`5!b(O30N>J}SbzTRWc7-~RfM#B;&i%JRZ<(Ur<%-sU zrd6u*5NPII>O2gZu|l0UfmYn3&RzE@S`X@eK%ED%?;gQEcqaCL8$h$LKkCLlm>=`R z0M@muv0m)K{ZR(i-I_rCPboVUxUcl!zNi|s3iJK?S|#UwUeUT2;2-7%5sV|%=#M_M zv&z`^)8_XivI}wwv$1Yr^{<5LM1|k@hN4G37Ha(Johgq<+mm)UK>n}}(q_olVLy-a zD}IlR`;V^n3NN*jq5+IwoX>Hemh02}J}T#_e9k$5`5T{Kj{w)zP2uwUjBempp}Yp? zHP8=sRq|YK=RPaPO*ig`Qr}c^e4iwQa^7D@QWf6;Jidnzfm{R1xsM!zycgp$*M%G4 zC)dA&$dj*w!sl~DKFBqooX-V>vCk`YW7Sie-$5_3J_T<7Zr7Z%%1cGqI;7tDdzJO; zmAyAF@m)Efsrh5!OTF`*TvA@wn1AMh{xQGI8|$6zi~h2Hn0M9_+XLGd^T+%$Kdd*l z3)Vl|9rIm}eSEgdXuWq)@v_~qURlqq57rm=0ofkeo><>*wj0z3+dcaS@9)ieji5cS z-LigNtZ%k2^f$Jf5Ze*k59HWC*dGIE|5BgU_1)ooOU0cIih6GI_f)J8z?NED)_F5p znoUf*Nqt-4_3ZaR@2+Ppdmnhag_?)h_dwnUDl*b;Id>-ITsx;AKS!EuUeTPG-_>Tj z4FTuB@#XUm_`B$D!4o^-Htg^ogp|)r2`d;J0bbCUk<&cY6Ig5wPA;Ic2eF0o>1T1fPd)Cj)q+)@61othi;a z$Vk2Oo{g0EfcZrQ`9*odttjRY&i306oC?sF4?nMR#fG=-%aZubamK=q9#YP6z%1u@ zrk7iP@8-Omv>x`FK%MWY{D=|3uSK~_E4OgkY}dI3Idk^buKmENZ2aztV?KK=L_3uz zH`^QQos{>IC3!Q-a`UI>7g!%}j?HFlJBR>x$rpXfMjfGs1BuJ|zKYX~i} z6UfWWx4P|oyY`}$VErNOf%WGBZrW*$v)8U%WIx*~_R3Li#>a7il;cA@Yr35p;EhWD zpYxS>oa30shBoXFmy~M;V#n-Cx}CHSRG#MbTU+AJ9i2xz@$Ty+PPRKg^e7)XN#W@2 zQRLaKD-C%k=J%#N+k2fMAMg1T8z1wyWr9??2`ed*9w;@f4t;#g0^Ws{hfcWsrTTA0LhMwu zVTb*kl>IQjFi?;2MJ{Tj!lBG=94Eojt}+S_yvi!9hze-CAcL4#&p;!v zlC6~(bxy!w$M2LW}K97h8*J*G?7mmtKwpLTU6wwoq0DXdE%qI9p}|%Ip@=Q zx!7$q?6wym>oDz0ndF;%$h5l7Gyl!-&!|U79m<`b#MUF{L$K4ytMR3N$Y&li!1oz) z^pA2iuop1o%=)f`T%{pr)^`wcVNFi*$omxLm-ZVW$9zhBB5(eF5cwt*d8u#Dr}68X z_bapu`F6ao*2~3ivsd9TF6OH(yS1>Z*H^syXrzByUPO-g%tsaE9G|t+f4u%z0l9QT zj(!s_06DKFCvo!rjqy{y9CD0T@+IR&Wxp1G>~TaJf5bo2ZUi_DhF#t#n|7Px*p=~+ z_w$rz{qcTWFSmSd)!*nB`x*NmaXhD~xXM3|jgS3Pj^X2_XwIWJQ2>i$c-(e)wieqYK1zBc5suBYQjdk&x4QvagQ^(9?S%BynX<7P~c zUmj_r+?N|)p1%{T+qK&P_L-QMBc)=kgXbKtrA)3voR9FF_Zd9rJd5YNzvnsk%6QJb zE1q*NisyW8U(PL`cC$W7+3(n|c>M}~q4E#{Wk2P470PQs!=Mq+2GAx@>XV8;R=qjA z;5)ul_M}|$6#Y?Wb>693<7YV9rI62jo9&zDwfoRxJux5DtJCzPKhhrMLgatd;Q7lW7VV0}`~#e5oaYzLHcLaxS;WBZ|8(?;cgy&=bTN4a{) zIX3C>COg<(DHn!Zx*%AX% zO@@H%NKB>qtFt z_cgB!L#|2lSMbcZIIm3G(h|SK#r0?U$+$d_)8i8PaE8)nd0Q0mIx2xfeCC1ca@a*w5I{8z2`n z(V;nw%YPs5$j$NINvgg|_Sk+px#= zL^H0+IQAqi{!VUNcADC-!~Hqaj$^yZgC3XI;qT40WhV=IX8yRZXxj0&VJB^*vfq}S za2s~GUuxQkv|*?2;Jw>P|0aHWFz@Tx9x@=W=gs=N)ws;|&GAR#ly=iJP}vIshw*cq zpq*Oqxn4#&;!=*|L`1`re#8B3Gf&NN{1?BtZ%cXl>+Y%i)yv~uNBrL+&)WUC$eD3@ zAs3{)WhmZtg!7DQP0k(`0c#4mHbfPVQQ zXZmIKOXBc%xLMDn)F%~rD?Ud(@bz`sczJg=s`&QRp2EO$L7sk@?SS!RLQeN9p8e=L zt+xIUuim*%QDxZY^A>D}v|ks;zSMha_ty0;<>50_d0YA7^*7^tC0DJjE64NK1vxJ$ z^JUIoh+7UhJzwG%pZ8#Vf)meP1p4Oq%l$R#Ge3=O*fYm#+B5rwXNSte{`QM3$Vc;F z^gsF)gq)s-cmAUjfK7FI63seY3tQ z+wiNQYpgu|;`qS0nxJpC5AJuG_MAK8=fNAN|HNyLKIohFxPNQfD{sRdpNpbA<1^c1 z1p52C-q{Fw=AF-7(GK&L`eXb&@OO{)b-ngOe_!K8Gw1)1r(foHMZc=s@QcrFF%IU- zY!8l~R9vmb^B%G7iT2VUZ}tmwf2A#Z0qC3UfzO}OU)rmPV^8Lx4F@Uz+OpHoh8=TV zm3Erq*pdFu=jP~_*pqUze@eNPlh*f{LzJJq-!$(tYx^sH`OkVht@lNFe`&6-nfIgB zzzN6Twch9Pf!}Dzu|Kh$aQ>Lur2E%;eIye&8Je6u?`fkQ`5>paBdJ%{fW6zPg`U}d z%z9$I*2S@7`*n!2L;GBh<2mDJz4G}DQr74GQo*s>jl=bevg-wva#`o)x?Ed+&>!=D zntF`461X)QzO2`>UOCTb1mA2=l#AkF-7odm`1NA?m7&Q=p3VIc;`$)Rd?P>Y8oDVv zdVh;|U8#k>Ic}Nzs!!`HpALEAu|3dFuA6!_IcXQ> ze1-Dmkkj)g{+rKhMBB?T%HMshM>PW1>_2Sp^qb?IQ#cO{N;H7JF5*MH6W}X?B z7jkA?=6W6DGI3aL&QDlw?$b)S_~S6fIqrAR55_I>Ry%djUpcpAcJul|%JmA4d%T{t zwV#%;TjkN*KNEZz51rs=f=apc7w)ggxr~q8_c8tFz6|3CYdBJG)MH%L;71I(R{KS$ zFXtbz?SS@)R}VS2A!qurfKtV%}*9FRjVYk|lXwYRE+lIo2oTIPYvW z9_kUl z++o~biM-gYK3T~VpLTgp|3zN<2lGSv|Jy$VPx?c~9%bJTD&^82*ni|)`h(dH>7Uu| zA{vhL2UD*W{02kL#9{kQ`&0QReh41(L+S#K$B;AIFWb4_kTct_6L=v*&TPL;Xcx7H z9P5StvHdm}a%TJG{Mh+dY`m<0;<5d@H92WV=KV3{vmnR%k~~WNHlMq9J2lWV=ON}k zAnkitO91{F{0r;1j6rfAyd zie}a;>e{GiXtSdJEsEA)eXAM!(T&)r^c{3N!=jY7tNm)`x09(|%UC6sAosbt9-3<53Va4gE6+nuc~A1Z@J%LOq5-(;Sy9{TCNinO~%Rto+W@ z%B^~C^F4yR@<4Hk@#cg6UV=MO;pgZ5^!d>v?wKzAR_ypt&i*LnVu$a+k@9*!xoCQ^ z^@ie{vI4%n>u`u2zOPUTyz)=aIdtg9Kb8@X?>mrkUQi}@#tR!Z9&j2#|D84J)+@gb zuM|8xKS?Sc({FzJgOu~A$wei3Il2Cv=>>TsN^**F{dsc)%06`ey}&Jby!MCV&)n8q z1SB84?;s`q%(5c;L&}rN3JY^e^7FLUn(e$)0IwQ!dBw5Wvs3OKD!38{@0U4#O1bz` zJ6P3!Wrm`kt^M)4Gu#s{5WZX=(~?#E)Z_Kn^3^^#FO(Cjtj&FG>WiG^Phtje{h-t* zE~%-<{mW`iPw?VBZ!i8(-=uZWZ!mE9{Cu-f9`F5)c=#dcrKhO8c|aLA->1lmEswsB zP+^qw`8MJK$H9Fk#>H~p_nYN>zFEf+|G9oiO1=H1jEn1-Y3)?pQZD$so{$pP2RY`8 z<)o|^p8sDd^-1X`pSvyB{FMH|`G&K7i~my2=XT6`33XTfh5iFS`n(nWjh5qn)RgCQ zM6Ki#6~1XV0=uR>_h-#=KL28t^LZ7soX>%n#(Lg*Qd<(!ux(R&%94Jak$@MmOIdn%yQnp zvOTcAc>ie1^M0?DJnqj-dEQ5v<09{SOnKg?nB~0B(95O04;F{5gVcfRXBDo4wV)Bu zMqVFL?=Fnj8K7QJKWGrN60`=i4zvNZ88j8+Ksu-gGz&BUS^-)G>PA1x1oeTIgN8s; zJF4*{9n=Gw1sVXY0IdS81&x3Y@9S`8Wotp{xab#_*`F3=26 zFQ^|h2r6|b{ksA4&q}S_s^>O;C!{2AR#`z#$>^f|mYWKhm-2n|U{~eG8B^c-_s`LykmMYb{c_K=UZ`bhjwT8p`EmD%D!ob^CeQwi$_kf z-bfc^>ySA3{Rb~_&bqDFLtUnPz%UieKmQuYt){dp0w55XyiekEu($C}@!jbHbj z2uR+;ZTQLgIVtl}R9uv6eZr)yRPIz_-U?TKGyl!NU3pIBzY{(^r8n)lQ{(4_c_3w6 z=jN5>*uhx;>GkUe&g%m%z3=!lW_>0yk{5n^kd*s2vkHo*=M;>#etpHdxiUWXBDf*o z)qr+8|GehEZ*6~-;7Xnv+why~(WJZ|ol{y;mRnj@qUT8W-_>2^A?d*N-4`q!@eS>G zQNF+J=G>gpT)!w=haN`-aE2{@;fgbxvd0Qv^27UEQqGU8s?PNB zYDD0*D>?kd*DQP~!LIl(znAgz}&5 zu>!ac&%R*u9e<8-i~n}}Z^ItH7ePw9^7}olTachBdu&I|z#aR~i&J+z&}iT0i#>PG z`0bzXt&y_*&d8gYW36SxZ@9{AOuhSo|8Yin)zcqbdxeOI-Rd^%vcHkC-;Epj|4RE3 z_^7Ju{~-a5R&i9&VNnNhiMTLTETM>wA{anqgdjms5|Y3~AsMs4P^k>AK~cwjtW|?n z9YN^0kJZ|^(Qzq`)@rb|js7YS+Cg4Txm^I(w3Q97L~1UVmHdB^$}rjB*e0Yxv00nd4{<<80ret%O_cK#%u zun6)Ngz<+0rk+m7d$`~5Z+^1N)^mhQ^tc9N9HZKO=lCBFm;A@+o@(FLWuM0+A;*h) z{GA0q%9Km{>3>J&xb~4Li?%%=bcvV! z9))io9p3;T;}t@gav3kqXA`y;A3nDAzu%G0c#(eas;{R%dB)Z;)N7w-#UVds>Fp|@ zm-~p5j+~70YkN2|yKkv6}ziAh~tM%miJL$J>nQ_$I$QSnuUA12k zf5$`0V!!(5T!cQ4wqKB9H@}ZTyZr`T?CyqrZs7U5+EoUhX*ct>2X20B{nP6!R%tys zyGb9q@t%gAAH3eVkI8spKNEf_GhQsy4k;^NdhHK(!JZz#k|Fti@_QVNgU6tYpK;Vn z0rGqPR9mU1`j!oBrx_-Ao7k{ECCkUa(Gt`VrZl2~o_*K&eU%vFWraz?Ly>v~< zlSLOg_a;T}pQ+IL%VuksIqdS;QdcfTAJ7hc3Fu!t4%J?l$Fe{$V(Wq^hK<))RS@MLVOsfDENdf?NtT4B7gzVQwE>%FMD6*Im5*7 z_bz#O_2$28J-Km4`n*@(^)ElK#TjFQ<(pP7QP4fp@@Z#03WmPCBP>vd;s_Fl!5oVcFKN-PPKt^F;2|OGvFs(8jF|u zb35CMkn_ocMdXt9%8jS8{dN4lJ@K($JvFO)y>Ll?s{)>Kp6z+{%*ZDrjv~G6LOt%8 z2fgb#Y3{*KKJOfVsppkl%!Aq?$DIFYiL$rXeX0ZewjSo^lcx9&xccMooaLoYeSfUv z0Bt|zw~f?xoxbtiu#%s5IrnSONh_3ZG4G+gO6U=R(ofCtB>gT7db`0V=W)EhMc`K# zU@7<#2EWW>v7y?2+ULJ-V>UAu`!g1u{X*<=?q}$4%%6H7-{Z}V6J@{4{9cXJ<9(NT zO5kE`N0m`e+Kc^(unOaZ_g}HYiSrm;pZP`1kR$qdUuS;7-}mY;_(UJ`RYK-pywCqw zNV}p#^5a`FA{Q4YepWuf-z%#$_#}Szb2YqQ@V?9ZvfZdB{-}S>MacUG?X%Ydoko4J zkMlI|7wq>v2A|kxzhA?7)rWbM_W2LY`ETB5xPNox$C+&t*6q{lK0|tI_wk3%AG_Z{ zV!zVck9wrsm%qt8eZ|EAZ+?5E47&ImMmYw^Jh#i>GwtR)@yB@gopb;CXqDI@bgn~4 zAN|A|f0@zpU%${LUVQFT%A(gdQpY7gi183YS@=x7{7z2vz@huT@Xy%Gq*E{H@sp4L zY<|tde-gUHi+ZFi@#455Oyj=Qm8Vy&JFM~5W6+&`jB*N)zengjsPFdXcZ1e`@a?xR zPugpq*ki_x^okcw_{YF+UwuUAVt?GwEB5n#K}h@K&>J%D<1$b1`)Qmfl7@ZaM-b&U zK>E>T@R{wv?<|#GH|NXrTcJs|AEdjV-~D%&m%ibooyzX*-1i{leQkPULv^hPQJ2z_ z%|k;6>o`93X7NP_ZyfX{=>22BGe7_0na&YTW%ZxvpuVkbV6Qe>CbNK zx%V#TITv-`+sSo^)?c+)k01W-Q{Xi3T%{-PQt}2QA;*h)soNeI!agSL&~s`2d~M%X ze5fBFgq#qdC^XxFPA^&1@Ar|X@41_Fjt9~o+B2}?#tmy7zob90y@g--QE)u;dDLukt2T69?0!=U&!RyRb0&X+LaB?)oswlzc9)jfZ^kGd%8<=aWMTm z7;@GeyLQv>mcMhK6ot*WS->ZoBj8QOi4+R{wtgrzt_z9}t|c;~fRx5ZB~CFh;7qiN@*H&x5;fKK(cHx7mJd-)S-Ly3DAjJ{7w7$Ji0t_YHopm~_|S zxqdEocEFwtAoC=z!DrfexF}ZFIYT#djUDw3Ek~_R^p2)i;$r{m@FMKdbn=?Dtfoke>i#oYDpK9s|AWVn>ep`I^dcQZ)6_ zuD$nq{D_+`E_p`i((cqFWr>^m=Ujy4N9E!n?Q5?;Dh;}{Zwbn!fE-t0gU^iDvCvmO zYv=c7Uwi3arD)nszv@Q}YMS)*rkjN>c2kd(#qMJHLtTVy?>O_o(fNMZd8ON+JM#nV z%>c69{RW@u$5^f2b@B4nWyin1-=C#u`awT^TR(|hKezElp-a2l-@$5w{5T-nJyk%j z)6hy*_f3-)-QIQJT9Iq&rCq;1@qpV7J$Ltz&?SD~;?rbcvS> zWiKGxJ!J5i@fr_(wSV~IPrn;eajg_hyXjZknBA+I-rwy#p)1=8=EoJ)&F2b_TuM&% ze%%B8zrSdKZ|8sCzZdBJy+76d@qT^C&Y@eJ%Id!#(i3QEtR1LB}_-MZ&jlSV21&Lwv6e2S1akCW8%FSQlwR|~SM0_}I)rRU!+ z$ld3L8S|ch_K@F-KxJ=#&(Yd%>iF*J4X0^s4t+oh^~%6k7r*hz+&Z9WK-+0rekJIC zylcZijyWZNfFJe4ppX9j+4rg5;ao!Z9j5EYKrjB+DU}02SN*bxctJ@&WxtZLvbond z?}VH#K>8*8GGA4V%D*4=fKTYsZIWSdqcmMZG=TH9pa;G_z zU)j8v{d(n^HNnBRAMzj3BYrdgqx|xJytymalHxb#;{xb3!xkZ zOaPXQ>D#{(!~k_&ebwfEue>m3iu`T*NB?I}KJ>14K3UfwbZIB*VVQB2viQS3LYSsq zu%kWCp5E*Jgh3a-0w{+7=~u?!6T5l-e4-elu1SH37yt93TOBh@zv%a&=cg7-t-jgG z{>3luFG*deKO&!HnfVOM*?a-~9mai6>eFuFm$+~|6WZq|!DDqhF%J);+y)o}WF8hr zISD9wWE|Mv2}l`qiDxOw<$y7d9yh+9<@$-Te*pPJuIy_EKo1*yf_Fhqn}sh$`?Op5 za`cC!g^yxfrY(FY?uT6#zKZwBu{pcNo*3G}W8pK%r+gMZ2z4b$31D~?+8SMXOEPM#~9t&Rvyn9?;9Qvhj?on#sWqhhJ znZ4w^jqeQ*&vC(ZnjiHmDTj&ZugS2^nC6*E@!{=PxE(Iq@I1w$No}o)D!*odLU-(&xsuS{Eq8^ zh#|+Z)1&Q40aBlN?j-SJcOc|_lJN*w=S1C>p6C#*CjrQO+dUx{53$ESKchY7Ii1AK ze(#&-TE5|09_vL6`QiujIYRDRCG*a!RQvk!^VXyxN9<%?5<@-4H)HTQb{>s(SAmjx zJWt}e740lNK0gjTw@G21?`z*l{9!&v$o!P+Zl1rgo%lUGwqu*6m;3u|xF6BJq`}u$ z9J$`#(fDlWk< zj347_uX8enJZX3C4|89Z>kYR*KOWq_<-REAPxD-}&-f#MV}44z?D;cd>Epg*8}cOP z@o|H%uXu3%5I{c0{c7s9_jkGtc@huqZ*m`!dc7y+;vssue@PEAo5-2>D^c- zWb<e8$3eBY)~K@RE1& zy-?Mcos0d5`K$Y69iKw^tNnWbh4R-RN` zT$!IF3_F~>Z(hC~g`Q7i{u=^+k0D3&+3is%pSI)A`+=EHi(S3u`F(To7JYVJ$vina zImf4B(<@JAUd(fw9}6X}PQ0w=xjGGfVwat#GEXi&C1;oL#S7%AW?m@z?7VnKd1&_j zZ|GBT*v{vw37w5=<~g+6v}T) z4L)fH=BI?ruXz6xeSNiil_5vsX6MDsui6YgwGY>?63>fzv41__Cl|k*I=rS?^hi8- z|0U$}eu1XCC9So36I|q^A-5awxr#d@vu=3kI&E)JKhG2$4-cL@ubUh!e)h>@{h$|> zf&SDPf^oT~_nUd{7ysDHc^~D6?3mc7ezF+vc#0j|hYv&Ey8m13SDm85sWQ=bwy{lB!#<9Vg9d zscxy8?o=}MB%x<@{m4Te3(xPM9JW6p_tMQz42hf!>bs_C|96}4$dz+;9q$|)D|-J@ z;CT+@Yri#nJ|p&0E+Nk9ukatb`n9OqnPq6vn6?z)@%-MSW-@NVfM>sZx-VJ)k&o#ZK=pVz2y;_4j2OUEkSl@lB zj>m>`=WgxKmo{OLJUEjtQ(?9BO+wal?O#c$7 zN4oo(s$r&oX^Y-=9$0qs3U!IeN!1wAStNU>*t9iMIc&Ve}&})CA1NDS1^Q`?oR@$J;JZtX< zw1eJl@!9MDzSi~5{cfa=2iO11yLPlM!*xIHw)bV)PSbLQE_&?sKJ%Wq!6*LncTw4A z?EJ}I$5T$XC5OMGT1bw)&ZnHR89BSf9{%oXAvt_Li|c&KiCA*@JFSJ}*z0!6Nm+9E zyRL=g*z0=AaR+jKsk*)TA)nu8d)oc5(x@-(X|Lz`K4aM66Fts@cuFWC_ieae#C5g3 zKgM-7_nET!AogXr?#@0RIZFG-{Q>SzaNmHC^5|z|L4KayVc75V+rzb7-w_&S&eZ%> zr|04+>vQfih+J8xL_m)le1eZbe$vAGfKOZaF0_A_g>PrSn3=OfIh6*2I#e&ly|I6kxe<$2w2V&Ly<9WLXA_fo>1{j^^}oVO&f z{x8M)H3T~nh8@xm0yszMHt=VMrHx}QC9kudupsfy z&d&80WpDrV)ckqi(pN6)bew@dLGW`O_ry=eUq_uz9soMuD_t}2jN_QsNFG4E$W-+T zuDeoscIDplrLIncF7uOp-VrDLjGTX>k2w?}=V6|&a2^)>qd(UOL92a$MfFSc!WR`}e3sAD{k02nOV0ZF zsfV3$??b{ObWf%Bm+RlP-!6Ri?GMh0fL>Gv`YJ)F%k!80eY5`i&13SnlQ)CT{?6yt z3%yV2elCCf&~K3^{e}BpeE%^F`Efw<+2^{2_N(lDt-klGiuyx=?Te8ffn54!@2^#X9yjz2OeDfScdoXhM7)c5rvt5(nl@r!dgA!*E8=^yt;NpG8%A4m6aUG@P6K~ETbqL1@5 zA?5M>nDaLE@*IqOJ%&7qgS~E~-qQIw`&1l?s`l6AAtG2^`))co_=)$1Gv#lYS2*u* z|L%k4%kH}4y8au5u5=g7FJ#}WsnL0z!jTh&-UMKBmwyd@?#Vrzx2Hr;C-8o}k2dC< zZAXo$z5O2A(E~c?x6Ik^Z1dC&o(p=B=Pd2V0zs(jYj@|SpYJzrq5Lg=l75yT)OE#g zFZ%m}aIy1_wMn0+$*$YBJ+v-!*5*5~%=ec3GVmAI zx4g?fX!4g?{6X?hdTX7%52O6+$M*`mp4In>voE~VGh*&s=W$5MH&Uq2*x2_E?q`J1 z?lJIp0g7!BNA}-gFxG$TC9mD|$IG}coNf1d(6`_6!uZ*zEO?Xk*)JBe{$C$$1B-tA-yaMTv7_fo=!(2g1Jkh44o${xr(3-@Iw> zzS=Ql@w=+DzN4n!?(VA{0~Wsz{9k@`(z$j!sZJ?t@`>5rQOFy< zWx`vlj~%vDs!Mw(fiKkFaqLU^U|$vZI{~$vTzl^ayN-L}<<%8cM_oxe+tX33kmnt6 z`Ii&djrfC2=Su~H({FbkF!Iw`LYMegRsV18<+u1FDEHM~JB;ViVujPMv*RZNd3)Z| z_E!B9T^*XP)tQm%moW= z?w$T^^Qsp~XaBky^fRx&VyBLhYreGU&Hz`)jx$E=eQ3+~jW+!X)c7wSLUk59wC z0QggYT28M2j1+{rW-R>j#7mz$;%@odY~Nc1p{~?U$8Gu7(a%34f1C811);8)Rf{kE zbanB?^0!I9Nf7EvO&$HfMbGZnYks>ylU;YNzc+r$v=(Qt$gJ-q9ExYyUuW*L=IE4T zuJoV8V)P&M1GYoK`#<>8R=v=sz&(AL0%0n~!FQozj20fbS;=b=mU|&tcrK zFADyWdhNf|QFRNhPbSOnv@|-?g!F^l`8Vnx`r*jRm-c^uf03i;{lmc1o+HXP9VIlm z6n#Jpbhhu@^O}Z|SLCyPC*Hr=@Xr}PtKEI0lcp%XUh6;Z3-bKJK7Z@9?CC*S?2+}K zeZG_gz4V-1e3V_;{CJ~ORM+xV$=HfD-(DbpoAeEWP}kS{-W~p8!uaRqZ3ak={ByK398LP2n(W&3=qLaAhJQ{%iqap`u!nIY>}!0O^6r7W*EgJf#MXbG=nPMj z?j#_J=h;u6T=3xFnGse4w*m?Rw;-40%O9>vLRwe9Z3WY&qf; zCmmIMz0PMiE_v?A=Yo0u*z26q@uRpnWZ4--S!|W@YM-wLK<_m8#9w}Ah(4Sb*pPk7 zL;UqNpns#EmK2@xOY(}ptWSTZR~A)HZtTBV>=1u>&mg3~JWq9v((;90`b8D=QAY%2 zp^INUC*^snAM}L5Cwh5rBcwc@3sWDz_d|M*AxHGNkAQtgYRLURZ)47G(Z~9PZO7*5 z;+OqBo1jr&^zeO9`@1`B247!#?0sZgPui$2diWg&elLRG_vtqHq}{o%O@Ck8a`jA?n&^xeE;|!JHL;>ed(yh z$M>fBK05i#?|z6~j3c4_{Kw8k^+;L#rGJFw&H4V>aji7yPCrJu6p(QZ8+>9{Y><{aNffK=5ci~4 z$F4ohnWIg+>DSrc95iv<*ywoS6}w9ed15!)hmiKOom?&Xe%S5gHt6C<2jph}*-n0g z&-CLIF-%=AY}>!AV)*=w{B8O{KL;K^WZ0NZ?~fL`_(45V7C-nNJRzU&;kgFSqqFl1 z#xKABz;iH;&m{U!D$nlT@56T*bZ34*IS$D8e*LYvILbM8n^8~BnX5o=Gx!`l<`?&}oZVti0{Bu3?+4y*;XS}tTKF{P)sTgE1K(!h zs1_RTjP+ z`&(fP--CVWsD&@V{&n2Km*X6x!@{TMX@5E`ydU^(3-1BGB%B|IZk(5TEqojBWfr~) z_<)5^;k-C#;XS}dEPQvRwj*ZYQ@|$-yz{kF^kPwjK#4#N(ar|jn) z`20YZ#mDDuB15&`yr1sq{bbI!_IbAbesbk6a`6c4eQ7EzrNbEA##5{u!TRW*$&(@QFUQ3nBG!9mw@A z<6-9?QA3{eAA4VldOHk0(aUuTA@Bd}56l~w2XTLl>npC$*^g+S{eEuAFZ1JK?_*@& zt2Fo|KOmpTm3b)wdfea>d3a`uY+An+aw?+4yz;rTpo zxrI+*993EPcHqMn-Uoct!t=W?aSPA)YC9}E->dDk@O-bf+rsm`+LBfIaVUX3UJK9n zYRfD<->VH6c$xoq^j>Wc{C(Y@BroRgBb+ZCLtO{G)3trj_S>BORN3$AKz+^wKm43s zP9DeKjoZSY=Y8G1+OqFtT`o27PTsMD_k8`}@5?@g z+wKHh#foru1lM_QGgMu3ZuR2qFUZUKCuZnZWmn25OT77fB)@yZ`(vlYSLnGn^Sw@| z-yz=`2D>h)|M;fGN5AWw_?q+~pwFCB>3Q_1vyxI&^z3_t^ndN2zsTE14PU6^%6-&v z6VAAcyr%qpA-`;=d8b^o?Pm{AKHtY<9rxg8vm3pt{(w%($G-d*BZk~eUZM9`^p4kB zZs$Ev=$?yUAL{qN@vH+lW@OwYt@>r)ukAN_RA2k-mEey7R)Rlz#+q3J;3I*^FQfcn z+Kx8x7yWnlaeQWm{98ITHW4TGmS3D7uN}ps6#R@w5amMgD4~4BBZhKc@lfNV zCdXZzYObmqqcwfq<$$E*4L zsj{Wud!_QbwzXoMx@3OnFzk@|q01l^a)wHx(BU&<(pzC!tTr@<%s=no;se7!!pb#zKR-IwM2 zS7wx*cpj|j{2mbFS#I&!d3ay%k0`r(z30aL@l33}Av6MO{n+bw)0@JS2bg?3I`_%QHY z7QTf2VolCI(Hp~f@L2c|@IDJ)4t%+VcVqspvhdtj30rvXt3)k4_f_H+p8F~t7M}Ym zofe+^D%}>o3;99G<+(UWezT+Z(7fR9D{qzl%zF=Ee2$i%!G25x`wkK0bxGu7m9VGG zut(Y@jQd;Iz{_~vO*)dg2!EoBuA0WWlj~}hoY>Nm8`$bTmi?XR4CFKnYHp4!8|pmH zBYNCdXgj%oB;rI5{UGE$_|$s!JqM@|`TV`&a>z+}-niq@GmAr%vj^-WWd2uM7iy|g z=hbz!Ig>?R2y&u;v%lK+>f0~B>Qb@DUZS6PKF=gXnIFs7>Nt|W3T2betk3s*rM`)0zCpR|kVF0? z$|j%G4+EbDq+Gsd)nnlqC)!K?z2y&e@qQtHi+`n8=KJSI+2j*D*v^zA^-VnUXUdI0 z4*6p!n|xBg68Hold0#YvbQ4lubUV-vfOC&?z^Lb#vIl?;;H9qP_CB$RYkvLEsYq;;2vl4wOwkvp($= z5hkAfL+~Qkbxpp19+XW!sox2GKF}$b_svQJuWan~+>aaMvl}pt{+K}AqL3dl=NdU&5Dk+k%ug0cU9rErfc+f5gwBJis*a>2iyNC(sJQbp~syyWz&?u3tjY80&n}v_!2VC zroWR5=r;X~LjLpHRzB)_{oh^Gn=YW2drX8}-%nanon6?AeCDquH)_AeeBJZ>{C%Ie zUF1u@Ubc(^9D`mnlC9 zIsbj<>+MY!UFPtJy=+fH-Un36E*0M`le2O&kmtHd$KmaNUGmA5ul%lA7^Hp6fVb`D zd`QUk$jR#Y*oBQv(w!Y0@}JqBA;_C?!PhH48~&3og#JVEt`&Kf@glDsaykJ2Qs4iW zqVX?&Eb_$e?gDmmo+0FXQymJ;Zm0`~svBy1jRjL*X-vmy{QZ+3K4kAx|3!UOz}s94-O)!Ew@e*?f5@;6Yd>uQO^``or(=0k)@)T4ht7Sb+$-yv=3 z=kE>L`q|$Iy}#D}{#d=_D=ScscJX&;0^k$8w5$5(Ts9P>(@*fb>}jK(!uRV&nf1Wm zFA03ft+{@s_J51LMp^nb*VSbfp6gMw{lrc_XF&M>8z=h5=MBP^9b7l2Ej-s-wtc)0 z60%)(WGBZ>q4uMk9YM+=q&)h`{btW?xpt9u;QA_Q;3eK%9}u>qKbIpORe)WL59+54 zIZiuc{C636CBIGK|pK_%lQuMsZJS72n1AjT?zM8|%ckTjWH}f7swzupy2J33hwNi+jT*z~^Yx|#@ z_hxF~#`lgF2B#f>x9#V=M9B82sIF#~Rb_(sep6_doo_ zZv6(X|A=-EhTVj;zedaH({Pa+fV>dk)ZhRBey5U{WJmqQ|9NfpRO*cu(93*>koO-a4Q>`cvud3F#c`2> zyfY{4e&N~IkNpSr^c2v;aYD%PqJ~RrQ*&cq%RxsU$PvLyI~sj1%bEY z$@LQ<^VnvU2j}lj==f1jJLFySz|ps#bM+~0)RQithwC*$>Z@sNSS&M_u?>>vPswkz zKk?IAQ{POheujF=fVcgz=Y5{9&Y3JV^<|Eu5af7<9RA|dA3yWDaLD*)I}>Kx`@DuJ z4U4j$8gvATycpyp0Z;$#yIHqA;hrQ6GJd)W*vohjGA?S|ht$SO?d1BpCAH3~PsgA0 zmiI0lmkA#%zP$f2w|Yd6*v)=J$o`|oe@jUCA2>dyd7`G zhmdhnn|`e|Ev-$}js%gCZ+`~z2EKKD(f*@9cgCN@(S0|@CE~Tb^Yp7en|9uGsV{N# zfo|Kubr&J+nO@)AtacyO#vp>eTv>LPR+Qk7fPm-C(XM;jZ;)!v;oLYyjjuS%aZmO?dxTLOm%HoE`rn<=u%~@xaT=AFj zi$VUg>o$D)<(7dJ)Z1A=FYjxFyg$#XYg*RVzN$N}{raZg+L80VnDrNtFYUwjC1k&o zakHc@KT#2T%OIx`uyJu@w|`GeS5qGM9SFJqAmc{MJ86k}D(=+!W@!tlrQ^^Bd2v9` zHIM8&_v7!=LYMewfVbn%@kz*Ws-oXCGgPB~zPF~XwzVny3?B8-56`_iF5bP@&N!&z zjjO3I0KBb_{tz-hsA;UNJ5i-ZjSWiWviiI|1~YDLkn1Yl^}UI^t-gx-Itu7x`x3I9 z=hW9Ot~27t{k|T^`F!*_ZP$H!nlo6XotaM%GF}oVEo)}oV$~>3E5sswiQV4yIzE2D z4|bh?LGAWgHwcHcOBi@NPK*m7^P1(3-Lo27n`-K8ji$Z?APK{JjS62JPQhogdzm-0x6ln@Gj0*ZP#}71|L%y%3<_CC;4Z2sz)u zj+5&`Ia5qK;*fLX$u$rEX_v=GLSC=^53U2bUgbGB?dpV_9?LGqgOKCAxu&T;)RMDF ziF!i7+wIPNMac13TeqmXbxF&tKGfyui$m_Bzx`v*RsX)! zG1D3U1@y7K3F+UGy6T2g>z$odG1<9HzdRc;?mN%%ZaehCCBo2GyK}!l=we4X>IDH& zui*15V#lO#@BEqluN`upcx2~2Mh7py4f1;RKkf_Ajx_3ZTXwL&5i$?0Q>kH-6%jKY zrJHm->RcnrXa4zTLF%al-fm~cnUMXdrMgMYONIMW6!P9*e_H9ft@o~?o{j=~*pCRU z{#4P2y1f3>1G#NSKQn*V2QPQ#Lup6fZ?(U6JMw&ykmFdNi%wR*zn*i>j9(D)lJ}2& zF!ryVZ=qi?;O+R)4?^n0Jdv+RgsIEamxkQ^Ute+U`nO;BM(E;KNkaSeWA&-$L7S?Z zR_supA97E=J+<_^m7PDMzHs0AzH$;6#YEVX()+JreE&QHSpI^>Cjh-K>T=*E4U>SS zf70a`pbPu$>6bO$pVlxA=y^q#+WG?Wqasy1~7p2b;+I@A0pff ze1L(ybvXrCR)O;68v3pPKVTZ?^<_AxZU+qDT-S|r&NjdjoCk&hy8+vAzEz3yAUDoK zB7`_ENCJkiFXqF(PzyZ>-0Qq_e^4JJq z51