From e69fd0a6f4ec433930baad95c495b009350f1e4e Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Mon, 20 Apr 2026 15:09:37 -0400 Subject: [PATCH] reachability: pin FRET predicates as numerical halfspaces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit predicates.json is the single source of truth for concretizing the FRET-spec predicates (t_avg_above_min, t_avg_in_range, p_above_crit, inv1_holds, inv2_holds) as polytopes {x : A x <= b}. Until now these were abstract booleans in the synthesis spec; reach analysis re-invented ad-hoc thresholds that weren't tied to the spec. Closes the Thrust-1-meets-Thrust-3 seam. T_standby now defined as T_c0 - 60 F = 275 C (from user review). Replaces the earlier simplification where shutdown IC held all temps at T_cold0. 275 C is inside the model's +/-50 C trust region around operating point and above coolant saturation at reduced pressure. load_predicates.m in MATLAB reads the JSON and resolves rhs_expr strings (which reference plant-derived constants like T_c0, T_cold0, T_standby) into numeric bounds. Returns per-predicate (A_poly, b_poly) plus a constants struct. main_mode_sweep.m now pulls T_standby from predicates and uses it for shutdown + heatup ICs. Heatup horizon extended to 90 min to cover the wider 60 F -> operating range at 28 C/hr tech-spec limit. reach_operation.m reads delta_safe_Tc from the t_avg_in_range halfspace instead of hardcoding +/-5 K. Current concretization is +/-2.78 C (~5 F); LQR reach still shows 28x margin. inv1_holds and inv2_holds are marked PLACEHOLDER in the JSON — engineering best guesses, not derived from a specific plant's tech specs or a DNBR correlation. Revisit before thesis defense. Hacker-Split: single-source concretization for FRET predicates, end seam with reach. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/figures/linearize_sanity.png | Bin 98049 -> 98049 bytes docs/figures/mode_sweep_1_shutdown.png | Bin 96400 -> 111974 bytes docs/figures/mode_sweep_2_heatup.png | Bin 102306 -> 105087 bytes docs/figures/mode_sweep_3_operation.png | Bin 105852 -> 105852 bytes docs/figures/mode_sweep_3b_operation_lqr.png | Bin 97750 -> 97750 bytes docs/figures/mode_sweep_4_scram.png | Bin 98578 -> 98578 bytes docs/figures/mode_sweep_heatup_tracking.png | Bin 42370 -> 42487 bytes docs/figures/mode_sweep_op_P_vs_LQR.png | Bin 41910 -> 41910 bytes docs/figures/mode_sweep_power_overview.png | Bin 76866 -> 78129 bytes docs/figures/reach_operation_Tc.png | Bin 69280 -> 63233 bytes docs/figures/reach_operation_n.png | Bin 35326 -> 35326 bytes plant-model/main_mode_sweep.m | 33 +++---- reachability/load_predicates.m | 73 +++++++++++++++ reachability/predicates.json | 89 +++++++++++++++++++ reachability/reach_operation.m | 8 +- 15 files changed, 184 insertions(+), 19 deletions(-) create mode 100644 reachability/load_predicates.m create mode 100644 reachability/predicates.json diff --git a/docs/figures/linearize_sanity.png b/docs/figures/linearize_sanity.png index d5528feaf49fbdc47451fdb6e57d26fef775c6d1..a4b3c9319c7ea964bd7b041382e6ce97feee88eb 100644 GIT binary patch delta 38 ucmZqt$J+Rhb%GPSh&cZX+i6!PdIocwSs58y8JbSc?Mi7}zI8ccR2={vt`4LC delta 38 ucmZqt$J+Rhb%GPSfQ-Cg`S)cLJ%hQ8tc)zIj15~W`rkG#-@2SJsty1cUk=m& diff --git a/docs/figures/mode_sweep_1_shutdown.png b/docs/figures/mode_sweep_1_shutdown.png index 1068d7ffa6759f117cf8a7731a8050f43c0502d8..bc75195bbabc1b5c638f16eeaa32b30c97708151 100644 GIT binary patch literal 111974 zcmdqJcRbd8_&$758l=*o2z8NUmW+x}u0&-dD|;k6B6~K}B~&VrtzmCbWE3GQ$t)|P z?Ch2C92ecs@B2Kj-|zMO|9oEe{kq*;*Jr%Pc^>C+9OuVZS@8@#Ei)~FK%keGBdHJw zG?(!2_6^kdjYerU6aKT&R_>BLfxxtl@-LNX)K`3pu>QKd!s+z`Yj%QztABe(Y=R7jvqRD{IIC~_xcwE!d`+r>7=T2_)xo> zj(`8M)TqVmqu zEN+l;M2iZm=~Au!OfXaao|uZC8>FvZy(%xiks;fx?)jyxD-LesH*ZqsT=;G3nbO_e zy|Ca;{QBjK*|$uSHTngNnVFeJMn>dMEiIZF8gDk&>Zqzd2@XC(3Jndl{{A{4_T{M< zZhrp#&wtf~iJ5%& z>gJJ1y6+r^8r*G8+s}p zf19p*ac2D%Hl4);3(}mpb!VZ+PTJF@i^RZBZEfzK!;jrsN1s@7FQHA`=?{(f@!Q9+ z-x7Ch-##%`&hE7^R(@;!76AbPbwh>QF%Gy2I~W;1M~FAKw-@N_^(Ge=7Y_{&mz0!zi#qp|ZyzyN$MeVg8+TGovU}`Y z3=DpR95!zGL=zw3HZ$TeUU6XO8Y;9OW%-8ifBqZd*3t6>IYqwrFb?T;{ zUsY?9;#;wzdY&EkzI^$Ta52u+)wRiGia=1M&LD87rKj8eogU_p_1`7oJo-J`l7mQ8 z)#dOmJKr*R^~oCL-6rd{6!Bs)HK%Bo=R`zAsA)g@J~lnQdGqF9UIPOIpa?V5yh%d zo!p4X$jINHBa*U0sR;3kKj*Hkb1=c}W2dlUt2Cu(9}yCYRgAcI*qC4w|MsmW*W>+M zT)%pH8b&r@FZTEM+vq(G4-d!Y`t(We+4-`pHLCl0c?a>u?9>U%0{1x~Ny$hBwG>%- zd3g(qfgoOuCkJ)J_wV2D>+5T7ZeA&INWx|OvWm(!hGWN%tM9Q2kBW-IfIoVqqM$}c zOS^6Rc5Kwgj~`o3k~3ewR^@tJU>GHF;)DmTuuzMw(*E|^&z211!-o%JlejNCb$XPG zUilneA(~_LZJevwLk8n|Vdc1X?HUyomAbmRRgsQ>()sf{o+dZ1dmI+V!otG)xI$0d zG4}1-qmq(K*_}4{kh^=nP?vvm&eu@U2W@RSl0<_t|J|ORp1kVGEtw`&*s!zLWBix| z$5~1{3f$&?xU64)7ys+(?3}EXJ%BsHTJMQl?2n6jk}MsNzKONB?BEkzEesF$?AfIQ z8ajE`4_ewCJa|y-YMUm0_Dbk>J05$B*k5|IW;v<2ZAF=u1q=*w69@dyZv# zF1ix!u3x`yYdbnQiLe`a#PoAz5U-`~_Gjm(hu?H&KFjl$h)XTgqUwZzAQltdp zk>aUS)PL(+TAXVmPaqDPc;)5g-SP2Z2uwfQoT_Vo?V4dLrW{+0e$%F&1L0C$o|r;h z?s;5XIj#F#Z*cM%1rnkQBO~L^K^+~Pq5l54pAV#HokE{I8*a(CrB>G28ReuesF(jK z(sX>_l9m?RF}vGjy+U_$BctMbF0QWMTU%Sdf6v@pvPEiP>$Yunzp8gPRWSIKV#-1e z8J-e}>Zz4lt`?QOzvp0^7uL9lWz)yf(yTF**;!9d z4qZ3W|ISrmeWJuhP1he*ekKN&HA_YJ=cD7HAO4? zo|smkoUqYHGUE04bxZfiIm)0$O1KO(9P~NGuzmYQbLvkwZ{GYgoB+|zrXGu`j#~(uArnOcIc3tlG1Nh&ji)^cBfA4 zxiJ~UZBgU0O~`meq&U~51s4p5zBbkVx%v64?Ri19rge>t5yu@8v0g{VmMR_}Knf7x zGd48r>g)S7&ZO!Pr&hQb6O62%o0~f%L-zCYyMO-*yVl8*ACQ-Q>ZlS_^NdPq*_3<( z0wP4MnHfZEIu?F>xP=6r=Q_p1;9F|M#1!m9$FwxvYV*$N&y^r1zfy#vVx5f$E0)cv z^cy#Jxm8zJ^YQTk29#&ssJxtc?Ppm=uwwYp47Zu9o_7xm3%9*Ce>_^HHr_!;u%OQH zF5^0KBr82VJ+adQcLmU}&G%&}m0d?ihZRXjPp?C;XyFv;%9Sfq7cY6s3LHE3?Zbx{ z9p=QBFFD1;-mr>09zA}%qsUADsG&C34?jXJ5a5jZ=!M zyew3BMj*JV*KV4`D_G9-b-B+9~ISE;5L(=pWnh%z8sONSD>|PTjGEMv2 z9Pi!!6r4Hx=Bt+211z+$VIVv)>+cQ4#W#IKG26EfaGuQC_k91kryJH#Rgd>p{l?tq zwB}g<{howf82m14jK%K@k}7~4Put_bzzi&vyIa^Pi`Im*JORhug_vQf40MoO4`HVzVr(fEv_G>zehw3a+*v=iuO&RxvOzu&}TwmGKV<(ACj#Hn7>cgE}1U*mJ;ddZQ@&4LiTbp`V9{c&)FLgjf&EFOQSyTW@a9DGuG2% ztKBP2LMSgjR@UkHm%sCeR6RdGKlZ}s*zWCt=ed%01$N!Mb<2nKNY}+etsh(D*3&aL zU$OB*q3c<+=3r^^I=7a`|%gvm@n5O<4MvU0OOi zUNLW-quR=v^r})`x@ZbL5G0q_l#19(kUiacfcYL2TQu8w6ic_m3a%>5}yd^164N^EqW`VNuz- zg&{-QJ18h(u#wV^Y${6fw}oHrx6`bD`bmOUt_ym9iE`$M~`l>X+L@LB$~gy+ji{e>Fu4WJHtK}bCnSNa(32Pa<3OK4Bwe%#PeW5{m+glJIZTn_=&`u zGimCnI+w=G!!-Fi-d=m5$}QoOKgf3%Oop$dV1)X1X{j*3)pq|<|_fy2;Q#ky2N`A9{g!cVmf#04C%$0 z2Lc*Oy1MQ4aY_hy882Uc1VVP;VwZ4MZv5LFWU6%a*~K`;F~y~&#lL6n@42L^N=e__ z4=8S}YfRFhqodoteY=aBX1c)#%$7U}5cFKIfXTUS3-g0%*is3*68An|UYaSglHuGI zam-#;Utda4@Ik=uw8TiYikg~UH4|MklTk5k^WwQX40x!>YG5$B@^jnk-rra=nEfIA z=(U?OmeZ_qliY7#<0VM+oF9XNE1lk#gc*PN;>ATB9SIaJD6NUdUB-J*c_Fg6JeI_AyStf{+=tREIWXN< zv9irP=tEi05ui0*9-eMP*yfDH7&oxI`-j=`zJ!wLlMUzO-YWu`}eQ2+!DOU>5UswI&TNyBv9VJ4Q3f_Pfjxm$JDHfW3fJrFAZ!_bBr_m!0RiGbMFnhc z;)5_56cS=~`SN9iGy{XtsO5z?#L(ZhQD^uF(XqFs`if?|>2k&@4n$oxHO;b?ta?=NB z>Bn3OjC`8!*(Y~0GIkVtgat>5I|;OY!7VsBnPw0iBkyH+fBmY`G_mhF>ix_!F8ta# zI4wtQRGdUtaC}P2kPV?L4CpWAwbwb4&@+FjTGg+A{}iS5Xl+9H^HM%#|NApQvoUCv zMUfCZd#2R>ZSv~sjOX-cmj3>kIDXs5CxBJ_>9V<{U4;u`h(vz_TKeS?EhQeI1=T_vWU!xN6)H3Oz+64aCMTyO^0aGU>3OQ52> zeAi>Xw}>o-(_bfxwx5tYRB`iXAT!qAlBnC%Kxxj47ca6hGv}v=t8Ox-=@pz+QhMO; z59su>eJD>iUM++v9fbn`>VndmHESfBN?KY%0_cyqO+8X;^)ZWbHCFHJu)QZP|QZY1q*8;tEQn z$?$fPc61b7X4UWi42HtO)3d$EOX~P>EzWHiWdC6RU){I1T{+gRicyl*ID?5vsn_9r z_qnf>di*lib4GqGa%uOyiE7B_b@~} zeE2@H4^+VKU%&3$zWwpz#|2y}`N6(zzKAFqsglLla@8EJ@un2nUX^-KGTm2q>(9{l z?4;3mii(QAGD`t80Xk%&{op~i{QF1>R{7yo|CGF9_X zM)Ah*>#@ci)TAlRCOiBP9|Tc!2sPT@>gv?RCeH0|s>bhbdrkl8ESe7;?CT?)IrE1C zeJi~aRk1koUHba_Q;O1sn8xxb$!t6D`HbdGjWPZnywoA`KH886b zUg+%s9-ez1Vg9FLesuXJ#%AL|5q`#iX4%--=nvgEJuCPc;klT7p zYE!tk`8xL{x=j4)t;~9o1ZW@Bv4>~d=D&h7^%pAK1PSpwd+3~7Q4QYTb4(><`6+p% zqreh_+uvWY6fWUnN1_}bLE7*{-dH@veEfR6tsZySLIt~rEigxBcJ>M9Q3GrnJ3FDO zHf^=d{Dk;*UN=?8en*URZrgb7{?r}W2W%capBTD0)wm8G^rg?_f1_Vb$;egtx6#h&lpR4x?u^AXNbt6+B9SWT{lw&544q8J+ z3^bb^?b_L#@jKD{mCaX)9ki!0%Q#$Jk84MKK+LYMp8$ClCTiVX+QMibyZ70By-Zmp?Rw?3>r9Y~D>yUeDDT>FJq7v1oALI9iBC^5KdCoK&N zy|%LQ`={;1=NOJc$L!C?H?BPd^oIH;sNymM14DC~KGT)d>9Mf{;oX{Q&dUldTP}=e z?DX0c`Sd9Y^CL?k^MF^|7`IT!H<22$Ej2`!o=Qotl=Ui(41u;WZ&4H=Q?Om+7OQ^Sz0)Ua9^uc0_BDcW zlR(-_!1}@V3})K;nx{{mShc+kRFfwLj<(&PP~GQ6TzJ=kD!rEKHuXeasQh~W*H@t@ z|4e;1c&T#muV+MfxG1XW?}>$?I+@n3qB;8*{R;B)5lV$cM9Lqq*RtK>WoM5Ovt$bv z(Czl)SW81Qc7Y#D@bl--MT^rcZp~JD{-YWn!5m91%^FXOw!Stm*+#n|>sZrq<^2t@ z3M`VZZ=?-r)*&#>Nj(R=*u*ZGj}6|5y={5qXp<_~r2DMmvr)*=I|VA8vF60sc|T;- zib_dEy%7V^jIz!NM0$*J!^q*nM>Bc^W!_y(qdBd44oL`&bnDxSyrR}q?_p&P($NWB z6y+CF^~A~!g^EPm4ZKk~4}*dn zdMkGtx)^2v%lb;?(r(!BgQFG1RE=oM4xMcuIV8b-OM1+wTX#sMl@86{n|1f>s(C!q zMFCQ#vwd|hhWwVmOofWs2!s#r)8SBf%a?0=k1FoPi;|`_9M6CJFzEP@G(|S+s`f!R z(|_j}V9m61r}ei?AEzYAxt{HM{ts?|?P!#6<|Ga?t4J~`7htRAv+UWi<70Wx0WPk* z#iX{Df@Y(vx4xem8?%+7B%zF8W4b%vxAiZvERdftNNPH~y!gkD;8-`p5kn?(T^wj^-mXh4;=Un8Vr!Q%bpP=SVN*3ui@tnUG8^5Jw-M?e9)Q9+EpD4 zsy#jKsCz|isLE<){Yl;7h%k~|`v*1CuTkv#N0)3beGaiJ>Ts?u{Q6kf`n&2;aR!2g z;pmSK;Es~nGcmQTZ)}2}JQ;0Z0}D5FBQjmEr>pC*!F%sSHm^o4Al8pYhyU(;hj_1% zrsvTAwYRI}Zhmcv+sU)tx*X5WgNOz;gl3aHP)_6Q;sW6E<--Rb5AG=8Bfef96P;~DQ@c{IZogNuIDJa#y+}rdd#$gTc$`V*lle3e+QD%EdDn6E{TbK z1Z4(M412p&NMA_Af@g&?N!iOdy4j$M@U)3cwz9Sk+Oqab(Z2N|Ksh0mK@xHND1^n@^Uwm61fs1{l;vcRT} ze2I}6V&c@lkxZmK#HZu9xUlebtit*Ed9YrFMK68hLqDW~=9X}q=A+Xjojx6;U30bM z4t?>~-=6|G=9qti@w?0-aZrq*vC)XTEOM{Z2;>J37srnK z5*o58VRyj`DoHJ(0xJK`S;eZHTCJh)QF`Pm)Ff9ox7sMFs2MgN_DnfWW}(Y+?Odbw z*ROA)r8PQtNLE&s_9Fj15^*{}^U|d;RT``h9;Z8AOLK9_$>(KcUZjq^2H`L}_S2oO z4CSUhRs|z1*tP9T??ewDW?0u?5rZOHCEh-S02Ff#%p=Wu5qj6kdao7mCLW{XZNnrf>QPNCPXd;biF8)f5@T~ z^0}aGEtTX+nOz!cTxE$+BZ|bk4BD}7G8>D0l2cMVJUr%}+(SZuW}z2S9=Ti6-C0?A zYm|rbSeSKF@;6|~mSW>Jz>&Fksj-JgWA`s8BBR44VU z2eN6KgFS|=ZX)P|(ObWH&(<6l$6r`|qvgNaESIf4A%+wysh}XalzCf9X7h#(25SyK zv7&&rJTT0Vc#O;Z?+Joxb9HNZODOoy3*a^}rMw%-7c-(}wGML&!U>_w*h_uFWUNv( zIcSu-kdh^^hw^k#MYZCC8E#cjKT*?gx;J)oMEYov<-iq6xI9XHThF7!$0&aEs1?Kn zutCN71OVj3*Nw>S4^m3y)ZCdD+;%83{*2lvPLh!^hM-$~EfjH`B79lC$V^vNdoyBZ z%JB-~RJ5e9g)l$8YBvzYcCPcv+&d5pQD;JrgMy8C0G5GALxt<{x9{Jv8oN$40l9>V zSUxQ*T!Kb0yL^I@?27)5h@Uxg#*ny&5Wl6gw3H&|kN&t38+!%CB#*#eB@zt{4TaC( z8hPXV0Dmo%)X#_KJG&$P*k4)T6C|w{FSg`g|Opn1DiQ zBJ>OwX@4hHm7rcX@w*n~((+_~JqYQuuT)H$gf0smIf5WtU+D2y546U)zgprZCMFNq zr3#(?MCu6qX-WwzEc7f*8wXiAbm=)XC8U6bUrZ@BQ_Tj@iwyJ6n#5D$zlK&KfBSoe#Gq0__Wr8vKl;P1?z2gn^{W+6uWj&ewU zV*2tP%+@l<1qk?dyyw=e{y})xM`~tOSJ!z+Z)&=9tG`sXB-03UC#W)S-TFQUxH0K_ z!rs=SE81S|G$58|NnHE z)o&1#1<5poctOz3Y8q6`{Qu7z{m{BDcMVkow6UbbBtihA7E=TJ|N6ua{@d67^HvSe z{Lj1kcW!UjlYIYv{C_>;|GfC>&+$wjDW)~b(LiVP|A*5`w{wHtp|bQEHvEF4b&OEM&+bgcg5$%iYU3Dqw6SOL9!z`oN7s)@?n zo7pAX9*V4Aog#-jn$p8_fB!-ywzM4FxScEgM3mRkvB6gG-34D|KuM9!P@AAW*+&G1 zL3CrN1GHjJY+C((^vG7a_yS}DBJ&AX;m#K^F^1OG3M4g!?R{`IFqD>+jh_&+>EI+n zBX>>VS^W|rE@gl=zvR*5$G-8 z5erojCfY3zMkkX6_Q&}8$`^SqT4;GG+ryfn?65Ps?$rO-#apnx?}MGPtin#;#4H@o zc;F0Q^fcfrIbJPEy*R?UHD^BzS$h5Zrl+UjSiu}X7IOcMDx->KhXs$QDC56v;9Uk9 zlyo#c|LQ(QWw+##PEhps1kKINR9!#CDuf~O`-1H^1MFfF(7{hFx%Q^W+2IipNqG-_ zO7}X=d?&dQ^!!ez5eC-$Ket_U>>VJ->wRAas+{5F8tM7Or0j;JKzganeOnyVzi&K+ z>Zk$(9!|f$1?2|FQ&34>NN2!!40XUN$W|=Rzy6zxY06xHj$^ps>Y8W!8($z(6!)D~ zckkZa9;nIp>l+nH5csA@L+2{Mo3d$EpHx}zMF5R30kKY8{N4Na@0CDsKw#(R z;Tazr+eZWr0spC9R#T%8qr6AL*|sI!5JrJ3y-*R%t*l^>`vHkIKAxM1rTsX^F{rcj z{SEqwJF6#`<`*8<^bQQH!)RMxCl?hJy?gggXg^ABaLMu{s728E_QB!_R3p^&4Z|bsY$0^sx(84g7 znVVBQGpGF+MNUA=83*3n=1ZEB!J{3y{Ap`%6-BoE>a*_O)?=2&ceY+wURn$~sIIBG zi-pAvKj-I56i(nlfRa89|4X6)O2+qTxL>?{+2bczxPhKNW%esD($;@@*}LpayD=4N z%9xlK>>=3TK!l;YjXRYyP}^*+LtIqV zW%&1%bL^Wq9?3lv(FsAaDpM<%g7mNjT4Jj-~u%Q#d z;PkE<8rH?gtlz2r@50fM!oM`%!x=}>A!1@K^e2H3g}KTU>Bro>|0WIH!-HE_uiQYw zJh_7%A_-sq^bpWeTT_$5-5NcE7MY@xoB1K>-{eON1sr3PCfVh-HB*jYGK?Tl4=Hpk zd^Y%WLY~FH(MzlgF{Z+87J?K7;eIM+FRWu+k1O&E3RXO}m6Zc89!L&!78TiwocuQe zvT29QsS)^aR8_)#bO}ieX$=lo6QSJ6pp_{s_tSmHi;N2(U>eu6a z%l6P2AUTz#x!aHv z%q%S}QG^&7eNDb}M6L1PIi=N@?fDF_7$A~bi$nC&*7lmLI|J*Ns&&f0XHY$-`}E6S zXx?m6o(rhopung#|BH6gLCh0xy;HQ`z=)yu*7l@8@EKIGr%$^$JCjMzVG^d_E%dRt znA-T?#*n6`+!=}qXwrq?Fag1rr<(P#QNd=aaqj?Uf`bGKQy7Zt1F5CANcIY$!WSI= zO9#xSu%r$#Gc&I)I#?oyn$a!Jw+=aukhcaOr6sm zr#XbW1_}tTMk;`Zk)~$Lqy6V*&mnd~r&Tp81TSDpaxxfbHw2ZKn6Y2YJO>ZfH8dpGCE(iRc%)SuPltae z=%oxJ6rCQsW6PKj9Clx#Pa=^tHKk^Wd3F{1czYAPyu4tb#Kr?Ox}>S8dQnnJ3jEI^ z#{LS&4$f^Au(cmh4A<0{`VTYeVQhuXzXDd^Tl-*0LDh@Va`5zpuN%|F0O#~oc!yWK z2S0#>aJ#(x`YI}!fN&HnghqzSnwkK(tTK#z7ME#rr=ZwnM&R zW7G3^hPA_R0Xc%@rR?Zc_#NR9S6-tNk1+=O0Bc6HyNj{$PcZk~`W>B}`U1fa%(J8k z3?55!zp?huDJmkC>(N|T~IroTb203m>wF~DiR`W(U`DCbbr z4T#&2sl6W&iA3^-3~wS_bi4$0=O-)V6MzF30l~Due z&F%vc0|5g}4;%@V`a4!8wSxzSf7l%~9QdOT!)I)jZiz{jR%o2eaEJEFFx6Kl^Y$W7 z(6&1GeR!XO&3Ifz@jn5^z-lPwM~8gr1)>aA?M5AL35nwRth{SyFoA$%Nf&yl0JCET zc%)zW{3|CZK=gBxM%ri#`@k3ccXs$wYwO?aUVU-CS3CpT=yrj{1rr7bw)ShY3u@0m zvo!XFCm-pA`qA|nXky!iS3emrg6u@lL7_)XH#2~My8?GWX=!d=-Ux^txJhL-nC=Ax zoc>p$MZ=YT7zWssxW{6v5$e{>n`oE-Sp-rRZUq-&=9@R{;*QAxdtrjS?~gA8tz+V0 zHF_8s`B@ayBjTf_fq}A?Rvut75F5p<))0R|O|4?3D3+<-MJ4j_xdvg13I#Le2`Q!I z!A-Q@d5!4T@Z^BV0T3sXB&a`VP7|6fJ`_PQ(Udaj!t7|8TwDj}}a&lXJNxy#mvZ_T3!>LoJS`2Q$5ZMYBeI4YCS$P4Sx6&kx znbqr6T=~A$7&&v@PEBoXLHJ5$ZVkwzWCbaUt3-tJ3k$#QX4!q%=yqJ3DWsGLo$mIp zA@=Lld$9u%4p9YR1bf5-{QXJ93jv=gMjlgBrd_*c;dFAJ?~g;$0lQ1;fvq8n06RZK zPOJ}*PX6Sl0=mq*cJ=-I`8YCC()P!D=)w?gBgiNX>R-w~KJIpR_4yrQUcS6d#$P8V zCtD)nEC;}uou6MvLlbfI+H(Y%sq6hHL=ZfbLWRvS@iv~K)3Vnc9AIv%ntmAX5@Wvm>kbJWxS#azf%>#zxi6 zwrIrIQ&Uq92r??Oqv0mQuw>oRZ`7-ji<9*aA3g-B1#BCiZbY9pR!)ryt)#dZi+v3> z^{gTg1X?zbv!{l>O(-aKK=wmIfuPt1k=o<$G^Pq_W-&G5fA41Oiy|}d0)g9qjfOC_V zi%XU#X!EW^uuLSQvRG(AfCXI)&JaQJdrJ$PY3&7WE2t3uz-gRkVBkBV5OI8FW_d8J z2m&6|$>E`)S^P6Q3nlOYirVjn^?~dHXT%ZbYhBvY`#Sy3jXc( z6P&#{2m%{jDR86nx{c0ZC{p!{BFR{h-ws)W07p#8$Zdq4Vvt3EZ4%Wnl*w#^4>z%v z07=PYL;xJXv!D*>AQHiXPlRe|XlRH!@*0RmxbI3)S|ar;h%TYpsjJNQ1K2<*NHp@8 zfoXD=E|b)_g!6~1o@RHY~# z*ano!*-JgNw;S$X!5LNdl?50bE1>Ur*O)4(va+(;xxVShA3E~w6(QGTT+yy2cUWNeWPpZi4;AIA>$+!%5ynIMZI)`8vw`%Ra^EPO~>Qn z=HUd(Ebi*+g8XpgN_G78x!iU20A{Bk-7>{)jE8flIS)13p?{#zSp)5HDMr*qxH`7u zwmQssuiYFj;#~|%ttVBoCR}2?6;Z`{KwP%X9Z$jPeOM&Xh$obd%AKkr6 zAq(+K@JY_QMW5=;?&@r$96{ukET`DyWPjHE;Um^&W}j-``?H9p&WpvTrPcm+vNSh$ z82&y5Q_U4aGSuh06bHa1SwgH$XCcy@&@(IWMk)!DC>i0Nv+}%+zNE0QR*E0#!+Q2l zy>?)D^qv9nrXOQCf9={~2CS|ODJ=P{p) zsnm9#aD8pdN<}ovA|RefnpEy+szMiDZ@Vt>5!||$q_15Y1KomHOa`kM4@wN%`Pbk( zl!qZt`uuu(doxOWSRHb7H8nrYP|PFq6Pj9Dko|JL25a_W3Iy6Jt^{Uz_F_YVWWbaZ zAZA0E3=bH6Kqh~xuI417Zt{GD_<|)r`j|{2Ca7wus(xgABq-K#l2WrqgMO5_W)cAH zvT;OuHSsv0i=hAaZ?N4QM5Bu-*dsjE_oC1+l8_)z!qP##end=+q8fhFA|NXM$RM0J zQ2_rkZfV?B8awIoHN*py=cn%zfgDijiUu%G)cmE9O@PRo)yclIn?EK6u>%Xmqc{6laf8bw$?osI&r zL(4E`Lesf*a1@I1@1CCY6ZkFyJ?Z1q1DEG$W`&A zwB3!LtE#eca@as~R$Z^e=rgjbf++LDb)=L%?2HzSlHV*aAbhter z0}PLJ7Ik9dL$8>t5-geo1{@zJQdA1$;H=3d`0V=8paR3vO4B-m99R!P9x0?ws51ox z1?ZFjiwBCJ!tiC;ZH3sio3W6(~-f?kp@811Ik5kQAgk?$!D&9oh$hWPQ zi*Ey+hA^HA&1di%32LT$4?hFOpfpF&ZDJASJ9Nkv#r@DJ_r;qJBcSc`b=j*{RbOvEW;8Q3*zYxQjk@6m zkoi^yzZ~j@|0(S`w$M6)dQD6v4}idgK?uZISu=x5xXliU^(PTRt7t?zL?I-=e*fW@ z-Rk5MyuWB4zVMIeATV$G{}LC?Uqka;`D*lMJT6|gkOqVewV%nCl$g4?;So|0mdx36 z=Kvv4Y&;*xTfI=eG4KNR)L*PFo*lG>AOx;{%j~Vu_;Kq_oPhmWbQ?k3ck2GQ5t{JI zSAMXf$yyx1i(>91BRc}$6kYFEVPOe_d4giWI%+H3xbrsi#o%jH@PA>CBNVGToL;?P z$6;XjB0w9kv3KvD!7$7&p^!Lc{|mUF28bPu5>N8Jh9`Ocbh7}ZWJ-+)=W=4|DjWY^ zoP(dg2K~8YtU*q^GN2CZAFzfJ3Gi4=p*K3G!9+(I5!AFgq^q}=(l=voZx8JR7Mv%% zNASOZ5kab}%;t~b9c*lhB%taqjg2X@iCI|_Fpm&9I9T%aMr9lJGyWJJt~qsyv}5<~ zOXlZTC7ciaHxZ}sSfmCJm1p%$sHlBT1tMD_e6LH{oloW9OG9}H1o~hbgU!LCm#D6i z(m!+qgMv^`f|%WmE^>o)DBl${VqVTsH^ z#J&!<66F;ah`wYqxI(gvgyV0bdTsd{-0K*Ny7uZc?g+=)5UjRn%^4ot=s?nyy~cUqK$f&OiYz46Iip>e`mKJYm`rei zJSlru9__uh#nQqY_WZ_;8vzS+@uCAXkzwOF-z31wgl;_IJV<7W03xVQF{r?))K=&r z&d)y#We&}(6QJQJFHwOS1*jTSxN~-yvM3D<_A&&potVGN?)jyuX&SwR^=r{DSYPC| z%)lYLcHO$N^75Jf`ZJ9pt8BRQyL`ldpna&`qY$2^rh5Nkhk(2pM`?!Lx@F6Q14@x_ zt5A3y%z8`9TMQI_1!38^7lZ(O+ z3i3-tRFv(Ifi&1VpcwE_ZvfL)>!VDeou<~e&c;_Y8`#)*fw%#%)6mdJPz?=qFu-MFpE_^4a14IZH zp?a(Q^p6z0|M8R9X4l5KbgR_f4>hI2C$kL$WovK@wTBeva%q0R2`y`VqnHcM?tt1vG{ z)di|N={S$Da6?s96*Lm8eVB$Lg#O=djVFo1?~DFV1UV$o)B&yhMi6W`)O7uv%Kisk zj+fa`++2Qi2~~TjU@}B=<=focMGPlEnuDF9Xle9+wvJbc8daYvE45z3)W-R}(Boa~ zl?abn;5`Qip4A6+W@#W66pSPI5EwvUV(sKyrpWzhv%iB{6N8V%_&wsG!z_i9AKRbv zT=p1%71rTJ?j4jki((+C=zr(!h*~c1C@4Rz+xvjs%l^X43;BdQr&2hc6(@##+&@8W zkrK?epN?0fFtokll;6nU%~vMBluR1WPN*cCgvlp!nV;ppNma&U#G$wK;vtnfvRyo`;YWAUpA;)>R!=?j*gDr*xAnIC5#WmDc6}1bnabh7NbPM_xVVt77IiTYnpOaZZmbhc#6Aa z9ItzEM?3_Zgg5+@#o_MpdK2|#x3ypk-hf!b<~$!NEPo|F9{om?@h6az z01a%>41!yNlfXYM9Y`@kk!i;cxG;5!#8#|X($<*1AC#-W^&6nw*4_^OcqDHyRs2sr zG@lQ*EkUFN>^{OJDmr~*J)1MI6-sZMk(-Ffio}>$i~Wm%he^o4dGpHBH;~1|9Ca9Y z(&Y?K3QXGe4h|{5MWBd2<-0^AVw0dwBtEY*gX7a*YWj_3vtnAa#=PcgT&^xwv7joe z9o0r`gitMM_9gn=pF-{SBpYzI-zl$-c!$m!F#4$T9Q(hP*4JmXZKs|2)2UxG3M5OR z&|fF4oa#^jW(ZQ()W_{gd(aVsoI0?P8dRj}-vx8wP(!ppFbnqqkG)2r+tm%Bd=Gdy znY)`PPa*vx{fQPFGT*+!ww%>8R*aud};^QA0P~9=N`OmM$Bndo(s8) zKgB9VEmiWSK_>gqc4KvFu3&1uSY#8QHxE)?gL3)G70`|O$;m^4UUOB}Z`v90W`%(P zixI-=!w~WDt$`>#@wSy;y}i4&8f4ZYllsDH{e zK=ug486YG@PMH4^S4C?pXP?NIs=H`?*48uV+SFAd9H*vV{V3_?!wrqNKW zWWYLQ{3!Ur5jfe~AJLFo{j-K;haiN`HFr*Vt0y_&xr%q88Hr%guNL zl3`Bzz~|Q1wpG8DR$!A3-7H4obWcv})g!N8Temubz9rfrdt~{jIhmXPy1#P5FZW*m z((=Z8QcQma4>7L{RJv_S(dz6I{4e~gVKZAo#l2-Uw6rW1)_%y$6k1UpK+7QCy!Mn+Pb2O)m&us#Y8=OaR|fV+&?-P0os zVvwP3a0*pZvIQ|Er|Z^APSWJFpo+a1)o~_(*~Ba(Gn3NCPF8gdqxhv99dl$~^w+(( z8&iiDO|hzG)fhTDt~tFLvIjfF(=))1`^rIK^=E;2ak>X7B(Q_up9dR-VMmT5t4?iP z2IF{MNvYW)8*t8JD5KoU+A>?fcxGh&&Wh#1n<|@7kLpU11i}6Vn*cWvCadESiZALQ z&L=*l_`tqrpW|o58&V`&=oWHOVe)(Ac(u9D)wnQ=pir6AC`u^4yNlhJ{ zeE8BCFbtq2G(3>;Uo{Ul!y1PThBxHI*U-QO%&TV&D-f6lwVG_VHw~{%R~fbJQ&_LC z+2GZg41w4qATJr}%!EOv!`3D?Y2KU~p_iudU?;>8R{qFZ!>wTZSo@YJR+G}lhf3E9y z{eI{99ggpD9H$s`yS)a#%onaqT*HV}r#F6|E9`aUF~ z@M2@Ax7T%)A8hPi-J{U^j=_3k*=lk~6%HyI$??{X!+)&@^Ibk~xXPg1|Kzo+=T&?uvdvfSROGxH()fp6;=DT#(XZd% zU$LcP<8#*u>zt~#V|PQbr+l1&x3BEiLg#P`_ODZHYHoDr$+TrD=NhAZb(1)6%f5Ox z9|{WdcQ<6HcKQ8qn7ps->&iLG$ILYFuKP5;eUBlOED;-${hPegm%Ur(ebxr09ozM6 zs5vSwa6%JbYxU68Jxo*7L$&OWl@U8-Y%tS|d#oa%DAv%PZ0@>)k<1xZre-w*0n zJSuzh@=`&MA+pCCBNr$4bkTrTK94GLE-#-I*tM1P!MX^gE&PW=46F z{Cr80S5fS_5uxVRJr9gOsyd*9_&x^1Cl8jB822a|bfo#&%WWG9&C{QoDu2#faLXlZ zj_eB;O&)w_CG@eCt4A3T$7;?WIlE3|p=w-a1`V#!5)3~Oi^_5#Wt{MYz#`h>m4f4$ zmx0X!EnAmR2>TH+b4WcdCxI#^78VA^gCB{$?LbDLtN`FGs>rT zZ|zeeqJTa7y;z8OW3%7@)4X+2`%_nEXc&=hdwcV|PAxUCRdWtmtkk1#6NP#go6N`( zi-tFmKR5l+`I%tsJo0_YV*dp@+eT}DO=-3>XU^jUFY^wbA*a86ZK5Fcm@hx){vO9q zF@;|pAG{jvd^5lBL)!y6^_}K-U6h-hkSEnji~Rl~x@P6#q`c-Kqk7(1xzXb3#zTi< z5&k^)`<X5|TmyB18p-A@wl^~Sc~ z^{(LSKNoj(&2`*0>g})jA^CA#USEkgsW7pKS| zi}9w0lB0v8 zi&j=8_kOrPwxsu#(v#OqF6q2@8~%M*a`UFmufLNle=%iYm{-0|gX4qj>(e_2IAzso zoYLqJUGk}u@}Q`1Nfjl#Pv~8&x%BL5LT4T4E$3G6`EqpQiDlxZlq76zzrZ5O$7}zw ztdAQ@hr3SSoK$zxY0QC*Gmp8wxeR9_wPbnJ63sa8e%}j^F1Y>mo+6|X3%6FPO6s~J zVC>SyoOl%F0$W91`7r;@qI+kx3{aGukR0!M4!=P z#vJb}1IWC?iNG#EAcH03{~XQGK2VRQ(4y1k+FyGl_KDn)9o7cvYd36YqomX^08l3C z2#5h~liwpi{^wm}74V&dU%PGX7YG{==CN|+uU|a?b8)gZiTM8WXFV-f_O(?`6`y7A z*Lkb8ff*yPJhNHj!hg1Gr;NJ-D1QndcS7U9PqRgw+;G5>2aKl~T|q2(9X?%U{cc%4 zyr`Mc81*k|mZ{5CEZ_Pf6la-5+TkI}fA)@CsIA;i^3*o_l77Om`+&Dith_O5>UJ;R3RL z@{Z1s4r*zDkk!VzOCOX;{+I?bF7WR$J{RQ!km$pQpBRh`vFg|}-ad%?1g#lZ;74iJ z7hr)NLl^xGoy+>d0D}!-_3)S&O9R5ryAWKqZN=@nZ%>B?4y~BPwepSKKZorG&!b!5 z>HNtsn?;NH;>M(LSN#4c1f2m25!J9E^C55vj7W_>UP;maUR9;z=HM{YZew8}3SDIB zkDU`Lcdgyz|Hh~$OoN~)R*4U2Dm(**CZZT+_RY|~!)3*D8k(9X=|~(Mr9LoKp@RH>asfeI+}^T@O*U5ESFy0GDu0`mI%PwcJ^;e$Oh+#$ zY76$_L1h%&H{Sj-x{Ru%Pc)ygt82%R8EoBh!ZRI35&p{H&HZr-&tK3la`S;4b=Q6{ z%p8VK6$HOTJDQXwxvx{}_zGxp5anNac|~WLO7U(f9f;o)h!+S~4F9G%gC(OeTxH1e?dMM|4UL1%pJ+MCKi_9x3Gj<9 zR(o$koNxEz_A(h%-iS5^Mx)_J1{5WQ^r;}K{aYWly*Bg5YE!3q^X5swRE887b6b^v z13x_P(80P5M;LI zT3uelpFB|Q>bE;R0Nf7y;72e{Q*$MqgGZv>nKZp0sgsx<(>5OF*1l>sVl08w5XPqc zyU6l%R4P+kixO^vdwe`d?6Oh02&;taNoXt zLXU`7I?GOIG-1bIw2bZ)KtP(@ed9-jE?jkYgl!G6UVj9A1!hg)2BO|&FfbG@`#`I8 zbgG0=dPV#f`pn)E;B(>Fz+-8Vd}aVVos&U9HJMfm1OYKEZ76hL*m+0(u|UDM>pVlw z-W3@Q7uLsmL&M@ChsIACZ$1QTet5HhLMj0;07(6`@=<2Q^%SVwfM#IyjP0yrMlz}f zk0-!Ou}0zi3`0A7Pl$pi$8EA4T+&%NdFY#FhvlkkKWgIm+r+1V(jH#3u#oIdrz zgiu_v;yKS`=sT?}6t+mFAAOlWT4##vCa%8ydzmt}tvajC7wnB3lK0OieTf~!Zz7j! z+htfEEv<^UEIam#_DNz&5WGCE>ipd$^V@8P;5zg8Fe5|mTyMfBmSKU+WR!_#U4&}& z?sg`@gC!n`p8QPgyv_*7!O<#*FRu7zrw3Zm4$5(+FAQ=%pKX6`!eu{egDb$j2EP-7 z94@Z^WFoTgs97@{20K2}dfC?E@rxJ2a@pu(pq1TktQ?;FDd@w8E?vI-7nun-bXNKC zm7$i}Y=2Ac*pu8`&u<~<#HI!ZVF%^$z74mE(Ch?tiw0aaC<@GTbLbs!Kg>dr`LOnC zhAbEB?0PyJ6Hy&&8hKf`X6k7E^m?8rk(&rr%h*0>)X1wnOVYD(4)O2mB)hoZkgejZ z%V9Q3OGK`wM9OrGn|@SF=PE_CC;P%W<|m6ot9N|r8qYsfR)MO!SeX4bA%x`bx;iH; zbYP9le)Ekub0mNTM#r(PfNdr%1V2;P-+aR|`cK)FlqYHf;?F;+uT!0I%y!EjTW&2XCAd8%yUq=A~6b)^d$q_X^JuE;Iz+rR&K zoHZoFkcY)r+=>njwPzs0Gv_;(-0n|I4eKrmO>+Q`gthhyV25GB&*JpuOejH)TOYKg zixFEFRl|4Cn38bgGk=k=XO$~BPR&$6B#^|jO}UXM+v5Y1lMfAQrKDs7=}kmOgwgDb zf+Is0KS=nQ?F8$=YRF@)5k9_gaw3d~BFNBiNA{74$A>L_LY_W9aubz8mFd61SzWAg zV*dSN>=)JBfl*#!SKLO@OIs}pHk8@i-SxY-TZW5Iw;x840nSLB#|omHseihl{`5!# ztwtoxK8ObZNK;2chevBUwI2&+(9d3k6y{9mIhdcFL0k}6F<@Ru+37|^*?VceIL3w7 z+|G`&+WCL|hxzLTAYv_L0Fv~l+?ld46a0NWJf)hfqrWIKOgDI)2Af@ z>q3l8+4G>jQC`hx@6n4FuS%=@d-Rl(TV^nr_c-?G)vFDx#s`C8CS?}8;GWLpV^`QE z`gSxRI6>fF=`r{C{ntPrQ(0KQ+745urk%%-YtBG#85VT zEzCCh`{BcgVliOJl-*jj98hXOD1%8dt##TE@UrP#ru8hWs5Xg7XBt z{**4D)X9a4*L?F+tZ>edm+LD_`=e#PzP1G#!TSkNs>tr ztVlJ2KFm(MNOLG0GI@r>sNNB$BuBE^A*E|BxSc?JiBl?~6u-p?u(b-wl(pLM#j7D6 zd;8A7RhmsxIs#D@1t3~3FaN^~Y<q37kp*F#<{6Osu%ssAP>)hY@^x$|k87CsR;4 zi-J(83zUr`^c%Dvjw6DQec1^nsYQo9Hzu zvpitKh;%bD>*kvLdl(dsf;pCGH$;LB8%(>o7_Cs*_%Lxhue_**Tlj)mXz6xWod1OiE41^f7Uy3N7nX#M|zCcacs~F+_EBwSRrD9r&~VChm^G({|mu z2?RdaWE5mG=-_!S=`$I(n9u6AxiscFVne6(%GkcpH`Xm^sL6_sy$$2(bAJ9>I6N#E zwg?vctC?2LZ7CvY=v~$ETz*)mh}^>q-iK&SvgTlC&+{8z3~0B4r8gO%t_pc z9@Iog7IJ8xUtPQPWh8w2+vsH&QEz}Z`JkNYlS5{bU}Lc|oNpE$5rVr`JJ(gb8xv>z zo@Uek2U|wFcjF^{aR0v1sw%4z+B9W)l#%>{ zHr+;tYURRs_OR-aLvdGlWVoYmlmr0pv$A+2ks4e~(Y+(yN4 z!Lx)?fQUm4k=gIXjvY-c)CQ=`s)E`4gDTdK`!=(Dvb5CU6{d{ipc-MxcGiM5j3=zy%%gW#l-yjWQ_m?>wd0Veu3+W>O_h|L_ zo|k>}DA6cmHW!BQ#^huHAtynBaI*Ze8VV(f;p$bCdTrfj_>ENmjz(n*77u#hgvzQ5}-XJ_Zp zxRb~GbW~A+%~nt{{Mx~g5XzKz9xA{UteVINoCp)yHuu36h%`wxCE^6X$S)1QaH@7K zF)t`4yjsOrR}mxG&f*XOWP58g(BAOEA;ORZY+i0)(G<^pq4JDe4ZDB?HIDkwU}HKx zd$8jTGMwQ@QH*Qn7Z*n@vr?H&qyq<1(VTm6P5#8pgNF}~SoTcSHG!3@Gg4doz(l@6 zvxP~l71I_}6r7mUfM;ID(_WKyMYjDaQd?L%iejZ6^;I5Q)~xvoGG!z_07?W81S$$| zp81pqQKjxl)W_3gq3)y>%Je{XxG2E8Wm_qgcD!m`&JU!!Bfeq#)O4P#Nf7pW2Lb{X zzHauO?G-)R5y~n;l3ho|E+l3{Lg9Wp{${adl25|IG%D{jX=`5Dgv~TYRyR2cCe4q! z9B=t1h&9oKXGHP!O$@2~lx7ul9q+jr2VJlF?;(^Tsu#X;TYVletqBSrn~KuX6M=z!B`{Pd&nVI)mr3xUp`q+rceGWKmqZ&;w9~*zjYDmc zJZ%ku1~XW&DNtN|rx39hxaaRos;`QbV861d;6ZDr(rnM;0*2AA!{gs7Hp^**TJpUe zySsZtnmCiXE;;J#u#2T2`}OnZ$n)Fbu%E{RGx$Pta)0BtHj8iK`-nP0sYflNAAnPi zh>3-m+STJWT}-Fl7$4XfBKa5ebMS+H{rg+#1Z2CJ8t!%L)~FmB)~gJKWY>L34fUIF zNTge|+t+>EEt8`qZ?DH%MqA`_QUXW4y*0Ib-<(9{mpqO@AKDyr$mQJ^z956F6{Ev9 zWC^R4=%k69U*v;EEXSl+7`pLb2 zDM9L&@vln4S?(~C-xn4xb#fBawB(6Rlm#*4*8Mvd4GhHQ%y{U|POW<6oqa-k;WmxA zWw7%JzLx%N^{efJwNCE^xxlva&lkM|f3sUQ?c}BYV$$a~qp? zi}#P~C!vh`!v5e97}7TMA3fR~1Vx(CVU}LlNVRGXB+S^Q(0tbkWt8QJC=r)yNFdsI ziu6-mTYEIRS)^@qY5tclv1txJJhqsa>|1yN?S%F1beKS3wUbs-X$$3+kD&icFTLCi z2`Tm2KVn*Szl6xhDTb_4_DJk)PhwI91ucPFFlM^0ZXwEDqrWc(y%$=x@87W+vA(j* zKR?KEeLb*@su~RQb+9=bP=3>A&KWF@1Zc6Vyvg-dZ_lMUup@49HrI+sx~PpbCy0BT z9sX+7$`QKZ;Jjk2Z7OaQv`N0*go;wyIn+T$J+-!LMK0X_hgD(_%r=SIPSBS+7qR>~ z%_355JjIfaPs>TYgv+O++qkNB^2$?Z&J5Rr057|@hW zoVz|{T!}k$uafuRv<=k{$CEm2W?uc3=ap1BJ-Lm7#q1PKQ z=ii_9P3HLe^1;&96ATu&uL`Bve*@ z*z9lI0VB9AH7-@_pldKHkzA&lW!2n%=lWoudi;v?ew#LJs`{3{y9b(#7>#f1+NzfU z5%aKhH@LW*FFCO}xt7CW3MewISDQ_ug_i+^fHn{7-O=wo)}P(3+JV8|2q|Hkb)K9+jY zbUWhWR!pxPnvVZL}*AOt%X6@|0ys;&| z6f5e6_3eA#J&`>;xMgj#5m9XSqEDY7L;t|o0J5P@{#Fqvdm9tP((jxymY>i(Jp$o7M5<*L){2_El=TTqZaQ?Z%i93GJ-#oiy4^MaD68>WU{l7mndAAVIbNHxiT>qK)W&C~5pM zTknmuHiAI)=LMooIEC{pX7LG(LHjASK7zOV97BG$`G5M;K-+%MYBK0aQCcBs)KI2G zQ|zqy6$sPKRD35nMOZLXIm<|&vJ6>_~Di)|9!+jeV>t0l=j2NjkAr; zG&VBAGAC$kBSok0qAz#OnNjh%mRc&$OK=~`-R9+e^P(1G`q67A#%4|L6u*mORi7j$ zpLx8UZA=@~jmO*{$8~jD8FRf&f^pPZMwPJ-6Ju4uC^|Vh?cHqg%W{GhCHujCUgUrE z!x6fhr|)`&W;V_o|4AWRpPakZduOY^{u=7m(jo3&sAZ{2mjn{P>*++%zWm?%!y=~& zHq)_VsmG3Kq%?0j#r?*!6aC}e8luMO*I(a$=T3=McR@M|{4u*cuG{KwWfrc{>0f=f zIF7NY8nMxR+;Xd=(d(aIxaHqHhe7s+qM+dXm}TzaURoDyqxIrT#%$8D(k^$lHLH({ zDrz;j@>lMN~!yWagi+Mmjlmb*7;6I&SK*Zg>5&>-{i z3DP9jncvSuSGHRA`+l5HzQvypf|9!AZr1m_(Y!@vtLMK}tY%)%PI6n{EcWu#gz>j5 zM<&#m#kCFXd;8b9E_NwBY%OxE|K7CxMt&g|^rU2;tNe5B$H4k}Pm5rS1rMVd7R=mT za@@^bCnw13YrnQVMm{@vrE86VdSAA8U0oxLk6GW@(gQ@-FX8|%yTC;ha_qp|$aV6S)0Vkna zbD-Vqpd4)ChVAM1M!(LBR9!(Ym}nVcNtB#jv%kkC2Bss_{C!aBofs^$l<@AmkVtmM zQC`qgv+zY)o@nQV*KdsF{I%v(puDQAfTOKBHhI$hzZAocoF=b6ez!HW)4#->Z7WWB z)o+Ze+*}1IbLNfF;_`SK<=N448pG@~?KKg2U0pEPG?A9l$dI|`k_v;=R{z3vyE{U( zoBmrI>xyn@%-b&A{!cEzyWXiT3`aC2pyPwHF0|TFw?f=gxe=|oQxT*o$vVy(E_eX& zEr2o7%CbE&TB`jD5mv!$1UcGll;Qv&M#)QhKgR3F{`vg{UjbVX&c?E|cCk;H`s=f&=;rC$;Xw$C#YRjpwb+GzoQZ2u8*mS3S_9{*q@HErU?oZY zjb>>)We{9j9Mfftl~nOta!0ng%FkSd9UzH^nH-Ms>YRka!+EAIW5?gQY^tc;1m-cV z1h4fiWXtWM;k(|lKNtLz|9wAP(s7f0nEgD`G~ejCdb6P3jd{M`F`q`+W$Ib}13Ty$ z|1J2OX8V66nxLSNkOdA7kvGp6d~Z*Wxn%wShYV!Dj3ETA<)FcXb=-RTe`Z1qMnBB0 zW70pqz4jH(+?^4kpNL!`;DQjFapSjbQ%K*H^zF$YNXL4dS#z^McMNArBJkO-K6aV4 zQfohfFCol2DRj^R`MI+EZT84li@#7IjzyJ3NBs6`zUXI9PwVvHq3Z|wVv%op-* ztWCbEt=2A1_6FW#2HV_7O-ozL6sf4q*|g^;$Dm^tbcdoghHBBD8z0#W9{edZ@RQn( zJ8Nf`)9KP8~b`D1SQ&0Od?tw=wJbU=(V|GQWzbiZ&65 zb}eHLihM7)6Dm+XUN7FylzY!32q&CT5fAYt#&Rr}2~s4ryp@bH>3wKsYnhqCq8D8T zfOAO(1rO#UfauETnvWj+C2k9#G{rOh*zGrpJ^le#wq5}Q2v^`ioHq{%w*0ujR|?$i zz7o7~b{zpk%8BcX3<*9)v3qSrdJ*jkbnZQV zeqaI696S>B`}JGKmx7WHdPf-O6o4BIFEJ`#woD6yJSH8pFu@DJF%32s+HG_+zCOS; z#Dp`aPZO$mMQ;?&bTISZp!f70*{@#_-YmA)R|k8H72k=2i)hhsdO)gSBp5cFU=M4C zLRv5^n$(@232{fP2zyVY$(DoDF$F34{s4iD;m0HMSI-`T6*oOdWSRpmUB?3gE-ii9 z+28mI=>b@dW@56TAz(Q+CYLrQKlY$0Q&}H4ODH(KV zRCF1r#zrR@t3CBJ$By`l!_++lpT_SIEm}!Mg_Z3e*W`$-U%jknmc5W>lRy>E}WCpa{7M)TPk&3TvqhFhzBmSDTf zZI$s6J4J9h;-nyDEY(J>Y{7wReI<@YiQGS45(!SU9ibIECl7=w ziUYYV$Lfp4b(hrJ!W&uVxWZ&#cliX|Y&MkxA9n?(27_&Ski3 zlNkl-t-OLxD$Hn$??}xK+UHCHYjv+tu6ZQpUVJrwOZ0;2JWlf#QoHx~nAMq1a^1{x zmF`-A?nC|X{IAY7**K{Pa$e;;_+LrmkEQO7Z06$wB5)f>#8vGw;BAfO0P)dsieiEz zHHp%=LrbDGn2oO+TtO4PYn=fGc#e)G_$93dVy4gm+MMedLYp2E5}WDxbW84qXrfMJ zRWrCuTP#%q;LAPzvY^09N}!W``24vVe3E0EqJ%!%4*ndNfrUR*q>zlrnx-~hW$FXI zZAy$VF_(7n9VfdMI(?&vbPjKcKFXbrkw!pq<3+4_kTH`}dMobTfzohnq^v%)9#!=^0gQVuaTb^g z+we>m4m@JnB}4UQaBL_Joo070042iVffxl6bR;-<3%#!xjG?1jfDa_=9Ncac6q~BK z^2!@O?CI~QMDRC}TxMA#T14UUls7a1k0yTp+V54D%mp*ACALRr3S=hJhM01bLH%ZC zlXjacjZkLiHPnwH#%gP)y60_O2gW~HxeLXG|Ikqy(_@>d+AwNBc>bOI^#q-FG$Pr+`2??hE=p8X~z#hGz6<-B9O zC;WLth)lmdC|jk;#3xP)?kQnGk{b))x+$G#fVGY#LiSg^dyZF~^X$sMHl%pf57*W< z)ltiv_r9Q@159f*HKqlz(#{au7;~$|N=ChFX+K(+SIlRk!L+)|>Rvq{3Hn+_-N1wL z(&9Pg>$aa;xb$1W59>peW&#(F&B9soMRh=XHr}WT;5V=v>Bdur+s*D?94fDtESim^ ztjSw<8OcOoLIbZh>wekg0}a6}m>c3o<7`x#0g6_bwch zDHS#`0?qX(jd9H$_#WaB)67CGhw}`XxGZt%X!*6b8aYW9=djGjdDh*4x9=ENlE2O3 z@zbYW@je#wWX@5)(y!01$2b4JB{#;aK0%`?*dGJ(Om|E+ELy_HIsqNShgmOF&-`uu0V}2v>oQA=`YUNqPlMQ<<+pf!oX0o zuKQMO#ky{2byCO4@_rkZFRwzi-m(`3Qqq#g2aVgxYG_SwwEmSxHpLud#^SMP(R%x| zIB(Vxo=B_U^oha?ZG7#I;xpM0a4Q+I_&kD{U=b5+BZQ&m$0&;p<6UjPeiBxo}@iro)P)@Ohm-)+-Pu?D3oqM9%_3J#C zAa@k?O=Xx(*Prl`llIwfwj9wrQt1zptXX{`8gxfxbAHY*XduUf^? z$R5l~U`m6DuWyn0Zr+deO_ebDxxpVsobqsF00X^p4IX5M&;gre*dMDJiMo4M0IHC zK0cAsS>Zdqx%VVIXK061TIc_`aJA1B@m`FkMr`zix{rx&DfJt%J!DaiaXx& zB=u-_VNP@|JUjcWJT}SwIvAQ~Q&cSn0;Tn!7ibHk7tf%V? z2=A-5_ehZAqCq+uGt&lcvu+-KuV>h{xf8FL@9Dd(-|TIhjnt;EKJ@5kZNZH3NpH($ zu3MkHWn9D8>UZDA{M!5?abt&&U!OE5;0H=Fu-b1uQe?0R zlK*qQo4=`TxAFFwLXk9ZeN*W)66CC4U1nQLPo`#HTD)5qTa#6nzK~s@Oll@Bg&f2! zIVY|8OL1-O&sFQ)pDDPdoURadZ{C$BH+l^j&`yla5(+ba z|6H_l#|~2Y-5Y0#rj9Fx+YW_lKP-ws`>A|m=Ux(ah(O*gm6UK+JqG9YuKiprY4G2G zfJAT;RR(jLHc*NO4qQP7A-7PKt_1}&*66GV#o`qqv6u||pCJqi&P_8hpMsR|`S=FQ7``Pjjv$B3ckRAR4v8f>u zq}1gWEx<8{xo(!0M>=bZj^K(X379TlV@n<^-a!ppa6f+2K+$Fk56IXh#!+hSI_xOV6&IP3C^wQ)(U3Uxspfjww0 zTZk}UUz^v!PHN2&oP%TWSt|eZNl4`B;-jAD7=DByY-!d+6lt7Z=~Y+I-Z)*4w%67k6_ZSLx;uMs`%jx&`QDt-pp+kLrBn^Su