From a58b207280f8a1b795b34079d5dfb00889ff0969 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Sat, 21 Dec 2013 18:24:56 +0100 Subject: [PATCH] By default, do not perform abduction for postconditions on the first iteration. Correspondingly, remove atoms containing recursive-call postcondition parameters from the conclusion. --- doc/invargent-manual.pdf | Bin 126055 -> 126405 bytes doc/invargent-manual.tm | 7 +++++ doc/invargent.pdf | Bin 296316 -> 296451 bytes doc/invargent.tm | 27 ++++++++++------ src/InvarGenT.ml | 2 ++ src/Invariants.ml | 65 +++++++++++++++++++++++++++------------ src/Invariants.mli | 2 +- src/InvariantsTest.ml | 1 - 8 files changed, 74 insertions(+), 30 deletions(-) diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index e0aac25793d00294035474792859df40ea9694a6..e2b309b9f1fa527c1f0856a6af2f3775cfceeebb 100644 GIT binary patch delta 16922 zcmaiabzD?$^ETaxG)Q;DF3T2OA|W8s-5}j1u}DalbR*Io(y4%Sw{%J)prpXd_xaWH z;2-b#YxnxhecvuSd@K#2UZORflXW<`h8yeNo}_&Uln zqh@t0)F7#9v@^QA(Lr%3ukyZ{n%&>nxkANvD845N&)Y_q5Tc_*iMHQ0Bj5UY5n{xp z1aBMO^!oUEoe23LBT9tBEUYM4YBdZE{y2N7OrE`&;pO9N_qtUT&~-l_kE!J2Tc1ZH ziN1#g-0>T-pY;qb3`V?>`7{YgXOS$LKTP|!#B22JxIM-~B>^q$iY;?#`C%t-_xuXW z`_!eoNy8hL}$<^m^-FZ_MZ+;a0VRrd2oQ{4ZLh_CzkHI}$0N=5*q$t@P7>kmHXEzug)+HWf z+gmez)@~)X-l7uwf#!PK)q@C;`r34=Ps)&UKO|Q_m%Ffn!Nnnr>F7EmkzM;%cUXt~ zbBCA8LXSgU?0ocnZ4`)UV9^v(#=klfsNvFTzNzx`wgdz=_i!{-v@y0Vz) zHty$x5CIur8seo#*{`gCrP{EPde-sS0Q;RX8ys`ZS;#n!K>|YCI@Xcs#Q}YSBE}ic z-dy|M_!5CmET9mR+ukS{pATN063tc$j?btm@+C%+9IUBXP@eysl8PkbQDi$T9UgOd ze+TbniJ}%9j%F>>V|#)4B-_>hruCgZ_yZhs}5vk9j<+wV1o<->V6 z0pTbPQt28tC&uG796Z2JL+i6Kq7fK8u-{5@K;st!+5)U3btm?iZ#o~~oWK!tt z)gWI;vX2ispxsjsuAM_#uZ-;UkUm$~Zx z`fO)ZlM#ZSAlMS7C)4sC#Q0$$_X|sxscJTZ2Y-3S&Bv^C($UT?*JlKAMVSU*v-ow* zYwEnX@w`n5$LmGTTQoLdse?B<2haNWxA)mS^2(&U(asU}2tRc>;ihUM{Y=wCPiIS{ zSK&XOr_``B`k!8CaFek#fgE4US|u%ZUBm@e6o%Hy_U(#GDWi{2o|(h~N7;?vbr&+Z zzr6fHr`)~4wni^R?-%K@zY>Ci0mGSaYd*Z7XdtLxNu2g0{AugJ57h)Jo#WM}Gd%n3 zr#^Et8T#`o8j=4IViy5t^D=LZ3gpM|+Kkv(_gz_~PTj{Mack&drVf#NdR=iG!;ig< z{v<$8!PIE&cUDl(l8Mn2<~zM{KSO^d;i`7RPr_n5?&`LJE6nC14sP$J^pOjzx&3zr z8gHqXI=veBN4Y>F`caL~}kRL>WqM!YqK~8mbtumHjkJN{V0Cm&`cQ^=(M`D)7nXcz0^zgWO9wW!CuHA z=glER(XK_2p>@c$gL9T8?kGqhP+g+N{4)~Twj=1Z6;_!Dui`0ENbUZL6%j|j{?smk zOF8*lLd5ExQ!JqUwrKXPZ-@%l)ZDNRSl3Z(OGi8H?MD>69+Qhwlzfc|Qr=cOusgYv zLnCEkGrq%M$=4TgfvMZ=Y+;Ewo|x zt@fH*K0U1UimJ2ocr06%0j{Rt7ImcR^eg#M1i4hOB!>jm9p*G4BbDw$qLDJs0;@+p z#CKYfBFM2djCy|ODNq(v2=yCTo5eiIQ5$fzt$5m~qRZo+1}k7L`(&1@SM^8G)v`*5 zP`QC=5+ID}UeLtm%u`FQu_t3Q+r!HAgz7*&n!y1n1(jTqb8Q*oQAJGAn*@#$QTzp4rTkg=3{0b>=PrEj2UyHtg~>OgV0A=1c^+^7-axL#`6sCMP2@nJ8a zY4<-qCMpKKB*Lw%QVF>p9^vR?{nX~!-uv`8pbhi5!d~pi_I8!@ZaIBp>Gv**rQfu# zG=dxf4{=qD&t1nWuDwqj^RUFq6wMr)^i54xRJA%D;~3cRVOw6NKmzt6_|C&~XK6vd zY~s6|4?!kv!n6m<9gQpKS7nKY;C(QSmEfHB%us|Ictv9J%7EGLb);pB&^Vp^_e{g* z&K9Q)y_gkupIo%Mu-P7&#gZD*OnT6 zSLij9O4w9ETF7gMwSBCWKI&s}5zpxXgAF=xw;JaM+WQyZ(&qcC|A@14i#aJHFC$c5 z+Se=IP#I7Fg!{7m03Z~$>d)ofsr(mBZw7M<7+KWkaz2^fjM2C~45aMz@54z^@9BH| zNYVbx)6&|5$wST;F(bdZSkl@EgcBTE2u%9ug298%2Es&H@7wT5)k95e7vjellSbbC z6sO4w@_UZ{9O}h>X_J%Owv9eytrfvq@3XE0uAZqbrB575>2S1whQyJKA8dPup`iV3Pl+FW##PbkQX z4#(EL(gJXpw_OxeS-!8EDn)T|e6xotfID_604np&*c~_aHjhR zs3*}@wPi0}7m0^0F>wlJH-sS0sU?h*bD$}oMOkP?Bus=doZgUe1FoBb8}kYIHBh3Fp=|a_S?Rf_eW)=XowH3@`olHWTGcn z3-!N@hazhtxIe>5O4|-7n|)C67{AF$5;fvsMQ+ZuZ``F?AsnJHv0UfbYPRoR${mTY zP;ELrjKve=_48rN8vZXi_sgBFtq$mlfzcpi;w+@up7X}Kq zzq!T9s*=vLV>-(^b!_o}(%PWwGQLGS>)Rbtxr-59izp5V+D<3&BH^GoB~GGYHC<4s z@(T}g?qG z%YTx2N#gZ8!_cU7Gy!t2B>QA?DLn#VL5vDHie#sP;;ZPoq zStg?mk3r(d?o5mPcBvM4i;RlRl_N^@!!)=_S%=he5l>*JTG}ziqDjV*jn_DSqALaqMsVYVzLG zDPGxi;ehtm7sw{Gr&~%Q?Xpd$_sMa8h1s;+gn$eqMX!EE@8<5nX$g@}?x>StKblK_ z9$O&vV`K}oce2NrMp~f4ZA+D_PqveU*ct0e^J-Pi?t81nz*WImve-Y!1(o?bv`KL0 zT2NjFAG1iNT$GM>|2ZEAG@OJ~7{{`z;3RfWmo|9vTEG`5JKhHCEY*s;v-`chUPN@X zwO*3nT^J@yWT7M@(;}0`D>&kzK)|)yj>X7`9z9)`jc?9=DOSa*G~n{|{$8A>usST_BgfDvsZzwlXN{0e* zz9z>Vo0zTp@yhL!4u3kk#8UOR5+5++;rrQbOIB9twCBa$k}~36z5M9O=}yP}-JL$7 z{%uZ7v3H=~S3|8oJs~m2E5)R3`p;?y>gq~kgx(%+kjeaMF#HJ(bGp}{b6DxP$(|hg0UtHUp+djxy#=c=JfKU^%lVSL zoWo_XFK9-!R-fKpRe#Z?Mwk9oqQ2;ma&fhOt+@7#&O2avqB{BS+r}1q0^H9c!-fhA z5x;W%MJK|3s7qol`z#TB5;_K_7@2@Ry}~T)ZS$^tC8v>aG=2zZb|?rdz$Cap9B%u4 zQ7PCm-?-dr)CIh);2S_zCV-d{r3=BQMgY#4o3_|)volAT+{$k{vi;^D4Zo|?$*7|z z$Qu^VaWOQvYYq|3D0Mmu{E8(XhVFl$`!77W1*Ik)kwu_vn7t>sKzXQpJ@XUV^RK&R{N0j8)|IFvp zEX70Xjx3;Ec-v3p=A~UY_p{QY3xy~yKlxUe1AEOSHKFWfTzKkd`Pbjh(_dWV{F;zt zvAPlJy(!5f%Kj0W1H|sAlh*v)6d6so2h^_Mnx~siOs@S%{d7~;cISM~ZPx9$@hk#L z+!B90aDN|;i#afuC2!QAor7pSuYtw|Y7_D3yT5nq=sZ`8Gt~2&ZDo{`BcuMz)4q0) zMDfdGzjd~jVYs0OD?Ovd6065XZgJk7PmE1Rj%War_`mzYxv4rR(dN5++V#M2ih<(J)q5wf z!594FThEXa<@;_Uw8oyg$%lKTq_x$a@t>)vk&suM2_%Nr$f_d38=XCq+3pf8jfE;| zn*6@0=2GH*5XRfE4ATsr3guzfu83Ggwtb`0=dkF89kjg)3<0cKhx{ zFDEDlm3pmGv6%Q0_N2Gv<|s}Ty)}Or5It-x_Dk3DOG)glkYI2v?ulqatBZ!bjT1!8 zlh8-r?VC@OhTbRwq&+-q;j$S;S$g~JypA{?TlOvggyX(UO+Wn8a!l8f*75SdQ-^(b ziF!PbpY<|D$SJ{@Ew$qXBvmcN&}?KrXw|&59iME3ZNex zit5ALhD7EOQeJh@;5D^;OQWtv;=FIJua0I{mw%z-RQ`Exq?Q}4Fe1$N8#>xr+b%Mue3#+DSj`RBUe=IwfAMCW3E*(m6#C?Nhv|E`m^5sUM8=>Z(oErc5lRp+h=M7lEX+xu5h2I1?fJFi`lDg*_g(;<5DHbbPIAY9f}w0=;wVzR-q#S% z8xotZwk&bW`nRcV(f9yqW3{cW)`e%(zx#AJ!Wuq#Td zE8D#$C-l5qR*riovJ#cC*@<}XseS+>ZO04d=ZII0bWez%DbhRA@1x7US?1&*ivNTE`>#oSBS?RZ1W|qiPFUsO{qZ&SuIh`{#4f;$R@%$G?Z1Mzmc=C0UljN3PNQm()K#mMk zoXF#-P`>Be!rkC>3A;$BDo4eVpdi_-3Z7eg0Lrtfmf`NR*<;p=2tcwi#kSQI->9_tF4emoKG12Q@N2|% z)ZJD%XP!xG`p0)JebDlhwBJ@_C>`XuUkc)$9yGP53M8*>)Vy}TF1eO7h`fQGf))^0 zZ%YRgd6=>IXur41K3#D`oRtNg_#5eINDj1`=UY~RRU2x4W%4*Ve?>BKygvBZ+2dl= z|ABtfTDaiGr!6Oc3_0E@l9YjnqWY>$8fi@*~f%rZeQmY^*h@*a7=j=<5LA{+V;7+NhVd3E72DS0ajdm z!i9HQZ>PvQr=Q?``kZIu?VnP%BrJua_3D`{88OaJg-_B=Diw_%>3I_aSt=@-oM+@6 zxrtuTp7clv)s{4yiY18_f3*Q|bvL`_5HNNX_aJ}5`c+6@)BVMULr%hJ24hFQ#}~=8 z&4!u=&KAMb`0&16TdUSAfll^x2J!Y3=d{sf5$|g)J4Xm9xcFT7xjVPkl?>Sh5*k}@ zezjeF<2g5uCZc@{Udxs*vZa6N>y25+-|x(VPRZJyYn`c?gYVGzRCzZNzs+&CzjxzO{+C2MlEt>c}qQyp#&YB`Kq+4|qz%34(E#XucUM$uY4q^_sVoa&+y%FZUiqZG%_B>nU+!|D%>13b-4 za>!TiY*iMEBCC}-HCOe}H4)8k&r*GJwVqz_0mQIF^p?xFOI)#JJ?N9%SL(V^0D`z) z5_*+C^5%3`zneO~;$0CrSG}E9q?UH!2SNzr|8UZQR4uTn**eY^PMUsxPI8ziUXOHK zq-xOM((!AglL>Wp@8oEA2<5+eYHn5BI@&dU5G8#RkQM~eVJMLS%cHwW9<2w_GynK z*H0#(k)ah&*Of{t5?#g)DjC6MY5OWp!t-oZ?4C@K+OdMuVHE4Neod?E;XusQTl^dE ziWkZ1Sn&5OyTJ`YmmP>N?mkRwf(@x4B`c%#14;Y*K9oorQhI8F>nLiuTMnV&@^kFg z;INRI(6K{j$l7m;UTE5d1-|gySz>lXeeK@-n+5-yMCp?QwXzR`Oyf;})aXS9>9*Qa z!uF3+=AqZg5hO7s%g4QIHZ7=GOZ}$Vdx!9PjMKGUq+V<*e{00g9a%`ghJE`0BkWa+ z*tg{6b^Z95kZDb#_mCl3n2Mll%%uMT38P)Xy`IqNC7s~=JT6{*?Av#}g~6c$1PQt4 zn+KKl(uS6jtLw0@APUj}GU+cy$bKE*alWnefW0Go3Wi^9B7SqtKWc}y-*`|r^Qrwr zx80g*lpXkH~}C z!S2goc1T)Xz_^Y*U6y;o}4wqdGG` zhQDMywQ4fUsIIDyLdCC_#46uz3NES-4`8M0h7coum>IA}*KoL2O3GV)cuN-rU575ZYp z4Z|rIZ$lutx)3For)q}+gq6vq4vy86*1f42D6$$2Wh1cXC50@{V zAtNd9is<3WN{JN+WM;S>NR+&iLj@HP@O2U0>iko)g5-RANx(!NC!g4o`iFd_i*i>!1T@ zL#7R%mA@~4?hlsWQ>8YOn%tyQxP88A7C5{>1=s)NXj6P8$)wv(q*(w#`ub%DO4S-V z#xDJ&3bssohC|BBDJ$~talTHSEp&U{bEg}W&!duJ%I)!w#|m5~*0+h@v$%b#b>1uR zE-OI*qx&@3YoK}-xuhoh?6YfVOqrXmebv9Y8E4{Kl74Eaf0W!J-P~f?TBjoKycfvU z)~iTzUc!yh;ZD=_kodsh`x2U$fmV0HDqea1!h}*HSRw_IZAkqLYw}%T_@AOW{L1=T zGPL|I?$R8+*(u$RjVc~g7B<~^>#uF!9L1p^44;96ZuV@!rN_q8YOS408iF0}GvmQ) zL&}^zRh&rU@437AJ|EE{y>>2c6?tu4^ud{MDRZJ7h>m>51wBCf;CXf#`SnH+@aAHo zbY8}iT;0j~2`=C8F%`xwgE;p@X+ShHi|Qzk<1>tUuJLEHahnx|`YN@A7dc(s z5pRdfZ&^`)2rbM~4C^U>lzM|)MRHz#xBY6$z-nR)6&^A9lhbPPEZd5d&L#&f^$GC4 z%U3FfpKkcQ#=*q;6SWLxVN4$rVM@L2TcF zh3H!~%HA|@?mr@q3fAC8ENV1`S5na*E{z1pzD68(;YNlnoJ~6R26lIbBY0DsWCbHE z4DMNnr5kqjtvQ-;-SwP{*AGvpTnTHWI>U|Ltr4N2=xv9e&;3!y;{82l+wJ1{f4w5J4#Gu+34m)o zgG!MRS_%#eGEdua#}Gz=v?f!F2kB<^isR4ZqH^ufHeZo{mC>7*zI42-T1TwRV{*vz zV@U;}s+~(bbM|m=Prb6R=-?%%Abe(YHj9`i8SK&YL^AYZlzVE-7^uTXo}Cmi(J%LE zg_qo+LiEFG{qA#wArCp@TvPU3`&xS{=Ay7CqCtmOc6B+L5|?>PSc~+iO&v$*?mWaR zAmtXV^w9Z4`KO?oxprO2@W6sw#livOQwkNrR$jgUMBsGDNotmN0+s-Q;BK*!>)j0h z{PB>I$DRKEO$7aB3gZAQqBFW|QNs-xLnGh!gFlxzp5$f!2P~&AWo883SG`OLVRDVg zh;_;qkf4=F8Zvis{ErcfAk>d$r*r0sdl=EQI7)FB-wU}%%UiH==dOO#LQrG~*R-BV zm{tX8!kjzQXEnZ!8zZJ-zp`OryMLFMmf5=cbRuNiMbuH|vnVm;LgMv&p#2?C{y@du zHkaz3KT_|sL#EUGRQA0g*dnI=;R`pUu_`2vZjP_2NY7`#NESucpk^e06}RA#y|klMyS+%O5k`@}UN?L_asHd00|53u5n?-Gz^?(&UZL z-09RA;!nhh(Yfom;2*NsOAfEt6xXeeKQd+`2X4j#7WZDy*1KxIMdObY5z$dXfg$|s zOl-~rD_*qrZZRC2FTBv5^%rAGxD1$GhRZ~$B*;cMm8bJ&Ya%l#84^``5>-+Sc^*X) zp=LU$Cqa`n`Y;y~@d@EmA9NaiZ^RANuv$`Fb-w1Ul4&`pIk$fgmS&FEvTJePxK65V zVoQqm$M<3->V6}96lm*(h3*XVjOh=#giOvkohpiUTEBS9xoeVpZ-bvO`D%ZLv099dL=Ea?-?+$ zOWjAAjb=e>8oGOWL}9AL)QuHiK*;C|(OamWLYgO*`w@%2{IjlX{5$lc?=<3dEQLq& zQ9iBHts?0~)A<7SIyEZ3Rrzgnweojw^-{@(=K7L1i<*jk?bbhvvW?$2l4m#86rW<2 z(yD#xdm*lKb=H`xs%F3=lhT5ERB|1mPjcMLenFIANUohfQ>?U-74s9$B}sG^7JEGo zprVO<;ZSobG5vJNJxBKKH-aU^!5am>=jYQ^2jO+s8SY6bv%dkn3**(CJgKbM;Xa>+ z3BWWw4k26GA4@Ch(wM(4kCT|%N}JIULZRODy(9-r`Chfd>I-Sxoer&c--|!nkCn?W z6ef!nEpier5Bp(ujLi|7lH3?uy{FrNVa4ZN;E4T}|6{VKW1xd;%IwpC$Qz4W6}0(o zTC}FDPm4X>uf!IR9x;e2JeVE-BCdhvTXh#VCf$#6q*2iL{ zQFkAB$5(1L>$TNgeZx3!`cBRqtH4Z+Z3i06HC4?@1kO)#oQX`ulrGo0-oGXd=9~oT zwv|9i`k^SEdS%Gl{EAMToQ76BoQpmFtq}Yg$&{tkRUaZ_s=TRCVB#>yHQ`3-pD_J>| zAI=ToYp<89-U-i4R2*8jDRaD?>yrBIu$bZHm&uAvQxPal&+=iL`1jqF7IJ8JdN0BjF{5%bSbtF7IW z__K>Uw>rH)=J)rgXzXn?^#5whPXr+J0D1=#YkVA_06-v+FrtAl0-53&W35}}!UT8p z;j#@$mn-tONEi($KFDm4voFb?MY>@|%Y@u59vWtPO`+1Y^WO8O($~!qn8L zxl4s5qCr58afQsHjT_u%UL=MBQ_i#DuP6Pl6P>Ks^K@B$HoP)lT|gX6wF) z&g-(LRTDJGBLq$q7+Eol(|dI8U%(*_Se{PyA)W~HyV1<<5!w^~#u8dW6rcAm3`s=4 zrLR)9ZFJA$e!k;T^x&bF(+~AsvTl8@<%J}cyY+!DpGf}t&ppt0_2is>w;wFA#($-E z|LvvHY4JMq&?RwfK>tU9p96)Hs)4)fh*h+_Ubs<9+tZyqJ7F|>6hAEdm`~oYyg4u2 zV-CIc0+Ia#sFzmraYh4X^Vph$PLf~NJ^0H_u82~0I#u4=QRuFl|96^kA=QryUD|J9 z>Dk2ZDD=RFPI)}0^(uKpl`bguL_d+=wcd;PU7%80R7>%6e(KEJoN)ca)EID-g?L-2 z@miiQNug5I`xsp>sFd!OjNtbReN@rx!RPA93eU%|i$(zV`qZzhTYeSg7<95|kr5;D z7}Qc`$CpSbly<*XdTNDSN*Awn_xk{q(yy`PmGUq1p``lr`iko4gO?h8uRpl+6rBr- z_+EV)8KFA9YY#0x0kYwpKf%{KeSLu7`tdu;{~)V+Xj7Iy<0I4j8;Br{pZ8JW8U@{& z=~D?P{&6O!2;1SV^S5^~H-RcyX$A%vEf{YY4{EAVMKtisbwt|UNrkHupeXQ{H76Si z8U;(3DL4{`g;hJo;=F%Ri81-b>{r*A8awd-8rvt_cjKw(#&_F?4#>WHVjD%12>BX& z8sGkd!_l)W1D~^v`=8doF~n(>J>T-fk{Ts?Eyy)iiGK~o4Hg;-dVL#{Z|W!+-I2hx zjfk%U|AzQu-gXUJz9>2w{m@W>nnqi#O?|6qk9%0}_%;T=_<*CDl_<6&m&-&f>p1NwRk_G9D@r0B8s=Mh0UbuEz~&EZeor zOypNL%ETaFdq26qqY&T0VLTkq;r~dh_dfipRx(8j(@nATnvEUVuJL>|)-__n>{Qa3 zhAdpCJ!d1pN!k0DJC7kS#z2LUonG$D`3OEVSxm}KI;&n6O29|!>oP#8uE=4f9)$Pu z`-Pb~#Kyr~XPp0e>#f8J!k$Ayj_b>lgCe0EQ1XEJmZ<`5lF{1mdTu?=v)dn;!0-@C zU!}r*f+NYExe|)>Z0vXeKLOvu_KM-Cwmue@T6>mK`J6G(VAG%GdM&L^!^ohs-~2n% z5XL?^mh^f4m>AV|jGwQk=+j$4Anp^Wz;Hk>irzga<1GO$G6S>yHVoI7X< z&hBu$$_i|3~eONw?D z%ie7H;3(Pbp6h=1x=!Gqx5PA8#@+$6r{5$-@$lZv{jd3=rP zsn$^=aKDwC#mpY~`p<7ZlJ=|f7Ob9JSe}d=J37w`D|Q-VHUIEeRPwPblHOx1GQ$VP zZ&Qv*dT>J4b=}d^M~^J_CFNmUJQt_;U zU3}N|y>z&~i@dN~GO_40}M?Q-P;1!;~K23-heGZwUZx()wh1plP zxJiqjLePKu-*i4zWaXINRHuiFLwuwmvCB1c)-1{5r5M1mOE#|O#G`HV`hVtgz4xt12#*t;}Rq^ z1{g5WoTI6zF*-VE(?0*APF=+?o?G+3W_`)Fg9s`qrlpQHrkEmvuczfKABU_-l*Q>O zC@3imYFWAL@O)e#PxQa2|6L~l*VWZe5!IW^5q8GfRJ=-Rha4MeB0AWf>z#DkCnf$6PDo4x@ON{%l)% zgI`bvrqp+>bV#Sa*7|U@y8PzU+wGlI2W+JZUTe=5f0-XNJbmVju^s9aotkOd&nw3i zxghhBHGSCZS#?xQOk|{~An{pt#^Q4i%szy|_(;Nh({+3?`|p^02j$y*(IFh8_g{H> zLd3L!JQ^3~4{x`5*LsEQk1K4e4pzj>n#K;_k0>oJ?7Gn%M&&Yd1u#SVUWPc&y~1wd zqV|>q{^4qnK1|VgD{V-ebP2KUB53-?Cj5!&ZNS;Q#QSb^ZRdoyL8~QK2fY$$)ni5a z*P391itXULY>bY^Iwfdz8N_m4`FO1 zD9J@9K|ZjbgG+x($^H&WUNWsJR{0WbEI0!BTfMB1R)NM#@jELo`uBzj{^Al5=p4+_ zcvQqMU&)5P2_W1ESba~AjZL>Q#ZXLhw7$7m3;VI09$|XtM-ja-VA~X4VRIHSxheXh zH8M=o5jdfY7UbD4Ml{I9u8Lgu0RCx^!J{h$vXK2WMx}@dew&d)2;8$nEZ0Il1z8RkA&Xgr zO&k!?F2++jHJ7B*BV3{T(}jE_7~ZO6MU!#*Ptku3b)km_*h*!-@)|DJ?C$yjvOdZG zIz8Qh78@?@;b%i(W6fAb;oQEy-xG(Bc`J-s`F%E?=19zwbCN zmwC=vVr(j~>bfaQj^ihYssA*1{@W-c?D=PEhIG46xAFSWcJ~0C3+!sDrEowjM8U<_ z)Wyb|%+^04;RWsSh@cpcU4?DgR}q}zTu8nn2Qv@L$$3lkyRc&83)uyPE!@%fhQA%H zIFJAedVT70v_JK_Wr}EQ5#=zpP+BHyQSg?OkbNMGBxF$a@|nj*X9%@n4vmTon{YEZD|C;FpDp2l1S>;jsl;#fqNH@=Z4&c4tDYm%Fhel`@zaY z9cW1Fr1}KL#N_1BJ+>+m%6B!D)5;>DNem9Kx(X@BL~`Io$( z00qGR^P~gihc&GABQN436dj0ENPGz>1ZOzP!NlYP8%+R?>aVYevA38rl(rR0g0`#O@NZEO$?IL4y z+W^al7Ks6mxlq>dWqy2d3cyWcS6h5k;@PiPoB5VLeQT|}z7mc<5R>_El69>q8AH$$ zK^m8_fLY@Jq|TnJ;?qJs^l_^j8>f;pT>p2m<#iCu07p0@78f)k-;JdqY5M1D)=1MZ zX&=f;EJ+kLTiuCv> zhLEvtvMBswkG&1~tG-Nxt{i0nc zbt@gU9*$zIxnScW$C?SUukHgDa7DCJ4I8CJWox&inCYuisU9;Egt9gJYZ&+JPc*_A;f*nTy-tHfeT3G$HqZ{<-X0(4UmpZu0DizD3=9UsVUI8<2m%B> z!oWZP{PBJ;eu2O21O&jKhevS0(|!PgK7@X-M<7#RGZ z=zp&NaTo}IfT52L1p+}30RMm50U$sixFLNN83h>uf&6p&e{2Hhhr=IXKqwdr{Z9-4 zf&=*pX=;P15p008vyS^)q;0P>jr z2W|cpi2xV?d0Z0@W{}6U3VUxnUlehJ^1`MoiKhl1o2p{Fc1LtsF?y_56$#%3=Dg$8JNJ|Rr1iVL4Vo7 z0g(UR5AnYWhQWc*$1K3$VEEsQA2Rw#NU(>(c@*)(G~s_7@dE~b)L9Y#bPB-ZgC8*H z;~DsXK^~VU5C8%_7VtmgNZ=9G|I`=w5z`MCKLm#O&qy9X$m25k2ZR2#7zTLE!o%q0 z|JxZjl>aYg;IRL#62yN`ec->idF0Fk_P8%R*nt6$8WQlKnt+cZei(qTM`?PngFL=F zKs>B{X#bB7=6|>s_zMI5b1(bP^*@?)h%)cB2LqLDA0ERy3T2({byqU03I+X@UMfR z;J<_fgu-B;&>j`#L+JwHk0%ZAp~e1{8-9KP@V_aK<{x!D7z+HazW+zw z{QNLja_>H}u$dV^z!)N61~oQ?z>JN-rp6$CQxo$Cv4YHi0ww}5QF`J3zllCRj;JU; ej*F|Yv#Y1Gxy8fpNc{W{WrdH!!tz{M=Kldu7il8^ delta 16559 zcmajFWmH_?ryKIUuEq7 zgc%0Y{^U3fP>@k*0r~V~tiCI^f|tut5dgAALzejYbOj&6vLQMqBUB+vSUm z=|j@e-IU&qbRvG`dZT`ZUdk`U`ub{j{2t#A&flF}PL;<9$(DBOKzc@sQR42TeRHyk z97C~uFGP~i2!?EQzj`~i(mB%hYj1u(cn2GPU-|r@lI*LNr8Xxf&C89sAteF)w^JP; z0tWb7TS}Lv!vT+}XuImvZTN>6A;KSuXo$;`k@eMFKcJx(wPlBP68OP`7_$eqP}Fs< zj>@Gbk|O#~*u_ZVD`d%WVSZ70haX+_<5;D1F0Y!NBS~M3W;#?4hBle=lE?PI`{=^( z(+?0p>2n5h{yuQ})op`=2+6 zoz`ZK-R!%wdl!=ytXASWt)YiT=Da;9-=(*ZDdM2s(u+pm{mpAzyu z?G+D=+6LW2d+5W-d50nxO0`YJVP9lA`pnWg*i&5`g;>QVDrc>3stO-U;Q@(-gWC5Bgh_ot%3%Ky zUvFLQhc7oE$X{8QVj#WE?jM09j1XDrc(4US4T;thXLwl+fk4%I_Cny(@wam~ET(FV zzbz+85+D&EFITlkO18Z&A>-l;5Mb0bz?-k|gUI>EAzl!eRcagfseM4pTF?(UWx?j8 zF%Dyer_$2dn{Mjb!@Sb3grVTYA;5_#0`5m5+~~7+g25L)dXo)nj%p#IJS6Ad9oJcR zLh3tpKg}1~jG!;bn4Dc=-RUkcO-1PHMg7GwB4xdO7yD`)C_j4WtG2+sm@wxP$#(IX zijoc0+mVi9z>SSTY5(n5dqz07ec+N5umM07UOB&0 zWN2?`6N<7l$6#%NMpZQEVTD~&N3qOPp^b*1OglmeLj-nQbgW*l&>4Rby&;uv_wukBW^H%@S(jvt2)<0W^vm)vj*i3819H|=ZOw} z>RcZg-aDhvS`qp2YGFxF!pH4p(wVw$zllH{lE>$8x=X9o2%ocx$Ula`O)Pv`Jv4S z5#+S^0Ivyl)j^+QnSxJ1B$0lXAJFYJrR_c^Zk3#@bz${(JRhvD$pj<=WV znM@x0z_;IcpzJfP)YAhK?f3gcm(A3AH7CU;)mgN%D4ruJqLqb&o@Pyu;LefIV=EZr zwV`D5X|cqx%>Bhx+Z4vq9kQ9&#>rDOm88?JBU|Ty>&fC{u z_A>fcAwU3feX_E<7#{ErfE6+1Uh@0xRzmK^lnn3gl!zns*20&4e~Ox+3e64B+SN_7 z!pBSF=DqD}JjIa7yp$fL!&OUPTcZfqOv)CEt<2*{QiE6YG?5RqhC_Rs>ORzX5&Vww z@XLxY85&SoL|;b(!QF?HXf6<>;7KR-tts*WcE!4 z#NI|3d_zOHw|eoyHRaP=&jUoUjYd!;H)&Up3n<0BwKOF~rID#<;@x6JVpcYqVuZCP zu4Z?%BQ>8w5M!2}qVLQ1pF8X+fiA6(Z7&C?b-nHsXu}`=~e8PuTmu5P;fi!^!q$CNmokb!n5p;(E+yESjcah}m}onZYO zgyF=512-@?@3sp|XEnbP&zE`SL{SX5AtuR*>C5+#+36KPXTzL+(g&am)-;7Ups`wR zDbK@iAkV#CY|acqZn63@jsV3D;F8i0-yKhQP+-&m|q zt$P$W>yh-Mp6Kk(h}iQ@)fHsSThHae$<)R%KEky`Mj)S^{dL%YF+}4tm3b+NCXTBA zZn?Rtwt=P98LF#UvKUJ2iX|}&{w+|IyS6?u2*UcJg(uF>h`oFGLzfw{;Fc+xF*f8l zlOc<^60OIzY7t8NJ3vzAOlif6H-^c@I%s9o+g%xAPHJyEp6NT&z3c9oB`+t(O5=@J) zer>@PwX!m4)FNBq``J+Fj)dRu9ckLFB0uh zpDXqNBn!HJ=gM?(w1hZ1p>%ts?RTrfGOF~MofC}|8kSTSg~!d8oPZa)>y<*%rX3D+5w=C8QvuJ?2`_?K8G5?4OLQ^+&C zzq3bAJz$mlm@quwWNOypvV&-xLZ!^_IU5hz-WOEr9SaY1;DO;%VqzZ}hbi#>SdXzZ zg5{5AG(z{F&m04_$*1$JmCGBhBzjz$L?gAzv~)!I!_=;*`?W6>InX|eyrgghfRsb% z{Ap3di9*#otrz$bVl{2(U`?;nuSulDlDc0{DNv}BQFci09n5%KAsmLek`_|HD;lHB z2SoE$jhGpzR%z-T;3ztJ-X;Z)e|0byy2!v{fnz2n-l^d^X({r0-xj%lhe1UqLy0wk zm>2#0ht}>oPO+luFrHvPV+F$(Apg{RSexK?w1UXZEp>gHNgvCSD3}8-i`cxk*Z^DH z#Ja!U4N8oj&JVhYDip&+wAG#@d5zPrlLRiAgN3D*9AiKm3q{H_N1&64NNGKR6X~v$ zN?BZd^ThUwF{~&TxnoHOv87;1M`177yRgu)dVnJ}NVi*xVbbfPzr0$gK&=SZ(V5mB zkao1nx{-C-qazV>31%yPu{UnTa#z6e@gl!CVeweNAfZkhuES?u&vDOaHi7oeVhurs z_zaYn*2FJRo_eX%c&*2^b&1I`Sn$bKOJulcS;g4uCap;Kn`Y*S_QD&!wBHtIefh33 zM4}wW&vA;$`{RxWY0~L~zJ0vSh5tqv6-cb`6R!PMLiSarB^saK^VY~w)32X@({K0K zFsMX+vkLgdg~P1Sld5KWOx?+_gYL8ayeru>U{C$_?6&d2%hmfFe0!)zY6b?!+RqSR zaRI0S)V2l|m}npf7qHsit`HtJq%G~Z(T&quEcM_kUfdr5e9_`{+8r_=*rW?S?hK0ag~ zQ!VT0=>`XSzgDw|mMSHhA-h>VCl$M0kiX)H=7bT>xF!-k=y=syHK)ot)?TfwUmvdB zesk4KekIV#M=9X(d(?bQT(yT5wxYw9AoYt$nozHH>4QKaYYa^f%B70d`IbVmYbaBn z!^^efBZaSCLK-ph{hTQjRA4(EBtO*EH21*qCs@~q0C+_dE9^yzV zU!{`td{L<=#`D`%-OAHw50gw2tCUchtlP5a4p5S@sk0oqFv?Ns4*mL0Q)F%yZW`2C z8rt{fq3>J=txa|G(nx9LGBwo${B~jEthVOOCq`r^Yk5948qd`!Sibd4>Zz_Dsu-^# z;W3uhsV)Qg^JV9+zd0jvypOIF$|+6Ajnm}GdgO10!p4-L%qV zYFap4U0-kTS>2u$`$5X&iYrm=2;-VNtmPVghFfEoUdn z`X&6Ye;XYFaHNia|PNDN`TPw`SAt&)A4J(9~f5$!&tum7R<#}Dx|K_{Dtto$8X}> zy^?{TkyE7i5}MfC0C{I}dSv*PNN@s;nqffsf{I@JYgjc>DcX+%D=(A|F;w@p1@CWV zny1(;LFdT~Op}`8O6CrwuDv3v7aMf_X5zW-91#whlh$uWB?wK6RT@{4Bip!*D|xFw z8p50wM#tN~YMFl9RpmxUPixhgF?_?9RQVw$_L~4@dW4@mFaAWRAesVy_+BXHZcx|w zaB<%9BpXb&1Q*9#b4zFCG3kgA@~+|HvL#G!bHLISm8gyR*TcSrwi>?oOVe+4cubym z^;Z;w7oH_&>c%@}k>&fa+k)QRZRfS<9AZ)~wKWPl1$h>ORq8(*ZXfT8HjJ$P7Fa_% zM#6n=TAD(7Cr5o?Zvwx-6FJUAPX>qq^Jij5JHsAW3Asc_w7M2Cr>1A!Ga8s)1*0dL zlRJtecU6WrD7hsv+$Wp7e9azH>GM%Jn*SAJUtdw$7eS=X$>w#X5G0_rh$^SVP?UlG4b@f&Ly^BtZ#w(z7l@$oOw zO|L;Q5ppEwb%zHx4yPm-_A$cgpw8y1jA*tFik4CwDL508AKO+r{Um!f15+q%0|Zvn zu}3cmnR8vt8F-+DeM7|GEPP^U9lM#L#D2qStC?7HY0lAE(bs8zunI54S73-rWtZ+0 zL29SZFWEDH4QS(=?yDM)zw9VlSe!1kx0Yh6BL)y9*@-W2N_xn44S$#2hAP-w61mjO zBDciO@9K;n)N(iM+w|v^&8J%H4fQVM>VMq(WFjU@At-#+Ln0_mkRwMcB!^(8TCE35 z4M0}F?w4N8le{q)FMQPmo=2P=^sp9IZd=~Iiys@9jD8cRX047V7ytU%^f{TBg$zor z4d%A2TBcq9XLqr#UyvVz6WaXJR7F*`SYYDARA$6$0Aqvu>&fe}&m8KNbZNiZtIwLR z4MkBHH)n}oPP@7p$fGQBY2?3l@#F7?CE`#LKyMffk~zaEe$?@Vhj47cRqh1^I}oH{ zdb&bB$pzRkP$UvYZ(NC0R+)+9yj;FKeFsOy5dREGZ_M)igAhhB{ShNA4WjT>O6JyH z(>5(FG?5emz-bu`JqG2G;I2jimy9BeY38US5`$P9S1`GNL3H^uV7@p+?_mTOh_RY) zNbqOdyA-jWo?PGfBXcdK1bgb*QV*^Li@REP`G&V%M%pHjpPB<-lx%C0;%FjzZj1Nl zjSIYyPP1r7;fuL{7jwA=b}IbFe?NfFAFxng$uO9pHQvlD5H&MK`O%74r2%kQh9tfe ztLm_BZM%%1HstpKGJ?fc!eRRh_98w$z^w`Ab8ts2PiSy7uGT239*T&QF+&`G6O!m6 zEKlOsTxjMG+pqq@GHmU!B(=ggjK^eaYx1;bxDhiA;XaE)t_TaT;={!4qSn3t#!1RIouXqebmE1kJ<^@|K|0z%gKU}`?l-tE{q6u{nLT1 zOmTd*n6Vl64D*R_gq>-Qjr)OA^~>gGJ~E93E|(HhR3F?U>)gq zsYLQpAV?RbD>X!Jxr%8Y<--KkTE6KDqY&2v)M4DL-kkWvw2tuW<2JULHa!17pHU+iLy zUD|q9YmhRDTO;|~n-EyJ6>mz2yY=aG;Td~}ltfr(Ws(%kIDO84ri=nYI!_c*d>9@pLQt!w9~`OV;P zP({bt=`}yjZr_rMZ0$=HMQrw_-a>j}lT2bul{MwDoABI=zFAl_!m0DRRADmXvDx{7 zU|1Ud@gOH0hBty{@GYu`CSyWlTu)wAF9!%b*0hZ2Y?;i{MtXBmtwKSM`<-9ztDmE> zwt4>)%1MZo&@{~Vx4n!hLQhQptM9)HFoScKd1{T}k62H9*~(_@l~^Mb<;%0R=MP4) zwirQ`L_=epv&b;hEwzTs{*Pj-kezhB%VtnU!6wIk;d+?eB1^UEkY=mr&ujfD>krB; zE|sR_*%<61$y&S2cd zH2?dHPXf*ah?%S>aZ=A;$wmsNephMk9E{~yznb$$S-m4bp9FvHdv!(Lk#_cdf#UYE zf?@`>TE-bSkie~b#nk)BdH*IKV^Dv+^tT9xAi}86>uDnJORmgGJ3~zV^wmf z#34WLydd3Lx#52`TICTunarQMdJ=9&9IPGD%hkW^uXpzfP^e} zWI#Y|8HQODfv_3(FdI@AJbq2BP)Tf4-j01bZExOe_j_THL{Z>cMEua(OE=>iL$4x3I+Ui^=OB5W21Q^jR1G8~5T?b}3S`zDb`M>#*;B(N%37 zu$JOyR>aYQY&sK21Vh}NT{|J z146!wPR_hv^8@vKBNHg_yf&r+?=X8O68d6gAs)A@%=cqlg8coGrYka8fx>>KtO>I!bI0-N7|&rkAs_Pzs4 z+r~Fa2vw{oPBRB(;nn)hj<$VUBUOpo(d}GP_OpQ=-SAMCf(@WK@D$jw-ZUl&g*}Qbz{! zigVvxe*a?fDQ_7Rl_O8JKnSB1+G#-@E#6sahs@J5e*870d)ZBT zF-IGNg%7*5B(NbcVTe{xsy`l9?=Ood6TB-riSutKf|+L zq0dN(AjkqtE5s7I=2?=DqgS3XkNS_CfbxU={d4?@ zi!IyP_L0_k>H1+DM=x>IL{E)*QT#SYOq@uX*6OIUky;6NGh39qT-uptWzbuy>7?>tjwkU2m460n@BC6I5^OJ+)|)lCI3%wy*x zZ;i`)QtaIur{D!FsdAyfN;*}0%DcaYb)xuJV(ZS9DUBo*eB-*1?N`Ofxytt=@z42U zwmpR|yY#-?KV?$ME?Hk7pXF-*Wb%S$U?LBnuDOg*2zj6HMU0w03Yfguko}^@#}ITbbAd2Q|U;N4QKcCEXXy_|FUe6X<4Z+s+d!|U~r_GEI%#%i~@85{M^ zk&+A!Lx_NXsRXxdy~(m&#(gbuwGBjmWiZ3F!~NQzuHL4kbWZsumq#tGVj^ARp>&`2 z6uy6Wvjc~pS$*~`Y!wZq;fxv%mZ3e7+ZlSYlUVfzj-75>Y9@BeU_wexe%yW$t4qUcu#|i zkQKWCLbK{@`=aBOtH*z*SI)t4Z+-tDP>r(t3KPxP#>mmhA=Z5cGnOkury6TO(~M5Os@b&jtLpljsk9@HVB&k?5mG zdVB>ofMV|AYI2b}XKT{RN<@r9`u=pMwdB**Iy!5cT80F!NK$X+^gvhsR<@G^?&Re_ z*VMTVhl^-ps2O6oD~gdhjl395_|DGFp*F%vrt@TwB5FFf=IB`OJ>;f z3k?EJ653D_;5tIYd@Q+S#Qv~_V{5)7AH|z@o1phmUbr7Ub$)5qYN!Ykzx728g@WFD zd5mIVMP$$F-e}C||B#Sq%n_2Pn6Ngeb?@uKPZqB7Vfq$vJ!*xja9R#Hh925Cg9Fa1G*greaSy zjiRKH7j(zk?e9Wzy8T684)#R+~v$CK)=bl+UN4^Jv@mySAQ>o?IBn<@4>i z>%#9hL!0tn->Lx>Q4+}*VOK9UK3A(=Rs@QS8pYL64f=nb-ujj9ZC8^2dDmMMp;6>} zdX;Pz>h-yVLnwqi8}-%Jkt z-jsA`~t&B~^q) zO|(kzA#P^dV!dlUueO~GnwF`c{*dt9hD60v&fHaNp~{|VHso9S$^C4q&4P95rF>{a zsvFZoI2qRn$0XqMxfjhl1mh|CL>%VpIR?Bu~roz8@ zml8ctBUwn{351iUi4h!M(MAI9FwVXJnb7;9$go5%$q&!momwxPe0<73HKPec79@os?u1{i{IJ365qENQLIZ3y+aZz zaF$#P}}lO)uetw+PO4QYG``f5ak8X z1#jW|BpC-uDMhzf-t=NOXZfyX_~7=NT$B*Z9UgB`A+TQ4s${I+Y%pBRQj0%fhD`Ri zM*ysVUJlnefaZaKMy4AL4NbU8*^=?S+^uBb2t>7^$Px_@b^ZG;Q z}i~fsID3YGj%4lWwy*ii$ z1E>^>!HhB^tS?6J1;~|T(EXLWXg8ulF5zLj)xvF3u1FApPJLoG{?K=puvz38@>b^6 zuEwQx|Eb>spMtX~k1HDTC~*+HK8ow%^LJ~lnt$D>bsVa>XOnehqn6YO_Fl4R(NWj& zqZ;e?<;X>hJNx}$c-^+KFEk#z>-XLGr13sHIc-z9OET%0ks3Mnt@&!ad~W`;iLQ1S zszjt?n~UemQOO0j=YmML*rb%=m-Z5hPGpBH+Kpvze(ZtW)te4m>QS0T$86czANU?D z{Vqj4)A+$)iE~}E@m;vu*V(T5!mb~y&+K>v7!iOCCau3Dw7RXnNYF2@A}!Lbb|Cy- z^}Ibm;T$vw()=Lq+uXOcb0uy^u=M&ACRdshr^^(p>%M(|>c&#$bEd^NN#%@r<;6~< zqQhVvC@1Lr@%Q0+ROr$dapZFZ{tw1L_|bLe)MJf8(wZ76)-|MP!isBP$d=v+d*4w9 zcc4c$hhbe!ZM}22vyo|)a6(MYu2AjF&dvapv(2*G;iafdcqCN6!qsfGD$zg>)|zRH zWONy3%pe}KhC$IMRz0?JwBRU!*>m-r%Kv$jvD=|cpS!tUA_&WCkt*zD@~nS-(OD2r zKQWNvXQhSNlx7D57PBfla)PnCv%oi}HZ=d1pMO}Zd!24P99f({6Qo#n^WcOeG)VTC z5UH-=oefm7U~**eTbkuA>ZSMp6hhw z;k@{7JsB@Wt-er4hu}|^>6eFd2>%}FA&+#$^Ym` z;(QT21|k3ot=}nv=Y9r5_*otS(qrWW(jVDRQ<1H0C^idXP&*+iQwwe_5(X2~?m_nEe^`nb%T`1dF-lN6)L z(pyz0mGm#9D~?R;6}6DV?@xz`yE?-7^C!+xT(bSI*s6@DgfY5VACv9hjmh<*RE*YglCRJg3q_5eGN26zR2}kmeaOGKf4oxJ0oW-rrYp)e zc$TdRK&zhJcJ-K}33Qw1#7}O(S_XPZWfW92AxBk}d1esaW|M}c;fXypsXgh+~01L}NxSG_ZD^Nr7K z3Y}ihgvgk@dc%OFA7jR4Y%x6NmLZ+-hj`9jA>Xtg&&1n)6#I)&ypd;U5F)mRWR~Gf zpz^}9EJ_fA43VBWi$pYt6`cNlZ-i}0H!~hnJ&vY2kLxA)E-PA0bZteC(f7;|{AA4f<+VmA^AJ>^GQM^1OrBD?Mp|EvmIAIN0~ zJ2|apV3psf%OlZi5Kt$>oA4yHKSS@M(Eo|rHCn!iTl+HoEUJ}(_1JnekkSrQ-c5|> z42d!yg&3FUeIM`_4uU0Bz5trSzJdR*$1n4Z9k^f5zEZH>`OkWdbzAk9y*h5$MdAeVWMSS8E7ERkM4k!~iGUKo{A0g5Lj5ur#L)c7a!+ z^Aj;k%{!AHLXF!2(5s-b=X|#wMrDMqk9$Yt*Jqz*VRLAj6o>Rta@wvIlQ6cucLI2= z&dW?o`zAupBngAJXHZkdLkF{T>R4>LWaCbjTj%?ZEbEG3&m!Q&%i6>sd&)v~Gn z^6BMko`|{>H(H&+>B@v4EBf>S*wm4e@9^OGI2LNH^5!|1<{{$?Gx6)NNZS zm{RX!BcBa-AP4(3eQe4)N$DvF4jM6?{4U)U_jLt5DpbVYF55^QX;SN?1y-@`ntsH} zYd?AUN${JzFpciQ9(nJ8X%h>zu|ik}cf)3$+zq};1v6>IGl$Lyzt6+%%)#HAx`%1h zMQiY1CR=BH-Jp2U>Jc`7@jMG_c z^4<~PF!hJyqe#bIO~bF>%{CAu(DjD=QywC65=}(q8SRuD35QN zpNlM8ZZb7>x*Y0W>ky`5y0|FU@n|`2z>%wduIEJ_!Y(2qw~NUh&VutjIWxUye3yY} z-YPh{ijDx}A1!`&&D`))x#%7d>c=wsr@XO%T-^V8$^mmi>jehj7cpV&7I=#I-W+{7 zhO!fyB-&=W8R%KA|e>sEXt#Mi{Zy(0Wu8sCI$uQn34eIw~UpYTuOfN)JXg6 zTFv8uu+^fn$pfTlPTSsIhYdE@DmUG4b6 zH>#8ee9Z@=A3PnXN9*E-Hm4{a3-bniId-$c;W+goXFL%Z&O=6JMCN{b;`a-KMvh=y zBfD%ZaF;}dP4|;X|CWP#FUy)=iwA8@@PG!l{~=yruY519S3Zoo&`q=#&+AqWvYCc> z;7d!cRWD5wEt<`QoXp3LnoWZi^DF1*)dx~Lp{v#6xfwCB-O*9;qlw-ED$?5M1v-Z9 zWv~|1h{CN)3`A5@Qkb?pD|!~>sx~8l^uQVC;IwjWxbGRR*KKN3fI%mzNN1jj5#-;F z{d?#hQejBA(gw4gv`YnE$1Zp@&P_L2)z25U6!1)w_0E%hGs&1vaW2i9(mdbimA>qL zlc%;a>J+~3!n>qft748)O7YgPz=ojl;Y*}gqdEB);?9;;X zaYrdL*M3MXe1&)ZsI2Gwnz>V-Sla$+`eZT;k!PuY6J{$h&@3gCLm z!efte{xiUT@y`w91pa0C*hEjM<_7*c~;HP#x0Px?~V{-qtgZ&@yGtMtAmlGQ2pIU+evd-_KPBq6)%=BlpR(|;q4Sp=6!h10 z0z3}3zk-HB{#TY^|1oA3z|_ zQ!#@*8uC1q;71G!eH!&+%RUvPM;|;qf7^kfPniKecG%Nndc+>v_}}yAKLrPTyf8nF z@NsHzKCS9UjOS@9K4O1W`eSa774noV9suZnTUO%V_pV37zb4zC8^~XU1O#(~{>tug zm;e*EcOP#PU?|W3ZvCH~A&+(YGz2K;(_6wL22Z>`}cl-*!*8E zA8&q7=icL-;ry#9IUh&x6Ipw-13w+~Ku*rbB7KqwCnw;aLjd)UdOR9(gA(cY;rWap zMvpTPU;+UH48agX&Oc(V4>1688$W8CJ{J_iPtEuLZ=!>V#?Oz5=IEsF;N<3DY=VjQ R=z#|W!bGE|7nK+L{{VMswEF-6 diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index a12677c..48c50a1 100644 --- a/doc/invargent-manual.tm +++ b/doc/invargent-manual.tm @@ -751,6 +751,13 @@ abduction. This makes it faster but less likely to find the correct solution. + >Include postconditions from + recursive calls in abduction from the start. We do not derive + requirements put on postconditions by recursive calls on first iteration. + The requirements may turn smaller after some derived invariants are + included in the premises. This option turns off the special treatment of + postconditions on first iteration. + >Numerical abduction: coefficients from 1/N> to N> (default 3). Numerical abduction answers are built, roughly speaking, by adding diff --git a/doc/invargent.pdf b/doc/invargent.pdf index a5d0e8c93a598800bb3e2a1c6d0fd280de62188f..ae75497d01d3b0c47c350b99d598e865b0f72f42 100644 GIT binary patch delta 32612 zcmV(=K-s_iiV}m25`eS;0hoVXZExhpk^U|~|6x8_IE!JwkWG4R9Gv(ZIKW+y?B4l< zl{2UrN@8|qI3_u(T_DJBPgQsI3uh>DG?eU(?GF+~Hk;M;^3+q+?O!f0;)wA@jQ`pn zmYd6qU*He$qs&vbP%%pvO?i3o{@s7&1=EkQMJB`| zN07R~bEdR@JTAyt1AOY@$?>8z@DSu`tsHH}0b>#OUk?IO6A2o*7DuKoB>ZVz94 zyV@_is@B)xCFT`PQMF}@mty5UrGR_>ws`la%ZqFL{hGx_f*`K)W0=T_lH>jK`RaCvGnS}kJaO?9Xnwl z2X5~aizGX^^Zog=5NhFvmdBI0`Qj#K@y*rwZ(xZUwSryIw&hC8n@3u3^PX-MdchMOC8Ynw zwtX!1i$IUPa_V^|V2zyhbogB1s4VxwNd|Oa-|os~H)DN8GAjMYs(a7|k$7ou!K5}t zU@93mN?#vJX;*jPp{im{LzorVHT5m{F1==H9MQv%+Jt{NI6QJ5cg1>rjs8quPosoP z%PfB)oY>p0+|9DHY}C%2^`wEQ(g9P5!A6{?IA3RS-WoqOF?#9^kBLy%SM}hOlUt{~lN7B3H$R9lnT~7X%@=m?P`(3J@SU@Qd?MOZ_D&wgj)5WHJguvLaBquGew&zx zR5N0f9JhS#W~;`94WV-Q!?NQK`~LjtCP^TQVTFG_J0Jz_Cm)eS!bT;Q+xz6W>3#oy zGjyL#tj4LT|Cs2z(bI^Hl|Tj3^t!3h-3Agw>=g z4oFDE1h3~1f-o2d@Rk=oW$6ZID<~u4+mdNf`4qJ`nzd%4hOqmB$fZN$0citfTFUrlSl2 zGey$RyQbdEa7rQ`^$KT%AKw^CGYJ!8c6{#)X^JUVKA%+K<7vGn<&=sjrT%|m zs|k>*)5entu$#Kx>7R2?dbPB?)~9^9T0r_vztz=Bvotcz$*J9z%VOW^5y4_DspveB zPKa#ARIHn_SbZY?kJyy1L%(50&D>lIw0P^rP~}56MxL`=Y2(f$4Mm)zP<*c8W)nEX zhpK>7m?8@T6MtE=4dd#77I-QQ++cs72-AeA^Ou$Z(y8jB{%hh0U9+OvyNk@i1LL@* zBjM1!>*pkScI)aPZSL_pDz?#V-a;`IrWT_srA}X|WOSwYtAYvvaKZAGWw(sTEC@3k zM=vl$6Qb+DVtAgbA&b#K0^%wSfMBE5Xd{ly>KL|%XWYI69t4-a)anz1q0xUl+PX1M zLZmlOw&kv9APj3rz%#%+q$7qd3rqmDJ|a4r#{6HTQ@j1vN=UGr zXl{aA%p2mS1Y^_Jq$S<7ZN`7fg0^;D-9K~$3kd?%t$qfHC38i8Dg0>57t0z8B3-#H z+g58DPaG;L4xTkkIE$^`l}%$b1Edh*MwU7RT!52#Fkla!vsX!$ICMs1ZOq(pdwWB<`4X4b0c0@k+TIpAZpg&FaQRSI%aSTo_PNSXd5YX0!N-4u_4HW>D;0&P zTT1C1VE1WP>hvf{nM20!h!xDNplBIzARF~eM3vltVh-D{AfE*H>nPchW+-O&*pEd;l?-E*pN)m8b7 zr2)pvUAFbUe5~4XSU%*Iz(H#lTkLjC{jq|Hm(iS@;EXJSD<3xaLQl~|jARDzwt+LO zC(L7h=hDSKPa5Y#tZ^G85K~0E}%&ht7TJHD^f7NHKpBlmGBgY|Ug6rd$n7 zJCuYAcfsg=!c}B|?tR@<-NQydmXWI7mfd5iA!>r2HuwZRJeC-3@xdg#h|3v;ge~5u zO*M&gSEVa%Yg13iQW$@amIeuxi){w?C7f#oUam_l4Cy%u7tG3!ySmj-ddLQT*n-6? z8)S;6Dz>(&Y9)Vhhg5`dxjc(}g%oT56uaRK-Ll@Us-XN&QRMjPd+p@mBW-Z%9-4Z8 zuZvd@C5=}xRW5x=MMP4d(nPc_q$J<=dJcSbv#r-3jE2F22he9o1eF$n2O>rYCSW>8 zMMYte&}a|kde;*24PL1qVm6FZ(*i75>`JMDpxUqIl!SjIYBskY@e;Mjd5$6tYTN@r z{qK%b?J>JUIk^MsvR45S$AhMhC!EX@t{FCZP$2qR|DHK@ag&35V`_FY(t|{eS9Jbt zadKjTOxbL%`b1>dWh1~4Bqe-2(QrL?DEDc#<`{27w~J`nK`?+p8VEAyLE496XN-yY zTz}||dT@XED$@0`K^#!7G==~#*)KU0{5Bb-&PWbo`wU&YmO4N3<}oLydm-~kCN)$* zR%M0o^_6LrvCHl>l*j3mhR*N>X*RB*-&x;n=Vc<0_MZrU7P+i%!Vk(sJGWX z*VZn|q4N&LxUbm^W`AFVl3Hz#vG`fzU9-6yIa9T<==~4EP6|WVfam zfY}}oc@}`KHb7Yk&oLXOm5cBae5?5F&F00TiZ5!bQ=>{Y*;1r)5}O-+O)FykoR2Db zHZ^~{8In%Zahv^pZJNJwmxobU!4i<2YtKOO8+yHPxzFym`%T$YOVbRdeDljw1DMJV z1{ji3FDyvzgR+6QGL{6ff;W*VLLT1l=L=&YrV{jugT(F_hHb&Xn{v5tTFNZ3(!~2c zpD$oX`~?!H&(4mVrplA;NS)Z4_x#UN0qK7}p!(nT6vXFWhA6;hFma%iSB4{}uw@=Z z6E{BAu;1?YkcEidLxhY3x4o(asf1*X?mNgPdPc=eHg{TDV$6$6*CxH+u4VzJEbB#p z@5;Mkzt)DS(#S=l4(o(EYAR*KdG-qO@z%DVf((xYdXIOs^ zd%bs`p1J%6?-s$WqwoIPjP%O-I2h)e8L4#~P+mX9Z*)M*ti`c6ME}|%&d~)v;}b+a zUO}2++7l`AGuCoWDU*+56{=3>7CTdVfneI!7b{arhP>15aH;1sS;jB#R^(*Itfu~Y z7;zdR4x8`GjXwi|_Ga`{qeA9#m*ameQLy4RHa}oTLgHf0;h*c>THiLbA+wRu^8GRz z(!SUixcb`1k;yqG=85f?s04rXssO!=RTlyJ1%TMrYX@HA=zo&;VF4g$1d`S&f~wrL zj9Jepe{GiL-=Rowsx>)TjQ*F^q$a5M^^uElYS91r2uli5$E=xn+wLUCc*JEm--6P`i7{ zw=_WNVn}q6+h#FanvPQ!QIDUq&6+_qI?aa@7oBV64jWG-Dy1`>L=c=;N_ z$?txJ8p6wc_pebyaI>9PLkKIL16&*;%b!i-HiWU%W~4}_B%E0T`{^I?oA?cXBmXhu zgTPmeZ_f8;jc|XJ^r5CbwES4L!C^3&q`vtpbL2%(lEhP#>>*VIg2C1G8{EM| zP}=(unH_^Ne1Z-k|JH0c$aoaC%ExZsLa)OX=V^N}=J*qyvJ=CZibws`oo2xJVBIl|fLBc%=D(Zi=J4*}C#;5x#}a-~-TcLapZO2M-q0LtCzeS)0ZBDo=o@s+(j9K9J_L-KT8Z%Z0}Y#I-R z*_M$+)cs34qmz7K>}3t1Z282d6~E6oVQ$YdZ43crwH@MsrK^oLi(tEmQ(^2%>uvWC zlq2*tSa^RlFe@S|cH*|VkV1PxgK^`wEp5)3(s--J4Yq-oCJzv%F45Oty~W1rcB>VN z8p^He*ey6V7ZK5MCIUWaXa{PZ_B|h-c2up(rks-`obv<#yv#}IGu{d^$Crg$L4NQD zAj0z5rZKm5$QjbA?C|)CIe2z@FUWCSQu+SUrUZX9Zu&6KUWbVumYbM)jN@hW&-34y zPZS(Y3lDc`LqXMcS6bhjGZtm;L#s{Kv(#l;V5eqlAU-SXPBFd7P-cm1HlKXmT|iUd zVGx!b(9Rc9Cu{zr3$>|NCb%Rlb=4Yj`7mcoMEtTZ0LS1?>9U!D6*4)#@%S$@R8~k8 z9FBkaM90Ktr`;r0#SG8RUDeBnc5HrhCjfMmolz*;)NN-NNX$je!rV9Yqo(sycT~)# z-qu~cMGA)A6uWK9#Hj-KuzLaMcr`2-kWoL`c+GR+wxu?v?7&?OVb#>TooUMx!f)?1 z)AjAE=3EcJg_c3pjUz+R96UR$c~Y4z&(eSHn71b+N_Q~A9ay`*gfW=}`s6p@URw(U z?#nH%2u+$h_5lwuX`K6|b5Bz{F9Rqz9$D(T!B-_!R4k~m)$|l{X|qqNTmx>I(|)JM zPdNC0#|2FtaRgFTE|+63bi&fNj<7{(WhcJ=8vdS)Ws?8lhUG}zjC?-~>p+hhXV`!I zTmeh)_!)D}-CX7I&C9}V@73pIhpy7xfH`y_40mBt`ss)q#->h->8T?hZwv_IhSjE z>)CK|f?IZrmz|(XSlv5NBzdl1n{)x}bVW+z6J5X=^225~?=+rjI?}}vcScxKQCM^P zv(0`Z{N1Y0>hLLZ$V6~t#HQG4^#bIUxD8roe+SFrQAJofH#M#ZTq}ZYz4w2bz}0KH zl+Q*J)RZP1uHde2+v?UFvz`cF;W$)=M*~cd&<{@Jz;mDtMAs+U8OX&=b`RLJ-pn}^ z_nPwaDU7xf5v|#`011QuXkAHhj5=kXxYHeNoIatUtYZJ|4)2)3jSZA|L^}# ze1>Fw<3indKgzFk)cN@Fl@1Au@#@a3lf3gqP^lPJPd2Qcqw-a!2eyAdJ$}X{Ad?R! zFifpG5I+M7l&s_X(e|h*V4pvj^m@V*sA&N9JX?qY|;I8Zan zIQJfRj{B6m%Ke?2;5j~(e~5pW&*dNEpXPVvtwsF(prCSDz-XnTJ!lD|zf$uBwO`YL~it-iWep2CY)71^q% zvA=b`N!*{Q-d}HHycvp(t#*f8>HNl@N>te#jkVV18QhBQ=f+%ix>>wND?E@gdyZ-0 zwvy*+Y#a}~pAYaszMJpi5AnTxA0Ohw{9(SIKf(`iv*SOmio3+!;Pw1~#-y=mMzw3S zqX}CR-c0y+;*)=gb%}@6-6Ay)iwT`WJetR}>N1f$2Iy7-N^sZdjpJ6#bNu%AqYS~2z#KbwRCgqL1{6iK1CKF2T;aw+J*C}Al!C&?du?P_d(dGpV{J- zF)dzSLW;k&$5?;3;O&-Ay!~uY?+U2s;4FMbc@fO} z2!00_rXuIzEQ%lX2B4SCGUV-U@1TV*JXs^P)PWoJ2>(ar>g_56oPe64;2VcF?L) z*b2o{k#Z=bwCCD7yL{jlJi*Se9~T_|G$IY1fMf78L63iq-5gdgFcOPD(Bk6QxS<7_ zhL6F}Ym$0dcNB)3_JiwXNw0n-PA(i4ldiE!%N4EKFHV{b0bi)y55lpeV4puUB`IU| zJEec;i%~-yvathT2dGc*Dnr>4+i71zNwv5#IIWn@e{n-y99+bn6?FtOyHyC7zMQm)WXwhGG^lV zMVxm9lmCibAQ%Whcl^AqtxVU7cGDRLt@O~NKzR^Lj>P6-E?s~B zJ(;gl`ac$hJbvG6APn}#Z`cef>h7Cb^{g1(WB@gJr#hE%@%j^JHe-6`guBn@e;I@W zp7;nl1770|5sWNr5PxAzy*j3yEWd3uPyuC-ma>>- zux*8sdP_F|r))K_uT_do=%@_yX$h7y%f}^HCaDwC`6N&wS#J(PJXU-6bCX06Xd7r=OX>VA0~J=U-T|blFR* zqSvllzhPtSuDFE6q?FXOe~irR+&oEsL6Nka#|OTVZ{nNz7QU5loi~xV{Reb1m0hfbiVmy21f8j;sL2@6NOeW4eweT-z zFV~-bi}7x3PwxfP7dlpDSDV!;old1=rCXC|;3ys5Y4C%|cpe*r$%a8|%w;?9fTTz}^2HCZJ&$;|q=^^X)SL}bq2#|jNvtJ(n$Fq@2K zbP=}*YgZpgyaHF?&CcEfuN-VU2Up>8;?bnW6Yc$H;4&i1$kXC-jZB{hWl(64TTQMm zy&L@C1g{3+ad?dwUPy@Al%DM>G-UuPSZ7RS4OvIce>KnzmBv=j?j&oval2_v-g8;; z@f(&Utp&6&;lw2uR9b7{vAOClwU@x|d_uvtj zZ*)@(JnAM<^H*t#RfTN+;tYZy2g$4|hu0Cv%S1ZpIx+>1C37qu+!BC{WkX*;-d#=4a|E z>dGqtHC8rM1xn0G4tA5f3`zh!n-sHpL(96*e=63KFK*o4x&fll@&xkC%=NqWy>+%5 zN8<@yOa!-_#0CaRX&X<}@edutn;V^d0{k}jmbgY*4|Vk1a}a8bGsVfWL7u~EJbEkm zk@tJhGy zTU=?cp##wl7DJ6jsgrAVLIJ2iW=9cRiY$PywBaiO{=W0LBfgy^~%cGpZz2`7Q_o3W!`rqYcbp z)|+$|xm#VSszW4(J1;CavBCQ?O}QLoN{8OawyW*x#--?U(nwlJP*_o+Rzo=|fA&>W zRXN=*2NMQkx*x9?oOy2XWkEYxB-T~X8P=mxcSW_|Q)4zUR%aU?AH=-6xVG#=6s9Aw zm}WTbyXF0hADQ$piO68_IFcZKq2!v=Vy!cK*=9W4)fMR3f8|IZ1gN_$bIJNlGCX@L zo4R6KS_05QF0b%&yc2wUh#M)!fAdA&F6d||fFhQ(iwYqgcD|gNl(h}i$N&nD!(?&T zn8R=P)1gGyMbpStp|(O@09quomjv3a&6Q>*Vn9g2#r>IPagBRe>~>Q^Gb5YUrc`S+ zDm6o-#378szfm?y`egO_N9F)ple4KTe7w_Svzpk-J#7{nv_k8`>YZ)#f7|Hn>A(Pb zr4o^1;u6YagM_TMscm+v-C|*|6uX3NlRfbb>%19(Eg#b94j%Pd^)|WOpq1-bMP6=6 z5p0H~Sd;%YO*k?CAYKz@um=wEgH4T%0$RaBaeG+{GyrNk2BC&zb3#F~zBrMUc#3Nw zh)#de^-)z9Wc4s^rAcoGf8_OfeYLB0FC`-gZ`s0_u3U?bjZRHl2iwt${j0vi_Z`1c zY13HL8l6_BXUZgbiG-5Qs=1YyI-2`Vx3cYCalONDtcJ!xXqT$=h6E}C6;NcQ#6O8- z`thn0_@fj2BTbyAS%4Ri1!8TvK@S>~U#oUm1Lk@cV|G~EgLsnDe_%IMQz$%*XHvd+ z{GIqy&ygvs$wsniHA{GP>yE=^Xs*Y@PF-*~X)8>~LMxNCfJ}LG#`(p6&1K#@ET+N* zN+YT;7|o{Yo90S3gztXmGg`&*>ySX9eN*Bb}v;{t<`<)Z9I~KrzYOdb=2{%b67C&6sHk;XqUl_+zO{mrw3IzbL&;&6UsD7 z4J}uNL*v#UE_}tSqA&yGb~@c|m9@gg-U?u&@L$fuMPj$re_;g=c$8L|72SFj`-J6o z8UrAiLLpOF)jk!=1&Hw${S%g{G-^;FnN#65o51d+;VB@5w}-eF>iBpm9wClf7GJhg zS7A^96d|=$<6wdiGB;Do>eRJ`mEJ~`-mNgIScxgmLEG)Ixg9?A7QS1EEh1Bak30Z! zl(9)ySa#bge=vJtzj-hH=2>0i-~k?}bIYN8CD>bZ?5Y8wP+td@V#@Vem0FHS(XHiT zyaiuxBiCuR1{&V^0Nz6#&9|Qj@DuNdf9gb>P{ZN@5q=zx!lS;pyynCsZuXnnZ?D3i z(ADMV$Y_RqC@LEIVy&qb^wn&Q-f4hx&>D2Q3RF!@f8sN=sLoE4c|S#*Saic5y>rf! z(@6wN){z_HGTKeGQEt>3!>SJ^YYn=9+k|+H=(E~IF;gFZgp6V%26p6!24;l#uig|4 z7zbVwoAq{u&R~$qm=_iZ6~66n5&@OUJd#gxNGX|zM-e`r@xfa?2m9Dh{#bpJa!FWZ z)f&B0f6pi~CC@Kevt-?h;!S{NPdtie_51PMKjV??=}Vs;p#c8N$pr+laXN#1yxa{I zYOZRmw2N;*Xn-H$55#;Rz;pglBN-G`(9~J{t_a7|q9)-iJaH}_P99;yl^OcD&Rb(J zc-ShvO$V~umHDGVe7h)r6@77iBe`#DA^ESle`FY&nK*wT8B6mKihiaz5d#IZU#CL2 zy@Nln8JCGoRs1aNh3cXsbXI>;z6PJ;N^nizc?tnLNlkiK?dr*+8f(lgztJfHG zVY6ycI~`_grG@Fom zfB$)}YZ~&pv_9RRhRFA6?)q~M!ucG13k}87>%(N}XaE8!4q!uQdgVVtEc0kP&$9fnH~27ki|x)?ZWS%xy|^ z0kWFRM%H9Irrk+k_D574#f5Emvr@0+EplfIv!*RJ3Mj5-tqzusY#BQ{j-INBnMxjLw zdaE2^)2;V~_F}W%32p%MAh+H_5xu(!pQYhXrCN9#Ul8L3B0LGR-{9eIFTYCeWy#zB ziPisaRUbkT9?$jupaq|auJ>gxi7$LIK8fA3W3_T8&3>XNVgT|3e>Akd06t2=)^e@m z69IPz_cyVv!R)FvJB@AO1?&fURauHeC`5!uH)rpA zonQGpGB7CgDwUqee_a$)Oq-gj3hW8lUbVEbCLfK%2X8M6WxJ@?9-vx3tC@PGi@5Zn zVBr4S9H}uF$|{&`YlS(7HZ{ITbNdY$O}+G(r~9_QTFU-4OW3VARtodb?0GY$y+i~7 zJg&joV6-tt3-ymCPsz;*XP@kTnbaRGo=Ok&>yb7_owTpW5{qOO)FK84{snYqq*8bcdC8Cs0twly1qU>ZHSrB&ZN!4>YE5^{3O!IZ;hnw4g#0wY)l z)oB4O{k^{*ix5k@GlM%QSVxj^5vh7LnfKpO}S8JiR>MRZ6 zd07B=+~^s6PMJxWERq{1E}`02R#sA~F9sFLtC7{V1RHt|zuf&inLzFjKf9cLV*WRH z^1I)8Y-&4o@_MD3nLm~A=|+cEWFJ1Yf4A=Qjx%hi|JeRxR0MXH`?6^>66lSx1NfN$ z|KMd@-7dhZafz7PHq#OR#a8P{@Sy_@&xRn8I_UPK}7HEQ6=}xUYnF3l;Q&HR064-rkd;PAI71F60jJiN4&m(uC zB|j)mEqh+{+$~lpeWZBSCeTv5T2yn;?CgR{R4?@u^P9O_gK%#-8D?x*?K(2 z7=G@RO{4R?_kMtz6yRUEEa1|(e=%YsC2p_}!bqO2O42gY?&PL8ic}FrY9#sX)YH+I zPaZntcCki-u;B5EUDWF)tXWflN`zUG%Ea zRAps?pZ2tN0CH4AT7jxSD`%BCI|wR?k>`}B()oV5Bl(q2yYUp~;FN)`bnsF3s?AiU zRj&F*o3H*f?c-y#Qmzj;fAe5KIklf6Iq`02^S1x|i_hlpVF*i(Tt)u#8M*Xp!Tc)hN9ktVF ztaUJrrw^V!2FO>Vjg{zR+VB(eY6{v@A9)5x6z_li1oa_3|7k=Se_bJ&a_fpvJGks2 zNu9>&t#o>9jMdqTSK1mobbl;?<)EUQk6d3t1xSXXd*Y6^2CKRQOydFfv45hT!o`x! z)N~Y;ySu6_^_D8uQcYp%g5RxZnd=VKw6)bYywZ1Y|6#CE)i4=6db(Mvk;woClYW~{ z5f2rp#9b7mK;F|Te`(*5wO#p46qAw=AD2*yBK|gPh#d#Uo~k@2xN%afD^*KCgQPx1 zrKiSGXJ?Ei&mmhQ3VbBA1#AIpy`|dGVzg9-`fmOSP_HvFHCL6T%wV$!DqJYk7AjJ1 z|2kxAY;!QaOV(No!+?sBj~z$kS4Be?c#ICLf|Oc*yY&7?f^I zdw%_G7&sf80k-z&KI)|U(eL8+J@?$^of{JwgICv))sX8?v*yBV*!ohjMAIMJx&yXD zQM^JbO)ih7sy+loW5C8#U#feh3s6<1GNC{xE8j$$Is|h*{@edM@s(T2-6b)sLShJa z@MrQUT$;LWf9pTx(YFr|qj|g@(-Sp&>r0YiMss{uX!~H)a%o9QSu|+>J?c7ldFl^Q z1KAkD(}x}}&%G?@B@tp}ie5$WQ9%hw8MfU)Xc>HV)uC&n-@d&M$f0Zt*qxqz_$hlM z>&2i^g>9*cfR>kEx0%3X_R!Eb$^7{AhhAFp&p!Ftf}1QI_yJ3e zqrK*$EokvJA8H6V>@7{ygEv)H7$;O+?rLyD0`FIUj7w9 z|4_qZe_5dK2A+E55Dn%2emt#Tz)j#riL(ra`H+vwoTY(4L-n5Cn7s?heTh?cK6|ya zMa>+QAC8QGJQ0ASa_>$J+k5_wn34cua3sQDcRN$!^ZH z?sO(O;_T3iS{hE@Xgs2duVfcW#KIoSqv zK$m4mRxt5oj&Mf!5lB%5wQ1}PQ55Oc7E`|2ush+kzx0P8rv$CSpp$8sn8_RSQUDdm zz3mMqyQP|@d*L?FdFR}e&A&b_cJJ!U+5byMr)*u((%7K`0-i&TPPQ5Igyu@uZcC-L zf8Mp523A8Wq{%U)D4C+gJ4sZEo1zJ-W*6mv8#xbjNB~gJbFBMep)fIq;;#I~mTk1v818o*zkr76sXyg?8K z+G=`^M*C9MByW^dFuCV9xTv&FUQ5Ke;rlwwCZ~z*`0jiomB89g#hUcuWr-w`e=S*= z9J`Y$lmrUAjn;slA}E;eD9y;tN!xy;@WA=5i#9XkN$iS01?cO3EN%?9MxocL^lWP6 z(!4Z4@g;2?l#r+gjo`|uI_|r%?JJ5Zw`b@_Sf3|9`h1%<%>)B6aJXfBhDq`a%O4q{6=<%}|C--zz zH#alon<}=(ZOlnY$lOjn;|_E2o+|Ky&*O5sytE&oY>QlyTC#P^fy6Uke|-}Rn`x)<{XmzAexQ9#RGa+lL;w^KjwF-tSW1MOQozv*`Rl7 zy=8#P)a6QzBdw}{B_D~3rBGN{0~G7|0WQkz_Tr3yh{U=_Fr$V)W##d{A3c(p{rxB= z_xn4TDc>_$qeuS_#TX$Mm$6m@7MBms0}TN*w;j#{?+1T>Y+Kb8$L%-{7f8+8U^)@< zo>#`!iqHlabfFbnh(=3jmeE$t_~ptpPU8~)i2aYR7Z``r8Zyv7C|pU>aY zRkIf!?(To>eeQ{x+a&b&2-|o(e%n1YZQsf%Zzm^BSGUz1_kM@h#OEW6BRrew=y-g0N5^B`YK=jw zI5|W~cAnTJd9<^0Z@c8Nj*d=Amr|}(oRFy`y)u7lNUoGo+{3Wsi28&=P8lRS_YYB& z=BYh<#>U2W%app^YVFCVceP8#6x5L9uv{nCj>-ol&#G0F!)g_`;SO@gzUO5M6^{>mnzx15&U=Q}!|UTAu2sAu z|4@H}u;HhIMB}54zZIIQe}Hm@#8zo}TMMrxThUg&5(gK6SpkHfXu{i;s7FYHlQQ1l z^0qnbh@|OInjsSSStc$_nZQ77e9$z08q{P<);J4u;S$)h1Wbb4HHFywHj+ZC(qsJz zpb>75b!Iw3<_g|iYXRozc{l?_&l&JGKUjY}>ngSeGH@noh7p|=m=RLP*l37C02p5k ziK@3*S*h}AiT`DFzo2Tbd{-Qe__pDI0@)Oyp>(Gy4`M@on-SYBeYmtc5tAn&~#+R=M6=OTVH?R zpWz=1=lhC1%RQM>=U&E*fIeSXOUF!LKkar-I!Wv3h*1mZ0J{~h25FiO21!x%N&Wk{ zvlJ>};rsks7yT;&tic*_`Sb!T0y_UYSYD9&UQx(~Y2Mf=Bow)+) zYvinr@dN>-lF3wZ%5U+L!%1oSARvGCezvW5uPR9uOyt1<>O~kt2R=H0CD+!1nPp=A z%-jk@P4RT5-{tI zxsj+MWshZX7Z&mHTuFfQF)=*ce^jHla9si$vWF%^vw!~-Z~ahNmdYvR@aunh)%keb z7mg632O70-sq*C|KECstF+p`t=Pyrm{J}x=K(u7!8&c5o}RS0Vakd&q-^;Uye5`j9cVq=1Rbq~>i*^jDXmxEYBPY^7==QeOY&PTw{K+Y zTs{p*`z@E*xjL6~bOAW^6lz@N3$9#iAYJEj+^qw~NNO1m4MFflF9!*bHuPqVYknO&YmOf$1nw&yY-xTe_BPk8m=T-?kNvcRFm#O! z3;|M4<`&}N^MN9{hZ27~P2e_+4a)k5Uj#ICEPeCx-0fezMJ}yfE37~nE@~2e94qJQ zZ-qr)^KsXW{7pecQf(B^8PX%_Q<_uioGDv6d+r>uxyHG}WH1xV_+!4%(%)jg4rT(gkVIEry>Mv95%yk9?Z75!f82jhIw>6mm()S|w5^1XkraZ&$Y z!+77T{V)Ho247`3lp~WDF5@OxLw`J0ZtpmB^!O0rxUnxe2N}-p#Fq zuetd@$DA$#m$6m@7MFnB0}KK(Ik%471Gff$F7@zz_{mC9iC88TN;1}qb_*q?*~Q|5 z>>QyqJGY=vC@wE77L}4;P8yd=|7OwRrK_G_yKd7f*}1~J{K7p&rQ&i~1&0e<3)jlE zamI6|aA?jn&P>iM&TlzSaprSYa8_|vbDrnCzVi0%#CY zDwQCs^+VJW0aGI#Gg(cb2CY$T)+6?R;lU_hz1yr^0!X2R3bjk`q1&(7+tY8D`K<|K zOS&rr@t_K%CJ9(2bcI!IfgsqyX7i!60fjoj&=ZU*&ZTED>i^T>BWLKQ6(?1H9e~ay zkH`GvuS%0aXQFF`#X1$#f&%n-0$Nficx=)9dLf`SdA*m~gP42jJ^JW{v*CSk6PlK~ z*E_RJs~njmtaLUrhM!L0y9r+cn-W~++Ev~_Dsxfr>9Uhgu~VkAbEiuvcHTe6@=aQ= z-U%LXTdYoW2}k*{9mldhCWXy^z)#-AzdbL$u(gXm-ucd1_!zO<*u{bxqt;Lg)lhEH z+P%(%#RH^1=AZ%LU*Qb`$Shm3zM#@s>Dmma;5Adeq|q&q4aa$px?r_E$J zY}(Q-eII!(UaNzgAt(fhl)1PX#+dhtORpA!5x^)Py(NS&t?M`@@QT4 z8k4cEj$-w!g`b7T*0&U0D1Rfn`9A@z5^t$h2EZP$I$T!Tzqj2Rg1vBPez2q^)1f@d z3J~jK!+dSM(F8iAackTzo6YT^V$l<)V=?sS+x&)5PfxHRyshhr18cfox^8L)bgAQ1 zc&LpklU{42)gp0i6>Ncj`B){rj?$Q<{4`!MRNu7I+`fImZXRBU%LNB&I-niU-i5q( zJk@>pKOT;~x9kxLarUtH-Yd!8*()S$R2aUbCk(tN!nMxHaXW%zF00@;JvoD7n} zS?bFZY!qrgL83GMruGCQbQUivm&V0=F#1lA;oDW?0d11ii|azY?XPvu^4s$LT>Vue z+SD}ywhW{dE1J1>u@Mb?Dje1FMu&%A?iQiMwm;`Srg;$2&WRZL`e;SEs*JOE<1+P6 z+UIr{?!Na&JRyfpRtzJ(c+(1Oyvb=zkV{)O;VTTTy6fd-Sz1WebNSRm6 zh|=2GUkidahH_(b{IT(%`iKgs+ z`coHD8Xq*~~W|W7!@~&r7jKu)5zn<6!xC zo06Z3Y0s65Jy@^yIj<$*9eKMaW}2mu)76Ofi`B}xHV+5x#IX<+g(m6TC}1AlgcoU{ zdRd-I_S*2sM&m*P3H9CtWS&l0zjZ?^?JD9}EAm{P7?h+dt9A`usC^J&?7OEfnD#Su zjWA-$fr!%VY6`Z1#Q!G+&)IrxU2r-2F3Vfu+z+L^8Cs)6==hfJD z8Vqhb)6nb7anG45XGo!GmnBQjTVXK*CHO@ae_7G2Fdf7iicYjrdTyQm4kFQ#>C`;Y*I-{1>yoJGxo?BCUYZ}CWfLF@SUk|E3 zZonTlZ+|2_+8a8%obW{G23&@4Gez}*;!_Ms?a0eY7OcHkX3k|6!-(oh@CZR#TyG2R z!iSr*&toULvx7MGbQ_xG+#0J|^d<65q^J-%^09K4TgI^4-#VYaNERxcR3H7`^Rb)6 z*mO;5W>MPFD{s@oflK1hw!A10Dn#>PTKNnA?s9AWrMfet+18R?=CHa#+btbY-$*gY zyE4}|WRcit83(hfO+j#l*sbC$xXMNFov*Tf_0iQ@USsLh2#GQqJ<(XyYuZZtT3O1k zQ6@8U@Tq5+I{RFz^73xC<}NVN$WMFji=1(}oYnYB{_xDC>du<%Fx?r&bR+e;5ODJR3b>ON9)=55gp!TSD~G7LA>R#=-qWAmjulV8w-e|PjlCTk*FY*qqd0OVw5dx* zvv4zYRrqNCJC2;k87I%uy$au9I=v?(7sIpmQ@H-x*8Hcf?Nnhl^X*%jNpN&gq)2dp zCSw-xB+@gmW2w?9d>Z+n$Tz7oWRcxr;aNfL;{qbJx*GSH8lBx|sfnvM157K(uIfIa zrN-)qYVX!Cz4qjiGRu07yOPqZn_9pr^7}qv?IpB<1%2W}trzby?>Y+4e!q+QUYLk` zwhb!biBn!Z**6WRzf>RSxtkggEm3j5l^|t-MpIN&lsYN5v|`C5{0ZsA{m&X3BWiPV z-rrojj8a@S<>kw~(?L@qB%d1n_uLai z-cJ!b>}pfoRyg?P*rDfnRnE7#jym3TGoSYD9P1{x;yXWAM!H575tJX>OS5fa*7!F= zx0COCQEd}b7uTy>n41=p8CTcT2~J){x()DwFaHpM4o=Zh%$;OgX-BCh6qmsChg2GU zu>nMh--vdEu5~aLHhZ)ntxF0qM-4Mxdy^;gDt8-5YkQ~LbWJZu*a!@Le{E1&cjxJG zjC&B=?q!*3RaT^tw1tQ&jFUbjin-%0Bj|?80rJGDQw&RZo->>)L ztogH)9ZO%={hH~cV=q(pNvl_%5NPlwh{tLyR_m@y9NuZ^a~AYuX>MqC7WjDM<4}!~ z?cvqhgjiQh;CiWFsJZmRTuDYB=}V8^GJfU$PAlZy4-r3IZl??kI-Ci+P8d7N!mH!Q zCM|LVV}BYsl>5QVTZAEUkX;L>oaX zYi|_sx%Qy*x8=e>x4rPMe!4N>?OI}fsYK*69(_)^X_FQ?zu^+hRGs1HhC2`am?HIH zYHTsry+?!N?hlJ6dahrxQLa+GrDU(vie1X#!d_3X8~J^I-{^Mk%#Xu{{l)#Xp23CT~js)y(vAuxn-UIVB7N^|cn`a9o5 z@1^zK@YA}yc}L>CA1~#L_nI%o$^#e;zR}B1Oj;O!4OtGN%`wGkTU^gBWF9uJlvKk? z2ng(xr>Awm)C?~lrv_%~2>3e>B{V11=o_p;&|giz@@oPwT&XNuoeFe+9J)WTxmx64 zw=HE+s%-ZAEp65T*TF}rKxE7XNg$L)i9-!YbqJ3Ga8R4;C<$dhkG?^d~1HdO=* zEJS5@1c>`C-k(_4)_ncArHm<~(TBep%c`#zxVDF>x+y3zoaixSHK(a7W`b%8DEVk7 ztgl(j*!(+az0V;$*4et_g&ca}BxNZN1Zadp9$AhkC<;Ug`~6!j#+C zpmbNY{Z4V}f(LUG$wNuoT8BD!j!JApMYq7_dR5mA-Z1mx6XyKF&$Ti7Mi zJHHB1D-A`#B^_n2R~m}#mR}8wOt8?_M*Y0rP8VU+8N^4>9!?LQe>oo1%P(!6gBz#R zS?O7vzBWc=P7QqQPtQUlM7}Yv!yl1j)cB^Zf1+FW<>}jQkCxFp2}}YTWuiD&krBgR z%qii9bWhti9{*O^{37%0t~dRg#>N9|=eQO0NaLD$-V<@AE%GcP4vLY}%RW=0C>kvb zqi<(V>kB>|_On<^JgIl7v3^o`_399vN%P64it?oouU~*!=1guVECB8SS z_s*NMT*koQ=l6iZz3J}X zk2Tk-JiGQi>St|+o?M@EQLz4$?o5@e!6@<+>tuhO9qcUhn#SN#Sc{d)+?$>vPos;} zqvjl7syXu;KCTf9X0L6Xye#u8Zpt{d`PgY^`Jl~ja6Ts5YzgC?+WNlqwIItW7<*&t zxy(Mn{k%BY1>1>JZX7P)O}%XA(&D3boi|hC!=Jnr-mIzfbWwB8*2S+LvEZC5-gmu; zM`E|0AKfd9Z}~t4-MCtSlU>^L^}qkIeE|Ex{8^lj#e~=Imo>-IL`t0PL%P-y?ZI)B z!)aPkr->^#!J2P2%2nY zpea?-Yi`6xmN)9dLCZk)&Jq&9@tvXV;s;0UP*sLP{$|NmshwF$grWKhAJx4)y(HD# zPSZ=51Tz#qce##bMPwvK2%070WiG@J(Og%%D}y40UPM)DD#xed*YYo%`Q&5*ydr&x7#nHCEZCf% z2PL{c+MTEFZ|nWdN_YLmGt(!dmXp_u*Tt|;cG>xFzLnhD_UrRE5rBW`zidmm_Hqe71 zr#@eWsnX2R4?O1We#VT?h8u-ywwp@*9et^bt3c(pW@*6R+u}+FqU}e&+FZPq_(E}v zH?36Xh{ef>+TbP3Q0lH7l!)&P8fA^Pz4FrL*2-hsb##c zvBdKpE%xiIC8MpG6Hc#V!y2EY;Y^G4r#2vGZk<%4b8JU0o`M5Oy8uWV;uA(RP-^$@%vC)dpSL z8kk$%#_l<3lA6gy&Z#|-UtMC~Gvvce)zW(NyVuow>}>Xp#VvKx-LPv6A~VKq`ky5Q zbjYQYUqU4AfqI1!^wkj;McvpYwH?zmUHpixnQz+LL3(*8TM6|ZhkmiOujkD6_mn3+ zo(annRpT%0zioQ@snO-(M0l<57oWlxoRbWpl@H8Ztv#*pmoEre+>9CmciqweZKN4g z%_QEOs3Frwhb7Jjedom%@@6y6_A9qIm$ySA^H9h92T8-%WJgIp%A1o2hqI`UvHoDp z+qUdl7uc2zPntsTc}1Z4760R?fG4ZYq^FFxb7JK916aRw z-%_6PxG}~xHIss#xS&xM8uYflVfWy3{EtkNAmvlelRUH}lDh(UuK-SC2A0LI`)SwG{ zlW?Exu8P#|?-~n}ASbIw$$Q~i#63s-EjQ7svXHps8R*#hyM$E}rtp5wQ`rgGpHBoj z2@+*9j|i`Q*xW|+XWQ->d~qx9L(s@(ab|IOWQc8oBv=k4qxp_*uB{w#n)?;2+^njb zEZH#St_XXz6-LzB=oG25sm9!#DF6!0(<79A??Zd2mlPZd#|hW3?h;mt&#xwG-lh(> zF#L=a6}>w0cP@No08vpPsVN*i9lY#ZsVSg1A5M^Loh&0r55$DkW^`t2`PMcQL%h@V zvU~r#ziJ!qIV*?-i`9pC5F4o7RbVw%CJ{BP4%Os)_7W6PPbLCc=M<4dF0r(a^mgzZ zm)%SKt{HL`v@5&CGj}Ze>1Tp+NqS#KZAe4=g8BgS4MuI2-^GXdx$Q2n2MviPRY{sri>^j7I=zF;T6Shiiqa4R zW?M4a>H@phGgzVP9qvZY9j+J@JarNue5J0fX_clx_a*XKs;0I;0V9m;ajMF;a*`co zW!PnY@kGiGT+2KnPuC@r)wn2El;rO*@)`{JiKvqdHvnH+#PhqN;2rNH9_L3{yCzL0 zde?{^N{>*l66lntZ?g;P!zSm%v2YzbGZ=DepJoU5Et^mRBziNqD%VXqn~|JlH2!iGyiFCRl|~a z{X?X7V2aXSe)9!0N1UC3+k7}qx#q3W*K!-Nz#b!y#c_w5H0}hZpAP3)EPlLRs_8{~ zODqb?%oxWNaBhUt$PX9mY99(hV&C11;<*!U)xtrUfWpo_@4+QmM6@hE@=tEID{aj6 zofGlCQs+GA)g}2mLZ+Q4(6iN#MdcGmC(PSjb9c8KJBu9|A7gWwoN5T$I{a}E!);^z z!|{cnbNOr;>$Yr@aFrcxP-{oevuzYwcTR=r*{WLaw-S%#r{f>?d7^Z43#UIw+~$8g z>S=i`!5D?jVGMR%@0W+&nVd9qfNoA!ZRpTERDBm)c}>7gwW2r*J2i8cr|fk+oGA6( zNKcdhQcUJ1*DMP*J+GlCdaKF1u#9pd7PZ+eIljWB@($U({MpQLC&=cEV9aRkN+4HQ zC;1NoxB#!0VG}3E^W~>sVd9}zFu0r1=EvW++DzK8OLARrV@L9`j62C1hl5^cwOGK6 z8AHX{b}bGfo8hpV-W#vLJq{lz8+@2O9fXp4GR}7P`jJ&<)+77jim`+CG^%d*8_Tmd zx3<{B1JKvj5I3ar8*?IS;FD8R=}jKv{&#(X2&^KVmo^XC9(K!%FztC#^(hXso<<1g zW7E&DahYm<+a8_*Otr~Y-nG}Pq7@Fl)Evi4+)DEB_;S~ zq9#DrIdOuJ#MqWSPj1xKi-N9#JOJADK&+wNnZ0m%T;mQQx>$_;WxM~lb50)NHORdQ=9S< z=dyF(qFVO~HW@OhI+*dk#=LaB?f5&4jp}`3uui3+<=(*bZT<-D8=}F{gJ4$~qpRj+ z#x5#)8tWGg`p*^{*raWRs?^H9(K|M47CMgPj`p~!mg*O?sU+))J6HDxWNJ%1fl*w^ zbE@r0BZ({1YjMo z6;%62U=$wB%K3vLw<UN>G3*M|YC}W_0UT#cl`%(g`}yUKF^~Eeq9k z7ZQn~up@_vzFzrB_mNx_qQ0w+xXo9NmPibYGWv)?z4RTr@l@Pz-21qGH7Kg7{Y3GU z3um7&9H%6N-WC0pYr^oi=>DGtvoyVJOkgxYFvER?Vw1ay#)_%q2+}=Sw4!m zGNwms&Ud=<%cnFe$~*jQCG6kQDHAPR`1&Gu>;blNX3-n-b>DWR&!bAxqm@ET;YMAi z9c`YtC$5h&B=n&w|KJ0G2_}|;rGY-jh?`0@<=oX|!|hEhzw4ccE`4kIp1h}8o|2p9 z!Y-ncPbar9lzm%J)k3{ZYCG-r!`G7x15YDcIQ>(?tq4NAx1s{AkMD$Fzy9P^+yqC7 z>GZE)k*uZi@p(Onua>Nio~zDQs_!z(lN4QZp?=^4H^9zdn2wjQ!zb+jOtuAn?|R3#=ScC)9j#^7)UL zk@x7BIG=glgCd*I&w10M-o=YapDBxU>8O9!%e+bORFL?!YGgVM0J2IK4NxOJ341hyCUU{ zTBrh+jVh<|NvH3#-#s$xErm2PqYH#d^r^4bx` zl;-n#!Q*?j&zf2nsMbm;|A-=@Xt1Hv_y<+9PHFLYcNKk;OuFbxk8Q8;Yi^I-=f(|( zn|$t=Ttx&^mcLw(l#pBUC=T)@aLLoQ!8D62u5k3qRUcM73!$3+xgN+-Z>lFcP zQyZ#JBdi`6Tlk09(G}Nk&TKwG%BSrt5SH1L&;_e)Es~fMrHBtupBP|CqcqJbFMMCL z?GR(-xS)~RYjLTO7^f&~wRTt6nkzF)+6wDs#;wU8aKce_Ic-IUExVUv_vpZJm-^BK z*51V8mFvBS46S^#9TX{jd!Pxv$UDQ?d*-31>{HuKmyRt@el>-=ISkhgtbH1^I-P(Y z3`JJZ>`)j950rMz581yuVk2*0H5(?T8QGwRUtrX)Gn+#6wW@z6BA@ecW^GhEAWNN9@P3*)fq(DH9vPq78+>_|{$eqR=lFCa<7hbFMt+ z-zS6$keGau{q6SQh-J5*3gpo`IO$MZGh|{OGeuQ&oQ*!_$_Ur`Awn!OTA3EpatLVc)DKpVu$+ICgd= zAS|GVsZv?V*2_9IS~UO#F9`G#_(e1SiTO@O$bs$x_47+)?d$f2bfr?oAo*da?Gga!t z4vwA~xa)j`tG@7zX^D-6WMJde!i4}EnsAz*7rQtRgK@Hq-eK$%9?L}JMRy`F`q)nY z3sR3MZ;-O=lU+MP(bRC^JVZcX0w!FR2#DvZYQ|v3RjM@;aP`f%{#&~=7jwjfY* zK@r@t*LLXAUFsje*}y@}Si*E-c`{K+3U-%$(qCnnBB17A!~m_*jN>42iIpScy?wLn zH0TBkD_O{qIp2c-t0G9`=3caS(G*=G|0>}H)9(@$>p8%?`FBHR*U30ZFOc$Or&*XK zzIe*5;d&ri`GTG6kxP;6vZ`=M%dk$-^~8`OrA}8k6Q^oe4ojP_J{E@K8!3#;HPg!d zb?~6zeSc7MjPg6iq$O?@F6nQciZMkj3fH_jO9Fk^Ze3|-f5Vmp5#e6;i3o?PurR*m z?^1=o$_-`cT=&+F>zUXPGn5Dg!HG(an7uitBOQ;Zi|<8OI|hzDt1}pFXi_x2W`9ZW zbSL?Row9-HhpMjw5+T@-mu?dCEO(vr???vp_x8#OYn|MmD*tk0?fIZa*zE(!h7F?K z1ns?-HNCwjc@6Ko!Ueo4ia9+#uAxb9jz2yP>?$tT!`xiqcwe140M_G}kTvfKo-nHI z^{n{zYWbRI>2uD~8`d|ppT_K)A=Bx_|@1E(Xy!OiBv!B#dxawEw`}X*Q z;FHf%*Ka-JN?$o{ZyVfyx1UijQ{$8EtCYT@;}N@E{YChTtjxvqO!Wg{rM$(%<{f3! z4nt?N+^>|tj=7DjJ0|beS+t@`RMXachZRe0>&~*7&n}>Rm#}~Frp^rs`Ub*UY8z=V zWj)s~GZ(QdX81D8!A#tCV6MZ2Kzd%wyL>s8V@dClPMUhnW@+6uimON0IWvwM@?BqN5(_8s`FYPCjOd^ZF=kEr!b?lUXJ47LdL&Exn zZs^i0)(3g2mhSnhXx)M^u{coi@qDrCRk3Fkw{8~Fa4Su82-iU&OqH5t!Vl$g=uj_( z+d>z2=obZL7q9&oakr`(=hgO+cq|~*Gbl${s?0RgUb6l1Wr#~gYv>RM)f$USHC6o3 zAS5|DO5$m!dICvu$$p|uR!<<-BJ3OE_RkM>#+!i;ZrBX6^|tJ7&sYZ@a}N-B)_dgS zHNb}62O39Tv{MsFi>Vl`tl}=q|DkP$6~5BC-ycM9~OILUlJoCx(O(BHkJh1 zs3gvsb2Hi6>gJmWJYB4`77e|^5B!#Pi*VI<1Rz;ge^p&AENm=^JMi9I!VW59y+Vqz zQH2s{p&W_V`zxLtLx(uXbSK~CXlZ#~0~*dw9{Lq{m8)sLX$6-%%Iq_A;%ew#VSW3D zOFjGPSM__-3XzpZS0*xs!mm(8J)M+$N}~Sw#xoZVYUSKa&D2`o%01`fL+2Tk-re1% zA9B~M*N7?Su&3qadlq85&e)~O0KWBaE>gSVNv@y$}EFEAn1ruO6-t|_@!HnQS~=}wedADR=-q=BNuorpLH*i5Zs2GAXRxP zsBM$)Si4j;KT*@!SA4~p=5Ya+y{eE!@0UQ`Ph%K0VF}%I?YW;#szyrM^4%_V&el^>!PI)QF`1{mXqHFpYPMTRtQbo^eLx^FV9T7 zyr)TNd&_=!zdTGTngc!Pw5j+&a&&Bec(cPm4l+E&*q5_}uF_|E+Fkl)hSkzD@U1XA zSEx6yQ_3vUM{|G1yvWwOfW zEiDevwcY!LmV<|fCe9K#DsqMINV&c)=R=6+C3gDy8>iq;T%ipaFQ|9(`D^R za%N!0UN)&2+LN{#zH53ELw3dHU~Z6KomXRM(T<`@d+}n^Wv@{4PGSUYg8jk9vDYhK zO%oNtQrS>A*oZ&Uu!K_d@n&Yehg54BiNn3(3tAfu>mMyfPlG6}Oq^`SATO>n>x8M; zxZh%SeWOV8@+fPh<5yw7Uu(|J704cZNBA8y2(q@{@Mc`adFzN17dM%@kMG&i%R}(Ehi`URDLQfUuvu7!;VYY;D^#Z;rY@GKd~@8S2!m zLsZ^GsKSG*;wtY8&6;Mg7@8%_Xns@>rF(u6_%2)~qXhO`hRwJVnYA|HQ*kFgdv?z* zzC(T+3f>dkx^vX>bN5R#Y1j-2Z)8>|^ElCJmoU+ilCN6YyfA?ral?4$lh*jDCu=OP zs_(R6H_KVyJo&V#sIo8Pl54Ldw9c%3pY_7m&9(V70hVwDO83CW0g;T&@{t3{{Svs@ z?p>9)VzhG)-m@|+q$NB)4*wnG;_vTpf%fC>Wg2A-eokX!>9VhU3?}}u%G(ZNY(l>X zzc(@r{WzSMw}GbZiyHLtX!Tlb^0anWaK8(TQN=REe;^7GEm#jyjA01zj(A3XR@m8M0QWPcrSW@v?U9ola^*Z^Kz zAgZx%id~--kJYH=S$Xl&I{QC;BD9D4?BBP`a!8`3kt|X=x^lC}`4L2phf%crYRkX^ z?sJma^HGPy{=$K*zO>xE8un6Cx^&-Q^U>PC*UaT@UK!-2^ruGV*vdDGT4jd89y`}1 z>ynf@1CEmglDnO6Mms(H9QP{LtM21t-+(k0y`qxpT2qn2*jQ0n`=2yn)E=X*o0569lUg% zTkl%hIRj~9Jt<@~a@?@6TZwPndlNj>?Z9{O`*_3rh)Q_2f`GLJ0;iuVsk-VY-8=T*szfyBL<=k>pb#cYMiLUHk z$cR&c`Y1n7c2%$z-_*77KkHa|NHu$peX?@=^|dSFigPpLC>-@kjXUfx+gr<-m7m5G zXTa!jU9n@T#kZ$*B%lK&;Nf%WuY{wLSaxS z27eP60tJQrcVj3Ljz)svnLc^fACq5uXX1owV(O@_Xj-&Sn zVvk1PF9^n<&$$-@hMmhN2oehYi|hZUItGeD;41w=jM#I>$Dk1S7z_+X;~y4S_FS|e z0H@Av1%|-zFen5ALH!Sg{U`6CUtVqVC=7|j^E`lI(0Eoupg@}72LTF4K+eqtg7)7{fIZ+qlH(f#C>9bAkQ5KhCu!)Hh=#8LlPLky8rRx|1k%KgyAPD1cn6a!@0?TgyCZ- z=(zyG0p-SL7#xAXo9hfn3<3qlKQSB$q%Gbi0ES;#AaEoKac&$2jKXIa9H-z5r0Jhx zg3k*C7y>zufzkMZK>$S&|2#mY#4lnH1RNk0p6LiU@{j32o%~l65I`luw;jOFoe=?m z=L|#xRSSO;pw{905rGCu$1FNI;~|EeL26?Ee=0dp#rye6A)S zf$YFfRU{ULgyTmBi9(*A46qL0GXQi>#L$3z;;)B>pwB5U8p!iMp84bdf06(I&nY@k zL(aJx4V1`p#sK8T_X6O2@Hu1Pn15HCzv2%;!-2Z-PfY%HAsSFc{Ez@G7Yu*nKm5gy zI|fKTd}A;uH1hm7Ec#rX#-QQ&3j)0YAR7NQ5Wq0_st5&Rz(~A}0Stl9tv}e`-1=9a z2!#MmD&Fb-R5bi*2w24!2OHqe|hx}_MaN^$NvC`#wXmL1{H~y?*N8@ z;)MhXgMks}F@XMf-h#o9_}T}B!C_eZx(-xQI2zxDFf?E!{(|UpT!6yRi2t1K&*1%0OFuqm*EgR4u;~5PH^!h&` zCi}Aq28o8^e%}QNVu9`)Zw3MaLE@zb6u{v4EE$-{2qrA}|>I772<3 z!|(+HxT8Sv?`{Bw#H+ACTp%b6zA=Dso@XNfo+H4YR^i-afVB8VBN69C1BpN&@jZwH zPW*Q`t^bdWNTAf<=ii^36@H9?8`!yA0}2QXKmUO2gJEz_LV=QhZdo)KzfXk%E&~d~ zpB(s?Nf;FVAHV*wCxPJ@6a4(Cn`^dslu4m>}=ZvlV{I2iwS`Ug8#m(Va6(6{^% znSZewAUYmFz)-;Z=O+UV4&F(Cap-fR3t;%Y2cSui|0@~Tzn@3_c|?GJtpPC9xt;=z z#GF%mG~fjM^hBco9^!`+U@*SXHvt}<(=Rk&4ZfzK(J1_m8hDg-zUl%P{%r*q_vhim zOe9Fk!5-=42u0i4I|0urpbqv9K${Lj+5>F}9AOWKz#L_HrT_njSW;8S%2HGK`P=&X Y2l+ZW0e^0d#sEq|O(7_#qNn=*0Ahl7iU0rr delta 32563 zcmV(_K-9m3j1v5c5`eS;0hoVWTXWk+mVQ^2{sSMa+6dD(Gyo^rt<213%2TyFHEZwY zA(~BrBqU)>0t^6JcGcAU_Bq{s`T`Pa(uAGFP97u(Xf#fr%XhwWx_`dDA_-*+qW-f# zthU!zKf@p3M^Q++$Ox5-uDZVZ;rgn%zWUvtUem=xe|;quPuEw!e{+9*MfGEJk#oL~ zOo+vst$F;-8gBpoztvw7uKz9G++Sb)xOnly%_7f|T<|Piyr^y#w}R#glc{9zd%fLl zs%_N_`g)oaGFP`P%hlVVD_1v*v`C7SQ+4m#x_Q9I1zy_sc#V-HrDn)d-@}s(Uon)+ z{cT^B-RkjnQ@@2FvxI*L^Pa=$tm}SNc58iACcGf}>Zb081g@n#OQQ?=JO9|By1aVdGSJh69@)Dlm1y2es zxcjzKzh^~)6R6&oN_OgEo+tWMtF{55t!q08E@_gQ$IA|9!83oBNMbJ5`X*Q$E2&34 zTtO3(<$9jWu54D1>OnJGv-sVE{po-HbbXa7-OyU){y_8}w9+s}gjWxCtRAoJ*eL}$ zP&<_yNz{YBy-3XRuga!r%_W&oT+lnhMYDFQ1@>7e-6B@EO1yd$|5Z59_cgv#j;%a1?o`^%@Brh$JbrWN|)fE2i&A|i>DMkQ9*`$XLI zzW=`&x=&B6#<{Bh8v$Bwwk$f^v7w%4I^y%0j+^bL8fW^eU%Exg($Ba^^6W+W7;pNk z`?nJi{JyL=eWD>VKx`8QU#S?#3WVhIAehMF(s~;>&2tf07B~Jm2#iIArO*P)19YXL zI+K4aF~4pV5Gr*7$uf$mZmFN)Hs|!oG=m%kVTa14waA5o6&gpVcOf!g*O15Xsxzzr zlfoseCS7qr;+Ezq86`OP?OrD@f;gOGlH5W%Kt4RyIuS04q(D|et@}&;7)fk)P%FT{ z`GA8NwqUy(H0@@hFhlg{Vy ztfL>wZomvdWs0bu_g%Z4;gmRudWCUVjv-Pf%u(`0j&BU5nTClmJ-&B_G+_`w-_L(T zs<3!kuSvNqOE9H=)o22w9<=e~9PFlTclzhTlU_Y8uk|VKZWfTf<8N)f)+~*X1v<55 zwJP_$9uX|ol8Vj~>4eB;Oy#Dl%Jm22|By`?2IV)*sJWYKsVv^QF{SdM8$-`ot+jFI z0*6A*k!NhK;pQiBh!0f(sc?!c2uy$c)0%A&BD|ox>DKsE0so9ihWj4 z!2vEO;WLa2|cznI|FAn?*FLzl8VcP<985^-E#+u&2uE93g` zDXlo_7U^LDA|=bDJpYx5Vm+G55{5c^JdFA{eG^Ia-%E?gERmx<-rB1{C~0K^O6wD( zqjAjtRdnjGZ>)qkEs*9$xJ7@xA#N)$HhoQ4(oNeY$t-B=H}%8gfUpoDP}}Qg6tQHk z=r4sIZTVu=s)EQ+HC5khO=GD;MdiV>h6$&{>Rr`!Ml(PPA#SA7A>b06%%cH&@SMGh zvQ$IoIM&w8JrJIA>`NU-z23YS3*WTT#msDc@gd`B2D z%LhNv8&lS^^|c_FW}aU^p32euLG$}|Ra?4VfD_3k9qh;{RQ;-}m!|9j09}u?>#BEk zyYDw25*)}f!T$vwrd5AvfVoi8ltAk(*~cQ zhgT&=TYNAHufpXNLqenO)25n|!d2o$Qbu84fXs|*gO?1ewprJ% z10c1o_L&hLw6iB+!0+1q!y^uhu%I{fE`3oXj<8S)q@6XR2t}v9#Kb}WEq%LrhgE24 zXSe(?Eg9F&@N!P!MtJ@EL>0q%<{VZ(V{keRD%KMi`P+Y~66wTve|Jo(2($aCOx(e9 zK>X3X8s2?NA!O(kC36-ho?ZV1!vpx{7huR+L|aqsE?mgO#Qs!2!5s9hwN`qRi+ZV{ zwTIir`H|dV3I#?GAzFXfKbAWTc)~TPOuf-SJ*i#7uIf}QuGZQRgik%NpN8HnP6>X+63Fz1fxf02DE{dc}WlGFOHu)RgZGn@*QMbrd--wxIt zJNnpIf>8O4jZtCW7xxCzxJELBa{F!7)hp9S0(cai^0Uu(wvul9P(o!^nB3^8j*2R- zxTxsggZZ+6Pnz`Y7K311IY5MHBoJ^dMsC{XwyS?u`>sbwswirfe=>uiM2-xGe=!C# zDn9Y!8~@!|R`IDU#(5KnvZo^kGiy4-1yPwEwt5o8SjceN3r!3H4Brq(4VjfUQ zkVSpk8HZPbe1|drB)WelJaWazq39Rt%0~K)scx^V?QUM8L3tXmzY`sP8kqkCV*kmw9+(W#nZ&Hu<|it?NNp)`+1$LZ=JaoY zBmeZqdluYdi1OzIJ4T|?(tLpcZ6Moe9CISPCGH^VRBOb4X>y1`XV@O*D9-f0oE$}bL{5kYS5wTxrV`i=UX7nXr?bE8>tHsJes38i6A-h?W@xmo1Y;wuB#bihFpJ=A|b z;#-2p+Q*8*r6V@ZsP=n|YR^Xs6}D1G#0yK=*}zoLWSq`WVmY9R*YxPft-Qwx4b6k% zg0NPhVVgyMgpO?Q7Xon3n!cQjM_Us;OJUQn(=2LD`Dtt7ggSow8?8UCcg0&%k)N8} z3_(i~Z?wcLi04LgEfnkh)c;NX9Zef-x09pkdCqUGf zDNGI&l%s4S0~TuEJhBQQe^smaa?+a9R^i)*&$fyaq=D`;hjc}t8GLhNO7-Ii!)SJD zYBR)~k+@C#aiqrr@R>XgAp)R{=cEMB$D9<_pX_IvM|iMHOs7HNl^_jL>TiFa#JC~2 z&u}o>fTBAB4fzN`ooY`I1qB-!#)#E66$@$u8rmnMW0q2znFJjs|1-)hzd0o4RB;Sl zqOl`R6wGJ<&f=`scWblWs{ipTv^`4zVJo9g9V=DrT$x70)Ttlnj7d0cgs8d)tbnKu zZaCQT13GxS8?=Gg(pM{+=4OAs$ZR_znIq!5s^4!+PoynC*)2dsx`=xGoGk#~`UFL{ zFMD<@sJub4kvX#2ym5|(Gu^N1HT*Aov-z&Di8+KI?0Z$|x$QP{HGkD25jH<4gI9YC zyK-9%rXLM#+qJ&V*>b~ayaMuL(9!*=vz1ewg>K6YKN(2y-TdriXyiU#)MKgieQYxcGH$BYkx z02$x#pTP@DP~x zzE^u{4a)EdI)wbCX<~oMSrWG25Z4Pes@ki0+TNEr{)9<-W;n}8)bD(&b7*OcFEbiM zsEpS??_Tuv`y12$pYa2FtG~Mm7_K54N06}3DN9Bz6as=Gat51HH}0uQj`i3<GUdVBht#(k?>#D2fBng*1p|I4K&|Wsjmxb+Rul%7Zuza?r=GqaR zA+4)HZHfE5{bk3;zhwTrm97Fb-s_oOybdgmh3*LT7{|-#pO?R}h*v?4kIa}$8}xxR zS#TiD-kjSa3Ljc+x}HmyX@Q-Zc4PG{x80|@aarWP*nfZWb@u^Hp*EOVc0fB{NS&-4|6i11sbrzM0{#GgOv~EI4pydI{_8PP@r> z6(+!xxdvSy+ErhK+f_7Rc7~yB+x7!?Pe~j9AG-EQ)A`bEKi#%XJG70WVDL@EZG}Ki zmH37bJhFd56%5d*RgUeCX;C$Z<;E1r3+~!eOtrdTu7K?3JUs5p{1^Vnas2(2+1RknJtq4w< zIrc$qjO?8IHD@U?H!lMyn54le9&1|~x1h%Ee~^Cyi|2i{0o*d@xSK4#YwG`lCd2ra zKagtXayfcxyIqh*#ysM8j<8kI%FlfLE&M%=Ws?8qhGmMniS9+>4)kPkhRx3vummF? zF<0MEE{<=1p4x#rQb!g)7Ugqm*#&0FL%p1G`=)%Gx&T+2#w5*5t~w2=Ov{iU zF614!uT8zK2VIW^7iZg)j(2&O+=r>%+~}EJ4c1lR#_Y25J_uCbR6AS(Wqj+!aPb7U z>=rLSLzh%_??92nrGD*KaRC>|kIB$!Ord{36TO-6jiX(SVa@INFndMS?^b=*hfkS} zYr!_OZP{q`0_3JqeY>5L)6$$o6=CJvR9q35R)iF(C$9-C`&=&NH=_yJDNQ(B!Cl+; z_0lv>rQBCI4wc~vyVumwWPVeQI$O>_bbU&Ofn3aF_kc~??VN+QZW$wrGN$~jWf*_6 z%M+sQ=1eAM@g^VLuNLgSH)v0Z3(X5Wc3C%AOJdS*(>F$=#YRUxooc^Co^(u87D@*8g&cQiQi?aj$BZIf;)JFiz{5+MsW(=oaN;qdpl7+TFwBL z@ndC-+vfRrNB+g+NO=0o#CQChG}Xg$PLDH>lgjG20lS;ZR`-uLiab5ms~LX)HD&R1 z=e=`$qm##`Ps8CdxI6Q)`ou9A%Eo1Wrb7UD&Z5~lVQvj zaylf;L3CQGwNlcgKWUxu}cTRwTf=-+l z`X8UB!z|WF@KGakgXLub^2o9<`H}Jf7t;LlH*iKm!_AIIf314CK&Bv4s_NGEaP2~E z*jK^h(xR7szj8}|)&KtsyenRmmtk%K7MC2Y0Sf~#HZivW6!F+i%G%hJM-?F^K-xR-SfW7a|tSr=Xvep@n_4j^(7mg z&CQ8NHYyKsik?@}Rf?#8Ru(3tb0zQpC{;A12;vu8#4nD_5z|WViq7SU=^V#L=de}v z-Fa-~GTEZ}?fiK7tGV0)2G0qci}P>;+;Q$b?i}|ica{4)H_3B+D*q7wFrUXi#y`#P z&dFJsos+X-ePdIL&016IFlJU|8FLE?@=eASIXMN!$Ll4VwaU_eU@WmXYNdLMgE@7^ z?TuAd$SzJgn@|Q%hK%&^64X zXdCEx9@#GkcAwrfVZnUI-(3HKF9DDJ1~+30ekT|NKlp`^8@k)dwzM4*ms09e zWCpSWWgMs7xR44%?U&cR4nj{qgbdo*EnXQ{)qht7X8I3WHLQ!k?# z&@O0|Jl141IyuVYo>4W%Tk5cMluXe{G>uYe((H<2RDtk*Y4)(+#hJ+wbZ3;P)z^47Lk@bVB268rt_^{ptM^%|Q@Cfu3Mc z_OY{Jz$X>}QFgOce;1(Z|TbM0N-UT_KSKv&3zi;jO9 z5reXY;-6zT!^#ClV(ABJTpF9uwL)`v1cqM|mCKrA5Nb#|IR~Txxr(`rS(KhS~>P`#XjEx_`;K=iR== z6gFzci?jm|96Yw~J$tzGundRTU|i7A-P7%t4X0|)m0ltha>Qf;K%EfVNGbF>ndygr zvMhVRBXk5Ibkq<1LGk*Z{)2{btoabrM{qUZDnUE-6aCjOhV>5y;)LN{Z~EGj>|#rbmJDA(kA8&Br`{y8e4IU8nSaED5@O-q%1F>Wkm7SyYrgH`U5n zeRQ)9l;mB?e9FV?PoT+!>6w$Rey{Ik5DvQIBk1yb3^z#loYKa~!0znWS&Ble7-B^` zW66|B6WeIPI!azaoHwq0HjI849AY=$FZz6!e*H&OVKI9Df{|a~nKyA&KRyb7n9rv2 zhdXWK(IvzDg>mKTxO%GMwn0aQltF6BVwSA))lSA=JEGM>$Dwr`8Dvu-1vQ`s|v2I{N&b@9U_A%BYC!%*t>bz9ddfYL3GDl@_QxDBe~y z6v9So!jsGzu?a)slrodoDs@bP5q;8+BRn=o)Y!~i9XcaqW-&BJ$eDCs%}!RcQ$Mv; zN9JAV)N3^4+=b>Ot#deuUHoBgpX7dJLLzkkmGP3g}3AvFgv*HtSGh@@UlVf)!NMe&> zGcsc16VfHI#q>WKfh0CPHe*+OY;JOvBsM=TIVB-GFC{%IGdnqDc0od%BrBJm`NSQg z$3%>~OFaGocGAO7KQn*9qQz0qzp!NKvX@pxuU)r(!^YTMaS4e@DXD3H8JXF+d6N8s zB565~4}2rv#5eOTd@J9^xAPr*C*Q?)^TzVV@E+u`yh*&tyx;Ps@E+nl%$v%a#+%N2 zjAk*1_XO`r-dx^Oyv4jI-t)XAyrsNlycc;d@mBCw@mBNJ@YeCx^EU7{@;33d@V4?j zyeDbLdDZ-x{O^Yq590)XhlWoYZWIcH8-(AATq9T+cF*1S?74TopAxuB{i2vQ~JwPh^1|5lSw9DU(Q~xKm8Wt-PoSq3#c!2tjex7t5rIkO2=%gA(x*~Pq%h71rbK*G*7RcfNt{<09ylpe6HcFfV;$<7r(jw%+qVK zN^+8!^>OPTDO!lgoWGA18njlm0~}yB8O`V-ZV}e5K9G0?uE3j}y$4=7*me%C!sW!H zNsTAk`_I5-M3#}K#pN2AJ`c*E&>**(TwQuM_`wNY4Z`E_8Zo?(5Va{i+f``F093Hf zn93Tmj+$$Kpc^WUt)AUU)^y``)0({Jvf|@6EK6DoXko&MOD?Fi*0SfYO&ECpGM+q|uTz6c$84G&_i)@phLGW{_|NlB z#~oe*h}`)CnVv3pf{Wfdx*{+zyN$o^%%6jQz97KW+;TCwGvg6*50EkF(Q{Fs;*r0D3klX7z@a zb)i*%tS4XGxV?1)M4{yg=(*=0)EH-qlVyWEht+uWR`4UA)o&W_&{$Pc*sd!!OC6=mq>bcpvI59P zAQNw9T+VBinV?1PSM4o>mr-_6d}21~^QP~VeEg+3XtCH_e=sR=hT>tJOztX`L z*B05L>z)agSo8d`yP+Ry0Y8Q#aMV|?p?bHt(q2Ocq8%)T8jVsX*X)D>P=U;jBDfS; z0AFdtR|5Qf=W)k*0k@6QiO)+hJB6@hCg~*787)L`6Hmm`aSxU-

>OTz#(YTF<3_ z;NkA$bY2eIURt|VxjAntt4I^ewinDzh)Q0Xur&ryYC+2<`)ntgzMy@&R_-5|S;z0= z6aqYed&PSvy+USGNviT)5Cjwuxr{~|n8B8k#NDOygSa4#4_hp)LImna_ zy^(EK+trOr(dVR*w2+{%qC%~Pa#ZYptEj4Sx?K(?490XnUNJcH+~UiEcCtvUtDrNi zN2TtHYQLw(Y+|g=HatFvd3AAZ*@q}hM`AI}aN2jv`xiel>0uI)!QycwLHt6=HK)Z| zXZEtqc(|)8(6j%_kw6GgcU$I?^_gUN_Et7^#kRBrpoLss;pccK`1lYvQjF(+i@aUX z(NF+IENK@NLOkqzIW;M38>o>16ds4k;;=D?-|nYFiLQ&Lk*h*&g}MN=NM9qOY?SoL>hq7x0kkG(Q(5?U zr^#kDv6Xw;EH-F`)`itO+vc}_(b?010rW~GBE`fdl*tAOS#49>>{h$Q!eA+O3EL)n z;v3d^GXh&aq|+Td>b2@^a=Ae(*RhJc+>#>L3`?;l|81IZV*WwACd^+||*SM6R( zMiAbzg)v>Z79AU%nzjzMqZj*EeTVNmexuT+v8XjVtxnIBN%9g2C7o4sD=&34_nmHK z+r8p?hu>HYjf2oGRp|{0R0JxZ$V!QS63O)ARVVOAC-_I2I8Uvg`uC44SxK8+;@DuJRrb3jpFmU zd*V|IbF;GRa@sv!i<3rdG8&D5j7CG*qU6=7sqF1us;pY8``X)hBn3}Ryr1i+<6q~n zVBjfEBlgfPgB!UOPMJ;*s&eMmtHdXiX_OjTt_p|7twCJ)idRKp2FUGny4@;kg^j%x zz((P}oQI3VZmYw83Lfw%tuiaR^(yuW%k4A$NJi9Fd}1%f)yLzTQTz(`*eiyz>FPhdP>XKM~+3-Vy)Q zi8!H##RDSzI39&ZeQ|lsiAUV*H?`khg+HOI%g>R~4Ea!0H1x$ZWZe_%5%6Pv7NJDpG?xGEHSwOY@-NTwz( zBMa#P5B=N$Z{Q~3m!kKeAXfzysti`IG3df()uMJf%+^W^(~rxAHmcb4v0&1-(YflKXz*b$_TH zS0$QoeOA|=p45H81j80Jhnb{fdsVwn?W!CH9>p8{I3Sx>G>4~J(wTDWg%{V z%CE)p94sIs@Z1Bv&dM(KNL{VJrp}q$l;{FvHJOd9$>iE?^`qLig_de-wWZqKYc%y6 zk=1RiwQDR&RszvF38cfb=5)YKqbDmWXl4!w7+XMJ&o=3-Iy$Ke*$#PP78yqFktG9q zbW%T_5pv;q-{O1N*WUR2^q0Rl5|?Rzr_O|M2b~HF_qEvBWpZ7ia_FG!BLf|q1yQ;z z$b{$3nJ}<$^kk*%XK6yOD@Ut|PDoCOPT~rov&-zd{C__sJW^!*t&ShMBvssAqna<7 zoBaWUKM>ISCpf~)sDPrxEU2-WtVSFA1`Z1G2~jM0S~6W*Do-mitOQj0D}Nk+G4Rn4 zD{wY$s@P!GhKI~p<8wO@j=~d!pI+EwX*D~HE+f<+i_WfO@*!832T2fbP8!TcMH`~B z>g)zKpm%EM4kOKws5R);c+z(bUlraiX(Oc&r_!YUw_>Quf018)T8tkd`%n4Uz5mF^ zZVONi_Z{{2d5hQ zXK5#e_<`F*spH-hyLxIu*UZT3G1gLoDrZw6S(geakZevJj9*K0Omn%y@w)tcN0EK z!=FmE@HoC8#tTGv5@x@_!{1(hmE6mcxBnBX|KF-Ugd#ki>-|9sJ`-K<%U%*+_+)$% zyJg2}5?hfv6Vq1gRRcm${+rkUjB`kocDJ4td z>>0KVfQe1+bheU9AAkljC4^Hg-uF7c@_A%nQ0P@EJ(IhCD5jV;HB}YZ6SBQ( zX=6=38ixnj)jst|LX^ zZNRFvS&c@YhdJDTFWkT8jj|I|CLW+R=YBlyLP|%ekCoJyS{|>@wBi((_fX_SsTx zyf%k5X!RB0JBM}0sEJn=A~r5g^sZ-O@W0rqq5e&PR1A=I*1wFKqQ5h~)hku};PRTh*& zDIyU!U-%Z^g~wqbzOS9u|60C(U?Lq{#GMx(erKP#+vG9Qb;*bvR0)|J$kb&6gZf%I6rj@5e8YHh>Q?Deu1Q#3?>*>$a}RMY6Bnb~B`q>arA4OV36!tH zqhEF0sK_<5zrXc&p}Eka^U@kxtPU?lZ{yGtxSmS_ZX_2WmUd?bcTlj7B;&}#xk`4eFZw9zP_rhy32by3{eH>==xcvV~SstM(+ZYt!t_am>jft?tLbg zb2sXL!jVFIGc^+yR9)dJ&MVE&*HORc5o@HNFD>4=epg8rpe<#`_8e)WcIO})I@#OZ z1L$|YdDI!I4H`CrTQnFTPTa>obPCHZ3$Suvp*Y-L$zr8Ghfx}229P3}W92I*m0YDr z(G)QA$nS*}TeKyRjHdUkyh>+eEY*nL-rRV9;hF8bGSf4d!UbYm08CEz;otREHUa7i zX1o-gN=8T%*wkg)li~rTqz13nLT%Mq8p89k0PeWaGx(e`lQLN(H%?qawXdwKq*PxF zDwJ0vt8EE3^c;S<`*|{f+#h~+Is3%?Z}8-Izw_ACcIxEyN;NZoD&f@N3Z(`F>l8)XOZGXeg=%ecB-fLG%ZF|}=`BmRr6)|22v2NL!! zAp-K~BP43d$@yRW!VR8PyxZn6hAL09wt#pKp8j<>$3wx)l*!}?*hMocBe8+n8(ek> zPx-JW!0-DQzwxnv6L7y3zb~qD4Q^w9#q58H{8%Kk_M6>}%um>HAaC!no|C(4n6|U^c#JXp+$)<#=Xvk_05>VXzj9f?rEz0_#70Wo zU>}5$JX@8dWu)E7O>q>dB8t>V^4qDWqc5L4bja;ujRs-C;}yH8*H@%Wod`vcYRq!B zI^9iBjjCj|+4*VGxLw_apW!<%zjLaRDZ-n?>KsXKeo=umU7AVZSbDVQl@>fI_$nJb zyuW83p!2?`DHp2^S~dcIJ_N^qdp_h}JGK9m0Cx`v#dT#>lI-l9>>^)rLw##~E3@#{ zXtAdSOs=4#&gz3&)SK45Wkv#-qL91jRimlO$^<{{Y3%^ysD`uxRe@H{Dsy%aR1zc4 zDNm*I{c=b0E1!1bDbB$u16}FhqwH0isZ6U}^^G=P{b}0A$7rQoA8_V>!GOv?#+hdY z+(a5tZCQ1mBtw!>=qsrY2AhHm+5Y#Z#6=6Ytz8FdN=H&>tDRz^Zm=M^nFUF4J^8O( z{G{*8M&@H~n9y2B_05d>V>`D@S$jKbr_osJU>Z*!Jbet1uSOdy(aE&oC+5`@w5LAu z42~$?|N05)Lwf$xh%&l=LNevn6`^);*+Y^#jniA{^w=1yvlp+lHFoI!SOUvIMK>S0 zzJdyn3`O_E9c>L(bqAQn1MXx0L_LLzC7Y?~C@Ob%Ra@#URjj3&!qf%7ThTJt9ja+- zt8aLv@8JH!V56#GGI;cKvs5FK0SqSnHk~3KDo}~LC`f_4r&ZE_z9Vb9@|h?mB_Td8 zp%g{@ZP*Yy4valjc}{TSq*zy~mVgFHeTqs?jib)a7)_o-wnh~ANN5Y#0@iv$ky2AV0_2B@k7o%W^W%JjroA~yHk?Z z#u8ECMpluhrQ(8rUhYgjL}Bod;~y|6-I(_L`r9yYHaG)p?a_VIN%f=O#qE3Uxy?H_ zCNc)Et|O}<*Pmw1h1sz6rDBPuKelxTY=@$Fg;bhc9!*t!2#Usljj6s=_evL_s!C-- zflgMwi8gfz=6w9O|99dmx01U{VpxU55bog5LA;@#zn}wB(N}T z84B|uAC);v1A&I>J-sn|7n1uDr|f+8YH5p_IVwLYgY_s!@)Q|ewgCDh%x+C%D>S3} z5>G)+M!}A?{c-Q(xqI-K-map?3J;UroN3+ZOmf88p%=9@oW9X`L=|7jMBu+u;N2g> zQFZ)(b7uv37geNBe^4YTJ4e)oCsA^;4eEd{%aE*K;>jH0jPN6nq6%u$*c+lK(yc9~ ze6wM9!fSu&4?|7~T7^L;(=aiUH|C`PDv*2I8%%afHBI-zZJ_hcxhb1}eO&C`)tR&Z zmyAx?x}v4ALk9#rha8=3Gv*1+m9E{EN^8A;Yc~z7hE_WmsEUmSZQL`9 z0d11^b{}v4ebWWj)B2+%Oi%nLNof3FclT~U&MHG%o-9*c$|g=NSP5Iv^b5JKo$u-m zR8!YjbUR-DIoBzC@23JTnM2~&a;l`cc{%yzR<&Ek_zS%`kc47a5h)qDS<-p*c<@Sp z=sIJs{v|1D`D%ZC%a9c1QgM~CI|(Y^4l#5cx>0fv&+o_Y9;LT_Ll*FUh-1SbZTT3# z{;>dmfRBl7P4ypN1S>RvzdTD*mAPltC^c;=$rL0NbD5+p_&u?&1X`Q^5h;zgD zb(l>~6Wj6K`9>;%wVjGJ>BY+uNhDi;vNAb#Csim36nGo00Y61hFyB#{k(-mY{Yc?~ z^IaEhX2z4)6@LoQ*Zo-B7;cS1uT|;U)X1fIX@KHO+Bzs9Q4boyl~Z-xcVpjA8q5`Q zcZw}O>PYQ_osyTROBIY>qfFOIRXM6`bvD{TmI<|`F)u6!v{`nb`(X8%jvH)$)m{s= z*FV>@pU8NwJV#Z;#!Zy2g_qIeXERRj>8NgQX395JY>nHPlai3RoqEO{=Hfk7;02$@ z<#c&zKSJ3Sxg@n@>y`tFXTJXWCKfi+QtLRc|3uHpIzHFIeJn03PtBr$mb>IGr`2w= zGM>u%<^ut{#T9wB0F|lBl^RD{RRK#r5*16Ku&@Rw*7E~g zl-upa837TAb&p_14S&kY<9$DRBs2T_QB3alcQ8}FXR=0*{vUV_Am^9S{{t2dGB_YG zAa7!74GK3fF*CPe&jarVe|>CQ)fK?)*bWy+&Dvl(5%Qi_#@33^1{idq6n5`V;gPGZ+i;`rO=z1WVw;_r_*ZX29!O_SD5OM#$JB(@=q4OY4qZPLp2 z2bzYuU56Jbd-jHQuI{3W+~=3SyjWG}JZoy0W271lfRy-5bPTezrk0KEFX2?h`fhc>L!3s=8$} zr+M2sRexnm)o}l}c=dcfvO2@lnby`Pceb`Z(V@{Ab;=X{lyv*?9n#0!+IF`{pJ;7u zleViAI^}V>TG}P2fBF?FImJx|q=z-fl?uuz-M+VFdEE8VA2Q_`QxRSIb>qn$f=RoVBa8^682wPxwisI&%3p_6uLdKEhL z@qVR3t5*(a)ZDVW$ZdOGkSo~ z%+j-P8j9Z2e=ynbaPf@0*c8aX>7)e)^)_GzNj+nyAqoLtd@&?myTi&$mFp$`7i)V3 zYmUmdCDDk_2SF5>2#wp^?lB9|+0DMnc8T=Y`abJ>-!!XQW(9zrQ5`l~65vlT{@^4T zotq0M0eyrwv&%M*$76SpY@TIAR;$|qPBb2xh)nq=e?t-C_UHH~_=lp|?qcU+XXfPD zSFjM!jk%R{%nXiG9@m(Qv<(fKbb$7=oAGjxrs-gi6t6vP_yD(+LM1HvfPedfe@TF~ zSSu-?nuB>j=Y9i=b28tnDuvs8jC6QB;05GS#7pmD(V4F@mqBxtoVGLGAfQw-nM#iP zt$uPKe<@2J0K`7XHh1k-C#iy&JkU$M1bt}#$NRDL>Pj%PNUWZoS%L@(PfXcuZl}#j zs9*oN^?QK&*zNGy{F{sK&XRa{R$_6RUk5pxue}YmCypdO*i^qN82qAt*sDq1@FD~-& z-Cqw2)^=4Mk+}VCKQO=)60s28^RH_QmvVElh4>N^rQ-lah*=pojg&4m7y!LMi-xGl z;U=SF)a(Uw%1h?F-~bocChQXvV^$B0+t9jZ$rUx}AwI?+>bGCHm>{()Yosv|enY^wM2VpuQJH+{e>hrhX+3!4SU=&sxhL5N==*B+F;6WECNS+IOn%jA(GJ(&>*B#DnVB3ho~h2rbaqu zvYJ2*TBF*mN9=#YgHgVEw^_RckU|L+YM0(aw_mfjr{6I1TNB2XbXN%CK@~_%60l0> z3ai=zL9m0(=0j-%3Uz{^6Wq7{gs)xaF}?T^LI0Qg@vp&$0xHngf>EZWs@Ck;ko}4| zWV&SX)O_>Y+cN;MGuTJiDQw1^OV47||EI%8&d^OOPO5)80G&%7kNL@8l_rDEMAr(7 zbt1<{U zKb^pL6TSpCCAiGBtGt0!=Az)!Whb9vr%Y$(PM1*Zynl@4o3viN6FlIySe@t+j`CwW zj%9sJ3Y&j{pS+8IdtQ8DYZraI^PRKsF=Dr|iv=}Ct)UdEq1>Xidz}f32S|O)K?B0S z!W#sTS+-<-L8Y_OwHZ*sYo>fjr{QFGhr`oJcT_awz%Im2o5^z6w5416KJr?;RuAXr?26nJn3FdZ!J207{1U`SC%?2*y(Yoq2CSzS4#p+oLKMRko zZz;M^{zi85e*#)1-cqX!fIVP!xU95)Z@V`Hd*RUhU`b1+LwS@HAlAo*`PzD;33N!~ z*0^0Zo7+Rhq9;zrV(8De`3<3-o?t_GTh|i@)^xpe-P8=|Qpc(AP#aYyz1B#pMdI2j z*aCm^u}XR!r7=nQX}n^nzG3l7wDKs%tl=V5=F(4JMB1@djQ)K?RM zI68f&`)hCd1PHVRM}A)?jJ(May*)g^AkLr-ync3>b1|WB`X?1kF;*BGx*6(JnpUXz8!nY z%ZiJd%Jxys4Gos`wD0eKF2;Np`>)g3wUsP&?4zcesyV>oR}| zP;FgZZH-^&G0@Bvwtet@w*7}~P_3^nXmNnkPo;gokZ=P|at984$-^&yD9{v|G-RTy zRKtaRby$>J_qM>$-3Um7q)Z15l2XzLlG5Fv#1MiaAqYBjcPQPWC@F#b+3ERGc!beRR0{oB;FN`ro=6*jcqvv5XfTtHIivV zH==@~LhrH`@OM}fKFucy^*Bwo<+{>U_$wGDeXYU)_r}^_byhmpa!`k7C?iYXttm)+ zzUIzq!)D)LifM-3+msJtfj5b;T&5CUY_l%a14WNZjm4KHj!+-je&Hgj9pfe`0%*7f zb-K;vP72mui%g5T4(_Kw8m2E`Axy1Zfp8MZ$>U!r@kcu>%51{R@1)?nIc}E~+dzBa z-F&sFX5_8Tt}!sDSmiFJ{C#!_lB)zFnN3<^6*JCPaUN+BLjGx8av@Zbhu=Usej8FJ z&CkLnykZukFG*Ufjq(*5qhjL|3klrlNy`_PldnKGA!EcO%>yJXHD=;iZR*u;%yPfp zv3mZn^!_OxMyZ@^{&hr;*-vl2>6`Ql%E9TOZ2(X)r{$ zx#xs8FNUXEMyfR9l7)@1wuu6Pu(*$AYa>I_S5Q71pFBTrLuG8Cs2nym!IFT{k> zA=QQ?O2~Lt$czSu9$HryV2h1wB3M7nog8gZDVO+C<@5&ZSX==!wrHyKiW*5=dsX0; z$KdrYC!7ZDq<*eQhq~o@R}#axQO~2N6iRACmj%}rpuXu(h;xdDW@yXCD81t_S0$J; zUoSOuUxx}Hm~AyxR9dy=uE*t)59{ieUo02DK%bSt8w5>yOUM!@y?}LZPlR_d1Y|o_TI@Qz@m}Q^3n}TXFeqGwCTZ8CDyU-bY1toxD=QDsC`WpzBtg;`mlA7jiu@KjC(9=o`#!)v zG~e<{WdNItLIex;YDo3z{6xZK4KZ!A#^j3Ghqx5#vZ}X%Z9O+%&8g1J^h;TOe`%?w zX0OGW)EfIrWpNf9WI; z<_vF{T{Ze8J@U(S$?wao)cFUpjj`1WmA(o@KHYPt6H91jgCGX3Xzp(XZ_|SL-+!Xz z-bsso9Tj=+@r(Bp8rVBrwx>Y#sc~Z+e{78PNd?oqO-@)DuTHxCDCmY`$3-ueb>TeF zjp`|$_xcqRVpi;;smM8&fQuH@4V6Q|{q$<1^4r)y@To zB$Sc(u#KI*KM7sp5x?n*4!EhY$h_zM$U)>$*v}UR2Lv69g`Sbaw{le-q0aE}2bguX zGQx(s)dO?+$%jOJx`H}%MEiRABBRyxF6JTNzNV}8xRK<( zBIzw(%?TIe!)*CGSPSII!e&3!={5_8FKrm-?Xpwt>1;aA7h~Wzy4!2Bl8kc0mms8kDW?6jP?AW|>>5Hx+4zp4LH8Pha z4a9@9!P*$ZpR~ko8eRo0d;-ik^=Rp%S2`WDM;;$^1tk%m$c^RMV}}pdszLnfUYj2l zAsbXy*0d2s;x8|x8XFt43#*vh^i_iRX=`ZfQzpyrcRu^{esr#6IJCiy>)9o9F&36@ zuLk-0=LoKtKYWVq*>s8Fad}MDKcJ`3vek4*l@qwOJjG*lubHxcF`a2Ua(!a(Zte%O zuth^p4z738n%rT}B&TI>-(DFP;t7Z|^jHS#*UnR3;_@%v5vBdeHc!cJ=$+isP-RG8 z=H%+B*`Vk4KJT*i)h|YN1=f2QB5!nepKvw=f!t(H(u6vKHtX8SI#vC zF{$_qEd;5vVK0uze&E)c&$@B_c;F7}x9{KEiRwWtl@baW%itixZAZ8ec`;-nBcJdc zNf(x?fxTM8v7&TRjYM+$htcgD+GV{@?luz_cwe+{b#c^(}BO>-+UgnS-4tfevpyIf-8+vHhX=ey6eB21R+kO*d|pRf4APFrdrFgvdC z{H|TXmzds|aBQCf{h6)S19^-siFs;aIsB4M$PiA7iUAe&N| zs;k3Ayul)_`31u_yhf@=R8osLXxQ4qhqSW4Y)$cXnOz;|284)NY|T$Bx6Fq0Ixg^A zr-HaXyUxWYec#ifFB(62^O_~rxo2u9f?<++$^M<~O`9L8FDT_>H?A*s)7HLAPj$Eu zY9WFS{H*MRmCVce_IAbBZtRL>iQr7r)6R!krWGDR8^*XEoxD`Ti?@!p#xn;%tZzE+ z;^;L@2Z|_O`MqOSmMR+k8NMIBvnVb0nPak*FTl^+vP!0`z-%cYX5SF>_E~dU$MQkd%L=xuYL7?7{^*T4*44O z^k2&_ua)3(qui{I;Uy`J-%=usA?CM!Zt!F)O(m#PLGlS}#_NYYtxu{*8`$TZWpY~{ z9E1m`#jd$1lm_^FX4j@<>z`m#WS#(dN3G% zG|%T37`TB=c=FV4JLPeMD!+yB9HR^=lBw)OZ=uP=gY!{K$@|lb-rBia*%F@SoI|{%9JpEWDIGUwH0TK9b~dh&{T_dEwoRH3wX>c6!Jl-g%kR@AyjkQ~g+cTATWF4!y18uBClq#Y#v0;;$=gv-l2?9SN3Q@8x0xNdg^HsQ^R# z7NvZFgOY${P~oMkB)#rcOzpH(S`O`d?lz2Fylyns;D_&48)E04%x%?UEQC9J35;R#z`*MI$VA| zm%w~u=ho}U&)v6WR=gS-r8tkILoX`^jL1G8)qXm(+nJcSH@h2lr!Y!x*=DlK5{CicKYy~lcjZjevFNU`m?U`Zc1-iA z&wgxRfkt@Min3+SqUv$`lg`_mbY>eDh0}#Czmt9;a=z=Bnx1-3f7;o8E`vgmty*U~ zC`p0NBd#{nE0YX6tavHq(Gr!YyH%(s^UFHUR3#{_&3BG{WoL00aTO)~7w1z$iySsE z{UR9C82g*&4eKDeIIbB-Yxade2J$62;qJ}A$5U)}btP@2kS;f5ZDn_kudRzI)=qsSQlibQWWvPAamVJD={c4lACNdJN8i#x>J6gl z*3AG;3k(BhH?e*jD;GW1&C-x6me?+^H1dEfKDt}K&!rPs4!S91O8_l=O`_TnjuYKfxcLO~_lp<}Vdgzyczo8qrOsYjBH zC&(zTicKePK3Pkpzt&o--NAbOmC5VCA8(#}Z&+VRLe}#)A`dCp zL73vXQ-b7uiP*oO&i3D@Z!q{D1%mjyKth;6x*(=dEyh5$&aYjwu}d%S8>FnwuEj^< zKC*#Wu<~VTO_61Voq3d^d{N9IW(vi0Lxz!x*Fg{2{ArjkWO~QhxHv5Ig_&T}zPTKq zY%PY)$%kzo$!uO`pcjo4(C{}tU>1MByjUD_D0;}Kl%xI1*AS{Z0OMb#n`$KZ|9nWUseEVDfo?~j(oQ7hUbj(+er8&wSaNqwOgG53u8uI7ImYX< zt0)#S;*u`E`k+t8LBl0APn9i*!)(nR+))^>pq zllwvES3b1-vEJeMs5Jp-ae{zBP`)tI4jh%)@_2ug)T{D&WPUVoIV z7tP4xm)?`SUvO*dM@lc96@SI9Rbj>l3!Sj+5)n=Q+G&n&Mj+eThd#82ra5W@G>6a$ z7)00Bb}kuRK|H&8nYN=SYg}z0x-9;3lwTBWh&$4YJcy2ZlzP72?D_J-79E%E2jdzu zvrlQ^Osef&UtFW!-{^oo|3q6CR(C4$<<^w}>eWl6>PulQYdTv!S@q|i+g_Y!G?TE# zO8W3!m$}eaTq1t-b0t(QWJ5b*S=Qp~;joqGg-zl;d#uB)E5jA; zw+J?S+WEx-qe!)?s>pM@yuZ*Cj9izuwX|@)$o)*IDv4dT@rE`_DKnWbYYOA7|#|1bZcfmYwfrDluMkWV^q) zy1Lu+bLN6XPh-f$;mnWO=awxtx}&W~cS)9}D?)E#T;lqOj`r$vM0KOTg5jZ8xfRBU zwpDuuxAd;aMaX?7Onb1C#!^({NGMoMt-krB;;}r}n?A}d@eXQk6-c^zwC!ACVY<_FB=&nzJl2!4 zvv$V`+1cYBUa(iUGn`nV3GVJ}xwSdkGrTR~-l1DD+GW;Hl-=6zGTC&akRdHl!1ic_ zHFPmMFM)zf73-T&J+fRMX&&_K?k~1ARo=Alp$~oErK9(^8pcRiDrwnov)wUyk1Tl0 zf9EOu{X1BQq4F165WT+cg30ZIgKee}J2|;-Zo|rl4|3`C)lO-%=@rud>ijfF_B(yVA`3&y`@V2}%Qy`%C_U<|94y7o_75fs_(st|O z2g5y~h^CNl!=Hy=KV8Y$$@M+;{g%{SBoiqx@M8P*)`urt*PebmJnBi$X7^yqVBLVdYA} zX|oc`f*x+4QLI$4VXqU1iZ9EAOJfD;X8Rj!Fq7sNM9&rfq07E2u~bm^>echAFUx*t zH9EEG=QGO+mOCnAPUBW=zu&&y&(-=^E%k?J_9MMGW3kHfjY{RVOh!_zS)Tx8J2lsXej^w0%3=SC@%Yqo2RN3Y(agF3R!ZntdEI@NV#Va( z@&}Hj=P?Fvgd2V^JXEb57qPolMQZMno<9g zUe=uOn7-bMU5c(o%rJrSg$VKmWs7jT$zf0hk^#E&Li~25=LMw)F4bjzP)tpdwToXD zJnBc+rk4qb-WBYwdY$p{viQZSZk_@DcZ<;-3mxin%sLV)ABtXScxt!3ws^VmIp;I; zHq8#@q4~j+?`q}HFMeSvowBD+6|C$jixbDmm%SbC?#ipph&#oP{|mk7y8O|KKs=_T#& zlJDXi?12y4bKVn31RX842z*(|w|64RNW3yal%z`7qD*#l^YdqKF0N0{LxMQ6$ZsBW z=-yQ-6eGUzb860e?Q0Xmy4cqB$-zlU(5M3XoK$%k7GdksjJ{4I70TxCn_yf@Z5koy z^tH)g-DbRJqwZz|?bT6r0d{Xtf{l$7&Fpn#8glXb7sYz8>}%Ke_k)GB>xREtVmxBO0<))XSD)XE*M$0!& z5??}jY<%$aD0s%6_*Ujt zaq>)$*+sZb=?W>Hz#WBe9>3Dg8pmi2I0{yXy1Fj;d=;H9(aPrG+zARk*&W7a%h0yo zkvfr+B#TIzUDy2Z-hdIlav>BlvBSQryifW0M^xjp%0ku5poCV$+RzA1 zwQkX+UJbW+qQE*eVxrevOOIm=m`kTS!oPqwFwo?PA>Rv}m{bf=y?yo<~LY26680IY2=t4v~%H zvV>Tw7uM$z65x-<)=j?Y?aTVFmea82X+3vy-)=c_e<6?LESoBq+jd(SQ*14ro!}y* zpC`Y`f0A@m`s{hfQ)xoWbGC+T%G$$-R#@xJO|bJIs9Tjyjh! zN)l!&UCKwzgL-4Wb{xkymoKyu=RJf5Mp&bQQLVTY&(y zxeblad9Fi~k5>{|?>#F>jBq(5zVy81L42-Z^0NQGHf|Ou5#RpyK7U zjZ0(ZYnofU`rf1Db4q0kO@Ym7W(4nIXj#38&2NuL-(p3LFx2=(c+B7bDJ^XH;vTUV zD=oi6>*P807k0~hQxYvqQd?IxeSdyg-Ce|P-Fmrwm7(_Y$0U^jxaW%lySbz{&5|je zJYByyDi>^xb_`O_(QFAB*SO_ed``prA@f((1l8`uWXy`-)aJs(3iEaT%+7QjY~tQ_ zUr8-a=(hh|lQgLa4_Oi%*NvIPd{~$ zmb*;e@RV87@)zpk1uAsNhWo9`R*f?EfT?M7^P*d&6jh*yva8?dP2~ugYd968i5(xk zlrg+*so;KB@m;;{DZ5W+bO($`k;AKjZN^Q)@1gO62hsS6Zq^BnPFL{?=725hr#F3D zs1EbOuo$CU?Xt~zGcsWfx!}_8B>wBo>k!47!IV!P;|!4I zDfb~Hd-_{RzN&E7jrv>e;ZSq&Wh!6owAQu27MmL*^aK{qSt$YxqQybvK@6Ky>2yAm zY>$~gubUBCeNGs4fZvzzy>!4XZ!jEUOCIp`oY+fd?O$@FH1&mqNg-RZ>M?{|&$vNb zmL#uL7O0mz*b(0q5oIYJl}6x8+3m9%UgxBpC?je1&-Za4Mib;jR?u$g^Wx-LH ztJvOz=@j>193~JWsPP@P^}q(8=Rl{ZEn+?&l7jB z9wubX35Xx}cmICPryo*uug1IVQa-oa431wMB%;vZpCAz$TuK+}Z-0J*%QwcX?>*d_ zfyISHUvo=Uj{jAuXNDmQ&)rJm!`-?{)Tdx*=bEz#CBYi!T)TKjI6D z0NzzoBMz!2!=7i$HxztusRl;-{SKkCnsQN$lX^6rt&srRb++maN_RUce<@QjfhJJd zcd#{x!+F7z@Jnx6e`0oTc0{rHOALbh}ZX4(r}=)s<{!h5FOg`@8}w!{q0x zrmgZm=V@GZeDT)Mh-{to94T*Zj@k7GMJXN{E?XkCMeM*A+LZCGDqZZD8yhN9dC*a2 z(CZ?=c9##UKzRd`mp%yoViHMTC8&2<&2-GxQ6@*3?-NbGcXI(vwm+g!S(&m>44wF{ z9eum)VOb3J5{X^>J*GxsaF`1SrrCw-2(BHET;*{kdSg$$$6Gg$KqhA$2r*+ zK{}5PXq&ADoAqDbFd+2Z^!H9DUF1#wq-HW!PkDbCTYsN8c+NVJdb%_JGqrkq;O;YN z<52gujFM-1TGC|HTMfw@h4xiAS$j-Cl!asQvuP)ZC8v{V7o>`i!RK@>vlba>TI=N? z<9EMKP|QP}$t2Dk#Qv`bL_;3)S`$7z|-Iv++f32F&abfF&zZr>CzIjA$lHfDOToNty(&0#6 z?3Cc+jnDFb;iF+!QEVtp=@IkZoQh!KqmHcf8xE} zH%jgFD$QG5$JW(MQYMhR_23vcT0gU8*0qHPSNLDt>Sd!IO{!CPf+bsS)bB&IbW))7 zCG{Km>6#S|8QgvzetY)u82Upj`_uA~14)}&LE*82!EN3>dqx=jo<~(c?$M7L z6yImiBL-qs{Byzi(kiWs>ux?VO02;?y5N^lo===t^bgcpoWjjB-aKf5rss`)xYx1D zf70m`@3{0eL51;iVJOxw@~hQ(EiK*Nm6Dsjdk=0fmuzc#e!F;?kvuAClLPg;TAnI>JYhI4AU=EGy|#RtG{ zgfHGJj@uix_VZGX9kIL=;O%zr^v3Z~e(9WAg#5c_KO&h=Wsf{uu!~CKKQ&gS!fZz5 zNA@v-yJN~nODVqFZZpT(Or{=+1RdU|Pq?{8`#8yv!VX8*(t6I@Sgm(>-l=|*C;l{x zt)TEFQQ=GaU$Dkdajn*kJ6J5Cy>+DO0h=i7ot8DCvFV9j*VZRXlxuz#rXkH={Cv7s zYnpt{Op$NBj^*ogE%MV%!8Zgqm9O9Vt0<_^(EpGu3WaEXA`g-!7VTmuCyvuI@uyF` z>1D7Vb#qy&Rm6?!&G2E)l$Yj32aGnmvLC$#NM-*mjztB;iwms8@sXSJ>FP8X3Zr(WAzJPm^`qy{g%kba38^`uOF?=NEEFbegWU(-r76 zB2N6Iy~lN5@9rtXR?&&#Og(lxVjlY{xS83_gq|MdAaMaNS;dQiHeOzNxUYfjq!``X zy0@bugjXoZc(HN}bp1CTv@=r1+*Dk=_4qc3S8jX)ccu7xM1QK-BewQ0>r47Jyxp_Q zr3c+``B&6^1%!cObe~#@z_^qKMXp^(8a_{P23?Af$ekY5L*>-Paj?>Czw%yWQ@Kwl zRX{v#ZuzaH%Bi%nOesw>;#bdCHyY-e5Mcw5@>g%u?U=Ez5Y@*W;U@mijKcVo*wan| z8^{>cA2ie?#c-yCkVuMt%`^7WlQ_4SE_(zhv@ByIy@4`X9-`MpWS@3l9oOA(4fYn7yNh+YE>^kciZHhbDB4mv$2YSH36HsMf3#=-aF$Vx-PaS1}m3Nis7u; z2GA?R`HO~FW;>x)@}-RzZ&m5B<3#V(DzAp~88GvREsq!7HkdR02?bBAT?ifcdA~06 z{ft##HjSS43T^(eYN>)y>dpfh%4Jw>;EgmyWGs*bH zk6lX}Sw;wH&N#fM!fNDN6z+e+CC;Ja?$Cr;+6Llg4mMzlyyyHyA6rRr5KlG?R5@^0DS6Ju0gGAJIy@Vk^v5 zzvjo)1F^ImK5>`!ge1Rr1s`A7Yx{Vy?nV~QabMnU!Uj42Fn)52?4pmny$DU8oZ;|}3)09D%pH%biP4u9zQ+G? zBB>*)0O6kfr2chfkPEx;v)vrikm&;9m^C{$#(6CF&mp_*Mtj_gw62*~-1g@8!wPA& zjLHr|BIkFEZo4$unFDsd`l5BVdauaz(dD4D(lGmA740 zt2K+eL3y=+|GY@1)^k6a`RX^MBn@rk=Y@0G1z}%C3mVSx->J}oz4^Y=x2k3NvE`}9 zIrp}F=13>@`{9E_NW}d}U+w4cgx;w76UomR8o&pket%)zEgcXA5fTH&-O&NL6C$Cw zJsnU4&R!R^M@vmXj)YQENILr1+xXf0;3Q2z+&Gu3AT{h&MVFUgx(>?iJF-H+mvuzs z+|DZkg{Yf-*(0cH@BuXn*d5M)43uaV+2z>~mxjH*B#)BR{!V;go>NBt>5RX2}NJ! zkz{SOVOxLp$@!t*@CW}nx(Rv{GEuFZ9MKXbHj{W4$YHT$SOZMvL57GU#Wh-kF^SfY z=Y1RcS_&0QwVpI~zGHvK>4_eQ3ix8b4m}V90ogwx!CeE1G=J3xsSpqdG(!wQVgw+) z>DQFFE@cAdW`85l7h-~{W@~ehBoSz>=Thq5_A*Nlga!*oz<9vFe|S8oDSrP8fum6< z2%Zgr!u)PtzkmK2hXx~%z^&n5HUta>#a|DDK*R9YgTs+1)bF|2KNf_dk@y3lFbL-N z)#P8Bzz{GD@DS`z8x#pgz=79~|7C+?U}!vNphyfH`scU{zziq~21Vm}2t}X~NCa-z z9VAEugMe|I9w3YXV~x+ZGANV9sod0)ziL?;poSA|WssuFM0ZEe5QDw+I>y zf#bV`LPHQ>9FHeRn+OO!&g=JoAP5-lxhF_V9F0QbI|2uvO)eAzMImu$FJLMZiNxLg z>pyTXZqf^+r2s}j@skV#qwx<70pbD2KOh>00itB*{o6M*7}wwp(lSJy%{v-~#CH<{ zMPV@b+d_eLVme^mnDDFgx( zApXV>3>u7QgF?_iF7OTqjD!7&VqkwD7QhEYfj4ygD+)llA@E1ften0T~cVrMS$XOfwY!r|H%+AckfdAzT5Pt|12}b_Q_?HbReEi8s zfb`GUkcczRp#Dc>0LI5pCs4ddEWU>TZKLpO8iv3?@lg#!g3nYA3~=zwT!8cO)A^fT z{%<|(KaC1#HVAwV;RxuN$pBm8w*d&S#hJm#- z_$LM$6$&5ea109lKWt|(g8)O$R1*S*#GtWw8zbP*Gp!i`a0Pyv5b(2H0ocxtLqN_r z4afwG5fWm-a z{f^A<`2Q1rz=&UVz(C{~i3e;9w; zkbro`KM8RE!IxQ3;HvXqX8N0$02}-aKmlR@M+yC1L4Xa5&rDDx^o+3leFr>~5+nkA zCJKNWI8%~H1QK5XK>-``Z|wY6%K_Ty?8OY|Gx+KR`n##%0}seBKHmf5&fKlGh_f%DZU^8#+{*JK!rf@ulc`i|K1qb7X|!n94tQ70XJsEp8)xd z1r!W*ri4&%7#trnC^&EuJRAY%MW5LNxaR*~1pm=;Kq~{EK{^Tv2t51+kpR}u*nk%V z&f4%LHxz|};*~pqKS0)>K_&`)7H}vu@(dPGfU?2wQh@CY?V>P%&c$;OQ2JmPo|Xe{ znQ(j&3D^+$A_1^r&HxSw{uv$z&h{sD0@(y4IP||f^B*k-7=cR}zK2l686cqn^@NXp zK*gK^D;mHNe(KOLH2$>;_}eu=<(%0V4qPAbodE)a4>&aNViSJe(FmX~)^WPs745auBg3&0*84v=tvkRhtwt~M28gd2;zzzGqX}a)#lnDgpOnsu!xClQG zBO8#_GtL7 - =0> Only term abduction -- invariants of type - shapes -- is performed, for all branches. + \k\j> Only term abduction + -- invariants of type shapes -- is performed, for all branches. - =1> Both term abduction and numerical abduction - are performed, but numerical abduction only for non-recursive branches. + j> Do not perform abduction for + postconditions. Remove atoms with variables containing postcondition + parameters from conclusions sent to abduction. - j=2> Abduction is performed on all + \k\j> Both term abduction + and numerical abduction are performed, but numerical abduction only for + non-recursive branches. + + \k> Abduction is performed on all branches -- type and numerical invariants are found. - For testing purposes, we have option that - sets =1>. In a single iteration, disjunction elimination - precedes abduction. + Default settings is ;j;j;j|]>=>. + > is not tied to ,j,j>. We + have options: and + that set =0> and + =1> respectively. In a single iteration, disjunction + elimination precedes abduction. <\enumerate> \k\k> Term disjunction diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index 673515d..c42a53e 100644 --- a/src/InvarGenT.ml +++ b/src/InvarGenT.ml @@ -92,6 +92,8 @@ let main () = "Do not include alien (e.g. numerical) premise info in term abduction"; "-early_num_abduction", Arg.Set NumS.early_num_abduction, "Include recursive branches in numerical abduction from the start"; + "-early_postcond_abd", Arg.Set Invariants.early_postcond_abd, + "Include postconditions from recursive calls in abduction from the start"; "-num_abduction_rotations", Arg.Set_int NumS.abd_rotations, "Numerical abduction: coefficients from +/- 1/N to +/- N (default 3)"; "-num_prune_at", Arg.Set_int NumS.abd_prune_at, diff --git a/src/Invariants.ml b/src/Invariants.ml index 7ab174e..2ec4ccd 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -5,6 +5,8 @@ @author Lukasz Stafiniak lukstafi (AT) gmail.com @since Mar 2013 *) +let early_postcond_abd = ref false + open Terms open Aux type chi_subst = (int * (var_name list * formula)) list @@ -254,7 +256,7 @@ let strat q b ans = let avs, ans_l = List.split ans in List.concat avs, ans_l, ans_r -let split avs ans negchi_locs bvs cand_bvs q = +let split do_postcond avs ans negchi_locs bvs cand_bvs q = (* 1 FIXME: do we really need this? *) let cmp_v v1 v2 = let a = q.cmp_v v1 v2 in @@ -266,6 +268,9 @@ let split avs ans negchi_locs bvs cand_bvs q = else if c1 then Left_of else if c2 then Right_of else Same_quant in + let negbs = + if do_postcond then q.negbs + else List.filter (fun b->not (q.is_chiK (q.find_chi b))) q.negbs in let rec loop avs ans discard sol = (* 2 *) (*[* Format.printf "split-loop: starting@ avs=%a@\nans=@ %a@\nsol=@ %a@\n%!" @@ -289,7 +294,7 @@ let split avs ans negchi_locs bvs cand_bvs q = b, snd (connected (b::VarSet.elements (Hashtbl.find q.b_vs b)) ([],ans0))) - q.negbs in + negbs in (*[* Format.printf "split-loop-3: ans1=@\n%a@\n%!" pr_bchi_subst (List.map (fun (b,a)->b,(VarSet.elements (Hashtbl.find q.b_vs b),a)) ans_cand); *]*) @@ -403,7 +408,7 @@ let split avs ans negchi_locs bvs cand_bvs q = let avss = List.map (fun (b, avs) -> let lbs = List.filter - (fun b' -> q.cmp_v b b' = Right_of) q.negbs in + (fun b' -> q.cmp_v b b' = Right_of) negbs in let uvs = List.fold_left VarSet.union VarSet.empty (List.map (flip List.assoc avss) lbs) in VarSet.diff avs uvs) @@ -434,7 +439,7 @@ let split avs ans negchi_locs bvs cand_bvs q = (* 18 *) ans_res, more_discard @ discard, List.map2 (fun avs (b, ans) -> b, (avs, ans)) avsl sol' in - let solT = List.map (fun b->b, []) q.negbs in + let solT = List.map (fun b->b, []) negbs in loop (vars_of_list avs) ans [] solT (** Eliminate provided variables if they do not contribute to @@ -611,7 +616,7 @@ let solve q_ops new_ex_types exty_res_chi brs = brs) in more @ prem, concl) neg_brs in - (*[* Format.printf "solve: pos_brs=@ %a@\n%!" Infer.pr_rbrs pos_brs; *]*) + (*[* Format.printf "solve: pos_brs=@ %a@\n%!" Infer.pr_rbrs brs; *]*) (*[* Format.printf "solve: neg_brs=@ %a@\n%!" Infer.pr_rbrs neg_brs; *]*) let neg_cns = List.map (fun (prem, concl) -> @@ -672,10 +677,18 @@ let solve q_ops new_ex_types exty_res_chi brs = | Eqty (TVar a, _, _) when Hashtbl.mem alphasK a -> false | Eqty (_, TVar a, _) when Hashtbl.mem alphasK a -> false | _ -> true) in - let bparams () = - List.fold_left - (fun bvs b -> VarSet.union bvs (Hashtbl.find q.b_vs b)) - VarSet.empty q.negbs in + let bparams iter_no = + if iter_no=0 && not !early_postcond_abd + then + List.fold_left + (fun bvs b -> + if q.is_chiK (q.find_chi b) + then bvs else VarSet.union bvs (Hashtbl.find q.b_vs b)) + VarSet.empty q.negbs + else + List.fold_left + (fun bvs b -> VarSet.union bvs (Hashtbl.find q.b_vs b)) + VarSet.empty q.negbs in (* keys in sorted order! *) let solT = List.map (fun i -> i, ([], [])) @@ -746,7 +759,7 @@ let solve q_ops new_ex_types exty_res_chi brs = "chiK: i=%d@ t1=%a@ t2=%a@ prem=%a@\nphi=%a@\n%!" i pr_ty t1 pr_ty t2 pr_formula prem pr_formula phi; - *]*) + *]*) i, phi) chiK_pos else []) @@ -792,7 +805,7 @@ let solve q_ops new_ex_types exty_res_chi brs = rol1 in (*[* Format.printf "solve: iter_no=%d@\ng_rol.A=%a@\n%!" iter_no pr_chi_subst g_rol; - *]*) + *]*) (* 5a *) let lift_ex_types cmp_v i (g_vs, g_ans) = let g_vs, g_ans = simplify q_ops (g_vs, g_ans) in @@ -815,7 +828,7 @@ let solve q_ops new_ex_types exty_res_chi brs = pr_vars (vars_of_list pvs) pr_vars (vars_of_list g_vs) pr_ty tpar pr_formula g_ans pr_formula phi; - *]*) + *]*) tpar, (pvs @ g_vs, phi) in (* 5b *) let g_rol = List.map2 @@ -893,7 +906,10 @@ let solve q_ops new_ex_types exty_res_chi brs = let neg_cns1 = List.map (fun (prem,loc) -> sb_formula_pred q false g_rol sol1 prem, loc) neg_cns in - let bvs = bparams () in + let bvs = bparams iter_no in + let early_chiKbs = + if iter_no>0 || !early_postcond_abd then VarSet.empty + else VarSet.diff (bparams 1) bvs in let answer = try (* 7b *) @@ -931,11 +947,20 @@ let solve q_ops new_ex_types exty_res_chi brs = neg_cns1; (* 8 *) let brs1 = List.map - (fun (nonrec,_,_,prem,concl) -> nonrec,prem,concl) brs1 in + (fun (nonrec,_,_,prem,concl) -> + let concl = + if iter_no>0 || !early_postcond_abd then concl + else + List.filter + (fun a->VarSet.is_empty + (VarSet.inter (fvs_atom a) early_chiKbs)) + concl in + nonrec,prem,concl) brs1 in let cand_bvs, alien_eqs, (vs, ans) = Abduction.abd q.op ~bvs ~iter_no ~discard brs1 in let ans_res, more_discard, ans_sol = - split vs ans negchi_locs bvs cand_bvs q in + split (iter_no>0 || !early_postcond_abd) + vs ans negchi_locs bvs cand_bvs q in (*[* Format.printf "solve: loop -- answer split@ more_discard=@ %a@\nans_res=@ %a@\n%!" pr_formula more_discard pr_formula ans_res; *]*) @@ -947,7 +972,7 @@ let solve q_ops new_ex_types exty_res_chi brs = (*[* Format.printf "Fallback: iter_no=%d; sort=%s;@ error=@\n%a@\n%!" iter_no (sort_str sort) pr_exception e; - *]*) + *]*) Aux.Left (sort, e) in match answer with | Aux.Left _ as e -> e @@ -1004,7 +1029,9 @@ let solve q_ops new_ex_types exty_res_chi brs = | [Eqty (tv, tpar, _)] -> tpar | [] -> assert false | _::_ -> assert false in - let bs = List.filter (not % q.positive_b) (q.find_b i) in + let bs = + if iter_no=0 && not !early_postcond_abd then [] + else List.filter (not % q.positive_b) (q.find_b i) in let ds = List.map (fun b-> b, List.assoc b ans_sol) bs in let dans = concat_map (fun (b, (dvs, dans)) -> @@ -1110,7 +1137,7 @@ let solve q_ops new_ex_types exty_res_chi brs = let ans_sb, _ = Infer.separate_subst q.op ans_res in (*[* Format.printf "solve: final@\nans_res=%a@\nans_sb=%a@\n%!" pr_formula ans_res pr_subst ans_sb; - *]*) + *]*) (* Substitute the solutions for existential types. *) let etys_sb = List.map (fun (ex_i,_) -> @@ -1175,7 +1202,7 @@ let solve q_ops new_ex_types exty_res_chi brs = pr_vars (vars_of_list chi_vs) pr_ty rty pr_vars allvs pr_vars (vars_of_list pvs) pr_formula rphi pr_formula phi; - *]*) + *]*) let ety_n = Extype ex_i in Hashtbl.replace sigma ety_n (VarSet.elements allvs, rphi, [rty], ety_n, pvs)) new_ex_types; diff --git a/src/Invariants.mli b/src/Invariants.mli index 0611188..a7ad764 100644 --- a/src/Invariants.mli +++ b/src/Invariants.mli @@ -5,7 +5,7 @@ @author Lukasz Stafiniak lukstafi (AT) gmail.com @since Mar 2013 *) - +val early_postcond_abd : bool ref type chi_subst = (int * (Terms.var_name list * Terms.formula)) list val neg_constrns : bool ref val solve : diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index 2c37f5d..3fb4bff 100644 --- a/src/InvariantsTest.ml +++ b/src/InvariantsTest.ml @@ -772,7 +772,6 @@ let rec walk = fun x -> "existential with param" >:: (fun () -> skip_if !debug "debug"; - todo "make no abduction for postconditions & not in bvs on iter=0"; test_case "existential with param" "newtype Place : type newtype Nearby : type * type