From b90e23f952042e8ab3d8888d1e64f300a9644573 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 4 Mar 2024 18:26:40 +0100 Subject: [PATCH 1/4] Add a protect_with optional argument --- plugins/qcheck-stm/src/config.ml | 12 +++++++++++- plugins/qcheck-stm/src/ortac_qcheck_stm.ml | 15 +++++++++++++-- plugins/qcheck-stm/src/stm_of_ir.ml | 17 +++++++++++++---- 3 files changed, 37 insertions(+), 7 deletions(-) diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml index ac6fd680..f3b235ca 100644 --- a/plugins/qcheck-stm/src/config.ml +++ b/plugins/qcheck-stm/src/config.ml @@ -6,6 +6,8 @@ type t = { context : Context.t; sut_core_type : Ppxlib.core_type; init_sut : Ppxlib.expression; + include_ : string option; + protect_call : string option; } let get_sut_type_name config = @@ -97,6 +99,14 @@ let init path init_sut sut_str = let context = List.fold_left add context sigs in let* sut_core_type = sut_core_type sut_str and* init_sut = init_sut_from_string init_sut in - ok (sigs, { context; sut_core_type; init_sut }) + ok + ( sigs, + { + context; + sut_core_type; + init_sut; + include_ = None; + protect_call = None; + } ) with Gospel.Warnings.Error (l, k) -> error (Ortac_core.Warnings.GospelError k, l) diff --git a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml index 345d4fd0..8fc44854 100644 --- a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml @@ -4,14 +4,15 @@ module Ir_of_gospel = Ir_of_gospel module Reserr = Reserr module Stm_of_ir = Stm_of_ir -let main path init sut include_ output quiet () = +let main path init sut include_ protect_call output quiet () = let open Reserr in let fmt = Registration.get_out_formatter output in let pp = pp quiet Ppxlib_ast.Pprintast.structure fmt in pp (let* sigs, config = Config.init path init sut in let* ir = Ir_of_gospel.run sigs config in - Stm_of_ir.stm include_ config ir) + let config = { config with include_; protect_call } in + Stm_of_ir.stm config ir) open Cmdliner @@ -38,6 +39,15 @@ end = struct system under test." ~docv:"INIT") + let protect_call = + Arg.( + value + & opt (some string) None + & info [ "p"; "protect-call" ] ~docv:"PROTECT_CALL" + ~doc: + "Protect the call of the QCheck tests with PROTECT_CALL. \ + PROTECT_CALL should be the name of a function.") + let term = let open Registration in Term.( @@ -46,6 +56,7 @@ end = struct $ init $ sut $ include_ + $ protect_call $ output_file $ quiet $ setup_log) diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 80b56456..8ef17c49 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -770,7 +770,7 @@ let ghost_functions config = in aux config [] -let stm include_ config ir = +let stm config ir = let open Reserr in let* config, ghost_functions = ghost_functions config ir.ghost_functions in let warn = [%stri [@@@ocaml.warning "-26-27"]] in @@ -783,7 +783,7 @@ let stm include_ config ir = |> Mod.ident |> Incl.mk |> pstr_include) - include_ + config.include_ |> Option.to_list in let sut = sut_type config in @@ -841,11 +841,20 @@ let stm include_ config ir = let call_tests = let loc = Location.none in let descr = estring (module_name ^ " STM tests") in - [%stri - let _ = + let expr = + [%expr QCheck_base_runner.run_tests_main (let count = 1000 in [ STMTests.agree_test ~count ~name:[%e descr] ])] + in + let expr = + match config.protect_call with + | None -> expr + | Some f -> + pexp_apply (qualify [ "Spec" ] f) + [ (Nolabel, efun [ (Nolabel, punit) ] expr) ] + in + pstr_value Nonrecursive [ value_binding ~pat:ppat_any ~expr ] in ok ([ open_mod module_name ] From f97b5935184623ef6d9126adebcf0655e438cfb3 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 5 Mar 2024 16:36:15 +0100 Subject: [PATCH 2/4] Add cram tests on the effect of optional arguments --- .../qcheck-stm/test/test_optional_arguments.t | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 plugins/qcheck-stm/test/test_optional_arguments.t diff --git a/plugins/qcheck-stm/test/test_optional_arguments.t b/plugins/qcheck-stm/test/test_optional_arguments.t new file mode 100644 index 00000000..26d56f2f --- /dev/null +++ b/plugins/qcheck-stm/test/test_optional_arguments.t @@ -0,0 +1,32 @@ +In this file, we test the effect of the optional arguments of the command-line. + + $ export ORTAC_ONLY_PLUGIN=qcheck-stm + $ cat > foo.mli << EOF + > type 'a t + > (*@ mutable model value : 'a *) + > val make : 'a -> 'a t + > (*@ t = make a + > ensures t.value = a *) + > EOF + $ ortac qcheck-stm foo.mli "make 42" "int t" --include=mod | head + (* This file is generated by ortac qcheck-stm, + edit how you run the tool instead *) + open Foo + module Spec = + struct + open STM + [@@@ocaml.warning "-26-27"] + include Mod + type sut = int t + type cmd = | + $ ortac qcheck-stm foo.mli "make 42" "int t" --protect-call=protect | tail + match (cmd__004_, res__006_) with | _ -> true + let run cmd__010_ sut__011_ = match cmd__010_ with + end + module STMTests = (STM_sequential.Make)(Spec) + let _ = + Spec.protect + (fun () -> + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Foo STM tests"])) From b6e3bdf7acbddd788b6bec5e0ee979abdca57e1b Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 5 Mar 2024 16:38:16 +0100 Subject: [PATCH 3/4] Add tests for protect-call (generate and compile) --- plugins/qcheck-stm/test/dune | 58 ++++++ plugins/qcheck-stm/test/protect_with.gospel | Bin 0 -> 208098 bytes plugins/qcheck-stm/test/protect_with.ml | 13 ++ plugins/qcheck-stm/test/protect_with.mli | 22 ++ .../test/protect_with_errors.expected | 0 .../qcheck-stm/test/protect_with_include.ml | 1 + .../test/protect_with_stm_tests.expected.ml | 193 ++++++++++++++++++ 7 files changed, 287 insertions(+) create mode 100644 plugins/qcheck-stm/test/protect_with.gospel create mode 100644 plugins/qcheck-stm/test/protect_with.ml create mode 100644 plugins/qcheck-stm/test/protect_with.mli create mode 100644 plugins/qcheck-stm/test/protect_with_errors.expected create mode 100644 plugins/qcheck-stm/test/protect_with_include.ml create mode 100644 plugins/qcheck-stm/test/protect_with_stm_tests.expected.ml diff --git a/plugins/qcheck-stm/test/dune b/plugins/qcheck-stm/test/dune index 6b6dd33c..6c49e772 100644 --- a/plugins/qcheck-stm/test/dune +++ b/plugins/qcheck-stm/test/dune @@ -42,3 +42,61 @@ (alias runtest) (action (diff dune.inc dune.inc.gen))) + +; include dependency is not handle by dune_gen + +(library + (name protect_with) + (modules protect_with)) + +(rule + (target protect_with_stm_tests.ml) + (package ortac-qcheck-stm) + (deps + (package ortac-core) + (package ortac-qcheck-stm)) + (action + (setenv + ORTAC_ONLY_PLUGIN + qcheck-stm + (with-stderr-to + protect_with_errors + (run + ortac + qcheck-stm + %{dep:protect_with.mli} + "make ()" + "int t" + --include=protect_with_include + --protect-call=run_tests + -o + %{target}))))) + +(test + (name protect_with_stm_tests) + (package ortac-qcheck-stm) + (modules protect_with_stm_tests protect_with_include) + (libraries + qcheck-core + qcheck-core.runner + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime + protect_with) + (action + (echo + "\n%{dep:protect_with_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n"))) + +(rule + (alias runtest) + (package ortac-qcheck-stm) + (action + (progn + (diff protect_with_errors.expected protect_with_errors) + (diff protect_with_stm_tests.expected.ml protect_with_stm_tests.ml)))) + +(rule + (alias launchtests) + (action + (run %{dep:protect_with_stm_tests.exe} -v))) diff --git a/plugins/qcheck-stm/test/protect_with.gospel b/plugins/qcheck-stm/test/protect_with.gospel new file mode 100644 index 0000000000000000000000000000000000000000..e354f099d66adff074ad1798250ffd4fc1113773 GIT binary patch literal 208098 zcmbrn2Yggj^FO?^d(Unv>7)R%p$7;ZR8-s~6j2crJ7P>i0+Eo!6sm{?#BQ)FsEb&! zAwKrDV#SKREB4+WyN~|AGjs0l21wxdzWHqKojGUPnbXU?clpKFKkV@he!=5uj(F&k zwH|up@dS^jw-k2u*1tqS39gX41&akoST8g*&J>88-- zLX+fpnK%?~3r7lDkTj?FH1fVm-mMX*k3t{9luO&zZqWE$PkKqif(X3Vun_!bhT9^A z73{geL+3Qis~%ckTh&lk(L8iWLu19fp`(Wl8(LReIkcgwVqV?Q=9XDNI4h1N|19#K z2r&ws6sl)a+ngk8F^hEeRXg8|I3b1Jf<~sw4z(fMcK0{~oD?ubuGtdlUt3>OyD+#< z$T_?OBx03wOm*1tix(p6B5lqdZO%xRd(S-d+@`y89fODYttZ>^}XCKzSM<~?BZX3{CeL`z>eN{C$hRtqhZmh10rLcy~#bnkZ zg$msiBHw_pQ>MwB7z&j@hSMeNlyZ(1Mx4cJO1dVeS4-WFq>^VX4XdDGjgafYO_2N$ z8@C%9cZ?Y4^kKM?^FOj$(!Qw8ky3Dls_7GPRx8vuWyC&0em;7oTCI2F!pSNWxF&IL?(?{xAFBVS3xxlf_e zkWzakTIG*u%mG&Uql)ewaW*M*pgO1zvWv57JI9mfQX1Ti1`iY$DLe!&x|2P! zmi<)A&<&b~28M4HKeaj6wmDa`nIEdAnGxqBg^qIA1GtT*z6) z=~xkV?z8FmQDfj!jyOB)+$FyHO@pVpzS;x63WdYrNZ$$b8e0}Y`mR^R@#OgvKO|Hj zN<=X|yA9Gdtlbjn*V5WpS3N9bD2L4DY{Z60pVs=?7KC)0gcO&+vbBzZMnhR>oQ@}7 zE5K|87l$JEg^-6Y**r8vZO-39+)F7=1#xc$PYb~{5cW{m`B9T^s7RyE(R?&CNb!># zpJrg+YMb62dzc9p1x^I=!1f>$!t z1}7gO<27VGr|DlVoZW=|W3cCjLa2zG!G=cRf2c@1Oc}!9JzT-HA?I&a`2%?RNHU!~ zR^a68zZFpm5&MXUs)Nb<5qZCdh*=8$5Hgg+GX8;#5w5F_*T_FuSSXbEYOo@>PY@ka zuq7#ozj+O_YHMn%n}aPw+%`(WtLvLvo7x3~ZMtofhP2cL2Q<{pieoBj$F*%_JTKQR z7_p7Mri$8TsFQLUEFKqZFFl@LvK9d`0m1)Exz@)14P?JM{$_aXgwO_D3^j0N(LTFR zV{7vqINDjXKhaG5;O9kC$UBL=r=cdC$Gxm}q^BssoQQL(LdV0;@tyG58hk>;IY*%; z6jJ5AKm+O{&V>p!awbJP;dS9QsZ}szwZ_knIBOJItaRKFZ*Wpk@cG`;aace|I%etS zu0Me2E~1Ac&J7AZ0_)G`QocCWdvDOFNW{5Ap+`Z4l4R%{sSs#B-A)n3k*k=YW^J`{ z+MIND(_>SJ-X{7i;ykX<=kRN-$e0;Mp97Dz)~HLfejauqCKH~3_17(vnH5vZY_8dvCK!KG5_4fWNq-4NYR!5}+~ znY+n7%jwPmp|BR^erSnW>smriA2R2nSb7t=SbDjvJ4IkCat0tFmu%RA#?jEY4WYJB zNZUy}CJ*VDoU1t^#)0^b60Yd|J;vK395&wEa4EVh>9)3%Ab@@Vn%FNmueGJ3vaXt& z$?CeG+d>A%2K!e8-4R;w|B@9L@_Aa35i;~!&HncGD`{weC#IK@=Xvt{4l~q?;qVQS z@Zd>tW4};|@m9-4;`&XOF)s(q)k_FTnHLIg-GaYR--@QDibWeDdJh@z{DZ?XbT!_^ z(?X#wq284hvr)EvuwuJ@vX=bkkpD7Rs?cimkwuU`nY~onr?R1;4qZOqAb90LEUs_m zB20~-Pwogl=Kv-y>r*wSq6x%&LulLnAcpelh4mXEd_~wLQ<<`FO;?1RO78A)6eViJTadyXGDy*Dn8&mSegLyA;N-LUctD1SLLNuC2JxrtCfuCLYBWQXT_MaMd^21IR8#qf0ToG^2hcNK;_<)bW zhG|5kP%5$aocOp;L40m}z~>;A*;S25zA!%SOAucaAMiDZ&)|xPDz^q#XEa}ihaF$o zaTpwf%(qS%70sj@$@Jm;8O4|VA@ipAfP;}q$zkKYJ?u;jJE5>s9D;A1y&%qb?`5GV zt8LB{zD(oGbiQCZQ&Q@>KdR}ecw@hXrl;cr{tHb>(DXvssSZ2kVdp?q8Df3MK&tV+ z#j>0DQqPx}d^w6Qhe^U3t1#z8xwfV6OY*L!$}+0l530U$k*Oh~rCbXJ*4CG!q}SJ1 zqk>qLAIP^mEf_@$_5{n1E>Z@T`=mORji1mPMFiCW*O2jzLM@XT40PlOR0z2vVz0wl z1*2o&X}u#jbcBe(G_|FAb~Wmn3n6YiI;Sn6K6Mp~(G^ehrN+wGC(sEC89+hq3za0nIrSG-ZPtT3fbts&5GS#?pe> zw4e^Mhq}lD$h}`p?%h;fW3ynp=BGVyIVWDbx>wjDy7^ zW&N64nriFOHd_EP&p(h81z@J}m4`~C7e+fCDjh#z;v{bF@fYelp{c2%X^Sm(zVdi8 zb0WrfTzmjJb?@n1%Kr&*RTu=&__zWX3UEhQGHBwoa$fkrw5~cT^91rZ4ps$Q!1rnN(E{t`l8kHn>g-VO@r`l@>7%w~uvEwo}Qw zhAI!C%EQ5Snv0Z!?NqR3u%^M_YHqFEhVd-&UP+Y~P~}BnJljRC0plrP%xA{_U|d|? z)DTs60eP>Y$`7gXWAI$)BHw`LWbhP!&=LrL^}?!HHg3iO39FvKmq}oMCO+U0uzv~m0(L>MaAO^{ zvaX>j=E^PPyBo}>cjHSBNO&neU@#L%k%ld0^W`f z7ytp^LBK#ZK@-qYy)c&kt>n84j4NK|%d6o2Fg^f71Nt1?!?{?g`&yb>>#L&f`+|HM znbYBmAM9Vo2V{c%E3og$>}vdirgp}o`?wvf%O~*#Ll_^rkXXRs;QtoPPMV8glIU43+)tp{3Y889-(d%p9XfgHL2U3WU3(Wh1cW)sb|Io zyl7x|U&##&jn{67^eP?~GR{l0;4R~w0r1sIfQ6NS-mFru`5qHL`JUtiat0PxH#XPS zHSmB16OL#xzn;98QpN4~LFo-H@-*s~B;0s07GgiwG`l?8`?-;Ngs8_9_OpW1U@zKv zSgM79bN4r_Bg0571b>m|GC{Zy{7at8t-GFPmwPKXbKrWeCMBfYqXKdgr3NT98+I#{53~1`;_`3PK?E26zv-Vl%Wh!;1s zBXP?pHB70uLYzVyAg)ZrVXcCt4zl8gKpe6bbAXAHtRKdX6{*HFO~g{f5Fy9pn-_J( zf?~j9Y-8@GYwwN>@f=8*`%t`9w$QgQ&V`J&Mva*_ui*NSyL!;6J;XW>rwDk z$f^=qhpVikL>3Zc%mia5h03ho$8{)kf6CaMGA6K01^0u@qeW(w%B)fQxSP;oJg#F4 z51@?uDdTCDrr>jshAAC9-mKE*TMLKS=~8(^4aT`0SLr#_Z9a87jU_6$3KCBiiETDR zPGga!{puQKS44+y+qVq|Q`T(CYGFYNE{32Q5p=Ga=E}Pe;<%q?iS-Q~n|3JWjG>$| zmZ;!lNIXF#hOKGq*tC+q5EPvmY;V~il6E>ivTtO03f=~J^&;wqqV8kZ7zOu% zF*2|)-Y;!hYTb#?_Ku!FX+Kcf|Cn9CbPw1Mk+l3*)AE~5%b%JSvctf0Or)Hk0MTR4bRT*FHJ0TDVuyz9dVgj-O5x&$7iK8`9WA2Os9 zCCjPLWa@LcC{Y*=_gy7QdWgIks^kc(q@M)NlB@_7yD5Q^&XRH(^{%1b&7wu&CD3w( zXyJu78)qtA8 zLlFN3TtQG6r7$d6+EINadKRVN+CBKfje0ze=E=cSk?rOMJ>w6vb3(nbyxx&GRFE#C zsY@v&S#Sc(oFr+#Rt>yCUEo_UiAPV`J8td4e+PNbr1A#*P**UNRpcbpl~%FDnaMVA zT^U?oJ=o!Q4`Z2x%J;$#{ExWEbnrJTKkxU2N^r<$L5FE5r7q7>7o0WmdK7#I zX*fXA@QkJb#a-O8g^daIX>6+Q&?Ac|>26AT48jz83bKZYtaq%C_r;>p0g%EKx3ELI z7E;fd)bn_@OTl``!Yl;&bC2ZDPb?An^b1?%%Ik0lwSJg2s%rM#}XrsKZtaLRdsa(HFjqu{5I*2>awazt*4DwL1u@Th)}3T>*LJ*Q)- zM^Wx%%H>MzQLqA17m2t$m5LoG&IxBX$%)}{Ld)Z)_1m}YGb!&*%EKnA*Q4M|5WQ4H z7pdsMR`gI2-MhJyu|hNLRz|x`V_^!S!1=Jgk73M8&Y8e?zVeErOb@m~BF2zdFPv4~ z6kP!f?2j=gE$oY5!~_m-5p-Gfh$ga+Skf14(N4<*ura<5Em(sexDIoXjo^Afx$1!`UV-+s&<2?%K$9PFzSyy(wuJlC97vq`FvK zXlJR8ou$ffc|REfrpedH&-{cl-E?$*5UL**e-+y7SE@|bMb>+OBPV# z!<4u+%@C33=r{#goCkcpYTi|)Lu42o0yyWHa$*}RY z^J|;2kX>H6NEQ~O+Shn$DdS@Np#Dk=-yZVp*T#j`_}?)8x3Jhcp?($*L~Cm6Vs>BW zsiusc_<{3!3y%tUCSjOZTGnR*Ce2YLw_qLnSNuSEtAGhkXt8MMKe3%RwsSdo$Dpa+ ze4bq3_;~y#bloSipN#muWZ2~T`4x4wv&t))X1C76fi|n(Nha@T7Emh}96XH2&xMpF zDrF&;fZ{0?Emd>2%cW-!st14r)M# zH?-Eza&0LhFK;?+K1?nVXJ9-&2eznRil<^z0Un=MJ+Gl@QPh#2d!|w98~DMDFD(3B z$TJ>3FBvkurJ`zXdBgnbCXB}xM0vjR97bI(!w)>)TX;jrGXee&4Vk{Exm;E=t7nzh zHbi-T^~|Hp9{7RhHw%vrc_uSY5%ZuPH#9}b|3RCQ_9%WJ|JQRYrF}r@6!J_|x8BWe z9eY^)EVTFa(9=|1)!NjI{hD(0tgW#Um5}H;fihR)7cmJ*IEI+{CT0E^^6bxIob$!a zkBfgzFTM3uH>0|7581bbx0JVT3CZcw9c~;G<94fW8KQI3@w{*C6MKqb3PNt?dk*F}H08TBN>sv3vF#1_*493iS_ji#n>@(w! zmljq22-{L^Ujt|=wO&B2*N6gz*F%9!qp;Qw+2HP?8Jb0>}_HVYVW}nZoZA z)o79XwOh^Kf#&{H^%Yh9A(|Eb7n)_Ez&}njFIK_Q-Y1;Q?LCz5FHxsU`ubtPt}42W zwF4c4sCood<6tB*MBz!$F_DcoXx$)ghKRcq;zW9dpjUDtO3I3Aa2Bi6u9|2p&ApfA zJ|!9y-U1EcGY89b$Zcd3s&GETerQGrW|DHhTP!$PVh&*g5cdf34QuJ5xzqlfXdKO} zp?Q3y!iASX^-NKR6(^{}(jZjtBg$Tt>l-%b)=E5&r=fFeNK}8!MTYm7%PZ>KEsP!b zbRsqWOegq6t-?uAE0cK#YZs9BqofOCQn^1YVKS-XB5CD!QX~(g7DFvLqCnvuP%ux@ zf`Zv*5)%Yoz_9;XQSuZrOn`TUK-aDO9|{Fe-0_D&LhsqtZl}G2g!Q0ujF9=@2a&=! z`r*jho&P%#J5Y7>)4WPVJw~U_yM!IruijL76jkDg9E2)d2cfdQ=pQBG94R3Fu|SZt z@mdfAQjrs-BA1Mx(66q#es;^8j@1;OC;=Nt9Fg3<WBs zaH~k>456A;RD;0}{Gu?H`yH7uC!~v9oYd!>)CKGS7O=SzCUloLoJbMxw=|UF zgj>f+Ifj-b(2`uyqA)kHr?TJ#>C}^ETe$;7?mV%*Kg4!kS`MRyO|$r5*9~+T_oo6 z0TBjJYf39-Z|!{OHkX$9Xjz7+P#C+@&beWe6b^}lWn_?aJ+g2Yhi9LjoE%<6DCglI9uFaHUb6*xT%=frSq#yV)^ z;EZQPI*KXaEjCwI3HCY^pso(6s%XL_IC}bI2VLXCP!XQOmt#av44(x(?}~=7$o$mi z?}uW2zp6P64b7eOGFL(71^xNL3(G_?oJYiGjyQJEyn?>jtlu( zh`q3qFWSt+aI7mj7?z;)Jj$|@{jSl1rHJX6X5#q(-3Z>%vM*f>$>)#Yi;gd2IF{+0 zyF|PUx{~vy#wNTi(tFx0*eVz|K%51$YMYO5=wz{)=mKau_bI;c3I2E-r!bt2qV9W< zsl$qdUj!M;i9tEi=R!Jm)(Mb&$|-zl6Y(+pVu-&W#C0IiDBQ%v4UZ_LlTUP1KkSoU}+y7ly{um8=>+N_TVMz z!5DrK^gbne{}Oo@FdQI;6NkukxYd4)#IF^#iDN@t;1l-|Z|{6uehXAzmdY3HqGEU- z=zmsp_7wSdGo099b;_tF8S@TFC7-P9EK|>gf^$alh1aEtVmQyNZWGBXMay$Y1=O4? zh#ku$UMSd`tf~|<>jAZx?eham9lNy!x=uZVFFG=h;bADeSagI%>Zg(dX`MSChF%M4 z7k$r{erMxOPeSs#WqdhL ztdHSbWxinXDXAjR4s()H1Up!~URu;x(bQ7QM`$}PKKDWTReSU008tUcIR$UAiojDM z^jLBxvT#AFc9lP=h2yJ_cFWLje@b@73KCym|h}50)q0b+d&FNXB%Mf!s*FO}3)n*<41S3NCQDyu3j(-AVJB_`?P ztw@?ldeJ1kfP3QGCJ~GCr6%Q7lkz$TY&MBcW6H?wE6{}7O~P$_pJT892)cxQO~SZP znMoLG5{3vx&?NN4!#N3llVEUK+XQ|wf&X$$;0+UCk%4DSU^DXu9x{OkCFXV$V5xz1 zCUA|!Tw($jOUw!rSPp4{g(k3oDdv~}>qRGG0!Ns@;c8X@6mX#ljKR7@2$J(nAkRi+ znLs9@{68E2Pl)orhj9Q5_CI0#kFyH@ZN`5q-&Y&|6|CHUE_Q-BV2<%a7pw9gVf?HL zfm4kCKo+;R@$bdrh8n-5+uzgpcjJgI#-GZR=3is}L4bL|nCH3Mn>a}-oH5IdIgKM0 z8M6=~%nW0W4#C6V>26Fn+`Ts#@Aa^y&w-ewZ|!sn<9U%nuTtnEE)y317<))xhE3|E zkkofs=t!Lc|A}brIg*2{8R;wCg{51Z zu|4QRI_L-Sm%_Zlh5iQprAL%sDzIOakCc!w>qgC5Cl=^vW?!yY2)hNE%XVeu*7F-p zJD;Y>w9vvgLUX2Qla41@*2EGAh^|NEy2+**BYn66kIu8oXG5a-1!3 zl2@oiYpcRv!04|<@<0&z3V$! zu=l)26E@KVY56StDzg6&zl&(Ubz-x^*Td$&#b&sq&7|4I;AELVr}1KNs1z@A=~(1jG=3V5 z$E!rp87j=jU4CSdDJUrriBm3YW=a>q`f&PpKC zlV22hHGEC|SJIF!D%v{DVtChE`XXRSWWtPQFE&L zWd#dkt2^yP9-_VOrM=`NhDYINAWq74`r#rD+d^WZl*sfe)Wpt~JUsW)*kT&1AU;T4rcy zCvcFkzM;c|gygw`im#<&S!}fMJ&<;fSdF18O7Tl-?yD+#jfA}|qD}f)CjA^#zVTB2 z;PmO$JDGUWi|CQAE9J{HE;DgBUUuMo8#d{mi=x!9DEij+6j*@V+4(1L5~M!3f-e`d z=s0{0dc47$q?9=#^H{2>k-%BZ<*?IDwD%!?{c66f7xQEItuS9k92qh< zOMOikc=_O&i2s$ zfXurJ_);W-WB5=AE)c=ri>-TG!F!0{UD`zZ8*=Y1=L=rdguIR6{GP(@A+AuodIjJ6 zM8`A~Eg*vgIh>utEqVW{hIv@6?PP`YW$3tmAHEzYiefm<|KjCfEVQc#tx^r$1*x@3 zs^%o2W^}%1_XFhLaW-GB5G67EDx^l%7rJ05i=wkcm5dVP6str=CmAaxO}nsV_bn7{ zIGQhf&K%DwM{x|94aS{F(j-xEk!r)J4XUMKLYW%Bvpu`lAn%6xd|4s#WB6Hc*-s(P zn=VI-%p1f#aL~?n?Yyaw_i$If^kt!OI0i6gC>xzxC^GM5IPC{08f#ezM> zT6byJ&YKR6kF4d34AJ87`=NHEs2wLlUlYG!^aNL74kH+bZoodY%C8XYbIGQi?Am#K zPF__?Lw5_~$ z0M!pTe39o-;_zLwgZ_o6dp_ffo=1z}zr*~XIO$=LcNkyOzLP|xp*|x;$7&+d(840>Pu5p5zSEHj zy#rM@E$0hAdq;6N25^pSab?y^cJvn&Ei6<9Ry*BN^KwJ|7`LL2Crg2g;W%(&_7SO& z4Z|_j;ToKVFkok~hS1KY=iVNW`~)|nPe?NwhaUp*Wh_2ZnuN^DtoVaP{8gL+teft9 zOU;`N>5q=&i!AiT;Riqk#(yYG*&-AJ7>wm+X^~BvEn)vrwW*kMA#IHk_K@b+d_j1K z!zta_mf9z<;FkCJ@{MFt4F3scctzF=qGYAOuiEsUE7;qT-d!1-(TC7+^CrINLUjy( z8>QhN5%)<*vg%4fzTyNR1v}eN`x!Df-olp$B?U2j6H<^Pw%;NW|4;|X+HdB+Y&tS) zr~6#qe8_&Rf-j9y)?)YqC>SdW9$^JpDb_iE3ziA-oPeF|b9uW%^y8QDiHt=VjPZk(JT{b>6ojb_z&a9apg63IDp>i*E ze@>RbjfS(Sdl%rg|bC2r|yTD2T?7 z-@aJ(aY~JYRVKVH0x-ypGr&0gIlz0Z@vcKa#?GaI#_Ml07fSLbe((Xhm(rz(nH{(?zCha_vb}k#0 zw$h}X&J-t_v?Za^2@_3Pvq@`Gi__{&+B}Y|GHI1eJjA3G^S!%C>n5tY{A0TO4g6TP$a|52Y*Fe4lX^Rvr}ocZ zo2)yCPNY3I;0FO4UF1;+ctr&~<_btQsY$RpVN!aVlwOG0=7}0w%@JNg|Wt;Up#hWs?6yMDouj`6tG|G|6A63%7)v#m2dp->MOE?sPV4C_3$} zpv(H7$@*8K;3<>!99)IKK_;tM7LvDw_9*M%Esq$-`$8srck(61UOI|b_cd0`k{5ED zj57`)X9JE(Moh+;3SzA9JqIbr6N-^7kv<3FDcKN8OU5dVehAc zXDhv=mnm=3=neA5;SG)#FZ+&9p!5SMlJiCEe-0(*6>{DL-(3n~w(mtA*);Z@j9x?D za+&eaVdQ*_;~^k@Six^V8s09E{g|aud7f56y!$a@vw~Pl_g>vTmBP@h3@<4ao|epb zS;2q6a8)ds;zriMA9gSqZ!6Ki0N)W1Z86>|2l^f{H>yR-@Uc<_!0?HJX<)#t$mzEY zL$fk`qg3f&_*TI@Fsuf{&=`ZbX`xv3%i(15$#et#uL|}8{S~0!BStS4l_|qNO4S<- z|0;-?toL#-@QcITlE6tmk`-hIlxQ%(1O-Qe{xZ<-AEQ?V%8;&9qri}%APz5kF9pN& z7=xssK@{XG(LSIrP;flxF9H2AF?v;?484?U0vLKLI0XzBgP}UcAPQPV!5}3%2=s#$ z#M40Di$Gr=qgMq|Dl$hMK?a0Jf?>3R$ARHOFf7=XK{73KAEl}Q!#D+N!EgZ>PTrP5 zO`51w$Ae*#f>;Cbt^&iE%HUS7%>A{RywXAS8Y=Gtkr!^3yR|Iyu%pPdkXZ!jhbxHZ z4!molwQSHte%+NaiHD9on#|dFr7{@G6}$or*KSwW2FEe-mrP7%t&-z0(#+!(ya}A^ zkdU}`C7w;1m&_)mT@SWq1@8shHDKGOdC8ow325m&{c~&a)O0lcr_3O8ADM?C{Zs{? zhxF^B>F;loAt^ZP7&2SPybR*A6?_N8w{4ep%Or2r&AeDC-v!ep3VsSEtaryJ+j2}0 zHCHLwXW+P6K^%Vb-V#eOw=|Yxws72_WIur8Mg?&o$9pq4;@TR^F-bT!DA}LjxI;iZ ze@fo<;D~E%EXPFQxNj!;9r9yPka@p?+&tX`j=0vwa`0R5P39&gO9%Lvg8AUM5gc*t zjpf)+IG$Cq0&qO1U~h2T0FJl@XMko&nVR*g()9t$YYGkl%k^NfZBDd$ys7znUkAlw zV2zaYXvz2(UxFD*er}sSQ4l*?-rG5|O*$r*Yn>~2p5~muWhGSNB!(mj-z)7GK5 zC8FK8bGxq)$H!Xu)z)};NBZ2%zm6k6K0s3ouD=yL0m?RrvP|rlu>zkc$RdrOg~5wg z!NogNfQ92$K9SB=Wu;c)>o(*+1z;Bixtia>f@Q!k_&_`Zj#?4p=&EFAgCkc#tl)V6 zvt3yqT*m2$=PXomJlLMqOTp{Gc_(rtuAUbk+AtR{E{*3KsKhsbZ;*o6XZCIc-!>IJ zYludl*g;PA$3STo&ihKr_k>&TCI6Fh&i!GNbub2N03X629rvumOxBI; zYj!9YN|oVWfMv5O(3b*7aE!dKK7Qab5DNKh2@anM-$At$IEn(tf^VvVbD;BX&CQ#5 zfSdUq1aYQf2F#j{P_m-{9;smK4mB0wtV5N&GD6s@=2Bn*1y+Dtw-Ts8a^KIw5ObJq13c1YW$@K5>IsWqj%u;++fGl#ma`MG9h7 z!F#W!?iEg5RsfRXQg@1yWrO2X1&8lY)!?eu=9Y$en7!BPKsW2$CQ2Ad3FyDG&QlN@ zW8VA1rfZk5$+`~zS4$$hW}2+OIFaiy?&kY-Jot_!_Htz&88KN`v{J&Il<@8jEf^?o zT_|r^)F_R2)^&Kf#QT)+G5D@m@LTA=AG}&``cG>tpHqo1Pq9aDQ;Ht|-mc(pAdYNT zWteHc%XFVo{tl-51x&=F6y8VL*OmdSCd#r&>AYZhOhLSp%=>VxqHzCE#4HU_o@bRX z6+F)=$YaHaz!TR)^aGD;*Q-j!x%`@fgB3Ga7Me}~|>B;MWMf+~!sCZ&PQ`eqR&7E|H~2>({W5QIM(&4{A1Iy^2H zwf>jIlvqZITyB0<5YJ0{pWQAiEL%&3G#1&OC6stDB~Fi+Y*O%8uswq$#5G-gOYx%P zxt!zKi6>HGIVEB+mz|{GNub{>b$}mBM^(5?Z>v#Y)YYjnf9f}JVx4|1#$zLC33QNxA1ddlT!y-vo)1Z za4ILEg>jN3l>;X!JjoEZ^In-st!^Ks2 zV~iMZkf)Rq-=)O&!8_H$JT7_+yhp`&2Trf5;J4S!s;v^XBk=Cp#2+Z}C$Jr%5tF^lGntY$Q__D!`f-vCk-jzaTD1AhJ{|9~O!}3Qvp~4g!d&m)4x8Kn zsgS>ri~ zlFKO>!;p=4c(^M(VdK+F3nwu@mL!sB1W|q?2 zVZ)n2v(duyLGv2ZR4dKBHhdvy?z8X`&|pzL(yK;k9l!bZd^fJ>_D$VmY9LrJJFIf0o(7ePnRZ8=!4L=_=uUYs4&}?CvSxWPc4ZjF9 z?^>7#T`w|CwbFcK!!HNT#}>wc4lnj=kS?Y9(uQ*d|H{H^LGwHc9oFq~>-d^u8*f}SR_YgQI zhn>Y?ypjPQ+;HZE@lFbSiNiTO>`V(g`*Uq_E;l)s;dYV9xdJyBw+6SfOwLuft-z)b zZYP_ZYj9g)a<0W~zRAI;&pE;5+=yG9$ytxvY?E^fZj~nIwpfkJ+0Pb_a+o}sJU0*; z>h3p1ZSIWZaB0s|U&%t3Yg-s4xfE=^{IaBdJ8UI+mhmUgK zG&zs5uNqCxV|<@$a-QJ(Q6}dpz8`9GHuHU|$$3`n3U3G(HSl+0hRkZHGC6OzA$^fm z8^;Fud6!^AO;9`0V0B$JzjUj4NRaJ2fjl=;_dDCojk3{KLGrnywzc-)Ope`F@G%>hOJ)>FVeEIi_m@dI9b$`=O7;z(dk> zBheTd^(l?|JYsTgvdCy0m-oJhp2Ml&I*~U-YQ|G?eN3*h(U^0a!0V+`%>EA2(bpjV zm}R0weIVC&t;Rm}v;`bYk{))zA!|tv2Yh1C`olC^m{3fQ+2h!+yK)!L2`RKmedd(ir z6h9H|NuvkR=pjIUb`c)IGfkz?{NV;;gq`!Ji;S@}RZP>>;|A{mgj{4VOLM%?1l(XO z@pVmb5s-+kSwhpr4K4*unu|=ZG!;UV;|5Ox4U}mD&`xN&@O>Q9wY!_xsX%(T$RU=d zQfPX+!H0sTkBjgukkeizGy~n>qd+srMbN_w&GAAr+zmb!G$UN3!qUtVnmyd$D$wld zA~lw#LTL7NgHiHP7H!te1q~P4uBC2DiygLcM;YGr0HVEV^lBRYAQAxxuG`=4cmLVQDnOk8^`pf~LYn&ayO`nX}zsjAFaa zagp;aO|@iZy&Jp=Gz~6tk)^2-8Z=RA^Ch5}?;@958g(9;DNQUo#;$0l6j^I&G{aAG zgV%v(xrX&l)w?TNE^Pslou?)Hq)vCeooF8#y_rTo2O%3= zU7t;-C%S9UGH%b90n0Nn#B*f!LNhnVHbJJ(rBH2+zoyQG*7t5`<6zt_*pl2 zD`=i`k&i8nX7S5z@TZ`8#YMibG_%EBZ`tII{uVU&wxpze^beLsvv{i;j444^G?z;A zi>1*l{@e}z4K!c4$e)%*>-2YS@ZX^M-bHxTfvbsT@h>)b41wlX7r_R+&}bI_?FRcn z^FJ5Ca-!Dhf8CTmYiKtPbIS3BL;)g(f&d^4-B-VIe#7RlkjcjjhkrtcLtmmxX^S`& zA?G;qe#rfcw@I$`8gT@^O-Y(D$T^U_A4|}&ay?oj%0f;lc|Vb$8FJ+p z;kml;F^c@3$on&Nd*zI&_XeRsp@izI<+@s~m&)}*xt=fAv*pVAjrTOUE|V*-VL^e( z{Ul^)IeGuf!nqHXPp%p7^Fqa4tD^=zDgh61z)=F;CD%JR;0OV4lIwMFo1yjGqpmlE zp`6>L7F9P@U?ss$esWQFLo}u!&m*g1GU+E&%oZp2N zsIs~1h#;UJjVS_ht&8B~vXE3V$$B@m7|6{oGSre(G07cn=x`t#U1X#snZ+dcx}l?i z+~*>@Tas!fdBhFf6G+5GY?oYE!z53-q3DrwpK_6Xt(4hJ^1PeM@jza1k%^XM4wJm< zhVBRCH5ak{abYc!yyJ!*2;^NCImk*mo=GsAQTI;+^0AB99=mWZlYHrhqQlPp%0>7z zHD>@muV-?9a6^v-@}r9!4HE7{b1}lv{235!Qguenkr>*j1*bZ5qFI{faYM05mxqy! zlGItHoTYgf*k~vwws{!XDAH(2I7{;|uF=pYAQ;yu(qc(COY?Hv(D^_xtWlDMmV~o3 zue%$%7)TEnInk1Emge<#Lr(&NL5)f|86@n0ynb#-t;2on24}Q$F~`N#bhI)BpOW`) zR7PJKSEqsve9fCI*9meRCD&nc9gHhlq9r&lLEc{#Srl>>lJ_@77KEJnLQW%j|FUgD-p3*5W%B-yt-!njTx;ZtDPv~X zNe??+!cI!qNeW|O2czw8ki>8Biuq^@z+W@6gKBZe3Zn5e=1lzHozsaX(U^~DcQ2ZN ze{2)L^FMao`9u?F%oQ{Sy>(uji`*Y8DVMlmSA*bE7qLT-LMbU|GgJmfAbD502sc+; zf~BOO)liZfKysan++<0lq@dMMlAA$ti;LW9Nu;Ep)lib#L2{>y++j(iq@dMMk~=|i zzl-n)MI7^>8*-IXjG%3tfv$ccjd_^Hpx@6!Gor}*k_?fKeqO^K0|6QlMV_z*h%?a5 zYv@xTK_jBbW=kT@KrgSM&w>Pvh$2|)5Ji$wbn+VdB1q7PDDsje;WjJ}eY}Rg0tAhS zBClBzZo~4>#cSvrK+uRN!ebqA#!qg@CUwTTaGP5!{;*|c%)d@ctSq2omy$H*^N7hu z6QanMRwXAt-|vQg4FpYyl6-4PIQjXhZs_+w(1a+-kCueXLVmUz`ZEwTAxdHgJcXS6 z{BCY2#yk0FLX_kWD}|Gv-^&gC3kaGJCHWsnIQjW~-H^|mFbAR4;9|YOsdKKueVf*! z+o$C7bG`kTYi2iTJ@TdX$d}e5Us{iRX+81>$F)2dV|4q6d;#W_Be(fuSVDfKTxGD5 z&%*;lvT8*cwyns2Kjh&1eF@-mvPGv1i1HT;-+Z}N3!glHLq)LI`3~lP=fK_eWTbh` zm^W|~%)iX|Pr;c&|2*Sw;4@<8dt-j&h|BQ~6h8JA=x+i=dXmupFWy)N8fUn1M&g8+ zasDz69~^X!HO_Ik=bvWsSMbp>V+!#45*BxvF;_4}qH&TDgEzpuWCE|qQ9J)wyf}qb zO*Q_5VMBt)BzV~df2Q%{Or`PnH-0{PH(?^{#~h%Q(jO zm+}3N#a@V4*@!WL1`{{|Vp#U^CQ!$bD@FZ2BZ6S#=II$@Ftd~5=rs=R0MvVNBLo(X)wRF9d!6QbyJ6ToNa@SYtLcv!4R z!25Y{rV&K`t8ki{0dul3r-I0QWXvawzirIB(1DlaBpQFR5W9uM{LXJ3N9iGc={H=Q zu$xH;DoKqob0Eflq46WdCLzxx6oinK`*96oMFknCYz0{%(|rM%Gs5B38^Qy18IZp| zX$p3?>wt;FgNM$kZ4Tn$?rQl4Ili6O9Bi3W9n_D52b){)*(tofGFVqz*@Q2D%KBjU z)B~_gj9w>YhLC41$oeZla$>X6Xpr;y(jdggrJvQuucvLNj&rb#IYvqHr z^>JG9^#`a6R<^bXU1clYN>~hv+Isogy_z;QNs!{;4Bmzf;+;+{GuwseDeU%Pe43(t zh#co=AH<&?Zy!>tUq9Y1aAtcO`d0*Xdp}B8gO7Fcet(cZ?kb;l?}&iEtQj1zkZFqa zBk(R|yF@_+zae&e1p{WxED{ABM2{U?6cs<9E=p;2DU+)STlv@*t7w5i`!H8QEG8dD%4Cnb3 zS`SM0+MYn0@QZBs3WhT859Tpid|3m?PC{Un;H0uxz{}~R^aEza#MFt^I zjbV2Fweu)pASF!RfkSR%hx};@c|a@BhUlz+uk9FxSSGh-l0Qq zpy(D#K#@*T=ziBBiGAC9#8#zPk?F9sK+r3c@Hz}s=r8LW#a@MT6q3QOtxpJn8Mk2j zV`C#FcBMof`}!Qbor8PKkKO8hPjJcbUIaj<2@NYEK&)B>v76`5Cl~yh@}rrVIH>QT$ko8)UV@Wx|g>|!5^S- zw8@*#G>g!KMw||sxe8(#)i>7URc~um@lLF&S9V?nYfx}a)T)hf zR{cjmOxz80cPZE%8uu}I8)H^Ipb`h8#Q`{XTC@J{F~F?l#Y;pX8Ajrb2}PFL_Q(3B!axAoT0omh3IvR?~H zXDRrMYgKO7m{qxXIM&7AO`L><&U_2+2b~j4Zr7+?xjk*nWKabyjCU3KCYs!WZ7jne z&JHqnT)J|5TYg@C?qlKdsBQi@+Y&tb5kw4FauY55KD16Yx!A?GKFdwBF&}^`-NIWz zwZF+t+Qv3~da-lcvMfK=jB>Lr{EKT_{*st&`AhBR(Xnouf0Bipp>>J@8Ol(fSQ*0S z*16Hyu{-ilvCOj|=u``@bXDe2Ol6)AC&2Jk*mN)Q)UhxQ@cX7={WnVXWTgZ&0U;P%G=k%cu2%| zsL9(qX50iDvl>(rEsT>)zQar&Y-?{^#loE!H`xj}8^ZRt@J2CiH8yzOx4rN1;F1x+ zGI^g$Z8K&HOSx;wd)%`hrT>i|;3pK$z)|S-a|QG>dC$kC@kRUH>HWd9#lm=q-*+U) zVrhKc#$Zb$?+pu20o73^k5?bZao6om$i{6~i`lrhE!SRv-?8wKQLn!eXVGi++tn|C z@^uTp2wgKw-YYSS-nB7XK=q!5Ujo%JFc22)+s>ls95Gs6*`%$O?P0(lTKHYpr2Ood zN%>vvcf=1tdCs-)bSOI(Ym!lu@_X2rLqWBhh4IvtuiWHwNoeP!y?5lK{6foB1_`|^ zd|cF`?r|3FW!FmvIlZIjMmrCjC{j_zgk#SbF97B1aExy(^G5YE3?GoyT{|@{RJ&txL5M zu)Ut&#ll0P)|oi#0`|+}DCPMH7QO>|>rB3hS=YtJp!d#CvoLqx^GrSl{o6VZpFHo} zyi6+sJ3{$c7JfQv-kx#h?PWjMegG)OHg{oaas86tnM@V{bW`&G{!tcZAypsoi|*F!Lcv*0n&Y2n1+bpDbs=06Rx zBE_$U92~>~OD(=r$}3d}uh8{`#yY#G6s%l?FpL?hn`9wtK?Ayu?N%9BRV#H}Xte@- z*v=en%zR88Ef|4QkQNNrog8Z-hW@#KGyE3i_KD6Ox#x*1q~^W$jBeU@^u zY~l4N7+tqWoV87Uh$a6YGKA;0GHq?*DJ-u=w=^u^74G7O9p@Gd`H6CQ4a75p@=7T0 zC^xq>hF3vs%#8Tl(gZvUF9bQdh4Rj8ms>@#%9A(9e%G0|6$e|G-|)G_jo!**ERVAUMTpUVc8Q~rM_|6Ml&HKvv`P-EVY z&p=I030l5?IQlm#D2!$xx@X^b+dcFC#sKc3r|9a4yCTsXTeiV&2i9dOu*!``Rd_$3 zrm10G{K^V9GVVG{_3Y}VnS+DP-0oDgbi9Hc#3L-cY_kCCL@m|z!B&0|<~Cx24fS=4 z1_!Z;6I@i?0+MQXT}NCxAJ5QLRMu5DOLOHKAgk-qEg-h5YEE_4Tr_G6YU}EP?U&l| z8QQucih74*gr%gS9mHPo#yb(^+> zAxlBrw6h@3Gl#m(r*0R5Dc`~uq3|y=APco^Mb4EBj5&Bm?XC*oSGZgL>q3cxV|B(3 zU#Onw~@NyeZsk8_ z;r*n#p&8F#x2=p?eo|>$8P|B~sQY^Aej8-0v+!nHWsPrkXY8x+K4=s@nW|$ zPd)WWz%OFDrCS&?^6lm^-SE+R%$Vh&{B8xFM#2{idtiv(t(%2;h<>^O8CsrTEX6h0 z=^4-{8%zU({VUmh*t9~byX|Hf#{=$Z;i_G1WKN(S*HMp~IO`O=(`{tN1ZRlKg@c2O zie_>(o3RiDct`mU&gZGe7ApkcXKq8FG1yQDuz1Aqc~SO>^t-C@I<$>x@@Zs>(nM~H+Q_ZN9+j^>!J%#zD3c(Uf-jf!t*+oya z&~7)Bn?gH_YiQbWL4}~NsOPs<=2sNVaNVylU$grK49W}G+=8kG zY(o7y7SX|C3LYNsey7m7e<-`(eLcNx7v|xq*5Hx&fxF(qIGebg_q*vTv%Gbq+d|J$ z3SK}#)QxV7ER4taedn8Qyw2RKxj$!8w`Df!2EZp<7;p9P;Y`m0&ZOb7=3~GhUTba+ zHusl&a(6UsX1OTWl5VG2NtXa#Zs8|)G1pF_!h9<1!5&r+o1t1u633yM1P2X*1=5=E zZgf=bjOLm45CgUaFxcNFvVRBF2`WmcaJV-m$$q&J3K{gOfEg=9A|%>Rm&+1uHni zRf7Y|1!ua*-IAl6;+x`9d^35LQ=iGyryR7mxX5v^Zw&}z#c!h<)d;#fU4&cgD@_4T zON0{l*(M#kQ~;xy&vxJKip3PP;2sw_Givv1ady8!__lA~6zYp!r{GN&=?#0rrr@=h z-S4|mBSH6pi;M!@T2t`)c6N8@{?7dUkt;SGIzDz0-NC#tg4b)k$gOF{X7a40zPC`{ zJApjoA`ifnFE*@-y>P^2zNhHsi)US;CO~!`13r~0J^VncXeXydgwgLywu^_z5@ow8M!W!2+v+;K#0N_w@IU~4RssG7M#Aa69}$583mTRACAgqbaO=&NEzJL zT{}qfIn=+B`p=OhE8OIIFL7vahSiPU$Zq%B0DF4M^(UIm9rsA&fl&Nbxe5SBqCVBQ z^TnqMZ;JUeM|fczwx5E_1bLSRWXAh6cqWtY9;?Ul30j>9w6J%AE6H;n4H!!ULO{^W zD029&dgpu^u!;s;D#k0kHtL;VaE7Rhx<-||F6p3WfRqPlK*W^@cx%)h8uzfcL*b9w zxkD|$yfpo1@&Ngpih9SpBmHk_Z{(;$`afhpK!GK<^nYE1*WA_{5Tc0nj`=P6Web^% zMo$Kc4>M3(^|KZSqlEcfL{9_kLJ7NoiteW(O|imwfk_w*-l~mQBAyXdEq=s8LwtR0 zs%~j*s$bfHFCpy{D*94SGF7n8(7Uhd+P(BUnDb7;3D4Gr9`PdDt!E#Zw zG`rbL-YBvs=r)?dWt>HE$5HU$jqHz0R@lKQx4&3tkg8FL7DWXVLK+4xicH$oJh_Yp zUqFK|6YnT|O*Bsq49*bs3xl!7cZYehaQm5p`;rA7v3A@tL*s)q_)%B;gH)UvZHhGR z5y=~Yi__XQMQZIuD2a>7a~TyEQSpiKd6RLPQOW z$;vp#jd~1p=eo$_pu5{-@O&jcZ}`hOu|Cmlw_7$oeFlW>))?nt8A)eoEwMF? z%o>*o1J=yhE^^SW`uQpvdL9kc>6pT?>Dct(5m?#fBJ8$8SkS1))^rojc4MjA^)1>U z*cPiNHMLDx9E?rdWYrk`b%%o#D8845J|ynGnuZw~mL7Gt#$hf8cWWHKm=4L~fghSF zHM%WgdL1GJgK5~F@$T+*Ow8TAW|C(u4XdDGEucTvMOxwR2Td>D)fpG-AX@6Sb+d9VZ0qio^>>QZyG)~nkO2^8)9zUymon_>3SNkTbm^W zD{1(>@p+OpFP0}+4P?J$h!J#Fql^5GJb47~B1H3KSC_Id+1Ae-{sF=TF7g)$f!D(T z9Py2wAjNhCzDa-_bXS<%IwP5wg=SM_eFoko78#MWtC@H`jhId&juPi6T;*osKEWAQ zH>;NRDZ0+ofvX{5DUCSQl?E6up2qmu@smg6P8L@yytbXIRXbLpGtU>|2WZ3x@vg?_ zNus@P<`rZ=5Z4{_t6c;O{=UadCf=50dxFfhZd5%xS2b)f}v? zL2s)a0#2`W+}J?U8XCFQl?wQYsJAulYVo$hPqp*5T7kwRbE}y2A&p9D=j|`W+cF%@ z{F+~=#9sj15A@%-$Ygl&N&bL`J0{Bf$&ET3beLKw(-EM1%4B}d-Y$-nYkbjH2C5hX z@fa2RF75h+N*x(x{_2XsfsV}IT%=}KJ%0<0x`#$-gRJmVQP0nS=V3&RZGS3atELO) z;H8UhyZ`^Fdk^@iitcZGPso)b76=j&6*jxskkF({3CV_zQWO+RKuB325E4uQLR0Jw zK~&Vo7R81Y6crRTVppu#!TQ)9d&lnod(PasGdE;$_4oY#@B6}jZtj^mGk0dbGiPSb zoSDHgD7uIyy5MfEc!IThMKvEwrBtkiGvWl zYEv+6!1g*U(*AScWS!bYuNsT`)idf4YdqMHf@7)wR7uSS>VE_E-|WGr{0ap&<#)di zHkEqJCE5ij0ESnn|ED%=?OGbx+U-s5EwNZ;ZP!{8IQO~Pb2yXJgRNa#?KKp9DVi7t zzUQ5GVo5gGv@=y$(;7E7cjI3p{M=U84tgbZM=ea%+Ci_Rh>3~fw~-FrK!@HdC8pjV z_V8Py@slL|a}4*;_@J!QV>VZgmR41w8^t~my}*yDr;@ORywNcp@<{s*I`m!1$K5m_ zn+DAHkXL?h3-Zcup$~bLZ)iMIUZ4ONR?~p@ZRAtl5aeZMld^-{%WFG=f2St+p6-{N zls6c8Sqn*dUwdVP4+>Xx%WV$$wmT_ra)Y%@9B0CQ!pKy63B+6CPWed3u|Fb&WKj_g zOcdx%H1JFsxIzj@yj&S-P#HxnH1;(6)_a$_o|b!#FR5;n#v0{i797j zf{hYib5fQvpUgB&J@f#Rb-eA zrC`>nh*+Y)+)snH(4ehSqUs$bT91Td#8H4Tg+ivOX(vyT&`jJe&%bcB2U`US;4>f5 zAguIakR$JdyLligKWNx6&Q^Xsd?3ON$%W;0%2s9=Jemft@->!ctj6*zx!3t_1OIcH zcov1e!%2At@#dQ{#|6PwnOo)iq7KI&eMu8L6D{8dDYp~lMkKT9{SdEwCkG4pvrWuu zpopn)Rba9ZTZApt-sA?03n=?;yayP;V^!5LSH#Iy&^Rpz-yTD`<0TyrQSK#_d!1M4 z%5SU`y7IfhSLiC;&^Wc*NC7Z3P%hSM%#fnp0|i{uWenKvA$^;*PQzXhl$P>T#piaAxEC?CSPt#olPns2JJ-bool|@AxD@SD#ddObKY9x6+VJ zGz5Be)Nu9wqzC$JbZcJvu#2&z#H|46X|kc* zWqQpP!ZH=Y;z^3;k-H5Vr`&4aTRB3UE1nEt4dba659%IgqMY7a-FQ(nbQpdhAa=GB^i?k zWEqsSyb_(doil3SGTp*2F8(sc%sL4!09N+r(<=^Hk7^3fLN^vDo32=ohG^#`t`)U&i`DiAuPf%|j`DbeRm3@uhSuu%@xIn8Q{`7J zWvbqS3#_+Gv@B?Xhwq4xqSDNB(k3seu zH2eq}UIPBrn&2%c*o(gs@itPa`-@w&vF$I`!Jq+azeW=YFLA#~!|$fySRz2xRqxQ~ z)uXS(sJ+TnsV7k2P^p{h%@S5yoaqYg_AaWL|4nr|()A7vhoTB;+(9FH(g-v!)Hc@f zD!=yy59N2P4-b_m?Ab^KGZ?C9#J_AjQui}>q_&~JTQp)Tjle)76)F!!@Id1`Cv`s_ zXvmzHC4};N7kp`&cn^HvW4AQEZ_kMiG_fgB6h5TUztR|z%&PajJrwfQG})GCT)x%2O^R8T!JJ3Wim_^oqmkm2 z?uRrcLSwqPALREkuXL4Pwv?`VpW`cCN#JNq4Lb~@02ofEG0)hg+hMGfu9)(47*BzZ zY0P(YSPSq^&_qj=?jKHvvD`#t-rV76?S*-Bhsm1YdGnu62kasGpP2G=IL?i43>FeQ z9IqqqktjN!&|zoMVdqO>srO4gbg($$Gv!f3b?!*q(HkZyn6UD>J6hN34y2^XzzV1g z23U*S6L*4&6LaCRc*80r;7&SB>5TtFhX?5JwjOfI?`}a(`LS&yvKduN=PL2AXX-GP z0$}JthY$53ceEg<5IKedpV8s7>F{OXKUNdiCZ3$+bU2!klOb&ftg0)%^T0Pv6Sx2; zxtY^}C(wVfnq@a9SFhfoSVuDtal%SMec*~j0sEW||AG$3ay7aZ_5QmDSgl^oLUZ9Q zZe`db=Pe>*aYMHMVly1KF+C2D1$9UcpP z2GIi-{gVQ`RPS5GHDR%ZjRt*)!bMhDwct?wTE0O?fp67{ATGX(l|xm9W&aq)_NAD4 zE7mwN7fF7S#yu;^|Axk=(fH#%xRoDzyXF*7ep7sKtL)Ze8&j1q%%}02ZMfY7X{6<* zEv3MBH2ysr|10>R%2&j1fUy;hqygNSEV3XIoV3$i-w7B!q(Pf6tP@hey0?>7?bVF5 zbG27G_@K>KdX^*-IBcod29vB)SNixO8p*2I(DNYN&mpjO#` zpd(t+5wHn`Y~VS8@>6C{%8%~^FtS_aW|b;_FpQuh%#n>)*iO6HH2AbjD6or;SV>2~ z7BB5mP22*w_5-7V^(yTJg;m7YH_ap$|P45F&$I=N0qeldufHSt=aRp2K&GLMcNF3n86kN2bm%tWMe zYSm*6Moc(f)~y4KxhS7S2gy2TMX}ad7`6UU4`)3!q&7;lG|+J?0n#*!j+`s$`={O$-8rX-=A$D9NA> z_qe!xW5D;FCUDMMa=Me|nkbpWt617lgUI}!xsM9vvkx;`peJK z(dil;*Y5>JN4+0?kd2O;Qf#A5zla%*?oUUbZljZar9mehw>>4%(YMjjkAuHn6HlPj z4|3A4^jd8C4cZGTpY$6w0hLek!A|<++z`848JiYc2;CM8>%BFgCeTU8r8DZ=FvUp6 z^%07AC&6Y%&1iB@n%rN?NWDkBW{2$#It`7{slha4WrQ2~);^BFGWbmcq zY4SAvRlIvTW=;`km?Hrh_3qO#yD9FC-1ZTMhv=AAK4fw&Wb%j{I;J-rgQMKi^EH99 z+>$#v>2j)_w43x1+N&6RBQ;S1z99C_8d;i-o7Yr?XYFI4+LCeIyogMt>K zWufv1$27d(pAY=-3wShxk3;YhlW7FTqj07x-G3O4tr$5I1sxp^%Qf%!lJH z3rAeV(SnYBn2u$B+~%W*ohbIOlfKJqVF%(q4&{Y2RB<_mOW+jMKs9cH> zW9^yA2+jXCr#kl&9K=$s^1J#xbH%}QJ=tq zMH=djA`)&$t?Bst>G+4GT-5tB764+{ywKloxdwSSmJDa;^ND1}R?n4>O{o+Jk$*_X zf2u$9Ar)qL04Tpt1ORz2#71`u0F^MT_orP;h^TM~6)v_LQW_t??OLUz-A1%86|SX1 zm_wx9t_kc_PVVA>F`;vNbf}voxhlHt(Ux7!AhM=%8n!w#woIDjo`&B;7L(F&(U}Un z4oSh4MLHsVbkDC=vT?s&8=5kerof~-?GH_0KS*+SC+%01hW&LMcVvCteAS(<%Gc8& z98`>04ok<-L=h{{G_mrMD1wGd-x%~cQx^?z$g#1mLL3rzY+YHs69>jo~A%T1#!=j5L0p5 zZt{7)wfx|BSj*4p;B@A-!2&0U75XNtSSn5JPE&geX6hZclki%8a2F9An$y&lO=!E= ztCXfL2N+GPZmdJ0WFi`Vkq_tjnt3HcZEdDv!7LFb~0)2krPTWRVBNvV3@?llHQ z-yw}bz4K*H3N>smchhiMgVPD31`J=(2_5Xl&`I?wMO?(4ARW@_geaYG3Gs`l; ziPBP~OoK-e9Zb{CrfFA#|7cC%T#V#?PH-X%B3af97HTh;&mRZfxr7 z6?~J+n!#y0j+KaTx+W4`%At-leJ`5cS_(+LxAy?(qilVPtYu9-=(QFFAm59)#baMl zJQNUdPnzCOe+2Kdyqc~2`Unc@eYUCD2auaUEXM?g2yq%sf6#}*NI^lCZ-S$Vf;9aj zn$E%ls40R~i36SBNJc^WtBB*ps8jfgu*{P@$O#_CEx?lMbBpHS1{&W^Z2Nv3 zk*mQ;`eUCXMpOnBWBWwgK?W7Ys0f-A)Km3d>%o8>Tattd*RGd0!ApTRTD4)_kh?nL zuFJ$ZfJ{EIl8Qv{$e+Xeiyk0~UM+yA_w7DFRPtsbo0$KB_=1XYhK$uLZn6NuG%ZZU z$5An?(1MtzDWVbuJ;Vv##DItnIEV{EmDghM;i^AHu&yT03Es+p{PV5x!Mk;QI1?s_ zdxBNu7bS{KCKZ24#iF7i^=?!&WsTR<;$V~bikf@Ot5V3wN>2RMH6*8`1C@v(h9Xol zi%QP$a8!Pxh;jYS^5Lkm@-=p*<7Q_BzLrY1+BjxhW5ip=TB6QW@+p-P_;I15B9eel zfs=6!<5(Ud=!NZ$%`7Z>W=TE#qjNT;lFS%q|KRo6ZILH)&BB7^O+*5>DbB zI;xaJQOl;%LMkni7Ny>?KeQex#bgks-0rvM_X^I3<)&Ky!h(y2uaQYNNWO=vLQV=5 zQ07C&3VoWp_ELyQ;`HkH_UTl5j-(@pN?)eZcRh%dA4U=Aft26-K8RGhry~D%3Bzv` z^Ue7)wpb87NYs^Ly(tDASjIz|U>(>92aG6s|Ir1=P%zu=Ttpjaj}tSt>Ig6u&v--= zCnQ?>-6*z>Vi>PLo~d_iu5wG?o{B3N+!>rHWoS{%%Crc(c!MTHzMW#P>knrKTY6} zx#ZDKus62=)xi(eUUz^mR}<^OH^vF}0bdwecWx`eq1tl;h+&%82+qTtAPyXiw(M!9 z7S*-I9$HXJm+^YNcN~a~TyUh0=@LXcN)wMKirgVIGo5Azr9jnt7Z16`*vf!(@X^xM zoB(fFwp)M1p53$wp&SQ`!JAfWx{XGUArP4?V;6F)T{+%hcbp)?&FrrR7D(W5nmI-i z+mmLlqM46+=qtZbg1+*5+=sr(9CjLKK%oYPcWG988~qGRp_Y+H)SG7I(JY)invt&w z96g#m&dCsknhXOopionM)4>NM6j21e@lFO?=lq3rfj8JwD-A)GsTjwoXoiD0OcV1G z1+)*%dYEQCA!VfA(bv08ae=ljzzF+qtu7P+U3)n}-G~@;0sBYx1%$+XMzg+_g!ZMf zK~y%=15^2ZDPSr;wv;tZS!L`I6i}E545w1rojx#eD=V6)3^p=)5cQ|BH>nKv2pNZH z;%k6(q?6H&`4pIF<-#``qr{BQBSOF=LR9zeA$H9!j%o zY4&0%FZF)92kig-_639_Urn>GljIMe*h6Xzp_GU#y8!0N3$OXtja$a_xns{LmGeSOdO7Cv=Xlrd+Fi zaS=vnttQrjbqZ<(*MPraU*O^1gndEi1|2z;UP3o&;`T(VKt5F*Koyt{Y-qMy(Wqh1%DV-K0=kSJO=pc z9V*3oJ^yK&NdB^d#!9h5>PAOi1V#RQatWdN|D+Lh~TB zFcN~<5oZE^7$cx#P=0L9h2n6B^eU5&p|IW-h6`w(&)7Hgu~j4fLo|}+eMcv@2LGp; z*arxfI-!qEjrdx7VXzqbMiV%eCOPJWK4hfr^=rMdzuWq?hcpItq3_*j=E24{^n;Ew zk|?mF=*0PS;*tgiR=s25?*i+yE`UVegLMIX|E_fbzE)2sUa!B5ckk?CP6_C>f{uFs z%7>0h>B0sl{0JwzswGt&Yq!_%HiJ(1If99K)yY(K8Tg;q1Wr{-HfVRN*Ss56b~Jrb%7t9 zc-93TN_)00z?ZsHb#MJuywCUAjq>X$$f$SUu@-KM9pttbF|nGe-|``&wjjv(IgDBD zSgLWTrW5#~l~qI#B|h5;4>HIM(_a0+H(V3_!8gYV%amCpX&7@F6-7Sy4%b8!eC1A< z2Y!&Gi5nMq&CCc?G`R419WRar4^Pm<=xBnFj-#5JsRlv_4NkqAn|p1A#{by10Fl2; zHL~}VKlC!yniUJ>_nM%n{QN5xa6=+*ZE!LV=2X^pquSXvikZAM)tv=pW)n@I+SOFc z{7`@>;x?3eg_D`(p_qvYlJeRLzMh(R1bmfFW=G}|6f-eFQheLMcc>Za;vr}Uf z|H`zWX%sUtOHv=X6d!@AMG>zgisBJ8|4^DgL{L=kqr8S`qxe6zEI{N%G=GNv5ZM-BScgX+ z$@5kf^OaJ%Fq#gxkPnOPRv6>d$yB!w)d7hx#;JhLLuY(Gs5&>s$+WaW4{(Xmvwj_Mka$Wt`&Fh0E40b_!;6e^0_8@MK@_cwg2ZrYZ@ zt9`OWV5}NgH5NKghlR2=v_cba=wyf0-9gnD96I52qT^{%F)gYCaiAs^A=%3uFrvJy zHNQk`DZ(9fB(o4>Crzx@Uk^QF722~zQ)qDuT8ut3grSWhxX)aUcFte77DkZw;-ZVr3cKyRUlC!z^9phqPoyZnK_XI=-%ThqW!C&%$^M ze4+A6eBTLUaa#GIQwd{nS`mZ6c(xPf4OO98vUm|bUi+b!2p4K14~*wH;W1nd4&AL9 zOjAn}?i!w36|&1KgR`vLS)^{9pd(}c-8wZb)iS zKZ23~wLqb32^)}9$7b^OsNnRXUOkY=9zAB2b?=okop(g&Epn=oc}so%P`!PjxX$4k z&RSHN%G#RhvQivAJcDbVTg7;Ro`vA@Fcw|m9#Z=-(40-nw$ZZf2!Vm7 zB3?zM`qXF96^6mF)BSm;>n22008tXhqH7MF)QnDQA!ViB4+1~e^8rM2XxUq|?473C zFL(#gNt4jfnzHCBr<0DNla3dQF7;ljYu5n3K^LFS0$Chy!54v-(MfW=2C4VUJt!5u zT%c6%S0b-mbPy95v%?LEfYD~gn?l@6C%tNmiHv`Xn2@1g#)m`|bkZM5fxyYw=9cl1 zA$gOS=itTFIF>n;*FC1ESy1muV2NS*OrW)IwHTaUbBb3bQ%T5@qlREoZ!w zz14^A;ty{!9~OF-2bv^C-0l(J4E?hK4>H~)`rHQ5C$Yow6n-3MgBbdbgYDs3lF+wA zCvvdm{5TVleP=tU;b7xB+(fBXaq!pqf%7a;s)qhVm+IiAZz)0bjw7fzj#HBO(cFtu z(IKzE438rPW@uhCb89;a%%tbd1}9Xl98SsO$fx@XY>Cu*rFLCLRKpx+@#9*AJIQun z1^h)AI^#38&Y-M%n!0|)tHMFZ3m&|hxXy>eskXx{iPqj)PRbYj_^yG=+0foTZd~T( zr9su(!s6hNpt>O@PEm6-r>64bATL@)5AurI@W|e4`LyE6^%b>A64pFJH7bp#PUgsc zM$@6CM!;~%E?|ze{J;P*bh7QhgUB^lQ1gUL=nUJNCkN0H84De?x>pq4m5G+o&d+_OQGM^!%1xG!O5~P znb8}7O5&UZqM{$bpHq4U`JB*I9&E;Ku(S|E*Z5!)cS-vG4Nmw=H|^(h5S+ z4D3)fc1EFT2E9-b(NgA^z>hM7E4CeG1C1*k1VAH7@PejL%#Pq_#5lutSdb_Z%Q!&~ z^5an{8AGFF>LCTNrZf;;Ev$XYV>P&2TAjo!VJ(B4smEpzz*A4yT828Ah1ycVSb#A{RXl_UA9lg(F!#-<5$#JsR)c#dk| ziH@N!^1*0QjLC6mqRV(YNB)fu#zKKnjTxpAoeGY#)A(@+!eJ(A9B}kr@^!dg1u%w+ zW$SpT)b{U%0BA!dKpzCS-oeE!z|qp$)K>6~>eHVPSEVK8sW~J(|77+_~vp;%bzw^dP7KRT!q= z_HcJXo9ziy+-wo#Q(65Eopa(%izJ~NIpInvdj?+5*@qtkyh>nrlycVa4DwY1lWA7c zK1n2uM{#7!eU;!vs}gJ{;xXen>-d3fW1*LAhX;Y_P0+1bl>k#P6W}2P*kL>HaAqC! zZ(IpNww)#}8;Mf|-nPTD#_}E8;e|x20MC=oZO;!iE;KZxqAQ5SQgbfUApeyL5D)yW ziNi06jB=t!G;qB=mtVPGJ-5Mw-|!3*8DMy}`rtPi?$F?bG2ax%orvtby>0lzzZm$# zzY(oqjz0VtgK)pw4u=8FTQO2H@Mku&{SU_g1|u311Mj82%^en5GC&kQ@hU(jh*mSl6a07&;hwe~-Up`Z zoy;e!O7Md1|8E3<^4-MnAp&f0GM{7_U@xDQmQ~NLMDhD80=n%?$Q%>=Svb66JA9F7 z4d8}zes6vZkk(}Ap`HjB7A*AAp(=rYVx#os=pSYkVf0Z^sm-%t1BT(++_{w%aYkkG zu_^plI`QKO zuPGaz=cE!Co{7FnU~;_{a`_G-VJzp!d`&sL$y9>yeMJ9a4sOb;-a)wgZHIS(>Ag;P zlc@yZhi!kf{qR=X;ok_b$q8>p!t$*p4y$)#07JQG)6YwI8BmpEGKEIBh zb0XK{GcAK=*i|yClJE91>OBDq5;t;-9lARlFh?`-k4+S*t2s5?#jM7hALAE8*Lz6e zo=GqE?_=e{JDSShJ;VXQT!qv$2 zW|ia%nfn2-xsRxi;|;(6~Aa^<8*-h z&5QQt$NpX#6n(shlHu7`P%<=68%+~ocaV(h~aMw{)e5+Kai}y*qvm93rl6zp-1+y zqPpk@IG__Zac3lo>-C(KDt;`KGBxxm9K===;h_yd!I&;e)OM zyBHSsl2h^UG9HG?zH3-qFL($uuOjK~X`(8O+e9T{EXOXsMiP1hzkZ0v8e^wtc&--k z4NqGXvH{;@66bqFRuM7dnr{5?tr$fvv%tTc=qBb^&W|++2f1n-E&-U2I+4o^_}ALr zIMySw)^^}S79VpW7cjpVG)30g-W$Pxv+Zy<_#by7tGTiaGV+&?DYQ=Pf*rfQ{n4v4 zV)JC(*%E z*M}x9hUs*qJr+{tiawM7y$niDrp632?fOD^NbdQVgsp2MZK z7@j+QwZ&vCh{8gzD2&@UGM_C;WP?>(?jpJs9GC9Hk1T}SXglD_)a0j}$OcneFsw5C z{lSl6m2o%}{7*ZPI~e_hY~DTeSyW(>W}<=(NaP{gAwN;TZ{w_RSA41JiVbbL;-U5l zdk`1a)CV}L8o<^=d^tLf|1z2|Tx^H+;<&9}zQrB#rK*GW=*!5%({sC2b2c5N(h#f9Fm>&@HW_cj%LxX45$3%B92Ty-5yAk0&u^spvk!?=ahaR3;STi#G z_k#Z`+hG&Zw}@(L`@omKF7n=@Z?E5HS~EtTuu5>$Fr)4#DPWo zzkGJQS&J=PmlE9xj>|jo1MMzrneD*s?s+F`vBC8;+j}JVPq!ULf&T?3tB!F^;I3B> zRkMDVb(S3;OiZ)RwjCxX+F0-6{BWzk{7xxYLvQiG<;JS-epOvNcgNhV^A_;k+a_#2 zun?;^uEalXQNHyme|v}dHq%$YsL)+^Fg$Mvs2+VqCm*OL-M6DGurkdKR}AEbZ}}+e zLJQQ3iSA|&7SvZfhHz_ahsOcZb|>pX11frQ!w;K?tSfDY9pHc2$vU4w{mYwRi_A^1 zO`%(FM-17Vb&c)tX`<-fgN$7{h9488gbjV1hc0gVvM#HY*6W(>SO^!+$4;bL4B-S? z9=c)KVNxZINQVcD=xV(CdtO|p$@t%dW7s%miX4=+76J~7ooK3mRJ=@R5WqQZ!LYR5ekAN$O9I4RL8z@6b$ z@9{%T$P8^JWKY66(@UjY1LhT#RdFLnO@M(#c5yG9gWua4eHHUb*2>09RTj4juuy1X z$iACkP=^#07UPH)Uo;|B5P`o&sq0@Lfus_aRzfM7h?wCVU(M6OtJQRH3%~MU?dsRP zYG!!UbkOj;>8oa@^e`RldDqxyw>r8mbU?y%&gGA_jfgQ;tIIOlE>JqIV4{@R%<;T+^A`Jbq zCn9hwiI*JH0n}91AbG|>+Z%DK5gM>XEf9UBYqeb*gMEPuX-Q=*@)B=FS`zUkCrVjt zvBLS9e144gATvDQG_VTW@EqZT%w*_sG@>mo<7|%1XId3`%s>`-f@mvqtmOwRX<0pD z9JTD=m+48s6jwj#Y?YrNub# z(Fz|p2!MoG+cfkh5r2XBH;J&YHW9sxn6c*KIjn7^QFCXr1eS!dW0osO8#v>on1YM?xIvayds*-5|A;B@Op^aLm54?M0T ze3dzRYmRLk#2m)i{z7-qEQZ^YVl~QeyW2>jr#O5wc_7wNwnJM{OUOeRaHFDhn}AP6 z2bfuY_Tr`Pt|3-OBN5%k6Y(Ozbp!Z;O#|H~*bbAVY!k3c*~Y?HQk`A_e6_#{^^9Zp z{yfJwlpmuSSOsn9LS_FR8t6J6#7rHVvVoT{Y(sfHpO4WP8QfAzFRFA2NLmg+7jUd9N|_;wxQqjpfGL?0)?S>qD)*U4z?466FM^9 za~*y}-8f7}TmBLOP{~5oV*QhWX{_--1_8de z9gahQubhm}kgk?Frfp!!6k{ALLEwHJZ>h*Tp^Ft)tQsRj?@}Qcnqe#rnGmPlNL=r8+-fxE(KojA!1CN~_)x&| z=o|MoU}5z~+$EjZRF?6Qa=0;q$Zs6)1B*wrd$Nb;%@D6}u=)I0g2-TrV;mA*J9w3Y zKg$ngeqiXgbk)X@r^+Uq$BTvUpLKe?S}kFBaa_Mit@h}f%=vSk+l{|SL3#8|ZF~hK z?vk$Ok+s?O9LVd;kLf~>1h&Zx>W4JkuA053I6%Auj2s}3HG(50X!ywww z1AR@vqy|I35R{g}IEf=isTy5qXqQ1I^fS@h%yBtC*q-he+kuZ<{MiYKp}QaxhM~LR zhb}Zswgc-ze{n*;GBVaY$!F;90b>+p;bc1!;2m~shlF>&zJpBM(v}|`q%;j3()eJr zj!v8TtetLMA=!PzR4B5{HExx$m;y zjN=VL8B>T@HE_#Te(Xdzv^nGO7E1hg2LVvxmf?-DAlD7Tly=5+JAx+>W0CEUu;S`{ zB0pK46Zw`0+i$U1K}^fMI6<0gRlw(f0lg{5RPSxDv!6 zC*xWqYfrZ7O*9BT_SYl?YK#n6TzC$*wN6xEeTaPAc04~+ff{}oPuo5BoYUn>E8BHW-J2i9+-VXJI)%P)?YU82SPY5e_d`N#T^}4xhyqs5t$K#BvMAiatcg zD)h4+LWbvdLCDb0`w%iII<>(GUF#(5;OSa!rMsMkut&j$tsO+-y6XkSIc*aTa*#>5f|) zxGW6~Yp!}^;etDXkV=Xlp>=yeNMhkR+8wW$ScU%9L&)%8u#KMI(BJzIGAX*L!3m$J z7}xKM$k+F_5ehFd2!)|w`hq#Q?X9mtI8TX@?SvN@gu+nY82|YQfb}!uun+)X#w>#(bvpz zEX z7;$8hakwj*AXMLQ4t~Mo&VUr9p<8LFFu9SG_)%K3hla$F+?mOb94}HukMQs@Je>s} zLyz*|<0WVVI`hzcB4I4z$WOEJanJIR&M35;=sV`Pl^>5H+$pxhV<_$v?65ZYgiy~- z04Tiq_*LWZBm%T^LMJ0(O}2(hN@JUi^2aKK82i7ep_F}yr-R|-GU8d%5~I;^3= zNWnGb^?`HFDSH4%qG6@cT{wYMM=SJn4;;f26>tpAQ*YF*DEctyLQIklfSDh9ba7b1 zkzZqjlX;41JeiPDKQafaZSQ&?;jqSU9AL5Rw095yZNZwacnc}n*4WHi*U1EeCK4zd zGJ&9R_#x5uz`Bo(QGSe+(lIm)z*WzJ^XtvJjvAlwqFtO7ow)N%iJ8|^HmWVahQ8Xv z!MM#891MMp4+n9VRAa?66U*`9a6d=>tq+H*EgUeA{uvy1r}Lv1!d+`S^ac)TPUh8& zgLQ9`wn&bH!u56(LBx53?Jzu16j&hLy@DSX3JQk4(nGxXGHpcwT zdz1Ll+)IO^kMxS%@ThY(3_ZzLRxt z_qOfuD=K|QC%gkagHn5iKd`(vwE+KzwgV2$cRD%YHyG0H22vc0Y*{UI=KZ8rd*RcN zdAbt*#ERQUF=mRK^bxBo=MX67Xz{-L~S|81s79f8EA7UVBps zyO0xlDT9yyc-@J|=H?oFiw9Pa&265RHuzR1aR@=?EXBAv%#j`8Yi}nS@H49^iI)jC zvwCMUR=qN7Y=`p!X2{7r(E~qok?jo~Smt8e0Xk1;#WKs7Uu=vsm)qXAfd3TR;a2cx zI+?S%vLs|y8l%h zQ_-CzE1ijmCXDeYNFmtG1j= zNzK7=KL@`5V1zr*cIXH+J7bh#YRhWd8(VTRFSH$cfIr*GJX48^-Ol~BRiPAq3w`x1Kt~1d4LP!fqkV+ z4c)=R6J5Ga(+uv>{{qi=HpX#rm2dXuG>FbQ$dH? zn2m9geCt{M_Dkm5Oh44l1J&@nAfS5mL+yQ_nsi@}vM45r{Gpy4S)C8mITomMDQSP^ zxP~8F5U#>@cmN>vaw2mKsOZTJ|BK+SwH;mpe{Ux;gF*c}HpWe%yU>mpTNNU8w!?dg zqT2=;Yv3tcgG@A&3~eTwjctsZMEHMVV;r|pOKNy>+Mvdiyn@%TnIGQey(-1RBa_o4 z!^1)m<)D-VR?c{G`YJ z+imZu;D6b6I05|q-4hKGvoW@i-_6E2^EEqeKJemo+hKm9Re(oc5A%fVVVRI68QM(9 zUiI4;n;M{PjM?f1HpbPkF|M|4jH``}u@VP+vN3Kf7+8pyAquu4xE9CNp2e{nnV(u^n)xwlmN{00@z$%vY@{gB2-lzM6TR9mh;W zdcEzSX75<^jP#S*FXpR}Ln$ep)4;R*N3k#+8DKlGtz9k$@F(Oi%vU3W?KqMUX|CX8V*LQZUUdc9zIKaLSnuNQ5Hy}>`q>Gc@%qhp0PZR%jy)fgN5DmrUs$2@b+DZ24mr%&P8yn!$3!EcP&zzVbL(1UOTLaANvm+ zc3KXPhXqZxCCz@66PA5HC54dZ$CvZtEI6PXjRS5Oa1Li%(#zL72R^Q~u2sQtMe|^q zSyeeVI44#oyBg#IdKhZTMVtD>YMfMEHxC=7JHzIlO&6T5eSmDW-RY2NRUe9EN-2Cs5t8QOw5SU=&jw7Za*gwrr*hm&~0f z0Y9dsYz}i6KV~7|C$_^J1RTpjRyAynHry)}QYu*Xca)UFK~CleC;fZdVI{&Xbh5vU zHeBlr2-V}+y8+J^8X|njW?j@7uxw8Ks%xA+ch#?2wW`4x&=pQ+%oZY}81LtmMeCFI zj;=~>9*rVka{Ky*Rmpu;IXNku>YNVt$FQW8lV&?ygdnSudw@GtxI5XNu$#>Z+74@? zQE)TEMzf>7DE!=(}`9igJDkdc0~foyZECf8^5R1Q@FUQT~I(B+5) z0^1ba6@VCRJ|j6vVVyI`_B{ja5XFZ5%4j1Pav+VmFakXIeF9Q92hzwmu+*LJrs;9!#K0&@M8t%;bx@f9EoeC9TfW+b5_|7Soa0@Sa6>u z+)%}s3_b8JQfE#=u7*>)&r zmD2@VGa8&O``QsWaM;gwz;!w(rDMR|T(}RgJzIjiz3tG7bI@g9H{ZwNeLo3xu+6kL zLUptqT1%+?y?jsi?hMD`9s`HpNUYoW))13q=xB0I6#sbhl31dHp5?-6X8C*p!K#5nYkl6n-}GRE(+*!JuTZpc={jaddbYuu80 z4DYp)%~Nfr{s?uN?Qp1s!b~_>`py22`%4OD=?DQaYrX?xur3$a4!NeJRJ-VVv1EL@ zWVv3RYbE1o8(r!p#_R0}qKNSZ+hLew{7Z0OCEO68=KI*s*X1_bVT5GidN<==A=C{L zYNO3G5~1$49Y#s08@-J0@@IU7L;)#jK72T$*lIhBwK5K%AC+9Ml>9y~&zB_EoTBF? zI;c8KbVne%S8NBUN?CZI%kHvW*fEGS>_>qeV|C+jv}E9Am2HPQBG@Yu?B6!mWCVja zHNlRNV6W&yttD8x&2=Jz9cVjX5DCtGyt10=FRSk)3Jg?DLSfq16$4e{u)vg+Y8?GKO4fHt zrVo|pAjvwqfv&JXKm@sV1dHJSfofu0rm}uI*!v0lFx&SeutTC6_LC(KxjO4-AlMKI zcDT*89Kj$`O|VlWSe}>l^L<%Q%9JRMwL@UI+!Z3#L~*8-^=qAeg`C%ZS(4)!@+^~l zbBbh^-F1!~`dma;ZabW>@_j$pXUo^CY~Ph&ueKdlNe1TVeBX^=qO$3_$mYW2r7Og$ zN%U$720cQu$iqV)@aKDyeECc}#2Q3#mhEtf$+xe0bUn}JnvGy9Y==wHJa{P8Z{_p&zV#QB48gl@u|r_K)Aa${0n-I8AQ}9ttUoMS zKTk5fO`Z^>5DT9pQQIU@P^6eN+=Cb~JvR=UCF@D)V1HWJp+_;kn7?#=!*-DQOV=0O ztS23aU@u9qcWo{#YIJ?ic0io~=XRa-0bzgEH%k;4e3~ymj3~ae9kyCo2jnu4?03K9 z_*Z%U!TD~+Df*S8>lUy>KMn`79iCG8J_77G*b=_YZQrNi(86|jhBMGDp!0ng2$EnJ zoti{%L$LjAhi4^Nl9%s^{(NK00YV&PhjK*^J04D1P__gm?2oFS?c%{ z)Skgy#KmFi5GF5fpx~k&ZcM?TBnI4W1YY<>DngfD7*w>Ch&=`kA}w}M(D8y=taa{J z{%KGvDoHSZH7CdjcDFTON5G+njo>S;X17~UTeF5ydmqS{o{)o2@et>!o^EyMV{^3u z+FG*1 z3DqCfh#%_6f;H=3aQfWl^tpX~)ERhc6z}+Z3Mw8u-U>C4FudgS*}fj@!VPQdS7lY# zRN>4J{uTyl{rFpD{5aF;^9Hw%B&W}t_(BwM?L=G`a$Gx|K5Qo^aee9Z`KpPyFb?a_ z(VWkZwN9V!-MD^mk=?Z?-AmQ_EhgDv5XK{47Cc5IXnbTqwrDd>^928{J9fmj?T{$mOJpB_t z{(!?-mcuh?UTi0FZ1!pr?xdKe(3@5stC(3c%b)A)d6bloIG;J09~c{DpJ+SW;zfL_ zL~I%Ea>R0rWz+GVLP-UPavQJqYzrY?%$#PswdFD1dRjv zf^wczNo{#iRkvUn2dSKo+c))5QPpK7oS!O5DU!yg9!RcS86%0|#gFP>wlYVr#>rEt zld+--eygit+mI7$KDkEgxH z&|Zf(mVhi>A9U+PPrkQvgqPr@+}v`Lr_f&G@WZR4UW*&YQQsmE2nQM>RYhghF|L=n z``R#)}9-p)j{9>P6q z8XED;o>3>avJwjv1K-9c;p_~8Dy!?fRY=efgz1h1bx-aF5$xu=yX1Nr4*setDp9#F zD5AaY#1CH^s$M^ip4ce&hbxa~z%y38K4<4Xqlk-WqVjnOuanfP42zOmNg37mPzB`MD zFuhQay^?#Hg6vvWfn~oveTBKf2h}O8pXu9FtQ8l36vnKDlLbTl|f3f!(ePY_MCCO#LYwV^UPhcL1a4AaJa@rkXkLN_BECnMuv3 z;fL2t)$7%JD4LzMT*oHrqQRjI-R5)A+>9`|1UI<{YMNKavS$>PmGh^iTy8I;=GWkd z58a_&w?r50UM`!IA17_Idc9}&a(PJk+_!tV{9Bhx@7>E~B$9*M*!EZ)+h$Yq2k^t^ zpH;6I)0okhzsU`0vyh7e`Uh20p!Dxn$HnoEuQ+%F)$dTJ-vA8P2JMLA9SBB}bxP+* ze^xkRVHuDzFrwd*YR+;(`jMiFI^E5AgN+`+;Fub8aUx;ezM)hOE2@Qb!5FiyvbKsl zjhR(NbLA`?C-;lF)WX3JS^TnsT8yO@T(P|YCerwEbiLDWxYG~nQ5pXA>*n<9F2ldo zjYgA0Xdbm#KrJq8aE2tQ*UJoC!W_o%3TO`5TX|oB*VgJ46-^6HALjwe`&w|eSFhI_ zP6X*7iN$cC--P=0^+PI4Fskmcps1>1T4lww@-oPdqVj3;ifZt}B6~>36RE|G)Z!Mr zc2ci6KZxt(kdPwRIsJ~|RuvhcG1+1|l%R;8Qa)9^0*F-To3DcM+M^ejk{U8s{ zW{_t%{bCyA2c3QoH4XC6`P6a+wY(XT4O6e^hnj?Ltn$7Koa5B1)p~s(PgdTW!Fh~& z-D2YOf&5-VAWvIBEgz(oTM^%M_4_5@|+LTdRQe#qIpMbv5zwZe?UZm)xJr@hnf zC#T;o7s{Ngu$sL4bZyAVOQ_X3)aoY0v|PR3Zk2h|$yt|BQJ=MxTHQgd8053n>kDpC zpQp$TSW}jwwukN6yO%ZwyzaQ&6KELNRtBrfX7YiZVwudXMMg+mOa=khgm7-r93H?{ zRO6CbhDh~n5&-*O`B>eu3XIEn@DD6&DmfC4(UpjEV^tX5qge)LVom_D5v;)& zF!zv%1X*G$_3_gD{=o2S`$y!aW$`+UNKQy z<4)zX#{=4`7>;x-Mqdiaz+08Y-@5Q||Bj!HH5fm2?LS;}-K&?|Y7m|z>WZW#!8Y*YhVC+%`ofJkL%vOQ6gmDr! z>v9|{=&GyHP@o(sjm75i)T&m^z0^n~h`L+Vxmrs&rJNY56drwh^y(>skT0C(+A^b- zl`Lh908c(pr(8TMkm&ib?wm9Js#3AA0Os=jJusQ}-GCq7{|FS)e(Pz!hZ>ddE-v4; zPX9K#d|NvGTkS6K^7ai(rTreJ{a$Zy^7eDzF)g+vUjKH9NW8rEffH!IcW6JH?Ua|Q z-uDkEiI)({KZ_HnTlZOI|7w#2kUR9YCNvWBRrf(ysh>7Xa6u7i}A zt2&hbcck2;y6S1F4{Rjo^0ETcX#XVqP^O&&CDbN~+CX1ok7sg&40Knge-{n(xlaG{ z(2#Po(U8vN!ah=qkK>vwX(?q(%r!BlfQFXG?mVXE0-uH2TO30xQB6t7y1YSw8Puj9 zen{-#z)WhhgxXx#D6xGxv6njiFVTs;$?3n26Pt^~-o%NG>BP>6lUQ{Yd1=}FGEsQ& zumQ(?6`{eR;aloGmI0ht2np6GLP&s9kBL~(xhPguDeWn5d|)=US&tu5J|QrN+U%mX zP)GTSc{Hc|Zm0i7o$_L*e+j4j2&BB2Q|_r{PJmhl=Fuf(5G*|J;i5Ab`)5eOF^5dx z#LTONP+>6(nOelj#^kAcF+}Yg9w9N4t1VP1E)G;s+y3|=#U+7CYP*QqVlL@RF|34~ z{*_LDSY^n>w10`yzf>eZwq0Wd1aj`f(?0~H1<7wS@U4xqIB(BxyxB{52^fzE@) zX9aikyc)vd2tx*hR7#6# zaL~6~k|-D+*h^|+RTvjy1SO%z#%9!X$85h6LXihHuAr{OI!$#f7F?V$f%Q_jnGy3! z3|>(=86XT%eREPJ`#uURqIRwDL#6nb0w>b}=g%>hc+Bq_7z;gP-gm5bR4V|z zqE3GAz&LjOMX4i)1ft3Lf$`8#=H7#vlw1JWRDe3=RsK+}n7HOAQ{WUj;0^p5uzAZR z+N1tYFqJ#MwPyMZO#5i!3ttP!Z>QbA0n-7R_^weK$UjK?>;l`tn)r1Otso}?0HpqK zL+I@3>1GGV$7af4n5+5X47GgLBO47P2dhbtaKZl)PP~qg--80DQu|i;fjEQ$r&Id{ z)V^*HKvf5h03`W?{Xi`W9LcUjU7$uYP!ky_NP;GS$`AwQ{IL``liDxF4__ariJPN= zNfu5=Y4`KMbhIYU_v180yRQb*R83se7^hP0b1B$jnz&+*IF(~60mTh^XyCL$_f{pr zNzx`fd|;6BzX8yE3Y6<`~p ziK;zd)LpkE1CyTUVSJXtgP~a}=SV|qSr6t)|q8KsPGwMWl1WH-VL78IBd86+KV(faeEBw~8 z@SDK{jLl67zc6O-BKS5^;BM-88GiWw-I~}C4a~Fz-xlq@7EBLl0@f(D;CocNuLIL# znz)6Tle*mC@bPC*0ohIXld>u%E2dL9l>h#VY0GbvkN5L0#_5(B{ zFqd6>D1h?&GC&pV(zhvqLPKPTUNC?H4^gN0@Wa;!xL8!ywBQKs^C#GjbcrCOMcipr7`jt#Tse9jg9ql#mEyFq=G4D4+ifJ?4LoeJ3c(4RNS3@>?TO}E4rkG+%KE!v@%-6R zpr`_NVDq8qX0@%d$`%E%%7^rDwHVO&HM3r(l)Z_uIb($|r=Y038WIH~g%a*+wQ?Al z@e1ufxDh>eKzd!rIJp@~q-4h1Ju;28>~ z1(%P86)t?ob33T%ZZGUw;$2RQn77+hv-_-9r<~ zQi@k;MGtEUSRPmFnvhoS@8fhc1-4OWG=50;Efjc;LibV#J$zi8z6#VZBKP`n`Y}+; zt`E96J<2%EXPg%Kal#@~}guZcJ8gjuUi zVJNY=Z!36>0^2FH13wVxXN3qiiw3kov|cVMcu#YF3eNX6@ufk`UR)~pR5N@F?$0#w zqv2kkypI%FeRhNwq&Pj0k6qfjc|BA{lkWZycbZgLA;W=!Un%f1;S#uTGUEPC6G1zx zQmo#FgrU&@n@8tA=$c1IaiU1?Kpi_h%EgU^^W?tCeN5LM%F5!>8QPWtuTnUKABYr9 zpyyx2%>v^;T{=S#(w=?6d9Wr1nEW;l&{^~3B0#n#kQ&{G_@eKr8HR(qmnKFVZe5(~ zlhf2{U3NsYb`_;ktjFmF^Np`uJ44WS?hzc}8S?PRP3^*|!2)}?U^y=>)l_zeQQ)ka zK_Xl+AB7;y%Hs7tOagg54}rY3Ti7vFRl^{WyAbpNutxJH!!sb`V`}Eh0-l5MVwMSt zjZhe5%4l*Te=yFX*57WmLx)n}H40D055+f(0y`-4Fv=XehZ=KcU@@vk)UhfO*0qM7 zA6UZ9t#w735=|ZvSjtXqxgw1MdZUs@S`}%@5~)bjDex9$j>iuPDAL5q(ZI6C^pzv z^p(FJRaX78YP4j@->*hcX8xb4Md;ezCLE-nxg2GOuI+t_R8z#iWx+^!OcaN{5;%$L z#-v8IXeSm{+5LE3jj(%V1O=9}+jM_Dg8a{_a0~qqmjA&19qwV4uoVH)&O^s@slxx8Z?GcP{*Z^nVJlKA+B9_I8%q?X*fxBvth5X_e zD`a3w;chqKcv%kxtqg{4-VP$YcTb{GCSJX)a-S)ty)80puooz*@z#?=0ys8Mp+kAmR~QRy6?O@qE6neSdn$|pfkm5bUhwU z9^Y`M%sZUC=Npy$dldMBvM!^n+YmdtQ$^fmm3)qr{Kzq5M{v=1ZJ~>PCKo+BH!geL zkfG=2O%fDn$qe~msOcSGaD}b?M#;XFz(FL$l>K>dM7l5@F zC2swbLNImk@7BLK1vLyKh3~2JWc-jDj1+cJ=TE5fr%e^qFDM;o5zd6s1Q!(BlIHDl z@_1Let}LJVE6cDj1%9T^pHp@cV$ak>3#+WUN@W>0VffK*bvaCz7SzwvrYVoc<>eY; z?N)E30sj5kGOP~;exd9%{E$p6cl}P;r%?83O%y_Y%czqNZOGY9ei8~He=iim|Hs^S zfJb#J|9ZA0A%yf^mu>?#U?2(IV1s+N0khamfR$sx z#ven(z-0|uR*F#o-BF=76R;3o|h7bfmd zrPu<_ZfnIP_0^*Um&3ixZPHzN?_CMmm3sbn2yrApujdOui@Tg+$qV=S<@h6VW} zbiT7zXqGcDC|HAmdW)^cAb+tb3Hxx}B}V%-r=mn1GXNVN+r%h^Qtw3q&`Y!#jT%g& zhQ$lzNbS7DxIJ?wrC>RKI1lC~mxG#euwd?=sa#ejHxs#V6P@axnP%ZmKrU9)PV>(k z&9Ys>vR#5W8B4ZT$8_+sh_;|nBWTnNH1cc#a$Ip*m##;H>XPiL{L&I7O0w;Iz)@;M zFpq3uVlLRdTO#Ac1I~A3wMB3Q0LDdUDMT@p*Gmw4*NXKfjKx|}V9^)Bb*;Rw4C}56 z%^5YvV}r9I_Z36~Xw-Zpe94vA?L(uUp;7P0liNS@To4ET_A~r5Ph&cr#dJE$Kl4n7 zP8&vP8>4h?y*kk~8<)IpO`|?ULgBX>VDxTTSS5G;6xnwR79u&b?-Ag?Fs$M=%A-;U z0rxQhHn#|GJhR!)%0on4W#i6F)exMihJWjQ1NAXGzFq7tZ;YnVKZ`2cR3(__Gj4iv{Q)vZU83syjv&`@VEBW?4JYupeznsRH`3 zrp$)1jaX8ulufawvfm}zhDPs>1oFK{v?Gl{!XkvC7=DnVjOUyYlyWY7B-vl8e5ZH% zrc%mzY$;!A=a0|wVUl+~ur=2w4KNNsE&n2{vN7C)3b5 zIM{0!8dHP>ilh_mLFv0t`tJRR#sQRaAy}O=*%pCuSi_-|iy#`a^6h*r8tWJz)@8hC zK*{hJ>_|o-(O#6kClZ=dBtRo1<6=uPD&+zEoHP5a5c)Iaq*l7u&U5L}ZT^tZKY+i~#eM z$Rg)B$=P4^<@LTP;)1dapD{NW;bp_;3^9B*rU(?OODy2{A}7%Ql+Sm{GVG(Ip-4XP3aLN zF!ns6;gs<^W&GJsU;H;hXSi=&VfQ)o#X2mjvzl(=WA|s(<0<~TTmQE~|A*Zbmf3`U zihg|=mvtZN>w+A1`QUcqjTWg#80ncR8!c2I3@k@0svXu|&J#ov&w&sj>Fs!2muvX9*eO=n{ zPWVsN6$hAIr0*&t#8p_k=VNOk>HLs)Te9y(h&2TvNrBZk$c%rQ)o>75iSRwhHHTop z9gO9&ExFSKn{nDhAa!M08ZUbFv*fiYI}NrBICkT>@f?6Q2LtdZ8oLk)fQKl9#%)gH z2H0#Sw2h}|H*l` zq38n8vA~D1LX3nV%m6fCIMFy7HxLQH2mx^WTFO;XoSp+g(};Tmahw1F6k|9&XOd(N z1IE4r-~?iq(~jWGnIX?d19_$Z=~i*DRCI;ofdQ&%V1iW~w?9uF?4=d)2y+PrONi`P z8gOY~R$|F$4rFCPGVo)<*5V`sg0W?cWc25+|GyKBc|_xB+)N~V*?gi&H10zh_fbEh zaUP{y%`)(ek^$%+@cU0od{|Ddq?Bt|LY5oRz;WP3lyWVyvSHHuFlY0X_;|(!<&!qW z^eVLgm#<@9v9yl0b4;FE!pajn2Se$8H0~25wDS-HjNi;|Cu<%qFJF4;p#f8x-e?rW zM#c<80;)3rYXc3uiMkhoxY}}>g%~Gm3nquAb|W+jVE}x*Tt^^tRb6xeX4^^Ck_dKF zcc`@%K0}0~@c4K(1l#ng1+_UR5lyD?TOgt7ClgJj@ylrZNwG~gJJp7)O;^1H)70rS z{uCsi7CE0mP7p7UNs z@AkznQLY`WxbOl|HsM0_%q-M}aZCeC!G#-QxPTE$Kdb;Iu9nt7wM$r=3mC)n^BN#y z4Aa0O7un%L+Hgo{dpF`#m=76S3m;B4d59mfaG`5X9vr3D#fCS4!7ZDCI_QA$ySFOwN{yGdFSG4hcCk41qXd=FQx# ziSlWJ2MNG70;GXAH%Iek?ymB1dtmM+z)mi?E#Ax>EYIO)ojXK;JzZpnH&_HlTTB

MhC|08>QxE5*5&dQAj9yf&iF!B$eD=L=-YDuokTb*_=6wKDTmS zNn-kNAhDuPK2Z@($VEbJ1p>5#KDWit2eU1W39r&z%(gUu^)pclHhmV!^Ex2c3J`LU zE&8aSX01Xp4mY9;`f#>OpLB;lZA8U1p#up;w+nD=KlHf~;fhR)!-PHuEBf5dd2GSO z_w2!{W6wRDsFWrgkA$j@5a13F=Z+ZSoG1@3048*~er=umy)pRE)f(k8;KSh8z!et0 ztGnkyckAa@0~xwo1J}98LQE&}VB~P_@`k2Qh&rg3p)TMk1T|s#yG%;%Z#NT_(S$pZ z0KivRK@<0)iTm`!onH{R$eeiG(#J3la#JYfF3x{Wxc0PKp}m{)USY1~Lh_*C0T*AiSLkVjXco61(EWk7i-{RWW z@*JbW+;0TPc99cst*fWOaBb{v!nH<+Yk0~BTkE^Pj4nplRk!Jq3T znokpNqlx{*RpnwW=w7fR2bb&EVc5Cwyl>!quw5ynIeRMB-N$*u6SHmXVP5}*O>J4>Lwaxn?e&tC^J zCIK3F%SBGWy0#v850o7=wpmygaaf0^-7U@}aHHJYBy*h!S4OmuCVq+ppqywCO{$uL_L@ZD~gd%QgF0rCj~taOnR@Qx2#F}%CQ z@Qz(%=R53^(^wSa^3Ci+G6S7_9+uu!fo&?SfdhIvy44|6SR3H^gBxw%-GP%SfvS#X zVclEICjeli3*%f*-d>|N5~&0F&BmU-zzhVtBFJlHU@UKILckXLmzveSU98BV-Msye z%X0U>V2#Mx=)~A@t>WEK*x-R(P1q8{ZQ#j>+7A^>O%JTZiTpVBe>yf&jST?q!wm$1 zba)^*TR9>AzK!(U@GQL{CdV9kQ{T{6&jey(aO)EsZ8J`t4V`--Q9VsM0tvjnh^U$N z8%FAGAumg6{DMaA`;_tsOEONmiPBhzns}7+?-Z&3my-I&I1iq%1cS{`O!<`DW2VtU z`=uhG5twOcU;*U*@ff*(SRP{8A@>mh;FL-t_gLZ5g~3IYi&0GjmJ8alxN={Y=lMW> zLx3W;@C0&?PcU*n&TGm2agN+O2M<9^^0CmR1&|{KnL#=VTrb%&A9*QkB~OJ}P`lvn z>Ow5Lme(d6+t$&mVv0I>R)_x4rD7TJ!gP_Wz$i%FXh@wY0xQs5Y%tW&1=&-XX?*zv z!;nd35;B5n8HzFe#JnxXeZ-2Dp4pV(1PMqNLZsX#b1`I~~wt0KW^WS}# z%JI?vJE9%D2Ocvov~sEZnve885=e&v(NgITeHCZ{0bL&gyG(&TA0d3ir{Urs5{FfC^Z zeQ}l5SW0=8^RVz0e`2_Q;(0bT;7;tL$(=O$VE@F66gm78*9je3gbu@1;HNVLI2RbJ zGknZ|pueDk=s=o$I1;`96F3cE=3vbwwIocuHOoKoCQ5nUKk<4*0!+LqYdwDa6K`}} zv;K+K*-Z@-t)|KAY4Sac#GK=o@Q+z`RCH7I#x;yq{WNts(Hfe3KN6aHfB>H-YU*QX z-@}MG_fNc^oBA*}^oBsm(vtXcU@{*nhM^yd=CQbx!1g4Oo`U5eqvmeHlQOfIJ#@xX%jGK>;f6h-ejLRLa822XUWh7+Wu-28D zbNOjR$J5kVNN5FSej4Zm=iZ9uL_Yjw`e8LNCkn8@C2kBpW_lWb5%4k7(?Gq2?{Y3b zSDuG~j0GNz+~gw1ac<;re1foUxv*|o9P4oCYHJT4x{C0wzn_UUL?_VHE+n*jA<;=R z^W4@GFa^}W zuVCW4F-*bAjehtwFb@^rJD1MZIFx^^JpU<~0Wn?<9-kUVcWv&OO-=bw(x=kY-;hx6 zIR@Z+Tas$2x3B|&za1m0vZr!!!xF~(_c`xorbpZjAwyfc)P<1w*Atyi)Am9_W$Ohf z201>6A;<0V5V}794goA(AA|p(pzH_yhXk0Cn0!ykb3{GnKP>?47a64z$TU7dWco*u z>ASF5Jb(uQgo}19X=zf2HNg5ZF(25&q$Zqr%1dfm#;erSG|6uDV4E_$Io=U}&fo(^ z-E}$r{@=FX$>RBMqBCe(2@-&Jh|Z?zgJ?R8;$+M(7)B`{GNXTp?j!}HDdj($|GNmq zFRGJ#guGl&!cGFAP(xJye~Hee>DwWp5q}6U3qtX6G?NQ9mxseP_zSiWV5G~p82s%8 z1?$=cI|u;9D}1*4Q~~1SbTi-=E!a~4%P*QxC`8d^<`|)1AIf%GE)e6ING{Z#wnTz~ zsTfiSds(zqqC{$nnss7E$?L8#*D;O65z^wslLeOqjvi^S( zwt{q`^Jw~PBoH`*XdTU%M>8-?B^9<#O8JBZ2=SD*3c9d5j9^ z!8y4~;{Lx9u2n>r(v0JfK+x4hSJ2FpXyz&X2-gPeePV$*B}TX&!PXjN1I`af*wBx$Jww$sj;JnPZ`rrRF1Gp-FKoIWYXkZGsUBrwz%^__7saM8Uo3!wS++zEQq+LWOLM!O=$Mcy4%6wJR*r9cCw)4rjpXi#Z=#HQRgRz_<)}xVVrY>=t-8)VckF zlWrsFkVJJ@QtC){*Ws8eMb(jM{Jts_rAeV^I3yUeWNEdq0JO)YgJ@s~=c=;546g2G zby`IX&p4Xh+^c|Z;_FiI{m{-+R9zh8!ADl8#yg+megJw@P<>pWA;gy$x`JZO+qvO^ z)Zpk0_J*gc-%;v!Y({OG-je7X55+Ytu8>h%LC1=r)=?2?@YI1>nHsuZ_+et|-H}H_Btg1Q*;SK(VXX zc*u3p?-Y!3px-6HJQrQ`AOa4-e^m`TTQZ$n&JO--VK*6Z@gC`%r8U|AZQxD8lSKcb z*%2gs2CU0FX!gf6J9-zMJA`4XU$`CiG(w}~VFICy=set@6nosedi{CY~Lm|0Z^DhcQu}Zv0IlEXTVkdrzbd{z6!e8z}n*%D%~#d}|nB z1|cf%du9d#HWh>NcUKJhf%EQ8$e<@|(0y03}jbLi7M-e}M#`l;|PKnMXPOSc-+GVdpDz<`0XD@SGK% zODR7iKi@B0#L*BEPoew+Y@x#$VFh`DOK zro>llG9%9?dX#cbMMAqTAbOl~{-8N2{dBu`Ddjh2PEiaaKctxv zF(XGQby*1K!ILz{gM>CV9QV7q3lg0;FM!YCX@P9$MuYb+!Gm!mBTKP7sK=1f6C(?276hUWZ} z=3Jeemql<2{mJ|}H=374h(t-@{EH1Q3w+E=BF=+*Jb^oV$XLb8B53aCXwJ1r8~jBB z1o$9}$P>$%B24}@F81FRVe+qm2VGLfy|I@dJ&HG=#q}GOlRBzX7L5>$=YT#^04usC zL8pWX?eelzcp0Z!#nRU1$=|42i}ojap5}argho#$dXeUq&|FNKT@%pa76!tiHAG(K z%*R$fRBI6ylYE^2m2j~_ana9tKP2YjC>8Kjgvs>FG`9i?ZJ1B=3e7!>=B@`9H;dy5 zX4M+E5xAIDYoMhcE-n)!%-f5g#q}GV)*E(@Eb11F6+rJ1V3ms=$Hj5#R*U60(yg;z zF>~Ee0I*8ejqGV}=vWzP#28itrLMp0d;o_DaA}shEwJcF$v6j3j}qWARY-dW4kPLa zb0H_llPdw7D8TimkW(b%avUNFqj=)YB2aa>8b@E&&Np*N2xuP(u*4Js6|JAv`Npz9Od4baA|p_Vt73Q--qE4&*DQjm|2E|=MM6n1^);|2 zIsb~M5)EXYVE=^TQ{jLtUp_Y4bKW(~r$X?l5WAb!$-XAs7{8onki~MVJ1&E<>>iO_E;At&3(-ak><6 zJ4(wCV1uS_@p#F&6;Cq-xG#oD#n7?(Yaap{bgTxRG=)r)jQb6f>K!JzowiklG8E?# zy-T@IBcUYFS_AL)!z5^ot(hS|3zLG1N!xJVABmX+ce7$rJ<T=*~bi$A$kk7iP*U|^A{xJ!yoanWO#geD1-xOFj1I!FqD%~gD`0K*J@ zp=(uZ@^;5l3{n~x9?K+{)cOe`4~k(@Yhauy1iDsdj4(`+UBnY{D7d~|3JudP8_lY7 zi9VpbOeB{36PSulb%1|n69p)@tn>Y_W$(j%d2lwp@? zVGP5bllGm25}y~~OhfCJBm)}`ieDDstXPIYW$KSS4`^=*aEU489mzObGi+ap?VA{w z&A0W9AIHloHp4zA`k3-ALqd692!N@5vH`3F-G4`B4wQ>lfPX56?ZkPPB#w z9J;|@;wAc&^6o_f;3N7BTXYCc1suc>%dirtOO5+1aG@?WkZg`$va?`dj$Z=xsnHY6 z@z-gFsYV%wjS{7ZW=3cI=@Z7=g3%@3=HfCoy9Jja}1b3sg z_N9lyIBSO8wmL#nAMq`ht(p4}_;eZgb+O5q{jb`_j&m86%pm%l^7lYO%V!dOMfvAZ z{ssNW2Q<$vEDK*6`6wz^^06!DeV|{8mjvKU zT!~|BQgKzCx(N{Zy6dNDZ~R{n92^gdWdKBDZ<5fQO!OV)|AvImIfdv)Dma-6PVGl% zp#64-fD}PKlu{|WR0+)1IOFULv>#tq$y*Mate0PmVYFmC9luNX=BMKs9}+>ePhGu#9nm?g_2ywZ+~ZbOYN zp>};6LkVUlzfi&ZNGSe&0~BtVoO7knfO|2Qz+KI`9~9^I<~%GOCbEao4mBA3Li8II zZiR%(eidLLIJZwM=SnefXk6%_QVbj#2)L|>;#}!gf`J%`QVb*-JS0AulB&cl*TBEDfEkNH+wNc0E6 zUt4%6fFc2&1>c6m@eK-H(+b561EhI$ak6e^_a+0MD30pwso!hYa5?5WWo!RE64` zu{XQ_E?0Ua(VtZK91_YuN`PPbVI5S(P_U_ZUt!%jigm*{Z(2gu4GS4^EFx(2SD}g1i_%Mps7x#0Fi%SG8X(mEK^W!nm1jOnr+Bx4&q-BAGCI~XMwWxLChy@9re0K>I# zmF+DVduX}Xf0p#>gOptSKaz^{$4N%Ww62&XtwDhA3{xYL@d=(b z3GjWaWVFhYpMlmUz@Mg&<&yD(k&M$sG76MrpjAretJUDY)b*1vc{Ol-)-(1`I73W4eFINs7tooR^u9$-|k5ncV-&P9x8@R8oNi;B@kAM%t-z z&ibI9(yPxgs>6I+jPAHszU%^&yg`7=409il3|Jp!4+?O3tb{x+Pq3S$>WKNgT+Dz#D-11RoF=3sM}->pad_5B-l59_PZt7Oar zgekdF3IWky?8{acyI~gJ7{T?Q*yYBdS`q9+4mI-SI{X&H+7F;7`F~X^9mQkR&gR0<|0a}|~EgOlJ``tt8ruI0nz^BzF)!v%O; zOImrVWNg6GGy$H75!dpu^5hwyjT7KyQ^*9#cv6e&A#;N<1!@<1F!cYC5a}D-n*ky*ncwNG}y}Xt@`%wArNC4`{6QJ@cDsMxN**C7oGz%_{ASz!Xz*twHqvapN zp)Ps?&<_w`e-~Zk-z*Puo5Z$L?TZn340O76H7IYb0E>;R9wHg@@bpjtLa_pWv^+r^ zV)-!ww3HhBh9c{>tnI!AzY{qPqq z`~ASP(mdfKwhdw0y+7xbBpjrN!PwM%yq-Kmsr(Wo)V7{H!>IgCD*pj|oE*o;+XWZO zy8I3S5XP5SkKHdAcLE*5psr_wiyp&AZjFPNOpoCrw@J9D+852miow!4tbtVw5ujZ& zpaSEOZaacfDnpU=2LtvL>37n4V}1c!MjTlQr5NsAc`7KA;^Wz(B)LsAc_>3_~v$hF)Ydlr3Jgd6T>= z%JvQNmI%Htp{e$N=3wDB8B|)<|FDHovDUFGdx#Dv2Or*-2kO2IHJd>#M2ddf{5;Qwbf}s61?t{RE_Se8; zu1G{n(7y!ZDWGFC(CE**=&=&Sjf%2Ju^$5}D@KAIGL5YK6~#U*Ed~kL(x`xgO?^V; zPXI7Y(%*xlNTL*b1qKBDWHX>WCxBT~t-yewpL&f1{Uj1}NUQ`Uk{>n`^>hbI8|;(g z1CEqM%I9QusvSi@z+p{%=6CWbQBoOshdldI)iy|I{k!CuN>!&()fvfUq!Ql#Y?gn8L7nBqHz%^SBbGj z1J}AtkCKtfEd>J#tP*35M!(fXkChQ?z%W`S!LU(@d5~@-hWE-{1^7_QNF|(Y`so{Z zx~BmDiII^?3^y7L$C_0R72q3F2!&NQgxU(olS|caQ1$l^q`Wvm!qBF1Su!xRX~2?< zXhB*e7z_aDehVVt~RAk(-kTNubRfEY=!Jfr31I>ERK=or{EIt(>Ik5N3T zQAS`)3u7eaPHErsDDf@IL7 zd?6BZj**y#h}yN9RASU;#EOh_m{YXW*hl&)A^9JR&CBE|p?M!6;j3ODPdUwBMDveG zE;dzr5EZeA94TV+i4vP)&O1J#*ree+F3lgd11i5DPbJMi3JJiM0{jc2QxYdS7~eE5 zLc}XEzG(ovB19IVM5ii6FfQNVuflkz(XVpR9nrxSu7)lZnhrkur=<$FGSyjPy0x*) zNN}teIw|{dsiaswxa68W`x3CGHK(k2Dg@n5r29 z>}b7V`{b+U3dXKL&lO-V7hUM?_~a+3pgQ>?(|gmSGF1n3w+mEZq|qPQhDxv?q=9bT zi>nq$27BUv`@}v)Fiv>8?6cUz<724l9?MRV}Px!8RP5x+qXGkky+~LF# zb1@TCg^lpJjlv&pdP5<$W+R&}WWFxQYs{ySE*F$L4#g~-<`IOH_&u#w8UB?FNvRrd(+NUUgMO-jE9 zw?Gx9Vj6hf6!NHKJZePyGZF1uagdIX9Ip3Qk*Tg>dm5xnV!Km%L4A201G*_Lqb7#=v&+AdrC|t90?VT^uT!;msKGaa|UF zYV2^RE=4r!DXh&}nh;>jcN1wf#}+T%!cvM}X=H;o5SY&=N8nH9y>nJ9zhaf3bQo*O zs3L;xSd4-4!@In+DHadEtBypCF1x*>J>4n4PrcC?!TJq^s-chH2{x&Nj3Jhpfl;FZ zC|oTejmwzCN6GT(t{gzE#H<=CZB4ZBNhHv8IC+**@L~!+-H({H;M{E%ofow@jnoD_ zuHKqO6yyhQDETw_xLzv{XLEBtT>lAfKN{ZJXk@KAn>=k4d=3e1$stcWEgC|LY9VX2 zv9eZOEVzipsV)%!Q$ZtZ(PnZr##CMOXF#7Pz_(g~RAWrlPZ1$ey-xOx6;&}_U=$~v)Tn%y-ZO41b(Xl7Hw{7#Ym(}`!AkiBvQblEl{hi zn5%o`$<{!_>`kNXU{`AGJgkOeQe*54^n(T1%hY+8WFS_p`fvgEMqz-DG;k1J((0q+ z;XYs+KRrgCzNfmF*-fChXKbAPm5pQN)Eg5gMx9rmCcLdixu*+YHp5k8sMDOU@KxbW z|MWYgyADIxH%kj-7(y-90nRISMO{lZhPw`0RELBLE)(FWex&+iqB;m^C9X@hwh60~jgs{&ZsR_RU`A09j18q7Vb-xI)^d&X-|J;L+% zxXN?Jmcoq!HMlnQr#qX>-3@R$vIt{pNEmAhiZ310)UZ51GB-o zh~b=33G?=pha-TwmjG74byR1b2Mw#sN(cG~0WzJ=3?2;9-D|YwTn7}pItFz{vCw^R zpfc13d%P>KYH($DV{1!8hH80zM-!j_yhe3_dHa%Q1=VIFp{D%=Xz7QXtB9JIIz>j* ztMb*ft(o&aXNtugN;Af;mqmUa)bdKIU4{ezYFPspfpAM=2sd9I9tKRza5N@n-j1rK`{hO+KvY_fhRS zB-Ga_z?1!u?^dD~CKa@dnhsPQuE@6(c~v75k}tKpv!@+*Bt{hJuzJ6WYM(|zjZn54 z_yeR{7OO4hohpyt11_|w#{I~p21}iYDEwLaImW(u@Mme@OBdN99ptB@N%sS2-Wd-F z=@Q5sP+8&>vXMDV8&*^8pGc_bS_9M#?}upL5VbOa775YrRYYrJLOz<1Xk+Yp72zHr z&swS*iG*4o6d(w~wZ{?eDS12-xK9g!^(qk~n{aR->4Nis40Wr4LKitX;r}TZ&ZFuE-x;dPP(YPqH zB-Dga6UWAN!Em*YPS?9&;4AYSM0Jah@WCIG=MbuUpXvuB=imG>L>P^NBPgWkyB0G!!%vz5hf5lv9nhhUl!6$D{GLZWjjqPkqZ=}n>L0#M^Swh5}KASKwE;Qm95P3m%*s$_Lm)irj_-e zX=OeBGU$D?m)>7?bad0;#5#uRJE*?TU#6S@9)H;h(zK9i8b`7n5SZm0aTgrJ@k1?TMXi_s_WVRAI9y)Rbm z-6GYzTlsu2s`2ZNTstlQ)ZEuU}V3dzU^oa5^UD!D;G8{W-%- zhGt9`0}|6ET+xVo8Pz0d8W5aHp`RmqHgDqQIs*-ee>1_QEuBs~v7t-?;sO{3=VO)W zSgJn=2|yuvPNKyR(&8Ty@%~aUd>zpWf7$uW`*qCwb^fx8T;7+jispTgJg3m&pD47s zzx*IAmgNTv?++5iGf`=eR!}m6m6_$zeRQ0kUe8hAfyggVfRCfpGs5{x$a5-%1|gyC zEdtC<(Dw2(v;5_!5v}x>V<5(#XnXl-{_<0;ws%Ljy^lPnQz(x@3;g9PP22mV?amgW z0v-O_21RB!eheIaGWF%ZSadsq)N&xEzRrCZ-Em)pdCeIVszbsTVP2yFtPWe2rB)L7 z4tV-;X@tN0X#S$(`HPPCmmlYTQNbf-9Jc z3MO*}A4mn`110J_&j2jAzJRlf8(L^gV2RQUjXhxqf_o||*M|ZB0%|yw8Zhgbj{#o; z@5I$N8}%uceP`<1PpU)DW=)5IHJ$(GLf<6Mh1BpaHNX!r|1ATAcZw^t6NN6vM`U^A zBhsu=oj!@8^{MRE@TThdj64@ncxMV{pq|eKfUOimtX|a9!}V+@^^5~I+#^t@L@D-! zTAe@ZSMsc*a4m&<0Q@EZmYA&SvSu-rvYZnimngw*;&c4Nt)Z?i9lsni(wMVV$MBrR ziPslz70ZV+kx^x|H1!#?GSCDASsh`-^jNStc`l~#)kpx~JG_L#pHpLWSaB93Zb_c= zs39B4Uj@~qtct3Wold+VBf1{-4yJjRQRD7NC}2nOTuzNu)OZHW$irgI$OV|_Y1~P` z-CF>xEW3^%%O|q{vp$VJ9q5?#X&^`YWEP}J##B5VCBPi*2O8P5T(yuv0FWs_ zxl^n9j7gF|QF}nmY83Ovq3gP-dNnF4Gl{ci!Av2=38*zofYVLmvnAtL-#8^1O(KGA zfr<$B-?uBnLVbf7H~HX(WJa*MAWLg?J{!0}{?z_XV_+dnox6-B;K~?WP)eSEP~(|M zXlWUFuAs(eC<2F?CBLqBXIz$l!RbVY!&I&Q)0nUG8sHbeT`io4;R&~MgQG<_+DP4? zJ#B=1TNNMmT#4X)*iDWZ)1{AiR`=U=#XeJRS{y690ya52Lild49-QIKlF!AgQP;aI zXeG~86d8zwPiQ00wG?R}+*@mXf^|mkVC)wGUJrS$r$`eLfE5B956L~!NbU&T9!7?L zP$Of}X#xC$8c<`gzUVssm16~KHC{PRfJ0rm;}OxS0uxeQ>XAP7Ec!e?ti0+!G0B_Vdd;S&;yXgI;+E^5L{h?!b|h)4~53TZvoh~6;9WkS9tPq84d08#N8^`&URGj5IraB1r2 zuL1de0p4_xo!NTy-Qlwwhi0m+v1V0f=jS6-7gK1n5G0bKmCbkLxtp3kLqc_MS1O=6 zdMt982`1OTU3nZBHxGuVV&;6@M2E15<2i2|W@em!Z8Q_Yxb>KJH5k|KrRLp{01Omh zKhW+3Lpwu_8Vq0>a||$d5@4)L4eql-=o*Y?8hb*r8)arWSJJJvsl*M`GN$HmJeF(i z?vhW1dTpfB328Bn;y!BmE{x-1TzY!uq)CeMHKTFdCpGVngipgP`+jOZmzr<4<M=s9s9m})LVor@9JIpaPM)TO63se^a0BaKVc*I+s>1!k<8<6s0#k6}_O_t$N^3(t-#}2ra;mC3<&-0!;F0VDz%{s0v)EB^33FZ_0 zVq6*f0$N(}2p7<{qpGQaUR-v;bw)RrKO+)S_ilz(bhMauo0qi6!2$dzErAo8K|t}wxOd#1;Ez8Tl_q=R3M=Q49*(pfy|vM8kccd zqTn9ZPn!W;Aiy$LqN0cT8cZoQen(Qp@wg01huMllHxu&`@ka7+&zcrd8fZ%-gzbuO z@i2q6=*bjcDF|kE1E$N+K9NSf?GpPdJCV`R)7q#^L)cface#KzTwQ_dhPzw))bLz$ z6M0^smK8|&#+%9W61DtJEq~YqjnN-J6P*TKF@J^VkB9lrD>|L^M|ZUTFz1M8@<*`d z7IrLGCzjScPM%k2X$lhRenNnBu;L8E3fGQ8@P|Q0=vmE60w|Npm}+cybu4GnG4n7J z)rF4)Gt}zeFyZTm@@NR~{v!Y)m&EUlKYVPh;s2eLxyI(%?5%`%JPIWcyBumk}Th=wp%8f%Lfb`=}$!6EEh8>0814p9!cAv!47i54F>iH)h6AIS46 zEzLjz@FRKNq^19$rB^2B*1{>c$%;9HFcPKh7i^K`n@n^L=e@Iz`FJ0`Gs`yv-#WuL z9lg>pEhCy~tgjcsr~Ec8y$T7ywgT|krRT;mY~gP5{9YjMF2F-Bm6i53JXttI5FSg` zcV_3h^p9Kfi*9T^#9)n%iBtA1E5Kl!jXNazCD7j}Kkj+DpDF#QIHy$K!g1vJH!Xb{ z3EzYn=sUE`L(B5|p+7v?=P|7@vTFKgtKM=xQ~sBPy(L|GiCVx^bk8Nvd$g4P4g``K~3pkV&;x$hS(7?;_5_y0UGo7`Yv9Ol+Z|)-?+; z)BBK?tw%!DnCWTY4UlkMyy#+-(a#?NGDaBHZrGXw_hYw1(f)fwtO8;VbB% z_4$?P+EfMR#%Uaopvy~#X{IVOx0f@L`j~ng(Wvg1>I%a;P7Anm3B=m*Em4sWR#@8m zbX=wR5Y1^WLj{yz;YHcjxRi|Z5{^7kqm>zdLcCtk!W-t|><=~B2W@!Yi!CxH%Y6k@ z5Lz)QoE27ss0-Yzd@}|043pQx9}?R{D+pkiGn=C|t z(#5PABBCx3poG!x63#nAjdqVE9_`Z62-iYUN*9agzf$|FNT~fG19a>Jjd5wb#(*#? zNH{mt(%OU2${|sxe`Wmpm^{Bx$IeJ-`6uN0ojUTV&8B^bcCHWWprsnyV zBX5C^6?oh{f2?S3iL+vj{U>?;ppK)EHu!@n0$c-T{KGKAiR}swkjEDQcS`{-amgEP zwg8ULPw4SCTS=>MA3bJc&IE_McT4+dX^o-6kWzlS{olsFUC8?(Aq)y9~LDE49-WYR62E`;!XwS9xY73{~N7Idosl3-paO zWehg0QR8tiK%PIT<60z8YA|^{w0tTp$Au5cW^%y@(G|?PXH5sInV`nwE1AXbCLE6^ zC}OyMizSl#S8zY_`e^wYBmnyhz%2b|T>lErlIQSd2WJa_MPlhPil@$q94rtN=4o{7 zU$8=+VQDQ`DZu4!StvB#{Lk)l$7FA)|1nvwOJXcx)t+=XW(Ha#a+(>C|WhKUSSbP!XMT{@FL*Qa5$7$U+|71%Y}evosm}FP}GB1fBlhvhlOGK z3b!m~wi|39ub-A*i-e9EChzXly&ZM;69gN)g6Jw%PuP*BW?MBqYW%;N^NM-=ufc8J zP;YUw-LWxRN@=LoO3U-HWtd##OX={RRIVeUvVIk>ks zwRA#ru`}1%ZxcfFcuS`q(7z(@Q0mzM36*>;0Hi9}fW8Q4Mz044=FeUS2W{|A{;fIN zaA+ZXMbn9HKpyYJ@Xf?W%|zdEd_+UL+8ep2EZT~^!>MN$5`aMh@ZCcW8Q}5Ber1>d{QjMROEU-xi{lD5BoXg#I9ksF3=s?WKh! z><%x&X?C{QtC2-5skcTyNxoFcMd+ogVB@Fi zHFCDt+zu^EelYAXZ*OT{(w&YFm5wl9S%!DC=Hn9&H}%@dMVFFyEUnlL314;@dB@X= z^|azfo9WSW=tbE4b1UoQ3zYEQWIY|94?H}RixsxYx4Qv!UVw(^yjXYLA6fK3z~uMkAs zL4BmNv!fIHRC%W%ld`K1OIK}dNC1iws?gmbnU(KiZ6cy-|BNr)5Q-;0rUVx3-vjc|>reUUz_sF|H_2wXD;@&5t0MTRr>dRrPbWHUyj=RlO!5JB-}=eRpM1 z`hOMx2i3*a|0{W?P;WDmzXpT1uKy`V!~3hR+koCP3TJVf^3l<2HzV(K>OG%&uk=?# zlDN&)H{oUO5_3igmxr6#4{T~)QPospBb|AL;Gb}$OGnz*?m*rd)O!;W3g1zHx1w9C z?78a4vi#K#<1%J!Awyhd^}|`~@#C+4$ZGNZ+~U!oirwU4Yq)UdC5SLxk=hQCc4e4Q*g`xyFnASyp+5-v~mU#T3#kVM}n3k5W_!j zE8Gz6p9h7CKhg4eTlwb=M9a~kXYD0zNDHjW43wHWO^_m{8|``)$=ufsQt<+{u;g=T zWhW9E&?vwLITDbuUtvFEtgfCcq zk%ij{fU12ScT+=?26LI&)_S>F;TWSSqWuayNY`FS-XdE0B@%#(4A8d?X!3xeiM!-e zd!;-FUu*vf06xP1qp7Fk#_q;D*FR zs@q8rZb?d{DMF+PLL_G;%U(EyFC%fksvAn)D(brf2`z$t*TA>^&;~Ipk1}l_Xo>oj z5h67iR@9kD-g(sbJrZibEI z3w;uMZZ=9RHEB?TgynTM)~9h3tEdIjXAwHW%Uv2`x2^ibHS8KQrqxFL)l7|Q^3JCN zcSHg(kGu=%z>Dd?NBiN;xkQhHH;epe zDZRSo^89TeA0PncUy1s7U7sL)oRmEm3VXs1do;<$VARE(#l6~V8^UIWUT(5GP_RTZ zC6$NO9UHapv9+gbN$eA)Gwa||s-*+JK*ARsP2M_MHJnye_e0VriJoL}pWQD>P5Tr{ z&nE9;S~VXDb(|wWFG%{7A*qa(b(hG~Wk9`D09X+T33|04bR{L|vqI359fHP@E`ct9 zKbL*BOt%C?&4AqVa*OtD$}I_9Ew~__BjcDc{8mE`Z$(m0)uzPMzn#1xTD1}hpL+*+ z!?fyCT0JP5`ijoOL4o1EVcJBReYkv8>PAf@Ww|K}sqS&|Hqq*Bkx<(c0!+7Si?)#P zu45t9y+Gb2w0b5I-hNSlMd0Go!bM{t)x9N8%Ygc}098r2_#Z)7kc^AD1Lb>1I9yC@ zA*rv`lKnk-TWEDH5*qP?07u(jYfVBC!dj0d-Dg-?AaVp)Za|@HATdF7e`LX~_mg)S ztv(hB0H!Y*xEdsRHcnU6ZzIpKeptV)0GB2vNT8hDf{_9sY9!gPUyn=9p5wmGYj6oDf}xEm;@C&^SbS@z)h{EVhW!Qj0R(y8 z5X7;M>aq5waX$twCM6nx-zZU6ugA)pM))QvJvxLQQyqFFw~sVgxR<)i1I9e6UqIdt zTKyvuS_Y5Sa#}N#*1$WHluj2Ay#PAZ?wpuTFpro{#yqNTA#W$G*&hkzFBPB?RC>`+ z$(Tp=@MdXD?2fPR7N9T*jj*twu}hQE=whK!rqJjwm`9cf9ZTLWT2qCD1|28Bas80y z8KRfCQ>{x(8Y4oEbyR;Id3$Kh2}r2nd;xg<_GJ+vv5x95m&X?Y_a6dWmV`Xl3Br|0 z$@7Ac=Q<(Jrdmfvu2``C-x^2tcae7mt+^Hn#K0m(AFZ8CYZoVH&0->Yg{8JNF>7EP zvD8||QT~QBV z8b|gB&#X~ga))?#aJEGKOY*L!wMQVK`B(v2Lu((RweZ>{(*lbp5WU8t{?C5tX<0_~ zf0FkgTKhTD2LIv|101v!==r*#r&vad2gp-IH80*$0K~c^QkRRj7lbX6Qqu`ODRijW zzh$Iolgu!33AZ>v-h=6&K}cxnVDcV92j$U0wb6uAB#JU>vYitJN3v0)9J!X4)*jQ8 z(@)tni^r4qa5`u)5-NkkOasT;m031T8iy{{i><$S3VDyDgHA-k%TonlUGqjP`E%qc zrnHOa2#_@TXK}HhB#r*b>onrbTSWE=%uQsYtFU``r#ax#F?et&LuW^uE3=9kEY&y` z4W~vYm>clP3Gfi$R7C9Jh(yQnDHpfdNr{~SaFbgVam5JVz>$scv?&j3oQQD6h<)H< zpeghMzS)U1r@c|l^sqrhBGiH6E>Uo{iY5&&!L-H{qC!ATxc z$5){;yijFXWNLfD;1)ZLHR09WuX4INg$@LpmaEZxph+q*Y*RK? zsEWK-b3N~?AJh&%tdnv0W_ImSOWbvEE%8Y7EqZJFZ` zJ>|0rVPN{>ea1m>s(rbM2ZiT>5JdM!{>j;FIDDHXBiO!7IsoJ(rowKZ{Us zpPkViSMaka_-QWKamZ%6P3CPADp-=k3VK6**x7lu9q_30xEfiBNEuz* zndH5JE4rV5UO{abI-QIoym7VNg4%B4+U}CtMg$^l%e&Q{PP?*DEAy#O*QM9jLzsQv zhHpPH!No5_0KZUDY;bFTDfQ|UCPPCmn{p|vBtj4f*ZO#NB!lJ`~=e&infGY&Pp zXJ?d0)u6*f3Y^(@uHu%Ir;mtp4j1BnT@N)Idz> zMEhU-_hI~VVRSoqM8MMJwRm*+7V5`eHyE0YBSq?lSSFn`LX9DaMPWPf$aU%mMf_%G zJcu#mD>H_;tJw`c8|V5B{sy>u-BNCe9z|lJLK+6yxVI-8OA0bYLOxXl)zd4SI*WA& z?&Yi;jSkb3Zap;U`JHHL%+)wNhX-*?kkx*DetC>Jj1H!K!iklmOL!$ityO5ng5V}| zlBU{y#wP-qyLOGziS3X1>b!Pd3sE`>@i@`CDHb0rY}kXmcQP*?Qa{MRD9_{AQAhC4 z%~3p$iePA1O!PGmX9#%V2mZwwYMaP6ocAXWaqbxt;#U<22~;(yew z$e3VfybW>qHeMX2**G}ntpNkFTgo&2ivzp`F769S#bK$4!yoacg?xoEDjf9)!t*0A zIa-&ga~ZpM`yj?7sI_ivoa@5c6z~7<4lTpLfvEm)B+%HSmZ#M41+89+(*g7;9PQ04 zQabdFBi>LLb=1I?5J7x2!K&{WdTyVl*x1w> zYGy%PV__VPI}IDwS{cWrxH6^Y99yC7rcyJ9Y&gcoM<8nhobzrY@PacL($|()>g{wJ zb6dQ6hMj>`4CmGOptpt#Y~0;_6Byg$n}`PT+;x)re^(XE%1f3^be_u=JZR*b-Cae2 zpolaN26|A0mP(X6t+M>M0F zPQ}Z+GI!##SzBTB#AZrWvp&sTZ8Xx}Gpj?XakSxD@;(A-J!XXZ0YkCa@g)8}b|L@t z_S0bydHW-G4n*GK_dMNgoV&prekb~gA0T+s2`0mrL{u=UoDh z`w+qJYxITPQ5kbBtfs3D_7ZuY=63a|AGG#mJL7D0uwRX=#}2Lkwh`f&Z@{vFTNG?R zTX4m9-T*Iwi*$N24O}=#G_XwLnbUd^AA+XirXglAr!bj0lNpJX=7nIeWyg}m4pj)5 z+FGU6tTRxXH(^~8u^Nc6sJf<_UGJKVddd?{CGSi8A?y%4?mRRt&CYl>nrezZ?h=Qw zNLZo~MC-&=gkgWY!o?}-KaVme+8KX>LjO(N8Nx6^+&4eKoA3&_8DCk1(gT1TMHbGp z@xH^0`F6%n){9X8(u>07Hqvh!J9e;8c3KU{49r*4WA07P+Jf!{a?DM1A5tnUyqLVN zf-c9Ws2?;kWM^Plv1iVXZbBSK_;R8@Afbz~rO3(0CWG)bM1LYb#B+uOoAuHSXWRgf zFx&>ObM=$e5842?ft#^3i##bwcyp+YSd2FhvojW0B#s@N!zb97@KuCQv@;s4S8eWK z>hHF!X`|e6Cj4V9?zrJ2%qxASLn78-=Kls$WSROw3o-L|GcM|fHJ_4)m^FvRu;v@` zcsRc~F>A&c);N(S;k(KE7T12U`au)!u``|pXS_)`^N5XjGv0jE&bZeiujY&su@c6# z+^zEgyoqVKn}IOIM1xQG4IAmnjWMQ(L_y_RjERe5Ny;A{4B{eM!k?1&Z6?%n>IW_V zjJ#}HpRgtW?3J8hjbq80m1yos5$n*kNz5Ilxejl0;02-a@g)y_bhW8O42b>k2lEeG!nwKH;) zzL##J72>@NJEO#U&+4-vqV+iyY(ldotu5%Sj0L@`vY^-dhQV9T&&T;DGs$657uAWV zd;oJ=8vq?)HduJ}&+~TdVq(pUWAhc@C||RJ94%EryjZIzj@{Uxu8bEx0idZXg0sX> zA~y1y6KN7@1~egT&Ra=-_^T>LnY_A1dQQnQ+Zf?vZq&Jga%_ygU>#Ssal_P@(3nf! z_gISNs~?aVBiV=e`^4S&2V_Y$CNv&Tp3PZahsVeF?10D23~YRUQ)hEe8(%5tE`+Liq&i#J*-8rT4bDfmO_Ihx$TNuZaSe%+ z5Alom$+I=*zij10{32VCXB*CcE3x>AamhVf>E2h#`#HBw|DeUMSs5o`zpZE6B$D@@ zg?Qp0c=LTLx=JGJDA_4?+LlXl$LAX&Vpu>E*5NOBCr z{^<>Tf|faRBNfc%QL+n)4Bk{n_sR4P9xXn2I8Du-^iI!2YE63u^b;u>vu~CwbH2E` z!ZdTzzDh%Zao#UL@RL{}orFb^$Y$jIivM26KUXCekw^h~wqw@5Z?PO!YXoQSZIAqh zA&TWQ(2b%FR2(m+kvi*4VoW1@k@p*}@f!7mcI<6uz|HB|Au;14BW=V7@g^ocZc(7w{e?Hg3kti5VZ6Y9qbAQO1W1P1k8fQs|C*a_5>O_5NI1V0Z zX-?;fc&L4&JZG7xax7q{>}a+JGFR12$iyaigWS>H+NaJkQI|epS&&CdUNut(+l9i* zIM}Is3GSwCUc!>e?>UYi6~o0|ADmaGE|_y1rdj~a*PsM-`%ZTYA9WTAcj8vNj(%LUpe4FE)QK~LTi2)stTvoF zh_-6+g`+gX6?vn#bjd10@qnHdKp312Ayy4GWo2}C$gb-(T7M$~O|Mh41D;#JUUluH zi5ySfUs5Me9^s7YywLGO>#`-33a9bGa z>kMFF8wY8ocJ+jp@M-|usPMbuvN0@ywk(%UgY|DTFilB1w^A)awV(zlRO`w=J%m3; zJ`XdGHR7pQn29`3K0p3G?Kb{-ExG(O?M$BCS$?jMmY*gZ{l5q2gBN%^ZU`R<5<2qp z3HdhXdfre!sQptr<2T69o=N2AI~(y6y!pMI@qM%$i17Sw z`OW-eQft%6(P)7jgsm_e)nX#^n>~T%v9p@#xY&cGaLv~1fE%2}hE5(pz$RaLqYJT^ z2WjcT3ABizP{q$h{k*8{l!*lzcb!t5i5i#>+3DzosBlAdvCy302K24oP00d++B-W| z;<#bN;G}l+vi5~A!<0zxXi8U6uI>)lG`Nk?C3ya<6t|MNKv!smddun`Qi)b)+%s4L zc#6&Ejx={LJ}YNbr9MY3qB<}2uvP1JM9lMBU;%J25K|N<1oGGOE9zadprF_8N!QV8HeB0vh zGuZw+bL)P3OeuNx;-2v_Mp8_G{Ed6@a;;}?)~ZILm=&X|gRvrpoF(=^&fOv9UF>uSa8!JJo@kk@JI20BrVO*Q1(g)3qGc-H2qdZC>$3M?LygvDVSaTmPVXlGz% z<=BkY5ZTmfBaKMP<5OJSNNWPwIBQkgNKstE{%v0Vjq)9E;^8WyRv+YRzG0%D)Q}xzt3L5KiBpnpZAhyD9a)i zXMhzK!amlaRDF8~TB5Yhapc>F%jMwGvk@oObiAE`{Q{n0NksAt8}T8$d8VE5Y!Z>Y z&_;SOsYpH`YA4-wi#g55Aj5}n>O;MiG%C89{(TMk0{k(rsUNiKS}Wt6f&I`AYdFK1 ze#a)J-vro*GQ;J-Ag5d3O}-(h?3_XB2Q}VfXUql-MDuE^eJyT z57W`XR8yd_?O-nLk%$iF!uW{wWu-@w)oCu{Op5B zTt^$ax*KGs><;ef%KsV_Yi63KO%!&*hT6jj5{ov-xN^(D;;RE#X}Wblp{dc zAYVGSV5Iul;BOvaXXM-Mvi3=iWP<{JDAsY!+mUZ9zg?()kg>g;fqgojG}Axb2(#ur zY#c0HH1BC=)JONQ=!4*zhuNs%WJ<0yUzFUcr17)t z?F`^M_PHL&Ek$#+jfoZeW*9JT-38XG7|LT5&CNDy$zP3REq%j?HV^CrOeCw`)v#%S ztfHM*x-d*>pK1e!wxofqYFrKSuxzY#J3Li;aJg^sEQ67hMXx6ER;a2PB;&fGLXFMc z)G*ZM2gx^uC9OvNfEf>wZwCIpuz-KCIFL*eF2U^@<5;fm;V{(38~;ypUjimoaqaJI z?n%_=8iVT>Z3u`c3?K-~A`Qa~i-0TxsKWp~YxndzJ;N5nJ^#cd#`T$vh`SP_Y%0;1 zjK+O8BvGGP)Fj3jjfo~kLNx#1@7#O)o}TGOOx}CnHlwVV^XC3&4&i{IZ~nyg@hA$VkHe#xBy!4HY6_-S67oa@-i1OKJj^ z-?o5D&_hP~!rDW4-nV#PK*qmWzy+m(7r5TF{nH|Sxzgx4XFxD|cED~B$Lh_7`tnpC zYGT2@B%^ZrbD1`8#RK@T#$%00jYuu?q2Yl_6y;IJti-;KJBju26-~M&v7h5k=JSI{ zuI;mncEsgiC!q3M2Kx=t8r3mtG+|G(L3+(-euL1EMs*{B*?$VZLX+#Y0>D5E;3|Ji z*#=2eS-gXhahL@}OB*B{K@wvu+JK5pve@+cJ-t>j)u-BMg(jhPtC1Pl(R&3@pq0f2 zX8`HqmEM6vp5CxPyMg&4TkB(DGXyaepi1vrEP`{3EP##|;0g2@mq7<7&xhECX3&TM zp0Lz7ZVlUtEADGC`X_1~cRHTeAI1b;OBFl)MNZ^I3PwB-meW*NP9p46Wrby+_Fk0} z=pocd*K@#GKNg>Duz)P&WNdjkX|;H@$k=89bBvsLlTFb9FwtQV5dkStuz=Hh<@Bew z#F-Wi;m8teEnr#2d|$F?&B*s<3&3z%oE9;+1s}W2;-p-ieRtofY|ge&%==8lEv|a; zS+a*)8D$SUCwX0ZmGdp5)P%jkADTd|3C4%cuAFXR;(dnJ@^Wry^kNTu&`7H&_x|B@ zZ!bxOdU}^{y7xAq;6%S1SHzVwuIc~> zJ2KXa$T8~1pc@_8BscglUqFfGEfHuZR5(RqoYtm_Ohb771>+WVnzlH1V0@Pdex%Tn z0f@Rvv2{CjzXZlWx&ty&4X!fcmNV>sxp3zgpGv3cCV^?s+h*p+L5QEnrGmVMwpW!^ zsn~XTsTJpUv(oL$?)1&`=qRy9urK*7v`>rP4l03+98}WP- zw~%hCsoeRJi=4>pKgj~lM2D*>tKB5AKNn_1D4Qhq=R!crh_Tn<{BDz+WzllT zH`@XVCLhE<)Si*FBRW;mq7KTK)Eo{8CnxI0VcXE+=Gqu*6vEf-sElzH5 zBDIv6bB!!f_BJ_@sf3^B59DoU$K1(IWEx>ZDPB`Bnoe=6!-3piTLtdG$@3jI#jh{Z z1Uy|}0p~%grk9thuUNbeWW3Y@)|5&|AX3=T3cq%CrG?ep`vQ@;ytk!Lr(``V=Nk*X zc2?c8)Ze%0Z0G9%)G&(U&L@xntH(vL9!=ipxM^0``I-Q5ljG9Tdoxd>+;Z41+7UOI z&S2Yg2kmu_E^kipVP)3B!@cr`exRIullM7pp5Hn`69B$%0o7==ndMvUVT*S>GCpDf z?R{0c7P<_8}+%7!ddH|CnE4O@mKPNJat^7gI z^6zNN&-P(uTK+h%<<%Qf8~r`UUBS;pHNnUKVgcM0J+*wJe`xX8=pR{tZFJ8$w%xVw zWA1?%NjAEBxu3yb9y6MEjNj5UcMkI!+f(1wy);-Oz;C6ucPlntcvURCLz_HH0^Ce{ zwxs6(TCzo>eK!Y3!cN>rr_G~C+Kbgsu(-VkRUK}yu&&^0CN3^Qmr;sT;3u?J7bb99 z)N!M%?`oK{yyL33FtM&(jN8-HQqTnq8Ad=2__D!|fwxb0##>vuR;w7bWB+U=8-3Vx_T|1P@DK}b}kWN)XBVo{mk!@ui? z>UmG?%Dc3Ef#aUV2DwfXR1y@ZbMU-@9eu-TyO0JPNt;h;=qObS+HoYUj_?9IY;W(< zqv>1di$un8&*Nvf0NsGlS?yU1SOt+-P+lZfTD&%7Tx9_rrA_P4|Lx~koaL2fl6g0o z@#Pk4{S16dd$l3kja{z9!^-n|WV8O8exF$XE0zB(zt3bAMllqphubGWf&ZrOkQ%ja zpU73w>oW);L61)@%D?3G>3bDoPE;D+jH~-f-na%8kUG%@jxQT<;II9wj(Z`VZ~qLF zfxD38?M`GNC3ZtFu3e|o<02ncW_lbEUKMAYKHH&+UCfUS(gZBrYyop1&!?4_XSmjf z8F8US`$h|xUS6KJS)5rF<@pyzo*S(^{|j!P|0n!DwfXDRV#l2cXm(nXVgN#Q@`2_A zb6}GOnbyt;<7nU@tpu!l5D;L3^zTpcqoshX`WFVhU3Ege2`z|l77AqO$?b_E^x8`( z0&_J%bHX$1ay)-`9g}U9MKSdsPULio-D`m;B9tvWa?bE!Wkm59&ymg_QK1rE$#2}N z3BLSG3wRk4SYKWOe`oO!Qmp+A3)o&Nfx*e7_CHyq7b=P1{Jw#5{(L2WRQd|5X+Kb< ze48hfIOAlBhO6LaO0W1{KBlU}1~V!(CNFc~|EU9A;8Y67eAu}^#;p`2w6;UXQZC8b zq0wH&`u@2l0AN@38a&_eZ6=#{(cINeWHFjHak$Qvy?i{Yg0>A^JX8BS?$=3nt0vu& zI=}+h!VP6xICYrCLkp)4w}1*Qoa%3pD!1^|poNDN7tOwxt=4j72hY@S$NdJ2!pge? z$Ba@V4B*avcTsuEoyZba-pulqcYIF|N3V;dCOPi6@U1)d*90Ggi7EteC9|}A1)gH@ zjzPwm7I3`jBAy-^xOb+YQiUHFjf{&dpn`j6YNdPgZp9^uPH(>D=jY_uuB*NuN$u6TLjkEdKtNd^=N6k~xpu z$pzesGm@Q6Z8GFn{r7C;sUMCUny6QM z6%Phb6Tn%xHgAL8^X^Q+HR~4gFhCP<20L8{m}WVncjuMe-E!KIG%uv!vUM9X&0sPY z0Jv<00NiL9>DqYt`t^R$s*)p)scRkgJIvO^1dD+b+_yr&70BD@cjzAB+fuh##1+W7 z!2-_h)uXZ9-!*y^`Gu=i_z8qwNZn-ta5*pTBbl{j>VAuK=`PonriBngDvd*&O>DV! z1`Zo+8u~&r;m>Ky^>SvhNBL6N`?{S~L768S}Hf^!6>An{0_1!6Ky%R~YV1Mxo z+dfze+YVUr=(2^i_LTHc$GwAvdyC1Rz-N^KY(5MnOqHF-(qjzXCWO*RV{@lSY4e_@ zfc_q6AoXd?lp*3i$cfFI5OAQ$X{0`lc{4=PbLu?4eiTZ`0G(0&d#HQx>m~E$SD)$29Css2IgttG zh4keXKo6vj@2F#Y^yCQ=Y%wd z)D0-grUoWU0l3?7H?eFvCS9PhQR-eYYEKg#@BM>oJ?1A)*J`RoB&4D6MMZc3S|wJ% zTH6^NJxW8htUxG(coql8{WFh&DXzFA0S#R!W^e{E@7=BGd9(Tk5icZyg191u(|2?- zV{rI}Y0vr*SpNL@3B-fTQNV+5@W%;qwcEnq2@_7kU>H5%coV04510rJNR~lv7_7D% z9QlizsaJ{qT7j~N0hQz*4IG4|G4?w??tIxUAZ@}Tv zH6vi1zzwCmJlazz(m!$B?~&%OG{KjCY5^EH!%fSQs~!^Z_3I`5s=(>N6i zTYH!1EQH#`8ddiLiq`h}L2O%eTu5k=fSb&gnP&jNp!6y$oY2*xDCC36??z8$&zvG%S*Z?gZVPd zeks1g2qYv9t}-~J6TXBcJ+rq3d<{PMKG_2-{0bmqvmwlR704?8d+FbU+`aL4{g8nf zL@)9yn|*r0i9y?p4$M_JCyd>fMA$s01=PCZnO?nZ8Oms;pW}A3COCp@-2gy;3;1nG z&4-f-GvXIWdU!ZrO)co((s=Rb3B0@@ShC<2x%QO8%)_D z{81o&)dHX#o0bmy^feagdF1+<1#Cwq_UXWOm%*|r{0Q{i43{4XbA3G4H6(cQ=1=4aSnm;;rLNtyOq-ZxxE8G?-4vzJJ!w#{V!m^@NT%zNLMpt+; zGmpWehXx_A8KXLolz%~fHaYI&Y{5Thf@;|8xKH8v?sZJA-G%(T??ld~<^s8atUOSv zqh|MTBIgkP7;4O&hDw~~P7RkW1K^&cN47IhIqoz35;x%Pz7F4i+5(<{7@gZgjDBVj zD0o=dg(S8?jL^*frdQ@y_T45RzhVJf!&U}|{#ht1B)_-V-$!<=>B4VyhuJr}`>Bwu z9|&C-MZ-A0@W4PWnqb_;jT{>2kP_i5F2NuUQ#-_hFT7#AC?INNsW_5Q(hz5-DT)zF z6_X66yk}XBPig{gcRKEKc)sV;Oh#62%j`raavt0ALZ0_Y9fUS3*YyW9w|K3V-Oq7< zOqwTX(k+?flYK%N}YGrXvUJu_1|>C9Rgl>=nMN0WxN<5HKyQ_Oh*(JF}KhbJXh?}E9t7S1mZf7+v)dbvP5IGQ}~0KYUNJoQrJh)~&EOD!P_%k0ni5sm=&z$TtuWC6djpDxia zQ~jV{W}75E6Ms`XB|Y1_TCDxSn6!7JEhV*gOj3LL+UCM9`&UqVR*!#24rE4Ngq>Mx8o#gSf z?CklD`!Z;4quFlT0DJ*%cp=~v%K>YF)jHEJ5S(zNn&Ev6QC&Y^@#Mvj2|ndT7V__p zfK%lv^^t)xu!8pci?u#qg6g#t?jCL2+nw4Ll23 zjRn2>Be)!-NzY1j!cP(3^Ie{}&}6j+tq?X+{h)z^)HfP6%ta!q3%ESy7bspu+)n=s ztGRw$$&FL;MJ|iMZ2cfnTHDC4)y4fc<<+lr=H|-klkyq+m-tNNR9U2{Mc_)wg_+qV8jc8Xz=k%Z$)S=(nIKIXU zHxO2ayD**`pg$)nEpI0?s7jT7ZO9IO5b2BwKOH*3hSkfUgU77q|dpu{*F z!pcek9GrbIpq$qaLRFIqufYPj9LrNEaINDNG@xIs2VZdT{UVj(JIJ6$Z|YK`0uJ90 zt4AeQK}Yao=phzZGoql?_a8V=kH4UFs7wZ!}tH70eS*B;dpFJMQXQ5VxK zxXFm?OeNq2j@?_IA@o5=uyA$=`jpyqa2^cTHKB9CGZRwBaI_rXFmx(`p%7NCO1zbd z=Fs65*1<5N5Ah15e0z_ahP)oAwBYEqJga6RnD6R!&}(fN+S#=lJ+Js?u=;+Y9x8oT zS4(WHWLl3UQec8+QQ=7z5R$ft>#eZ-2|5ZFzLvru#(JR6#R$Dn z7C1A94Xz~{h(4lo!oaQut88#g<3GOZL5fptIZCi5g`=*KN_ZfY>4jbpO^O)HQeVPH zz--S>;Q4Nst&CzdsP|VUi8fS)4#Wd0rPYNG*QY9UWvWJ)QNz6TsqzwFO4;12lxCb^ zRckRnmJH%;l&!3$7Fa{jef@Dr#d7y3wiYQu5-_j(6(2|v46we;SJ1ru>Pu!<oU{lWWDT zl3vF>iJ6kVmVc*8`a1qSLDDzy?{G=q#J|T$`WCF`CQ0fKT-AM++iEeluc4Pd0(jX+ zBz-6Gmq>aO|DG=CE&L0*cWM6g;ofTTaYwkWdw7&4;PeR#=mKuAqfq2HUEmj9kaRaG z=CI+zzwMHK$fMlsQGU^pqe*myCZPP11>9yR`)(V4Cke6#T8{jRA^fCZ%Tfl2rf_qyM+4n5`M?n0G1w0HciP}h-f46U7 zcFpdzfX98*CZOgV`{qdiA{GF#QL4>E-P68-sO0vtfaiVG7NYKN-{8)I+yNHwQy-OE zGP#588(431hgiT%KxO6T4zth)aW=y<0*41Cb5V=&I{fu%OK>MLzq>chy(r2?Syba| zntKh7R_kIDhW}tt2ox^N9Xx{XwX#~|a#fBDX1l(v2^bn?0FNADyO*(_VjCvc>GatT zww?3?w65k(W}1FM)9so*s43#}0Ddocr0qU4KjtDHKd&T7J7C;J#5gzWWIZeRjX^sr#Gfh&Dd=(-XTuWj^Fc)`Z2;ZN?qz<_nEug+Ag1Ll+ zj|XDX0#M^c5zOW6n;1~@7BJaIRS{fa-yqUdZlwj(`lu>`Yweq9Kt0O>X85Qof*05~ zGlBX=3xJtRc~ud-*uI$q)JrU29#FM%FSXEdMG>?$d9|%>#4gJHrv>2Lso$A%-?H#V zAg;3jj7won-eBLf0`*1^CBU~6d`vwcM zQ0k+Ikss{o_3XuJBPpJM^m>WTp}vg*zNP+3kP&sq_9hMm4?Y8o8saH>&_06^BGkWV zPk{=fu|+I(m;qX&t8>c{n24&G4R5DLKm;%H;~DFApuf0P3ci)j*Up#fi93&d>>v6X zkxu%#=N+kHr@c%Q)c21a8Hwjd*E6}k@~D(Q*y+PtaWc&ucXF>X&3r-A6`Hna8rQS| z&7z~y`!V+$P9NTylR1-bay#_>6`EeE=~_)!Yq}im>E3~n>kjw3;mFm0$r1`deji7; z>G0@{ngFn`BPa6tLnMzKg|RBQNyqds@GYZ>w28@6$c5=51Z*$%u>9vNd@B%-w1B%Q zYW{SYA7I~X1L{Bvz?iJ4>|y!i>>F$&<%d|n4}4Viu>A4%O*a4|E#N^Pl|3wfl6~_K z0AnrS5g(O3EFZIP5ceZL$pW4Ls#b2bg>Lc2D$fbdR_07c#;_h=VDc`A&9Z6AKKf60J;Ck? z?sfV%?P7#N=h`TzJ#U8j%P|s~qKK@zUaw38Qfw zu9^msl9pee(2(!V0-03yjGACqS$oyue`W-$hJA) zX?mHaXER+`qiHo{(A^2S-0A)u(-d|E>z?t&@g(j$&hhRI53a!B9-nTyc6`>6Ni6&} zO}eF{uLb=^2mMje=jc0g6 z9J#LLyfqE`dY=```W(uhIM?r;x!EzqTIh2a`dUv-ySp&;$TzA|YTH zy2#<|BA#j!c!YHLO-&OHjC6BxuA4}-#R+Xwb9*I2fJ>YyTc+M z$5R0`KSVLMupC|X?O|?zfI07-eoff_9A0JP$)f3Jfxge)gZ)%r4zcFw*{B$mD3Xjk z=wEGE+{5W9pY?tX`v=`avOFiOM2yhrY2-L=(u06dn7l54!GL@A*oJ9Y)zY+_^K&u& zi1r%qCHfU_4Z~|(jN-*p3}o0uN9-Yc%o-eV^-EVtE&CoGPAX z1DnOtb3pK`4fFS)bR4?~$t>=TQ3E;lTLys@?8uH~@%Zf^D>goXN^@(Lfe*14T^v%1 z6^QN@3=JgbbrvXtr&3;rYl7B4*O5hde)=9JJ9g1o9(MZhLbEj1Ro6*=GrAJ~+(lur z0Vps-Em-6WPXA%YQodk5IGx0IY68Hw4d5AQnc?hgrlJwpqf0g~ZB6G;AZ+=!WK>vh zcBBDxo|&o%h`~r40&?hd!BuIY`K@E4#lazm4pX*OBvg7Vzy}Ieq`fjz3$p>yhtW3%IFb zzJFM>+mP==3%K3nGox8SEYe1I6w!7w*lp?fUzqLmiK1n4JuV0@EO7ephN|2%1|I?c z3X7dS{Rtmx;3EOYJ*K=xC6XH93)qg9 z4K5H0W{mR z{uIfx5y?CrTi;_|E7Tj5XZ`{X7hAvw6*z3RNdG{t76W*8k1$s-ud!|^UQma zd6i}GdtBztm}H=0A1#?*$M_iAh(t24d+PJT(ItaZ;Y>$bSg22H0@`aW04vba!3o3L z!lIRa5H#?yfd|TbTx!!yFAFGF1-jb@FH|2dz>eF-PaL2LzH^BMj4%C8OqL!Pn_T^z z{}1kte~=Tl#U@GnQ*y$M&%x>ONI9W7HfgdfxnEBB{BwXTd0a;Q0~kxT$f)i3-M&>u zbpxYX+P^EKZU-g6*2}1GlFAMlRUnlY3mBP~<%m1^rMKjWE0mkm z4mqMrsidEmBTffS`gS>D9I5OnM;u8ixrgP5JxB!+Df_+*jNEzB_YqQQkiMIhn;J>Y zm%dk#9m3PncMb8bmIE6|X{^XEmC`D47b`#8P*cEIa)~Ut92gC6NyDF&A4KMEcvz`4 z#HFDXI1SUKVK#A2l!ghU(y)&-97rmQcgW(8fU)>DviSG>{hTcRsq!O>?~}#d9yg0` zk;S(YYnd!=0oEBGO8xIir~Xkq08oFd)W3v&Qo&iI+s{}Gw}6M`g}+xvbF97Kqy=#3!8{=sVp3$Jk-=m?rXAeZ*oDz+$FN$*T76=WWg=? zo%%=?e4V6HugHRnh>>|m7OVwE<{??ohTqveWWhXTD6>@-j8`h@ak5}AaMFEc!9m1X zE_JAb$&!9c>fTW*2T2`UDRZ{e-A$@_sk=@&lFT=y?qZLd%;i$InpkH@T^+H;N!>)! z$s8+ngO$zO*D>4VIGg%6E$ee|w z(sZTFIhGg~%Bg=P#?5l-1Imvyt&&qO@wjPPCa2aDYp0xgG_l%c_PeChxK?K0t#qno zHv3#tRAy5;TON~He^G9leutDLT2n>j!iP-2OdxDGUGg@()2f(F^69S&RF2I@01z)l1g&BOn-$`+9NW3D=?A| z$n>-EJNb@GKSgJgml))q(2b@f4}c>^N~#Yl5*4b z8<_;!(z-(?MTyfXG3^trXG`n{O6Bts+eD1C#I6TM+W`{0O1Z)4lfF-4dGdo7ja?F( z0>t=-5<3LHUW#S-ZXxWu=@(!i4Y^0q0 zD5;zzCtpD-KarD{D3!P6WF0h?b;yMGNoAr;cmNoU!(@WTkTf1C6IwlP@X-luiuf9t zz@~_wCgZo0PGg6R|2DY+f8$fcSSRC0 'a t +(*@ t = make () + ensures t.contents = Sequence.empty *) + +val push : 'a -> 'a t -> unit +(*@ push a t + modifies t.contents + ensures t.contents = Sequence.cons a (old t.contents) *) + +val pop : 'a t -> 'a +(*@ a = pop t + modifies t.contents + ensures t.contents = if old t.contents = Sequence.empty + then Sequence.empty + else Sequence.tl (old t.contents) + ensures (old t.contents) = Sequence.cons a t.contents + raises Empty -> old t.contents = Sequence.empty = t.contents *) diff --git a/plugins/qcheck-stm/test/protect_with_errors.expected b/plugins/qcheck-stm/test/protect_with_errors.expected new file mode 100644 index 00000000..e69de29b diff --git a/plugins/qcheck-stm/test/protect_with_include.ml b/plugins/qcheck-stm/test/protect_with_include.ml new file mode 100644 index 00000000..42f1576c --- /dev/null +++ b/plugins/qcheck-stm/test/protect_with_include.ml @@ -0,0 +1 @@ +let run_tests tests = tests () diff --git a/plugins/qcheck-stm/test/protect_with_stm_tests.expected.ml b/plugins/qcheck-stm/test/protect_with_stm_tests.expected.ml new file mode 100644 index 00000000..e3f40374 --- /dev/null +++ b/plugins/qcheck-stm/test/protect_with_stm_tests.expected.ml @@ -0,0 +1,193 @@ +(* This file is generated by ortac qcheck-stm, + edit how you run the tool instead *) +open Protect_with +module Spec = + struct + open STM + [@@@ocaml.warning "-26-27"] + include Protect_with_include + type sut = int t + type cmd = + | Push of int + | Pop + let show_cmd cmd__001_ = + match cmd__001_ with + | Push a_1 -> Format.asprintf "%s %a" "push" (Util.Pp.pp_int true) a_1 + | Pop -> Format.asprintf "%s" "pop" + type nonrec state = { + contents: int Ortac_runtime.Gospelstdlib.sequence } + let init_state = + let () = () in + { + contents = + (try Ortac_runtime.Gospelstdlib.Sequence.empty + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "protect_with.mli"; + pos_lnum = 8; + pos_bol = 268; + pos_cnum = 293 + }; + Ortac_runtime.stop = + { + pos_fname = "protect_with.mli"; + pos_lnum = 8; + pos_bol = 268; + pos_cnum = 307 + } + }))) + } + let init_sut () = make () + let cleanup _ = () + let arb_cmd _ = + let open QCheck in + make ~print:show_cmd + (let open Gen in + oneof [(pure (fun a_1 -> Push a_1)) <*> int; pure Pop]) + let next_state cmd__002_ state__003_ = + match cmd__002_ with + | Push a_1 -> + { + contents = + ((try + Ortac_runtime.Gospelstdlib.Sequence.cons a_1 + state__003_.contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "protect_with.mli"; + pos_lnum = 13; + pos_bol = 479; + pos_cnum = 504 + }; + Ortac_runtime.stop = + { + pos_fname = "protect_with.mli"; + pos_lnum = 13; + pos_bol = 479; + pos_cnum = 536 + } + })))) + } + | Pop -> + { + contents = + ((try + if + state__003_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then Ortac_runtime.Gospelstdlib.Sequence.empty + else + Ortac_runtime.Gospelstdlib.Sequence.tl + state__003_.contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "protect_with.mli"; + pos_lnum = 18; + pos_bol = 719; + pos_cnum = 744 + }; + Ortac_runtime.stop = + { + pos_fname = "protect_with.mli"; + pos_lnum = 20; + pos_bol = 824; + pos_cnum = 882 + } + })))) + } + let precond cmd__010_ state__011_ = + match cmd__010_ with | Push a_1 -> true | Pop -> true + let postcond cmd__004_ state__005_ res__006_ = + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Push a_1, Res ((Unit, _), _)) -> true + | (Pop, Res ((Result (Int, Exn), _), a_2)) -> + (match a_2 with + | Ok a_2 -> + (try + state__005_.contents = + (Ortac_runtime.Gospelstdlib.Sequence.cons a_2 + (Lazy.force new_state__007_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "protect_with.mli"; + pos_lnum = 21; + pos_bol = 883; + pos_cnum = 895 + }; + Ortac_runtime.stop = + { + pos_fname = "protect_with.mli"; + pos_lnum = 21; + pos_bol = 883; + pos_cnum = 940 + } + }))) + | Error (Empty) -> + (try + let __t1__008_ = + state__005_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + let __t2__009_ = + Ortac_runtime.Gospelstdlib.Sequence.empty = + (Lazy.force new_state__007_).contents in + __t1__008_ && __t2__009_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "protect_with.mli"; + pos_lnum = 22; + pos_bol = 941; + pos_cnum = 961 + }; + Ortac_runtime.stop = + { + pos_fname = "protect_with.mli"; + pos_lnum = 22; + pos_bol = 941; + pos_cnum = 1005 + } + }))) + | _ -> false) + | _ -> true + let run cmd__012_ sut__013_ = + match cmd__012_ with + | Push a_1 -> Res (unit, (push a_1 sut__013_)) + | Pop -> Res ((result int exn), (protect (fun () -> pop sut__013_) ())) + end +module STMTests = (STM_sequential.Make)(Spec) +let _ = + Spec.run_tests + (fun () -> + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Protect_with STM tests"])) From 0f2fa2adf002fef4fa609b59c716b790528d6cde Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 5 Mar 2024 16:39:16 +0100 Subject: [PATCH 4/4] Add documentation and update Changelog --- CHANGES.md | 2 ++ plugins/qcheck-stm/doc/index.mld | 16 ++++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 64788bf1..49a25e65 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,7 @@ # Unreleased +- Add the protect-call optional argument + [\#205](https://github.com/ocaml-gospel/ortac/pull/205) - Add a comment warning that the file is generated [\#198](https://github.com/ocaml-gospel/ortac/pull/198) - Add an include option to qcheck-stm cli diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld index 435f5df8..a1981bd8 100644 --- a/plugins/qcheck-stm/doc/index.mld +++ b/plugins/qcheck-stm/doc/index.mld @@ -141,6 +141,8 @@ In order to generate postcondition-checking, Ortac/QCheck-STM uses the [ensures] clauses that were not used for the [next_state] function but it also uses the [checks] clauses and the [raises] ones. +{1 How to generate the test file } + Now you can generate the QCheck-STM file by running the following command where you indicate the file you want to test, the function call to build a value of the type indicated in the third argument. You can write the generated code into @@ -177,6 +179,20 @@ like the following: (run %{test} --verbose))) ]} +There are other optional argument that are worth detailing here. + +The first one is the [-i] optional argument, taking the name of the module to +include in the generated code. This is a flexible way to provide pretty +pinters, QCheck generators and extenstions to the [STM.ty] type. + +The second one is the [-p] optional argument, taking a string. The string +should be the name of a function, and the function will be protecting the call +to the generated tests. The function should be implemented in the included +module (the one passed to the [-i] optional argument). The funciton is of type +[(unit -> unit) -> unit]. That means that it takes the suspended call the the +generated tests as argument, so don't forget to launch them when implementing +the function. One use case of this optional argument is to set up a [Lwt] +scheduler berfore running the tests. {1 Warning system} Now that you know what Gospel specifications for the [qcheck-stm] plugin should