--open-chains=X or -c=X, where
X is a positive integer, limits the number of chain
- goals Tamarin will solve during precomputations. In particular,
- this value stops Tamarin from solving any deconstruction chains
- that are longer than the given value X. This is
- useful as some equational theories can cause loops when solving
- deconstruction chains. At the same time, some equational theories
- may need larger values (without looping), in which case it can be
- necessary to increase this value. However, a too small value can
- lead to sources that contain open deconstruction chains which
- would be easy to solve, rendering the precomputations inefficient.
- Tamarin shows a warning on the command line when this limit is
- reached. Default value: 10
X. This is useful as some equational theories can
+ cause loops when solving deconstruction chains. At the same time,
+ some equational theories may need larger values (without looping),
+ in which case it can be necessary to increase this value. However,
+ a too small value can lead to sources that contain open
+ deconstruction chains which would be easy to solve, rendering the
+ precomputations inefficient. Tamarin shows a warning on the
+ command line when this limit is reached. Default value:
+ 10
--saturation=X or --s=X, where
X is a positive integer, limits the number of
saturation steps Tamarin will do during precomputations. In a
diff --git a/develop/book/011_advanced-features.html b/develop/book/011_advanced-features.html
index 81159e9..075852d 100644
--- a/develop/book/011_advanced-features.html
+++ b/develop/book/011_advanced-features.html
@@ -59,16 +59,17 @@
A heuristic describes a method to rank the open goals of a
- constraint system and is specified as a sequence of goal rankings.
- Each goal ranking is abbreviated by a single character from the
- set {s,S,c,C,i,I,o,O}.
A heuristic describes a method to rank the open constraints of
+ a constraint system and is specified as a sequence of proof method
+ rankings. Each proof method ranking is abbreviated by a single
+ character from the set {s,S,c,C,i,I,o,O}.
A global heuristic for a protocol file can be defined using the
- heuristic: statement followed by the sequence of goal
- rankings. The heuristic which is used for a particular lemma can
- be overwritten using the heuristic lemma attribute.
- Finally, the heuristic can be specified using the
- --heuristic command line option.
heuristic: statement followed by the sequence of
+ proof method rankings. The heuristic which is used for a
+ particular lemma can be overwritten using the
+ heuristic lemma attribute. Finally, the heuristic can
+ be specified using the --heuristic command line
+ option.
The precedence of heuristics is:
--heuristic)heuristic:)s)The goal rankings are as follows.
+The proof method rankings are as follows.
s:S:c:C:i:I:{.}:default, the call would be
{default}. The syntax of the tactics will be detailed
@@ -142,39 +145,40 @@ tactic, specifies the name of the tactic and is
mandatory. Then presort (optional) allows the user to
- choose the based ranking of the input. The keywords
+ choose the base ranking of the input. The keywords
prio and deprio defines the ranks of the
- goals. They gather functions that will recognize the goals. The
- higher the prio that recognize a goal, the sooner it will be
- treated and the lower the deprio, the later. The user can choose
- to write as much of prio or deprio as needed. A tactic can also be
- composed of only prio or deprio. The functions are preimplemented
- and allow to reach information unavailable from oracle (the state
- of the system or the proof context).
+ proof methods. They gather functions that will recognize the
+ constraints. The higher the prio that recognizes a constraint, the
+ sooner it will be treated and the lower the deprio, the later. The
+ user can choose to write as much of prio or deprio as needed. A
+ tactic can also be composed of only prio or deprio. The functions
+ are preimplemented and allow to reach information unavailable from
+ oracle (the state of the system or the proof context).
o:o "oracles/oracle-default" to use the
- program oracles/oracle-default as the oracle. If no
- path is specified, the default is oracle. The path of
- the program is relative to the directory of the protocol file
- containing the goal ranking. If the heuristic is specified using
- the --heuristic option, the path can be given using
- the --oraclename command line option. In this case,
- the path is relative to the current working directory. The
- oracle’s input is a numbered list of proof goals, given in the
- ‘Consecutive’ ranking (as generated by the heuristic
- C). Every line of the input is a new goal and starts
- with “%i:”, where %i is the index of the goal. The oracle’s output
- is expected to be a line-separated list of indices, prioritizing
- the given proof goals. Note that it suffices to output the index
- of a single proof goal, as the first ranked goal will always be
- selected. Moreover, the oracle is also allowed to terminate
- without printing a valid index. In this case, the first goal of
- the ‘Consecutive’ ranking will be selected.
+ methods. The path of the program can be specified after the proof
+ method ranking, e.g., o "oracles/oracle-default" to
+ use the program oracles/oracle-default as the oracle.
+ If no path is specified, the default is oracle. The
+ path of the program is relative to the directory of the protocol
+ file containing the proof method ranking. If the heuristic is
+ specified using the --heuristic option, the path can
+ be given using the --oraclename command line option.
+ In this case, the path is relative to the current working
+ directory. The oracle’s input is a numbered list of proof methods,
+ given in the ‘Consecutive’ ranking (as generated by the heuristic
+ C). Every line of the input is a new constraint and
+ starts with “%i:”, where %i is the index of the constraint. The
+ oracle’s output is expected to be a line-separated list of
+ indices, prioritizing the given proof methods. Note that it
+ suffices to output the index of a single proof method, as the
+ first ranked proof method will always be selected. Moreover, the
+ oracle is also allowed to terminate without printing a valid
+ index. In this case, the first proof method of the ‘Consecutive’
+ ranking will be selected.
O:s heuristic, but resolves SAPIC’s
- state-facts right away, as well as Unlock goals, and
- some helper facts introduced in SAPICs translation
- (MID_Receiver, MID_Sender).
- Progress_To goals (which are generated when using the
- optional state-facts right away, as well as Unlock
+ constraints, and some helper facts introduced in SAPICs
+ translation (MID_Receiver, MID_Sender).
+ Progress_To constraints (which are generated when
+ using the optional local
progress) are also prioritised. Similar to fact annotations below, this
@@ -213,8 +217,8 @@ --heuristic=ssC
always uses two times the smart ranking and then once the
- ‘Consecutive’ goal ranking. The idea is that you can mix goal
- rankings easily in this way.
+ ‘Consecutive’ proof method ranking. The idea is that you can mix
+ proof method rankings easily in this way.
Facts can be annotated with + or - to
influence their priority in heuristics. Annotating a fact with
@@ -260,7 +264,7 @@
The tactics are a language native to Tamarin designed to allow - user to write custom rankings of proof goals.
+ user to write custom rankings of proof methods.In order to explain the way a tactic should be written, we will use the simple example (theory SourceOfUniqueness). The first step @@ -274,32 +278,33 @@
tactic: uniqueness
presort: CThen we will start to write the priorities following which we
- want to order the goals. Every priority, announced by the
+ want to order the proof methods. Every priority, announced by the
prio keywords, is composed of functions that will try
- to recognize characteristics in the goals given by the Tamarin
- proofs. If a goal is recognized by a function in a priority, it
- will be be ranked as such, i.e., the higher the priority in the
- tactic, the higher the goals it recognizes will be ranked. The
- particularity recognized by every function will be detailed in a
- paragraph below. The tactic language authorizes to combine
- functions using |, & and
- not. Even if the option is not necessary for the
- proof of the lemma uniqueness, let’s now explore the
- deprio keyword. It works as the prio one
- but with the opposite goal since it allows the user to put the
- recognized goals at the bottom of the ranking. In case several
- deprio are written, the first one will be ranked
- higher than the last ones. If a goal is recognized by two or more
- ‘priorities’ or ‘depriorities’, only the first one (i.e., the
- higher rank possible) will be taken into account for the final
- ranking. The order of the goals recognized by the same priority is
- usually predetermined by the presort. However, if this order is
- not appropriate for one priority, the user can call a ‘postranking
- function’. This function will reorder the goals inside the
- priority given a criteria. If no postranking function is
- determined, Tamarin will use the identity. For now, the only other
- option is smallest, a function that will order the
- goals by increasing size of their pretty-printed strings.
|,
+ & and not. Even if the option is not
+ necessary for the proof of the lemma uniqueness, let’s now explore
+ the deprio keyword. It works as the prio
+ one but with the opposite goal since it allows the user to put the
+ recognized proof methods at the bottom of the ranking. In case
+ several deprio are written, the first one will be
+ ranked higher than the last ones. If a proof method is recognized
+ by two or more ‘priorities’ or ‘depriorities’, only the first one
+ (i.e., the higher rank possible) will be taken into account for
+ the final ranking. The order of the proof methods recognized by
+ the same priority is usually predetermined by the presort.
+ However, if this order is not appropriate for one priority, the
+ user can call a ‘postranking function’. This function will reorder
+ the proof methods inside the priority given a criteria. If no
+ postranking function is determined, Tamarin will use the identity.
+ For now, the only other option is smallest, a
+ function that will order the proof methods by increasing size of
+ their pretty-printed strings.
prio:
isFactName "ReceiverKeySimple"
prio:
@@ -326,9 +331,9 @@ Ranking functions
described here do not suffice for your usage.
Pre-implemented functions * regex: as explain
above, this function takes in parameter a string and will use it
- as a pattern to match against the goals. (Since it is based on the
- Text.Regex.PCRE module of Haskell, some characters, as the
- parenthesis, will need to be escaped to achieve the desired
+ as a pattern to match against the proof methods. (Since it is
+ based on the Text.Regex.PCRE module of Haskell, some characters,
+ as the parenthesis, will need to be escaped to achieve the desired
behavior). * isFactName: as is given by its name,
this function will go look in the Tamarin object ‘goal’ and check
if the field FactName matches its parameter. To give an example of
@@ -339,8 +344,8 @@
Ranking functions
corresponding the parameter can be found. The following functions
are also implemented but specifically designed to translate the
oracles of the Vacarme tool into tactics: *
- dhreNoise: recognize goals containing a
- Diffie-Hellman exponentiation. For example, the goal
+ dhreNoise: recognize constraints containing a
+ Diffie-Hellman exponentiation. For example, the constraint
Recv( <'g'^~e.1,aead(kdf2(<ck, 'g'^(~e*~e.1)>), '0', h(<hash, 'g'^~e.1>), peer),aead(kdf2(<kdf1(<ck, 'g'^(~e*~e.1)>), z>), '0',h(<h(<hash, 'g'^~e.1>),aead(kdf2(<ck, 'g'^(~e*~e.1)>), '0', h(<hash, 'g'^~e.1>), peer)>), payload)>) ▶₁ #claim
is recognized thanks to the presence of the following pattern
'g'^~e.1. The function does need one parameter from
@@ -356,31 +361,33 @@ Ranking functions
Free variables along the variable ~n. In
the case of the example given above, the list would be
[~n,~e,~e.1]. They are the variable that the function
- will try to match against. Once it is done, the tested goal will
- be recognized if it includes an exponentiation that uses the
+ will try to match against. Once it is done, the tested constraint
+ will be recognized if it includes an exponentiation that uses the
previously listed elements (just one as exponent or a
multiplication).
* defaultNoise: this function takes two parameter:
the oracle type (as explained for dhreNoise) and a
regex pattern. The regex pattern should allow the program to
- extract the nonces targeted by the user from the goal. For
+ extract the nonces targeted by the user from the constraint. For
example, in the default case of Vacarme, the regex is
(?<!'g'\^)\~[a-zA-Z.0-9]* and aims at recovering
the nonces used in exponentiation. The goal of the function is to
verify that all the recovered nonces can be found in the list
extracted from the system state as explained for
- dhreNoise. The goal will only be recognized if all
- his nonces are in the list. * reasonableNoncesNoise:
- takes one parameter (same as dhreNoise). It works as
- defaultNoise but works with all the nonces of the
- goal and therefore does not need a regex pattern to retrieve them.
- * nonAbsurdGoal: this function retrieve the functions
- names present in the goal and verifies if they are “Ku” or “inv”
- (this means the key words coming before parenthesis). It also
- retrieves the list of nonces form the system state as explained
- for dhreNoise and checks if they do not appear in the
- goal. If both the conditions are verified, the goal is recognized.
- It only takes one argument (the same as dhreNoise).
+ dhreNoise. The constraint will only be recognized if
+ all his nonces are in the list. *
+ reasonableNoncesNoise: takes one parameter (same as
+ dhreNoise). It works as defaultNoise but
+ works with all the nonces of the constraint and therefore does not
+ need a regex pattern to retrieve them. *
+ nonAbsurdConstraint: this function retrieve the
+ functions names present in the constraint and verifies if they are
+ “Ku” or “inv” (this means the key words coming before
+ parenthesis). It also retrieves the list of nonces form the system
+ state as explained for dhreNoise and checks if they
+ do not appear in the constraint. If both the conditions are
+ verified, the constraint is recognized. It only takes one argument
+ (the same as dhreNoise).
How to write your own
function(s)
The functions need to be added to the
@@ -397,37 +404,38 @@
How to write your own
strings that the user may pass to the function (the pattern for
regex for example). Nothing forbids the user to write as many
parameters as he wants, we will however only use the first ones we
- need. The second parameter is a triplet composed of the goal being
- tested, the proof context and the system. The function then needs
- to return a boolean, True if the goal, proof context
- or system have been recognized, False if not. If
- needed, new postranking functions can be added by doing the
- following steps. First registering the name of the new function in
- the rankingFunctions function in
+ need. The second parameter is a triplet composed of the constraint
+ being tested, the proof context and the system. The function then
+ needs to return a boolean, True if the constraint,
+ proof context or system have been recognized, False
+ if not. If needed, new postranking functions can be added by doing
+ the following steps. First registering the name of the new
+ function in the rankingFunctions function in
lib/theory/src/Theory/Text/Parser/Tactics.hs. Then writing the
- function. It only needs to take in parameters the goals to sort
- and return them in the new order. To be considered, the code then
- needs to be recompiled, using make. The new function
- is then ready to be used.
+ function. It only needs to take in parameters the proof methods to
+ sort and return them in the new order. To be considered, the code
+ then needs to be recompiled, using make. The new
+ function is then ready to be used.
Using an Oracle
Oracles allow to implement user-defined heuristics as custom
- rankings of proof goals. They are invoked as a process with the
+ rankings of proof methods. They are invoked as a process with the
lemma under scrutiny as the first argument and all current proof
- goals seperated by EOL over stdin. Proof goals match the regex
- (\d+):(.+) where (\d+) is the goal’s
- index, and (.+) is the actual goal. A proof goal is
- formatted like one of the applicable proof methods shown in the
- interactive view, but without solve(…)
+ methods seperated by EOL over stdin. Proof methods match the regex
+ (\d+):(.+) where (\d+) is the method’s
+ index, and (.+) is the actual constraint. A proof
+ method is formatted like one of the applicable proof methods shown
+ in the interactive view, but without solve(…)
surrounding it. One can also observe the input to the oracle in
the stdout of tamarin itself. Oracle calls are logged between
START INPUT, START OUTPUT, and
END Oracle call.
- The oracle can set the new order of proof goals by writing the
- proof indices to stdout, separated by EOL. The order of the
- indices determines the new order of proof goals. An oracle does
- not need to rank all goals. Unranked goals will be ranked with
- lower priority than ranked goals but kept in order. For example,
- if an oracle was given the goals 1-4, and would output:
+ The oracle can set the new order of proof methods by writing
+ the proof indices to stdout, separated by EOL. The order of the
+ indices determines the new order of proof methods. An oracle does
+ not need to rank all proof methods. Unranked proof methods will be
+ ranked with lower priority than ranked proof methods but kept in
+ order. For example, if an oracle was given the proof methods 1-4,
+ and would output:
4
2
the new ranking would be 4, 2, 1, 3. In particular, this
@@ -518,15 +526,15 @@
Using an Oracle
The generated proof consists of only 10 steps. (162 steps with
‘consecutive’ ranking, non-termination with ‘smart’ ranking).
Sometimes, one makes mistakes when writing an oracle or forgets
- to address a case in which the oracle would need to rank a goal
- for termination. For example in the oracle above, it could happen
- that none of the three checks apply to any of the goals and the
- oracle prints nothing. To help debugging oracles, the interactive
- mode of Tamarin provides an autoprove option that stops proving
- whenever the oracle ranks no goals (it is called
- o. autoprove until oracle returns nothing). This way,
- you can easily find and inspect the cases in which you might need
- to refine your oracle.
+ to address a case in which the oracle would need to rank a proof
+ method for termination. For example in the oracle above, it could
+ happen that none of the three checks apply to any of the proof
+ method and the oracle prints nothing. To help debugging oracles,
+ the interactive mode of Tamarin provides an autoprove option that
+ stops proving whenever the oracle ranks no proof methods (it is
+ called o. autoprove until oracle returns nothing).
+ This way, you can easily find and inspect the cases in which you
+ might need to refine your oracle.
S&`-zC@JCcZli3gthvSeTM4w`<)*>5doF9}KBIE2=o4Qf%%L>Qg|WypE!s
z%fjnKldcdisi8Ta^$e<>f(1A2x6@5hW7%_8;>zPDYE_8OJw<#P=H$68uXM3$@Z!B>
zd3%aFb}{}7jMr;qG+O=>xHp>|kQ~cv*2PgWoH&n5_y@q>oH8JeGx$Y2)eS=<9VJYj
zRa{%TRijTw8q=xW+wLdtWc+S*z1!lMkN6-5fqQRoGIXS6X^B_Q*^HRO>|clZ^cH4K
z;hY9l(3`hCG_nOEb_kR?2sdGnYvd}U&G(G4j6Q!Kk-63SCsmnHU^A$l!ZHG1@o*}9FE<#%|%Fq~&)
zR%M5<<%`Be#BRWK>HWnu`>EUFGiKU3>Zx1AgvEik=3fvU7i5-UAi1{F86-4P(yGcE
zd^0_gUB${lg1`31ic!}rlcDywHO6tOga>`d+eo+GMF;EHcQkR=4(iPEj$xFf@#S{x
z(n0<-6B9aVw~L4(Hn~AbtGZn#OwN1?>(xIqd7zs1Q+f5t0$G+_OP!d1HWGUH4TO9s
zp+Eo}P4L56MpmkSBPv{2k|0g|Oa@g%ADGj;QnufDf2b`u{UemKdsuh3K$%I+X%=Hn
z_quYB(wOW%-WN)fH&4xh9(%cI#1e|}qN^g0*leMtA69#a5jEKJt%UYNt2Evvvz_uI
zUB8iiSeleE-)9NSkS1rKtH{K5T)Bv!${q(4Ly{`(X&(4sqkFUFmq#et^xa7Us;hN7
zw37d-+3_@L%OQxGEfxjIdd*v%frndAF`D!xNY59KmOZIwXq&4ad9@B=7~q-x-MgZe
z5|1;URx(Tmcc<$-xDhqZK4BtLL3|ZB>~>`)*F1k{Le1MSUYuPtFI$wV7xy3gJ1Pql
z{?iGjV}nPPc(Axb64x5K~;zL?+KMxP*jPEuj5IS)?|^&1lC%w&}TtTsT{}KjD6rJCW&#yYY|UseJ!m1c@Ps0ytFL
z=gcw;pTPYqkA_!^7z1kXGO`Rd*ha=A?J|`8k!#rtG&TO(_yHW-MWa9aQn&!1Kg0W$
zs&$dyp}eYwSVKs#lth&g;D%CWN?)x_?HFWR)@r)7e7rPS%(h7=QIjb|r4@?Q%dKhl
zJPF^tsbg_I4rI$S#ib**}#@cO~QCblCGR
zgG@bQm+M1A=$SSe4K1X2s{Jx=di6r4Jzj){zGgCmf#z!xe71bDkzq7aan#&A+0tPO
zA`>MgHHGKQ!t$ZBTy#X3VQ?Stsc33z#8^+|
z<+#9sc)?f>?5qrMr
z{$zqA7%KE09Jt+hXZ+q9$=_9IIN=%=L0mg?k|4)?^~3BZUnL7w_`r3Nq(`(;{`F-h
zvKS)@jNXa;+FZ0LNYxM!mc9}oAi!#=o8R2D{XBJ}0lhKhCt1xJu*`%WJsty?QkAb*
z&(nqfQUsajXoBXvWz~^Q_3XCrbZ5$2dz4=XnO42%=@!Sq&w2~
z0KtQGL#M{J>7boChN9l{BrE@&(CKf04n
zegNLtuHv@v5KDT*LjJj>1U-J6!|KY$Gz6Sk+mPMshX>-Cd;L{5MCfaSIOfB@x4HN|
zmzpo*GSwcR@8g;g^5i_aPk`p1uW*{SuNoTN(u2CyXM_f1v8GzW-K$IecFzxPYfK@yWf$w+niTz6-k
zV4_iqNeT1iM)Bij8|5SK@jtsZ{R4Qo`4D_7(SOR>UZ1Y{xce{F`TlUF1?)4xU4%W6@V0a+qOj>_=*)>exzTF*0Z+i^@&wnp`CLo5B
zSZt|=_~S68I@N6Nc-)kvrVRw_7*9UtyQAu%4{6WVS&uM0hZeHCJg+)iI@cnK)D4^t
zSVuONACH3dbeM2~XI(QI>qI?MoEvv+f;{;=!q!L2-7R9-z5WITMNhi^Jy!Xw@m}H$
z3=gr`zvNwb?CuA^w_js+y1shMflO!k;p?_31m+`l?o>J
zS1b^w`;zMSM3jr3!n?}7&%HTLVkQQECAouQkhBcBbW0lmv8Dm<#x$Ntsp%kXC7T$S
zn39n>t?WGoX`sPwnU?Bl@?unE_3xIJC1)$SRPPF(Ee3_JjA{{ggZyqXG)TdhR?#vA
z!+Kmo_K4=pFX{<<{e=N8X8vsm+3+}$lA0GUAZ{a*LtDimA+)Zczg_cHd;AQP_O=5}
zobP48G?Wb3@n`q8h>%Upk9-FP-*RQQoMQqjf9;)i8>#%k`_sufnjs)TdWMd6+jnIn
zC`1xE$J-}AyMGD8=R_>T0sYB`g92oKl*%!DOFKUI60oT}A?d^}^j5^|e#
zxyL^D!32xk+H_flT|3I<+!{puh;$Tx*;HE6Lb&KBMb%FpO@#E(a)zCI!f^J
z`Akm$mZq+{1^8Pt?&Uj@|HKbuHz{a$K?&_Q(>D6i$=?&|lxa1yII?d^v}AZ?ztb1?
z;He{K6Hkjy_6r0GLj-)I!@Uuu`Ch)(w1s7%c}2iS5s4s0mHM%Ug0-tZ`r{dCSz(TU
z>7t#ArHR)Wp;}keXQOrwzZL&CgL~*18K>(CuGKw(2jTxY|{#iLl)-gvbb-L;gR
z3nTM(lfBD?W<6x1ev4_n*~y`*)Yt7?ac9;ravMf}lR{pYmz_K8Q(C@Z(h+=|aU9gV
z{SvccvdSn-v%Zk@+(2X^asfRp9Q^bclpgzN*0_uf`Cf|gcHt4w+OP3*XN5J20N
z4ji_WA;NSs;v@1Lhye=wEpxseO_;3{NRoAm{xe+@=)QW;Vm*Jmoe*U?T;0T0N8^3RG_kvIJ5q
zPeR@76_{`qzEI7ot;7m}j@{JS$tYS2@6+ktP$Fb&)l4&2hCI7p{)40HO^6_VU|7bV
z`mWAc#a?25j7o5?s`+|oXOy&dYZYQQUKoo+0LGP2#uB%Q@W#xCr*)g?Q|VKYJ%*L*
z7fK~Nx=~#Nl_IAJj*IC9=0LdBMC=}dgX-LQITq{yJ=EGU=Y(^wKsnqR)I?j|*a|0-
zjSxcrdfhNo@k1~w%Zjb4f85_Kz-_5rxX?r5cc=pKu>bvGeMS~Ig=J5p2g4ACnIOb&
zoJ$q4T1W2N#1lGM!P6v*$rB?wJEC;L!KFxyXZ%AgJ&
zSf-}FY}jx&jCT{T#UmEzKT{LsjTGR0XJuW(!ELTeph_fMk$Y{41|@@0fZsJQT5fo^
zYT7}iQ8)#)_<4VNdSwJZ)n*v{8ncejO?X@xBrUYBh_o^pSJ+Lg)h6-qtqFM(6oFt?
zX-vz>*7RG}!t*NzmGZ^rA2~bO=jI?=--hPz#l}*Yhl$gssvZ->f4NQd
zn)ay%P9uKk=S?*??#`mfK#MbaWDpAoGQ76Khgq(B1qH7Hrq9RQVz1Rn%{SWPUvIqN647`9DY->|7hsud`qvoN(E!sH-T$su
z_BTya4il{(I3^g%-pvaYQ7%S241RBAi7`
z2#GIQ53#hbkQzFYtpbk4{|~~95ezO#{(&Wll%llTl!%4i4Hbv5*dhi283akYr9TAa
zvcb(bqh_}iB#4ItsPJZq@_ta{l&-Z8QAK3yOvjuWx>6F~NM|cKFDR$W07tyR10TM(qU%MHuv4BvI4Jn+o5Rs6Q1VxvEKk<&PwoWPrFZ`*$K`YkTQ;PqMIoxzABU%R#wF&0>#{7>6^A+Cd
z@OUc;%bv;duPzcqEyzOIci7#i4lQ0cr&JaeVX2%!za2?nvL$bd%uskj?I+@Q<&5Jy
z@}G;>(Cq7tbNTw%r$nyMrzr!o{1NQ0ab4Ka;;)_n4dkDzz)1;3=KuaA@si7yTcag=
zF~^bjtQM3*-!Km+X_diBNkSp4UoW78CcVK4BfXB*1Qn-set@_v8446rrCuMbs*z$3
z9;L5D9)D__yDQ=LbDIVt{LP5&rJ<7RKBay)>vG1tEx`B4N7tbUK!$(TmDFPL>L<2p
zc25S{y{pv;Cu#Sa-q@w**zX#I6mtM}xjh$BQ#Ko9
z>C9tf3`Y7eQ<;QfB1~5?2=y1yaMi#CR^^M-{qNyug-T!PDRERVEM=D}F|@P;$1{N_3k%!sq1urISWvo}YaAe(FFGz*ye
zVU_2nq@ycY{#;V9Z>HC>67UBWAg~hh1UZb
zQfN>J=_o^q$p>=|)(2$C-t6%|kX;Qw|JeB6TGTd8{MGAUUpl4BV^1{|@r(nhgkmNB
z2=HM9FGZaoWXJQ$+1*gmQ<|ts_of2t5}^9Un8nS;98(JEvLa>AF76sV(N|3}7+ek;
zxkO$T@3rB&;-ch#`Ny(^2mZY_2|OGyddO|^f{)k=c(hcS`Svw7Uv&E4fqQ0tkM&Y(Sf4DWTR%a8NOH&8{6ExQK%PAHwrdHV>mhiy-Dyhcd;myczoG*UAY+qMn0^
z`J!`QEo-ri`P9xG(i{FKkaRX}ZKK+1p}m1dQC_F(lr)$>+g$1p>B<`~YZmHL)i6C(
zTko|*;?zGL9Pdb3VTCZYg@O`bSE@+UK9Pnw7Obr^@jK(4tY4G635CKziN&^k3ECer
zRb2K!`y|Suk>q{tNgY-aY#g>{K?`ZakV{+=#V6?Nw4?ZH6Q@POd7}r7)9Bgp1fT0N
z_tYJVn0BZUr6BKaJ+M-*WS`q=D=U!P0h8LHeCFC-(+)`|$so|(tZ4QO;K*~){
zs#izHfv43D#$p63j4#)8b;Cd7@KmD`C&82@eBh_UB1`AUn!|Nm?J9hUjO*IkipcbW}c62wa>9F+(;g`NLZ&V$V32EF&NzGGY
z%Sv@kfi~MXa+UZ>^A)YthWlsAi>~To%D7qd5dwx*Gfb9E>Fa<$>-k>3N*rj#g_2KH
zyl^~OognZ&7`24Kh(Ak8-?>F(8#+XMrg>+|6YoD|m~``5#mABrSdJ;;AIK@9sw&~X
z@~2YYl(*7NOKXz}Pxz;9u+$n?*9>?`1Fvc)U`{>gI>W714-QVVgygeo9`-5w
zeH7`@j^=jf!rQZZhvy?#e%sgJL+wisk;Z!II{E@g|?BB@nR)nn_UyK?+2czqtxG~h|1{8
z2lsrvqI2i$-|~)<0F_e1pvw;g
zk%)(^_G3IAq6aWq62o5oEosc;3e(f>vCzlUP5XEth~vfbAn5hC`qPea`>R^MXR!yk
z*|xiQNvRpn`7+uw-G1DkJ2-Qw(}sP#MdMWddTIaqu!`!!1NJ^&PNY7vh;x>-eDS)^
zdas7vBQXRz-CPE#JdN#gpt6
z(FUhq*cIO@z4sZ8%Zvm
zYRGaIyQ5$wAg{+lP`CQZkwBKWyGs7wnD>&d(J^ly=+mpD$U$|U$mQO7cj`23qruU(uU7s`YO&|l}3L&9)PS&$EriGz#Xxm~=#_K@28_k_|rr3+@rHx*3a$b)eVlJuGtKx9OJPP{st;Vhxd
zkE#9+I@t&#_=;2X>3Zdtu)sNn<+cs2}@xt9Pkb&0stq)ST?@bSCDK8`WP(O^#>os~F79NN9T_
z28em|VPST|A)2kz4H3i%u4!xqLjOWDCjgO~8p2#iIL+R0or#3E*jz%gH0MxSwyu^R
z-bSs}2Y$JYQ9qENnoGKs?B~IAkl(7+M`%#W?v%X>PMQ~~AF7T%9DvzsiP%n)7@Y3R
zf)mYgG3Sb=Nl9S~ti!7%5cbG29^``aM<12n9Nd(xN1DSh?Rt`y^F3h_J(v`=Es(1t
znOct)uSM&|>;mkK(jFWzyk0`sN`h>P_c
zf}|MRpZD1;o%trQ^gR};xr(IU%!nWl>tA&1U0`leS)QnhW3s;pw1
zF)qs%PU|TsnB9YHb9O@ST@SPqoDD8PA3yhPZkwyb|1mSHCNH62Ep?430Gui~sZFJw
z_&ncOe=P$#pe*Cj+v;-_VTxi7MO#fjE}!ZvH|r{0!#qa$_`&&aOHx<}A&0Kt?pT_`
zuqldQ(KErPc>Wc&-R~W@@+_vwZr)#ac$K$o_7t^z_|aPCDZ$V6qE*x(PVv5CWC8iM
zYWZ8=CliPYSurpRyev`2fdCqrP)NLXe~86EoPX4WGE18*`JQJM+T;a9n}ocdu#-mc
zoBevlRygTJGtl>MaNwnOji^X6ICw70Ebnf$@DyJgAw=4vFDo%Fa-8uWJe`H>niW|1
zV7`itZG=aB+4J)pg%ezfnXZJHY1m=3x_$Ka^YXJu#yw6Z;wC``zzt)^aVEF3b{Z6(
zaz|aO63e`RQ>eyitH4iQfq>l1KfxeQ^ITf0#X>S-FZsU*_Q_(YZP{XMd4Uv2;-tmn
zgsgJ72PtxnoR%&M-!JpAj!a(beRfc)!@K>B1P_NzVjGY~6}U50xy#2cEs9c~mS0XJ
z?lj*r(Haa(Hym%>fLND+d2g1nL5H_Or|SD6lqa}Vd*yZWaS5i4;`6MWU+SwxdElAb
zm@kEQqR$nI?lMp0tH-d>@+D|I>uoV5oIhhI(H0Nj#Ji#Hy4l;+CwGM@IL-D;HZZS5Rua(QoRf2B=r9`GH|-Y_`IMQHYMXA}W_aV+V{0N*GC21>R^T?eUBCtUKX;ehY(BfCM3mhX#o8eJ4p_
zoXp|Nt5#^{fEwqI_*@&C5&8*b#mTK>hBf&%n
zwy+_SPv6y`J`U#D4nir+HStB958h7~9RjUnk-e4ZZ6^JKu|IB#tdqlW6k+5#(
zw(y8PbZuLE7ZyZN)_ciXZ9)J1)pBPk{TkAUZ_E+Ko@rrU)qu?G;vnK!W<;bVtR3cL
zum6Jth>n7}|D~b1M;4U9~9%(r!moeGxJ>R@NJUs&8Aat&YT9C0g&?&>=5fwdT@@4m1HKx{ssplI;
zdUY6E&$g4Q?cLkws*rtq!9MJ&z0a4pkjwT3U^~#v3%$g*;A4(W{41fVp%eDLdKoWE
z%dxS?TXRqK9dj$-L@JKSDz3zy`W(A+^ojE$guFA64+zjN1H<4vDv9XFnl&{DgS>_j
z!S}6jNKt%dMCq!CS%bmK$YzIdAHwfUb))hzcp0ly3}pJ+I_P#eEFix3`{|;F<}bO?WY_{^KgpYc(*b6(Vz3X
z^FLA0_5s(CQtNx?Dfz~B_04f$Ch1
zHGH0lIT*jq8>ZP8L-QmiqHfKAAP}Yoww#^Sqn$^%*50lyJ<8C?HRITBF8nEaWreqi
zs4YNEiDwDl)3ucT_y(7rxHyWBZ5kAt%F*Bsg?-1|Yg7T!=h>8?k
z5k`)Y!(RK%MXnvzF>sN~kWYiXH=Y2@b)&MQz@kG<>lo>0qc5VNozh(0lg(4+uwm@b
zH-Cv)e9rM7HtwcRny1BhGRR0lrrAKi0lbD}0HHOU00ekO8Uo|;*;toA`M0u!
z-ScQ{frB>wM`AWI0eLjlLI7}1xRj)*340f}*qD35e;8j%}8Rlm?!%a7q0avDBKEg6CI0t5K7MHsH310^t
z5eE!<6sp54@Ruiehv{!t9001oj>;Bvo0@$oxdZ=rJ79nOzI9sAy4yjue}AX%ozv8A
z_bFk2;Ez{{s`(GYmg4tW^?IMvq`Y_YC$PrYD$yoYOclx6Xfk;@pVkGdEM_0H#q8_
zcPUt7UzfKRPq+8lFCU>m&&l1k03-0RSTf#yj(2;o=Wrt(_30=ZNe6gud_5cjnLXSv
z+uMe8z;vwJ6+hFk-N8_aQ{P^QHLSu`kPO}DWB1}wXOjME8gXOx$6Jr!r{0U_0OxD%
zAZDb>ARE|+18s}B5E5$q782zTf3txouPum7*
zMSOM3mQwZJO{RO5oXVtrmBLR^XIN+~TAG$8(0~Wcq?3kNIi9|duuW%v`(-s6oNpPQ
zKL*`sJVex}{Ck8K{!9Vl+iAo|ZSJ*DmhHVc#-qF3xeAv_-t6NmP3!|8*UUs$S&2l@
zlM)9}LzcpS*NQ>X%A)_vcg*Oc-L=3+_&1nI@T)Yz7hZ%jaZJeQN&d#q!@ty4}L@RsvTWsg;G%bPv*&e
zKZqPYTxyo>p;bQeN&60X{=kZz!jvi6Z{<=%4J-*;%plex-PU3?RD
z315H)_cGSvGW!cNwcW)ZT)}|z6prY@M-yeixg!M^ozCZ
zaLIgi-~wdd%vOk{R=0%4yf5VUEk_aZyB$z5{wOjx&1QgzoQ=y&l@%ci`6?yKc!rZF
zHnn+#cl(LVuvVhXvK|X0PsR;8JdayvQNfWI^hx|AIZPPfb(llceofG_L;_hH0
zPpi(e{|0i#QwzMJNKwVZiy$0?coo`-qOXOk9(XFy_b16Y$_~9lnMul}UI3n0_&v~F
zrA^sHAe}$}Fa9rIy%hqwcy{bC?}wzPojQ5-`d{ocB|ga!Ez|l-tNiBrZE9oWlkR*l
zO}d`%y588p@5_U9H4)F)h@rI-WX6J*Lwm_klBXlf4ohQZfLM2sNbM3u-+iJ!=PnhLc
z|0yM3quvPkLCCU3jE86bG@3oU8$4~4{SSEsAm8+AF9e}B*E9RcBWO26W#7`y8g6URcsSX#JYLGaZNv*n6~R&N-?q#fz%<#x~gV{
zydwc-sn@m`PN``G@0`HR`G}L}hYfd23Mnvr=5PaMo}0E7R!O>Mdvw{Xx!#$yQkhX<
zg8IfeTG0wW&|mAg}ga;~c5f89aW-QX{uWRU(;(p!8ucCB8)H74&A8D_H@<
z>8}OR*A#1$O`*(?Tyom|?M!%(dA@cyT>YIoBOQ^c(ccJtc;GcJj252l8nuieZTFzy
z=Tp0s=G_Hm(jj;6)~y-he(dKZaqJmW#|EoZB=T|?uaTwkmkX&-plCwrUBI(cK{8~i
ziOz>7<&%0I1|N8)C`B2k_-Ns&uAKwo9Bet4n_RHMN&@Hegb)ZN>O$ojTWn(&_c6Q-
zYK+9!)~}ZD_(#vGq@ILk))Q9O%vD;v^AXtJylFpeTZqjgC1oA`Ii8`+?93srk0Y`~
z5H>4jsagJMPFYnrIdE7xo^ZM1-e}56Bik4-4yYh0E@znAfBnv+ArFnbp~34itKQRgpQo}xSShYB|Yo_+5cNa(+b28U#G}ch$4qiSBe(tS2BrNWTK;pv(
z!787Psi(9VnA30U`BMIZ$lPKXfK||btL`7;+hwlcwM;Y?G%&a;B&oI6<#$Iqq3B`!
zW@u4=X1+I6Cp&6~GZ>mvM{)=_Qf*^!^f_R$&vg#%CS6qKNSUl;zb-VnoYH4aX5do@
z2gi^#ff`XT*?!Ozk@DW1K$rM=_*l2*
zieYJ2o~|~#U|~xViLf{V$^VU+Y#xv9#2E;2qb2NG^%Y8Z5thyK{U(WYdt_>pn|eHb
zMpGes(ku@fckYZ{z$6;iu(71B
z(`IAmDsC~;lQ-+gGG1!0jq=>2j49c79zA8qyJWLnQ8xTthvE*?#pz~
zI|`1aWa9sdCOOmpO6)mU{tshRh5I+=ob7r_eII7c-HpEK&<|36H-wFI&|jwKaM1s&
zXU9?1BQjAA;a+b6W2EV->Aj&;tQfF@kxQN0xXHyl|b*D@&%
z2%-;KUBO-*L%;9hq;x-rVag22&14flsIsUL(<1J{#IWX|0bt0j0aVZNZoSy|U(;|v
zXJ41NHo2QXQc}AwHllLZKn8~dx3UapKxKV8Lxv_JXOXCLOw{PHkIA0*ang+Gtt8g4
z1v;*rUtQeb96|X2E@{rU$}F0d`yI%^J@
zGn61r{=Tzh3L<~Y$G<+AlS2y04~k#SH~QI+!KrzSuCUr~vcr+Ra+C@%7kmPqS%z7d
z!_Pr7v}k`U8{Ta)x>yT;c<16B
zJ+rOcZrg{D7LDIWpS249gs@QQEmB+e
z0$nw;5m3yX0RqhdMf9G3!2^M*#QI=oXSt!k)(OB?ro
z%RHm&dJa`o)W<&qI+a!fyVWP!+C#hR6>=0W{VO*Zi|6QnDp#PoR;t3TyNJGQbqtZ@
zO>Lmr*<%H7uYo;?Ww@s=(ml7=6K>3Krf0Dy$joV$@3X%-^r%pi+=u!?!ZiCkTVzJ!
zv$VF8oxQ~bO*T-ecAx?FWIjD>m6I4L@$K?Dx^sdOIy}`Q;nFV+gGKN34rP|RN=*M1
z1X?>*k=59Av5YjVQLrvjuwqT2uY$4N4Wp@2Kw_jZkMXty#ET!7E70qKCh6!p5l6Tg
z=dDIq_$0m60k)?9w)RNGtZIg--MK@evNvdpk+pmbI@8c+bFu&(nEwJ5x&lvQa!5{p
zT={$tjT#)F1DSqkyFXpbQtWwfx0_5M|4M<-%dFCH6x4!_s1mC}A!2XH(%7tfxuh4J
z$)v9cbPAss5M>uO2GB35kpiYgy70t3>z%Jc%=a;@IkWAv#52nLh
zjk6L>f6nv5Mot1BaUo<=!^LlNDrnEHc$a+2)|-X%4ogsJa|_(rjv1zV-`l3%s;4t6
zb${KN?PyGBcuY;4;?4c4f}CGlXE8ZnmC@bJDB1DO0x@K^IXlY+q;-0OfG6y>h4f~r&H4V7n
zrFpO4Ei<5oqO~jS_N#R8DvXZ~RV-0fxMVfEDv4HEMzPCU#}_|mByj6IvG$M3pufIU
ztM=XhzS;xMFYE<-@17cc+KOD~(+%rw5qKVv--eD2^DniH*VAs5*sENvu?wlPw<^V9
ze2k&aQlP^-lf{0T?U$GbyQ0SpM4mRGDP~<+ep`3jsGs!>VGvxM-WPft{KeYniEaGE
z8=tk>0To?j*!1vQ$eg@wr9dpYF8UacmP-7wGwi$Zw|z9_q0M4rZNu{ILyFuL5ENi8
zZ-dJQdaKDYXh1JzTQ924
z4KUuhL!$I1S~@e;
z;PaheDwxzWx*g)T>@2q2zkgOW`cvbHZt?O13HKf40Xre9zF|!d+RKSe1=TMh$;Ggr
zX2}AER_rx=n7P%g9`Gx{iw+eEno>doU6AZP=Kmj8=iuE}6lU$DNn_i#8k>!6H@0ou
zSdHy8<}bFDpR<2;9L}o$Ds|N(6`1PxS!s
z(GCk8Ha1;cXB`Fh)OfVE4YB-EiL&*;MPSX}2%(7=bY?cGBB=t+E|Z3|x64_Y3~6qB|k6C~MBrWbvr7QK~g?
zYjYVToh3zz(NwLkqRMtE{p-2UV9Nwpuv6j!KdL_?n=(q}+vihZn26}M5yympgtw`_
zM(U0xqgof*L7(6G3?g4kjuYq`m>XF4U}Q~8Fsx`%X$V2E%Bzrwwc90vvu<*xq6A;m
z1V2zP&R%hRuq35(efgunR#56##aR0b5|u0W^y?+c+jdIM)7~D^*m>oX*b#wA$UW>s
zaPSMI-Tu;2wvN4!&5nc0$W$;3s8K$
z2ozV$lP4TO{@9~72%LB|yagFq{;H6>Yzy>wA<_0G5Ml7Byy~3en5ww;(~PJ}XI3{p
z%CblLtv_pRQ0Kl;u2^#I)5`&CVO3~N%Aaj?gdX)}c~
zRgB3L2T{XRgXnF`wn~~SN^Jc*B`o>)UM0ltUG?-fMp-g4#7*mvp5YgfFWR%3l|!j6
z0y2Rnq0ZpA(Y&c&t>NcMmDo#R1Y~-e;~OXA2}FCPgu!ctioqAz;k^O5!rj6sv`Tgf
zk%pCd=43{}KlPQw=dH%B~h=H;SNiRZhP24spFKzf?-GRV};`4zb
z8{wmdDf?6#ROQXorFXYlEkkU`F(el
z+z@z-BKbiZ+UI1AEn@QdQM3f!ss1_;Qgn56p-+fB>G+YKB_d$;i*vSl*_SMYkFh4f
z#O#7wnT6RK@d|-p|H#I@w@gwmb5y*sd&laL|1YMT6?^$giC3H8m3w;Un#O@N?Y;YK
z0)c4MHxg`r=NU9QxLMueu6
zNt3=vIc;j#fs2+=>i9whczL>hJ?y!GUCa9qCYsZ%{S$dk{68d`E8RaNT8BFv>D#VL
zL9fTvKZ@AVxVlXO66^GpQVyin?Bp2J`zs|0MNAO-WG%lki`3FECVvs;CkYYZ%}Ax3kjvJ?
z?xyQd2pP6-0UIGju#*j3)^iHRgVCY_SjiOpeYUI706&@h!wh;-$a
z5EZ98ADeIkR+f}Odt^li<->2V_C|&KlAdb?e!*|BiM1aPHsMP$TR@|T_$3hmCL6I5
z-eK8>qF_$a5N(RUF%axt@W>Sti{QPuv5GNfoL+(|KVl
zDJJ1=9^cYG^COL}cfGO?a4t0P~&O3$K@7e#r9
zt$j{xaphoxX*N{
zIb>%@#VkQQ?jS{S0m}O8TWnb-ZD4f&ih$}^Z8T?=SY5OSNi?EpAFEh$e!o_EA9ud*
zEshIy?#!e$1-xmc#F}_n>B4n2HatkJ~OtD!V=l6^c(2cyp+%jawl*b
zMTm)Msaqvo&{Tj!XqNuF`X^N#R^Rd*FG%XxZT3?!Tri`$;t(0Nj60o!5>8nlO>-U;
zCbb9WH~PEY8u4AJ!#M%B4#keAA+BWnDVfd)w4PyGoMdWfSSlM5-TEl_gY+_6)a>@R
zZwv$Q*M7IPk^YY;{aAd0PhiX!+CP0bfnd1Sec$Fxng~=@D0nj(vn`l0u
z)M2jpyP$O3u!VELWxt27g=%NnL1N56guGqDqy!6WG!eYz0S7W@WC;V%>N58j6$%w4D2DaEMn0Y@{zzkaWGrvXq8qwA^S1S5X+g>5GVjq!f$v>_jja;uk6v^RW~@MjgnWWFw(|`QxChQAOUPr}
ziO!o+XUbqVk{_*dnv
zYv!t%@`AyC_sIA?Rm2#u91=9U~mR$dZG4xCy3dhY5P2yx@aa?2y
zE^@5P^bg*S0K*gS$$=Xg&q>}6a0$bUgGxYfrH#I`AVuw)bHbbJIC7AL-(oR-<`*EU
z9b3tVI(?a=zGk*h?I`E3TAV2bccCpIpj)L9W0PLfh0plblM(RD$ddf
zCTy1pQJaW$d!v`$4iO1ver<(Z*)Ew(yc6~JsBl~($|JcJQQZvkWU{MqNw#F*fU|3^
zf_m+u0qgsZF8@4!z@RqOP!p(`e*{GyseO(-L&Wm0rQC}q1W)SKUfrJ)ynF$
zuE-l5w9m^(n_R6c53hJ6CNJ9@s0e!ug6GEELXkQ?B+iTIGM`L%kuqQNdhR)$?_l)>
z+a%|usRg3G)^yVlJY5P}?e%h_~ghp|7*ozXc(U7Cklbu7%6)PnCWv(zaccUBz7
z204PC3W_}?r!~IsI=R3L_rG3p_tI7|hqvQhr`exPFRt!CWrTv%t#;fm-d2I7KN#nv(}(F>om=*
z0Qw*84X`FYhw4%dE>=Q=y9bkxt@Oa=DfE=vhxg(b?K%w_3dflPrU7Q`QiKIw8_R{~
zrOD7kpX2EVjG_jah7|2&7<5hJ^U49CWRX_~@1yBE;>nO195Trs?7eD#eS>Ei9qxeAby9ZA
z0~Cjp_!+CjCD_l3(2<6sVf3J+c3$*xG1KO`AnUJo4!A$M0}7DxlA9K}Id2vyU)={62%^XmL=)WK=o`OG{OI
zk_Mu)s$A!!J}2P~!XUB)40{o9n=UCu1kdXW8?2b|mXv2fUE&>gP?G!2s*=Xn5NZ~p
zxp!X2}n5be(Rp
zy8rlgR?Q4TGrXIGrx!De)p>)wp;S%vNV_Q+TuCD1#uprjz}o~0P95y!q*cn
zv?Qg+!&&mSM#{}oPZWul^In^;zjL(uVPWg$LeaQO1f+cv0_dx+l8q*
zwpyU@UEz&+T8@sGh|tSWj|mKypy|Vi^Gf1+QQ>fHR`JMhum4G&&%HCvRI+q8?;YN`
z#J-0jV1--xvz-%ws#l!)X(Xk@BWJDK?LZ2fL7}3451L~gHP52qbCS`9*U14A8-EYJ
zW;Vi{(C$rq57)t%AN|1~?;-DnepdW_#pCyK8I+J4i)gu~I{CK?V;5+O@vv5sVkv@w
zp9u1huq#k3r~xs^b?qqxNt*(?aNWS)|6M)Cc?%z@f%CX<9_s$DWDx!CE{
zb(NiPH@&6gq)#J)$G9WeLC*Oh5guVu%UMe4fCF)aqP&$hd^H41ppDXjoAGNBr12O9
zyrxG|%Aez@Lo;sZ-_6?@t1>q$bWd>Ft{x=7X;;J{JN$S*8XTrY^Li|)dOOFl?@-b>
z`*QO6WikqY`v9u^HA$tOHa39cb;%KZuWh$Fye2v@fNN4WVB;?H{)Xihi^?>$Q6(rN
z6_}_MY2`NM;ZbfS9c*Wq7QyN$%!7(tQ5F)Ovrqs`*x86wRbM48Rh%$3pNe}#B~2yk
zO}#jW;P=7K))#4*IX7l$6g$~#7h-NLJ$&d4DND-`E_O}gM2-kl|N53?$mPc9#8MF!
zH96ljPT0O0o}hfHySQEEFcEpcfByH_%C1)_%M`t_>u%qDv{*No3L%P@87gj-i;>no
zzU?niMhCL9+PZ%K>izOV_lfs+qd;5O)9eR#Lo=g<$2SK)@?SY?Fl~&V#^|`7?GY>p
zxYHUhb1zN6i1CVfqIAc53qEkQ
z*G`gjSi-@p?zq~ih%~iS5W-k;uL`6)7^eh)G2!T{t(O&MI$&w(UF`IM!6(RUX=j
z+iS9J+97MhNF8FLcp>e~A`^l!6*z6yAbz!D$)h*^hth38@NYP)P<6v43n?>XQ9z@^6w#`_wxd+yfpG
zNj|yKYCaDPdJd+5r(2u%_s6O6tq-enGu>vG>zn7!R=2tt{c0nYO?^S)o{eZ&z)-I9
zpL=nc_esYWw3%>LpXp2m3KP0PGKu~idY;FgNgU&d-^A7A+Qy_*(n
zPD3xo*?3)R^zeIAa}*p-hC*8-;ej^
zl#NGZDXwCLPw~GNPgbU?&+5qxQna
zjy?Agx$IsRSiNAt66j|+gUd?gqbd521#0&;imymm7GT7+IYufBkt~~28|cjh1osK(
z9g$1Db^VsO_LxQYQzUx#?{|_LZ>EiPiFj6eqX&1A*`XlHzWm-f6S$f-3Ol}`{z?@U
zsr$43C(DuGoIJtTBevEmz>*b#K)I>)O)nqk^1*Uhdxbp4%$x7eJUf_#CqU|UNn3WJFnQGG(uVgrc{jISYpMeN6J0ofSOvE4xqOg*H;x(_2#f;u}nf9E0cI$4np906|e5nvhGL
zNzD#;_eL9!I57;30B4hz)4Ykhb7;0P8PVt@((^D6ZWkC;&Qj9NGGE#w^ob1bcTGG|XqK189s@EnOJ1%q`=M}9~n)MU1UqrOe
z&M5S$$HhSff>g?%*ed6WjKBXv(FlZ?UCE~k2C2CwHcU%B0vAXP3O&4Ti)c;jh|#To
zF+cPlZFj9y<1d-u%pWn8S1vJ@QJbvxB@xc!ur8CdZoa_kx_Il9!?$LT?EC;9W~fY_
zMJc6B8bxKB%l*n3vG%h7GEun`eZqNRQv%Wo;kb7&SL*rDL5
z$>NGhj*ZHU*DEiR`C+Zg1!3Brv<=}pu?&}(&z^cS1WcR+ez4nB3VgNli-MSb@%IR~
zOJ6qMXFl4+FONL%#l}M4$nL$;7*Xcv|GLq6Lc0;887sv>Jn%#X0lgFW@wMeAK1Ykv
zSsXg|ugcjxG>9uTxjy~^x`PJ6eL-T-K1QEbWAVuh4VG#8RO
z5JVQX(CbJ!e3r)SOh|2SQrIl53e
zH~6Ng-oC~90xT{fRTaDKn7n8ixVOOoa@@+Loq+s|A3RZH)wcWxzV@G^8AN%IkS~C?URmJ=Al}e|ix~Y*HC?N=_
z4bvD(KbW&76&z}|qG^=py#jBL|93WyYcU6Y7E)7&rC-7#2iPt;cBxs|d1zDf|GFq=qU^ZHl|F*aXmO7<
ze@2R)=fbS#Q+g!SU&=7Jhts|$WPFX6MP}I1z05~D@_VMQJKK=h{zmIhvCvfK^aaR70wO
z@lM#r1Z%zzo{W>38PV4IpwcoCI$V&0F#WITQ_M;%leAP
zNqYQfeK^VXI`=AhO$NVGaE&&(%}`q2OXdMSzRV5SJ^bLQ^hM;CTpQ@EB3OQ~lq2`9lfMb-F%2%>wxoZ5|
z;j`+NJ41~D61Asazw}{qr^9Bldf}1h!%f$2A
z@Kj96npN(!gBy)Ejg+mT#f%j^68wBbd+7D-W#qRnS(zcoM3-+fvX<^QPeGm=6P9|P
zBYJ9CGOGR*WHOhah06gsfQ!94;V``IkAZ{Gezd=+>%{PD*VuL5b
zn_~a+5W(7gc&e@+`E(#lAQLa&lT-})i94W2CqN^JO#6J7mn4vJGnI>${CRM9fB7Gq
z0B@UuJ)^e7rGv?X@ppw
z)wP070ymTXXfVCq+=iErlqW9qW4oh8ILaSgu#<7I`wUCQCfwb%
z6Yud43AQDRDf;G~Q@M|!#wF@BEcS2d2&Bn94Of*nvy3&3Z
zgU(A2|Dp;06hIS6B~6&`?@)SeGp9@_4QV#OB0=A+j*&elybayFwgj0s`tQ@h5gg9F
zJG!n31E|Yw8CDi#EN--~0(LWlOg-drTsbfVl%pIW>NP_L~4kqG?
zbpEs*BABna<0W5`v_4{Owpz`$sA+5p+C8PR>Z)mNO^4GWWcJj}1jL#reh97C*Q(AD*8
z<6ek}XCI$?_pVGQ+T=U#1~x|x*Y5s)ofYKC$FsGX_RlE$YQFyA`0dr`+wA9kth*}(
z=)Q!ZX?S9No$v>b?Ts*@Nc`#aencwzdKAZGBQ77jhqI(bgUmm{>S30_glUnJm~L*3Uv-kQ+&5YTQAgZ|B29D0o8aPd_#Mqle12^t6
zv`ze0{1tVo{@7`2USv?%&@j=#^gQj7TdlFY>{))>ZKM}6usGl{)fo3x!N1EQDThja
zZh3s9hDu&A#H$X-$k(n?RSX?~yTeJ=;PEpR=Ey3hOF6{J*`iR9WJV-6!`TbNoxGJ>
zq3eVbtA6PZxHP#XZReS+qH&FP1C;6UmDa9BZ8DVUEB|2^BEO!oeKr;&=d1Y=WfW_B
zvgLv<`u6o!CwNm
z#r>BvLTx7w2~~^f>~;E69q9H6K@gIN-xmpf$AtxveTN_u#XV#RIx#LxP7#+hBj)N;
zx|V>iW%K-+`O3RTCZPIj$>nc#>Z#*S*}oe2l1$MA+`Wl|Mh26V5HMd|=c_oxwO;H=
ztBHeMHT{50`Cs=7MU9J0)>;S&y7~Ef0vZ^@)8PlgUy{SMCdA)2&H>?A!%$x>wDo3P
zbsJnzyyno08x@zfm)uUNM(Lq7LlbqS(Uz1KWIlJ?70ZY3@DIyU_>!Oa-EKi$FeF|d
zvSX4r7hg?SHqyGg{p`K(*gKXQYSQlvQ&#K$s8qH(OP5G1HvIDbZa`oQneXy}lN4q5
z2RR%m#VH4RgH9t-aSA}en0PPnynHiP*L(h~lBmQh9>p)>PDVcL4ceqV9$B#I2F?50
z(U2VU9o|%*wvOQsHAR#ecXyU{m*HwnDN#Z-N?+Ax5cpFDg}lj{h1VJ!P^44izsf0j
zQQGD;XMb24>8dB{r*K+*+x9+?dYy?6*Wrf!g(@msfU0`mbqk262~(jWZzsgNz
zNZpWPQE(r+hmU=~qr(}?K%o(ny*?s9S@o3Io{J#?{#1j
z+wV7T{{`iQ@>Pf6yEuUNTZG))Nvg*oGB`U>4|A(~v~hnY3N|ZPU(Xj6PGf(x_PNoR
zKz+1oZFWb=#1JrtPIyJHDuzO1g~tn+}h9tcMr*%Lo_Mvvp_*&D$4&
z<^Jgyggkq;qh1N4429<@mnEd;Bx51cEQXV4@Q!9!A2|K{Qp*FfzcY{h8xtv-V!-`a
zWhx9&yvKRfoL8&V7P;37C$XE)o<>-45Hf%p&>UgdTmimt#ljHV(|_Ykw0I
z(0iZ<6B944>&Am(i-cy2lx2hMv81vfuG)K}R%%zJrDH{$oY2)!-a(YQxH9|unse*DYK4Yc;(~uQubEuUX1J`MQJ|w?swN!zkVw6zM`#3*5p>h)1e3&U$kl>N*Xk4QupC17gu
z@&{jkZI$qW-RLtxgm
zJWwNsH#cj?+Df&~Q&nob=%>CGag@;UB{EWV4CWv6*}hs&LNXM_u
z$kFL?fYXX0!ijI2S2sTlPZuhYA#s6~KO%DLlJ#diAEpfQQ#^{ZAcIEb`G9&{Hdg6p
z7v|T4d8fh2+cCY<>|Dt0$tv=~CqM?P6)DilUhqyqXedkOMFz{xzm&4A9Nz~ob
zS!J|>z4r_2+@;DXw5j8$a=Xcqs6vX3edv)Wt9A)yWG&|a&Ty1u^N->(t>M)y89
z4t3n4v-u&XXfS)}^XykXCA5)749s{(+T3lYy}lavS9Iw!*{f@Od)$4jR6$C<=}@8C
z{Am4*!cb7L^+tpPriwPMIFxCM&vXm^Eu*&h)Ubu;T?Rw0iG49y6dNIf{4j&EZnNx?
zI2^Ni&7G81StZZOyRd8L!k4ALmrX{|faz8`;VNm@lbg0092V1k-l5yJo*f}>^(SP^?Eq0TUUg0s@=4+E
z1t*&0;3Q)J?oiOxIPMH%2!otnn19Y^5falJg98gVL1NNDiqWMK93&>&;8x?E?2G@Lxld3nNNQ6tVi%-I$czipB|_!#`LCC9t=P@@@*r=58Q
zgMZSJ5|Sw5zg@wIV&O5@%_2QZ_YxLNWf58^g2nlbRdOZHYJ76mLI7GTHF4VgIW-vL
zR28HQ2p_XqJ^ezyG0YJ@b0DyxiE`Y76biGL%W@$MM?9tz4H)P@ql9S)u`gQ|<9Y-?
z*6d$dS|DF@fs33L+c#-=A&vFQO?6ggwN=*#5s}yHoopTY*DDvB$et(aUVzWX+n{oG
zqmy^gaY7-`usefHDTgUd_H?3~7QYMXV0)Ya6O2uMs2D4-GX^%TMbsQF!Z3&b4lk5N
zqGoe&(XY(-y%7GIl$o^pSpL+19v$nR^9h*{Y
z6ir131EK+m?RI1c-2uhh57m!BMU+@3)V11dheJX)Bp}fR%IVt?Qv+yd8On{m5{8n4`vr+)BNXqT2X*!_4#C<
z1Fqg+Y{9XGjV3CLIEJ0MY@H4DjD|CC%e~uMG3ff8d{Pb_q;a}N^TKK34zAVZWTFkM
zGWqqFG&r*wm$HcdHnPO&ORlsz{UUQf!clK;5@u{Wj`!~nbU>pT4|pCb{EfgzJZcghFVBsu{P!FA&8g-2G?8Nt-?Ep~cyCp-%2wv;!*UVaLGowg{PW
zEcQgs?zA%WO7+BHEX+II(C=Ye&&?vY3j!tDyMHV(S_|xN$X6kc*rd-|z6x-oA3}j9
zxso5M-0i5b^&zO-txN~2T%69m<&a`a)gPl}bi+pv-+BvaZOY_s3>-SDxFg2ImoHA
zei+O4>$ipQ^#Si#P^J4Dq&U4^^R>pEmYXk(9iC+eU2A8`x%ClssK#IIS~%*0q~nFP
z4B6Y0?b$stgPxMESQfatB>?B@d@%i@JUBZ?vy}rM2%`RHwc9%=+VK
z&W({)?BGs)@>y>y!E`z(w_nwC?h6fE*~qBX-PI5?VZCJSss*<#Man-yN_Cc`oW2wW@F5N^
z$8o*LpvY9!J24bivGamKFgAXC!g?z2!H>8nCIHg8Ac&RUj547JBrujm8RgRsQ9%1T
z`|8Jk+&4W}kzjXo_AF<^DMS82ZoiE@w}zb`BjSWMaUqc!Ms^v`t9SIf!7k)#O{-0J
zK>Do}9nFC>fD={b2!2J(IT9NLfcfDl!jS9}Lr*kUPD>qa#6Z+@y+D%$!lCo5rs_b8GUn8tk`1zK#B3IIkWA|y
zBU6(_D%?=G`kqMnBQ6R)zNA-Nl?cPg?nFs+QHZp5xTZrX28T#t#Fpv+e{d+}80C(z
z5@;+Bf9=PCV`iryCv!jGJ)!wTIf)AHmHS3l^+eu5B)axTlJovLGtOp*nq{RYOq`3~
z#9*`2Y_rj18eSNj&2(9AYNfob^Ba^V=NSu6ms>Srntn}s@Q1Nz6fcoWU=<#CEn3Q@
za0t^6uh@<;Xh0PGLz({rXm+5!gNy~UG+q0X;_1q0{SpZ(WSyD9pDJ<5BiJ^ML&wB$*dY}{*0}I1HCqjZ;a07%L&~U9R4N8B+|z~;
z3yF^9R|^VV1(AzeF+R(zh92ko-ayyskc6q>V#62rZ-9VI-&p=8@ZHL!OE+h~N;=3)
z<(_9oF7-eI0-`@DO}@+yb~7&YhvFo@WZ|+8`Mw$_IImNh_6cD8J!YC0HsJ4^$&0oux_)8^fQPNpy5xbM-q>dErPg9OEPxNK?5(X-4wHJ4r|Z=$deCHBELya$
zi8s7wR9ob%?30Cf;L|jl_rwqaFRR8
zE`tYWdJX5bVpaPn6e#R5CO$?N6j4A${qQA*@>4)IX_9;eOy6;qwi$vWTDWc7)a3n)
z8^JZa6>HPF|9JO`HU|(`AU#MW;d{`~flO}3ok5CS(CK9L(~tVU2QoqWcSv`-kT1iE
z8`C2bQNu~(OV3)=U`60l56j$LB{W~Ms~ZCTwY+V^lFV*MhunILCgG{>z+EcmI+k>d
zRrQ|6xPZL?p5xpdhDu1om#sO+O#uTlZehdfj+XD_mMS0Fc5@mtR8s>`aqi7o8MmkA
z#K!sliGw@D_g7YfhTJDezI?Vbg|rgj^Yc$y=Z*F5<{PUzv+EA(!3N#)%#z#dJQR$=
z3hwv~VeBLEJEHYLzLzel<9mW31{2vMOR=lU@0V6Ip<&9{G(z&&2IDHP3
zhmBX+r)6*UgRQef@qVI~JuheSGJ?Mur?chXxjs%b(Pq=4*PnC~s~uSvm-SRSFawx`
zqNN!w2bKOB+#(Fa*{~m>l|s<>;IA%oZLMB(_IH?joY7c
zqHH|U-$7`M?ucR-dMf|w68897Pv0I<*jmZ-@|l%*OCpK3zg+I*5FZhjv6Hbx8V*47
zrN2!fq3?Z~KRr$`}o?`t-~VHEw^OEz?z+-RpSg&DKnl!c+37&0}FU`
z$^jCnbe!Gic^Ea9yd$5b2?C+JtYYy@N8+S07*-Ou-gBfJQ
z`?v!oV&vmdmR#yAk-y^|P0l1)cmOVOae!gkRuCc1e22y-%ItSx(fHXUMW4a3N5Tmz
z%ysa?x|J(#HTn~3=iz__Eo^LYwr}<%0`!_1!@ZN>Zl8#`A6bNBo|U8B)bWb^g-#I#
z6sJ~#b|WOfBVtVQ6)IQXGP5UH(UQVbMH{jJMx;j?+h&Y)8y$m`R8N8S7kQv#2_WET
zB1*McssN9hZy1HWPCb=+E1nA1I7`h_c~;6s{~MQQ+hH|S14Afrizb%RvW5a2q`i#H
zHk=S_*V}Gvq9-Zx^C|fkXvlc_?<`*9lX^-9))#gYA*nr6CQ=!k>$;i!*bnywhB5Y)
zEtW*m>FRP3)#6{dq39tLcHi%${DBaxvu^J_mMMm!mCS@kTsjf-Vuj0RBC`GniWo{J
z{^jJ=2SCaamU>&3*iH&s<-4`QByIUcsdh?_%C~HT;e>Ry=M#yXz(;;$SwI#APd%_5
ze)O+lxfCNi{_+vk^21=wYvF_+mjar5{(QFXd3`C^^6ysUL(vMK0K#1bq6$1q~mXG3qe7$k@)w&1Rz=``qDZuy}h95Wz*
zCy7yGc|k3jiW)S8)B{Pl!TIJkklTO3BuXw!E}rIGET@^+N1^CI|5sL=3UmF~vH5|;
zvTa~(sd65`{Cbzr1I)!@n{tdHZVGf(3!-f$sVzxZ~+tvGpEQ#f~k-juZRqP
zKyppKtEI2T
z=;W0PEZw;s=>iFcx;6OpMX~KOGmI!ym3MP#i&NyXw>7n2(uKb-Hrp?lpU1K(A%;?z
zQqWjSv3-}5dT20;6(CxtG9FDF#tW@V4U;x7O%SMo?QwNzC-@nBGIP4mABp>Gp5BsJ
z4y<~(-4;eZfoJ~l{v|XcYbes&)r%`kW(?$xJx?Cjrhiin9js}owK=?zYaxq
z@>FvYE6F8mntwqfw{|+7d2y#D!|s#o64%8(p;QC@+~N>tHCUJPch(2-?#Ish{S_>Z
z0P^^C=o|3q+-u=Y!u|i<@&oq(Nv<(ffH4L+O0q#CVHZ0Iyg*%JAV$ow_$Ey+px
zZg^P@rGUrH{pO*vBy()T(kbZ7wfpIFX+@sTVhl&mN
zNq_NklMAKS>XDCDUR2(=jvbqE{!OvMph-Uo+t`;X-R*dAEwx>;85yLvk{>iJ09Q>4
zt{AKHafODpS}XY$>k4PVV9IuBa`WW|NRpyd#bwjJ4w@7n#m)eCjq$Zp8BMq9FE
z^mXyObU#i_#jH8A_3AX4bfqt+$*)B;j!G4#BrOWN_#Y%LA`^cIsdy%!{TlL~nAFw+
zETao1v9I1|5OPaU+RRCc`b!v?f#pM`{iou~S^uQ#W)8nOaa;yB)C1d7D3{AB%OF6Ay_DZuQg7qK_ZLMQz8HL^-Z=KTlc4g@#n_?OKye
zdtHHkLX>7XMRYwkzWalmWADn-RoA>MdGj^FB>z00Oe5q5n-|;6g=UuvAki{ZyRxhl
zx8$d{u(TgnJ<|?6_8_XfU`AZJb!*-SruY`zSo`P+1~S&G?|u&_z2596iP;*ag@xlW
zlyqVm75=+59~|HF5z-3*xRfEtIIhT5&$H>!1@Vs~Snj@7D@Cpif7jnWX6rxT#3Av4
z4dQ&oPV!8@%Bl5gpXF{@fE#(cK98&W<#LzY)yq3ma0IWT(#%(2}HHC)F@#WpLf*tVTiY}Jm+x~O!`+tqw*o}S0*xiM3)|zwh
zXZsTAM4suhQjY&D`Ym1E1!~=@I9av{v#hV2L{Ko1xyu~=5PwqydJT&g@2GP2_suDO
zFwiL;JrX5~DM<%laP}6pDpAD@bH(-F4!*S#`bDG9wIlk3z*ZzuL&vgS+61!LjAA&G
zB6GN&BRUQ9_A>W;n%Vk_*i&e0K#wvm_AhsIxOJ~#k=@M=U^NUR_Jp4Gt0HI6QtZ>O
z`6poMXO7!5JrL1lPE2N7fQlm>h^E;S5^*eB*dD*Alz9$-9RCz2IQB=EYS@oX#9w46F?sRNuoKT;uR5dONedyZR&eQ~Q2x2~-Uyq``^eA2m^7{J
zy{2<$0LW-|l9POBsWHar7|Nm>L7hvHcYfD?E
zkxpP3EM0k8B4r>sw5?D%Uf}*!S?MpbVIoWf30(c|xj4O;g3QHir^=4K%`dq9zzk8-
zZhLXm#R*h0+K9h%VL|Ajw<1y3kx1sZ)8oN)A{2)Y=`5-EkmQ9>-BpeYM-z}O?`DB@
znyNGaG}tZAAFPcsL!hrE6J4&9mIAZ+{+8k}KQmN<&#RZyZ7D&`GUb>Meg&09y{vYv
z@fl>CB3!5>Pf+J}M-Y=>M-B?Gxno=usM}W#w^{XQN*imm71jf`NCA!9H84zh>bGm~
z3ANmeKMC<2pELEm-{db?mb<=^q7=KcO7j?GD~qX?$C;Lqi5$SL(;_lIF1)U$h}6mxCzAhf6Yh|ZM+!RAl3K-noet6%yr
zDdASQyz&IJ_j4nqIAB{Z3}SLGJny1_Q0uup#|JPZVYV23gG=j!>=&cUtm@=GQ}x+0
z%>(lxpYO*DRy}}uiyuKVmX~f>uzE{(#Xn!wPoK>SE2v2KbC)6YQdpxQq#(Dh9aoK2
z#2y%mtnewCAhO0myh}Krj%s6MOVwRe(*P9bkCQ=O2F|aubmI4eRrX>;5oBk;l-faR
zZyAA6B*1g%0*|y(&5X4b`H}-a7W?@nk;Fo0wn4eJRLy@)`
z6qU-F!ih-5tv_bjwtY%GA
z))g34to+i24;-GaljN>N>oz$boaAhK>|6;>$Zl!qq}X$p{Bh1DQ5j$6PD7vBagW3A
zGyCwDZB8MX1>v#wx&`akA$8H$QIOqqAU77o=JpQkkVTplLm*a&LqKx_B6N<%V~4dE
zv@v@KFlF7vl%PEz0jA~Lm`BCMw}Fruxu!X)YkQ#WddANV8_W+~BD|RPH=xI@>N%NP
zS?_(RwXMhf6WnlyM$z))Q9ER+r_B^>6;7N*JEqBqa!sW)Wyg4yS)9KlpGiw8>q#kU
zs_Y(El<9EYb*lLI?{<~}@96UaYfwFG6PfE#NNu(6w3S}3HPw`TnH3@JDHcGkbt5$R
z(e0%Q464(9;d8@QaKp8D?3v_=!@^g>;&*TPf;fFO
zL$4V8oK__Owhs4k$slPPb5?&f3!Xm#1)(spJ##lCvV
z2321YI_(#zW@$E
zwQ8)txFQXw9T`lM+CgCmsj^#GB)JE21+iMHdw}BVfgA*~mz@QXsQj%V;TLb}$W>0K
z#%Abak5(^@Bt7Im`??_Pe3slnx-mbZpJt-saTk6nRXJ<2;`A3wQY
zS-8(hOX25)&T}k9AuH_VZnrcV7IX0|L$I>+S%ppGu6A_6Q{x7jy^yR{DoiT;&1Dty
z+NjHNMKVT{So^3u@NLo(86_Vh9+5gLEX(>WcV1rK4cMv0M0l`4zp;grY$9RFiO
zT2z;rCT4-{zNZ?CN;-+XP7_x~5U)kfjNQW7tG#T*MTGqN4qAyuA-|v1cUS*)sbZTU
z@o_m4ef+R2k)!lhB3B^sy?FX%`u51+?K7PdbNKvhTXOBQ@P!(JDb3!+Bj;f!n=|Dj
ze>%PXaV}Dpn*_k_Qn<@C!1fv
z@eVnj4+?vQ`2`#~*$^6P@!;g51YHOsZ*QWXdhE=Yh9C~Y6>3WNt6eb;e+v!GoWYvd
z4+P~YTP=hf@A0%F?e$cF2K1fzO)G0k17X(F<#d9!D?7`<%PU`wQ@9e2FNxJ|42FEQ
z9`a;0E(Z{E`g$UchZv^PRgf@jVsrB_ET;{Rl;Vv6ZC&rO+m%SBGSFupJ0Z91cylW#
zF^un5GRGvmSZ5_^mgAagN(U!SP=74|1A7Y2QxDGrCo;Dr=`xXM5`MzUp`tyq7wL%O
z8<9Cz90RT8o)u%nY07{>&gvX3Oe3_8ErGTHCkm+Ku6Q@cxS{sTc9xF0D8e6{VPomJ
zu+~f>LHyxaVEs9bgyq;ywXT$mT`_X!R$Zt~8AFRAWQxyh5S>8-Mv=51uI7l|uNV|2
z;pT5Bm-r!m2An?mQv8F?@6IDfF>IME9~>)F
zV+ydPKL_puhbk7iELdE+N{7@T!q6h%VWFnwpG66PS@s<~QbbNgpkt8>W#3EzK
zo=U(b8|Z>^63QioNH@fj5LAQY(c9#;v?prYAP=^G>y_1nnH-<`m;PsTHcTkGukcyP
z5E?zs{OE!(xDRbaO_7RVdFYJ9-!&ZHa=0(LE(X6ixXLi5Kzwv<5qnhbO{ZMX_XJ=M
z{k4LAg+pIMlM+~6MH$c~MFd$3^yS<0FsPGC>hcfairILDLY_MpR6Fi(xu}hEL@21?xz3kh&J_h@P@nBdlt=7Q91`G8n#L?F_k8(0kZU
zqA0`q)0lAnU1=r$^NgG1=t^dy7px%|gU#oefRiVvwK7uXYKOczW?|a_Q3Ci!0kap>
zg^&?}&;VgA@Ed{<$h0&A{76o0;PTIy-N(o-8a&G9b6B0gLqy3-I^j3bmXr51M|)pM
zjkUm{S_<)VFm86Tqc2Xb!)1DfmcWKu8J{B6@?j@shswdolJ8l73I)Y27B>bHb&w%~
zU#Lie3xu&D6X@<$bWDnZ8Ye&iJqc&2%3SEO!BZg}-lGgHDEWWQSg{&;DlTwRp{MJjB4@D@aK&-A?HIkaaPXfq>2
zg9(vLQoe0eTg5Lg+q83@JmuEZOp5M#?U6NedJ9Rs?&VV$gz(FKWkLW!XS;M*IiBYo
z2MM}Zh7D&BbYLW2iGE}+$o3dg2W{4#?E3YZ)GnHKt
z)fY~vVhoaQ=EV|KMjY#6WJc~28#>8V6!HK-5?w)?DF%0BbSCYrwP?{GPF+YlFlEr?
z64Vh=2WenVPEEWtGI=v?D03?aF+wusa)0o{p`B|JJLG0Z!30=?ixz-aRVv^Rc7d-l
z3!ms^xNfQz&$P`X^6XU!66A9ggz;Xe26U1vK?vIv4dYXfxnjAQh8ovoN@rXh+1VbU
zbZ03LFQIWtcWncU$IeQ3(6iU5zHjy$*?*vc@|$1=8j&44)2>@|Gd@@Qxkyi~(r$;^
zE!qEa+pdqx;06?RyenANsiL{*Z(}T?s|q!oS>z0%6nCk}$rCid3P2F_h_Cpl2m6I?
zVVphFO(vVHIKG>-e&$Tn8AJgnCw*$ch()~>X~gpI7UgAa$iE7HEAiIF4c9ntKUUam
zOLw`wzd_d+nGle)@s8b0YQ7E(3Y(4q0Iz4Z_kxbJ&?!Q43Ml{iarT2@{vSid5O!Pj
zK5Ol?D#a!(B2_2p|8v)L(uyN#s{Eh31`D2}&|K=;7^AN`&yxLlXcy-T>mhfKk4Kv9
zOLgG#`sIQ2>r1kS?)9~#Wp_lk5kJ}f7a6SWy58|$NS@4((oFoVrR`}+_X4FC#XkT`
zIzZPRre?qQI;Dh8J*NBRvR>_q2T%>_%TR6ys-jWn?&-#JUHHK=V$}fkz
z;h_$o4eHxT^qS{TK=?9?;BZdc92v@F2V_)FA)+30jXH^%c2H03NYUV`(
z^W&n&aKP4Dw_2%D+*5atL2`B5-+{
ztz7AHHIDmCZN2mI-}BZ^3!#was3F}iU(tKlPzk7k46-iMWMJj0{U>b;
zUvJ@dYEf#$02vASHys_w$8>nVmhl}(_VSO#1NURs5e|2hp>U?H9Ib?Gn0v)JeAQSFMn8jD^r73U4HU$*Y0_pe
zi@fCKztSH|Lv=GE4PpZm^h3eOiFa0rZlwGgsNTOX_J|z0%=ijq9rg|2!&NNtZ1P_
z^9^#?HTc+^Q3L}ojo4&Q>-AYoU?avq=@?6(2XZ$koJ!EuctpRcqL^yU{%FTvJM<8K
z&KXl2QLk^TC01f)gY=Bt=ZoQqOcqkgpIx
z#!8>eaad@JXP$tgw)?yov-g^4Tk(GBJ_O-jyq)@{!Z59o4Hf4|
z>kEi!Nn&K-%B#Ty9)6}^YtP8|U)>Eqn_D3=i@&ep3iO_
zR7hIS9y;to8#qG-=29Lh5kRp~xVGLKpmgWcam@}o$*wi2e&~*H9I=6PlYELdH011(GO$a$^CgeQ!%|{K>z_$OSCwjSN@9Bzq
zl7;Cr8bJB9P~J9-Msyir-yJDutnHKVBZx!k;-2bY+?;_wK9R|~c|<2s&OU8t1V|fl
z{Oy<*p0LCv(`FjM>!I#MhNCMUbO0otLVEz*S2Tl5)8ugPjDK;gD_y!SDd8jRB{Ze!
zW{}@^jZp|iAIUs&b5=kF2QYJ>-0N&T-xSUrN}z>rrfS2(>l>WkO+=v$e##sf7*ZIH
z_kk$PW{f}y%=bS`zm}!-%t@xWHyqbXRn#@Cp+wsKuobuj_CVT&JkcO=Dhe&KTf+be
zj-4fq9*)(sZ$+E@=_b6If!gKd19I*u-Agof97W|2BgrGDTDraRYWFhu7}2*<2bST+
zdPgc!nJQ_cndhP~rX9@}?{gA}mT1W*j+cKP`!I#r?W>i=Z|#ZA_&n`+H7RD%gjh6^yUR81|s~2QJr#4ytdVO1W{RX)<&V)~4$W=f|us8b=(Q*6_
z;krvhs)mXMcI&6Fh9{YdeHJR80{IoYLX?GPVDDLMJmmk~L)5%Km}XL3
z@Bu>EB!Akdo#{G6ICm_wOR2DdRtES$JcojQS%~w|-7`zW-QVKagsp_mwHef9$oM(Bt>@|o;j&yv^6ZH^QBTMj
zmk);8$O1sDBbx;Rm!k5t)kAZxti|>%uJ*@&aT}2%>_&GDAO)Mhk74$uo&)O1_jtzK
zY1hpq=*FS))_*+^O5ibz==XeJSibCx6TU%V^rKkyWNKRKutEBoRDh9G?c{1bY#b6=
zlR7U|peGoDQ@MmeBE-T4-ota=kxT+I?cFlVc>??vKpqiCh5N;$FqGBW80f59uAFk^
z*+PjON3JIjE2mlfGt5oWDWjy{&S%Gas#>FM#3u$OXV>3I)>H^DYfLrPOy+K)pNrUx
z##^8Og+@TKGk{oRIKKmR#xy^=6QJS_Wy#)Bq(MWwkdDYPnBpGlY)-H0T`VHMvMiFZ>LA?nBVFWZIOiO4%-jCRm4r}=M
zG6L-$aZ>Y*iwnCBR%dg>XgQeR5eK}@dke@bZet;DIVhxQ=FLLabRn3XWZU-El&B<}
zl@gFm+Bvt)kt@MO$M|m2!!yY#P>f1sDe~YKsG!>aX!y{@YsuA#qV`VJw*0hXVTF6fM~NZq5?0i4w*M<
z=yk6^oZ-8AhpQLa&YgTW1l^smad%M*Rtia7SpY2-e+#*b-yGgC0q28=J(f
z!f$0KBLy7a2s0JO41@^|ekOH<`39DZ<7?cJQJ+jWA#2Pv>ru4H?^Q>Zs=kypC2MW(
z{_nd#aZpQQ?iBHin}0G!po?4ASI4(;S?pD?{eyl-ayzmTLO)>uH3%lEb3fH
zCf*SjvNSKn(TmF+WD(y=lb;P?H|Ij%mn=_p{h`oob$>EotW()R`UzOB^=zFJ(iD;u
z(0jDs$ag?)U=L$8>EteLHgs~20c$o1QGFM|+GNL8LHdlik%v>Kac50|iLT2?C%*@o
zcHoYYuiq5cUq~d#R}qyV<3i$m8_Kf;71i*z0^~JLAKs`WvG7<%5C--_LDNKAH8IDS
z(g&_YYPhey9M9%cxHV=6{bK=Qz4}wS}LSIh5A9I70V8
z8HAG{0a`?F*b`1oCo_cd@ywb*7!DMs_?z+I(Ho5NI>?0{MK&^T`bpogX3>*10A
zkQPmpnxQxD`6hib!=xOJbi?*{ca9}%LWe1S->r9=?g(W6jTklOR5B-Y#GGMzXRRc=
z?i*#ZUPQjup=etf(Y8MFW%Kz&^{_IESqo6MSQ?wNq1q?&UD*_O_6qKW>IP$oENJ(F
z1c|kM&W`slWs>k&q;`yL#a{
zW00%S{>+^v<^YFTvoFZm+`pyV^7&fbbe*f%jX_}Bs|&Etj=maV!}aXy9l(D2x^#yk
zDzn)2a8$c9dS@%J-LKjxOE2>_h
zzY$`bGJ0?p#lH*E(LZXes<%JqG5ES?U*fX?9n3vGD&?ml*S#z$Vg+1znHI7t;sxpB
zm(vZ20QACzu0(6T59e1rQma3+l(Q0zSf&H2bVNnWs(-YPNtM5@lxA*D72K3O=FmN4
z$Z`1{=QP~F3pa8FucNW{<(GF03r}aSSm3R1l9Endyd^-k5y)YlaJSX23AsBRTi9`O
zE|W~vdeA}bMQ8R++wf&b@nFz5yw#z%Pm_5+0d~CdOLb(KlT3E4p4y%-7v^p>@MJpM
zhV&nj3_Ft00UhOuCsjpi^&}SlaUZu1E|GP;&lNt9mcf;)npi&zU1x$=k>pcshSB!5
zX`R{`Nd<~625|0$dpj%o(vbx(e{teCQ!WpzslsB|$VNip$QVwh>4i)fa?wS*qgl}rq6*(OQJtnd|
zXlF>I8!)(_teiTypXP5kLCL0V2|P9H0$5Fm{)Js;cRFj{{to!b-8IcCM1+6#!NmUIGOQOzfrWk3Q|7ZT3M1)Y9KZ{bTU
z16XwoghM-{VZ8HXXCS7XM=J2>im|ixgDI_QiNQ>(N7ayuqe{+fPYFf89kDt!
zkF{K4wKTwNcY6B&y(ev%DHP2YQuISjB@dsF&{3&**NR^R8>AeVd^5W5BZ}Kw>+P#
zuELm&5XJ(a8kXxTj*?KbcTHe6msXD)^?qZe#!U_4D45blOT1b?gyb;O>*p`H(PP=i
zev0ZcBADl~%T64WN*!l~0&HRW1H$%gHgN9!^I=_gg=-bc>#9+eDcFrhM3^{&<)yN2
zI`?U8;hXDfgK=zxth?nD)a*O5L)Hx^>GkIeyg>lUuV~MqlxJbG(U8
z^%Oc|fbp{7WL&3Z-}K|PN3MDoNc8eAHjg-?v(XocPO!izJ69fLstNX;78z!$n?RRX
zwIl3Ol{j5w{_DWQ5Dp1bPB|MtPx9Zk(rToo;4C|bT6qpy8`M4``xvjUSv4Z(H
z)FcIqLT9vx&5LbQnfEk!Fw)!IHUxY;AjrdklKsDc`X3un3e2)JB49{^qlSb9aq1OK
zXjoEuzrd@J*#j84QaJd5QJBBST}Zh1Th30qxnrGa{#~W_s<}AEp-t;?(fIoG`acw)
z?}^jPn!ATKEx_1g8}Ijv$J?$cj_f_N7=~O;OF|aV#VIbCqK{5Zk9K6(QYvbs
zUyDPIZav-gg~HY=Af@5Cn!C-_u+v!bIfP+XrF7i;hF$Oq&cW^V^ARI+&PCDx5e19_
zdO41Kws~`~Z2IrP+3x=h-RUCQToB0Fw_0S4#f_)N47ym|?zO+IRa5TnU773zdpSHcL5i51@
z8lF2sPW2ol;`FiQ-t7uA&)I-j5fe^^q53={wy@k=)B1+cLYKKb3RS1sA9VZ0u
z&bw9}Mvk@zupNdL_$#M#8X9GH-wAO7&R_iuaZ&JVA|;M~NofkP_3XCA^>mEZm`?1!
z%d23)Q6de9sV7BNSY9pv`4aSDd}d5;3hjTd-R+ZY3lxLnIA}I2-k|kDPuYZ^W)iTv
z4M%k%C511pKU}IN>#vYu9t6c?;|SFxXfwRjs?s(C$jfD0C0!AY5QxJ6t&SD4RU7Y;
z0T*DlErHJ?Z?A|vo&9^-HFi8W$4tvHl-e!gu}9btU&tht^*coC6CUT1g7?!ubA>$7
z^f91lNY{?X7O!B#TxO4oSwz_kKRED+PR3T^lZ!yyDJZQE2-v+oPc$?yio-OLrm}5M
z2V_7C036LzAH~lIYrcCIN;l1g9d#|Qg2Obnb4M0ZTj$0{P5EZ<+EXk|8
z?1pl5&qnU0$3f*5?TH%r7!IRz+KOxy_eGTju)j3!?O+F6ph_gi$!V>GI7i<5dtjFe
zr0^1blq(|2=KJhHi{)4-`!OA%7&tSmF*2#-SbfhOfB$HQR<96|4i