From 62c97c60e620c93543367b436b35d7960f355e70 Mon Sep 17 00:00:00 2001 From: Jorge Sousa Pinto Date: Wed, 17 Apr 2024 16:28:03 +0100 Subject: [PATCH] fixed some obsolete proof sessions --- .../BakeryAtomic/why3session.xml | 103 ++++++++---------- .../BakeryAtomic/why3shapes.gz | Bin 6112 -> 6533 bytes 2 files changed, 48 insertions(+), 55 deletions(-) diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml index bd39627..1f64a09 100644 --- a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml +++ b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml @@ -6,6 +6,7 @@ + @@ -23,68 +24,60 @@ - - - - - - - - + + + + + - + + + + - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + - - - - - - + + + + + + + + + + + + + + + + + + - - + + diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz b/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz index 21920313f64df891fe2bd95eed669d0a42274b89..33ca9799d8d4aa1e43d91d8c559606fb396afcc3 100644 GIT binary patch literal 6533 zcmV;08G7a)iwFP!00000|Lt5^j~qvGe&?^?o9tZ}$onv?g&Xt|O+eNztVR35Fodi; zyaP)!goa#d|GmG+qbjSrXGlpiw6T_#6sz)xh>ZN=%B=R^{pRKUpTpaH|MD;Shx?nm z+kbp%UjF9qUxY8i&550O_;B~bcj=4o|2u@Y@!Q+l^y-^8;pW?XyL^}E{q>7*bNd$z z7bp3K9#3NHN84*67Vl5$q|d2Q)4$x^<~Qi?6VTKNVv0H0M$t?o(AY+teCu>?!u`Aa z_S--G+sU1L@8j%E_#ub*=dgU2@%H+~yRTOECoc9c^fyDye?D<@;x>FA-hT6rggkMM z_tytZu5Bm5r>FXM;{L=PNcgYXgx9ZMoL;>wcR#%RA(z`1A@C-7_z>P!;h@$2?+^L@ z{dezPyuG`B7w>M<%{%PCuItS@o|YJhAjs5z+JHYm>glzQn1(~3_OG;KEFMQ!qmPF} zdysZ*`3f(ame8e7lAnY<35|6_D;S`$d?}&5aDWn}>>9u$DMone`O^>YGc*P5l<&fS z)m{O@x9`7i&qPBIjT6^+1&#N&*tyhthk`|9O~v1bA8QXM8u`a}?S+W&D#+{b-97km z(1A+t-&Ou^)=j7zD%KqeoX{C~Yu;A7?mew649UlGy6|C>lzJw9t01AvTNg0oy_BZy zGKqmTsIdid9!MRpcl)Z_X45PU+^$F%4P)3Kr)P3Bpjzg(2n!gWgsKbp{hP1D&HeAc zfBWvQv$kzooh}Ye=9pQDi?O{^b>nG9V+R!~pqcS$KHGWyyf6=_c7w>Q1-{(}D$T@sT za-Q{}rFAtbXT5`TCH(&TbGq-pZ(XFOvp#BSop0k=*W1{Ix%si&{P^-e{^=k7^K3*N z65e7*UQ~2f7q>Ig-rdz|!Ut@`n7=)X>6zE( z*DtmSewyH?34WU3_a@%`v{0+-7HV|OmY`=#(6c4z*%CJMA!9PL&6(Ne%xrUJXLEMu zWM@ux=43BzPO+0TC#g;nNdY?v;9N1XIk(!J+icFvHm4?=6FZxeY_d7`j5hc6LuNL= zhZ|m*)b`uIo`Ly>&tSiR`kriidwW5?uHlH7;H#dS|Z};3U{1x9E)`ObZ7*>i8IXAxZZVyruyRDd%e6bQSt>htU za&undao;BPzU_(-`(>WFyAPA6`!G4V50ihR=kBS7vkPzei=8`M8{~O|x@h>{2yQi3ueM0z~!yv^pXC@HA^YB(Qq zSgZ5-65ZisWKAs0nlT*0?@orDwAp*4(TIOYURP&nw+V$lw5#f-v>H5r-;$A*l#jG` z&AVO8N9Oc|1iMK0Y)khJUq5}8@;4gCv^*()Qud_uNm0dwO`(0zd<7ccfaYhQ*$HS= zu_#%gr0^>DKqECvUwci+3A-C!kqs*9~ZT z1{#?K;n6faabJXkR}VV_F>9H=Mib9!7rkTeIIHt&`tsqp)Yc zI<8+G*Rwb--W}JBwEs7r>sgU@_!u$XM9#?5Fei8>WH+ev! z&Z9+~e4V#HfAe&L=c|4^fa2{Yu-B`=6|BB0%`4CoE!uG*Cos(Y=Hv|Zn+XnFV6XT^ zI2_INK(a!TI+sr|k@~5NT;F;MEqwTP}{+a znh##obnrqc1tlnCXuPEq^EnJ*U7C@9NHdwCIx|CA4NV5JAKvX}GsCS{)7?Nd(pB&9 z{P6B)T5pXt93T$VNqWLDg#&U$)ePlqhCSsFdYB<49(2P|lMuT%Lw(H*^`mCUPS%{P zI$3eDjQk0jz`(8tUUt*Fo%L=fz1w{%XQu-%<37m@8Tc{4jX~XvoxJJR-wnH8LKW-MDTxn-Na^k~~;5(#;5I z6S%xE!rn{|)zWmE%V%H0t1lr3<+?{|Y@6~{njtv~HoQsR-Fq-M1 z&Sib>6e6g<`IvD9BpS3fqkc4L@cqU|P{JYDb_LWM#;`%o&*W$TT_(u0>&flFTlCA_ z?M!@akryrMv6jR6q{BJg!xh%sN=3iKRC@J^N{_C-Ix#LWm0nv~`Y;_r%X;@?$33QO z2?eDmLWF~A2?eZxrpgf-MZXNCOCuqghwEsnU7+w=xRW?td7KG)fCSl^&+aKj7k&sEx@6S)+tB&oCGt&#-uf`(jz>v%vultMavn$> z`&}AWlCmmyx{~Y-W7r_4XL2-v@TeZfqrJeRy}+ZrK;M;?b3C5k{fP6spGss}X^+vG zuXxmabdA-G7_C=?+LrQ8c=RJV?l+Px5vHUWIo?6HRG9X7%7nMPk+9n~y{E!;;8`m%?biLq1VkJad(fd#&!|$4WFvwQ?=%EeD=kJA?r%N%NsV~sB6AR zUq?21hp3l=bi67OU$UWaKM$mi-7ZSr;i>2_LW&Kqy{1^4zM{7J1R49&0(APdc2_JzQb^sAk%d z>fP7J?s~?Bi9S4jp@K~AF(vL;-h51#hik0v!X5r2!kr9vD%{o7@!>VzQTJU4ccw{q zxOP{5XX+?ZS8=$0)qcn8n1PYQ)w}vTQ3v%qs>4GU{&%ttldEw4QrvF+sL&hViV z{4>nt>a}?P{BL}(cBSRbwTb($-EMBz;b$Mbja_S>?9pdDYWrkw^)2f4`9MwQJKMky zc-_YX*;7llWtnVrjTk^aY+6iXf3cjkd7V=;Q?|C$5=hZb5|61`w^XcZz8;-zhnrX> z+(WBq5mqT#&?5n;FFgSmS;Q(y%OWU(*5{r^NJS|_%^_-3t$jPIYKuVQTIOC67}c$D zCu8U|7Ztr>t!AZ?7Xrg1TG84CHf|Ewm`z|h1fB#QhXVDPtrD(vuC(WMu1CdfPmZcR zI_a`hn^HRC{Hi$TS2>)Wnf!UmwEsj*`d)o(g|XJ7Yb?)? zLPW1E&5Jy6Rxhh#7-#jc_Jdi^>S^kFR$pKGSzCRcpy8WqsfhEvI;n`GoP6k(>K?@= z(1e;o>(DyR3W?TsFoSvLyRq!t9$_>vSxbH;x;_-2ht{5*mX#d%sh(4*2~oXe3>*~Y zjv|d9OqmBErSv(Z))sluq8@8GoKHHO(>+{a{Zk??VZ>ZUTxHH9F5$`TBCgt>V2wi@ zD_8j15rhX=yS#Aet8#U_kC=iGKN(9$#zxlj;C@MQGM*%*I@&bfPgBkC{c1X2uFr&c z!|Ax3PL$1dzo7a7GvRB5OD`CfIqPz1Z1tHfhMQ=;>^-H;iF} zoS(_j0FWC$`rua#MqeCG>WjlkeQ^|dt>th&>2OZ>aE0}@)N%4-wqID7^?c~fI0Nb+ zHg;`kNZde7@Z}A@ld8+n12yP?#xS8_jFtn;9p?Qn5z z83W&J(QcwhBgh5Y2VJnfI9}8j$BX*nF!5T;Iik*w7xnq^qTU}b>JA^fMRlu3*I3>- zUbO3i`>pNd7A1K=@{F=UtNBfGm)g~zUh(EAX=iP7l5Jyc11DipJNoU-@RPd3aBO)0 zD5LJW?MSR!Pwt`Xx&nGSEVR|7+17jxFuRI2LeHeMV3-5PA*Xzp?opIuwbQDxg^UYXD_)va+1W zE^zJDOU{p+9sSYmr*Wn{YK`QUi2A^kEMtjmDbA~c|Etp^rg3pL6GI`J%bfY8EIH{I zN+{Ntg-b7_eQB^NcjWkEk9@yA#k>?jDw~Zqh>2OS#RqOm)HasI)w$;STq9KqLUS2& zWJUTYQ^s0m(KjX16(3;{xFJ5*nOZ*W>2|Da3{86~0 zut#BzLLY@X3Q!Z*=|denG9zVFLM%cq!RVy5a*{<6ye0bj0iDPoqsz%zC3sQAln{*y z63di~@udPs>!SwTcKIjNumT^sQ#jQdQ&$Y4#8JQ^vqD1wQGPl1eT-E64bCtUi-4GAzp5WNAl`c}DFQlTCq& zok19o*RlFc!eB=Nv$QkCYuIq+iNj*F6Atl7%IjEtCSi15Vi8s{X&iI#E(O_k1ZIV2 zaFPwH`ug0(^Jo#N3ggyBknq841U;-y!X<^5)*Y=qT6Q!KcvoQ~S2iF_IcyQv#wNrc zk(t(Fku*R&dD{)aZ+*tWhGJyrc7 zkJ^?vXF`utS`ZXpwYnGr=tUKrIr_(c5Bl}_we%mDJ zk+a(9BP`AriHx@b%E?cs2P7cv6glc)+f4APp5 zB4y`Lws@Bqgf6;7xFX8By&^yCTwCBKwk;vX7pYei;%%Z%e z{>j;*w9Rlm$)l7jiWg+VzIbdlDqr}IUh+Qu?gCFjCAE}-+AS>{U}eS9YAFx&y7A>t z&NtWv`7cs{wg#NNqLT z{$i!UDaD+)6-=UFb4Az;9H6L2S`=A}cijC_HgVy6L0%iJ2@>@>a}1TRVvOnNv1^Tu z|D|jMs$oRV;-nN_I)em;F^5b>qBJhf&9&z*VuS)w1*@Y*<*6)b%d1?ZVm88P63mzG zO(ZCjfxu=$v8YLm7bvc|@K!C{I=VfxX0so7gs0&svADc26eFM&oziso z2Cy(#t?|ubC4Wkm4wVlp$osOQqXHhZlssl+paQg84$OspN|p%CNb{wL9yP3%ln<%k zGKVu(BFCk%bWh1LP;~Ao?UGVzeqZ<}Wr>v9L5V>HI?j~Nd-}x} zk^x?1?3KHGQux3jTI^nqdE3 zt#U=TsY1bOJpM?OZ?i9w?&-N3Z6pB9QLaeIJpLf4uq76{aWA%oDs4LY;UnS zB159^FDakb2xm!jx9FdXJt|YWqXb)tlGr7tqz*8sh$IKAZ|v2xDL*-Qez-}&7tk>d z0chcRNd>CNg0aS)KNtJpG~@7=0dZA%O{bCA{}L4a;!E|CMv3QQ@0_xQC6!SMGnC<8 z^9A*Du(lYFEMw=>o<#uUOYki|850vK1uIMlFnpbt1@$GOl?FFWc8}=_^ObpeDO3s3 zX%k@b)(8i$!{|#HnQV}Y&1JKH<)2p)fn-EzB~do%z>xLp6oLMX6>1jdjOnqZdH5()iTw6gHHSRK4_T38sTOCGTR8ZwL=cJmRMe-=>| zXAFSK7iL8Y62t_mJ-Q7skfm9S7N0{DrGrSos;7#hAX0n7kyDmZBy8HYD6Qq^5G6}X zpO|SyaD{d>eLJENP&ERZlFQDIJhw3P84@!4ERy39ph+&!ePGmOS(vieA_HmYyBGS_ zN`r*9&%INbTlz?8iB>VX+s_7G&cnW}6ZGAe0aYVDpF}=bq_PY7JxTXYZqcwV!87u9 zCFxk2zO|t5dp?&$WpQ+uRUO)ahyf2Th|5AQ>ynDF+ zr`P87Z~p#O_-(j5u@etJKm7DV{^rO34dH$I{=PN6`R-k~`@Y=AA2L0^eHHHR|AOJ- zB;V1;lUVxE_LhXD$CEngy)Snub73F(=z4n$-w2_7NxFJKekR_@TW2 z{!jmLawk9fIC~dz7MS@jCvHyMh9ATG?>>-`C(iNw z_JGN)?Iif>Q+qmbf8q`z{I`9=+qbVyZ(i4jpI-k|>iw$_c(*+K9NstM;MMW_r}Fsm zhYzpbKRkX&5BK@*10t~LdN+@!B?b}*G3{3$@JCp^dK@EG!(mYWE$uWGAE&M^A0H0= zgS2zYw|H2*gf4xO{3Ps2XsjDv!2pfrO9}6V1Dq)3@BluNV}z%kKmGKvz*F!}{UQ8M z>lF}u|MAEEnPdo(apD?}kn!;zk;}bza9sf-0C7RAu=$5@_xSrC-+%b)w6Km? z_-FM@+k=+)`&U2TeYh`=kFU!wcd+U{l~>p1)4IRu0R86U{l~|WTNB~*x8$H*A6j}> zm$K`fL^r`7f85Lc_+#&)knQ@Ysdv6lyRP?X7<2baz5C_$fBo}6{`YP~8xr1!gM8H- z-FDjsFQa>?>6R>xXp34cdz!jaGcv-?>EVtyr?>X|zwYMT@wMq^hHqohpWdH|Z*aZs zf-&`mG9Jb{ZwAvZ9-`&%o-)+a-jqTHR+wYbMEBTjOFJOW%pun*ATkThDlx^rm zc=83GS6#JOG|Rb!WxfIPRcT@qt5p=vmMT_Dy(UdASQWRSEVfX-V8nKrGrEy){(U;Z z==kg{;;coUwWwPyhyA3(Uhd&s^&hSRrGsJHuyIZ6n82YZt zQ+s(FW*;uY`k{3^418Z+=iR4L&EXOR9!Tng2oEwmsPLc9D)FYFO0<4W!>R3`>x0Fd+Y67t|iE9W4*G4YxDWZ;FR|R2#1#-icx;qsB#-Ta`(Hagru-5wOX}$eug`C3wW$Yip|h_;MCk=^EnB9 zHT>!+@xTWjIGH1_nL`76m@(!I6ldFYXnml9?SZQ+jw7KxxLhqkyOC4Rpw)b+=acn@ zO^OC~U79ADa228Cw7!urY7Np$ML}!dRE(qS7iwk#LQP#$m1qYO5OW!7-`#ycB~I?3 z@e3o+?4-;|sgnZDb0?|3MH32fw&3{SG(T#qW0Qcf0bt6&pJ&TRaPilV_)r9!%^ld3j|9XVAwK{=(gi zoxC}DqSA~)#+jKwfRD2^7{4+HGZ%Xx0`okr;pF_c__VRl8|qcm>j4w57IVFr&23Qi z1bzI36@qncF4zhR>wbB1lKSNe44i@h0=a|3)Jz{}h2T(aF4wC?5bwlK-qmtGsqM}K zjnln{sPkkHHM=g0;J(-);aK6$>=@1Tq0MDuE?e0lS`dUe%}iHJEK_ulE!%r$fxTnP zGW{Txf@rv43(Fi0)38aLUyGvw#4_dX24pGG1m9PObBjD{QMXzS`$>nr+`|Rc%Sy$# zCsBINj!I8mV|8M>CsBHCLCVtWZK32z`jfQNRS80)2owr~MK~ZyD&F=3O_kHNh#2=R zbj>0}&vgS=tqT(V0f{B8?pB28iG^S!_$IN4aj`OY$+1IdB~vu$7DueELK?9RvN!Lp zLc}nBGBym$sP!Mh(1VA>7ZXP7b;SdZlCFQ|<3`B!KvkI^s)O)|$_F)O_liRyUp2dPXQ6Onie! z4}cQ-2$i}aOVM$p08b=n9BRsTJlYOrLNI#9(M8zpLAM>bE%3HOx52!h+j51zaW&ZD zZ##H92SWK8~o#hXE!(tqDt?%mQk=@?O)N?}y zUKN=y+2nA)9!MRVC`vxysp$4piUqHuVH!5X(T7=F8$fu~YrO96<51G{`?$}#zIyW= zze)Ph|5+DU8{|s4-!yZJJZn+6S`Pb3hrQgx1=Tkf-YssIT%WqLnJzx`;r7J{O14`* z+NgYa04|%9$n-fio;dWUSr%U?a_94d5niCu6OkWO`W8dFaLsx(Wc+5# z9Pw--#e>~W#Prq;!gMjvxhQSFOTpu7I(j{RE4qIpfam=E7TugV_{}i#HLt#L$-y^d zy>F9?FAc^E#OaOKg_d`hCT`!C-QCZ_cdyK*sP&hA5+$2jUi!_sMZMh*#QAAf1AoTj zHr>lnIkKgQWK-9a;wgu%7Sq+AEoW|?=d{9;%`J`VD2gQMSkZDztW@`t-_nuZXe;>Q&*gtR14_od~Xlqe4mPh*^*u)&;i*#k19bbst8(%&<@Skx7k&F5onzG>;;2C zV~sl*b25skyJ4N261RoH*b<$c4ugrD&ITK^7;MzW;EDaW&uq4ECbZJ-39SdUwkJol z?&M$=kx;5uoSz-%{A`D_D?6NC>~L~phvSPKmTD$z$t4zHv3BJ+i%Rv(akgIsyuIL4 zuO^>vI5`*`llY6}_>;FMuZdbW!pijQPkf#ig7K@BVCJ$Ezr}!GVZiH4F5Pm~Rr^eC z=$43z!&&URxxDEMTM9lsRa|?@K1XU8*1CV&T17PhHdU{KPZ# z+|skiD(%QQ;ZSa%#6Y>FB_b9Mre_zzobSn{L(ccq(h%o+YMH|2dunNj^Miae#8JsT z`IcynVk^*uRw3)qJ9a#ww;jx+eCShiA zM$0sCk|;M4X#`=)T!oax_M~k}|P(>Qal8cQZD+ zcb6?;+Kw>8>Dvv_+d!Pha>h!+qLBLck3%JWUZ}Iu*G(Cl#`JhjL9pwA_AIi~)uW-r zqE}asqhT60iSui5GyvkJuZ{5w8%CeqJ?gW&M}2nFc&X*EpLE#EJzP+|EOolrG0S(f z%zXXxZo1+bAU1Yx=}25aOz`C$zEtjM+0ofBEyBTefFkT|Djy)G2ZAPrzI|SQvu_EgdbvqVkNqouqkV_C-gdB)?xA+kIF#Mc)6vuvU|~~Tpyg&L^=zFy zt`6HgIA^&#oLi=W@0QbUC6Pu@3bt2Mus*vz)MvMc`s}XoQp+Au``bgkzdh93+e1Cz zW0zCi>Zxm5-gJ9t=LJ*N+nnlFQU;{VC_A)z-lTM?UHkGT?}?HkYkQLHfwdi+gh}n_ z+j~=<)B}c7z-@AeROAa%u8^6&o4IARu1xy^V>+{?!E12w6EQ;ept8%4W8Vw3hgK?%<=+#X?nLfg=X-!W7OoTE8XWNeyU?* z;+r{Qf0Y@=rN^t=+#%E4|p8-UJjJWt#8^?xXR8$+-mL{JPyc{lHq_sBP?6X z@a?&aAlk9$AEWt3uARP3-aEy%bGI?3VsASLh$_VTzHi@afAz|z?3~m#O2?uNSvXsn zN~RjggjDXeJ({CFs-rxLBR{fNMM@E!j7b`yd^N(bV5L^2X3G<2uem;QwV9Hm^`;0V zvI~Vr7c_UlIK!$7TzmDJ^CM?Re{|bvoGA~kkzGvS2c{O8YGScEuPXj&(A2d6s2i(CwAXGV;oTF$v35D!vxt zDELvZBlnjjSeJ{)Raxmkq=XYf>0}B#AQiVd&dW9Ystg~k^pW}Er7p!fYgG)|d1qDP zrI=ZU6i3OAk{yLV3U?ItD9lmlqfkd7uZqtV@fO*e7@6f!^O!kjym$jsd8}*knjiHf zUiqWKPkU65=ShiSN5ziPlV<5iv&08;l$s2YP$_Tuic5s0M3E!~ELG-nbjI40QnaqR z&oM-`)hhgvM`57{Ozm{d%AR+zS_=4O$6NsEH_+y-0VB2`&7HS>~$ zvN^}9Q!dRS^^z8;T0-%aN2QTUs`RWzZ(XRy37cGK7U`F?2w5a#Eo=~mYh)siycCs7 zDJYeszrN|ke$&Gu?Z`T9zsjP_LO^mAB}Iv2@YnK~k08V4bsV=izL*gjCRN+N%rWuaRzOYHmud4)vD1cH3s81ct zOClwmk}4?+6I|3g4bNH(M9-6zB2>mv0Z4}0&uf$gfmxYy3a_m^TKG#Jjk>ZLoJ9(L z_sPi+xi&U4T?CFLEuxf5IbqB#F-aB!eM$40lwyJlkD@mqcT4B9Ytgg(lVXtY6-reZ zP_eQivt!n)D54U9C#?jDG4_*UIHxmBX(dx|#%u0TiUwIU3ZxWO%K*lGQcPgjA<9Hl zRvHImG&&oE+GPTm)(uO>e^N|Ft!OQG@Ca)E%21>+MrDAgE(P8yQ~PNbSNPF!DUyge zSW{I(l9i=YnVhyYZ8peFNzvC_q^TjKXtEc;uuYkzguR~>W3Qb$IsnHUtv*_HOO#Jm z8y%wJ${A-tP2ieZ5j!Ti7HNi$wVx$VY9YXnw9m{qRFDGfg9DF9QbFa^BIm^C%fo4u zOJpv3;1m47Nt=8sF`>QyiEDte?(^jV31D(U%PK-aRUkr;1{(-FMI_LbCeMGqJnUO= zGgLbqMFr=^#~=bYBDSIet7=5geS!ZhQzZymA}b0kNEz*{ERnm)tYr;rj(@(q60D68 zlngnU6$?tJvnyIh#JUP@*P#1Mku^)nlqflYu9gbqfv6(l5rj{Lh*Fq=4>Lf}9-TQl z{aI245(atAB@`mgq1^U#1|(K>1yyP!)OpIK&V89=3lo!7fHsU1lIOsjN+H^+4APXJ zA!(%4+!fPd)&|zLnR=#?~nuF7b(Dt@hPp%ed5-O`$tByW{CWOdPhhwpo zYvx;h;`NiO4K{M4asFqg!TpU*v9WJDevQ;>gJfh#w^!>eX`V}-FW;sawY??f8AXgs zuAq9X#YLP-wQeE(4EmEv05<4q2D)XHESGG&(=1{2Ir9y+pFw{ysB{>2)`lSH?W%LY%BkH6iJZ)`( z8cryoz1+b5IpQBILd`R?l*BdsAcanxp>p+BhJk-hTdSRxzvi?+MGcx(aZpOI+w2+m z8dr+T>LUu174=}^*XppUC?pG2Q534AjA9{$Ac*V$VQU`Nbv$hr!TGIGM>>%sinN5R zEvt!~*iQRaHd_s;-jT~Lf#FRcPM2r$I@ z%4&?*R~D6hx#)%ex8vFE5FT`^MweCKpr1+7+Zu-5%7RPL5t%VZPH&SKrZdcE<_k*} z31%cvkRgp_a81XwD1ojRYKZuERqOg+uLZ|sMkO7yq5nlq5nh1wYn&9kdR<(*4Ch>Z ztr~8lD~5h(FLF*&<8T((O(JouvS-V$Uk&QJSbVNIYh+F?kR%;SX=4RSfsn^)_*Xj( zi71uKtzZ&l%vE6vZ~(%N!Y47=)rhZElOpF4MQgGqNN{oH7+9`ijOpYNwXQ~ftr`KQ zi_@|?DTSBLpi*JXp=6Puz16ujuly=SAb%=YoiswAEP2bTQl(-xVbjosIW{QA4&`*m zMj}YYuhnLY01-77gu{3N;>?A&DuU$G%U-*@gyeLo_aqu67FQwz(?FP#Q<`2C11t=? z*7&|-DfK*^N(WlQDr&r<=o)|rEhSF{rKW%hz0&1^Kcz|>$0+2bNFMxDOR9lXaD^ii zD|#2wRf?xn8A`F*6p!OrCzg_oRVcdCls4wv-?Z>i%srJ#l+O-M3@Xr7rF7oYe}9Mq zfLED1D~E@lRAm+x(JP6^z=}->B^U#EB4~sKgW2rEr&1b2Njg^sURnxxsh7qu6)7Vy z6h8e%MVP+{t=!d$oyiJHcTr09L6lfjDHP*ckWVGFNKBRFX=oMxiS`VODuo=uNjdU2 zk3wPBc>Ix|YU^Bta^=aj8*L;2%t2A4WFCKTsIZu-)}d6}k1J`PO}%s8T7HVB_l&BRC~aD-CT5niM7|Xjkm%txz>2r%k|? zw?;T*9Y$a5lGz3sZCSp&z?FPnO9YA$p_K$@(t)As*EvB^0bQ}qrG7P{+)J3kLQzVf zHjf&WppzNJLtqRgp$R7DUPvhQ5~f6+qSe7Gr-jAlblG#I;UU8)VfP%N^oy7hoiP9^ zkIaf3B$9>z+oLxf2DbDaqs&W~qI3`$SoOp>Do$!|IBLpTtHhq}UnfB!{}QGYY3Uo0 zS`l2~9nGo=8V9Pz!KP%~z7d3X5;01NNl5_>F zp+&owv#3T#ml`(3>}AM0TbWgRlj>2DMOZ{%WijmKEXtzFoSd&H#T1i7ROxzz-jjGO m1L`shZ3dbQrW=}%2tptyi3V2E*MMKj+W!M<6OIs0TmS%nq|iwK