From 9585835c1114645f8a26e2fe5f69d90d0f6aa966 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 22 Jun 2018 17:05:01 +0200
Subject: [PATCH] doc: updated examples for why3session command

---
 doc/HelloProof-style2.tex |  28 +++++-----
 doc/HelloProof.tex        |  24 ++++-----
 doc/hello_proof.png       | Bin 21209 -> 20750 bytes
 doc/manpages.tex          | 108 ++++++++++++++++++++------------------
 4 files changed, 84 insertions(+), 76 deletions(-)

diff --git a/doc/HelloProof-style2.tex b/doc/HelloProof-style2.tex
index 507330e7f..c0f3b7471 100644
--- a/doc/HelloProof-style2.tex
+++ b/doc/HelloProof-style2.tex
@@ -1,15 +1,15 @@
-\begin{tabular}{| l |c |c |c |c |c |}
-\hline Proof obligations & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\ 
-\hline 
-\explanation{G1} & \noresult& \noresult& \valid{0.00} \\ 
-\hline 
-\explanation{G2} & \unknown{0.00} & \noresult& \unknown{0.00} \\ 
-\cline{2-4} 
-\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\ 
-\cline{2-4} 
-\quad\subgoal{1.}{1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\ 
-\cline{2-4} 
-\quad\subgoal{2.}{2} & \valid{0.00} & \noresult& \valid{0.00} \\ 
-\hline 
-\explanation{G3} & \valid{0.00} & \noresult& \unknown{0.00} \\ 
+\begin{tabular}{|l|l|l|l|c|c|}
+\hline Proof obligations & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\ 
+\hline
+\explanation{G1} & \valid{0.00} & \noresult\\ 
+\hline
+\explanation{G2} & \unknown{0.00} & \noresult\\ 
+\cline{2-3}
+\quad\transformation{split\_goal\_right} & \multicolumn{2}{|c|}{}\\
+\cline{2-3}
+\quad\subgoal{G2.0}{1} & \unknown{0.00} & \unknown{0.29} \\ 
+\cline{2-3}
+\quad\subgoal{G2.1}{2} & \valid{0.00} & \noresult\\ 
+\hline
+\explanation{G3} & \valid{0.00} & \noresult\\ 
 \hline \end{tabular}
diff --git a/doc/HelloProof.tex b/doc/HelloProof.tex
index e58790734..0d32e4683 100644
--- a/doc/HelloProof.tex
+++ b/doc/HelloProof.tex
@@ -1,13 +1,13 @@
-\begin{tabular}{| l |c |c |c |c |c |}
-\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\ 
-\hline 
-\explanation{G1} & & \noresult& \noresult& \valid{0.00} \\ 
-\hline 
-\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\ 
-\cline{2-4} 
- & \explanation{1.} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\ 
-\cline{2-5} 
- & \explanation{2.} & \valid{0.00} & \noresult& \valid{0.00} \\ 
-\hline 
-\explanation{G3} & & \valid{0.00} & \noresult& \unknown{0.00} \\ 
+\begin{tabular}{|l|l|l|l|c|c|}
+\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\ 
+\hline
+\explanation{G1} & & \valid{0.00} & \noresult\\ 
+\hline
+\explanation{G2} & & \unknown{0.00} & \noresult\\ 
+\cline{2-3}
+ & \explanation{G2.0} & \unknown{0.00} & \unknown{0.29} \\ 
+\cline{2-4}
+ & \explanation{G2.1} & \valid{0.00} & \noresult\\ 
+\hline
+\explanation{G3} & & \valid{0.00} & \noresult\\ 
 \hline \end{tabular}
diff --git a/doc/hello_proof.png b/doc/hello_proof.png
index 922d6cf39851f32372373672141075cdcaa24cea..fc552d9c41eb938628adb8ec71ec201a1c6a7ac1 100644
GIT binary patch
literal 20750
zcmeAS@N?(olHy`uVBq!ia0y~yU{+yZU=-wFVqjokb@-CPz`(#+;1OBOz`%C|gc+x5
z^GP!>C@^@sIEGZrd2_cuL;2-g`yboi&kEyxE}hxVx$1z?stwGSc({WO=dE#QHa*-V
zdPBB)I%D;ryVs>Sl2v&kgq_wn=&e1+y5{C>+3Xv4q9&hCQhn1ay3cn_i{%==oe{jX
z5w^Rl!}NdlT{Vc0v8~|`ca}Kqt*>Ri_sZXe@u5pE<)8f2|Gj(J#t{Ed+pkxGL*+wl
z&j$<7TGrUn(b3`dc)xTx8;GT6#1`%1;^LxwB%!;bqa&k5B1ceAP_S2^SyxF(X^~*k
z23Hps7ZWF*Z6MWd8EX!PX+EC6LFB}$$7jTOXRdk@bg{L;zldXNtPTfX;3w8+P7_o1
znY{Zmmp!ZQU?CsB*t=iB%TkmW182;bAz)L?IqkjVj#DMYPv%`-{5whd*G})tn(xot
zy0yG)y=+EWyL4Rbq?Ko#i@QF(+jBQ5@$&zl(?9F&zMGdH_3}&E&P-F~V7oi_Z^p#O
z#?6^KuW0w2wmUc8_<g@}=Fg{F*WxaRm2Q3WS2Ud8`tY+7|Fb&la^A?zd-Sb8qOv~u
zTIL;}-KXD{Uf*B5_Dy+&Lw;&T`L5+@)5Fa5gA}u7h24w(W_7%7!<Uo?vGu>s{bY>3
z7hfp-$^3GS**=CZ;#%*kO1b&3@9jN%FY`_R;<twJsk<zT&Of|ZyRo$N-K&*yS+fjp
z+=?x^nPc|4;dI*On{O_^W`7nVo98og)$wZ+Egx5(&fD#~KV|mWwBmE&#X<LCjgBTQ
z4?lcrclWW<+i(1qZ{B&1d4s=hzU-G->;GO|d1_j;?#8R%8FKC|Jv%SFjBRT9^q$ab
zcKb^sW{2!FDB1I<Oz*H*>y7Jj){l2tM$BSrTj~2*vC_&?w&MEyeV=O&n6-C_?XNwa
zw4!v=@$Q(^d4_SRyUrcBVeC0;S!wONR~zM|<dnJoO<A*QRo2JX=e9-#gl?U}?Y)fC
zORx0&kF#@A&XqL#eo*aF4Go?8rH8kn{Bb~NXs9PU%jc|P3+kp{+q-3B`I42Yu7O^w
z!t8Fu%{3JH@p13>|ChE;2&;<Pr9Ml4<*HTFKAm1>A-Qg<lV@nC@8!O4+pnkfy4Dr_
zZ#K7Sbon^vzO!Cx@=Et#`Y{i0%!&9J{J~v#v)=At5$llVbEzw`W`)_^xEnFcD2A*5
z{oeo6_wAfw^CB!jzHQTM|NBR+6VAs73eU||wknU@c5{;0voq?m+E@1E%v@XZsqg3R
znC{~<m)01SGgTaB+;}~wZ%%EY`h1?BGGFysG$qbHyT12W%JKa??nTb_^Q~+SdMw+J
z%(bkr=>6P;H3i?!-Mbt7H0I%v54|t0zpZvRP@X=e#zpGbE|!z>UeCC)m;GLIeEWT#
zuM!HE1?D_kXJ4BBt>J6Sp=HNACN?Y%O;Xxqu&Q`^>IT&cC*O<Lm``V{p5py%_CA}9
zecM)ToMtWZ#&Wvy^DeiweqNViu9UnzR;Xt?D}H^SgN<c!o!dtP!PE0!XLy@FjT3PD
z<sAK?MY#Lfx5n~El5Ww<-)$-XyV80x`x^CGw<G74-p<`%xm?Wr)6CY*-w#iFkt2O^
z=jmPMi%PdloqG1A*Uyl5NB*c5O!77Tzb}}3<r~fieCIv?rj)p_#M^A&zI}Rkg^s$l
z4BzLMTQc2wdJpfvFr|BP%`+amnHGmx&NrR^Gj~q1<fRXDPcnz`xELRuv}&c7o#?07
zH9w}kkjXau()@s%^{hF^JN3=Wq*<~QXWBC6=oMd@oO9{VZ@;tZo7EduxBrgv(i7yW
zIuf<ryZuRght&C$qD#qlSC=OxB{_A8NlWr}KRfxagp+~g<nzxzmx!sWF4dUb?5TM{
z>*E2Lq|bLvLp2$_E?r;uy=dixzH>iSWA7&#CiRs~b+Qti_qp07R;&HR$Mda^U+%f|
z@zaIJZ?3+(cE09mbMoUB>-gGZS?s(M6*|s-ES&viX_A`YOzs!keFSX(?JQ6V&bhoZ
zTyx3ehnD-@uj^JMITdus#V6>AbgCQgOj@}s%G7+h_hR8S<*)NLHdpH?n#vdX`1ttj
z`SQ;BaZ7dnAIIROFY}|VUe{m$9&x;_Ab{r;kL-rES~Cr<Z@TF`-*o>bE6eF7U%TcD
z$V@seAH#7xc&3wW^WSSHgD?NoN=}@xNO~5d|4Z2|w%IF>`jjjTY-GJC%yING>*Zyi
zH>F<MWc$zWa{+I#bi0`6o9<}o%g>g4I~wb(-<7rA{`5O{u~>s`eA}k)eU=)wW7@XY
zcO&@B)8~lYO=X;Y_uZVR)$3R9+5YJ2*VS8ZzAbzHrtJ7V19$80XTPhz{XDlhQtbIW
z*XrA~!S2GB6{Hv#o_~tlxohq;+2($}S-VzTd$wxruY~N%QvnCemY;rVqI25r>L&fr
z_|5XU=cCdk%&L3q*m>9UY+bx|*{K_=F5kX*Z`a0|o9{j~`d3h(pJ%rAz^3pGm!FpH
z_FWouoAc>i)$OT?XRcIBZC!CfOfvs^{K`Gs-)z+@joo-V_VX@1qrG|F>3`q++V|>)
z1G}sH^S2GTp(k@TpOyXmYu(SOrf>6gcAZ_lad*rzt>Cvi@43%?lk}Wtxp~s`@R^FD
zcLl1I`6|5Ldz~&^u*}>{JesFJ>9bz`Yo`|O`kPWIFW7?<&zrBke4&4bl>N=;<)_?d
z`-)pUpJaDyRhZK2%dy40#eO>(Z|pVR{Q0wST=9kU*`|DYg*Ud8t$ujm)xm{dU7Qas
zKKyrX@6?&gHoyJj)-4?1es|99+1n47tjp0`v2v=aIKz#*mqD8E-LiVc8hbC=^vi|K
zzH8sfUEQ?BEceFYdsFW|bF^lgUAw||=I&kpWOL2uDz8aiyZEi@Va>zQw>K@m8~RuB
zhS}b{h~pRg76#6!Elc*_f3tn}>(6?Z{Z@#!?KHjFv(jMJy1TY)(WbHGo8MPQTfMHk
z&cC;>)J9|1ssEO?31^+9qFAE;UaRrFyk+s+RA=r#UKxSsU4JH2FP&DKT*zDgqW$mI
zqc^*LPMy0r>RQ;d)$w}kBLBEZeb6#4xX7!0Lux}?$=ibT<lNlc(v_MrTNw-d^!3)S
zTc>lr>TG)S^Gki1Q^mh;x|(d8BbyT$yUpOPh106*e7FDjMPBAJKg)aaVaz4hmDS#U
zTWoHd=Fi@^&Fp@{D))(7S)T1K2+Ov*HEZL-m*3`S`hG5B*ifB5Eo}R@U-p(I#qYN5
z=w;gx_T_eBXh1{pKEZj@zlYu3_16BDnP`vZ1sj8}+qRsQa(gOS@Xe4V+I{!wXY#S{
zrp9)M%H>J$TOOVpQ5^B)+S;QgYv$~(d|>Ho9WnpX+m<kI+4>Dv|8Fa~_I91Tqb&0+
zIg!|B|83+p++~Tby<X!Ba<47Zvf1aCx!>OW?b#!#-#7A^<5StRcO|k$Ghd%DuY2vv
z!-6rVcl~%$a5zT&&F5nUuP4QCle)zced}UbaQf_H9ZRqNI2l$eb=_pk%71slYzto=
zUjOYj+xJ(Eb_eI}ocy)tqgwvwnHR5pnX+M$^X;Ca??wNrosa6zc=hF+UjCQ=+6({g
z++DLFS#BFUL(b)8@)==UuT`*b6w|Ys{{58L>yovz^zN~*UUq-wuFuCCHb<vdgd7a}
z`68jb_-IIn+4n!YN-Op!+citLKQguN%DE!-`RJKnOzUoQ{yJoleDE5>?Msp6yX#a+
z*SvMSSo-h$ea7g><lhOa|Ib>V`82lJBI$3>rm9_bzYm7xhtG8EI%mbamp$5fg`%x^
zbnu4MJl`vG4rTwiS$0xCn)hwf+FN@S_D1op%A2${PF{DG{uO=EsmyDi`fcBFFxyI3
zZr1VLSydtx8`9$TuJn>wvoo;r+0D?MGO}-Gw4Y#M_<pIZe!sBJxw}`{59%I!{aw$L
zzb>zIUq+Q$l--Tnw{P3)L~q??9DjFfQLs&He-Qhey{>KTGC7gOzWVFd<iFio)9O`R
z%yN0-{hEI(Y#s9FUA5c0W#8WXxbU4dB_U@2H`!(%4EulkQe^n<I+M~hcO5U*{yTq{
zF*-K+c0zW;to*C%j%5FxvS80{o2OsTNv+$FZgAt(TP<Uci(5}PoIiNYAj{+Y(X@N3
zmfbkIXzH4UNim;JhdJLC542`V-2Za*<QT1ZCWYn3{R}LJ{$<t67z&uRTk~I@sl*@>
z{Ib2FR_{)!d&<fDS0A4noLxDqTF7JJjFk-Uj|T6GV?LVli17iB>)*Ri4=S=co!ql0
z^;R*z-H$8<t1WiE>c@{CKmO}ppV{uy)|+>1+E^T*rSg2&i?1(u%y<Q~J?!S6SLRwZ
z=j`lXAvb1Q`*%)yxq5PqTNopc#qX6HBV+!`-SbQ@;)?3+T_k2)87v=sFmX*{)6PSp
zs}`^34015?v)uRjp!vREm&E7K6sT=%^-!8SJ(Qv8LBX7_g-eg^(^X!ToXgks@6*kQ
z&ysctyA3_ghIdPTHn1=2KVEbs<ly`h;#@PAZSS39Xd9c#rnxK8Qu=wy#pG27n_d|H
z*VEkg{(PmUespfLuEn3k;tN%ie8sM0{b_kwkgO4)DPeSX&T2mE_%lo7nZ70PH}9LV
zI#=A-s_7zYaKaRiE63&seE#^v`GD+8yL-$G9mOZ7SaQ^T$g8kWo)rCMNw9a3;_R;W
zU2?IDUe+vB7WbLEcJ_HTfm!>jLRN(AW=yx2T{pEUC}``ahv!x;v^;vUd4B!lsM8xF
zH0_LPKYzG8{Y&iR`8&Vu(>&_AG2rIQOHNyMhMF)uxcJxFzW)DQ^L?L|rpxSWb;*0M
z@A_i%Z@H4bvf1SUJdb+hH{6w2^343a_ME-jb-ym!zWR)UtGQ14qd9j>4lK8P!BU`f
z`mNi69ZROK{dQ37h{K6HVy{)EpAj{h>9ywRb=QtdF*js#Z9P)Ej^?~lOyF+Wy=VCq
zeMJFY>GvV_UPm{nGH5(~^fLK?bf#SM2I216)jO_#`E-0^<~q~TRkx;iE?nJMaCMT^
zk2lM`1(+}TT)VUA$-mvj(;iMcx~w#86|bpk+ojvy&${wTYW_cezvq){{gq#9L(@;p
z*q-WAy5_8-VcBA9a16e;t`<L>px!(2X(G?_l<u#Qckbs{Z+ob^H>Z?in*!VHd3<u|
zNf(bWGXyI>KI@<<VPq~<JHba~5<f%qhU3*<e?PeR=wG+oDeJG@Fsb+dCzcs~-;B%l
zD*T*vEAPb5%e5ib#2quNSgtI)_<pU~;!oD82X6Y$SDxT8D>~Gs#y;nxR93fdwy98f
z^Q1N535GLt<lg1!oHr{KH{bF9UCfr_;oIlbt(CgFt>odIs~aa;wO*1~@~nL7-tO!R
zlaF<LGH82zG>KKLFk^q>57&J;rCi(A+)A2zXZK%@26Gt`+lsGebWL2N<!e4LY+!Y&
z>wZyw<49{p@Zq&C3ukoRXUy3gSX{=q;%JW5)N|XUzh2kUv*TYb;rMB0d7JB(dw-^0
zR_1IzZ^zfS)8$S~_<PsIXSXZPzAZ7u%l6*}!M_V#mIYku<15>47B>Ca@>sFA%jB0%
z&b|G8=JKzzIu#{PZTs?A=GsO<t6q?c&ClPyQuIwp`jBUGK>Fi~%)Z!Jrw^*ljCL)3
ztrWk_iY+=UcOyf@(Wr(k7ruD8GBnuNSiPTD&XTN{%qFMi^zcUQfqe--mu0F-S3W*#
z{wyhXowC=)mpgYKE|#l{^mg3;GVkcdOCseOn^w+kJR6_;-1@<rWX0CW&)(fWZqKjo
zyFOfC$%6ADelp_GG3H)7Q%r<9T_$f051jI8rHfKzz3&R=Pv=_~oh<PS>;HBw{fuf_
zM9$^2#g`4&Yq3f$&uqw*?E4&X+%5gfQbUik;x@(qmQ}8;UwUe0g^5t-vCBo%e_FA#
zS!ME^o@o&`ORpoVxY+FcoaOgT;~tz2d!BH5m97}WcGoqm2Zf_HbZlGZuX&A$rCufJ
z%$t*ct@|0mcf^_>nH;k#bj#AHJz2M}-kJVLN9a#r@RQCYKeIYTai7MH&2m%tEPhvT
z{EJw$(%o4n>D9#tAKaUkxv;)|XY6J6tGE1q{r|rq8*ha;h8k@wzxUHEn1TJkLvHo6
z<=4LK{lRiEeU(|)!oO>xJfinr-7EhrcEPp$MJroFK#n*5<Z#<a<@u(*-ZPq0jxm_Z
zH{HL(%6YWsYGv>_m;Jxr{eHiHwpq-RU8^UjUx(!Eipm)$rTvy?83r4uer)@_-wEVP
z@q^Psqjh#1o~A!V%x2-U>geF*V%dxzS{6N1``chGly}?Y-$nL^ORg3!ewO@j{;aA=
zx0XG=cyYVEG}}ROZ^`y`6*E@eKgPgtV&|5H@7rq4B-gVqWj<%8_Q**o?N@F=k+qPq
znMD!HS$>)R%O7(t^DCIj_upe~SQ&9-$7y-B#WVHlwpQ`le{k9VQuFuWl2sRWJW@F%
zKcimZ+eyWlex<$7ZHuhFfxNQ1-oGXu<loJGy{9y%98)lj|8RWrv3Mi({XOPi&xC#M
z{K3p%mMneq-m52(CLcVLInEvVSfnp@y>xourHxxY3T4js*YWtP|Boqto0ZAO)frL~
z&*jS9SaU8ZV|&^A<15cx`Y6l#Z2OBX*|Tr_nYHkm<qDosE`|-hy7})+FHPkyyY_tc
z`xiT-_bu3R*sScU&{IF|m$e(Ve!3TRJ->5SRIXHM*@c__|L=B0U6%f@H8Z<P^z6ZB
zYc!{pSMD~{Nv*8U-nr{#@UHK3rb@RrW!Ke)+xt9w_-@w6i?eGt{?uhV`(9w~thw{&
z&n>&nFuVHHl*M-JrdPj(`#Qf2Z&$LrwbCYaZI8aqjcp|tPVW{xA0T`A>8l#K4Y7Nq
zH}0PmpZGD)<!{2ecI(xbzr9++e#~<B>dA|Zr+|y|J>|-LA<k7PhIV^+8;Y~)DpN~S
zPd>Wa(LMKmZ^cTzXx_W5(W${(uIgPgd_Q-YxzEc<?{s&+HJg2P!WpyKXDxTvE|JYU
zXQ3N>Bgbs^-Q7t)ld>OIZn`U7#b<ujH#lLt_1gP4lIKTls+nCK{d;wA+3d5|ij;HB
zW}i(f*WGHbc1wK9*|g%Qeddc_C1h9L+AuZjy?uP1-2bYEo7QPJ-o?J%rL$YZ`S%pX
zU)w7xL$)6CdA**o{kHaH-*lnnr{9)c)ov)h_T!NJ=ZOKH@6D#NNA274r{MCV)b9)l
zv!ia_HRn%^UHxqJZ`tlEnG(!DFW5-sr!EiuKj)@}#IbD=ud}cBFX`KAs}W`SoIS_<
z;IwPuXY<!2)hA!fm22E>l&@QCoGrGwEL7b+;Y9e%d)@11D{o)ExcWhGmHyJ}B00YK
zIeKRMSFM`Fz5XGu_VnMIuCCdga9U*lmiM2tWDM?Se=WNm<@I^y!HlfeCtm3~SgpOc
zZAE>h|8es#Q~1A^n_Ul|{ycrz-n`&BspY%&T;A-xTKe|yzjrTW?NZM;`K#wfspG=#
z3%?8Ui%T=hPQAUNdjd2jr?)omU0GefXaDB%a|Pe^SG``v<6AC!s#^D1W|hCo&w}#e
z(!#V;Ywh{6qqn7hw0`&^p}e{{H#M^^?bK_dF!9-UU(TB~Gd?aqI=b(h*|hY%U$5Sr
zb8qI-uXmNtewrHIyXjTPl4sZF%e-5oe_qP`^t&(Tbk@DB>*U{~8@7A(`&j!gR@aWd
zzxcWCK$&DtW|X|?eS^;j&mBAU=**OVpHhoK<AK+=N5?<fy>ha%dDCj2eAnw|C*FR2
zacw5^{7buaZC6k4nfl#4JZ<l~W0q%ZZTD~5dA-E@wNU&v9iNO@*Xlk#pEQZD=3}ol
z!-JSxliRItaSC3Xx#XGnk@bIKuD2aC+Z}w0rQ+Y>e=B}Y_#x`N`{~TLMP?_suD0h%
zotW?ZC}xe&;$2FI^Ot(KxVT)|$}N~P^+{5oSzl$4tl2f`w|{wUU0j|wtrF>OdpPfm
zv){a@<>G>|YT}AFCIugy9``HAVCjqfUElt<$tf)=UNB{5^~<HxnK*a;Yt@lHp7ohU
z{|Unem*?kPIksuNQy04G*nP#R=HcAm4aJ&v<#KNFs!FeJH;0r4q-~wycjvl)q24jw
zWAoG&T`n(d(zU7hKFj$_h0P=5>-(zt3v`$2zj@K_;$q6bullTFrOl+rOUp|(PAe|6
zoxW#A^V{J5D>(r(UNj2)xjJ{l@rMN+jGtHB+y308{qVyNuI>NUUFm+O#1frkux*ot
z@zYJW{p4&bK0KIs)^zKRZP5=Z+dA}&4vI%c&Y4?e{Z^e{-ln30=|Ea}<?`p@W@UU&
zeJWU*|6TsM<l7gm4Z@=8T{Sf|HFs=opZxgo<Hn=X>?@nOt-de|3JNj?Y;H{7SGBxd
za@qFNmV6%!VxYs<FO+QDRFssItTy8x=I%HsCMYO)k;CwYl9G~=lp;xE<h0OivLr#<
zyuFk2uzh@%h4(%Qw^+MYkJC@L&vaS)M2MqG;fmK8#Y5sQUUKEzb}X(gN&Eg-f_JHp
zUa@V+rVrgS1O$2(r%ZL2I<e=#dhI8ijEh<v1SYn8)v4|FdUnb0gmWw-Z?EQ!pa-)J
z-tX!A|E%ak%f@Y8lD{j=lFqzpeb&t6;CiC5lhemyLilP=w^+MNPGFnGLR9`#Je9pu
z*C3owB`N)ygW-F=va<P7U5A{~n2G?;d0)2L6o?hsK7UtIR<ir;s=vZ6EKVmx+BfW)
zn6X*@|NV39Z;oE^zMJ>{)4T#Nj<XN%DL-J@zP~%;piQiw<1e9oAMM`R9_ZxVd^+O(
z0XLaC#`3(!e=VLYytZ+t#I>*oGS8GUUDid^zC6++@AP)^oTGmyA3L&AvSVxJs-D~5
z869|(gjy!7t5caAIKBUHf5-i*pSfy*#;U#L??V4?JF76cfjQ!X^RBds5dwnIt}9!f
z?5>FTf315eYlo5yLxY3JYNIDSb~~=mC@f>GW3QPvZ*#eo^{%sJj&6F*)%^vZILhm~
ztnH6p;o9`^)v<Z9wr`Jrc5%JXczdhxr%Q5^_T{C^Ce4hwC+x?$>0MStNKbG#$G%SY
zsrz$pXeg<KE^j&1@$198g7?{s{{;T1F1f#U?UZwRs}oLJw)<=n%t>Yb@oMfb6BXkR
zSDV-B%=`Ij#b%F^Dz25s?gwp<a^|pm@=d|yxSP_UKnGVp@hKL6J6xsP`_mZ%7epAb
zL@(5Mb}p)7(e=9BLLO`%dv94jytjMCX9aO7Z@1{I?eelSr2Us2TeE$a?=+Q`y%o!a
z+;0gOy6tLZk-PG5+xbMtOTNMao=mOB)^hDi(RrUE7#r60Zu#;B-R(B9_w9H5U}*{V
zs99MUyHnUTap6blH#!;H<)=P-GM(x5w*Z$<6DFO|oYAeIAf+Z+>Mwef!H2y?!okMi
z*Pn}$sa)G+I@T<>65<^tXcH0J=q^>Yt>f6^B=cL6Qi6=?a#!SIZJZXe%)gP>7kupR
zjh<8^8K!4S*Ua5RV+Fa>Uv6ig%eai~6O&V+OH=H5Jw>VGb5d*rrwYz()(F|1{6l=g
z_Nt_{r##voUjDjj!k><1(O+(9D9XAYxc=gWVh4wgLT=8A8N3l+J2Vvqn^Z#f|CD#>
zPTQZfqsmLmjrYF$EGZ|xJe8-H=fCsXD$Uuy(_=B~lSdz}dPRRxoMe=;Z}!}$953}m
z_deUU`^!|h#rH3mn(X|)Y-d={mC9QenPiS-dwTBe_#Nn~*IL2Us`sriRez6O|3^J@
z-IoWC827S8GuZ72i;i7zciC3`$^X~>oU!&xwT4qxVbvSw;;%2h*4(bin|YzMbjstl
z_lJMJ`hHg?EH><J^;+wwFs~oJtA)(|uP&Xt^7YFD`e_>;v@f1?sWE}&XySI}#ex^D
zZq2*aaLa!Aw(z`}MR#v|yo|fFEN7Rb_Wzh$>k7X$`<@M*{VMj#wd-3e%fBwpJ+)`u
z;oP&)(aUP1qNA^0n`XK@uebfH&G{MOZ)2~D&27v7cRYN{|5DG*FZa!ix@1<i%G=`B
z)oWp<<|aF~UNz1AzM_<I>ej2Sxpi^TF;}%#noZyOvog0X(%Rzgr;GaccVB$F<em3c
zY3a+e?&jTCu`-kQLe8<?t>-g-Z#`4KdGnj@sGaNYl+FKF5FH(THSJBC&$@M)+1b5O
ziEG!KeX;3P%%xfU6aR`HewJezx_tAF#kX^=Pc&P5Kh-REc}?B7<nQcnLLTqge)$<s
zz|H2@v##Gg5%gDLyQS&!eV@!_AK%Tt^>5j>ZMRmaH$02IbnV)ft){uPt7Grontt-$
zvTfTIS(bLk-dz9gX|HMS#jBh0zK8JhZ`*S9;JNM9vv0jxw9xA8`i$AXx2nFmI_<%g
zuxnf9I{Uu<wc*vKS90%Wb#L5vHP@>m*Ef3RRozp$E7ELbf86#yR&#6B$uGb2-a0Hc
z&P+Kdw&3iV%=TGfb|zPDt?YICwOBS*cjmge!F(p=d-t8o`r5p1&-EX2>)gz~OgFq<
zbh?-^XV%%(xo@*)Eqj}v@$FRQ{x!O<KRt^w%<-#q-|Rg5{>vDbSgFjP8MU#^zcsF&
z>)WFFSMuPxT)B){%ck;giL5?-wCrBw-sfcptdg}3PwR2yoOA2U8nf&_=4*E+E!4bW
zwb*)B>4vTQvu?=zT~fS9-nZl_f5v9(*t02C$EIr)Pu*&I_xrEpJ<ol$vyFFM$jw~e
z&YKmkb}YFpb-$sjd<TzEPN<Rni=W?4Z1}lsZqU7}Z+1PBeX=1dwDkAQEMMzeS9BxA
zbG}YF+|28IHR|qF6W_~xTU8(LY(01_(sWnC>D9j-m)V>8n`fP06&-GRJ^Q{C|A}9T
z>*IG^u28!6|4Q`LxoSS@`+A-4YQ<a?K7MePUT^H}i@A5N`Lw@%d)4E#`|H;_7u;8t
zrP&njzAhEaV_uQdHe>PZxmUCE*w+}>vPH-KF=mZUFL9UNe%fyRTltLN)wgzi{KvAV
zE!y;Xh5amv^{=(>$}+W`y)JvY?Q_q&-}B7h#;`{pwz&W9#XF&!X*?G%eOvQzjnRq3
ztE*mp+kSOz(^|Qrj6avm?%xn>Yc;-MwcG96F1c`luirNDd73+}wC$QUvFgH)s5Q$4
zA6(qJ#aDeH(}al^Z26{_9B$wg`odd0d8U};tb;MOa~oQCR5=+ZIL+90b)UW48oS+1
zKXP{{Ew*b+T>@JR@G9B#$)}g+A1uAax<7t<m%^*oUg0HCThDF06S?=<w~%e?W)^d%
z^3M8r|DV@u$#W<B?EYEC{Su1X)s|n=khNM-IxW0#M*IG&hDGzfE6aE+eYlm`?93X)
zYrh|G=+!6xFl@J5yeqlJX11AK^Zfk3fmhglY<Kqh?9I>Q{1|`8tUY1r1$LV?Q8D^$
zE01d@xS3Cxrhel@&tdlK1;%d5hMN}3e_?D%l?_dGwm#^@^zc?=_!ZxZ8Sb0~62jJB
zl0`V%7)9mN7P{$Pd%?9uqWogx4W_uCnO`r@m3YGH(J<$jZ9?tAqIrrEc|X5g=l7A_
z5wctHmH3ke=H8FryI2(x47;D6du6)aV(MDyJC!#tZp&Pvbk(zo;UaVYm4z41{jL*v
zzAH=We%C|yDN`?7GMt~*cz$~mzoPoR^>bZ>BwG$KEJ!I}k606Wk&%D(wCmjuUw-BK
z5imXC%JUnH>^#9QeWdPMM9=l($>Q7<XIfDrEg!KgIDm;IIVpI3)WNo6DWa>co|0Y5
zKi5HI-TZ4>ubGc<dsI#6V7{zt9mRJr;PmqI*&hxpwNlu6w8MRx_3G<)lI}!bU;25|
zVp+K}XTOGdP0zBAdht=h-hZ}PgX8(_Oos&b{J;BZ`R_uJ!yg!4vOLJ?F|vA)c=cJ8
zq0Zh|#@_Guc|u)xD2P5@Bz-gaNFR&icNfkXHx2D8SN@y)kddWbabwn+%2f}0t}c4E
zb!ESt%W|ptL53QvOXL#GZav?ct5Kyj-!9y+VkMtjM(DmU?boK;lke}+i+v(nJM&wz
zyxxapTa7>bytbJk|L<XE6>bN?&ff*E=Q;6JMfC35QN5c<>T~i6EgAc_H4@1iQgfyR
zWbHe-&}o|D^i`dzwT~t#&ipso`o{UhO#<0heou~95;?X}_M*dkZmD_mPAz{Q>hUX-
zXLpG9m&aj?QzF(ZpZ;Ot^*em^uSJ$T>R8@p!}PQD=0)XGXDp1@E6sM<vb%8GuY$I3
z-meq<WDjoRui7_NU~XQGm+A!XM~VU$ZCh<x4`(^-jbr@EyZKg#sMYFY;yDMKS!2Iy
zK0Cu$W!Ix$%ehd7!NF<C$7r^qeG_kdd18GhTwB|nLGkYF%lY@)wQb&A@Bb2F_gAuT
zW!RI?z5Ac8d3SCnui}2!U(>42zAf19cW@4Sex3OJTH&CA6(6s;-n_W@)R`Yf^LZYu
zzJFl%`v<ewcLv5>_;t&q`*INHOO{DD8$Ug|IF~`%enQ9-w-05D51!wC&_g-K`k$uL
z$z{tYEH8-QU2$Cd!JKtRd_tdY+Sl-^MlyK=tIOoxI@RNvDW#!qx=Npd4|G=KTKo>+
zdUxxJyX1+jyVRCT^RA0M&EZ{}>gu49^g~HV?tks?d8d}!FV+oZIM6I{$tXb5(EjF+
zd!p;UO23L)zf<<nwW*(eJT3hCe)4VSeP7~wWNmky=~4e|B=ohs-QFpQ<^2SQ_}OYN
z-?fJ<Qrg<_!Mfu)+llrD%e(sXopO_}GF@7nQDyt#=QY72bM}7x_>ePA=^51V?J`^)
zN2G)0mj<o~otndRe8J}T`}>b3>8htqI&tr)yX2qg_3LZDzCWO1_c#4Ov;7rWnWZ+9
z{&)1-9jae@cSk@dN5A4<!+$^JC+=$fzx>|uubK=e{6DG-wTKIrDAY=;GyG$=|L=an
zKk%2xPLY4h|4aTq+ICe&?B52f`=WyDe}9}EUGYW!fZ@N7dMpa_4_*H+HuX;B^a;NM
zw{mx;)_th{vze*B+dcgJ{*F8Mug%K!Q~a9iQx@KGSEBUimRt9<<$T1V{C+tv+#d9H
zTG#wN-T&8r%RJTp{l243-|YHs_N_KI(kJ}pJfi*9=>DF~p!k2)!*gEVS>vJm|A5`P
z>BnyedW18uuAHw>E-wG~e(&eI`|Xb|iJHx=vFv02{)6uF5942{GBNzf-|y^ssCzQQ
zxqE$in`0|A_$uaYzw!2YvVBy_o~8XlKi2;b{9CQpWxx5>t8cUKf0TItlVJ~2;4${C
z8UcEbelGWL`JjKC<NuOWzTKLW#cNOedw=!tw~PN<lQ{p+aedN0L8c;NHH-gzr+|+U
zhd%Fry;<%WZ`HoNP4-hh^8XL|opIcM(uAJBd)e&Q_=Il1zBqqJxI;UCo#g-Y)HM_8
zkK6xIexh{A{>cAN=Qqq<5au7K^|0La$2$Jczg(R!R&lJ`^s!gwSpBktU%pLSJL%?@
zxyrdG^9)a}lb*bG&-%4`S#ftea{acO?Z5Ph*V6sgvsGqq^LSQg6lY!jd@IfTXJgyT
zvgU>F&xB7tyQTKKtGrvR-P&#CmFw>=X?y3jHF_DN(DyBKue$x48<$&o*gz!lJg6k(
zi%5@&N{u);_msBpoLi^-N~e9A_s~_ct$yo5ZeL~9SN~_Sowl>K-gURkarUh(de1&@
zlHXmvV`=4EshnGHqMlFJ;3?|)9ww5Sn|(9Ff6uK`W$!DqwI+X>x6LHBI(UNb=W|)N
z*~Qjxnt4-lhg{YyvmZap_8Y!i{nUEXDrwULiK(l0+2()cSl947`qrP2WO?7S+19_0
znU^^<-~HpIVa2Rw;wxRgr#x*1tH<>ZC;DVr8#mg!*zEWE@SpLOe?r(d!S}o6Wd&mc
zZ0=u5HM(XNo!+>}WLFV~lFEUd7ph!xl$2hHpWj{*8T%<=HOGH(!E>SZqCz{^U6dZ@
zOZmH$T>MbuJ^lI%w+Z(4b#hH2tr0G7YAwVCpBd|Wt3LVk?A%GUCJuMTn~N4+uhMJW
z!CstLQQ@b$>r2JHrQR<mZNC{Lz^gd-@L^$w8BtDFjGcy!qNd&H`)+AoH2D{Guv{*}
zC(_=fqUZ5P;fpsuf-F+y-?kz<mM!|Jj69cspx{gB;KM@idk*tJOY^o2nlX!ANxy17
zKRdheNppwa<z8v?V{=)R7M(sMlhc^~@Z-+P&uZNDI(pG3KbwmRUd()y?1HkAu$d(~
z%kWh(hp@2lp%}lng<8B#skhZb&$ZMF3n%R;u<UxfDOX?c;>|0HH-frfzL*nV#L=X{
z(e#3|MaXigS>T5w+)EF2ovsS&Ub!^JL&WCdBLlxbMQU<apQi5Mwzq!LlAm;FV*=O8
zHD3ExI`o|OWR*GO(wbn<*0FYqzs?VrKoQqKu9nM1ySHlZJksPZ<hpW_Me3dXZ<kB0
zJbI<+y!c7c-6s+j2EEn(dQb6Z)4~j`>t^$7gNr^|&VM1`>RDp3#KGcjmh_dJghO5S
zv77wv|NSN;c+q1k_qHcrn!W^CyzhT15*ix1HN-=AMQ6B5y-9v;)q58K7tcv5jxY4r
zSFM`UwO9JQMlbhe0r9#rk;^B4A1G9t_&Vg#S=J<l)}p1C&h_wayE%8#s>M0JmTmLi
zZj;nK#vI?N^>EG_4KKr|C-*&!KCz`k(0k{G_fuC0ojTREM&sxd{ol*<XH42XD{EQG
zB2B}%6US?1KdCQ&W^?@zYrW0#5HGKDE=&LH&foWG>CQJB4(o0e_`3ho-6nfo?XEQ%
zturQ69o{}6bL-}}_nv;`oqJW%dJlKqY1tcZK^}XN>9#Rq%_sND{G+@(!oQt5#?mf*
z+3ZHz_P$l~zlX<cIQwo!P-d*JtV3n`HMZxQEX$uq@BOg)RQ2h5E2m!7WVk%r{n?dc
zo8B&RICVAQ^o%D3>DAv0KI|!fosoTu?fR*@$De&p*T}D_PMlG;#WcCOcH<`2x68N1
z{TF!<W3<*k{%!2Et98Y<(q`Y3D=WPnU&#1wYxAw=pWf|}opCSg*3DVVrk0B>?|r&u
z|D#R5`P=SS%5Iz9(c$N~+B$k^j>$)c;Ef&UOO|`Ybm-skuaoqAHQ#T=(wd}mk7t0E
zqW)EU-EQfnrNAXDEG)b)<gcBZ=KP2iXP$jHbJW=L{*fa`S{`tyq%N4^-NGd2`N?CF
zhS$G<P50io=(^NC(%x@#aPjxQe2xM#`(EV#>wnhjeA2C1ZsVt(ljh>*uPr;_>Hn0m
zM}Ow|mcLhX++ST@D0Vq<ze?9670*ff5?Oys@|Ik2GE#S4{P4ya-g2R}@BSUw<ghDq
z@#1IBlk8g^F6cA0C26K8UHvqNBjnw)Ew_U+Vz2mm?L0D9xH`daRqewM`V}8EazoQY
zETdVLG=!{g;`4VnQm7UhVD0-hSX0{9X3Lsy#UD?^IIOA7*}Yfx)TskC!CtPX&u}+}
z=q)@weU|?cuY(x@Ii}2lf^$WeJy`u~^7cK(*~~Gke~W#*dGVSE!~0*2%QCOte`fam
z%&T(?mu0qFYsVe1+aLQkGjG@C(j6~Z_efv8|A_td<%Zm}+V>upPq9aP=UFqnuS(6T
zEWh|N?%rCR<$LxUCT~BVV_J74`pyYMy*~xn_xOI-JT0&PnUH*p?|G7G^wY!5dri#~
zzWeE~d;jL``&`{>#@{un^PlcbRgc+PE!`gd`P;-hvo|N~xgT&Z@{8WPDW+@p?9Rv+
zsknQfeA}tr-RoBJ#?HLfotjlvTAg2?Uwkoh_C3Aw8^O8Vx8}6&O<n#l%x~=~U(@?L
zH_zI%|CQU<)!%}nv#OUbkKLM|v48K|)2lKgXKyaEc)p$Q)U0K)Z`b<Wd=PUdb35Z#
z-kbBbn&-B=8r{38q$IUltbCi-rWz&-mDSf2nw&Q=dO2RVIU(5N&ZNX(DB!JY-Cr-4
zd9!4h-`V5I<q!JQ58JUTcocW0Tv!&}tv~Pl(bZ=IS<X8hsjsoVxAAFE?ZeiJAJ329
ztEh2gVQ}P9O@8NY&l~>kIOigjE~W)t7hNnKeE#t)>7%5~b0b$#hm{kmSuU!Fy;JNc
z{+N>EXZ3el!qS*c5<Ndy9X_}p*1O}sr2XQRpHHT*w+YUT{Cg(6?pHv){L(O;<9!)g
zQeP@-xIg-6y%N0je&sjU++|u?3Kn0EYIZOM1kEa6`+&2mA!%FT<<%<BQy7*8t-O5Y
z-<H+izUpS|-Yc6`DqN@-dxJyd-zV?$7BYwAW4e_$1$(gW%5Yttk`!rpsf4|+qvPCy
zhdrC0a#m%j*B%u9!pMKA)i2yeb$&I=?)&leTtPdlu5mU^;`^=Iu3#a<*KScR9q=Si
z{<-GPH_A8u?mMO|cJck@$B9<!<C{djgy?5CX;^AEGAR6N&bw26Se!%Mh}E@qivX`@
z?7H#_uboRa39O6rwtculoPScT_3fD}vsSv<Pk(uC+SRSMY@e?d>wXc>;U)Vmq}=tc
zc%kCP7dHPgEv5xCtSC~G+E>fuAkfkm?7r;px3X1N)v^>{ecux~=eFe)FV(Gk<_iQL
zbg;N>88zkd$0mKLtj!rpN>;{EEYW<Pn;2DZzFM<>+7n@iFQ)Il-QX$LlHuF^buQQE
zAg>1JD`&HIc!@p!w|>v$sgGJGMQKg-@+v#VR#Kb1dQ(BWUA&liKu>wZE1Qph-W{9d
z@3;5!^y~Y6^t{NwD_vhQ#mA;v{Z(<uPo?jT?JHfbpPhK+%^l<V0O1XCG7cZqxo@^U
zQ?p-|l(~QTE}g8yDpv*mt?c5ma9O?Evd>}FhRx4Tw$?6E`6(6@lvI3=Z+6JeuUG1_
z>~Dqsj>@~8m%ltJS82J^`+Ma&s>xHYB{Zo|@%bTFvq9kG_WS3v6a~YXE?SyhS5mSP
zk79{#(ihqAFmc(1nsO)Iw62Egg%_hF)Z4n#SC-s)^=M^$vvU!Hs;l|xRc8P6(kAgg
z=sF_ytEwS9cE`hcezUWygxl?>oH_OC;=gaV_B_7Fp3kx?tH92sNKI9RU;6tpuU8MB
ziO4M#mR)zKw8?&B^mMLmH?j^U%I3`y+Il;9ujp0<R-0w+7gQtd8ZW=koG550;Q73}
zOX>8{8a1hg8lL+xwuQe}+GYp8^*$P77Oqoz;~wAETP~rWj1+#AmflgUd}DDgI>llB
z^ctJioe`_|dbzly`>a0R(U)NJ=-A$f%agTLg?;63KNn8?E6fvnT5{_QU50n8@yoRv
zU+`NL&dImQ3F?mAX?U}wc;S*Mem(b1-mN|HbI#9&OC>n0davuK##^*yAH4rF%|TPT
zGi294OPhlpR-0cPTKwnbz1v#LCckRhID4i9NA+#~9jQ736@N<Snf-Rsb@@~La@+N9
z->O$_UsT3&=(5GR)K{OUe|o7jhkIdE%Mz_kdP2cHySGj87R@o97<F>X{H&;u@Tk!0
ztpeQpHcgmfotNJpm8)W5!x#KwrPe1yg=<Wqr+ou9ZR}AN`8qrKlpVN&Yh8J8&%W80
z4nEr>{B7pdxy@PH^AGRsbrsJEUcGCd?{95AhHo#g-c|O!+*elpvUi7JZgXy0?fNyD
zPY=I+nmK*#z5LaCwm)H+(>;~1qy4tGo`bzjaOuh0sc$o?uf2=9r@j4s?+(lCH%jR~
zF_Cj?>$b1SymfHb?PqZ-zcpXsGfT@UD1R~EOl9k#`|*X<UuD0ovWzTe-ZnE#d5)=g
z$IPb|(NFKXhA&<}XJy2z)p?tjTZwJ86#u<C?#8m~-%o?eS)H8;^Y3P@sh7$S`F`=)
zl(Sp+1iznT^?J+soGaYR{)Sv$^vbyO&D`=0mhW4N%W|J@n6#{B$7ZwS_TswLtKa6v
zhfQO(-W&J&*RH)!oEBRz`l=?graIR*HkkcJoRX5%*0O`smSwtE&py35Zu;IsFXzQY
z-Cr4RcIvlw+-}~6+_dE4%3G=184LV$^WIGV8q7HRuIc{b4VI7Bd^^3#GF>Zt)#AHb
zE4RxwoP8O4=f=$$mttR@{w>`dXU(wt^3%Dok@HrayV<c!Y;W1@yDv+srf+)}trKH?
zCvIk;^<2N{mtTH4w=VCx^6IxYtCFt&Id}2ku`QdY1-^gv@8Z8_r~XVi{jz9hjNkIh
zwwpKIt-Et#Vdv4LTMv)*Y@Re#^KNNy_>2vf>2-DIBep$V#<Y=R`kb$pJg*iu?2CBw
z)oD%E_T^iyx#qsjD9^q3y2NU(-}3CL%;Nom95QcptP<D1fBfm*tu@zEw_C^RO+Wo~
zZtPvV3#`0vm(LPgn&}>G>{q>4;BDFN-GURN!m87k*5vqoKXd8WI>m~d-Fw4QuV%eq
zU%O}jMw7Q?w?MwgGuK;_DQx1ay<O^L$%MD6N{c4Wx?tj4zxegDv$M_f?nrzoi>#lr
z<bC&j0ki&3+|#!hp0eQHuP&bF-@D<7cjkZjJqy>#iycZ|VflOK%1jp*@k0e|buaui
zrTJb)aj!f&=gzXFCcXUMMFa%{?;n%QS?Ogb+Z!5PGyT)X6X!#_#g|_AQRpuyDEKvZ
z&cSJi<vA-qam#s5atVw&@$=f}n;T4y@dR?;3H}>+$uY3zv0TA_=}BLA3wCzA5ZYmM
ztdx6RfRVIUpCS7d*>@}db#O<fCf=E;ptPuPbB2Qbx-|k9S0*x7DlH05E=<=hP%e0N
zQ-R^c-7_0M99Jqg7Uya`Hn;ooWUr;*-i&w3oLumhCp{bJ<gdw`gx8%l-)-X+6!v}B
zynois#l>aG<%Q;tCO^6xy^(+O&GRB(IU80#;?`&1_b2Pc)^O%WSEDAK5Bm7t)vl2%
zX2QcG=i4r+Z$I?DcE)d+1EJ@?ZV$@euNC{&xX`~F)InO9Ri5tc`9I;|(jUizUbKI5
z-yc^0H~Z`2`Ag$xpQ)3me`>w`N!6m=_I|eC!ydlB|Ebq*^Yr##H`^QY|3y^lD*k^Y
ze(L<9dHwYdejkioy8ei*ZdXS~N88%e4PTdhczi;7|J)eQKc#<8>xbk=#@3$uf9rd3
z{@#SkONHbACcb<7dQY%XNdM;dOW$>`SC6lDWH5Nyz5j3O*LT$){pWv~w_~|0Xg>VH
zR<3Pw^)h>xK6o1N#I;!BX{GM0KePJ%dE8$VDh5_0eUF`<6>kw&ceVNa<(ubqW*yn;
zf9LWdP~Y`O6if80<u~sL?^w5A!_0qnjipG<%!AintngaM(V=g5z2f_WB^t3u7yIid
zE&0}29VG(VgXYkkuzHDxdV}*Eo4a=e7#^H_uBG7f>b+*1=z6Apd;PDopw9a6^+Vnf
z^`G*!wln_9_{+)LS0?^cxA!!$O;oYE@8|dL?UN;+mcPB3p8M9mPrcj4rR3cfj%_lF
zG7c|SeQNk2=I!p)|F+kMRY`k&dmZ0Xf37`1x#X)QV}ShY+Z*fy=P^t^A8E5Ucm9s$
zuCZn6<@bv8@2#xc@vZ#7$j-0J*V_MkeJ$R`y3IyN@Z!(QN;ib!czzXrKX=!E%KE(t
z7jwGZJOygy?r7Eg+R3%?*0om~mFycoKNWA06aKzsh4=Zgx4)yK|A+nk@J7D&A-Dea
zpC>%JJ34k<d1d(M$#miM-PiM$KAOMp)bZBkxtGMhJ?uRcE2&@2z_8T6F8WCE!vtNY
zs!u!rR0LJM%X)r9R@~L<{J)D^v)j(++6xH^mM(p25glHeuWGi=zViR<i7)P+&+1(%
zFK)k2^yi1*grHrgIC4tVp6~lQEqtfwztGYjZ7=%m#MaeoNA*_O``15Tzwb+Ue1H8l
z-$&nqJ3BfuuG})2uwSdKZpOF&W}?48SO@(vWcbP{^QgP=^~Jf@<9M&g>)Gv-{^S4g
z&*S6A8S1|Je%u~@G-1()Z{2$ejW`~*u7CRPU)GPk9aESJt``6O{d4>J>s^0VY1p-U
zZoC(|CHD~@*p?$!U)=V*s{Fe4%j*2C-bR(Szq|X}W~wqVSj5%Y{+)b%?J^&>Mf)%8
z^1V~31xh19yUUe@Kxwl9$LNUgth9{m+Rx9<7N)j#_?<<JRxC1q)En{U%4SD~0%Nh=
zjW>1_7fRlB(GlV5wH9BlKGmz&n%l)?I)^;ic#Qp!vQ4_89n5kL3@is2SsFzaToam-
z#i`=JQsYpzMRK1>h)SO0AL)*IX3f@;%m!FyTot=Pm04&4t5E~j3J1XghJ2>Zs96>Q
z%tj478V(FUv?fSrPSbB*-mzSuwkL+=)b@#0a``F~EANCqnkNR@hI#m!(T$)+h6fCr
z8kT=s%CUrTyJ4!!bcJQV=l=@(C1S`r(Z2mT7X!;b9%FyOeYbZkyip6)=zQJi#wjNL
zMhOKIUoXbSTlWhU*3DL7D07fZV$)w5Bd5;vOlIqOCb4<P7vEp_W6N`xgV&{Qn99WP
zV~yHR#`^A^UIz>XWGtem-wJ+G$M55Gg||t~vf+4`V9;-<dbb6s8&sJYWY(%}pTL&m
zP}0C7$naFN;Anw=;0zXqqpu#u!&J7NOJeyM7IJ`H<AC7<HZEU(iEamx6HJc^K6{jS
zVb8KW+f*Ld1zd9VV+vpi;NIzzqL7et&b3x}J%c}Q?v1O*85GRS7rdSV%BDpGvZ>Jx
zF2?;VpLWe_%RSK`@4>+BeENoJ8EfP7kNcROYA(6;Z=&~sl&$WG{GHWNSC*#l{`Pn6
z+WOUX72o>zeQ2G2yC!9ctBXr)R^>@vCOri<orqG8E0Y@=^ezQ8S}I)5)XP%-pngC%
z#p{DTKSRL8f3|b#FLg|qA|%t7#kt-8PGR7c4{zjScc=Zh^G#V$FfcsIY=U@0OzxJo
zNpDXJO<;J(+!v*z%3ODVd4<EOZ|e;%>BKYf@rSvp*sbEd|3UiBzNRN%vu0}VKP)c%
z;qF_l!rv=F8+5bYzRUM$;5pKu5Kw=#oBzfITfH8}{)XEJa_{!!SlO)5?r2k}X>nj;
zXnDTzXXzQ=Fm<lU1x%Mx!aJ>fR6!ekUw<(0%#hl4MI}^vVt1R5!;?~%HOnkiG&bf5
zm(TNZadBCE<)P~p&{km+4rq;d1a-^sg_dQRzs{TI-;)Us>v(bH&W^(5JCO=XyL5D_
zl<##M^|O^`VK7hL7@%SDE+)opWyq_bsWn<trOL%RI`jnX!0WQ$E3Hh<B&_DJXy8o9
z>)@7Mb@|Lfrj7$F52XL@>gecraYia_!&64D2Ji2_oC1w2-p#g{ApJ<I`pTTcai;l!
z+DZ!;?rqCF7A@uC;!?up_FE#5LB(NJZAhcU1j(0L?q{~RHt%3q>geL)B3oKv{-}XP
z!TyryoL$}9L0QZsNcVltN(TvnZ1W<g1}2fL+<8q7TfS|V*ND<RcqL;cL&pKm4|WO+
zd<!m^rB@zc_F>>t;QNtPe|l>xJENcgqx^)cXCs)Lw&rv@a0Kku?bVW;vEr#s@a-;6
zhizGHSMBDDO2$TN)=p&;6cn5rtlPX+V*+c61KTGDHVvkIQL~rdW@r#9;8@WhuVD(Z
z?<BiM18)Rd$bu`|p6=kOVV%&R?7*1v!0rL7R|AVi1A74j*8&E?2dj5gtmb&q=%oAE
z>;2h>st*_nn2jbdZ91Tquo-OWR})DE_8i9V4Ib~o9)BKwIzgMgqk(}zpmE8@g_DFk
zuBt6<NLDbtl5>=i!SetkhXd0F$>nm_FEMa1<|)Mde!*PSz|5e)AoyTgsLqXfEF4?k
zeq!WySQRF9_xWZgR-p#|8O&)7G4IQ7fg<QnmShfVW3>ar2?nhV2|U|ucAYrP%;3Rq
z8f|%iuVZV!Q?9OP<l_(qy9bGHIp;Dg$-X#gaapwYOKs_QQ5V<}7Jjb@^Vrqu(X*wa
zqeE}zw1Z(XHyBbL=r^V}Y%ugHkPyCIy}$H|+tZD+4p*pqW>{|(dN(D@vYx%;deE!c
z#a~zb3=8}I^G%T=DE>EYmHws3a^irU0e?+`Ow1{fC|UE?_~sRNCTd9@w%+>o%BkMf
zUUHKfRv+zM@i1$?KWM$*7S3%-TRDy~FJYWsc%pfc-l`QPu5V0tOuYSVKR3hiUFr3!
zHWtTUun=`%ERdAfx%Txt!$$AMZ9m`4J9DqY#l=ND<aB~Iw@Oz1Y2VskURzgAEfjm>
zu%de^XT!0Y>N5-s0xLl00z`1TE9Kt4;?5ZT_U2M9m)`Q8MGdj#%XN8e7$$A)cYKhT
zyCGod?u+++U$dM4wlp4`nCrIkY)f)jXBIV8zC&X1GzZ<VAI-Nc=J(y2%`VThpJmCd
z6(Qdne{XdZW>CrcEAw<);sll_43ZUW6By<frmzTVT)Q_%nW->An&a9swFcJ*`i$%X
zYmRo<DO{a$IIMBvs?$52uYZfrytT;e=M{YyCNBqu9}E`jp6>sBNkK_z(dX4qIX-dc
z&gThh3+a&9|HWkM)2zA{^XsL-RhJ`Hb}ke9xHf7Zx5KH5#TpBL@1DJtTUXAmEA0OE
zQ|X_bihMtpLA>DC`|WN=t+wQR@331=KaWqDX?D)r4%EDeIhV0vDO2X%wF@K`nBDcT
z=7xz^RST9by!QW{q5|X5gKQJKqHQBr*Su$RI>4mBprycA`FO=D=Zk90vHNU}7i#@f
z0lRd2!fEp>W^Na^tvxh(7hjw5B|GN30)DFVK`ElnH)Gba|DgE`^cKORb799fe>gka
zJpV|N^2u{g%Z$Z#2i6`mpSx=Iju_SY&qldAf){Vhy~y?nR1AtUqaBg3_p95MB}|+O
zq19*SGyKSAz7WpVrorf`5L(@s@RZg1;Iz}s4J-odb#?Fkj$WtFB-+_8FrCq%Lhhrb
zj>RwEJC_%&c>PFA)8n42S6db9Dz1;NN18eO%!D+Ilp>$Vg^P>+E^e78U-_-G<HZ`u
zFXyK5csPiixRSK;)Nl6tSN5u?^BrmMdE0u8@xf|cwjHaM_cK{KFa{lv-n!i@Uddn3
zU-6g3PL3)0%3p2nc_@9}0q!7FX|Ah~G8CQ3@q}Xv2NT!6SuX3o9XmUTC!VW||I_w`
zHPV`b`Dzm%y`I_8p*O#=NmrDEflq<EA}hYjL8?GH*sX*!Y1jYRQyXUJ)iTUrJhV1m
zs#bBTovV-Ilk*REGBGsTA3hV@@;*x330&=0X|L1nU|FrHs3687r>qvPzHD=aN#~LI
zA@AR_G0k99vYcikcyXz5z=o-;a!iJ+3!el#EcjNw=bO(4Cx$n=_rCBbu+L#A-jy%b
z;C^hnZG6Q}8$XsaSLerZMpVf4*R?;oJWu%h7L8XccRb2hURSN7!Lfna>#5m|;FNlP
z3x%ulSGYNR9_{F0@}Af6Vv?lB4KK!wk7?5NufH2kZ+LtycUutyL*VybmIpzs(f$*E
z+Zu2NUSHr>#L&N1@8?^P!BT5>c&W-TAGFVz`-p3SQ`$*k!B`_^)@UP!1=o*V%RF%H
zm#yVg>$qRhsZH;GdplKf#TbemQen^t>tAq7{at3DiAUkm_lKT2Zu#W=kgMrD^Zx6u
znOa4v3>q7sbav>?ROJ7=fJyEEqYs1J>b5Xf1+J9d@9R3w?S2&N5}NW{O0-&$V|iBr
zA6LWj6MxvY&u3~dXpuYM;!-k?M<mCSp=bRvu?D38rafWn*Gy|{*k~EP`P5b~`K2p&
zz1Qdb$o1h$1V=xkLr$K|b<INm?nVE)y!8}5ocE}eWsEgyZ*k&~liatzaf-{S#<TWp
z>l~6`ep6&{*th$L(F1m&xol^-7!2%8rZB#+GLEYW7pRb{;Bmda!(ESY^47lmyC5H4
z2`@akzuCUsg@b$YGtWgWU#>5#k^Xf1L=3xE!-+}iO1nzfxVAMlaCej%>NWGQluVq)
z#Zp?VxobZ&Ll1NIQpV>?xwbVNn9rbP^tHNK>(c)A&;8QZGnX#W-ngyPTCeL%l~yIg
zr}qLsc!d_eI<Wjzz4Hh2tt|Z$FaOU7m>6X6cz?|IjLr@YX0~Xi39Eazg}&E~U=lh|
zdmu3TwjT4pDB*P>Z{rtEi(}lk;`OB$3}KBfxs8?&%qDD+ihaaXT(Ln*>0@B-kGA^{
zzKN==zy6Es4_~~`f%5IEkGx$z$<tp||3BZq=nsDkLnK!^eT{$k{pw0p$%7@iJ(rhz
zq)wPV;m_mC_drX<cRRj^w8Ivxn>Y=%8Mf_~Jkx_UrvF!UFgd*yo6e9U)qZ!E$T|h7
zrVoNloD2f<jz7C@7+&qA>T`(GV{)wOJA<h{yYzo9@2G8YKk#<<v98$N?AkW{3mSH^
z$S^Vd_{YM!f8jh~!HcSfE$yC8mp3d`TY0M^W|~acVJnx069*)%@3XkXZP#OIXHmVD
z`{-Qo$t9;J?QaU%5_?q4CFRiJbJBu>bDf>#et}Pf`GTYSRBJY2zhpPBsdPxG@W#UQ
zhm$~Q<6_4b$sE=^mbO{EObvI=%5azI6qy$<49K{%)53OTNEW!+=kh~hBB<*RJ5lC>
zB=5F)C(7@CW@UO*J-@8xtrDo)CTZ3p_+-Aw`+HrrGtSm6Tj9?TBN|^}`Qd4}^ZLC~
z0_&L=<iy|o)B2Zaw%kVW!;+TgP3!kh{c&r0^uGS@C(~E{_^veHfmNpY`MWz>wME*0
z?zQhc&lvMHre6E&x7C-f+JQ1IC|XuIzR%HoDX+6f<bMR$-++HFuD@Dezqann<}cZk
zZ}LB0U-NugjOVAD?Zx-Kr#9J7sh>El{v-F#-}?^r?|<Aa?zMJW#rNYYpWoB^^EY~*
z7^fcd*UkLQ_y27C6y@~qsQ#4suD0_34}5RleKz0pl^S$BCsA7CMpe*{!Y94={nn}c
zv-<Z`d{z0vb#~9|-~QgYJ#NFxOPu<9=2g69Wn_5pp;ajU*y0?m?>DLzK3Z*mW^e7^
zqWe{qb87WV<7;dqHMe-i|9Pvwy8M23{jVk8p}noPya@@fKOVmr%@xPz8fW6}Ht+hP
zlk0!3dU%~XU$p+)wB?2$S3Tb8`Ji~I>ju|~7!Q$oH)^jhy(Qi^J^t&1&n4fCyTx+A
zB^xM!_Axf;e!ZOYjx*+Z{FaPb)1O5eKZ?4=!uy||mwUWZ|M&dY^;gAbuM+8M`0=RN
z>F;XKz+GML^CMh5;3hOOHm#ksXbuBk;im03r`$hgztigX+Vwy6zBV7)Hm_zK)1f8%
z8rF4%Hy)oKZBmjA8cqSl{|DZM=8Nu4{?ort?o3^udVl}?JsbW^p0DELFEPJH?Ek%f
z@AZF6Us=7+zId~^=u^JB`c(Ve^LE+U{|jv*Rg@MLr#B>=R_rpXi3*Zq{(9o&s{e22
zPrcVR>F+P`$Mel?R|Eywcc{d7Jlp?t_nBm?k}|Y$ohi|vn(5Uh>z$vcRe$vRdU)&p
z-^)*|wa@+gF@F2MM>h?hOzh}5H=nUd_u<h6^5yUE{B`+xi(8ldY*xUf`@hrPyt=*f
z{r+37kGy@!809fJk$mK&zIvSa`nz67?Q5_8*>S<gvtD0l@2|3Vzt?*)d{Ftn_<d@V
zeNXtaD#$QTU+#`9wc14adm4A9ek@ulp8j(3eX)-*77^VOzNlWaD?IKx@!aP6lDD%S
z7T@l7adC;2%$T!w^}g*w(%0wj`G3~q%e(ZgY}fm{<?naZ{LnPej9q)g-|JWP{hGxe
z4mG{^)SK-a`mgp+=0>Y8ho8TE|L5xTf3IGDJkNIWB&)II_qE&ioLc)~{i?&}F7;nF
z7W|FAnB|hKweef$ZGTV)GEjO$<DXE&FNe4M-@fuj`~8WJ`WaXFKM;uLiRpj0=UbKo
z3&YpRAwS+dKXCm0zV93B&fWZ_bmX~#rkRx~j$xzeul#yG9J*dqUvK&+&c%yy$E%(H
z{{FdrJ-a{ttm-wh!gg@SH_7=$Z^hNmucBXu-_J6Qtgwta<r;n7PO{^llW|QUX!wZj
z{I$yG6+gdz@sHa+>rzP4TOnwN*5n0f=(wX}1uxDHt>mq!`+F*jV<Ht71s6X))?1j~
z*zsc1h8MjOI|MDh<_Iu6$$J*@BYEQPncS^TkIx-_>A5uM@i`{Ji>il?gZcs(=V}GC
z<16m8^{-be-QO$v|7!l``F6*ysxLi0q2}O^?f1Cs%zw>^FInoJ*LwfA!FS7s)$?BG
zFTGb6n)TQ2@HgmyDR1a*>u9fE?A-cC?WZ}}PqF{C_1Ek8)$)IJ{@zOYcKC<({hg}e
zmuu$z{MdgveE&4><xjupd%b-B+y3wW+q;u5n60zud;DMLxip_Uhts<5RYH!fZO``X
zkTc=nJ=&V!^kG5<hg6fmvE~a8vNmN;c1$tQnvvk6c&Pb<f>42R2j4m-sTluPNii1^
zY+^N5DBUU8cT`sCW|!{Cur-@KzW&X5|8D*9`O)u=?=4?`sJ}Qn^f_D9fBVh-ToZTl
z7OR#2__cNCOwM;}CA399Z|?d%i;IDQC+hl!ry=G+{$*R{7wK=BY<K>6a#wj)+QvB_
zdgo5n{1;$S{cDMfvC(EbL+$80XVxFpTKnw(rS$9RHLE%@+{)@Mty`0pEo+?f{?Wc=
zObiUn*L8Cut7k6KTv(x1P<K$%Vsd1^<k=sp_u6M3T~b$eZJo7JR6y~<s}~bPi$kAp
z6a2QFufpl#f-Bp-+{^YKt@UMPU|?JCePdJh(oM?o?aaT97Ds8=$$pBl(L0y8RY3pR
z`{S4TZ*DH--4<ypaFIFg>z4`3ev4M_zptqHRqtK476ZeBCOzpV(#tA!9$j4jtL4=K
z1M!pZ_m^*ZpFV%OkmA=*@e8b%=XI}$`fcp$8t$^D%K1snnYWQ^zMG0NFi7mNv-|tt
z%{tq!HWd$kDi&#fGWq&)+5ChzOMh1XynlAf#_b=jZtjiEzEI0#{@}+C=hGjTIx{e=
zTjG7=(~Dm-JPzmZ`<}Y;C++du+s!2oM_%pVc>2+`xO;PXcI%IC6S?>H@f=;<bt9~L
zPN|Q(%jdERv8%gxtY7JN_v7v(+wX6+`S*7Iyu<v5--$7NSo&g9&kD9>%a?pww<-Tv
zjqJAEts7+nZ;P!Ax%<KU<M~yY$7^)d>f}Prn}XI{d$sMw+3bv&?R|H6OLr{U+x>f1
z){|aeoqd&;xdI=5e|LxTt3)6FLPv%J;wx{v`))mXXN_Ipne^<7cUr}T&d)fy@=9Qx
zaqgUH5oyj(woSh-xZcrtQk%`nFg{fg5y6Sa{+(;An0$F{%abeox@X^q>gn$*(b^)p
z-`w!y$sNxH7#g%+?n?JI6xtb{_<Z`#kYz<zGUT@Ked}83<m>WT`)oz(?4>D%`y(G*
zxfX8zZ<>Re*n_w_-dl%D9_@?t$uqaVKOypV@Zpy}#$T^(7n7^~{37z(3$3Gj&oePF
zZ2$UWx14Lg{ry?DPX3RH_>itExKZ}wi$)KN&&PdCJ{1;Tl#cbEz4MY+L3BuAj<?Oi
zm*M->9@)KndVSHaq^HxpicFuL@9q%d(SLWYJ^J;|u65O}m;K{K-$vG)jAUSVuqj$y
zUH$Fjr%#`r2ukrd+q3Ia(adgpk*80KY~<w2#Ld;`pV!yb<=xHAAR$^?^NW#zf#I)G
z4kH7@j*bni3=9vH4v8@^G;~|#Opp)LX2|1_e!}?R*c|?71_lNRg=vC}3=A<YH<%b0
u3Ir3m85j<@w&*f2Fo+9oV?dYq&-mx@-xBA=;{FT_3=E#GelF{r5}E+TDSF}n

literal 21209
zcmeAS@N?(olHy`uVBq!ia0y~yVAfz@VASGZVqjn>JovbUfq{X!*vT`5gM;JtL;nX1
z3=EtF9+AZi417mGm~pB$pELu50)wZEV@SoEH+RcxgrCZ@f5@M-EOVFUW(Ubsamh_A
zDIqDE!Hj`j!cG5J{wOZs5e*Rd(b%v^qa*rTz|9jA7BMMxaGYq{w&oJkQtQmiU+U_Y
zs7&Aeq-c7K+u`SbA05@+`TJh+{pUNMPg=fxQG!Gp0|NuYfzMO+`GFV@>KYrx85kHE
zrYAgLWe~8C2tLQY{@Z%NrB~fT<t@G~wh`7-WBj1cH9!9G(g2M&e%~vT6c+#4a@c!%
z?e5RhnV0J?yL;|ja>%R~UK_tko4&oFy7B*l<-5&RzkAJcy8Y9R%?X#QZ*CLhtle*w
zT>1OJX=^{dw{H*E{AoO2E@Q~~!^ZQ$hdb%h=Qd7Xd^Ues=bMZZmIr1=B<+w8y|>~*
zNLHP+pt;@mQ%wIh+1m$gF8@?Iac1S_?Wyth|Bo+pcJKRJ{Oin2@0H>COO~fU7n9;~
zJ(Z9f(t2v^YtxL2%MK_1ZMV6(b|$wwN9*m$qRT?E53LGWe|1af?t6dR_n53HU*dJ8
z>EHVU>g#RH@+$A`eRuGANpyGq;Rh2obcJS{_+)(hplmx|Zr&FM)3sY-{zmWool#bQ
zxjMe`e&XY;uSA?XpXN?5yBAS$vi)ZTN40Te)x^7<PuQ*b*y5h{oj9-O`S(IvBHzOt
zlZmoFyJK!zPLN$3u!8TI*vG?VYS#*;G|V_+<G$mRSZFlwjUv0_&aK5Q$F}{h2=8Kl
z^(t4g{ob>h1y|mf{w)eysQCNUp@+OKdD+)*1xSkgys|`}%QtSt((sSjucCUEpWO6v
z@A<9gp4nUH%$=Z6mgJ~dS~E9Lvhw$myG4I$mJ3X7I6s-i?Ns`7?!OZfCEBIG?p&2P
z=j{EeZ-wp$Pe+A5WU=4$sHvdfeed+#PaiV#H?P@J^m_UAch=Kl17g;k-(T?O`uF&^
zXEXmQ<o@~A<79sQ(8|Sj@87L--krYZPI&Haz1AS(#JPvlboA5AR~=aS_0yM{&ubRl
zv0svx?Vg))<$1jQ|L>>xmz(rnDqwoVeuj6$!s#>S9^Gy|W#*pQ_kN#x$+!FE&tq@a
z%-XZ#=yl1d6Sw={(mj5@oC};X5|-4I?YzJ*+1Pk}qa=S(m`q&mlDi(kfmJ=Ts=3xV
zHAnI_<%e(tX-zqJ{Bt+h_1dcwdKYf*x%2+T{QFO~Ie%Suf5&FAMyt46X4)>9p99wg
zh2JZ_{@~WDKQ6qzUBRz)l2@KyYMJZod~IUio{iTxM_;<Lx}{!l^X4CA?M9Q!FIUG~
z-c9uGE&u=B>wcD?l&{NGJN@(L^*&BFn+|no*QZU-n|_?v6aS^CZ16$r#E)tBnak2{
z{`B#*H<%;8G9b%OT;k_J^E!W}MK7u@vu^rcmv6kjFyd3`KON^XBlV36xwYljlwywG
zU2pdAh)K;m@#|sF)t}tml;q`o_X~@<npIt!wf0x@B&mbjt*88d@}Tc`ar;-9^R*%z
z{$B!^^kA_YR<Kasi0AQ#q>mT0&VOBhVz0r^y{6NDPW-L*KS}-crA6l7?>_MVpL$8(
z<;tVED(<hpF4WB3sqWLMVX;Uz-D{=c<zmZ{Ip5gQPhHKGugoiDTv@e!yG8J)_4Q9D
z`zSm}Y-eRS$--9Ke%$r|XWyEyZ0gIlsO)ZYTN<FT?Axl7oa?Uq5zgE2(JyC%*TR6m
z(+=<baxXAxe~tC>`srbzi=3L9Os1~7`qI+n`{9Wt%TE`{oYuBpJ2RxU`r#~xuV;B8
ztu4A+LOqLiO^HpC+P_6*y71x<SB~(@Hs9}@KRy5D$AGIV0-o-D?PsAX{yZ*j?~}g|
znX6QeT<^J%6~Z;uO*+unZsGBUhnwvpYb}@05PWjzk>B?28Q;p6^7^vQk!TH44oHi8
zHL?Hx><ix~wr3p=yR@P?#PQ(8&_}mazSSmwOJAOEZIc^P@p-<gvHF+lEzUJ(wH8Wk
z4U!a*k`oQrUwC<OZOQ++n@W!QFAsX(k;(g!QAzq>YufZE@#Qfm8Ygb;pZVPCuI7?!
zP4bV!t=IfmW>&oR`RvrWzyCIGKmO&-l~rj|Up!C<oe(7~C>p%|A@khb->WO{T=C!k
z|6@qhw97}1sJ!gBo7&1<vL(pyzLCs2)44OEy7MK??Jpe_xDl~@Tdm!nkA9}w?yQ<q
zZ++<Uy`|DO^WVvzG4H%u&C3~Ta&OLkSMr&&^!uLdZp+uf8X@gD`Qdv?|AZ=Wt^b#G
zP4ZoQ-KhmDR=cXcd2nXGn_!^J9Sg&)sb1axzQ<_)D`^cfe)s$Gq^MJK8?QgRzGLzE
zfAMpQcTI^cdvzi>YSP(!w})9qJe$j(P5u)-F|t)`{miwimvL^|y<?_VaPE`etGnOM
zJ6cv+*jQohdFpzb>&|vd!&xiz%DlBr??swyTOaoFgC>Jk>C<rgJ165meAsmT$8}S#
z=g&;sYJ_)gQ*!^Pcjc(&O3M@Xj!P`JZuQ>!;P{WLeA*k_@@}pBR@0W~bM$4gTUmH_
z#f!GfM_ML}>@RIm=USrpFWPO|GU4FtK;6gB+;?U4aoxAw+kf}v!H2wJZ+9szV^Is(
zx9yEzxkwJLK+d;I>-M~!vU}~8ow@0sA8+kk@%E4K(q)H!Mdhi^|M`{8`bWE5q05!J
zkNe9$J@{E#mF|8ujLr4^w!KYTUFt2(W>lNTT;90<V|YpG?*yf;HD6~X9F=r-{Pt3L
zcY4o@V|oD#14^VfpLrVnq-Fd3$hu!fem)sb6%Vzh{QJ4?(!KTtmixA-ynk!=@y*NJ
z_!+fN4)Hc`eDUn*{%5b{($06)|5<Bu+q>{?Oiaq!r@4ox$g>qBz2d!lkl$EzX@5@e
zO`*jBE8_lrXrFEQt7*5nna-7!5x%p2JWKo5wEf?#lk=h<U%a@xZ_eqf;<LNHhM$*>
z{S+3o;nKs8qRW4FuUrsgn0M`{=0wYiMg5%bMU0-k&$nJPV@vG2pFD@BNUY<@7dxzH
z^Q@6kyIgMH+}MOG&*xk2`D=gowMEqW%STi;M)wsw{KKMBdwR#s5~b(^nLWR4U9{@F
zv|1nS+?l;DRrJN?%jP;2op<L?b(}bV-UB&>=hFoY;-kxw=jgpy^7{X;Amwwfa`VDX
zUP`yG>dZL2)~PMA?v3Pe&c3%l_HNbn`T6mdg3_%rcl|kgBRv9cTv=b9Dk}2)j*a!o
zY@PJH%h&%sn6lyZ&$c-;7EJi@CFz~P%eB8Qx?IUm?s8cB^JGg{_NOP^!u1v<t_hmU
zkK~+|-F0lvjAP36qIxdj#!5Epe&2dh|GB#>|IhC2`Mm{Y4`;_^p5yDwGdQ@-)oZ!Q
zww?LgernIYu^AlhM~kCo{rk4CT`BipR6x6#-2v;ZXARCwZ_fR8=2q?X4bSWDpT0Fy
zl<Vk{zt@8K<yAsb^nd8TSDUo>v$gfAm6!h<HJOelpmpBH&)&O6ZPQ=Zy=OCfgMts9
z*fp{2y7n?#+phTySMnvxXPwJqN}BY9WygKzC6AVee7>lElQG^l>2u4u3tF|7{{By<
z7sS`*ezerod;ZDi+$&M9-lvy;zT0`yMI@?n#n0Sl@m78tv@EU_2|t@#AFsY>Lze!n
z^UdmsKATeW-i5v^{-B)I^K{CB{hKvA%$weQeOp=P^YE>_2v@6D@L#uy7YeoOjJQ$@
z4x8Owt`k+-Z9Yl({L5{7c6^QHeg5vtgRI}1yIZ&eS&zR<?oG{?mCn}O^Wd4(ImyPj
z=$-swJ2oAD_S{8;>+7r8tj{9z^z=4en`EK2cFBql$66n2i~D+Z@T8sZ&ARaS_~x5`
ziaxEYIc9mv_SKc#vIA@D;}XvEuKly*>Fd_d4X5_*vG4Bw{J$(Dc==kzWjmjA6>iq^
z>pXeTxz;CP`2@rI`rC;|m%Q~mf8O`+jNqczk!5o4X8ikIu>0)OEw;A3^Bb0cgE5dP
zX;RAhsY}~Ej{3hmTA#O(Iq%<35%mX^w<pK`5qh_Jy{=vQ(Wz3=t?b1{FE(3VwJAP-
z`D^EjqfZt;+phL_Zq}a9wTt^wXFY!>5iz|ZYVY^$e{CwB#hl!FMptv!v6<2$LDS<;
zwCC>Fu9~IIm%u-zPX6+gj#qp||6C3(YMRr1ygu6I=g$`kvroq#$}YQCqIv!0Bc<0F
z^YTudxBGisZ}<7+IXfOsy6hy?d*d{phT)PZuK&3#-_L(M|K67MoRa-tZa<&Lf~m_h
z?#9IIxK^}PalX^S6*AXXe4ijVf6dM4j7{}3YVU9OHD{?sfBdEUH;-{vJpU8>c}>7n
z-{~Da@ArMUeOCNP?H0>iUc<Ah;XSiU3%z{!<X$B+S-1ZF`TH%O_MB}qt!?YyU#OZB
zX?*F;pGoZ-AF$N#^%MTgRL3-FU+SGqD|gNg&q=o7)8v#y?U%-G6V*QxbC`3*y~^eS
z&hJ;Ri_QQ1sEoJsc}l>_n@Men63dpvx)=!Rre1w@``cBEgIlZq9x>nvj=G}b<Ljbr
z^rn8<=hv0%Ce&U#d}QY80G5y3JBug%mSI$?`n!J9#Q2q(`zs?11a<c*B|e!_nG!kW
z?G10?uL93s?DF_?hXvI5O(|bB!|C3Rg6Z;U%er}=vwS|UD#`ut>5-P>eUnlP-8pw(
zC}CQ9GjwCw=fKPR1u9COaPN^%dmwY#M6|FzWXnly_OqL-LO33-4_p{<Om$0r-J9su
z<$or=PuQZq%=8E>zZzOrtmx-_Bl7Nv{sH;22>0xi^QFt5+n<mAX7FCm%=4{gU1a13
z;R#=KANyUl^m6c-^k(O#F9IunXclVaU5S6dlA&#@7;~uh>(-;s_gGYK*LGVb<yCa~
zpSz2q=&sGp>(%+6vaH_9%kAs)?P#XUlC>rm66I`M&%HC<5bY<Fe}Bc5oNbk1zuxN$
z21aasJ~wRU<L@8uNJ~fi+pBFA*d6*{+f=nRRd>~F+4t^vvHNWw8}FZ`ea|fayjgv6
z_j2X-aGn3#)+qSS(doAKiYPj4seN`ry>{i>Jr;4>uFB7x@Opvd>d$gMXJoymOIa`m
zmfkZy|FgGzv9`O%QMdJH{ybZ^S6$W`OJcG9S^VQR-|LLtH#^^bsrk35d`St<!y|hd
zpn1&C=Vww<%1gzdkHL>Z=KK#34J`<L2+3N{k4~M%C7pG3j!N5~qPGX?X9)y84&1-F
z*_$U^sd>ltW&T#Px4ys0=5i(H(0snn1!4XZc?&C<zxSE7I_=b2+>kiq=UFYmi;K5~
z*LF^v|Ic#ynGZLnFBMbT#}&j~XtFIq!tLzt=Qqzy+!ds}{pggeNU`Y~uO)fy-c-s{
z|L*YnBK>~d)w4QgKeRNND0}AgtgdyunKExp?3Uf!P;zf+i(mBN%!VFtWeAJ&PtV>v
zDb9nIE6??{GadBi%n-NmJy7hcZp8T9^29~wB|;O+ILmvvu7AI9;P<UZ!l8GT9nUJ9
zwBpvg)p4Ru9T{a>-(~(kN}FnN@aw!=Hx+}NUA)&lw>)z=($>|?W#vb|%LeZZ4C_v$
zIe)X;>a;NAc+8}_X%|A~9Mqg(JV)GfTCV2G2?u^(cHFV0d{+3AGoh=JfB3&nm1z6_
zL2&sL$BWaB`W}^>?_0aDjOF_$_dfPxf6qng+aLR8mhmqB%#(+W)2+dIyza*FC%R!l
zig6jd<yHIkD#r=6J)Sh{knkL}2RoMu&uq9nqrvi#>V{oVAFSOU|4?ONKvsu_#Uj)H
z`tz>%_7^uzbqsV75&GM4Al}{YwdOv>KA+r^ogpi=*Uk9BAb9j^)bot1Ow)5enon|)
ze6&Mr-Sxn4PHsCZw*3|b$AXgg>783z{^!it<-hLHbmKYSHDbl*l?6vls!jMkOH$aa
zw06V3yZhUmld6iv9^S7wy|3d`L`9fS@k!CgX|Z#JCO6A}Gpy{M8qy&ib$IT)|4F9r
zHqCjS$^H34+9X59^QLo8u*^Aj;u5HCJhJ!L>JKvN2VR=SF|Fp_vtHLO@aW8X@s9ak
zdzY7eZti7OH~lv6)$NKU7kWj(9_jkr*RuMJeP{Kuz1+XfY+e?(<?{u`&4;32TRhEB
zk{4UieY$kY-U;_B`6V}%*B>wP^O-!I|HP&pJzK@%Z*7vhGk;x>#+CcAPvx@i+ICc*
z?zo#?YseE^@;>}htGk?Qc~JeIM}NOvb-J0V75Z?F!MVrM9WPj3J1c%am1B5TRn1NH
zgGWZX%eAALhLyh(<tJ~C@NBJEXnN=6&)<`z3Z~7SmGnG$v&Db;b4_XQzIaAj+!dRb
zZ8ee8qIV*=2Fo=6zV6u7ISk9oO}W<Seb~3{#}TpZtGr9=wDRYi+$8-c&(=D;ch7li
z&CJQ|o2$ICI<D?1UhJ}D?U$Cj_WoyzU-R8c$X7dTa3<dPc0t#wtH0SBx9*N{zsaq6
zCg!~5!?%Ar)lNO&o!PocM=yEp(do<f@11M^X5FPUF?F5am)Pgbc)0&=!W+x4fj5);
zX8T&4IhQE@equP!VUe^yC-jUpmhh=3l$5@UPkz7gTle4O*<G1>hK7GGD?L-sp22^g
zEi-FZy!i4XPhPgy`rJ!W6@Aottzh}{=dpk1d{$U3Ho5<U_?~U)9hG^D#lLS}-u-6s
zyvHTc73*HQs68-ogVaCM{chMDf4$+!^9oLw=cm^_i1d?ly!ES3Zc@p=+3V&!c+g>X
zXnLa6+T}~yPVD|AY5(tG|Jy$y6PKp61{qi1H~n{K&1CIWx9Z|FLItz)3*0Xxo!F$i
zRBTge&)LrFFW7{0^-mf2=B0e*xzBz)Z+c<j&Me)PCjSl}>CCtlzuh8H{@bRX3tM0O
zvii4Jm}}kp9)3=xMGC&Yr*kcy{ir%T?Q`{(r}?#;yZCjUu*gWwJ>a>fYWwzc>CZ&P
z@7?`;*ZN_WHGg@*TEThigidu@&Wk@|;Ny7g`w^>k@BBcCUj1=BC}@_7fr4h|b7P**
zcQ2cr-xSnt`gqQ9L(z1eRbp-~UZF3<Zp&*5-c+|eo_V@r%gZBE^wp021y|6sZ1*Ly
z7tD`|-`Rgz{W|x0!vo+HlCI_V{LiGkIX@X=zll8kb86?6WA8jYXWPuV8l2_qvns#%
zitkD;`-%Dg|Am&F**sZX-fC)Cf`+EniM=I%zW3jk3JlCOeifv#b^Uq^?LAr3U%%*d
z^78$8`S<NP3K`!Yy;(dxPi(44`ZAf>%U_?EcQxU_Zq{w{mGkuU!q=)!P1E_YUF>~N
zoXZ{VIScDM|9!g5X|_B5tKa#x_rAKPl{tEPetf$+{aWp(vgQI)K~0fYg|GEL7iawW
zaXPzPcHhLQ`C7VHpWppg{l8zoWKGu0)d6hv1(SZyPHkH=_s{J*T`S+)`pcS<lD?@F
z%73#cd1{z^@vi^mSAv0?JL@6I?c|SmP&Qi$%4RX3PR@)j<Nt?WNw|pIU2*=qHDCJE
zSG~XX)PKvDxVG!favu5G>D5)<Df7R`EZ2Q}ahY)Nz8MnVt2;veObOvS+Wq<Z-4oYd
z7w6^0SWNmH-Ru3Y@LzQAp=_QF>viookLqr()%&xenqO^ec1|xx*@q{^-~7FdzGa<Q
zx%M){?z}%%lVrti|IEHFl(710*@IVy&0S5Wefe}(|M<g6OOKTnyB+;>Oex1v@oN0M
z-S_?ldWMUa?>{x^)&$x5oO6f!4&6HQ_qb4+me>5nuQR_-a^dzZIW$N9oQJQQY*hL$
zso(Aq{yOrR-(P)YpPVM`B`c<vcJ<BH7w_LZjQ0-<TfAc1G<&BzYr0S0?%v%X|HbfQ
zYM0K<uR?cjCmvmMV(Yy4X|bN~((`!)fBbe_7-DaE^<1ux((fhe93hic>P}ZYa(1rq
zku<lzbT@DB-OF;DcL$Y5>}9oH&!Mj!qA&USg}=OJjgZ&QUDXp(@2+|f@zDMG+?X5Z
zb{RTJzm&aS@@C5<y=_jJf!i})cg{BVyH_SMqxS8cb@Jh7=GwjdxsX{d@Ajs=vsr?P
z3mvsuomO6Qb2)z1|HZExlOHeF|M8RK`+4z+bMibU&c1wBsH-?QOuy28W&L-x((IP(
z=BZq%8_X8D-Br8G&Qo81a#lz>|D2M<!tbkf_G$QKsy$xIx6OWP?m@YVnNOGf`T6lo
z=U=(E0o&a~a|<RoExgd;cI;~Yt=A`?Kd=9o%=Z3gX!#|-+^C&z-hTZ5^8Vt_%)GBd
zI(ULti*SVoM1=U<J*F!s{pZh{^Veb?-gQ4*_H=uw{<rr*n}b@s7V`A2xwENw|IPbv
zMAxmHQTAYss{YgK+v6&Cg+8_lTqxD*w2+UpKl{d~nHP=w(xUtscE*eER>{@jzW)sp
z6K92D?j;^w?~!#r{c`%B-&fh+^VF@$ZjRcxP--j4p|02Sul?J(@p8HKzYU_7)ol;H
zY@4ua=@PTKGd?YS_TZWOF6*_&4bIrlp2qX`>O!}r9STc>gu@mFuGU+;ytb&Xe0yWT
z(l^(<k6HaX>CQFZ>CCKCD=&NRGLii(E!gT}KWq9{b&pS%-!m|rl5E{Oo4s}tCkxvb
zjhmJ>F)|ENy?@Tt$e(2v7Eids%D}*2Cw_uiKgo;ROR_a+^N+1+`}|lL4t)0dI)~G%
zw8vkFk-?oQ{lU@@t>&htbFbFgOD#QrYg%+r)Y7v}eCO);SQ!?~F{=L(t8FG2SorV$
zoSliGJN=oM818e;X%s(fpf)-4Ma$Fh&0l*?&Zzsi-ctFQrpPKy?e^bRrVI@JhV@_m
zmOq{E7JO0PTdnXJ-@hlN^HW$E`dH2#{rZQSp>xIM7Tx`|7q0(4$-q$2ez)IFDM;fA
z^YV4S60arbKWF}TGSI%TB~fB|H_MqH2T!-mD+=6~^W#zTTl@F66;Iw@c|CKf<HL`>
zw|Q$*KlKRq|FY6&VBr7t>2T!!f8Soq*U#Nkq<lHRDRH7<;m6)v<?sHT=?JejS^ehq
z8-@n$g1!ny28M=MJ(-W60@NCy^CcjMfo4$Z_?Y!UwEn>Z+@P5iZ-Wn@*`E(WJbOUG
zdsqgq^pS%HycbURcK%|}cYb%@M02+VQ;!_kF+p^{jHLNAhvOW*OQLvJo)7+V(@M*1
z=RPj|6IPCo=PzFNQDmL!(o2=<`{gaNgjepl%zs+7tuD%~xhimO#HAIUqAm{uLw4Jh
z*0ju%R{gx{-S=f|AH@6mD-3(i+8b{EG4a5&6{<`93e$TxiM-yT(YEkV%&+hMvpyQ7
zF2DHg>z7vnUAd08gPue#eq&S~@OIml7u8mCo#v`toXd1-pVwjOA6B~aCvEiIbD96|
z<!3iTlxM9nU+BB?PUO-msTmIbdz|dwERt4>`Xqe!)Ur7~xAydO`Ct5gI`y2&gV|CG
z<^&j&mAke!?e5<6-{#TzB!9sUo`h*pvsa&~%r?LDF6N`5-jieczQ;r@wX~kgXI+_S
z#MRjm5@l7_E7wt&?K<zmPOHE3;=Wng&R^9kDEL%%*@<u0B$h{C<KMZtmi5+=t-Gq1
z%m13q!TVHPSg>{bf<2GTHjAlTI`TJl{q(uZ0)5wPe)n$4jN>+!L>TW}VR*{I7H4$u
zfcJtG`;P_A?mrc0KF>4#URk#5JOL@6s^pv5$(pP;=W!eFzRwoNl&e&2#Q0~Spqvk@
zo6@2UX;bPCrG-s3*cBS_&1!jvQuE%4{tV`(4wereggm~xTj<mT5uWc0pRJjAZRyc{
zrw<!CcYfXaTe;^zgW1HRr(TLkdtQ~g*md?!WF*_`*BtA6b}<~_x3GAWsvhv=zUTMn
z@gWwER0F0MPHtK~Z7<(CCs)b5wI_s+m|Xl@cEtOe?9YETk5mt+Z{24<Tk634iXVkS
z$IUNZ-n+t0HE6YlPM4L9oBh0P!prtM6{`mw7ZVY7)Dm?KUB<UJ<Diz7=2qdD8E(bu
z0n4X_7|v>HTA393>dNeAHNLH?cRc>Z+WZok^~1(=h371VcJoJjf9&4c(!Kca7c~V>
z-DgrC-@duBaptw_U*q+w71LhtnA3B`@6ddu(&GHz@>e^S%{rTL+%)jxpI6;?B3;6K
z7sUCkR@<}YuJz-T{mJM4%1(}Vnz}rfNvo~MTVQ8&=bK$jxk~$5EmhwBsLxs8cz0!%
zD;L+I7ptzk^}JPe&9RudLEKPDF!FzA|C(!)ElZmXQ;hR%BFtPDrqu1s6R!Vbt)|wZ
zm~?2CF}uEjo9*Y{T53LL1q{E+CBKu(Y3i>%9Kw^>F{8um%tG#-iw9)xop8yLP*Pha
z`uTdU`p+w!DQfj6@0?68$~Ra%%gCi?<%G^l5zJ!qp6KPBNjkLkjO^YUZAD%_-dx8$
zvJ4+yk~v$ndG5`3GO1dbr<bihG{d-DR`2M2t97c%$)6szvQO8QyBKvSD5zX)WoYs8
zIK2|-hgUtd0;b7sj+(KxCA0n}=L+$&GUqg^-=52Ry5hCh+N~c-JSFQ^B~RgM>*%cM
zu&n7cd^MAK^^6Y!lDn)Jb{s#<y#7gby!6fe8|;>-MK^!$Gg$a))64sFxBLCylzsEa
zvBfhkRSOsM8{euvn5`GteEqxD>=kRzKM~`6dO34qY1O}vn|9S)I4C7>b*AA>y?uoW
zm!CPShfZsm+drdTW>Qqoez(RHojdvIZHZrgp4ne-RD67Tt)YOSsC+`%5-#1;^4A`|
zZquH`Cag@0DCYF`ycHR<VwUySNrguqL^Zy9KVx-Ow0B3w=@~iYJ<{>U7h_MCiJ6yc
z?~c8`HOhLHp621z_owyl>X^YheeJ>QYR;$33~>)1Hin<uyPh$4VQEr9X!eKGzH2TU
zbFaOeUza<#?nBy5m)PXr2WMulxm^0Y_0!MqeREs5&l_e<HBFoU*03!r@r-A+_f8)l
zZ>}RAS%%A(-kkfi&N}*EYm1@jE8~9NM7!A2B2z6^uDrWe*;MlT<npuq#xt`f`s4_w
z3FjARI$S#U$m!~xmD6LC*`{-s)F0Q`bugo8jjGD+X$D*5KJOP!U4Qq^+Bapf*R$*d
zw^+i~0=&)GwS-50eX9MBb7HVa(f>AoMw$19IW0;_T@m${q=MF5mX8ZJ+o+^{<G?R5
z^O%i(>rDbQ<})q+J7@mN{N9!37p?wYx$Sc`(eIV^)EU!6IwoF8^7Gzoefn>i*!h>&
zCeG?HpIknF$=su@t9AzK?{wpNC-UN7-_IQ8Y);<$8~x0e7~RTH+rQ(@+S$9OF6I}z
zo|Rj^YYC6`20zVBySofer^m`Ny!-elwzq6K`^pm~?>AitYSU5l5!7@(6?gp0LhESO
z=5EiGn$>H&7EFq1|G8m$((bK|tL#$GzVgyL>M9_(b+y;ze+wK-Wkas2=H0uhvGVAg
zX==HPJMz*$mU~;?wF;X2G40d4$?55ZF{b=?uWD%KmUETVA3qc0e6=m|y~o~}{-I8t
z9s6GTX~!?Rd-&9$J9pN~)NbGi@lBZa+)k_YGb6+L56k6GhHZNHbYsmFfxvf;H^Uyj
zIK1&wLRR3(Uu9R!loqX7Te8cDcZKrpTdB`m#XhUm@5&YV)AZXqZR+xsi6u9)+ZJ*@
zi&mDb`YfRPI=Nm@yi8la{4T@okBsk(_sLbbX0KWAyYz@b*+0q6r<k-hG~L|4Bj!w%
zUP$XZy|hnfyRTi}T{<OyNvCkeoAA2tFFZhHSpT-o%O`(a{p9J>=b_rVA3Qd`dp~17
z|Au{W|Aj<nzj(8IiImUBz-uq#ZmhkdqUrq2`NPfFr7Zlr**@6D^Y8g}EHeJNNa6E)
ze`kttt@`D2^R{E@n$1Psk?SMtpYzJSPg2u;7Vz}Krt8aUs>+4e?(__f-W4(Hxkr}a
z^@=TXZRhr^pS0cX`0G`FT4(PJFy*(c(Thl}&8=(-`DZT|IsLbF+H%!v&ku>mF5jwY
z@~Ze(!7kq(@iJ|5&r=^BuDTZ4w~LG6N7s$+gGb^gX};{b_~x(AiM_Y`>}(Edc2@2*
zbY5fq{PVvp_x$!xE4BW6tlGS{-7M)-*Ur|C^EF=|n;qO6X4zTZJEMjrNoDJd%a`7q
z`&44>9p#l}bkAqr*-tX-Kd`InsAi@YF3g(7E+Am&CVbeSM{%lRl9TlAdD4dswkogP
zyy=~-=j-b#>Sr~!%17<kpS<t$g3^y%cV}L><+JhaWz8pd*SfS-zFYk1*7s}2JvZz=
z_3K{JWj2QXk6#aTC(gJ(-9YdlkKp3IM7!UeJLjIB(KXZi_>96@38l0vMzbI6-=|mI
zl8_SptiQWwV~6FZ<eSZ6+S`))c7D$}^C;RZJ|uIe-=kP%HTj1Up1Nu=vld6n<)*Ln
z_VhiLeR6Xodz`MSj%sQ8#Hg)}rE8wP*?B;Md&d9L^o|*cvt!TqCeDa`EO~VA`>!jd
zXDBHbm&ph3owS@S?%n$tJK5JV3o1QpwJl3ZxdU?km&HXdPk)zNaBCW<SQay6ziuR0
z(V*4vzVpWS8`i6S@Q3*=Dd4OWpBedhCZFyMu7^EA2Q!>z{$P3bGJM8-|C^ECj$FpS
zOP4ttFLPp9%#)-Ql4kWKC9OX5d0*bgnbAHOVPe7Wd7tYlPn}WY@=Ryb(It6;-@0sW
zoeP>SG{2{O((~V$V#3lVkEj{UzU*>z_nyrjSzU`>pUL+0d3>wKY=&ZzNutl;X=i@0
zrn>KsIdL}WZq2e-VK?bB8qG6SZJp`3-k?6!D(1-Cx{PQ4`hFJVL~?Sqo?X25#-00X
zUD|f;`KnqQA{TYu=3?(knX?*GeNt4H72Bs>mIN1Z?q43Oyc6EZuDMKjro^rK=3PgA
zSxGY}D7~4%AYfte;nB;m$^X{*N1m+M#n>Q!u#c00@!<7x(_hT3O<nKq7M>Leu2S6l
zUDNIkV-1hB8Uu?G&z_EsjC*26(=N>osd}oo>-MyNmycZMWMnAwVc>9(s1W@6#>KmI
z3Gbp?xi7rDt+t+gFE@*;K>ko4CqpC0bx@O^p@I|K^k=BxWQzke=Hr^6jepQ$DF%iI
zsuECT10n7B$MfXLlX3pc3=BJ_>BsLYdg>LQ&d5--$@qiPq9aFK-Y;WhV2C+AUH^M2
z7lVTFoGcaw28ItpzuotonKWtAo@wrt%P+q?)6RJ@V_%c+1G_B?=Wod2VBoNEV%AqW
z^psU;qkfO`;-4&LjlVCn)iH_RVq!6XnE~zE968RsUhZoZ+W{?xchUFm?BAfz?7%R=
z;KQlC8}c6&|9yQt>=H|+R_OZc<v;4n=bubt*AU@qby5sqvR^PobLy0J2D`JTmy7CY
z=<XC=9~z!v&}-j)U*QmMM&uDa%gJIZuWU$YIa{7sc&_uKv;112wO8H3D@$Jdn7s4o
zA=a4N|F2GtjdE$vbXvT+r1sNQXUVGFiOUvU;k%gl#_F5Q#sdm@ho3E%onuv0;IuYt
z;lWoQR%q#3mB|18_NP`ouOsRP>m0Mh9%(V3H&^z=?Fd_Yt?hdDz0604dR2Q4FU_BG
z<NJQ|xUA^`);2C{IeT+1Ec(3T|Jn=Ft>O+$bMP<N%Im$o{#RJiYPX4rvl4P${)+MU
z&oC&yzH#-nn{v1J&#8-fGUu+r0%xa+j$2dzoqxT{rR2@)|7|Od)T!*+!@TSAOhyHU
zj=xiO?kX<({LVP3`hWWOkK8|9e~SORXZ-79lySA%nID=*g$^6|?UVb#Sgrql;*@pV
zdp2+-n%7mDu76lvns@H@q|^szif$#<Jad(ht1OzD@%%^MOaF-Z#z$rpO^zzt_xZt!
z$C;6lnaAC2E0!0Zepsp2zVoi-z7;PU`m23nrWI-H|NeE;^1PYk?|}WQUDfKI%$i>H
z#CGp2+ozu!U-I|=znR%~z5IOri<7OK{(FD^-oNr^Ypdq+y6SS5NB8*ezq+=lZAzEd
zfy~LWi*NVdn_>F(bMDKVRkh#FzCFGC-d&4bcW2D)6I*|A(d|3BH}m!GR=v$@v{Ns>
z{(bY5lfltE(aJ?{nQRYkHM99~PI>*?&@-`nznAsdy+3#Lthc)KcineacTH10Q2cxP
z<^JxAo%&lU^B>=BI^@l6H$BQC-B|GAyPux1%VhM0Y>%nl%hM>*oNjH*z{2q_{Kvl9
z-)HpOc%{?o5_jxg@3)js{d1S)#G^aa<+@hx``kD0@5RIV6F%Qmk$J$^FQ(UXKSS)Y
zbl3&iU6miUE<1bd|H1ePlQ+-My3zZw?k;cn_bVCS?5a;Ky;_^~_2)d>r@!sC{#v*9
z$%+<9UacOx3Fqb&{hdCM|L=Pi^*7HBzPvTV{c^YO9IJC#VV|exG(Xj?7ZyoXzrOn3
z^Qb`1<p->n+kFTq{&;&yn8yXd+p^0o-g^Xi<hrX0T<qV@bu+l9H9h2&*Q4SM(WcXH
zZ%D29;JVkB`PJram1{S1uJ>3QFe655+WwgmZJn#^ADoD7{;_K3H4eRe4h9a1MQm~V
zZLV+lT`vAcum0a{_t*TllXd%67(AY^&j0s}4G$h{cu}@@{{1?|<7u^P`lbJ!(0_jD
z+w<z}s|Cc?@O5V0eEagPc#(zS|D0bt^4rxC4?0eqn)O}QQu%DaA<eUk!rtF43!hk9
zcDi`)?V~N(CJznYR@rZVnq#({<?q_Vi+`1Oa9+<iq-|^S;p*g{*YbUnAGS&^p0^@i
z*=;RX*Se_n=Zl56%lMUE$w>QU9qoK5T4aV7cYgjAmn|1R@6-6fduS!o{23Q@1)s*>
zw$E~yuJzq7Yeu?dZeruNhZZ0AZ`-?V*~aBMSt7>&V#KPwuHF1-*lS-B;xsiO)NP}0
z_Y{%X-j3?SX<ZM!mS?=3vv~UtQUBYwR==%zt<k%mb5eZ9jql4v+_Sd}tlM;1Ecx+v
zPv*71G|C^8hOEtfV4}_K{LRky%He0%pM^e;x$)0uJNx3TS<83Nm}#9G;kedpiq)Ck
z%OcOVSFXJMd;4l}A(?wC9xqrM{;5bm_to`f^TK3<*8BdqHRrZG_~>;~d2AYgk9E$D
z-Pb>r-Im?EQseHYviGsf$=#qR+Zm9t<#rWQskmh3!*gv64GoG}53a6XRL1>!gV^kU
z=frZ4?z{G=W8RwURUi4;H*t0GRBoSi{Y-a%-j?Uv4m&5k+5YSHZfUpcv-hX{e{16$
z=y*+j_VjIQ@Ab*s7p4}KE!=3J{dV)kwXeR!zg}UoTbSFp{D}L}+2MiH;zIVy&NPc>
zI~--V@7wj@)}yMGGpCE$+}_}}Jzu9deaosjTM8auwf?E9dNkbszu7KtQ}2g;b{hQt
z8Pg1Ym4AM%`E^me?Igts^A>CE*uWw9HSh12bNhq4y}b1P?YbcIcuVWtZTz<vv58Jw
z`h4^9Eu9>8)AFrPoUj*@xp*$nRcrN5X8p+@%O-5It3Gw>xwL6rX7k-y&z9@2z3@T#
zbo4(piGaY}-QSm<R*XqCtew<*UyXfP>H2G#SI*g=e=0t8Mi=)v`Ja^`&$I3>mlZhI
zl_=3>_%wZ~{H>iu1)sD2|Gf7ronLV4>U+;F`?kBhOX{i4{gJs{s(<fa*C@U38QT|M
z6}<Q%FS&17n&j8W?B(0~*VtxdT)*fZyt(I>^=kF4t1nd<sz(IHw%iv>sgV~nZ!=xE
z#NYL8xOt9QyJWqwrB*P5;MuERJA1FJ+B(tK`b*@m;;zfCcWw$W2pG8V?l}~C>W$Fv
z`ft;u-fM+Ey!NOg?nZ5|Y(Zh^{iy!+>FhVw%==pQH+k!?+w-RFsx0U^@I1luqUpJb
z%*&bAo7z6ISiNJ%uKbvO(>D*y`|oetV|wTAQ91UO)l<SFj^F4i;<J#fm@0M4HRIZS
z>*6WfzILw4wHNg`A1L~xyWmFe%=wcJ&wK$6`{?T#XZN$ZeVf8Db<=^A%l=-ztfv-u
zxQkZqj{7ph+5Bd(QGZXkhVz>I|8thEy>PT>-Gt!a<b(SaFZM^=yY+UvCEu^Ltp!t;
ze)FuGZNRhn>0HOC)SFYUa4mh-x!sI&`4Q0U6<6_|Aklx9lx7D?2^O9^&-FejZ`;C^
zFOJ;_XAj}&eD~wWhMV4D^LETS?m6{-qrJ!3o#8(?zukWHXMeNPs~y4O%dJnJzIu57
z9`j4PzJ70+(NZp1{U%S%J=JQ_r7IQhU(Yq)#NGSr&SLBRIl{94{>k65Uwz}w9Z(pj
zNLIK;bSrzA-iQ$lnp3Z1v543DK-$+e+t(^L_1~7$Hxy0hsOQrX;c{PkbM6hTIlH?a
z{YgIfaP5tQ+k4g|8!UC@YQ6L+&#T+ZR5(6j?`!>klFqy3r_6Le?sC*WDSY`fvpL0&
zP8PfG`Q&@Y_ZcKGd!kN8w*GAtUtL|0^3PITY1h@~(fsM+QoXG=+qdiH$8YWQ3SO+U
zebMXwBN_K?Q~nw~zOrSDN`LLg$xG_86=PCY)=s*wCLZ3`v*Kp*(Rax=TaO-Xy?MNB
z{fju|q$6G3hazW6e#-y5^YLu=q{D7&wj2`{d~UGtfZnq@=~<GW*S(9_obzV$-)#4`
zE%il*RQI0MtSeIyylWa2b>K+l>3g%6Ts!(Qx-Ics?bL|+8|R;0m*2L|=$(gJGJm}>
z=M>GLV-K${dUU_YBzzq&BLkzul>@8SPY&*7UUT%L{WdRNuBq1o8Gf$~Tlyg0_Yj}P
zDLb==Gvx}WDuu4G-YCm@JHB<&cCLe8EP{Jlr$6hFy`{4+s-R-(wOF~?TN0K&t-kw?
z{pqE$Q1(2()al!D3u=C|s<Reto6WF%lOE5xGjq0Wxcn{gar~`2YDz!yt(QyP=6W)7
zTl!DoxzR4IZ0zl!8Mj~W)K%|q4fQlS|0^+NGTY&BORuS*{H!UGby|A&@)PALH{Wj;
zI}}=WD@o>$*~{?2-<er@)n0k8gmRD89g5ueG$u+UDs#exTe9C1zu%s4IAn@pdO=Oh
z`SmiQFV00j+|?0zC!#>hXp5iQ#*-7i7N<N_mx-;?F9_Xtnpr=%u+1y>=Eazs<}3_T
z;up!O8?Gxqd-V4Dn{!J`U$<}lwg23_Nts(Jm3lWm*kZM1<&3Q=EvwFpNZkzfaSgwb
zfB)r$zbSt%SO53a++}`8Fjyyga=_Qj+o2NNeyg|oy6DL*>7Bo);%uk)%bl6^=j3cZ
zyz<XCd%N>M;0DA0H(uAL{=2fD@3*IYty#>!^lu@am7BLuoAUHc!L37+ZmBDI9IV_I
z67=<hs5#e-;7{w<^Q>3=Qha)=ob1oT>yK~d?&|uq`QM$Nxz8`mUuFAgQRTG>`sd>!
z40}G$QTfI^St59$kw(yh4~6|#|77$}eqPEMelxSX@WbsC|7{O<?kM;+<-?BWyf=m9
z4hjUir|;O^Z2Pq9t*|*unc?@_6PzVuQV(6v&QtLh+}~mFu~bl5W6R4u%YIESkFm9?
zty#|h-1=9^<9szsgCzw&3blT>F*JPgzH(soWp(fKd;k4eS)-i3%kck`&%%28(N`L6
zKmJYLelvf4&RntEshehO^?4VPd+XZjH=2^|_mcPjeN*#om88DO3c2LEV~WYAo=;g2
zpwVLQt6sY1*SWOW`scKxmxsQ!@bsyA_UXT-fzU*?Wo74=yVY)gUhr%EW*OG`|C4;)
z2uJ^PzWeXg-pzVx)={T2MOnm3q#kc+Ro&{pIiPgb!DrE%@ArI@R=dR`Smtx*LZX{}
z<DBwz@r}!Ke!O3m*?ntv{PZbB{icGiXUGfA>{_?t@GMKMIURCwe_p=asJ~od2S1zl
z{r_PlfB(;l=Y|I366cm@yR*$?P5-|tpVh(lgkirgSKb=lzKrAZKD|50<9DbJ6p{f8
z1OCiR-~3p6%0oxRQdY5vE;X?(Qa=j!?_Hd}e^1vw*+&MR|I#LTEev?G^{&s%`hDV&
z>01_8d^cxdVB!0B;=sGWciOkpudcjXdT^EO%9%IaCL3BCmmXim8k>E6?&r;Cmws`%
zvd^vhbEx%E*79%b=gQ09E$DyDUc2%BtoI7P6Yl=AW<7fB(C+%2e`{)+)o(IRo^_<8
zvi9Uo>2lwt%dErwb!)aVFW)ll;lca!PHE`s?kvgJ`P4|Z%qQ{Kw;wBZeZHo0UsFTN
zTVJcLy6tRiZ=ap~+4ZmaDqg=hI{VnAONZ8EzkbHI>dvoN_TDh71&hi)PK{}Me&&+i
z)+*~gH8=7^S%Qj8F6Q-I7Aw1Dm(wj3^5f38Ya1?2n&ViyC~nqvJ6rel=RM=?-!EOU
z%eg2rJhE_?jNs9-pYJbDxxH-CqS@mAX4x;R{y+0%+4a=zK|f#456?)b4QstyH+$F9
zySq4R_uu#wo#yAb^5l$}Rar-yuCH#t9#yF6?lX1nwi%brex@HxerQ^~?pC$U@dOj8
zqJQ@`Z*uS5aNN#9?}FOYDBImnFU+)Q-gsof@ALai_hz^9$J8{*esKBQKJ8D*hjlw*
z&zv<=S@i1eu|Gv`lIj9IS6-Y@^l7{KuPg6t&i-<-df4~;%i1NoI$l0ms=Bk+`RdvG
zTRxw$;r^E<q&Iov?wL{c+y8#p*_0GqcyMmBeeEr!U5}2dzqjZr-=$<YSCWCL`37jZ
z)AD(}r2U@!nynIBy<!(;-96skd%L*r_XSz4Y6Jh%CnhMAW|Z8HJHJu>%wfs5AKB|I
z#kbjBU!7aB!b(GBmG64-I{)*j@!tcc{Jnm|F?O|ER_Ln<QNHqZ^;ZkeJ^Ei~x-T$i
zi`T-g&gutiw~D`Ar}X>Gv-Ik1y?oq!eBF7sKi@o?zT^DIM>TskEuVAq^ILD`UDtXz
z!?l{VLe~F3vO@A%`u`8oXE!}CPG2+sD9_<Ldp~IH_W39EGxWiO-Z`D|9d|pEq9S(G
zTKt=N``N~~ciI(2Q|0B&RW=5tczC2NJ)-!yFJ1iO<n4QGx7OYaz8mG*%F^m`WXlVy
z2aDzZmu=D8ZR&gb+U~bD&-?98*=^2#b9rxecwdla^P<&9?WdXKy?+{Wn_;0=arB$C
zg$Kk}-8H-U^W~Luy02PWSy)?Jj+(zWNj=HeXlA*;{_BhMs_X0J7KdqVeJDEH{!aQk
zu6MD$t>*lDZmjm*685%4{PB8^Ea^DAFPCTUI(YVV_;t3`O<M(dqsl5jFZNZ7o2j>F
zYLvKpzU5S1Q_*exeLp9E-;!>&d-lnT_m0fVuB`sJ{p)((_m?-gxo-6m4P03De4qY0
z>sgut?@L^jKz&LEPG<f0m+#*^weRSy`9J*^dp`2xmVWnc-NmH7JwH8+mRI_I+ibXZ
z8z&1}TwI25<JR2=!gDj!@?+1edtbfq+T(BX4M`6_uRHzxHZLQ?J(Y*<oAx>^4Cwh=
z^nLB0q&Cf+h3_sraonXBEcVN4WrI>OclM&)`tNtWJDZ#NDNQ5j);9BNwwv}uZ#kx(
zU4CSHuF}-{Z3|C}a2@5JzW!{*!}fB!_sTLa^Ji-wFk@lh_`JUHdZ+IEdoh+v3%7cd
zdZZk86gKg%+4uSEw0(YB3r^fV)URt5QMuUf*q0;HJ2$>M*t&P`{<zbBGy0fpZmIcQ
z*Xvw=>w?d{T{CzyZ@hSvJim91;5(B`?XlC(Z<l6b*rRjeI_HgyYv1i(|NeLUdL)a{
z%;*ToPshS{r)c|j-HrGCa<WQtIsexWDYGr&cZ=-HayG7ft+dnOerc@T{X7na4@Up3
z9)Xq^2pnkXt9V(m>&cUp{8S-@3mJCppus0ahK6<y-aSIX!h5H>J#bk3QwBWl#K0ie
z6x<6QdQ&PnqOIxqBK%u}@AAtt`Gpo-tYMvfpf<zVJ`vO|ub6Y^szugQjrUIi?-`!F
zX1yxy{Jgh^ecnZDYHCiqeuHIQ;&#Pvwem^z^B5c&4z6?qnTauF&*{HT-}KI{tr>6U
zovn|xnLcrP_LXBH9o{RhuZe!`*DRNLZ_6UpH-E0n_sjh}oOjudKZTp&UfP+RUw*Do
z-Cb`N>amdj%PYgQpDTWNY(4!k$eWpg!yu`@;_3XG=KHRm>G3*yd|mVoz2w*DS)=#;
z$-Q=<uJCty{kL1p%{qzh&(Bxoo^nmrT*t%8!P2ubA?)<^BKbGJU2jd(&5Zw2YfzqZ
z`a8ETUwOg9ij_+l8Cc{3ne~GoKIOc7ZEsb<!Oy$&wm#NkSv}Qp)`V5PQr~8Mc=en;
zF3H{Rf6V`jH~DQQYcW(r|N1pEeRkh$qn*)9HG0)n1#LeWd`xxD%$<gJx5CX_UmTp?
zcD8bL;+DC_Oo3}BPnwx>`u2JMJ=agfNia-tXHTE=Zr29eYOmj{vH$1RT|m;fRr_-L
zm-R|&o7%#j#@R7Ea4)-m;roh(ss0zQy;-<_-*qIV%H`d&-5*+r9jJYtwNUfixAmG+
z&CV^^|0rtDl}ii^O#L@@OTCTzKWl}D$^L}-xhxF~$36DQ#972;Wil{4ow=eh{599B
z<eNu3r<%-p`RwDg)E}%lrLV4R+~eo#D_Zw@>za4kH(1_vbBD%Wp8cvl(q6;o*XmUl
zqShVt*5zeT_|PF$!CSfM)usG(>V7@nOUxQuKF8|)5wl^OeW2EMRd)G(gDd$0c{3O7
z-{&5^cy~4=9&Hw_`<V6V;FLYz@BdTweg86t;lTQmITI(?d^D&&^|13Kr?J&8G5xJ3
z3=IdAvmPw%%lP#1T>7+al0Q%0kxf6JCdISt(xXSaGsFAW+}@S&AR~7zi+?&NgPoxD
zleuo{V&`V>x7Xgj!@@lK|DVckKhv3J7T1I(tnf&Q&ry(hzr}>1p+WuIqhBxDf9cv^
ze{+22YdfhgXQy7#+3P79y0d7n8RuJe`|pR3l}$4^?Y`kBtKKeljq4(-Hk9}2$1VH)
z<7njj*PgR4tUmr|e>{JvW=!|=C@BVq2NOR;_r988<$t#N^U6vmLy1gA7Kzf3y@s#t
zWF9Bz)lV1i6Q9S;An@VHzc6J`cG<y+V=2qR?$@POvXgt_KTmL5etGGVB|ogXe@mG)
z{@(DOnW3WN!U1hV!;8_GEPN)j&L;}*;Lqh?c%W!;m4g8^gzn_N2WdE(o$~_PaI~M?
zf?Y*dwLtk=^>xX#>)O(bF4ic_Tr)f2+nbwqXO{d)ikEKBd*l4(91jB{+j1#J1_lO<
zMK>xudwg8(3w%{s<+Ma?mBSZ-i!6)ozhjM2o#l3=$HQC1?@HebZvK>*J`w4RKUJ%Y
zrf(^JdGTw>rW0#H8RG=gT?qyUw<Pwsn=W@d*9p|Rl(epx@IrpkMHlIgU3a=yx_;rj
z=(A|H%T1Tl9s87}-Y-1zS1#Dg)BB~Lj;y?U<l~GGozgh3%B6b8ymfgU#9ka@VE9y2
z6uvl;GmwALQkS)n!r6kh?q4hdQ?DIa-^q5T`me%8wMDaBxSx7$i}AGdtq)tc#V<9#
zy-ew`s8m_oHj`3SP+r*NV9v%cVfqT?IQPy)IqtDyQ#*9*bq;NCi%q-e!dAXX`@EU@
z<p*(Q!N0yNY5pD4Gd)VGLFYm*Bf}HbtOr{gGUj+MmF_gr)0JQddv@^y$861q6Q|67
zo&?H-DUEqN3<~;z%<JcOTI~+`Wx41WNZmQfl@o8Jc}<w*)r0I8q0(M)!I^J-L+(@`
zyfJ&W|CQ-4#Kk9pmO*j2EMkkh+xbn1_o1(O|8|i*FI}d1U+K+|2($&cPip1MJrkqY
zqL)vR(DZl<vbmw-)s>aWm2+p!()x2PJ94T%IIx6FKUB?q;aknD@9rnStMJO(<oMG)
zr}i)5h??lGs~xrc$@9R9mTpi^eZ;%G<$hBvL|19=b!V6I&TX9?DIH>hrD{<gUpCHO
zIkot&Q08I1*_zg6f$c8hkC#qkQ{XO1W?-o7l&WAA{_AGanIUsga1oP|aG=^ny+zYI
z54~@FD#WW0<zLeGqO)4~?YxdX@<-GIX7flDHspy-T-aeIvmo3!v$V<7!LV7x_{cG9
zUETx2kdXfN=+`NidO=-9DescD6%8wt0=XC2xxD<IBqfw8AQ-qt-AFfI#4GA6m+vj7
zvtmJZfxmxk`JZ#&;yD9@PzvZ=fYh!6n+u|SNRe0ez|}=+(Z?ox#*)i_OPIV1ICQ0)
zx@FF!rg?OW&*Ofe2=cwrA^F*$T#IYYs`J9puU2#QBA0)T(rR>Eepyvm>g@Cqt5`3u
zuJxNW?t>g}<C5`U>WmpL)|xP}OPzhbf%8tg84JS)0oXLqLghG5PtUm1i}zf9S@Nuz
zB{MT~-?^v%LU)(t9#SjdzjeWX2B@ner_LV`yEAKQ`6rF{1%@&V3=9^n&`KRPpY|i+
z!PUdRSA%D$nC0XvG&@AL1$$L8{%e@84mzD+kB!}jq>A8gRaH~<9zN$}U|>+tk9iDg
zPdrdv#1^OO@?OYPflF<b!<Fe7ulGhiGcMWba=1fFAhSbG>DI#?8s{W!S+f^4op{-t
zUDO$;(51+wRy84mef<HMMbA66gjxk`kDR*vh9%H`QNbdOMRhLWM?&Nn7#JMX7O};>
z7mii9<-SDS$}^;W#eJ~hwjEZ&v1+GOXStgk`}ou4*uCgy_v|0Gn@M%t60&tDY1EjX
zp?R_7w$WFYwH>nr=c=DloaO!{e$m`DLQw*yYP<YOCa>TR3^$z0&cMJhp>s0(idnS|
zC9_tj2?}0SiSpQT#B71?#rk)9-+686UNL)f;1up{LZ)i7D&D_!c8Ts-wUNn8*!BRI
zLHZ|-*C)iPZ!A}?@_okxD)(4AtR9(8TcLbWN{Lxeko7ZPjPK^!=<XNGbZ*|9<^5&e
z+bO5E<v;((lqHyIq2cQqq7<D4N+Rbvr7HHio6O2E3ls^IUUbsMavNi4&iz%LJw>V~
zie|0Y_*TU4TY3fK8=tODHKD6YT)WCsCElfgVk=+B^aGdDET57ljp-R?7ef~<+r~I&
z^_5<iterwBo(fjU)<;u*Z{xg}d3@#`=aNYo`hgesdY=MWy2ta%0dL1I{DOj+9aTcL
z?o;xlKdgIuTia#hB4dI2Cz(d?=cqk5d8D$aykcg^-tWJR7lpd;c7(XJfTv(9=H7T-
zVe9xsJdktZycg_?y0#U+7pnD|;+vxKYw8O1i_;ewXE=Vb6?86{>7gufbNUOJi%g4j
z76~mn?9!aW{7Z1I;w=9uM^B~P+`DtVkgaFQycJV4x?eb7lmr!8C!DSvc+GQB*@d~&
z#Kp8DOjvdcZ-i&blofh`5*J+-`FF_eHTORFYySUhd*0+InFdBLGH1EWp=jk)(zHTu
z;<OB&i|pH6GdueP=c=r77x6Qh_`-S7@pory`&Y0APOm=CaM{|M2b8+v7Rjk!ym3=d
zNB3g5OZ?5*soxLA=5V^CA60R5ahd3Hf73mw3igwWI`$QB$T7H>wCLy>&0tnxW>BID
zxBPulf%Rg<qG%VMi@b|Yy2RGZ6$0fHk9T}~_SCe!W4Y+N=$K2^qCOX?+w7M?dVUxO
zE|+3GQP+0vqQtp9i_%<PKaB&`>kZ{QtUpYWUAL8qfuX@c)#SsamnA2y=3Wm1r6`UZ
zC+77>j=1D66|~5@zV7X7k$2@cSl&5HGci<nSngge$iTp`;E#~iqp4G-JlSe<qr__N
z&xG0Qg$f)i&sZKv09E!c)ODnp7?}DecfSr_7xQwi&5cQuC$HsP6ZP~jOU!|N5_zeI
zKTRxd@KnoTDqqO^m!;YnPYZp2b;GKLWEa^^o_&7Kdy<%a?>TAf1<C~;ulkZ$pS7&e
zHZCjEA<tyi$`-3yhkA*QnSo|c-PmgX^XKkySpI%epySr075>JvJ{x52{ni|5*95BN
z78e<RxaIqWC2->U%L4tHOP4Gaxz*P9eKD8I?EawVOG`?1TrDh4XvpYqHBtC3m3vn0
zRCU9P6{TLi=QVZ->ArWryE=Huq)U01kMCZ2)Yr=XMzQG!TX1zUb#~)*fki2cwt?I_
z<?@$wQLon_-^w!7jp7z2re}Buhd)|6jqQos;?x+`yRN%zCMNaY^7;QuRZ1f2+pfIO
zS>{v3&QG<@v~LEva(&U~>CXZene990IO*(3lO5B~PO-Cn`M?fbe?7@sJku-VgV(HY
zI-$WgebUn+++$NGs&NIKp14BZ8PrM$-ziyf^?NB((AqPL9}1cUA5zw|KYtX|y4iUv
zLwftAw`wLkcLn$~&il8+<M94v)8)#|J?+~e78kGDc*in*iQBez=cX$mNhOA$K-M$8
zwf6OwLzcS?E+#r8GPa&oR|?X4**fn_X0fHv*JMx?^hwLyeGh}p+AA*3;TN8$tXfzk
zAuQ!~hR4WfseN1EDMqQvOWi*i861ALH%?z}5_Gxpw*6D@9;fLnoX5R&c|EEY=iYL=
zE_GqctaIMiSb}f=`f}NOOI7=B&tI0{;C&dfc)5z}g)W<{$ct90_Wg&H!A+bAU)-cW
zna`96nzLc%iW!bB*Opgqbak1$P{uawoGRE^hXnQgUrzUsF1zV-b7Qxa$}R~|)V}Nu
zGnzX?((Hf78hsJtjO}j?Rx9*3H9z&e`F?>kGs6jO2evparTXf+iW;V^Cl?5^zep35
z?8-RISY<jnOg(~G#Q0R-vX0L3D5(#gcUk;+e^1*MxA>2c(bNl_AyS`Izt*|DTk@A@
zmmx#Lo>OO6y0yOLK9=6uu{7Y)s_=|UVp-cJeCoV)efeK~Zrg>?pstR?JJVUI28ote
zEB?9udZDp*-?U4gG(CKIS6$rTo*A^@{?!gh>==I#lFR)0+(O5qMT~c$E8nwE`qDz6
zrhA#^T^6RzQdgGwXPurL`V*YimH%u6)t)$4uKf54YZa7=U3yWnD@7~al3gN)>H9)n
zMh2TB>)GQvJ3IIJId1wiqqyOqT7mp60fqz41*<^izya?+zdFK$f+npG7Vrl5(Wfk)
z!^~sW2wFgLXp<s?!iOJU4|I39t(AHDTEr!B(%SO{y84#v65rHj*j8`jH`d%A6cnVh
z{$g)!$K9EX3I`s9fXk=pXsc~Je@axO%2|K9TEA?+#D5q6((U&|=T$8IU48r8oe!l!
z=Ol~ubS16o5=zd`yU2W;Keov7`U^iqqjvEp!w*%fzDnEwTP5-F?jiZlWx3w*hKZM)
z?fIoQrg*ol|15N923OkF8r|;)_r)*Cy*cTd>wWg(<J)TXUwHCiRwTIp4e1iZJxzY#
z>N2^0?yZ%<cQ;H>2=$0)mfL&pzi#H~j?{gAULFK`+z3;qo>8%nF`Qwmy6517M{At-
zopSGKHufuzy)n;r>EEVx|NZP=fIG*KcKP~Gh94ejYwlRnm-X(oPRpBp3*QGipPsj9
z?M>(U+V$Wb>jYLvN_&0a^{eUguU0)(jZas6lC@CNZ*`J?VCG|=U)tdQFtj)F>AU*%
z+e`g_=bozm<!UbV!%Fa_MCWxuZcs*qC|Rdf&%D0Ln>{|?_VdNBt5>!E`1)|yj)1GC
zdso)Y*xKrg=wf%Q@SAHj?fS}<D-Y%God!*K>x;}j?Ar40_x8A$`w#26-M+4P@;YYD
zi@@03zuOkpH5Z%~`TN!Omek!?Q0G)2-$M0|*c&HM!8JWz-Xtm6tLXavPrtG!_x1lv
zep>Ht{<+lZTq(BhcO*EkuCC$P!=)!%x%%gZCyUJP&!2t&XCuewBQCCsR22dzo~V1x
zpVYqR@{1#fDnEZue<~*aJnij#`}~V5)h@Fgk7Ba0<UWpQ!H3$h#T^z_leL-r|GoL?
z`8@B^{w?^vJyC4Fljyf|ACE3{ud6X!mw$hUc)g9#t{?BWJB4yx2bJs4KE>4j>^*fl
zzg#U8W_o_}Qo6Ka@vGj*?++!|i+@^jALl;L`au9xnn_OWR|c;!V`RYB%Z@E7+O*wh
z<9vq6G3V<1me@R#NkDJ2AN)|Kp=)VrX=r#+{3HWILugRYrBhS2Yv-~uoZwsz=^wki
z2uThKnsoh>#(PkWZJ;Q1HXPi%{~|n%myx0I_(|pv_q8%l=h~dI{>EyUVKP4<zv<@Y
z^xp=PKXupU-Z|B_x@N}7TD_Si`}`OgY*?YjqVIK4`QuTx^5M00uG!yn{=I&*vu97t
zVzXsVF;08a?naeMeew9bOtkaGx6b|LwfkRR&pjTbf8R{gG*s%!YlAiW-}SzeT6!q?
z=Wo;Gb4$;=>)!nPd8HFq?Sk-r!_)3Z-B-mzx<p;PCY9W4ceqr#$iBYV{&(ffV_!kF
z8Uu^OM)y6R&cBhqpOxme^jY$C-I(bczdmo$jsItsov?q$-_7>bZyOz-%{ZtV7r#~Y
z|IDSuW_RxXEI#KiUt=FMaZk;W4e>V9_QWUqux^gpH|=-Aef>+@ay)-8df&V=IeK4w
zM$wM|uZJM3PBekq3?=H*`uZ2IDKycVW~IM$PmnmMU&$a);UfFdNHlKVh1|O>#@*6x
z(R>?QLUONc2w&XxR(LVnmdL!$Ie&iNo~t$WFQfGBJx8_eYc?2W>0DfFlpZU$Wc~cg
zZ7+9hoxEF6aN@GtPc)a^Z$EcuhTZd(uk?<9hY~cGzdWxs<=V<OZ!h?z>~T7L?!vTX
z>p)VVaW1PzrFpN;Y_QDV=oT9W8O!_pIz{cK(JLcu-E%>$$9B$5*;!I>?BzP{+nbkf
ziNEmm{!4an25iv57&%~Ycpzx{A!@f#t;c_@pe|k0J7=x_ex4T@d$0P>WX*M{VfWr*
zD~67qvXPQYG*-2l^yxFWdIp(Oy6WSJyN}ElABj7jd*aUB-LHPTED6c1t~dDq^`U9Z
z`E@qCqcXZKueuQ&a?4`!zb;6DcGObYbkp6h&9D{-14E<xo7mnm{l|VGDzoAv&Y1}X
zdQ6o&>BFDwcy8%^KHcifM}M^9_ZsqCSG;@pw`bAzM@y%%F)%RLslEzHehnT${PXgp
zk5ToBqs#cZv+nHvzUIFByT9*)%0FrEf8-Q;{fpW+k;(s7X>FMXc7f8W!;ik`-ni=F
z`#iVbW2%JaiH{HS!6^VV8tcBN%_g$+rTKMX^<&<;wp;w}KiVDdab8Q{%Zhb(YYzwP
zcifTM_3xKlZtpvA!P}u>Y8v_{dV{uRQ`nQh(_Pmze^!dfJp_$`fQCR<D98EQ&6xE4
z-|hM(FIx`_iFUeg&iyyf^v(}ejYS(@-<+B*o35hbZ*yi|QAJYGp`Jdlp$=jgLmQwZ
z$h+r?ps(G%pJy(aDcjH7{rJsIpXP%hQ86{<Z(mI;jTYyTS-W;>Lg$>HFa9{!$6OSj
z>DA4pulnEU@5BDvd%w>*KIwb*M(2B(B}otW{QSMSsJpv(^SAT!x4#IPoY|bL%h=iF
za@w`X@A2GeY!5g;a$Zquc9U5!+ciaF5ik3Tt3FY=cOQGg$3++v9(3;AVfSlc-RbkD
zzYE{(>SwDhRyFm`4{{A%7qi~i>G#3&e>ZHLYngWRU#9f*cYjhY%;=f@bJc|pvvh^z
z=GxXrOnM?brO|OASM~EBk5YH_$Itn?Z{8Npy;VB@et!*^dN|%+2vRa&jH;w|75w==
zs{qs#U|{NRxt|qs{7Plkz1jX}izNa!dvE_=_EOC`sL@F_H2=&l{^J%iPVd)uw1}(F
zYiMU_zpzMg%ZY<AX>D679`0mdVC1jQ0reFta4ijX62Jbs#7a%l-b<NR>g;nwDgE#M
zJlQ)898QiRSI)g?HePzMeeTP-68fhm&6vq$R#15|f30kE^j@Y1?eh+;o-%3HM|rti
z%lHrT%voj}St-b%kYa!Sqh45ctPyL2<NMmLEDyZRAF?tW;PLBaU{E~7&7j~?!N}0U
zq0i7D@Q{^3Kxq#HgHww*gG0v$CI$|{ICMo5xIHFc5-O<cd<^Q8d%F6$taD0e0stub
B8%6*C

diff --git a/doc/manpages.tex b/doc/manpages.tex
index dd89acde2..2e06c2a69 100644
--- a/doc/manpages.tex
+++ b/doc/manpages.tex
@@ -719,8 +719,9 @@ about the session, depending on the following specific options.
   the session as edited proofs.
 \item[\texttt{-{}-stats}] prints various proofs statistics, as
   detailed below.
-\item[\texttt{-{}-tree}] prints the structure of the session as a
-  tree in ASCII, as detailed below.
+% OBSOLETE
+% \item[\texttt{-{}-tree}] prints the structure of the session as a
+%   tree in ASCII, as detailed below.
 \item[\texttt{-{}-print0}] separates the results of the options
   \verb|provers| and \verb|--edited-files| by the character number 0
   instead of end of line \verb|\n|. That allows you to safely use
@@ -739,36 +740,39 @@ why3 session info --edited-files --print0 vstte12_bfs.mlw | \
 
 \end{description}
 
-\paragraph{Session Tree}
-
-The hierarchical structure of the session is printed as a tree in
-ASCII. The files, theories, goals are marked with a question mark
-\verb|?|, if they are not verified. A proof is usually said to be
-verified if the proof result is \verb|valid| and the proof is not
-obsolete.
-However here specially we separate these two properties. On
-the one hand if the proof suffers from an internal failure we mark it
-with an exclamation mark \verb|!|, otherwise if it is not valid we
-mark it with a question mark \verb|?|, finally if it is valid we add
-nothing. On the other hand if the proof is obsolete we mark it with an
-\verb|O|.
-
-For example, here are the session tree produced on the ``hello
-proof'' example of Section~\ref{chap:starting}.
-{\scriptsize
-\begin{verbatim}
-hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
-                                                |    `-Alt-Ergo (0.94)
-                                                |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
-                                                |     |             |      `-Alt-Ergo (0.94)
-                                                |     |             `-G2.1?-+-Coq (8.3pl4)?
-                                                |     |                     |-Simplify (1.5.4)?
-                                                |     |                     `-Alt-Ergo (0.94)?
-                                                |     |-Simplify (1.5.4)?
-                                                |     `-Alt-Ergo (0.94)?
-                                                `-G1---Simplify (1.5.4)
-\end{verbatim}
-}
+
+% OBSOLETE
+
+% \paragraph{Session Tree}
+
+% The hierarchical structure of the session is printed as a tree in
+% ASCII. The files, theories, goals are marked with a question mark
+% \verb|?|, if they are not verified. A proof is usually said to be
+% verified if the proof result is \verb|valid| and the proof is not
+% obsolete.
+% However here specially we separate these two properties. On
+% the one hand if the proof suffers from an internal failure we mark it
+% with an exclamation mark \verb|!|, otherwise if it is not valid we
+% mark it with a question mark \verb|?|, finally if it is valid we add
+% nothing. On the other hand if the proof is obsolete we mark it with an
+% \verb|O|.
+
+% For example, here are the session tree produced on the ``hello
+% proof'' example of Section~\ref{chap:starting}.
+% {\scriptsize
+% \begin{verbatim}
+% hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
+%                                                 |    `-Alt-Ergo (0.94)
+%                                                 |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
+%                                                 |     |             |      `-Alt-Ergo (0.94)
+%                                                 |     |             `-G2.1?-+-Coq (8.3pl4)?
+%                                                 |     |                     |-Simplify (1.5.4)?
+%                                                 |     |                     `-Alt-Ergo (0.94)?
+%                                                 |     |-Simplify (1.5.4)?
+%                                                 |     `-Alt-Ergo (0.94)?
+%                                                 `-G1---Simplify (1.5.4)
+% \end{verbatim}
+% }
 
 \paragraph{Session Statistics}
 
@@ -794,27 +798,31 @@ For example, here are the session statistics produced on the ``hello
 proof'' example of Section~\ref{chap:starting}.
 {\footnotesize
 \begin{verbatim}
-== Number of goals ==
-  total: 5  proved: 3
+== Number of root goals ==
+  total: 3  proved: 2
+
+== Number of sub goals ==
+  total: 2  proved: 1
 
 == Goals not proved ==
   +-- file ../hello_proof.why
     +-- theory HelloProof
       +-- goal G2
-        +-- transformation split_goal
-          +-- goal G2.1
+        +-- transformation split_goal_right
+          +-- goal G2.0
 
 == Goals proved by only one prover ==
   +-- file ../hello_proof.why
     +-- theory HelloProof
-      +-- goal G1: Simplify (1.5.4) (0.00)
-      +-- goal G3: Alt-Ergo (0.94) (0.00)
+      +-- goal G1: Alt-Ergo 0.99.1
+      +-- goal G2
+        +-- transformation split_goal_right
+          +-- goal G2.1: Alt-Ergo 0.99.1
+      +-- goal G3: Alt-Ergo 0.99.1
 
 == Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
-  Alt-Ergo (0.94)      :   2   0.00   0.00   0.00
-  Simplify (1.5.4)     :   2   0.00   0.00   0.00
-
-\end{verbatim}
+  Alt-Ergo 0.99.1     :   3   0.00   0.00   0.00
+ \end{verbatim}
 }
 
 \subsection{Command \texttt{latex}}
@@ -910,14 +918,14 @@ override this default).
 \begin{htmlonly}
 \begin{rawhtml}
 <h1>Why3 Proof Results for Project "hello_proof"</h1>
-<h2><font color="#FF0000">Theory "HelloProof": not fully verified</font></h2>
-<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
-<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
-<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
-<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">1.</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.43</td><td bgcolor="#FF8000">0.00</td></tr>
-<tr><td bgcolor="#C0FFC0" colspan="1">2.</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
+<h2><span style="color:#FF0000">Theory "hello_proof.HelloProof": not fully verified</span></h2>
+<table border="1" style="border-collapse:collapse"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo 0.99.1</td><td text-rotation="90">Coq 8.7.1</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="2">G1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#FF0000" colspan="2">G2</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#FF0000" colspan="2">split_goal_right</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
+<tr><td rowspan="2" style="width:1ex"></td><td style="background-color:#FF0000" colspan="1">G2.0</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#FF8000">0.29</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="1">G2.1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
+<tr><td style="background-color:#C0FFC0" colspan="2">G3</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
 </table>
 \end{rawhtml}
 \end{htmlonly}
-- 
GitLab