From 731e6567cf048d706fcfd5b3d5d87e1dd88e3212 Mon Sep 17 00:00:00 2001 From: JKarp Date: Thu, 12 Nov 2015 14:56:07 +0100 Subject: [PATCH] Logik15 Klausur hinzugefuegt --- logik_sav/Logik-Klausur_SS15.tex | 78 ++++++++++++++++++++++ logik_sav/Logik-Klausur_SS15_Graph_2a.jpg | Bin 0 -> 16420 bytes 2 files changed, 78 insertions(+) create mode 100644 logik_sav/Logik-Klausur_SS15.tex create mode 100644 logik_sav/Logik-Klausur_SS15_Graph_2a.jpg diff --git a/logik_sav/Logik-Klausur_SS15.tex b/logik_sav/Logik-Klausur_SS15.tex new file mode 100644 index 0000000..0b2ca02 --- /dev/null +++ b/logik_sav/Logik-Klausur_SS15.tex @@ -0,0 +1,78 @@ +\include{settings} + +\usepackage{enumitem} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{graphicx} + +\begin{document} + +\klausur{Logik (Specification and Verification)}{Prof. M. Mendler}{Sommersemester 15}{90}{Wörterbuch} + +\textbf{Basic Modal Logic} +\begin{enumerate} + \item What are the main difference between First-order Predicate Logic and Propositional Modal Logic? \\ + $\left[Punkte: 5\right]$ + \item For this exercise we fix the signature \textit{I = \{marriedTo, likes, loves\}} with (propositional) variables \textit{Var = \{Doctor, Male\}}. + \begin{enumerate}[label=(\alph*)] + \item The picture below defines a particular Kripke model \textit{$\mathcal{M} = \{\mathcal{F}, V\}$} for our signatur \textit{(I, Var)}. The Frame \textit{$\mathcal{F} = (W, \underrightarrow{i} \mid i \in I)$} has worlds \textit{W = \{b, m, d, c, a, e\}} and the accessability relations \textit{$\underrightarrow{i}$} for \textit{$i \in I$} as seen in the picture. The valuation is such that \textit{V(Male) = \{m, d, e\}} and \textit{V(Doctor) = \{a, b, c, d\}}:\\ + + \begin{figure}[h] + \centering + \includegraphics[scale=0.8]{Logik-Klausur_SS15_Graph_2a.png} + \end{figure} + + Consider the modal formula + \textit{$\Phi := (Doctor \wedge (Male \wedge [loves]\neg Doctor))$} \\ + Which individuals (worlds) satisfy this formula, i. e., for which \textit{w $\in$ W} do we have \textit{$\mathcal{M}, w \models \Phi$}? Justify your answer! \\ + $\left[Punkte: 15\right]$ + \item Find two modal formulas $\Phi_{a}$, $\Phi_{b}$ which separate the individuals (worlds) a and b, i. e., each satisfies one of the formulas but not the other. More precisely, construct $\Phi_{a}$, $\Phi_{b}$ such that \textit{$\mathcal{M}, a \models \Phi_{a} \wedge \neq \Phi_{b}$} and \textit{$\mathcal{M}, b \models \Phi_{b} \wedge \neg \Phi_{a}$}. Explain your workings! \\ + $\left[Punkte: 15\right]$ + \item Consider the extended modal signatur \textit{(I, Var')} where we have added a new propositional variable Female, i. e., \textit{$Var' = Var \cup \{Female\}$}. Define a valuation \textit{$V'(Female) \subseteq W$} for the new variable so that the formula\\ + \noindent\hspace*{10mm} \textit{$\psi = (Male \vee Female) \wedge \neg(Male \wedge Female) \wedge (Male \supset [marriedTo] Female)$} \\ + is valid in \textit{$\mathcal{M}' = (\mathcal{F}, V')$}. Take the same frame $\mathcal{F}$ as in the previous question parts and let \textit{V'(Male) = V(Male)}. Justify your workings!\\ + $\left[Punkte: 10\right]$ + \end{enumerate} + +\newpage +\textbf{PLTL} + \item + \begin{enumerate}[label=(\alph*)] + \item Give a formal (or otherwise precise) definition of the semantics of the \glqq strong until\grqq\ operator $\Phi_{a} \cup \Phi_{b}$ in PLTL. \\ + $\left[Punkte: 10\right]$ + + \item What is weak fairness and what is strong fairness? Illustrate the difference using one or more examples of your own choice.\\ + $\left[Punkte: 5\right]$ + + \item The Simple Mail Transfer Protocol (SMTP) is used by a mail client to transmit email to a mail server on the internet. As seen in the picture the SMTP protocol typically proceeds in three phases. The first phase is the opening phase (OPEN) in which the client establishes a connection with the server and transmits the sender and receiver addresses. The second ohase is the data transmission phase (DATA) in which the server specifies how the email data are to be terminated (here, for instance, by the sequence .) and in which the client transmits the actual contents of the email. In the third and final phase (CLOSE) the client terminates the connection.\\ + Consider OPEN, DATA, CLOSE as atomic predicates (propositional variables) which describe the state of the global system consisting of client and server together, specifying that the global system is in phase OPEN, DATA, CLOSE, respectively.\\ + Find a PLTL formula which states \\ + \noindent\hspace*{10mm}\glqq Between every OPEN and CLOSE there must lie a DATA phase.\grqq\ \\ + Hint: Think about the bad case and exclude it! \\ + $\left[Punkte: 15\right]$ + \end{enumerate} + +\newpage +\textbf{The Logic of Knowledge (S5)} + \item + \begin{enumerate}[label=(\alph*)] + \item Recall the following famous axiom schemes \\ + \noindent\hspace*{20mm} K:\noindent\hspace*{8mm} $\square(P \supset Q) \supset (\square P \subset \square Q)$ \\ + \noindent\hspace*{20mm} T:\noindent\hspace*{8mm} $\square P \subset P$ \\ + \noindent\hspace*{20mm} D:\noindent\hspace*{8mm} $\square P \subset \diamond P$ \\ + \noindent\hspace*{20mm} B:\noindent\hspace*{8mm} $P \subset \square \diamond P$ \\ + \noindent\hspace*{20mm} 4:\noindent\hspace*{8mm} $\square P \subset \square \square P$ \\ + \noindent\hspace*{20mm} 5:\noindent\hspace*{8mm} $\diamond P \subset \square \diamond P$ \\ + that play an important role in the axiomatisation of modal logics. \\ + Which if these axiom schemes are valid in the modal system S5 used to formalise knowledge?\\ + $\left[Punkte: 5\right]$ + + \item Using S5 tableau calculus (see appendix) show that S5; ; $\models \Phi$ where \\ + \noindent\hspace*{20mm} $\Phi = \neg \diamond(P \vee \square Q) \vee (\square \diamond P \vee \square Q)$ \\ + i. e., show that $\Phi$ is valid in all S5-Frames. Make sure you explain why this follows from your workings! \\ + Note that negation and the modal opreators have highest binding power, so that for instance, $\square \diamond P \vee \square Q$ is the same as $(\square(\diamond P)) \vee (\square Q)$ and $\neg \diamond(P \vee \square Q) \vee (\psi \vee \theta)$ is the same as $(\neg (\diamond (P \vee (\square Q)))) \vee (\psi \vee \theta)$. \\ + $\left[Punkte: 10\right]$ + \end{enumerate} +\end{enumerate} + +\end{document} \ No newline at end of file diff --git a/logik_sav/Logik-Klausur_SS15_Graph_2a.jpg b/logik_sav/Logik-Klausur_SS15_Graph_2a.jpg new file mode 100644 index 0000000000000000000000000000000000000000..622a94a985255deacb10441e08a63de06d470eae GIT binary patch literal 16420 zcmd73WmFu|w(r{nNGCxWLI_UdBxxkLLkI~FG=?=!5Oecm|lo=nAJSGN_(~?tA zQPI%QkUXIS(@}#dscESHaS0G_ufBR)ky$2c=vGb-E|!Q;iE?cfPXvt?h#0V zkI5K$o-j#&Ab-ltYxscTqmexe-)nWB$R9rkKdEUrI7WSs85nx=+1b}Gw)A()Fe|^H z49wIeI(=mE?z&I@`F{U?<9{3_{ik01$I(duA?{rdNpVR5Qh?p%H?Q8j!TZ0YdP}!) z|Klu~%%p>BwFkkl{nIUtxN@;l+1G0V(2cHdQz-k~V|EH*(Q0+r zqR6Pv{xQQrElOcfX(G+j-00vw?-9^M3vC4!)gR>0n7h%Y~J=$pK*(5u)iL25uWt! zUZ;Um%F2)4?d=_e@R?+gVetXX5EI+Ix;JjBOiuxdjHMWDFO?PL8t-DVDkA!}6V$*F z^|YiFw=c2%w{vcTYQ~rlGCt_Je#SaP)&D8$b#3R z=%$ZLc;JL!m9^nYtvX!&`CyJ2`&MM@DepTLCz7afAHz#IOxTT)-z0JHfN6Hr$gb5T zmm-0YpZQ1Mo_OygD-Q9pX3n7c9SgXy#|soet}>4Y!{tIfn?ZE|pen zh$h?qd5sk=Yqu?n<=Nh6xhJnp_Qj3%Tqr!?SUpR~dOB~-`cqNJ+V)^#O7MY;z(T1s9~JXM z*yO_WK$p&gWs>)Xa0!Xu8&n|)v;?gAQ0n2g0uta%r`i*`P3D?jScjo%8>_yC^o2bi+w}G_^n#|+7 zi;G337UKhOp{`^&gLwW{I#c?1%)nobf+@eC6l|)mg-SwH&?o!TcgA2hExG0whf{cw%Yw#hHz(ufE2YCe=`fYhHn7VAn>Osd2h=a@cg_9k_x zzYwIEBMKg@&|J3dDYRe+Z{^NAf|xv;NRRZ1wU`X*?<4e!?ZDon9h7|Ym;@S_Hydig zsXe5^{oF`V-Fic#vTP7AFDsUTL(A+Gnj>_MpPUpwEho; z!4EMGvF7U`aqFmOiEDfGrvlpy{AjnOv53meWIigI_}QP42Lj@ z{O;)m^FK;*<#|8#HEQ-~XFJ8Wx-9#*+9N?0QR*F|PXTMiF23!1bPmDAe^r__42Eqb zzdBH^FR$cU3&G0J1=h`xRb6*RZH`0l)HaO>$zn^t&er$uuGm}J8AJ~A>Zju<+(E;0ri2RC6k7WZd`t|p1q&98eq81FP zN?Y;t&uZiq+gH-7-l^{!x>KJqR^LJelb{;Xk{{DUT^yqLBTh7;N1s8ZEn*rDJ0!lP z0c*MO3ycI3dy9Oq&9XwZH8M1w=Q^G`r>Sl`QWU~bUaY3Dl4E=R7ya!`f68;;j2rm# zw7|mB?w5li0Qftn6@nrM!aQMk)vbGg^Y35;$zfzl)69!Pp)B(YqhlJv&MV-3LCiN zOsie@EL{tGa5P%X>Ni26$TbD(@64eU3QX>3$a{QvrsD$jVas}*ul|F5xKuVk=;DDi zIxz4-;Fte{Dg-Ey@S|{%d*#q2Ju~bF?iRF!@zf|RjLR{63y{{UNnYmKg<-2!WmajE zr~kWxh7dV2J9-`J%)8=wNFRNEE1c&%IlG%}6MOQ)I+vv+*f?^cwMNIY;}Yf(VGj9uvoA6+i$2;}mHTX}O_jT1_M>96YT7j>w1n_ulZlBeiWSaA6q!%N zj@d>^b3PDNp-L|yV=ZE44Vo7ThxsKg9OAhb5ymQ@!C*7SSPVWjxslT-hh~Hv?T2!Q zwQ6i<0l?wi!J~-v-Z{VZWwED{-7Y0g4pa$TaM6|*l1ksz=m>SMK88{;1&!kE!gWUd z1(s?n(RhXDvo(IQBTtQft!vU0H&CU<5Y>B`CqJ+wUqbj%FkIBUlkgZPakIIcO{sM{ zg}1_KP>oTwQ7t-oTHg=)6;3-@KyVou9XFQ9-@ivoUz!SZ%f60Iycl~fBmNfs4P{`r zv^Sp%Kd`+h3KL6g))aqY z)*H%VH=4()1yICy53#t0AgPCx$S$1AfjuCb5W{yUEF+JPQp7Rc4tIaS5v1xaRK5Ul zB2CaCd@rS*#KQ(ZeM5W#ld=z*RgqXm&sEQ0anZuMvVjmT-;IP6?(FSWs}TwRX*WnI z78KkG2!1zvLZT^uNW6x+^Q`g&p1|RK+P^l&mG#(WCJ&msu^P;=t-$E~u8Wu04lXIO z79f}1195l6uayddqzW^#+AZoCnkm|X;0i%P*Ne&=+D{wLmB-oysr9Kst;<9(Fbebwl+1Iyif#ddPrbvZQZGEDc0L{ILK;11D@A}!p6oPITdm|@ z0wK469{pQ@=#KYh_$}b;)o|!`Vp5>6^WlMM z(yv5{eyA7xB`=x2&yJU^Nuy1 zvq`=Kud>+BEW+X*t#23~4vT&EP@q`#G#UpGQFAPZ@Q{Ra%^ zdM)O6H)J}v0gL^MbT8vn6a)5Lxl zy8qbb(%Bf9&nuq{B&nZW!)eY&yBaR@MG&0?`st^1Hh=qVT#85@9nDnNCZo9SZ+}^J zcxLygWqp+|M--%btRP7&WRtB5QlS`(NcOzAE-uM>d7%5GtL zf7rf)%?af!{hwD?#u5H;KBq=&Xo88JBVW?sjfPs6E8)79t&Q{Qa4XlX zWywyC!fQ(OJCyAOd!5${o8p72P%oFS!+cJb%fEWXObRTYcF|xvd+Zo)0WbV+tT^B| zw*ch|#fyI18LZYCBT6d3hq-picB6$wW>4CPsqm)GYO=4kVZ*UUt)W`ivF1wLD|&N} zgYSeV%4gru!J^$Y`Hx3x|>xP5q=?u9k6Ek#|VewO~i#+sI6Z~BhI@5$9&1H zrAps+p8DBBgx$RVeUV6YDvc|VfV5b{=)BlgS zhUorO^}><6fQ=RJBnsk^@UiyAd-QT?_x$3h;4{k8C>b4(q&@w_!d<@^rmAhP=_qB{ z59EI;EW1ATm_<$xaF7W^VY}q*cFcG1NIMQc(3gu^_FGU<{#~{mYu{G0)~4L@I5k0$ zK51(F{Vm)LP@UeHJ^W(My=}EJv~Z}>U{9nS&V^m%8GF%?F?{FEx3~?>8atzDglv77 z7l|A-&)p*P@kBD42fMTo23T0>S)FnhJ-rNM@$!itO?b$HQ1y+0oiH$!SLDp0I*&02 z(_&us!;(tLOvzgNw-}>uk$)2X=IoO}n%!W(_)Y@4hxudWvV_0c`GFU7SsHQ!S>rX1 zDeXst<{0;Ln&TP5n(w_%tow&g(AWhkc*~N&GKCzC%(U@5FrZ5G0|nQo;W;kT5Ut!5 zrj0t9;%cNx9QjMD_yxP_9V+?(ntA8PjMnz-%&}!H78Z+t{z^t`=#AN$a2vEs!Riyb zk;+K|Ash|3(WQU2rx&J~IJS^biJ_TkVBI?c6H*dVa;a+Pk$AIJ#?hA)j)bi<;Z%{G z@1}^9oF{asNa7`a%gGWfInL3@6S~^5r!rJM(cm7Y6@-}P<&_-jk8h1R$HF#RjUywz z?65|JKU?CmH9!W^wc@MpOxY;t2zGwk5O6J}vbH>auK$#C^f_#IplacX%a$x1O9LL) zes?IyZncrU1I6r4zGhL0soQBu%)|H4%{#LkEs*2*xc0I%oEl_Os1)7t*XpHgJ9_bN zHNvshNBUX%ut%>RkvB2~BnMQqN%SCe=oF9A%DbFTTgQI4LXqHOmNNiFVv$b0B%2^A;LnSKngeev!|{;*(Zu8sNL_)B%p*_KsNKu z;mk!ZOKRfGPXWD`9LZ)IeMcmVFk*gYI#Jd#%ozE1~8J`Ek+ z0-Q#$rUfy16)^3~8J(@2A{)kor|GcP20fXEm%H5VGJOz*?No~ZPI`K;6jS|}sM`F} zXT0%a{Hp&r@v{bVRLt83QT^|Sd=DPG4#||p>STN?{uhswn z^W~EgpL|<(f0RPZzrYhtmA0~lV-9$!7@KT^V3H0cOTsjw?s`<9p~y{Ax&SYF8Rvap zhLFV7$%0|(o3T5K4XVb~{a!kELyoxjXa0)rrQ?k~|K59fm%=ndXR5rRYL>Aw!AV_J zve(Q;D-j^P3dU7xP~OaB`z_#MvwhJD@chM2ipd5&u1#JrcC)t^ii(Bilbs!W@(E+n zPFeC7xenvtG-G($-oJMGSWHfB@MWTv`u)d0tn+L@)$Xk*^hjm+f+Alhvac(;=?DN~ zWt7%N1z4(K2=CVh6baI79ML~zXMMXU<{Z8^O)pKnD;|eg=ysDlROlZcy9gtONx(aT5n&R~MLZ&iLI45=cJcvetAUnbu<+M5I(a&^#sHVpi32BU;Bt zbYo_8NwO;F>@d4ag({I5(`mmWP>?%iyS)FKw$6Gxza4qGzVC&mb z`-{4h)W8>?1D{tORr2Ip_`0bzgpROeS(!An-;B%?Mp|wY{Nl6UOF*2ZY~7QtnYFsOI#;qjsH2T zi;Yud^!YVAUSLUj@?ffyrN*xh>Cq|v<~)dfXaqkaSS;T*adl;hPp3dIMh|9*HzVTIA3E zzKV}U)dM47a=*yhkg{mhtI@O9&rJMZSu{KtI&~Xm9 zH?L<(1lJtJgb~5z060xJz$EwKjy|Cy-S+QNRLY`5dy<~Ty{ESTc3Uamn2j0f(Nm!w z;`;9>WCXvc`zP6plOMqThKIPu22#BJ>5zBD8}U5}5y@XwP%CDLp+?cqB| z7?621A6m2~E8y;p+I$I|vCDQz!W{%tsx*fl0^N9Q&^V)8dG!aNu{$~M$OW=s{h-I}VJOUj55-|@)v+nWehYYR^m-k9Ne~FeXaA?P z7QXg}&W}Gv>X(>fD)nMCUsj3g2?S}=P#;Pxj-Cqpbft(<16yOm^~j^DyK>r^gzVbDe;A%XDYI7OVnTS zS2lB@p~HKl4P}joTY`|5n1q$6<~v5zv(TW?Mr&KR2&~i7K8;!a50vp!OydI&^(ciz zgnyeyM%67%VJB#CFmdXxd62~(5x?LL2I()uJPborAvX9bz?HDT_=hTL$ zHHIPqCYI%t1lygEuVIdzAXo<+S+%8iwqa*blb~DA^c(rvHMh6$g1<~Kl>oV9PBOy_ zGRx>len%>|q=3|vp%!@{`no6HVl1|;I{oewiR7w+!=-m#TNeCT3q(Ueb8orD-BuHS8=(+sxjI=`V%R1}UIhr7udVW`X zY{O_n(UINqks70|Q&}HFSSXlxY5AVdyD@7#;b6CF-X8E}x4PiyYrab`o~^~r>$LH0 zCXbMf<(il%mnHO9e#{9oVUAXleK&c)MDa~E{#xHGu76O(UD|mbkA~0|$}gVsYeUF5 zPj)&xFs-vx;jz4zvemYs{S}Z^Rl<{8%O=I@n*~I_h&*?Yc!DXxXUp!K#3MLVBQJhE z;ba?6*&9f5f3}R}TlXF|FNXqL5<%=5a+>XK_Z!*&N?=CFu?Y@cCBy&PsaDWvG!Z<` zwwFp)^0@6e2*WThDkK@b5>|L{y70x#@z40m@sx0~N%z|VQIS198?EQK2cnqiZRlPF z+XK+RNSE$2Z#-UD7xR`B1^!^oNi%A)_`9PpW;_B(c56gSp8z3}s*sYgNSg|mlgVu}PB7^Cic@2cX$)-AsS3QbQ||8$wj-;&H&PXxV3l_8kiGB-Wf{_^R5nn~t?&l+P8_t`^s zlt?_ND;36^nt;1VVv^gJud7fwq`qD@iptwqIT0P7>P1trI62Rb#nlKF`|9tY#8VEo zUv#S#X&i}xmA2dh{ICZM zu|&3yrU*-?WyLj7OGUgN)Ka!fS1D&+iaW4yux8$5W}sZ5`Eg1|$vqG3&poB|I^O%b zS-pk!vOR>Mv>rM|37{-+dRgLx-J;xHd<mNwEL2vd%q%QXKo`}VK_;^EXI&AXg1xk2XQ2eX#MSXLq zQ$U>j;otU`4r_H+)crbMfV8#g(Iw=gNov(kd?GK->e!StdRGlAE=s4`6$#NTHd;%Z z9`-e|fu@m}jh219luO+*kZ+?WTY^JDKgx{{+%&o*A?kl%G)FO86-=7UywcCO?v0qQ z#F|fuhr^-J2Qh^fZ0prudXI$+f1rIsCpkr9vT~ljcJYhBK#c~^T7mHkh8!03FC*u} zXO|F(#R9qzVCG0HomYg<2`$*NJKU*)Q=C|AC1JTi&VJus9K_gkApOWscKkGcU2!SebiA%Y-Shl6eW`W8nt&iqqN!iBbeE zjbCk|8~r!@n~+a=iwVA?cH_U4%jh1xRJW*Q))yfR<#$Ed)~uZ)+Zx^+Vxy)Q#+(K} z71>U)Ra0$aO(2yb3S1uP@pV`$oIU*Zhr(wyS|Dui%;%kIs_N0iD4A6r_xg(QrG;(v zyfdAfIapHo_=^31CQ~R|_fWBh5(J2UH(NZVbf}tg<=Coy{w&M38?$Y()c-~LfK`3~ zA6#G+tyg9SEY&dOhPV4{4?rqhEGItFcQ9mmK;% zGgon9jSQ zuzuVD3eh*}9DC3~NuFX!)#0Tc*OB$QgxZ(O?kN#AeGWoF4A=^80;&&92LzBP4>`Ye zmdqVIhyGqy>19M{?|QcccRCfewqwgpK6%o^W3!b&AHHYD5qc3s_qSqlO=W*v=}Y(W zmezR1$H6g^(l?UoxEmc%fH9%e4;m4F@oUg}*1|SdX0a z#5OAQi4J532~*H=asEJIp>Wr75SJSc>svW%ii-4Vi#WcdPgH4ZrQCUX98YA^zlNIy z$@dxdI?hgr(GN231voC*)=4;t74D+*XEWE*rcGN-`IB141%8ifL$~emKDKvKuTmL1 zN1c`w!UKr6iD=6Y=;%YJ;l~^Aou|L%r)x!?MK!dv8ZlzotD>8hmR8ejHioINlr`{g zjWvyE{6EtgSfPC(mW6Qe@|)~C+g(Bk9u|RxVgft{rO*(JW^QJ*L}TV z76nDWbbGiD5o-e}*vW55>Qg0A_Ux=+bWql=j!LnvCg}yQ4q{5`q@Ce9m{avYZGD?Q zcXaMYTXE0FXhvVZsYRJ>#$L9mt{`5;$<;5qefagWHuGPm79BXcmYy#&2AeZg60jLN z3SqY40nAknuHxXg@x_HssFPZb=%dEx#DYoFdUjL~y8iN~>f`iWDom$J0zF_0l*=)B zo+$?*p@<7-hr_95NGl$zjIY>OdGC;n)1A>A&>OU%l4}f4BEhCyBK{ayB(SVdg-$`48l*@cOwS zLkrK9aTs>_bqdp?&2{=88(vyE))Kq4b7v~gD#A{}M~fhJ&q3W4>W+J6%{G|c^iAa3 zG1xC-i6lN6WM-Rw&@orLr0GK${i%zlr>Qd?Uc_fM>Mco)`Rgooo6i26xrq-e@y-xqhnz^-exb3>+ z)ACC7-`LNm)bHL}a|1*#XouqoL~?~povB!h3}h`kPRM8i84iY80>n`da2Jbj0jxH^ z)He_c`?hWK2f~SzFGlt`&~s+i*)0UnL$JkKxt(|iy;-=A=C#H6vEHwB8o_VDMc!5= zEBcvn~~wF|X0EJZxrSfV?!fYoQ^W*yJ1h?9c5%<1xd3tY5PmB)EsIJd`_ZG58E z#GBp*=?4+X?6v2TJk1Lx*eBQ3&u;-^$HKI^i(Z53-MPAssU>ZkSUQ>y9hcy8IpPko z9S*Bm=w6OON!K0ijbGLrzm2>FP%dqm z{j!gEE?f4?5c8H^Dn{dC|D~m#2zpi!vH%fxghSp<|7O%Ryc4aGKrr(Qw&=2j|-spNZJ5sb_9M2+3$tp zIChwWAG@lVY8?0uf{ zhEyJd^aeL7lzMiolnpVEPq{4;Nl)ppRv%ht712narEpcg<%en-A8XQ!H>zue){P;{ zd+{aE8%3({4Ehec!6>X&iN%h^V{~T1@r_)?P*W<=X;<7Ni>&WaLHd5XR)9^P z5q9&a!)l>shQ?vsj0J}FcC>B=CYGj$T6BC;!`BK#xrEkMC~l#E0(D4V4o9!Q!Wi9W zQQ3f+XSI5x)hpw{gd~@@tpf_eMP$IdnyYkH&vUn2EPpRO(}S@7D>{ zGzQL7&vCOdk6nC7FqIm2NciO(Dwg3?)MBaZ{DFDqG;}QW@}~wkWMV#g<w;B_6oG|RW?Fq|cDu`+36rnXTwAeG**uOft6~sdS`S*#C;oKqr;S;Ci zr$rLdZAz=1Dv)Yn?LP4qJhQFyWBkK=AX@AOxlg_Y^dvz~Uclq6l0p2bD$9rKjGgP} zEaDAvUS&a2!E+2n8%`kv67fYgu{JyB!pZcVjt+vFMu^@Q1w_8QlEhY?v&mICmr&~d z(J$0M0Lb_HpF-q+RY?ACef#n88)@9eK_zg7a?}WGb(YC0!XtLiA&>^rr~q9SeW<#4 zHtqF>!#301FX!CUUO*@mE@8b;mF3idVIn*u5oCvdD*R*ANQDAX0zd1^&Gt0taUb0JKMJzU&CT7Dd2SW~Z>f&{0ggSfY?rYs7}jJ( zr<5UB{Yxp=sT5Se%og=cZf(odV_?Bl=4Cls<-g;$c^6(3^lPH;e&)6qX;N z4FY;i_=Y8IdN5O)=HnyRjs4F#xOjFg1h`Z*a%ph62(a(z+owNzkL5?{j1Pv@H#A8#b0ho=TsHl+}0Oh zDWx&)gAOb07ptGeOM6-y=Tcq9B5k--O71XzQB7zPxc#w`fW1iEX2&YB3MkNYC5=ZO zl}8`=ZmWv+1gEiXb7GS}4g7;J3^i7P zFLoVL##k8di->=ZV{62n(kjpPX9rRypLIy`Anc-N2p3w=GKjKcGSxg75p;CS*T3C9 z@?B7{QZlFWNyn?O{(Czn#4Pt?5Br$EbxqJGuQ-&KXJI2-HRAAPgjkNPR^XDE6ULp= zMvq*eV^M!iQ9=lpbAF$hjuq7Sj_@T_-OdDp4`Gn=ZN}om(`WN#)Vo0%Eq*PYZgciC z&E0m~u+0wbZWJ@7B@U?U={R~*>Zx_n9CU%5So9>{9zg2b+9D8sGjmwmRB?B=g2}X( z6MyYyG!k{qShh?{A}R&Kd?v(ud7&CCde8HzE}o8*Hf$ z?^ze&Q%M?#u|K%`&V3bvxzGO$-U7ldZUGmgplxo7V-1=ATJ)ZDR2|o+g2)^JrEjhUYAOCAhIe2yGQ$qKn#u&~_?1;KtT4sa7BgmT zco0uG%UdUCniIK4t4sK;xd@&XD@)oX&s;@%@QHz*A@|EbFA1C67Mg%+Q8io7M@m z?Bkei(ph+|7Z?_AH3^p#{xp|!={2xxOQTrgG_x5zs+cDfKH!P+OqZ1NWgo;f!Y zp2v&!PDK3ku0gY4Dbw`~F2ng)gkw**T!yevAAU~*JSpq-J-R0e*%g|Gc1JvFaBVze z4+0qR0d3V@KA!X$z#JzH@b6aSpVNH*y-CsMmF?8jfch4+URW7;t}{t->~uv>up^F%S@u(|v(OpjFHi_Oom zbAe?;N;h(b=}<+ejULPlLgyN?+&0NPS4ug@hnMWgjvFf#cOD>K&hnyky&|UcuMlq) zdh2b9X}i&?0u5TcVO&dOm!yWisR?=tE`Ll9ofX4DaF(o37e(X|)sVGW=5IZI%g+rm z4r7j3t#TvrGDI>kJ#+4~ab~(s(NIp=AAomLZB2`xdTV0lo#-@5D`PKhrGj$NpG1$Zj_p%R2uG&|ebVn%Rg`MZ zx)We%?k0HyDxlLl-OOMc|9ul^kM zX~M9}2R86}DkRGQV3wUpFXF27`gf$PWi{33G z1a`;G;Ng$U(iB&d>)vfd-q&it6OCz4v7rT)mRy5$_Kw&kM)2w97!tXgpO%en$=nw; z+*?JOstrq9Mbig$uTYFF=lU* zVpUP-sn*~9turY0W!dozCC41uaSW}Ag05#?Tolgn&4oE85#tJROVa(irh=NKvQ3!N zHF&tD2MEO>1j?R}3n_`dm`$;!65q60)Ukyb{IpoKgV7Nvsj#Z@OXc-cO%=Dp zFAZs*sX2PlV|lc%UVuv&)dOjvZ1?GOO!oMKyZGJ`!7(?|qrv?huFHbSt?!rZtLJF7 zr?tK|6UU_QGipI)8;=zg#{_OxYyXDoT8dZppM4NW4sV%J^U4e?8}2?4lX9qwDX&xN z!Gxk*L%=cRz-oh%>8H(LiGc$Vu;YAT}OvwdW$jlls>LO0u z7+*X&>?ky$Hlh!io1oF1?_-HX)Xu;&U^JaXEEN1CJ)KUlN7l-YA8Ngos>QmaJxTty zxuI2A`wE!B6fB2biKA7AtGjP=ucmhQ(H)3xn#F4fbv`QYYIPd!cBgjD&UPD_DihLh z>GY@J3t%R3AVnI|q1ksOW^Ms?2zSppskixk$NCDR?am3D>4e<#xstOo^wZzzhX}2S zE(hX#XBEeR2tZu9<0^^Vrjx}v=(=i(cj8QSE?tuk{9$QXn`B={(%LCAyB{U8ifvo` zWw3v|KMqyfABOOiJ{tLH^`U((8rly4m%M#;?ESX-*V0L~%QPJ=(Hifw?a4pVwALxz zyL+@ZHv`WA2fgp;vX?8yD(f{U^uj{XJ>RnRt~k-jWy?lk6-@T#@Fmu1iHwe>2g{F7 zu6{rKuYTJiRLXkc?+Av`C1&a~zwRPnFEC~6q76G2Da0eaRI`Ppb738iDJ=hN_JgWl z+jW1F^&+xLZ!Td~%PBWY%^E8CwW$Sh=AI}>a@;)=NPbgRk(Y-- z0q!l%fosd@#Zp?7QaML;ArDMZOba>R7PKOcMOxqHxs#Ibg0IKomV?A7zz2n)@Sh8_d$f2SZx%~o%l zcXkbkShw$sc5FFa+YRHH(us@imUp*8q5aZPF zcl{b>oDVXO5|W*Nux-GXEx&`Tt*02rme54)G24cxP1;N$vnN zFlrMVZI|CO3db4C*%4pHO{3&GcG@vNwqSDh_I8{^2stKVcT>M|DcTv%i9=&#HBDeYFSvx^pgxph(rPGRS(8eoV#e(b}XD zS22T=?H+B*Nm#URpA%}Hj(=Sbt~FJ@hv#=fM}myN0Aarl zbGE}bl&AyxPl-X;?ca=F52&L99jvL@PIe%4WxkZ(vP|%i!u-~nLZAL0dc62 zyGhM_v3s2pY%IHTeIn`8lD6P$Lt=&GMHgX(1^t@xAJM*IZ+cd~g4rFWdPqJAdquCM zPwpj2s<#V@^-giF9bn)+%!}VjjZ$9=8@R!gzT%K2p9)I4xy{>A7aITfF3tZAmH&nO L{NLIDzMc4A1F#<+ literal 0 HcmV?d00001