From 685f43dd6d8470992c3e74b4c14c133e74789796 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Oct 2018 13:44:28 +0200 Subject: [PATCH 1/6] [micromega] call csdpcert using path. --- plugins/micromega/coq_micromega.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 44bc20e55f8c..d2c49c44323f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2141,6 +2141,7 @@ let really_call_csdpcert : List.fold_left Filename.concat (Envars.coqlib ()) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in + let cmdname = if Sys.file_exists cmdname then cmdname else "csdpcert" in match (command cmdname [|cmdname|] (provername, poly) : csdp_certificate) with | F str -> if debug then Printf.fprintf stdout "really_call_csdpcert : %s\n" str; From 79aac956aede707ca816360849bfb1ef910ec484 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 9 Sep 2020 17:59:37 +0200 Subject: [PATCH 2/6] [micromega] Migrate from num to zarith We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte --- plugins/micromega/mfourier.ml | 1 + plugins/micromega/numCompat.ml | 143 ++++++++++++++++----------------- 2 files changed, 72 insertions(+), 72 deletions(-) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 3d1770a541d2..1c0ddd502a68 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -190,6 +190,7 @@ let system_list sys = let add (v1, c1) (v2, c2) = assert (c1 <>/ Q.zero && c2 <>/ Q.zero); + (* XXX Can use Q.inv now *) let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in (res, count res) diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml index 4cb91ea52092..62f05685aa48 100644 --- a/plugins/micromega/numCompat.ml +++ b/plugins/micromega/numCompat.ml @@ -31,37 +31,27 @@ module type ZArith = sig end module Z = struct - type t = Big_int.big_int - - open Big_int - - let zero = zero_big_int - let one = unit_big_int - let two = big_int_of_int 2 - let add = Big_int.add_big_int - let sub = Big_int.sub_big_int - let mul = Big_int.mult_big_int - let div = Big_int.div_big_int - let neg = Big_int.minus_big_int - let sign = Big_int.sign_big_int - let equal = eq_big_int - let compare = compare_big_int - let power_int = power_big_int_positive_int - let quomod = quomod_big_int + include Z - let ppcm x y = - let g = gcd_big_int x y in - let x' = div_big_int x g in - let y' = div_big_int y g in - mult_big_int g (mult_big_int x' y') + (* Constants *) + let two = Z.of_int 2 + let ten = Z.of_int 10 + let power_int = Big_int_Z.power_big_int_positive_int + let quomod = Big_int_Z.quomod_big_int - let gcd = gcd_big_int + (* Workaround https://github.com/ocaml/Zarith/issues/58 , remove + the abs when zarith 1.9.2 is released *) + let gcd x y = Z.abs (Z.gcd x y) + (* zarith fails with division by zero if x && y == 0 *) let lcm x y = - if eq_big_int x zero && eq_big_int y zero then zero - else abs_big_int (div_big_int (mult_big_int x y) (gcd x y)) + if Z.equal x zero && Z.equal y zero then zero else Z.abs (Z.lcm x y) - let to_string = string_of_big_int + let ppcm x y = + let g = gcd x y in + let x' = Z.div x g in + let y' = Z.div y g in + Z.mul g (Z.mul x' y') end module type QArith = sig @@ -119,56 +109,65 @@ end module Q : QArith with module Z = Z = struct module Z = Z - type t = Num.num + let pow_check_exp x y = + let z_res = + if y = 0 then Z.one + else if y > 0 then Z.pow x y + else (* s < 0 *) + Z.pow x (abs y) + in + let z_res = Q.of_bigint z_res in + if 0 <= y then z_res else Q.inv z_res - open Num + include Q - let of_int x = Int x - let zero = Int 0 - let one = Int 1 - let two = Int 2 - let ten = Int 10 - let neg_one = Int (-1) + let two = Q.(of_int 2) + let ten = Q.(of_int 10) + let neg_one = Q.(neg one) module Notations = struct - let ( // ) = div_num - let ( +/ ) = add_num - let ( -/ ) = sub_num - let ( */ ) = mult_num - let ( =/ ) = eq_num - let ( <>/ ) = ( <>/ ) - let ( >/ ) = ( >/ ) - let ( >=/ ) = ( >=/ ) - let ( / ) x y = not (Q.equal x y) + let ( >/ ) = Q.gt + let ( >=/ ) = Q.geq + let ( fst - let den x = numdom x |> snd - let of_bigint x = Big_int x - let to_bigint = big_int_of_num - let neg = minus_num - - (* let inv = *) - let max = max_num - let min = min_num - let sign = sign_num - let abs = abs_num - let mod_ = mod_num - let floor = floor_num - let ceiling = ceiling_num - let round = round_num - let pow2 n = power_num two (Int n) - let pow10 n = power_num ten (Int n) - let power x = power_num (Int x) - let to_string = string_of_num - let of_string = num_of_string - let to_float = float_of_num + (* XXX: review / improve *) + let floorZ q : Z.t = Z.fdiv (num q) (den q) + let floor q : t = floorZ q |> Q.of_bigint + let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint + let half = Q.make Z.one Z.two + + (* Num round is to the nearest *) + let round q = floor (Q.add half q) + + (* XXX: review / improve *) + let quo x y = + let s = sign y in + let res = floor (x / abs y) in + if Int.equal s (-1) then neg res else res + + let mod_ x y = x - (y * quo x y) + + (* XXX: review / improve *) + (* Note that Z.pow doesn't support negative exponents *) + + let pow2 y = pow_check_exp Z.two y + let pow10 y = pow_check_exp Z.ten y + + let power (x : int) (y : t) : t = + let y = + try Q.to_int y + with Z.Overflow -> + (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *) + raise (Invalid_argument "[micromega] overflow in exponentiation") + (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *) + in + pow_check_exp (Z.of_int x) y end From 43ad95fc6723bd82960b15dda708600073fc7435 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 10 Sep 2020 19:16:10 +0200 Subject: [PATCH 3/6] [micromega] [test-suite] Update csdp cache for num -> zarith migration --- test-suite/.csdp.cache.test-suite | Bin 329899 -> 192943 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite index 046cb067c5704d6e206cb2bf01bda7eb4cb689bd..ac5a25bfb9fe09e447ad548d2d5e8c15831c7e1d 100644 GIT binary patch literal 192943 zcmeHw3$$%jdEQ>@+$)wy9uCdGWZ0qB$W^0-3mOez_Ica~C=oki+L5#+6i^TZd+~v7 zUN$r_D&brN>gX6Y`zA)=Hns|ah))s|o7UD?`$*#hk*79E)8eaCxc&b*|M`BbIoFzN z@3r??XN+_9*=w#fAOHOR?|;m>*1GzJ_kLnBnLH1E@#jqVJ!3YT?RniB4qbHKl~-Ij zoy~69o*kY}4^Ove)9EJrx;>r3H#oRConFl=ID=h2nYbng-KV;X3*RV_Q?-5q9ssef#EQiy@cv!=%5-}>#8+H)B$iY>=!aGx)G?`RC z3Y~eup^MJH?7Yjbxcst9F2CsfL+8Ej&=qgI=+HJ74qO?K)%MLd%(mBO>+3fkrGMb_ zx)03OPdxAP^Iwl`{2*_LeeQz)EBekpwDTTM$MLg<-!=RWHE-Vd&KXoa+nzi&n>@CD z_!(E70$+HOM-Q(jwu&vwpXOG#HgBXxjvhTc?Yj-a+lP4vtH*(m*5XqVL<7!oLA0pp zy$NUF*lcoaeS6)M37ZQcE*i>jlC1v#K0g^A%7#=u7!YDr>7!4PRBxaM+RPh0usXLf z+gP_ccN%r>0DSI;&KbnORgbzt8Z7k-y9Ymfkk$KmJ@u&o*puygZn;IL#e6jc~U zh2N1L)Nwv|{rEPp0DfnusbcuLG2OoTx~Z*Xw(>9~i@=PR%dURwVncBr?ct$ICV=tb(5<|dyl~9zlu|f&_G5jeqC0Sa+3*|y(u*J zTI$Pn@Of=QU$}(_2H~E8#VcB0P!Cc%@B-?Dr^?=A-x$5ZzVLm5SZaP zVP@C@%@5lcML0^Wdyf&h_bPOn;E#gUqJ^knnZU?uOd<|6MW+xaB6*l1E!+T&f;`u^ zWzG%PRHjy>pcGZGP)noS-sgtL@5*yu!P%L-pP+LGeBNgJV`%GGSPP$gTJQs@u6sbo z%ncCxxlTZLaCT56O)#ip<*%N-T3P_Gc`7iPoJRwA2YkNW9snVSEB!VNMTgdrZQYS<{uscbHlx$w_XM^jzwCt*PeYzDRi7Iq zLt`grlSp3!pO;u7)#y`dCz(R2xGYMbgWS@B$ffjtpKAX$d_EkO-a7N*nEdqMBdsk> zP&70Uk(LnJaOFkkS<>+&V>0{CrIINtv;WeUz!9J?v|XbA4}<*wIx2tAgwnmIp>*m0 zO@yDM{&VSyM)-V#rCEY^xYQ|^hW;s^1vweqX_W_sg2^yxf_Vn~ zc?f>*4^J>pWy0l*@?fG{G^uck9*ZX)A;4N%g>p3g`N`j7U7k$d0-wKXOGX59C?bwX zpcDFny{2!FB8X6h5|BX9|Aw~yDl8!M77Mj(%E_f_8h zpg{R>!Jx>XwgyH&lbkOo&vLSV&;vOjETH@VNTT0k5nA zICe%1{&=ne6a2(H9Lp0%f_s*$1FO2h(~mE+Eex4q%q#2*ltGb`O{B|sAiwsryi>bj zo5Jo$lBI}V8jJ{NGyEW~%lznQhcsI@swJ_!W=?27Rx`OGkAy=?n7jp&M z4a>B6g&>i(6v?cd7F`Z#9j%mVWV-6%ApAP+=Q;N z$w0=wL@fJhrQ=SSMlMDfT&7WjQN%5MQ@TYn&cdiu2%3~`iMYwAX2Ns8Pv$?4)?HaO zn}^2O)0PN#lucZcIx;l1OSg=W=Yb4KTk>04(!)C&Y)c#`j3}4d6FfrRmPjMywR8(i zBg?eF*4^p$W^BW^Zd&wgJw=08kVke6cw}#B^2j=>k1z?$BJk0YWk6AgQv9UD<1(9; zb`y1>$0>8Igjb(AD+H z>Job-j^?1W$U$kdYW6*GeTlATW}lHP?Z#mCT&r9Nh|U=`O9PN0rZFrR{-jv)1@VBV z<2x#IP|xB)^sc*M&%&3Qf@n?LBjg1P$xl)dsbLO*;Y|6Pf^#m`M9dW4Jl(9yxj5eP z&WfcCL82mPKCHZ7-}8J1N>7==F?(Eth;7OLqC2B^p91Np=l85R&R|AcF|+925E0ip zO&vzXVQvJ=PO{+FVkO~Z*mANI2ed+q&kUyt!>WTSta8fs8Bv#^P;jM|uraPAU7M$s zGJu5R*L5ut2#t=JhABgcmZoZIDNLMp`e>y{iP&>-*h)!sk>p%W=iEh-wLhgrl6_#M zUedFbiYN!VF*M1ZfM-;lQFRa@%2}4KttJ>OPP9`6^8~1dMk2Cxjxe&=iN;e`WPR@| z6vem2PC&QW&p(2{=Yx(%A4AT_n1n5)DOa-i0TCQd{v)rqIvJjH@Vq#A@H8TuA^O83 zPkqwtX4IlEj4||(0~C$6$ItK%SXuZ|xH9fnBuI|;-$b4>CS*2d%B19enM;m6#_wo? z~iy}DEjFKE8IO!4PB@mp}BNM?%oy$TnLR9AE z7;(@%@a|!8uk)ZaGmv@k_o(lAFsA{<9@d8fOri$qHlyZY8JR>A9UmkZ#2ygrZAM9M zuC~ybOf_(=M<#-k40SV;$d<@U1_BTC1`aDG$whExGiua}Lhu$jUB3XI=Qa7kC>ptS zMuZ#67V3h#p6dP2@cFq;u9M9$*oq;yPS5H*m-_i8_pJv)*kEpQ`E-K!{^VrZJ;B;;fPJ)%ZH?)gN?cprwA><5B2wWmDLv^ z%J@uNyxdbsZ9qx3DTad_e)KsqPr&l^**|_6-VXr+LAl^RMqp^~P@%i&@zRvaFMXMM zOGJk!Xuvzau&a|}`*Ais?}f1A*QT+v$IHRkCqK&^wZP!*TJMSv`a}pRv76Q8uIj{- z)xd+VL3#Y?@d_ubL8$QYr$e1MbnLA?MOH75$7dBso*%U5b}WZVkAJw@b30QHGte^T z->Q7V=0Eaqz-RKxFTK!QSepDE9)}-%mB#sb*Oy9 zsnFtSR${1;s#BYl`-k|;IxGWV6F`%wjN0_)|M$>eGUiUrxqViGPvF&J|7W@h~a#oETX^}?MTT`i#h~={fa-7g${EToUwQ)ecBb5;F8JZ$6DAisY z0pR`dspcEz&9AIX`t@MZ>|*Yann(FJ{=jjk%y67xibF~V8H1hX=OPHjSKd+h zCTwIyyGCjdS$#qneb^1Fljc{mkpT_VKt4R~QQKc;>kM+hF^wH z+}mcai*S-4FcFK;Y-;zKGapCus}KP&7upBR1pz|1P=Emj0p0@DDWSzn1tiw~A@3%} zLG^=iNI-oH?zAzz+LLq(a}Il*p7lQ0Q_-rI-d(R~j=#arOxUm{wUwzpMu{(!)z(Yc z`vV~jU_L3eaKq3b4`KP+K@2tQyQ%(WkVa)1DuZ;$zFbMf@NeMr{WdWW&*BH^IQwKY zAUIhR@`G?Dy`=?B5?6EhhmnEt$xZ||;N7VHgm_04m;4W{amK^5!ZzJxVhm37-=trnal`d--gd`C1T8k zRhKzO$VPw&RWo3kfUN1|oi)6Lxc;?PfLzoFO!VUW*KG94_kgqbwgcA4VoZ+VOU;X* z*QgO*la4Vn#o?v;2@!Eau*wu9q7c-{gPST@*P(MZ1z<4QeaJ?wr@@E?XW>klX7;pZ zEAevDV6+y8Yz<~^80Zl9_R%3EKawk+=J-iXl#Zs11}48vP23NkUyCbTw+5Adz_^Pn zGQ0u0{Q6|6*xs-*l$zLtVVwLK7fZDXhH=_bENLwoa?u<;!)xeu3(`kvtj~b4KHZk5 zG66i;1={AA1K?@Ch<1?S&>yq9$fP5}Q9&&0hqS2?Ib(H-iFh$}yT8eYv+F}}KhZVu zsau}G87R>L+Ni6{a$8&)(Im(Tc+UE4>m0ERfN(Q+%SYQu&0SJE>qa}N5nQLiz_S`c zLbKhnrj)675D+S9Z%^t^SUrSf-tlNWWDLd@7Mqla$@U@(axT42hMChb`fsNRJ0Ta0 z*jy$ZLve5&FkH4>sM6yJ&3mzSOrNKpxuFpIF3x<_^TDh=ub^4m-WDcGB;n9#rJ1%A z+s4oF8@I=OKOfX?*rKx=ZFN$>o^81oGQ?IUj``bMCQ%bdvBQSU^SdU_akx?~Q>Q*e zER(Htf_&LbC*hFo#rmXkfq1A+MGfC zr45XC&LRd=U=BY~R&B=-GGKQ7P2QKc|6m|P4u!2lsRlpPj)uAZu-zp(u4u&7IbinA z_Lw~|FCt?AHb#A8|6{^V3-jfv#%^Je*W542k5uusbP!mb_^Heddd0=09QXjZ&wxKxF+&ohX49rh?~@Lpif3~;3- z`s^!1Ds7+VZ2=+UbF6LjGCt63u3fniovzO|w?H^<%CGq??$urn&FWVG6u;;|lQfo3 zKd7eVuD)tJ8cr_hG&^xGyd@2e$wWCy5PtPl zSp7UqvWt|3so)5L$R66zfXJJ62priadf~!A_EC*+dqEV0NYj&mv`UF`V@2rUdf#K5LVJ@t_GT(|l9MZ;jn&It5q|S2@>BjRkaHvF3sK zibI{kfZf>IWn4_l$bXPCui8v%z+$=wb3F*Wn)8Y>=d-GLf2%*MH5ttM-+{KGe`0K2 zBA0|w0NEj&P5O>Zz?B~ff=@Gk7sqk864@w``e$De07bk>W=3J+4l#qmJVCNS`)2z< z$+%s@^;1~w1ij)$hg&9YVo+beI6X3(JObwnOT?->dv>;Pei#fybsJ=y@VZB5lSlcT z8rYy%!pDxtvz29IC*xPAw`k%#yi>ZPE(ioU_?9o78`Z}p2J!d-*_L`5MdmM zeYjTho!?ES6_;5ac2FUL2Q~T3cCfjpIj5P&sYcr(U0eMUffIozZfH2+3!t!1s*`=F zV)!aoICs5>cX$oVXY8JUgVN15u)DDCD-IIz5Kfa3V%bjUZkihQp*gFzGYfY|;Cj!# zS0;Jz>~G368 z##@t1Zq)U6!=6K15?S?XVn)XTHI*C$qwn2uLQJ4#?;SAO17S-)5dqPZp7ToK!8g{J z4idy%lc2L|6E_A3^7~7e-M_HO4}`=$Umy^$b-FJjXi+ z0uoMJ^N_hHqzsl(bO$1^NeG49 zjX_F}nazM%v&~hL&1AVdhy^!<6C5+hc6^v>&%BMK2BEDR>A^5N10lmqZe0aWEUe;B zEaZUl6XXg(R0U%R{7A5>;9j2U+PH!XlbjiF4N{Gjj1pq5g}EWtY!v zN%brMb`albTTEJ7TiCQxHu81s64*X%9oGm-TlQIb2xRjXl?56qGDP+$~rd7a<@L0ih>p@SRe_U{evP$CQmV4Q@%wYl=Ldj1o;hyqW}yEO1=5hVdur%j4-`sJI-H9P zQd+s4Mxc#Sy6x0WfI3Qm`XB)6cjpZ#<#sHIBLaq_5TKk`837eSYf(qJG-{oZL{M97 zAms8~z|p(*x54FkYHRdj+$70QA`z3kj3`C6SCok3(uooU3eJP{q89|-Trb4IQy)~z z_AP?5wxv63rMT8xd1)`iX#~`68X%{(YUi{;Mk8Y_R49+sh_v`rsnU`t7i=L42)_va zS0hgY5DkSBZ6WHg1wr%{@@sAdzvexyEkg@O*^~EFV3t}SgJ-Yp30jz7fiz$2pS(mM zi-yk%pttS3IR0iI{*AYh5Q`TZNe?J?20|zXuN;4B^v-{$HHy6$^C8ASrG?cI#BguX z2;#^s5+M-(3j*wa)ggiE$uaU8!2tkokn0FrSpVN z8=P;eAL3B0ZiGER?~Fnf*wH|qw&I6Q0~HJBRoLy&aVL}%7dQnz+D=>XQyYEQE#I1% zH14hdX=`DGQA9#IiG-AJ5im&W3`$n(=LOp0|zfY(eB-DFBs9)_S)FfQ&45{uTsXhc! zy?@?PRnDeR>1=%ns(P@%r$M$66^yY*n7JP*5*Cm2n@8YvRpHEKMT1L6jII7 z(n_z{GSyG#sH_iwlm3!!sLUf#!;9iz9k{N8zg}kZB}=@7)_gjr4Z(1RT=UL#Q+ncQ z1RAgv^%>njBUDoIJsto!@P!!!i70{NBWCB%E zSMY74HBJ{_P~aux+U(?1Wg>tYuSZ%3plAhlW zY#4vjQNDuiV6pBev3>)@8hLjpJkzrWvGOW)80R+<zKX}l?Um(p1f{ZFI*dOpkfI1B9krhGiKoCtn2 zzl9)O1`B+BO6AcpXS7Z^qk@S>p_EBJIP%{J8rZ|q^rXoOJ*3Ds4_|7a??hu6(BzxI z5j25qft_Y#{7 zu2K%t?UgDxcZsSEQq9kX$bOJx1T2m$@Bo96T|&nPExUvVk35^S58mWl-4RDuHY|Kj zx`Cu+7v7JP@ID2?`}n+t=MtMbLf{k{OKK16Zld_U|`P` zhB~q&;uAY$uLt-Yj>AugM~xQGYi%8Hd>EvLuG-qz$Q*6O$%GWxZdAW8juhrpBNoyp z8G)t1F?AvgIf;3oK~ZiC-j ziqg}nOKuNIE@4-E6X;|{PI%g@F1y@}xJS`Q{Ww*jy-Svz=aQxgO7-e|^9Efj{a%lZ z`%ZI5<{N>*cgrt5^6=*R)}1A@sEhGhJz72hxivfszF53~!L#;+lzuWq(1x}Tqn|b? z(Rw$xk2Ng0*S{b2EZR(RD0m()h6?R#a~>pwzzIdn-bgr-HK)oqHd7u_+7|lW5u_$w zS;8P^1U*3B82|-pKSPk;4Un(nkQW{WxiMz;M=69lK2%^sW>Ep#*z;v&1D!H017noI zglU;_qll>GRFX43IpXxVoSXcgJlA{7tAvQAEf+ZXKbUr#iEvB&@9shdvl19`LU9mMj2p2%N`mnoiPdb_%N8JpvKw zxw1e9C~E56OXLx{RLHfdCfnEYO%$R{bvDIu&7qchDBc1`U8SP2wdZ(csF*%EIme*~BTg$lO zcQS=t8xVG-+|c2f{g4t6`}o2xPc0*cUXN3;j2K$T?PDGYMS$q_Y<>1K&F`G9Qku#P zZTn#~9{)|g#o4C146+WFq+}gvN@>&205}3tNh~$9g@!=8v(Jcjn*(9-?5nqfAl@1k z1Our7c76|KEM7BCmmVP=^^vhxH$uA9UT3oIUrCQQvN7QsfgvM_IpgRcB-flIsMELb zs1d=45gZ~o&6#^cMuU^w=oJFtMz)4J?k(l%evEh;Uff-MAWBaJ9fc)xf2L$Ffvwfn zzUrAIxZ6Q+w?+jgB_oxl#kyUt^rAvvU&5^=cJ>@3I^M6+&I+7KWCoiNsxL;#tcBLZFflj; z36|@olhuOEDk||1McT*mLpGT){t40C&XXLfC13>yu9-xyd{$g?{f6iRM^?h(!}Gay zsKIrs_s+{Y_~99|CG+zy#eZ9Uj=?HceSFl8NmC*nq^6Y3K!LJCd#vZTcvT%w;qY%kIQ;e~ zP>4E`VG`mW?{S~ootCTX^%QueB?pn@PDt|^Lu#7&%G#2Vd-p+PXtokYbq(uLi+*y@*$UmK_?q`+RJpH=iij_d zt5!sQx$i40DnH9;G%hkYGqhmv<=*-d5ni_LF1zd&^cu#<6wDP}2`d3lqrmt92#o(c z>V^>(NE?h@or@kXc-)g?C!QBbVJF@>Jvp|)-v}DYf7+?>#Cq2^^rsJoZuc&^cRY04 zcjp06;`TT#T`beo$E12<#qh^M$|dHKO%mvu&F(IPSqltbxUYX1aY4BeAmzuje?=^2A0C z%%hRg5BqgS0s{##b6fIs+8`7^oluNV4x9T%)WE}%IBIg93n9#&oNHz-qlDtOb3;eR zwzj!Y^Oud=v`FcWlG1$;leqsIa6xOSw(|~_N~)BNC>4G=adpga=eizFL%9_Zkj3`waJApnrO@Kv52#UqJ8Dj;8HmZ~j}563=F`^lP+PiOAn?0o^UkA#LZl8l5##eu{B=0A|I zzLJ1<9suv}M1d!LJPEPpEe^rp6s-PhL;41W_~_=|BEGOEkK zj}Hx!9Ct84Ss=X7RCWn~_MX9}#BXk@#t%?Gk?kmiGJ_SNP%?&?6CP7FQDg+bl*^An zGa4-L^(xiAiftFoK5=%c#;HVv8i38RR+%ai{@O8aUM(uMJO zPUHbhF_G*Pjgk21EGicE+<&waAk@ofv=GA>s=2krD54!{-$zoo7Nqcws1zc@^)grF zd_S~2N4txMfkfM=WXPZqB$ap&@L>?oZ$-tUVBk*t(B%_Rq7bqu<^;LmPmMRNot_{c zlmuylrWk{ikC6?_%>&4MX*{uliL2AOWUJ zI_i!!gZr(tv{R-5-zYP2YZR3Uk;zRi zHEK2n3oOg*s|e0YT7(fvqOC?3Yw{f$@TD-|ixX_5r>DY~vTdht1Pc?zJ`hEmY3fgN zQPlqw+=bU9h{DgrUUy*tqG(t}ZZes+*`tlzTx6hm`%4)8tVXoiEMlN(?QwlmABje^ zMk7t)vdfvcbTOGsZPaZ`A=Sfh2EZvlTgCmjX55uRQUg};Y*F~xZY4zVT_S$CeXwfJ zc1#qGMH>L!sk^tDnSYWiiwG>1UKZj_$QJ`HE=sV1MP*_6KopEyM}6qZ^^6igkt>J@ zZRUf*8uCH~@h~yPg@B0jqllnht3b>QIN8LZn1tu+n@PZvT1Fg_7`{njcom4@f~XkO z`2GFgS#pTzMYcQPm#1~qhpO`YQ2zY z9CBr9UpYK|PCD}^4aZwa!8nZ0l)gW^ zf!J*(YMpsNIt;D+6l(<92&HF=wLw|)V}uBZ397Hh@$b$JPQq*^pdu8Zu&sBS9U;+c zR!vyQgdH00+(<~EwrXU?kNarOxFU@#-DVRZVOmJ-(IB1$rTPV2HEP(aQ5}n_hR^`n zFGZFE6@vkwCO6J5?`f4?R;#C}LtJb3$#y;Ma;NehTu!GAN>ht`%OwD$lz0j;<5vW3 zj?n-Qg=DidiU|mW@Cf|=RaB#t-{A@(?0gq3BqasYSgGPldq$VD7glKK3Fo?aFv)BV!Is+jzh`1Ed(4Hgw z8ZZ43>4yj!9STV-Jsdg@fNZ8%xVju*aA`MEaEM>dzQn`aVUS}s<=XCLAd5@7$-?$4 zmP{0N-yVe5iVTGuiqZLsB{Af?je&fs??n}aoIT~_HAHF+=TosoAJ$RTm@G*2DA_{? z*1NtTZGEHcZfGaWiNPt?9ypcv;CeW1kj)XdrZg`Hd!`haL#^)m3=4BZ0~rDd45Jq7 zsHf3n9Ep9CxH}-8_NX2ucO0ZqJrGqUPlsgxLr(Vsr7*^4FtaVBUSs==Hpo3;+lCQ{f^~`y~VBY586A5LWOKixc6i=codp zJUx*q8#p4@nmIx4qNDZB1E47V&jp z@qk-|PoBe{`ULo`qI2!hJDB5$TQrEt?(hy`x_57KY^$t`P4${L9G0GMrxDXPH0)F^ zZv?PZ^}XCYT+>m^(#N8$VvWqvo#=T_%7_TY-iQoT_|_X==7$J*tKuefciPS1_#I4- z%UIrx5Fs~i%W4R@#e>^F-H$glpW(8bRJU%12uDOZ#-<9StBVU_`u zvaW`OG^6si2Ga3oEXelLNDrLr41@=C^%NlmpaMs)dL+uZ1Oher4N0C6Q&>8$z<*G@cW^ta(Ox=#};O6ZwX1sl2LX8LD>ZhJWV7E6?n8mI8Ny{d>tP= zAyzpeMcCQ7(H+(Gta&sNdcS8|W9A)6>E}Ir8!7$Nb8jQ1^CaFzG>z{EU8djLPa9e+KOT9j)mJnV74-!LTB~E8PIWy(2%#K*^Y0+f8V-Bd|0tc^5KL_hvIkM_cr= zM@W^cS84+GODnN60K&d_y};W5`@hs0`(6Vq5zqe7m4ZwsX@F1&kKK&h{-6a87I>PN zlW8VrxBrK?qg5_#W_+3Q(gwh3g8=$$BImOKpwrd>jgT`d5-csSI3o0L$m_D%tBIeT zFs}!II&Bbmwh27&nA!TDwFXa^-Ml3^>@yNvHhfl%;7%iqz5+11zcof91UG^-`)#*v zBTI*e=ErrFczMOwA%od|-(mzuF+=GId?ITNd5Fy6(`0W>tWM!uK{P+!lf9B}TX_%! z8{hxuaWCTp-{>N*uw3ijJ-Zmp0905k{Jrd%3xYCO;AtWmtq>r0NDIy__Lv{r?RpBg znrq3ZpJMJO_x zznUKgS3j3qg?c|EUQ%8ngoCgqKR5z$qR)lQ`Ijw@#Bae^S>*ApK1>|rFVj@`fxY=2)2;~Dx6ML9cD& zDoP-!H=IEmrDHdz4WilqLR0-dnCf?Rn`#HF;((lTOHH_5puH9a!_bs&=|Ea($D8&J zAX*Lv_VDEzV`l}w4=8#Y37P!PBj^F=&HxDK|CMllGvNGRcEh=!(!5cPaA4g_Tq0k9 zNf?2ib_?th0lgx>xw;Gdo=@}vbmmeEY8S*kaG>is4$ZRqmLn-_tv(6z`&c*m*+P${;{U|T?1a>NMsb^EbKo$c|$UFRhPdsQa;AIZptJd1&5bk#k2m{MtQEB0`vsOFuH zS_RpGD~3PSU%>CZ-B{M|Qy}mL={pF=Yd;cJC@b5ROPrLDiQ;}zTeOl$eXg#DDLve6 zN}ZX*1H+$DQ`nwJWb#dd{iPtI_#4IvyEJa=hIyH3P{%_=>pkwt$))F<#Zx;B^csT& zIcR%fj3UCyGf57&f*d|j7Aqt;HAE#N4{=7$_DYWCLwa)3wUbjqHDaq%dO^K|T>Ujv zStjR9lH1)Nw=YHI)?#2R-6h8{e6cYgvV5$zQO!Ub08vYH8by>tyqF8L{`=tVpBojZ z0+gI#m{)DZ$4gpFrh>f$Sf~Q{Kx9})RXb`1<_1N>K;*jQa@~<9$+bx-Q?0)5F=RMf z_gPeKLdNKLTca%HBHAGA!P9u~r~VQ6{lO^qa+O)qlP}O5C<_{*&Yec-_mo|qk=2Ts z>j5238)PD%#nDmS4pe_@6dj5&a+oQ`DQ-O>+YqZoqEIlLr=vX>$+c6sotH4Ld2GaNuaT27*$Hpn<#L`w8` zL5W^kREZjtZq-ys@_WywsU*5(pM~no(e5oKG(=J#Ao4`As5u*n&vwM0d3%!s6`aA1 zx#TY4-?PfjPpjmeqZ@#bpNP`A$4P@ZZX4$g5+1Z~yVNeORrdv|pW@V#aNAOYZFeIA zks5JIs3!P82#E+Hw|=_Zsoewe^hhKr@1*%@p1f1FsOWB>!GF4)t4<;?Hs7$63l@fw zK@t|^h#BbEnvr(Htbr`BCR$d^D58|Y_mk+hA*FCl4@O|9vZDuO?>ECIpM-vZBy=4} z=-T;6$U{XS$B4b{h11eSln$a&`ZqWUHKj zlcG6eBS4Y@37=w6@M;e9GF*q&3b?G2(^7~&cK>gj-D^v&DFmHGksmRnYM{j&M*51IaCk{@d|03I64S=0bzG|8WL^C z-2t~hwZ$PxNbQO?UCkm`ciJGVi-&?Wr*>M|gU}8JkF!4jsLvy{qgk0E6YJ!UddLep zZ4h`0?soT^#N~nydzI(Nl$38kub}jrro&?MW6J8sD7wE5f{t6tdIb&CIz*o!Bj@%^ z5?u3k%?3G0=Sg@+4d)MCZkj3Z1svkhR38Vx-B}iJ();v@ltuO~AG0GKyA4uiSJVl7f@QW{I+Brn<458^B(14uhoaY?lAQhs- ztb6W?`2wwa{RPVE{2s*m9dA#z2~cvYWLtq|L5;3v41r`vn6DhntA!;mJr2VlxLo?L zE0(-mRDyr-^9+$W&T* znJl5Ye&Tt77g{&H%1X}T9PU5Sb}Sfa{oGhc_E`YChb*eo24U|v2zyrpFTSZ8FA5fv zG$#&>v?wOF53B01%8JlpwU8Y0P)Sk7F3mpeViqlyUvQHzaxTQ(>(v=iE+jiF{W_MG zR92aa1rgF|(ik@#_f(XfEpL7{e4}w^Pl2j^JgRD*>1=?^Du_?p_T~d0?A*bhjxSq^tF8k} z(q+;}L1Ovyvlx|5cnM`0sm4`$=Sg*wu=)Vt_1?ZzeaDGa-k*6k1a8yTVhvM(w}e!e zm|$5bpxfeBjrd)M-LM<{?Tn>fph)!^FMQA*f@WkC+U_!S+MuZae{!9yKMUaLXnsYI zFTo%VNHZ)-b|QFanHx7kAH=x4)T=$IUUSh>Tk9~;lbet7R=z^p`f7NFDE`#{34TA> znmd`Hcj6LhiAMZ`h)4W~64{QD0Xt}3zoEcw>ECIC(|@7Y*n2$$iF&CA7X9;h0k0JW zD-=QOW4tn{z7D?b1Ko&4m{BPuJm8Hj#BrC3*b%(Oa@c}bC>6MU{%2aPaDaY z?G{VWD%|AQCc1-#-U;R`?Zq6;wx-0}hz2dgUgbKR-pWfmoK7Pq>lgzlCM9lg*Ulv+ z!)-?2>!xHjmrFYnQFi^(A3L}d~*KDQKML*A*t z)UcUuS}%eFDfY|dqDYzi#~{VGk{P9lKQ z_T<|f`_-k8$8YgEyJ33?>cwpP%y`w4cQ5%ORj&bS6ZhB^1v7}j0?z~`r`AOHiA{pQ6QFw|^LroNs<349T4))%qLcEB$-$ zl|I@7RJ~plVU!Rn0PLYQPyuaaa z@>3oJKjpq2$lvS15czYqNBvk5{ukbJf~!(+mztkeR#vca$GWEI79TKH|6w=4`UM-~ z>!m~Nd_0!6X-H@9Y%C3#yXxbuymSu6X#|oI8i0#zcyijH^!&HTZ~r`K!d=}o!FH=< z3?ySs!O+V}-J>Fy_pz*yB2*jX!`ufx%st%{!EX{`wsyH9*bEP5Q5h^0_NofCF1V!X zhib@s!Q;f;g31S-Y#Db0AgS3t4_kK97l(UTR&v@PcjLX}Zv1O-H{RWiWgYz%2Yl|v zh}>~A0EZs?8(DM>Aa_EJa&-y#2d|1Em+X!t%5Kjbau}NGO^PD3m-G_WL$|mbJKj3y zH8E0iNrb}4&{tV(Jxp=FB7!%ys{4VA1!D|6Bd>7P_C*_)acZn6{;jSDfE|tktkLE= z0+Es%v|!D!*CV5v-cVZqO)wu%YAvHU_L!{j6bpT%ch*rU*@a-TTR=)whY!p+fY{xy zaBbuqYzJb%TV<;~#7=jD7JaxiLRhR8)}m#ChzQo2Uq4!xd9`9#ySyc&RzoDFZrVi| zx5ig17R`HV&%*1Z!cMvn`9U*aM&-puU>bma+Mqz>xtu3zxL>_Ky$_yPF0eN|X1whT zJG%=JMxm@>u9djQJD*t#!g z9Vz-?pz>nc7qbJ!8tK6v1XR54+a4?(M7!P+k{X+q1WRfEHUO5z#i*WDu>r7|x*H=Q zMqN|}XsDv=7Ne$WS*~mDAb)<|R(&eD3kShnh`$`5Wga!e#dw^&h5;oBDY6UY_S*8N z6BwaI4`m;UH3DsfqQ_!wP=vQvOA!2IYp>Ib73r!==iS1~h$2{?UWa9tA}JsTs`Eq9 zlxSx&pLKw}cTQAAPjyGfzm z0=)dIAc{S&d&8lN&b#u8E2p!W7`&zs+5*gxZLzdZi4CbhLT`>7c9Zq&B9GaIi_Hqv zLXS}mvN@ip^$F(!yWm`b&9DM>g?26#;vGnC3(x@TyR1SR99$^BS-_x*9ME(Gjz`nOifm&;P?~)l z1*VSaaAO6!Qb|=zxI&&w>WocDC8J)GDlwIlEF+$=B=vyTB(CLJg5T6-;kM+ps4Yr4 zWM4>ape|L&I?O~O+jLa$bua0Hqs84~H7%syul!SLMmA@Og`?$_&p6`3Q2|oJd^|h|~?Ip;?w@O5wwW(jZlA zQ4$=fUx(jcYeMmSx@JsZDxq%7HrB->J#dnMQMIVXn0sCts+cC}LYky^!sm7NBuSE# z+d9CjX1KTfGYAVvBW%GGd;_;-`t@eF=M1Gm2>?I>Kq^Ah4BoZ+T&(CKaJ zljD4EyGJzd+Z>3rM-l+?2=_##iK0caH2~9E1WfBPSRfMxBM}2L$ECqsHZIKC4v?#% z9=aQ7tB3ZQB!hZTJ+!QmQx-Klnklo}(~?9^ow};(*C7pRRl15;KY=Ua+KT}`FY+rQ zAw|QD1{`L@bQM$@Li$1{CZrD~SdZE#)0qD(*Xi;;%N@y`iQ+JIw zXPeUWBQb^+$U85TVC5PkM-!kdvB_~AeI`Dw#%vl-gVdrr};?9kY7pn@IJF4Q7$>-qv6Hvi9hY#$(Xy3s@2QPZ| z!2|mb@4NW$p-T@Op6T-O>Sk9Roo!xq9R4|e^s?VQwt1I*2lqb@tKJTO4gSY`oO@Ha zwhgauUjB+>M~}^BlkXlm-ITweFn@x-l)gyZTPukV|LYL8vz}WR*H_nkQF&J<%x(p zjvl-G7}9Yk{BtG}7JsNqXYN!~{*Jzcw~=MLR6$*4hkkAc@Zz@CJuILqxXl#Zsfvd6 z-zL>>AA$~I^?2dvjBq%46!G+F@cq<~(z9cTTumeg&PZy!iX;tiJ$Vk*_iFe)8prhx zmW!;~3FZczv(3w0tj%`dPYs>PFH#47AHJ^%1_Zd_=GtR`E_rtq%4m!*P$SrCmo|9$<{p zDA}qA>p~IZ&n8ydLmg*&08w}$fSgTjoeST40)S}EqSZBHo1uyd9X?dgg;dXr;QNJf z<|5KHlAx%nL0f{LR$>f`=$Vc#)o`a~e~Oy@CHVe@jApfrshK!>R}vFbfG@trsr_@urL6VPVh8M7AuT9JFMM4XOu%H))=E7Y6}y zJ4$mxL-andNMRIt1rHga&Q#K8JdJ9(?bGUVBbcTt=`hU-XVrMX!PH zSHy>(7Cl?7l|A6qea*a}K z{yh!&oACXmIA?YNvZ4%ks@0sC-@Ubt5txPfoLp3u3~!GO2n{8_M1x7-GLp;9u1a%{ zLSiux9CY+fEbtQ11S^X$99m6YK(zV|`2O`!cc2baPAPnAJ%wMWld}E!ld*o!pWlmQ zn9X*gJN_(mFs;+Pk2>=*sWXZ>5POh)YcuVNnX6CXL3mi{S1nB5O(R&7cTkfkSYJyE zR=*vv%5gUNwnBxb5(=eu_GTI~XTr_1k!CC%p2^xv19%pEKQm;Y>N15AuF+xQxfhKk z0<%Cq(MzcAcf;%+@mJ8Cx?d2vb42)f2g!!EIP zhW~T#9c#=U9N-hA6*{&#%jwrksbAN__q&r6Q!v)lfq&QnDW1+Y&N5|626Hxc zEV}@@O~;SyJbq-CwwlWK70uB=2^9 zgB|5*Rk%$;bqWa;*wgKwT#g-ei8RWTkEPL!_G(5!22vv88^5^sIsGU}%>j^_XMogr zbB~@f2-w*Xx{~Fm*qEfbbqEntu~@Z$lJ`9gEWLyI@B`gYC+xvS-6mG$5mHu z=y_UL1=W9>OnT^}_Kec?Egei#Aw@5yq=VVcg{NPU-*O-amgs20Hw)_A{)LaIq z!RZmDm;A?L{<=_{|mbpzaFxl>I6a4Aqt_B*uc+BDNaa zjA_EDufPS34#h>m)R)tTDy z+jM?}yd|`u50R%p*kla2@nTSSAltfp@QgJoEV1w(^?%0<$JGoCj0>2;K{G*Dus+?g z_Z<9ys|Gcqo-{t-hF${U2pOWmKhs46IT_KXgILplfsiE=_ ztDo0vi<&g(vEKIxjGCMFYbbcbXP{p6fhLD;J8A z3-d~jmJO`M$Oajf5E$?X>eJEOSi(589|cFj$9QT1mSjCa=7!BjMRGw4Q$;~7c3#2! ztOWEpa{5b2>V5h@$U?$azwME&etXsBinNSps9a#lXLKaoKv*jP&;p}~Ta9QX zUHcAN0|G^JLL3?M>t`GFI1P^2j&OG2frRpF0p(Yh`GF(mwNfoKE>>w6srCXPk5wA% zE};WGK4RXZ7yMAfblhjH8}NpSpEhu*MOhHF3v3Fl#BhVC+mrBI4Z`#GEfO9JiNK1Z zIyA(kl1NvsU&Xqqc;*8A+t@yQQU(pr^@|< zyC3rz4P8Ib&Uz=UChY|#aVgLWo9P#5yU2L|41Dhc$VH)ED;QRjJ7}bmr9uiH3y$VF1DgyEnpN9C)!EoEWXL$RW&?jz_f!8X7UpBzgXYvcU{KEK@VGLW;Nva?lCt&bZCrLn6< z6bFz>S;EA3r`Qrk!YbR0=#DtAN_t6@LOnnh4ADHl+EYu-~$DDxgj{1;Vxlm zk>TVOnr@T7hi^O{DfFYY0BV^;9s%*#e9;0VVw7uxohP|~k!WLn4R<|5&M?t;jj&HI z(cPSadp^A|&0aRDOY1bVN}uvrq%=t8)!TyXTddAPgHy4Q&8_VW&WNhoDioSrn|hxS zz>QC}tQoISl3-H}mglafo?g%!*0|ox0KstbPJrV(LTMqrf?tGxGF&J&!A<2r>TBBV zgc6K>BO&%%3!RaM<|$el8c2#X|1~ZRcu-)_uIZd^Ke$=fDRLhna{P{pP4quINktfuek16*Q8aOx~Pt1Qti%c5tL$-IuwDN-L;B9C0Cd2_Y0cD?7sA zf)Eb)NdrXL_aJxz^sxfXZi7J%l7T=iFL*X2a!?qNDr^DHmet$&*k|~lnmZf zY|4F8e!2RgymI5I>njd$$ty7UoV-Xi0IzC*?>|oCbG`=I2xq0*o=Dw#K72nfd*o`I zj{icW(4vVWM-k?szlGZPDt!NI<X1$?nx7vtj#x(8JmGK6tC^>(gvloxw53g;NqROvFF_ z1X}6)@CFACyh5VL|MKgI_`Ug^fHRJSfuJ&!k`;dA;D_qSXO02X`LcdL1P2=jpooy< z0C>RFgRk?R{f=|!I0peS9#E4A^VK2H5b2l7*x9kLjjQYfrLo=v4Pu)QfOvel=je#+(qu)%#u;GOe$~9!&gQ%PEzK#c5LLw2t(5VDy7? z+u=o+Pt_OIx@r5$%EKgxSHbs{tr0ri$D!(e>O40kNNskzW~>yLi(iDs-C)|%!!jl!Fg#XYPYk_&P-hj%y`dJ65a&)Je8<7o43Prg?h&g!wx9i z5aZRvxfe6bueF=}i!RXY1Reo~1NQ)+VYvZj+P;4fU+kx`0}p`NH?rYit8XE=TqOZ^ z7`EB@Tb&nBx6f1?3v|{6hYx?0hIVf6^55_JVxrmW;QKW#5@-qp3c&pASF(5d{ZdO4 zfGu}}zq^M0(mfy*W7&keZ0THRj?}pm$Wr@O8FJ*a_-`I?eaH2 zSwe1yzyuij8X&nhXNuZHmw{0G{zcGTc*EP)Xx4DjU zj-*;utVEBiD67PyI1{_5JPMlEnC(7#OsmtKs3EmV-KjOIR+R7q;QdXjWYP6_jPXZI z=^dn1;nDBl1G`%fumb)L{turqUD(xb?mK>SPHj;53~Ebt3~M_>x9I&(weT2UkAnN5 zKK~p3{Yr~LB7Zd54f%-)Kz*eZ*;lcwvn)g2*y~!96blXSh^6Yw-iDu?Y28MKdvtJ0!O4H(CVS1jEZT)2Bfk8>QKA@tvMaPUkA z!N~xx6hF-s@b`w~&;;7S7*UnRh;2MRCz$X{Fkch==_nCxoa@fwv`eXTNs3hD4zfY+ z*xiXzZw5*Mp%NhIq!jm!$Gu*p`aL4m*ML-CoR3t#L^|0SWAM9`K{-2m1{ElCCwG9# zSjxoV^~vV!Tr>iD!*I(8q!MVlIK2lnk^s#sPk6tEnD`Co?w96cqKtQNmb8Y}skI*VTMWC5QUK# z$j>wHgB$eIcEFS{H(D*XYl7yY;buk<@`FSsh@qRrCO=5Q+g|35VrA*%PXCkhx-1<& zL^zE)+{h^_0EW7`12QtQF39K=>+t80a=H$b)9)=vhZCa=-^#Vz0(A8r4B3S>H~9qQ zj8kREPg;+T1!?{S81Vb^F@P->Q`(rxkpuhHF)--W+Ne--VDf$vf%^ala;M03`XevX z9eNlGKyxHftmX<}RBwd8*Ug8ma1gAGSw9=lnc=n3$XDo*uteB~sVTfJD3Cc_v>r3+ zJV-OT6{eKnq`j1ck_;g`_5TuUJ_oG94cT*qV@y^i zw2?tZv$=3W)UaB$2Ep$i&u4QfVlPrN=xEgOA~ecxkmiG4XG8MJjF+( z474tW8R$y+uoZwB5@uby8>Y~0(fVqII6kOpx*ijWEJ#Lz*vhg+F?UFY;0yU?t_l(a z0-socvv5(AWJ-x=xhU#lJx&Jw0ICFZk>KyLUR5ZuC8lx*#x*5QvXgW&k?2)GqE{wK zR0F+~>$y5KT9UVo#3S(?iufmhbQc2BZvl{A)i01(H?p=g^dJna4wZUbizC~TnD0AO zFjYETo~h_#EzVmAzF!3R-jakbVJ@cnTNvdF4C7&=x9x2Y*~Gt<`1U2>+h>z}E4E)F z;|@yG9CDPCKhf3y^t`MImG2Q6&|w;k)e^a-c-2F-UqkY$2TUV(n=H+f!lH8gG>75u zP*QVOSzL64sGza8#TEd{i~f{QQEswt4*im-j)x`5K`bWR(%w0`sDXncx7S53EYBfuGv30PJ>7}t%HYdp zye(Uy$D4QA=QxZ~(BKyoa^+oKq^$q|R1x;s^5li)r*`V~?rK2Jq;}f+r+G8!pD%#^ zxw(I_j5+Fpl3oe197^^(e*&=%+pEks#iKxDY2^^zeVM0D1*O(quqS2qw`4wHo!;~g zy~=5a+^wSVoLfo@ZJ%y$DU(~p;=NMrjvKBix)bo3J_7!Jv{!*h`jbK&-a*lri_p3* zurk*NSG&q9j-|A~t#lXt3MyVdWGkpsl(zhmy}p40gQ@B*pIegGH#{2U1!Edy#omL( zCU8M;9=akTTb{7}7OnG|?ujfxmw?NiSWCj%h_zo3E`yfS`30^=`G_h9qi-bZr{dg< zsa@!3j?!B#zTJ!Xb~OZ9Z|~JsC2Y^|giTpc0Lo)>fC79*zRi6+TPr_L6374Rg>*A*)0#d5!h;Kv zgBIFm1Sk_1&NDLtB-Nq--x_$T4Y@>=RM8tk8yQlyG24p=bi$jsv$DL_B|$xYZo6Q< zPcwJK!HoBMp5Fm-svbh(@#i2OAE-u(;$mx3(m-b&kfP2}-U~z*_A{J8H2g5o@I&*_ zuq``lNyK(4e!6ItB`UKLb;4?KR9TfOXGK)jx*%n#D(eIw;*_@gP4|J9^`vUOFH)-0 z%L2`X1rsjhsIS;sFIQikPVNC5pV8b<4U;+-Yh_@PQdaO{G(X+`MtZ1AblFIN{bKJ4;{WJ>x}Sb`MRiuhDw z0tz!!-Rl!8W~%M_Lh!2kSf99PT_gHSWQ$gY(M#1eYfnMQ*WqV+Cj6aR?N`Qijd*9( zAgH{eIdqM1bY!=Z0v%JaV!-MsN^W1T_^S_^Ik}p_q8xBeo2`m58>`0P8AQkVZ}5Qm zlH*6tYtMYdcxtCi>Ue6)6HnhmJpB(Kw0D`0r*bg37E-%nOr>p6(}x37)5{s_y*`pl zBc`c}l*G5tL0*F`XsU|du#eIsIH|nRHL<&aORZ`o%q}jeOn6}hg1*k5RD|*szGX|s zVVO66nq%frWVa)GOj@fpThn*fCgM6|HcStepid8K4xwRqa& zdl*A&z|u)lX@s;`-bo$Wa;B!}4f`lPl9i0*>|1-ERnuddQpP@7%#|aQkVP>s-1%=1 zdc89ldeLYd4s|5oV(LK-{;6II1%n!U#c6t@J5#^AGG%V3DzSpO<~rq^JLc5W3qkaJ z+Vnq?0{_22fu|2E6lerg);Um-4J_gWRT2u6fFboj0ZdRL}VtS`8vQ5|k zhGbXM8R7{%=3N{WXI1!s5#FNJ-LednuE`zSFaf5YjXJV?t|wx=*|?ZsD%5Nmgb2{; zVw7J&1;lIxfD{2?`5hpn>><_i8z2+^Pg3m*GMN^8)+mgabxeHPDB@v;cjWGMp!bJ`_;W?G{y9ORGe%0zr*+x4bIaXT()| zMQE3ivd&Z`zH9|Dyz)Che*15d_PHLk&pQ^NePZ4iqK8bCv0TIU#-hn3DW`Wkq$RVULIf}CBH9H{Laj}->f@5&1zrZb;vTG$%8Wx*Z6 zG})B*$94ftmo?sIh0o_#Pyuznf(q4XWu?w_vmGGSYxa*`0kZanY6!{zVI;*S4J@jS z$SoU#i5Kpe>6HsWSkJAdl<3JaeVAenJ!IN0nNW6zx^;r~&YPc{+jvz3Q=UN0C6FXg zXK9_@d<+EYqt!5xnZ9~B(Tiv4FoO^(Y#LolNo2fElW_{MX7inDGRCD%5jc!F$hMMf zIWid3v!!-XiQ4fa71Cw>Z1n5|bA{lS(#f`9PYyom&gON{-fOD4nGlNAVJ9yq7gk9x z8uS5-foS&pf)Vtnanu}2PoV!asW5o^(bk?*gu*Z^b_!W!Wq8HJLh*aXthz!yCpZCF zdah#X$Tmz?>%GMCJA$73Znd5h#gtt`b^-$XM8+$)%Ef{gqqkQ0Q1P})Zm)0)8Bs7< zt%@Ma5*4{w;gZ=3pnM-(U7GbmATZHcTL75mhMWIAm3rU!GLj4W!cUgt_2ql@`IEF;fns zJO++z1?r>qvbgApt;aQ6o6iEA{%18?MUiA?0{8F%M->InZ>j3q&@a!Md!l3j7HL8g zCe5Y5y-TXOmk>(4H7xci%d>|qx|>IDE+a7iDUjouYH|eN)QX6~to{?gStcMUt$=)W z_I6{Y_Lt6WN#;U55PdGtYfCb@g}C$t;L>BOxuj?wVspt{QrN^J_}Vf36JgYk zpKsJ{AI^A(%K>L%*b5g)QCLaxtf)DrN6={YIVzZS9>5xjWCIElKPp+hi1Q(r$EC82 zLqAGZ$UNk`+pImjY0&)g9^4rRYtkbKa38Qa&qsVkK;v#!mw*ZGI=o zN^&){K0`%klRYB4I?ZL^yO4Seu8!)HHZwGMs>xPvW)N)I$f6)lCVgn)Ts#5!-L*ng z=W_<)(kF)m>n7tuw`p}Sz63bYMV$Usvl&3VARJxT5f$_Th- zr?*-j@-lT`!f`G*ro3~=DZxbe{)cRgSDK$OH_%R24TX;{BR&E@n=6xiOz6fK zuhezL-nK5K>c%|eUG^Q^|2*UZg2n=bqO_M2fBq2ob3DnPl$?zWY7-djS`TwK&6UKU z_XC5jOEM@SK%#Te@%#b>XscWcRD#P4qW_+Fw+DC!0deBRS1I8d8uJq2$yo~qX@;ZnL

$F#%$gZZ@4XQ%&r2fan+UR)@*w2c4BHkZB!PFMxM2)@GPye zXW|$17w05sYT(<1z>Fnu21qWo=(P8My1+GO%Ak!*j`E1}AqQI}sL8%qi%t)&fzyQd z*1+A3=y42CoAbup1V9bF%;>oHtbNTLGrZQgmo5ZmBd@Ea$-THcQR+=Vshn5lCMeY& zx1rrykZSS`A{FG8n}bPJ$QUUUvOtgqft!egnQb7LU{BkH&QTbY7&&6<#b7f;GT|Gk z1@Zbp!p!S|Ouv=JOtCs$Cpuk4bova?>EmfS8MqY4mggO4v(|~qmNujInCdCGb~`4t z0ADyBH$OnZTuQ~BGSBOnE5s!ma)V~x^m~DMx22ia1#-jO6mi)v86;cbJglny>6R;4 zLB$$(TLF|8yx4qP5nJC!Z2dmSQ#bRmwIxg}MUsvm`D&6C$kV?0I{7T=+6zEjpOWM& z8QMV8GBf!)OC)-STC*Y#jS%;(IaQpd6`##OxETo$03l3YUXUaJ+R%iFxfo)p&_3eA zl?F+PQ530d86*}q%Yl`mRK$xb4U!U+YVkX%30IC(%LD9gbFbgB_Xz36{W=M&P0n> z0WDsc6fYW+9gE%6s}K;5LFy|!Xy>yBNF*6B&0UB{uK^-mo+Of`PB6L>j;<(`N<;00 zJd`V-fZWA=DB(}0#6`e#Zvqo;qrWx{CL>bRIV*7JdDjFvbV*!a`BaU5{SKYHRucV(HUidgXCRmRersBY4Gln!mi-ZdHkd-#lLxEV}axRv^HyK$x`d zZn+LRwqcqTHJd+RH-7V1Y3Rrrl(m5R4=T+-9gq$*S8EW6wQ@ULk?D`qaHb9w-@lnJ zb%>TBEL3<8iT&+?ci&3#u2hpVu^rk16STh>P1Oh%lbFx-8Ro^V^Mg*qIZR!jWeV>l zrrrUVn)7mm0-{UA9l5IL9VmF4m<3VqA^+CgKwRx%O;MRYKMJd}H??=RzD={W`6LMI zUnVs$%O0CUSDjj;XkF|fa&8ZrzO`87x0EPoh%8+n%XvNN*xP|HelsnMrP=L-|1|P+ zfeLo=*Q8({1w4ItlBdKXU%hI*DzJziW39Xxzf>iQTg&@Eg|^c&eC+quPgO0KJdxFW zrBhV}gJ7ns|DgXIa=-0j@fF4wJI+`ER~go1VpMaTA9UL8j&Br>A}P?)sj38_c#x^y z`r~dF;VVO<)Uu|k5(E#?5z|U@pe7<-Lz}8vE|DUlRXSBwFbIjGo@43zvN{c*_ApPuw&7#plXyFx`YK?4NL0HQ^VSLe##UUe&Dcv7KiurWs1r1}sd z*++n6f1Z{!RyZ(PB$7j$b)uPmzpR}!){~z4H{iQX!v*_Ff(aNxq&6&HX`n2 zR4SbY5JpFu%F2t;S*+kCUrDIQ){w9KM5QP-47$`gg@qdcN5&jwvren#mog0?u+(59 zbOvMBYdJRn$Bxa`eD2k-rU917(i3+Ypp5AFwB%w7wTuc@y{LAs@Jp{!;@1m48C?4F zlP*1|I*%1Op);#NV@mthm#rxP8c_a@0Hm>N(9K^JVoPA;2MO zIpdDuTeSTB(kZpH{$wJ>Q6R--Nm9^|BpDUQu!1y-xZwFY-D1sj;t~ll)0UDoN76|o zZ7%_7dr?x_7#O4q{N*b#A#4+L>1s#N$nCU9b1x#yJAp9Ouk91T)1kJ8N3qOgTz>wt zSShV5$?{_oD_?DVtUSsnL9h-RG$xDnbJTYy-_90P`Uo%Or=4?cnwZFJ;z z2I$ERlSTvc_K|NX)ysNgIEtR%)%A~%P9IU?u2kRp}d!BOWXGFNUC(o9pe>i9C5zumsw`IiP~M?DP=&X^&UYWJ1UqG7On;@FEcmEZUn48nZO& zLx7f>l4wbdPl+y)O!HDxO5*Zr({L}(F>CPAj`@CQh@@kZF{suKhY=c{L0ap-0}ek} zjYCDlmL6iNu8lB9h*+@j+Te<1Rx5vVIYz0#CZu$N%nNF-tv;hSB<_KzaW&lZ`a&O&i(H-dTwPQVDx`XQhKNJ!WdgMber1j0K5oA+(Cwp#}X z@&QNZ!{&)crzvP42IEG^Q6?@4G$BA4u%vnm-eUU@)C}(COl2b~j;hhcaT^29i&h+P zzJ;9;`Ruu2Xt!dF`%EH?{ChUjWc~b{aa$mFP?TuP>@bq?uksn(21{M037#uq+5#aTG}s4o9FdiYio-E^g3Np_=>( zBBGlCRWhi7(t@-tPZ_i2 z{H;qsV&O(<^`V~~fL$-oCEp5w_OqFJ#6Ov#eX2Zm_LW)|77D;TC zW}y=_WTSV&5phXb=n`IRl~&?on%bJZp|`D1&jro?$Sv0FFn%N#LzBVUHXX}V>of4s zCb!+ieO;^+iD?Hzhm3+QMqL>%W~_kVnspbfQ{F9ys5GOV0DH0WUL7!?pA^yDr5W`E z0a+MWJPb)&E)6(WKrbF&m1Y+cBy0^s>g_txu;BFIN_ho9psF*fY1l}Mtj;`*g!Kjx*6X)e zSXYXEkxWQwDydgVT>}E56N;bdFT-E|hb(!nh}Lq$71ONwad^85uC%CKS*VMfBy2_e z>Q^8Huu>KmgJM+>JC7fp3>0!EQU!R;Mq&^-SIn#1p3@v2oeDAC4bV%!+@u&YNh7;{ zpwtWe^o)QIA|vr9>G$&Ae0jz)Rly>4O0@O#|4FD4%hl&0cpRy1%(xB z$8?8LCB{K0&1WfKDn&;6&r}3Z-u=0Om#(Qz_qx^Tr2!JG zFoZYIG(y~BQS^p{|86y&64uf*K*8{&&U!$DVPbWL94jfQrD=c!{aP?M5ePU{!5zk7 z@b@E0--*e=io83!E|7b$FdLUcpes&s*?-h-nOczj)HEzuZWtGymSNbio-uk@-3bif zY5`_k4Z(ovXZ;MK!77LmG4N7cox!m=I1K27R8Lnx=T}gXf3y|I(RzLdw2E2e)HZ4n zNxR7K>fPO2*{SU%({0gH+v4!pKIH>OYbXR$;6l^S{F-`)-dap;i+qZbDtbfWEbuJn zNS(-}^c;ZK=vGzb2?P|MNn26)5^octA(zVP|-@Ny6Y%- zxjoDWd^;Vy7!6KJ#LNho%aSHXVDjTYG63ITsYEet#pH~2_t4=Krur~JFU`)_f>5qv z;=q=t#Q(>Ln=n;4y?>gUrP7{MC#%J06^d5O6j^d7rh+^9Ea0Ow9_Z=7q6)RQN{q&x zf}5Qi1>I!<6_~KI^a)I;3A&&!e!&V**b3^Dhb>RaV}Vn{qJt83Mx!?*9n|fmj#I-n zS=oGxEW|^>LOd{SA&g;X1Kyp(j%bub+H=XsfF)|RM?_R83p-Jd%Az8%WGjI3!dj#* zLt@KQ?)s$!hj#-U(l0Bs{xRc0J9O|*b((hR!$Op+$u>3)QRJfuD0K0He zKv=A0zhH$gYAb-AS1e+&(8{qBkV1+-(lWWlA>kpZ2p%N#v)*9k!W*n`HeUVz}cD zi48Y0Tt%^IE3T2Nc16t)xOxN0 z>i2@I-c~KEvWgsq)x20_%Z0U+t+KF=Y<1SZ4M18aaKbQtn)|}vz0=ZabT7L(%AHAy zq|9!rAW-E}MWFC=_W12$H^a;OniIEggRy-%J+@xGhAkL%Uc9VRpV6bo@V2zX0CkJC zDVb|tu#hTYMIxoHtJgm;pYRwAD4mf1g}{Mt^l)3hn-;d zDh>Na;x?So(%du6Z6mpb<~p#-y$i2wt0%Nby4eE*17&jToWlq9U$pPwp@SDa`{057 zhxc84_|T;X4$pQRJ4PMUdIs5QXUyvK^rA;BtE=X-#7dYEX}*vgu~n(W4I`h16v%2# z3HTQ`F&o~i|G0PPK`Q9fgAWB)rCKr^vf;TV=xz8u%`#mQ$Uowz*$aQWGx#oWh8Wf2 zuEa5oh%MlI!XN2HxRDM#K!aSq(4xh1M_kI}gjLQF%ONnibjUKUSBlFwD@lgP0z~=T z3{g&Sx!ef}w6%v8%7 z44#9P(y~Eq0==;Di!{uAFwFmw942)w+XqWLzZK(GuP4*lHa%d@F1X`wOtRpsF#dl? zj=$I=TOt8Qf6O~%1D!#go6@sTlYb`E?+32`bOzUDz>1;A61lE4I8OBG^c};#z06|L zi`XMoSVI}_Y&FJT3V?(aH`;%t2+*kgdVu~J{Jp$d0tSWvb*ze7=d7`hvfzRrf4eqN zHVLoS%3=B|ute{LK$=r8e*WPD`z|?j$p$APu5m&SW!Zrc7=zC&82q5zfa8iIZ3jpd z5;P37;a3PAgl^{=uNvrpdeG?;!WG?(RtaoI-LNH`XXz%4L}&pT@mv{K^r0Xt0#E>^ z6{jL|32HGF`3-aLNr9NL+D5Gb*7r6xXidTY(hS=M^BU9d#<7gOp*h^#B3cwbKnu{ql?D_J~8?*AsKg;}2|=EMc5 zB?nyKYS?SSaQjIGU-RMx7%ijJ!L^1uqg(3={wbAkZXyLkbegFad`yWCL(b`m+l=mk zDWGBq(=UkBOc5QTez%8+jkLd?*X*EYnrwT=mnFJXvAa-$+{_#(IqVT z5&xNn1B$EpY)D3{YPBEXK!r%>(a3WiLX~P1oz|nBH97S|2_-z{d!}pxc{QNO&2{sw z?!)aF@=bD3;Q^}NbP65~u9)Af=b4#&MO!r^bj?kgl2Z`A>4)RM*kq548YdFk0n_ks z)Q;iwcoA45YrNKot_*cj(F}F{DhaEi^%`OOyQRXl%IETKg3O7I)cwHo(n2!5lVAQSfO}_Ofskvnax#b+|ti0EH0WDUhFs~7b?K!x>hda992@Ewy zUv3))k4|kiK%wW!&%#G!61YRBitx*fE>aMi=8~;OZA)gPs!Bx{MGU48_L5pP%ES3- z2Fpr7c-;0?Riug-(cgBS#>e)9F#r0qIil}VIcRP~i{&{HioRAGEv(SUecWkWp1n#z zLH@e?m}HyPMa>m?sm?YHNBwV5sb7Jxy#gOl6(kD^yKS(bw93+Nk(4hhW7j3I%6E@F zFlS;s>py_{uML$i3ldAdQU%6tUK70!@~jMTTMbyqp{md|8A+e)))gNs;2)7g|T|391TPl(1^AFcj_~J zu?01$6^;G2sL5DiY@Qx5g&m6cRhcm(6*5{DsBYs3OE1j=p>fYeFvPG-;~L;U8NH#- z(}=i$DV(N*E$k47$zcfS(^!q@*fI5Gg4WlB6JLP@t(gksW%1-lb!=i7F5Fa59ICE4f zqE%}|2a2K|4GXarr!7t35w|Iyutr<@y9PSwpE=}IFYeKgHw%zz zVOsaI80>@=qhGp{&yXLZ|)*vsG6a;5ceO?6rzA!FuxLMFwhK|0qwUV#^pkdK0B0Yks$xl(UzXadE zkkPEh6m&b)Y^uS^T%#SDA=pvs`D@_&6&XF}8r+`qMWbG{3YgsHt*;JK-Jdg0}q_PVA8~abcim1-YAcEekmrY$Ko$gZ}N*h-hkdllVb6Aaw zE;8wuIxi*aTo2#xj#CF#88{lDur1H3YL8%tC52~-)I1JptHQ470oQg-85ii=<}9ac zFCnVE8@{hgQVl&77sA$!R#)L4nLkW3(=qtY>Dh}*dZyt}OEUD4aw%4pb;f=X;kxn_ zQD1K#;nF^AdS154=g? zytW9g!DizM|55)BhG}}%DvU$s0;X`94m5JADjZHgG%a3=I&@tTTX zDV%;>uvpq%S?5N{V1~61u#HYYI0;tDopjoQWy&KtkPx_w#4*IgZz98JL>xRC`Ve_M znea$z<%^&<%9J%CH8KVM;PE4muU+i5)8FHYb?HUlo>*ger^H$tH!nS9#T%Dbar9DI zo+SR)bVDb>;r=JxZNU;R$@VDn#yd1tDzFG-Fi3{UK8${&cB+{i0nz9>*$?$)vOzji ztP=v1M*|7!$PQW2!ywEle3q*2Y(K}0PbX}%(j!(KBo?lJR14?!1K{F51B5e3-#F@? z;9k=!X)6|nK17~TIx3~Z z3urogDUhJ!N3_%w6f-+_o=_Xi!M5@snbN~4;M?w_MSVNG0%-f2w?@>}vJNBMB-HTJ zF|11KBbG-|A4NSthDq9aa3NPXa6Jr+wC`sOVS&ufcCe)Dy~5f)PCH^GM=4wOss462 zjFdq(L>wfrhRYPCXl z$Dl)UwnxcOk%iF-AvrXdV#dIc40t(<<2Zq1B+ONwN;U&F9dEyS2sUGk$2~VB@DD;P zjDC`!XS+nBXbR&hnDoatOS&y^ZbW-N)L8&dlqad!`x#L<5ALt@<%_?N?xUQiqk&}n8#ByRU$u_Q*45{#J` z3qY~hj3seYK>I^+ss~KsXg?lB3hV!X@1FpL6|B33%5euYQV>=ZU$%jck@Ai%M=hxT z2P^cC&dk2{M^k-Ihwq3~?{Rk76P75ew_R*-$WJ3AT#7B8PHdccd;} zfURR0JcI*y<8=`Wy$2ugyLOL<;5FJd9v1kXN45*-N>tCVrFJWK{7Spfsp^!WO$8e8 z34|3y*gZu-zk8GWVP#G(fAUtm03SrfH$s3ZtEDjnKr*SLxHn;Sgn6a~M>AV(ziI9Z z0#fTR=~P4T+jCCv{YUtj{sH_YTmw8UV2HyYVQHU?f}E4K0H91vHq|)<>a-dZvkc(t zVz6FR?>z`1nbXwSp!Q13;ZX@^%}nIymBtOfGuIpdZ=tOqB-IWF6pJ_tE87wp*vMj?5Wg4JH;}0}XR-KqMV3nKynl>>(y9?-)F-xCyI^JEsHaVuLJoz{H{%R((lk`pA3=x4CN+1I25|A;a zJkJzfP&9pD6*7{YOx~Pt1Pr5H4vcn|z(^gg@A)7ZFycaIs{LYTXX?V8;=E_gP{A_^Dl`?F=d(~0lRok6R7zkqkZ8#=-8uRViK`ym8X z-w)7_dZD>NGmx|)$~rg7a1_Id5dOJ|FskRjN#u$f=xY*DPu>R|JW5y1`uhO_XQ z-Ut5fl{NzmENaVEiji$gVwW>6HV$z3llv}qCEw_|^0|`AAv7EKwK>Q8Zthe4ZtwXI z-ULcdxfNqQe%0D7Y<{wY+zx@YR#E&0#tx9&o0{763h-f2dqS^NR_|T^Vp~j!zFL4> z{CehzU8@Zp1!F0P0a&_ygKKb11w823IN~VU44WbSYYmSEl2^^cyQFbA-FJl!B28b& z0-2)t=<77nLom{dk|Sjbx)dWqD&kvZ$w~;XqxOR@hgJBK8KVfV=H6uvQfqUw)}_rJ zpoROENKy)Lt}}ibI5M-jJWUJEC3cQZ(}IV~RCMSuP%51p0Enn`ou<S}JvqPt@3RBm(x^rd8yMSAVY1b#Svnq%_m+it5$mR>V+s z*&Dxt0UWZ{+*QM&fdw#4VwMYzxY2NsRZQT5t|}Z7CTl`+qoy35o7Tm~M`y8FQRz_R zh&cC4v*5Dk4gfe9yHrXhd2|(aNv>$9WTK2l^G~3KZb=K5nb(gbjo1bmW5pNLe~E`UKlbdD5_A3SJ$zroX1Eod8V9;SG z%@;t#|1K%wp5`{Bm#v9Sp~}7meWbB zDZNp2`Y#Y7re9xBOn!-&9%ELAzk4fVKuGk`3Q4R$pVd|*_I?EdP-0fxFIa#Ozo4EG zoTJMXn#%T|E>UaCQ=<06q^V$C?(_j^O_i`bvMO0Okn3{>Jch?0W_3v=xNQZ%=mKop za-_s4BRIVf82q%YX0X+ZD`2QVk=3Ta1Z0#sEfwm|i(v$W(m4%Fi>JD#PYXNg&+X*76hz7KuD}*zhH%xvK7=>DO;YbR6(-7x1^(mHLa}`P;0%cl?2jM_tFne4}hk+pjuN^I4we|VZbm^p80ugq;%2S z`Vgo%Dr}oyfuMQvdr*fM+W|rhygLU!$_sjGHDbzb+Xxu7VKkrL5mS|4K~I2D2m-*s zYu2Vek_JqL#aS&_s0_~DdG$zz<*{Onu&A&cwgM<$5wF|wT8~V=to2CqOt4rNCSgGd z9QGZY>@6CeAiqP8DL)y(VZtSIon!CL8L`w1SBo+g8>`La9qTgN? zO^<%36a8)k`n`8P`n81Tgdm{WAP>a*5d7V=)daL&u@UWJlp7t<;$HNI#MVsJ7Xjge z34|X28s0b`4MSBYb=DK&H6dZa!YV@|VlXY?UpqoY48|X8tWEC@9w+X)j2{BkDM~Go zNzyRtj1JM_LiXL+ei+MO>5Rcl1;9f5nl47KZWY|k?sDWJ!He?nGX?NZ?=&ATjZm;2 z#S6$8#Z%W!g6ktI71@#W_#d@I72Jz?SXr(l)%%j#s$9ZO3<|=^75p^+9sWMJ)fB7<((=tj zR6|OP&9om8Iqor8VC+e@A{=SxrhDs*$-2<6VE>}Q8A-_kvjxkQ*of=$-?ZAB{(FdZ zPToqjR}-=kw+%nbo$RWt?=w|CHYC_R-

@D-vH%*f%Vc@zA-ajWUn28g{fJV+J9Z(Wco zmOM+B6%fA3w+U320;n!YgUV2X*{w|#UPi^t3f&CbTxSZK8p& zCGqaIZYiA&FR{c=^A-5}$22{7T)Cr=ddmYBl)t4zZVNrrsVHhyzSg`Oh=hozYt5~V zm}rsp!!!%0Pl0G^b3PX4;BCz~Sh&Czxr2ZFsXdP=UXg$ad4o~QlM@=OZs8y zf)B3}gxW%4DJnJ#}u{Nhs3Ai(KznY8%X6$02j6Y<9s$lhQ#* zo%M9nDiLZaC-@FQTSpFLT#Cyki0P6^6o2bPzQ=`;RmEu!o)<2>V>iD8l!$x)dErlo zuWJ&p0@YxBfX_0p55(^j1{RU05>GuN7 zZcEdw%kq}Fa!6>VzBb4;0*!*JOnjGf)a{^<7A?%>vs~5Y@cjxv6ok}$sTOVCLu|c0 zur+;%Ern*5_Er|MX{*^sHH}OK+AoBu?;`(L$~k?VU{1 zQ^+6qaqu@zudy7!Q5;yz_oLg!JS-hBo3jB}4h*yA^3bsYVa)`3j8b5a*ZDAviYVEZ zrzqK+i}Vp_@6XeyVc{XsH%N$Sf|bLQGkI-;W}Q6YpjntCqBCrp-vtuBBT2#ziYT3c zBIrQ_LByU|h-%&6K$;_~?gigOz;|6s0O1_+{nnKejwLPCF zP&$Q{AQUSz9yWGg9EZ8yF2Yv^N2#UxOh`eX22!3WJ6tjiZGJxi*pR9QmEraNrLJ_T zNWmba&H{q$F1?k3(t?Bkfr?ecpe+OI!tR#55MkxMmgt z-Of1(wTwKSZO$8XQtY>s1?K`w6Tmr8t8Lipg*4+D5E48s(=;tFk~#^ zRY@6%Sd3v;@@%>>n#!o>`>Mt4l{!0cB1IDF`7_;?!@xpUyOeNrxI|hf-{WLb0!Kj! zT$WS<#7fIs>q>~yyFS2269S*+CGhv6B#k19vV(MOAz7-Lq~yPwTNDjQlb@U|)|#tE zvApDLlOMcUF>9kk6t`8PSYNAX=W_P|(|t_x&^yzbcY<5wZ0q(t?A$Vd5o{ zIsH@Z#!X?KzWKML8`q(EOEk3%x+O}~It4Gwai>O>E^v)*DNAK$h)O*n)p9MPl+L&Q zic;Zk)q1!2ThO~7N$OoztZb&ud}WLk17zF)R?hX53BQFH_hew)`ANo+Xl1i4CZFPU z$zuf{u5(JF?u^*xDjM}?VALN^jyeKYslPBVJ@GC8wlmb{H6Ar?YYwH>2C_|$o9x19 zarM~hthuZ_gDJAZHGfVGG|^m3c*%skk6icfgIV$>Et5)EP>+yK3T37xOe0_KvX6FM zZ8cw)c)V)~LddMKx;K!LkkhShQ}d9ei!c+T2=Omm+kBHxfd!yr()q-9WpKJ9SR9*w*+_rYABLZd<6vyZ-HRp z)k(*MI80sh77HzLXhlb8tAI*y=WydwdP7xYCsvWaAxzeFH%$KH8;DI?{DvAK*fY?K zVmAMVWYII+k0O?<5F&EMO`7F$4kDLhQ(9XvJpdm61xdlOehbSM2$YSsnM~}~pms)? zQ+JR@<_=sJSe9x)Rg=#$({QTtOzEMozv|&$?`4;LKE@Eay(!VzXj&3QIdD>l$cvB~vXde+aB}z>%1f%z~Ei`(oMnh%y+D5Ni zy+rg`m$k%-^~nHOL4~oi6+n66NP_$hkb*3I6LmsC8ku8#mvWC*4Jj(#kG#$M3M0nWP87TmDEQv_C|E4YYeB#dYXVL|o~I9}CLjWdnQQRD7u0`TtPyfnhJX|*3XxvS zYT5uRV)VKT))_n7Fd4go0~d@05PM9TZM_r;PKgNKZat3C6A zR*jq4ZiK6lvg-1&EbOoXAp9 z)BF?s-I9b9E64y;DajKYDr&wce<-mH(XELjeaE!bJao*&0FELL>OY`Nhr(U)Q-Q`G+ z7Mwz6#E$jf!ct(SB?F2rQ>F0?SYwV%`~Vo78@Et@MFLP39OedVJXK<;B#fjrdQ1)R z@C`(gdSi`f*kepyPD8+&8);hCW`#g_n)X9*J#KUT7R&KE(68WJIHQ9Y9eD<0rKluF zyv;`mWnTc4{aq4eG}?ehESr3N80vkaI*7F%OC)L26~y`#RK%dRf_Mz7R*q=iwPH|P zo_wdz>j$T>(SCYzlF7K`2*&99v#8Myn1ulM44By|Zoq2hrf6 zK!dZBG*I+Mk@BfPq_Jv-s6$WD?Z8P0uGX@aPVm+4GLN!7<3E9ES^PBn;P1aAN0}Io zs7?~k%hDiRtslN(a`&rlzDUF055xcIbF|p- zK@aa)#!oYYzn5o#UQkRR^aC5eO85qE7C=nQv&!-deqZBbnYpZ8@t70ZtQ_IN=(dW_pCUf*0X~DraqOJK2lijI z@8F?>7d`vnf&GW~U3~b^r3Vhrb{soK9kh|WACW6|AVsnj_>xBaX&Uif81e4pi0x42 zuCDEn6Tl92nv={>-6y)@TiyO16ApdsNm2nN1ADu=5^ZW`p2Q*iB-25hS z2u{;!-jRl0n^tT^M;6)F9c)92nhb_83y{xZ%3v51a2~K|Pc@4W&5m4a)=3i2OvMs` zhKT5mHZn4#h)qCyYL?Ge{~!$c-N_+S2dy8xH7XdXWvmYGoky3qQe9Vq2c@db4_J(mWQJw>QZ=%QYEi`o1ba#iM)m}%TUzjKaY5?*R$|K&L1-R7pU}u`5#?!1bX&p&;Te=Cz_1@X->^e3 zs?+OQtVU0ax>>XxTOP01$&URtiRAkMo7W|=Nq&`ev^w15j_2vNNi&j=23Kukd?P0u zI5C{#zbDppPi6>Y1nIF^>y`^b)VAe(UNbYiT7s*#FyF}G9c~D~nP?%DdpQmG4*{#k zlUNnn=B~y}x4O>3*p>}=os`MTh(Xr^gRV?6C;_mMKS)LNwXOfuQ-iz*HY z@7=mAc!o~oovgFut9{#+G9elOhj_{Qe*#-`O48N{v;y_!L=3Y17wku$yin-|oF8rn z2a|s#I|}x+c}{X{&?AMVh_BD;z*tK*pH$FX?{{Qs7hbR@!`+i+6)|to6R2<#QQ^Ko zg?lHd(8*!Zomd`&n|ILAFysEt>Y<5RWGgtlF@yJ+)xJcc;&@=|UIz?(dy;_(2_5-Y_4eF~#RDP#c)@V@WGwNI6eOimQVK`pDizn|@QFb2 zwr>bcWJHgg#CEs5Y0Pee1>yMFb`JdABZ*m|ZMK-=@Yv3<_Ho9CC767=p5g|!jDDb2 zCbxB-Zma!GJpQMx1-o>S-O7W?tl|Z9eg(qmLuEY>7E_c}P;pS2KZJ^~*RP;LBiIVq z1uL>Bw!D_EDIAx8pXnv=_l#=kLZ3v?1;&3F#Y-g<(-X9nVr64UtUw5H(1<8Q5@dsH zK`2*&Wm}%0q<{o%!9IuSBdehlSJVn*22zfq#_OPHUGuc+idq}~InHTAEL12s)S#T! zt58q2JUN`#Yfwyo2r$uclqbi60WYIAl(h<*@eveA?m*716Iq7|Tb|@x2|n->cBW4^ z79i)M28g2|ft#|LN}9;=Y4d!twGs6{CsDr-z~XMzu&D4PB1P647hS%tmD+x!zIljd zZv$*@KClS(rp&wGTMm}J<~T+7$TG5q4<;JoLiqPr(@@lEoyKrYNO(PInT0tNB6Z0$ zz!%;&ZpI1kW%i?5rr*{)-3Gzw^h*m6i#27bQt^SacY7oy9q=sVXt0PBh3aBvyNQsS z$tzfqlkr=w2wD6JD&knbf{LKWRsix)vE{~=Co^%nmWSs3z^ogp`?uvjG(|A=;dJ6#Yy?=DJW*2AMW`dIOCx z)gJRdY!Vs-w8Hq?@+8r)v;jX;IEZlC%*W0awHb{gKevpZ=1t$C3dGavsu5r`687vZLki-FqJ9Ue$_SK^qxGWH z^nsdE(HYW>2v%&XvD3UnW2d{}3q;W`ZuufmH zJFEk&O4cGicY@m?A?- zJXwgio~2sLxbFXBQe_ZdHQz`QsS4UFLnF%gS0rF9?$9AAP*b)bJ2IX+?FxBqc>??= zh?lU+WqOBRdD+4HVWHh4A`(fmNt$?bD5+&LdpUkB%JZIK~ch>kie_=I~NoFgdss_R=iNZ5?1h9(P;S(sIBQoC@0f+G21;Ffw>6 z#V5h9g-$_fWhT7#pv$2*5^!=t$a8*!MD8$<=1`I}LRUZu=7c>1qfI=^`As6m^MDx7 z-5O#PQ?+lT#Ho=FjZ(C;HV%+66k-T+(&K!9yv#{(D27Xp<}M^DzXg)=ss%|(OBoVc zNCJ$i9RihbIq6)+xmto&pGZAU(8eWe<;gUCfR?x^yt-rh;|q|ufl2o)JVzk-Ue%2rSpR@w3tR^`XYRcdH;kTY+LT!97~;{r1)z+lU3X7;&C zO;(qy!_IMqBY0ohEa-oOUGObMa58yquYz)~?AL~LXb!r)0zO-Qro3awF_*(yPk-`# zbw~s=M)+yo2!F5Z7egNxNyHc zY?G8;Jxa9~6;1D}AvJvpc(=RegOp6ElvUG=$0vrOpH|$%jZLFkgVc{_J3WP9^CW=H zocldm+Q3|3m1MwS^hz6OOV&gqYBU_W+@Pgp90VgJ7#(;jkySV7Gw?L16e=pQUTvM+ zxfv4&jpDe#3pKA+)gaTG74JeVO;31^)u z!eqU`hL-bHOeNd$l=JxCWEma?mf=U|<4ar58%{Bf4N!?A#5Z%*%0<92dM+jft?NQX z88W_vtjA!srxz@~Cf-;Y=P0q5TZz|)g@U~I;OTVJ3NOC?3d#L{2DyLWd~$E3oWe$u1jI>VP%<-Bh z&=M5~mWMf`=_81za0bTo+4D(-2^EdQ$FiXQgPOE zmi$&i!&XoS3R|Ai(*3+XNHh+tSr{CFiqU=;mNhp7&#c1{k2-nL8$ug%dVl@Uu-yAo zCEB8>uHe1EEJrC)eq&A=3L(fD8t~1BL7RSP5z0v_%P( zXw~ljspV~YB|zo!`JfW&8CLgf0E~KHL8N3Z>7{8Z@eSTFRN0l(=vr2w%CA5`RbI;# zaI!7exgoYZxgq_$q*7E*Cn6lRzKI5~`RWST+e0AREG@kwxIu#19f(y@(<1}RFs=;& zuP1{y-wP_^8U_i)swOaaVE0xe%2}=a7`+{3x*wdFr_ATXwETJIrR2pRH_4eXtRAjf z8J%5PUpw6gIC;{1I4N>=N0?}(tN#shVZ)1w9!e(S5`f7ws$mj05#k-P4J)HfRz4t7 zxC^jo;}LLp=Zc4PJTv)>hEnr*$O}9s38j$#dFymq=8Ev6tq=mu*rn(V!C>X4pLTOt z;LU=QId0~A>!#>Pu@NS6nb8S@@SXWkUq{Iiy&*J_OQ*<7-FjTX)55`85vrf}1*ZYU zex898A&l@~t_mm^5YQGMG{%9p#sr)`oIC<}>B96`Ni|-K4<;K+tbrOKk8o(N7B@iE z=yHp+2zfE1p3Xjz=ihr=%^^!;%)dkhIHC#tKD(x3)mL*g4<--ugWzGle*vmVw3<S+hSMJB5oH>tlv>-i4Ht)bR#FF|WwX;Zcs=3g5vRXI4%^$n zVe9!op-zWwL?fEm5smP6FPhcvaa(|_98(5nWjwxwgpl(jX&d<@D#?2IQ zJ{BU*y-Adi>0t$sH>VNiD5!Ybt%}|dy#L%(ePl|5R@64X4P$;wa?C>8U`6zbVG;kF z_akZ=Jwa@xsfYF-D7drdXtlxH5t z@rrQHoYv9CcTdN^$2FsPhk!jWEs%$AngBT$wdvk+f51;&7rdv@FIcgf*H*xqu1Lac zd6KYqY1KHrBS_e7i;%F@!A|@rG^AQ;M~9zh5!S4rVpJ74PA6Wo1?$*p%M&|)SF^ME zDzx{7YIce|W0NK6OIgK|Zs3wDY3#a~-@DN>XQf;LJbXhn4`q%pD^`bzal6-iTcaKK z=1)&s1f@hlAj2odLO}r&bjZwzRwTqP8L^YnUu|O+(>)fql~&NNK+t+clB3<4B4cJd zutnN0;4W~rV;5>rp!0bdCv|YhTpX&27a4vrP;^CR=H&QiTCViN)yZFLt~NggTzy26t7JKt z6~@#D95t6^Lr{IO9d%|#7LV;1lmqdea7Ks|5W4{J4$zGB9SI%^SX7*{ zM(I(9-NK3srWRe;bkvN)3{&+_4GmmA)t8L6Itr)Tq9Fv`Mk-{qY#~I|m|=7IbmJo6 zgb5VrN=9#}aq0>eFon}y;hr<2JYEoe{9$4l0IvGl*w89^+Xg`#-o~)~69DmZ4j-goigLzf;nJcC!o_;pg%=A!C8kWqV!_^p~@04tcb?}xSW^CRFb zfelrOs0E@n0^S0Cb`^M3S6!KRsK0h_;dw90iX+%jr1UWlj11*?#gqg*<$+5*?AZ`4QXL|qViEI(o7oQUg*EQx%xx6BpY*+x z$w`x?NR4ElM%T-66-P_t+TdE(tH=^z%ns*x?(oHkk9wOcxd@WmLxOqR0Wx?00Os!I z1q-euqNvUcGTHNlcx3b;M}sHXuz3xh@*yX;bsoXXPGp(W8Hjq^VopCwf(HV)9ghPE z(i27|bWrC0nk!nPij>H??!YK<9-$q2BbCOeP4FhIenL;vL@EkYoS*=A5I@`h2>!0^ zvMvtM{kkcSW$xp*YR0rlsh!q+ouHu0Bjkdb^-*S-Xr8WF-wFYiiBhWXn|@_ z^xPoFa6{!OX3FVvau49Gov(i?lR&wK`;d6RF}d5{ykPNgxNYPHF)&Jp6C!CvrY(U( zuaNDdK|thaG9iBQrK2c;x5EmJ3Ykb~KBk4{q*Ec)aL=U(4atl~i=zWZC(2@Clo_RE zjcg>smKd7IqOcHn3&}7%NiXiO+3$*i=PFy}73^AnpaUk#5YCm^AUVH38OP6qalCcG zaxSGHLIjV3PHwla{6jL0#?hxwzHvm?k)_>ESv|pVBdt*L$_Fi~ZZf_rwcuE8zpHt1 zR>EaOEEsi$-^w!{t>S1E!&y8M3JTmceO!0S$0a?j&{UUN7$Gk??Bk*z6Z@HUI}T11 z+EAgn=v2myE~-2%7BGc_Cr!GA9-jm9X3hz+3a|)bW46=VKMf{>OoW?S_#29n;Ec(W zPVe%boMHQtmuC^Yfx{1z6H)oM(IBw$Gm!Gh?NM*^o@LJyMliP27gpH5rA`#E%sW9N_bX<+vE zZWG0%_H%5dMM=s{A`lsK3l2U!B90bC*0|DD*P^r%>rZU2*@I Date: Fri, 11 Sep 2020 17:22:50 +0200 Subject: [PATCH 4/6] Updated .csdp.cache.test-suite and minor fixes - merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite --- .merlin.in | 1 + test-suite/.csdp.cache.test-suite | Bin 192943 -> 136962 bytes test-suite/Makefile | 2 +- 3 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.merlin.in b/.merlin.in index fa3473765dd6..80b0b600eb2f 100644 --- a/.merlin.in +++ b/.merlin.in @@ -54,3 +54,4 @@ S plugins/** B plugins/** PKG threads.posix +PKG zarith \ No newline at end of file diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite index ac5a25bfb9fe09e447ad548d2d5e8c15831c7e1d..36efdf469e9de089eb12dc15e3a35a6c8b2d76ce 100644 GIT binary patch literal 136962 zcmeHwd(>@LRo~g?yVUTg{lkJ!Y8pl)!%A&#ZWICxzt?>Ti3v6-7Hz{TLX1t|22zBf z0%EO7+w++w76kb&&*Tm*!wW)(S|})xAjn(8OC1(L5UQhqm1vUAxz?O>z2;hbuXFbK z&OYa!Gw!+jJ8SQ~9>4jUkM-DVzvPzJzil)cJp#V?c`SS%v%kN8!Ly!w@|vq}yy3>p z{rxkO{k_f2z0Jw~=H`z1IoaHVUy!)7x%m>C!Hdo9qtTn;_#2SH#V4w0Yt{VeXw>{k+^jQaPHp;a+uJ;YKdEvPsU)Vm>o|P^ zARs2@GItt&Zf{O*|D{c={jO~YwP71-ed|6pV+Z~_j19vdCh72wY2`g|38vwBymxoY z+-vXJwpVTg8uuB9!n1gf$>ctS%G|zVZ^s<{Qts1BahGkod@j6Ye{+ju{1}q)RdBpA zMsu={tgt|MR6#f~6=91x^Bl_WRd9Soo-^CRxlXw=g&a$^wqllS+Z1Zo5vs>=I3A1J z#T+qhq86}D*fi0BXHq`@5sp7wZcm3?sU5dDSsb4DOs7^+8=gXC{}dcw(4lOr!XlHX zMO-!#sZi*}ROt7^@kDpvEES+^LGD`0=ojGla~*0gIan)XYcGkQe`pPEC+N0YTESxL zTDS_GUiem9*;67Y=2#H?FNEM7aC}!D!Cio=#67a|j9_Ai(T1U&Fp#Fk7?X3xcr>Z3 zqKdO?IqNwYe&1D0U&kj>9e)OnFOC_F=EvAGINHkLVMomU6@j@wK^|+z*y?9ki{n|- ztEs4$!tod5qS&t(Sxu-=Ut3R2d|SJD<`j4-x(WSsa8gKu&KW+<82-DjOp<;p;49>= zaZeM^$y+Zq*(Y)x1{NJbl6g!Djosr+Ge)BygX6UkbRN4wCtbXPKF9zF{~3FMzdVNm zzsQs_Pw#}>-Qj8C6zyTGT#WmVRZ*jk5&t0Tl4wvtfU?sa67 z^lrfMcZ)cRY$_$D)DWxMy^8;dh}5Zy*2GU;MHX}whEJdh-UP?zMoedYx9CwUsuDg( zw9W8iceFtGc^7=&nHQ9e!{ByfYJgHx6iE^T&E7h_2Vtg-@)NR$>i$EfcB9dY;P}EA z1PaZKDvN?6G*m&+@`)e3;g!NVAB$V5tdGF)gLy2_kM>lu2Z_VuX7RE)BRKwmt?40% z{0==iMkR>GEm63=>HfoKKA=TmsBG1z8Z3R1kF(Pl4N_6P&`o#cs0Th26_7 zxxZYv1OSXN-A^qNsNjzdIJlbw#QElORix%z6#~X(nl=;9ZSL=z1AF3)^N8Yq1Qh>h zUKy=n^70G?K{Vky! zAhWfNk@4xhOPw#^L9e4>5?mBHP#eE)d^c&$7eQ-2KWDA+l#bOYqzI?3y#yLV(w4Q- z_~v3-FW~~Gc4a}8+Bvcz&7bEM@to?YxW2UYzq0FZzIKdA1Kb9b5#B zUGYebU2D!-b5v!>1)=K28O<5phcO!r;X&*ct5A!h8GnfMhJr-Qzv^RAJ17wG9!v(Bkl=tZE~2#V+hnGAEm{^PfDUjnq>^s@HxS9+4kZ7b zHmAUpPDC(UH=ad`$2H{{1hyt?$}7|^_y&)pY;i5+IiA`q&X-&sc0+9JG`@$_Ozpb(#3 zh(ZK{h9B(O)`3#so&%WH`Y^3N_=;eA)xk)xOFEwP#-si@^~NtEkMd7;wHRH*sgdMswb z5fMNu8g@-M6|?ouu1B-HC~fU~h&E<;!UM(+yFy-)o*Ax9*GXSf-Yz&n1@+pFEqk7geSoyiXsVsNk3)bUOJYd(6@?Q7DtZUqy>?jK_*AHy%~3JYUbG9 zRR`ZgDXew3Fe|{xHr{}pVqj0MgDfwW2*6u+@JU^WhCBisvQpC}zZ>Fo=rZn^xTIrY z65I#R2l^B6(+nBUs6gd@ikCU#vDToq2B|tRvp2%WAjR|4bk#jO7S^nr4=JmFmpQ8d zd6=~(tTiFz8+nJ4CM0x{uKL$gALOmj2YGW_AH>Thtiqb|u=0Q1VK=5qdJ};g54ux$ zhFA+cLRR(P74f)gEhs;SjEk$Vt1izYTcZzdfM*WFUiyWkA%6`T@})UzNK$E9{$e^7 z`IBp(u=WX|L7vJdP%j-cLAnucg5v~t8eG!R(|g>xXjz-Magc5%uP2BRomFN?)>^dI zqW-kVx*2US_zKdb(9IkoH}eK?Gq0Vqn<*&4T17aF3(SZOU%ZG0aEdNiPo0E_06cb3 zIKT;0{YcC#cZW$6FZ>D?ZjFvwy%;?ej!yx-2v)V5uo3e&onseL+5pqmKtf9j19@wX z*HgxS1;;Oz6>gehoHLD{ti*9`Sz_ayX~iA}?T~PQ4Y*hk$gc6vutD4z9GxUcUIxco zJ3vxd49^1Kek_x1fI&v`Eev)ba`Y2ai`T#rDv{g%4WHBw+rh0XHT}wX?>n_C%j(!#bP*s>(#5luYB#`t$zd|uAc-&a3un}1w^y^RyN54{K zs_2LOlAfZmh=jGR4xXMX)?P6S#9FDv9Iy_dMriZA?m^XEqtapqs_Gslw)UX=bD*DE zj7Ptcaqmyni?wj{D^;dl)dfZu=-8yBbW9MeYw1^6%pB>rOOe2n;dnJf0>#+Rf*_tH z)<_?bpQe1@2*+QWDZN16UG9G{eCiY^%N0^l%j+=N!#hkfJ|&ckWsgOKU>Y?jSAu=U^l%Fy}C+S&_X zm7VNA`%)gA#a3N+DR0|*-!W{d-NX0Uqkm=GIJ6fpYDVv9zUg1kh0QsShTnKCUV>*I z@a5)$w-}tfp!2$?o5#;7=zJYPbvGQp7DE+=nefYtU@S%q9Y<-QH{i1dX-3>K)c_55 z8GsOJjA}jfAtnB8JUa`dp{*as4;+og=i~*FZq_-BX0X_;ShrwP4Hg`3W4H^8g>Fku z9YKRim*NJG7fon$WE|4p6}sTwkQc%Ci0N_B4mU7|l z7sXG{!;bG}S52Q9R`c1Gy8Vx!cxy22KAb_hc*1kJ;mF>N#E$~S76;BY!HH?^nVx^2-oav%Qa@ZXrx3I{CxudZ{YaVj^G#DTRa&{2xTdT*hvQR zfD`U_D5-{GHtX>S*67Uh+}Tq zKOt|iU?QNH?M29pBTN?f+f(=>St49cL_lpk856;HPSigu2}H;mYb!s`v5G*&n!A7o zH^axzJK_8GvfO4X(Ama{p4SzoZm=aX9G}w}02gTlh=d4r@ z8FnktK_KScn`21l@GF4&ZED1Mpnm@}28!wl2OI9uF*c19{7J*~s4Zm|rLbv0KKe$N!ail0qJCPA#`YSW$K!|FMs57)XteRPx$$@*O-$Lm?Sf68&CbLz znY;@7cpZnk(BrsQ6r>89gKIg{@LJ)xyB0XER0~o$ zhbRaS?YyrK!AvWTf5NA^KYVfQC>UQwQ*O;DTI=AKIfL<==dR__mQELsUdHdU!g$5J zxx$RRaJai|U+@9(kr|PpB{SX-C(jw)4(+%tX+jvFkS5vz1kzOJfTn2-_aVTC;HQCC zzBKqYt4trlj26thPNXz2Y=)4U{|_5r{ZUn*vEPM|z|+2C2zzbNpTMECFpSLiCq76B zJQ@(VB#{HL2M*T6QIHQm@J$NHFGDFXnM^GYCGINlt?nf`F^A~gX52Cu#=`2um%GOF z)-$A-_dYZI0(c`D+6s?rPql3v?ZI)9w9!`=ZiUz2e66vL!hEP!RO(v@Ss0yY9vqiy z3k~6wLL;|f14t7>36!a_+Lr-&7qIGMA=V(^|F%fTj7r0UXD*DONzo+Y!U!8aW8ld6 zk$Ek#1Dmc8Qd>S~*g`WF&@R?At6fL^F&8pan8cxw=Q(72)%mSxDGc5S!)jvQy$ih{ zC`gUUu^B`q**K`7m*sU61X95X*%QkU1pzDjjT{)bVawt9q!1@SA&$qYJ)c)fg8ZB% zIvETt9R;#j3o7rF#9=6FME!R@-c4y}H!+9Du`_XRrS#q}d5`hjN0n>D?%rd(d{CKP zrQG<9mO-9qMajII(GZiTnHPo2@FZq$|Kv(XhW3?K8l$hk@ym%cIMlI5%^E%c6My31 zGbdXkX&k-G67o4?E9o9Ir7qp-7yjmSe&vwK+MR}G*gcc&*L zhafE4^t`uUFgx7QA6tSnu#TdESIp(YQa6+6=VGdZ#$O6|t(tH3L%#|^UgAVqa3G>^ zP64)3!4G=4=Gny-3zA`*rLl6}$ixW;E=N$j)B#|03;+RxX`kx1Q31L7ZzMo|6#)5_ zG9V^`Ldmu^(Xw?pp*o(jiJ*EEK?QG!YRYejatbQs5e1Ieu$)kBPL8A2X=4t|GCMfo zE22#yFu#ew+y^jU*@1TmTM8z!(Sgl6w`#RX9duwJWqbq8Mcid9NQ z5`!>uF)lK1(`w=BRSlO9u1kqsFe~0*7a%i^2LY37TWYnYa{(?#wsVUnm+=B@@7?M! z@d_?UVh@|-dj*?9Ug28^UwE{q0eD;S)wOq3@U`PcdF8cWjT%^{-rQ71i~WI+(ex+8 zESWzLHji4mzgRTqEGGGQc459!w~P@L%e^=fPO9jdoIqH)?p@eF%JZidE4_(2PqZq- zmA0RxXEbQ6zLPA|{{&t8t+KAkNV6zg&~QP9bxjh?ABX~oPeR*!4yAGMA5Nqxp_d3>J{QMdz3RHa=)tH$Dj3XMJ3)I%d@+dqPv-4(55&PDLo; z63cBYeh`yJ5))*T zd=q3-$OKgk5;4jGoef!5OA0Vmkn+Dh>H&PkH3a-$nCS_EOVASN%nsb{oZkC>hTfTY zF+DCx*e+IIpbxA*tRcqF_+0ot^Z-rI8u|Gel_kU1Og_qnla9t>R9sTTV=yWbT>8u& z{jDMPsJR|`nb#GW4YoRf%d-PY49I?yEj_zUP8aXldP1DF7kzfJ?bPw2jqPHVaDjgjTE0XyrW#ZSU2< z3#gm&3#eP$Sf{>0Fk|6uErI35yv~A^Juw4{+Y>Y3DBTztE|FL-=q}PGVa?|N*v}lG zIufoXoR;mH)2DN&qbYqg#I?u>o04%$}G* zMWd%|XbpC@!%?viVG1fKzO&W9EgHVOpXeu8Mn;Kz*@{bo`2#QEGsF?1BBu@>#e8hi z4~odF1gojF*1dJ38wHb z4$>4NRRwr}Rp#~(VmRR&$gINGpP0c8R(6AX9AAj>&>CSOB;W`aF{OsFYheBGy53Z- zJY)YE*@Cx&E%=?XEnr3p(X0ZqMjL`g8oZ3~RgEz4oU-VTigbV(1X-ZQ`!o-hwncWrRsG&S#Ty!wRE&i9k020yh>B5Q0iI6Uj&H zAYSgyGd4YA*7wsf1@U*0a?p5as;`0$i-lr^p@@vo1+$XhOze3zu;*1}_DBTQwJAl9 zIb34p!TL4=>kR-_d69m-+*`qNS+ZKWl&%t?>%Lg2aYtd ztqeKOcN{QW4bkfbK(FVOb&=r^!MBG3x@mSWNmhY9bLZy@O8&u^?;=oO*V5)~Wl%(Z zU7J$WImIhDFuImN*Y&Az^iY~CVV5Zw2^jn-nC1zDA3Sl@+&vq9Ogd)5GQ%h9>fFj_ zSy$(h1X5WHEnYML`FjcEj{wLYEQ8D-3WM4;ceqSEhJmU~Q9Im(oGwX#6DVb^nGfX% zx0QlV1MB{q^16ROFhIr&=#}6ir-`|Ajob$j&o>Vx08Rq{Zh* z+5}3mYyp%!NAqET@&iRE3nW8)6Ngv0evqV`5y?3};H*&Cag?AwU_EZ@l=t&+yvi-j z^1y}J-Rgz`RleKw5b^-804;o3uUfcjNL4JUX*2!Od0@R+HLPko$Wi!>w0TjqSZLCSIdW%wO9wcNz*XQcz)z!A;FZQwTs3n z-l4*UrShnjgr%|pd=QpC$p!4 zCI2D8<`EQrz)Oysca+g)TTHe&>>W8-xb#6{3LQ{J%T2$@5Qa;VK9kJI$q+^`r*a7a z_;CR656b|yxsEzdyNW%j=8=Tv#{kU_7ty4SPmXuS?FJzT(ia(-oS~eA)^Jgmr82Az za|&6=kjl`dGo)+)Xe%X9ZQ*KQNGtYDYGY>H)?!ezlEnOWBId6HF;5qXDf|*b%`oVz zn9u@^ReEc(>JTz-PG%gcoAanhmSxI`1A?sYQIU$4XhODj4BD>bW6h>=;y|Gq+^C2G z$k36h9TicU$TIIK{wS0X`w=cVPS@z%!Dh8BQQ)PxFzwWQVHzV&%9IN_=rl(Ji>D5} z8>*uf4;G=hSVLl7o8)&Rf>@(A3a;Y_UcF41hw}-pPa%<;^eMQT7QE7>`3?#;{s-{% zH;X)NA*942Ov#q(he%)prbM_c$XVbPF*H@j=sqL0wy>jiaI>N%nw^%g!?ZE=DUt$Y z!%IABs;JOq36-_7d+-spBj*LQq@~`+k%I!drwq8s3by3x_)@nR>r1D{9_c=3XZb6tReD0Xk$acU; z&F=CZOj`JI(86CXY9S%$APwieMM)Xr6(ik)2&n%IK>cD7C_#cq=5Q*RpOm1btECJ^ zyN1x6j1`ZhMgw*^b6zooS8cvpm^VP=s)q2oucUIim$o_Q!b&Vkb17XtZ_edcQV9oJ z2IbEu9eoSv=$nc<+CnLKJ1*D0^swlW1FMymK8gzY)XjSW~;apCOS05=?; zbQ+%q_hp}mm_pfAIcO5<0u!&zLygIH%fo@e46ET-=KY_VbE*Arg!cbhvHcmoXf=nXXGaNJr{3I~&t}+7+H411Z)Hw^`T--K5 zHG=6`r`yK^lyfeoDLZ&E`o9z{Tm#X< zQ;X38$(riNbJ{~NCEIo)KMIF%!Mx1mOU$G{(!8K;fAtPCvc*~*-wrV^vV=)aXr8p= z@E`4Jmxi2br>}X2CDC}c7qeq)rOxccBtdg;3VseaAu8bMhFaZuF5$p{-L&rz>-X)* zwOgz!kTC#N)?dlTK|46;(T7&N{ah8U?-?ivGZ8+zlg1fnF%2Y<`18BM3v=1k>Y;w zLw0*7?4F7rvPpi2HP{2HVu**?NGNeP9g~ep@_EL2>Ckk;VdArcaEUeh{V*e zC_+k1lcW#HrtM6QB5|Z+?zkkQA1+Bc>n=$!vq_K@4~Wn{WOf?2S^UE6Qbp~h6_U72+&g>~&DEt}BSfKdPn7v484Osp^p8Nh3`A!}Z|={gz&V1e|@ZZV9TFpi-XY zWYG6>%AU}aq_bM*=~&xusc55CW4PU^^~!*_pngk*EV8u9p3tP%nQz&C%jj<@62Bgt z?sY|{OYEQuatCkV=E_X4$jqGWv3c_(!A8KNPY@R02Ut9&h=mabnu!n%g2-7PLW!=T z(;V#SsZ-0Dx4@F9Ra&d|SVv!`*1~$v=IO=O7MhharY2pualkMbq01DSzz_jL&p3XC zV7L}w_|YN^POPaQhl@i>eies?qwn?s3>WgES)g%AqAKz#Wu8){ z_rFZZ8pI_<3mt}-k{HE>YL7ru)}H1cllHt4wCCkhYtPVdFk@c4_|PJNqg#>U1Or}z zlkml+5MO#RwnKx-Z1t1zun|@S15C2vr?~*W=a=ciJtonb_HjRhPcDLwZ1&V{7PnK` z^~d1?Ie*TyZ`AxCH1P6r14X~1n$b_GAln5=&@9G*HT`I+2UfPtcT>~vgr>i{L(_GW zs5+2EH$5H$KXxlpAN61Cq)QU!yHQ;6D)uV4PppJLiaV-hj}D<~CKe5$UFnr&Pj%C= zk*VS=Wz+wH6z57%oF`1JIJyNGy4Y*mUJ!d?_=n#1KPS0g4syS=gWP*W8p&4h|OC?9WiM zFN0=3uGnnXUcJ7n-R=UrW1gdgnEW(pF-8EKFn@I`vE7fGJ^ys8esHQCU7thAm(&< zX-Mh=yQs`Eqch@>r>j7(esF5NGSrbyOlN~KXT@r9G&0!wFQM&M%+_{}NSCDPO+OYx zWqzw0nX}YqH>cf0(%Jx|<$5~JBOWMZ=-_C(xI*@_av5$=jW zx*3p+ZH1szpz-^0J&k${4~dy6(i1YOiY$~Pd1Shdl+AevQH4xb6FqfG<(V0n5ih6u zPOvHuFIp9)il9Soy2zeKB-nb0If*PquMpUd3JxCYBVyKSj+&o>2EL%!K&qu{XBbb2 z1{`qn?4s;+DPgoaSy^3}!({Y6awQi4CM|2|B&5`3xF}F~37sl)+1C37(7xvtW$uKX zwog^+1L3rJ?F>uY4RngcT~g#BLE^Gd%=ek2dr0Cx0f^jGM5Levs{}~*!C(Re4j3|! zO{nG#-JTlB>Ryzof4q4IzBWt_A0{#agl)sJxYrt zz^NtSss&`tP4*L#mg zZx%W(51UC>#U)8s#U)8}=8_~5c1aSk*(4B~jKvwSo5Db&JV`Cs z+$^tk=3QOx1QfeG8;N*D#(;i`F&0o5CCxgo6o|Y-!Rr9TSI>)z5$Z#y9B%9)Ba6XM z5x;g5>~7m`YK389)v5{yR|Tw!F?DJ(98gC)3@GZRkM2)&R^b~ILl4{~RzX&yyLl9` z>j4=qp)mUsK!!h>O?6_sBux-juw{y&g6c!3P-&q(!H^`Y>G(uaa?0B-SZ!uE+Z08z z14f`);y8mLq(>8)9d<8GtJu=mvk*>xA<8Kr=daFzoTxSet4B^uCysLJ!pUhB8Lhg6 zV}T;~W7Q2JiJpl9uL@Z3tN?zRd*S@K)Ob&Z+}TD-7QWo)$^R&bQoD zMr8SXLIzVAS6Ph5_k(WTcs7hv#JJ(YOx9CICcS0RAfp2BS`Q;YyX~c9?8YSt&@z}V znjZ|N^K0jC12VsE9zd7Oq_vC4cb355EhWF0^!0$(Yi7fXX((;SgcXAeHY~!=7{1Lt zv%!@rB?Fk#V}NsT+?tCLKf!>!7>{(;fXv$uyc4MW_IXe_r~1fYvJ7G>hTxCj^+&;8 zRdz1Xcj>|G;-cd50mJ8G6~yBWDfCYQ*PcHwt_@Lhw`#U_9<{R%!+ z%fy2W7ZVBJd`w0#R)C*o2fmv{qEO4kkOWidVoq9?x6<87PfiKjx^x}PPLI3#Dph^N zi8ls)Ikfkei|tja1fsXg2UHFaK<++=ga zEv=PiE)AOWf>`OlOS~jZ4C1AS5Oj0c16d#w5Sc5)At8z|I;Zmo!$e%ZoHusgOGteb zNcN%rNmgp&uz;dD2pJBtd_w;!`r1OeM-r5O2vB~cS14Qbdssl4hr5m6h_tl^%f-Yh z$kw5OSytZ#`G_F`1&_UItn;Ilz(;gfSLat#a;OGQT!T1^LHh_YeWI=|R1xngp^9{+ zYzi$&nllYmkVzJBz|$VUi*>j8pjli?5Hv3;R9U`$**_xx`d`7n?)B)WOxGOTSX#h|3^Vu$*mI)0K?s5K+~JMvQwI9o1*rmJpL~ zB$m7inDUA_nUaL@L=RGkf*t^%<>AQw>4SafSzY+l3bi6g^*E1}SF{zuikC|LJt*MU z=AeKkvWX{0N%M%OLsG!GO#XN815Ty6O9XMg4=6TI`hZcdkotff zlUIHP7=@ShYZO`-K0uRT$F+r@e%vo_L2RGwY-xASo48Ok42qWwr*9!by%q>{s$W7G zo|_ar7s1GPbWL~Ck&L=`6!MW?k1H6{wzDtR7&mmd)XsNvr6t#R16MK5 zMlKz$l1s1@z$;chjDby~@iT^wY;*5yIL8VmWE5>?G+8B6$qYb==MpV0toNcAM8&|t zRg35o>#E;(qdt5J>=cQg=56r( z?Kvo~aUHQ*4;m^Q@s_AgCf$W+!7LuUz|NreH9+rgW|njyXt7A{04QA;^L1 zWQRUn{nJF<7j+RR4uvj?ob%wAJ}`J;VZ-c;x-KQY{y*UBS7zfYvs38D31>51yDuE6 zrEB5(L6Vghj))}<`p1hINEkFw;$VEBMzG6@aWLNj3j464!V*EmYMF4%SwlL_+Dext zQARFZ$*6nuk$)E;_y1?x!9%s;VuqrYD=i7#Wa5Y!lkO*!GP1SW3vMOrkW*Vd1T@$mqtH`{&ik|Sh2)@1U3B|IC zu0Dzvk=KLQ88q*mm+G!Qj7JH^*|yuwtF(HCG;X=PZg%TJd6q5c_QOki@H2)tE{x~# z#)Z`Zb~oC)&~0-e9RrsnGrKK2U;Gfk|3HBMoOzgsRl$GjXbAuIQQ10@v8E(&Xc89K zi)dc`VvBV%+kU(%pb|uBme{z!#Lp{UyCqV~1_0R;N*R4b2K@k89~mq$kiy6y#QGj$ zInoWX> z*wStVAq2d@3P0oH@ZFsadmeb@u^lm|Vqp2qGD1Ir{j-9Xx47qn1b&w!@Vg|zUsjNb zHrN#Mbp7n=uTp;XBvKhLFRVj{wj5ZGQeh=f{QK|>w(vM`ef^BlsQyiCg>aSeBBQZ7 zD9*cEtm3ZK-;H@nc|GHm}F1P1Xg~BnI7j%6Gn(h zghu&pJ{m z`|9nmxg!;rNm)iy+~cH6iV8X)6=F_LZ&_L(dmOG#QDIM>Gso6A`XPg2EGK0up%cEdjUa|?R|d)73U6=5ecDHQEC6v*)jQ#z~8*%OKqbl3CzNZ@(Y@H5cx zHx?VNR6w*)Rc6s{g3N1sbbSzaCFWv2kifQt{L(TzL8@<4D62PvSyT(!!S1(4CvA9zW`C89`_Dz_~HD%#9fw$GQvJi@489%x~Y<|CQ| zgs-&adp{eC<(a0QA&f{1hs3n}RuS?Hm|Gw%>}wf5x`h0~C%`Yv_;%mKGKm&@3M#Gy z{!pA{B$9)582QK2yDkiS1flu6fad?2lb01#J#HeH)^8(#-id|ciL<$t=8>Po>*39d zIvovC3h{=EV97!*Y*UG0!etbgqdn_(G1`;;;$4y`w76?o=^41|c`J0Jp8%^jGMO-# zoRViwTd&szrNsDPH#)tLs#2jB7Vlug2k690+PtX9dZ18MGHqdz4C*jNjYILg6v;@Z z#4T}`P*Ik+izy6-s2@d<%v})4d~6PpOwRDFBABB;CNNr z)7@!6ID^^WnpC~Q5#DEppYe;}`$C}41stn%k%Mq71FE9>F_;%;!z;|Cv-Zv2|X8fNuF?{c#hGhZC#p{;KoxOr(|=gniELD1a3QlfDM!=SkQ;W=x#!vrp!k- zL&JY5MqjL%Xt`k?B8FmMcm>LUgDf?igyQ5s8CbFm`~Uffaz z);QKQx*QLF8C*p#Hy1Zz9ZW4v)4W@`a##<%z-u~XWbd;onYl5zGbz-8%`G)q8eFhQ z8{Befbfnhs9r%+QE7l>ZJ2$~f!k}huVVf|1i{;0m$BssaF6m+uumD$ZRGa~9%@#u& z0*Vf-3mNPN&K76sIO^PSrbwAXVdJ;srd8PZc}ZgY+*NGpJmVKd1)ill=En&V`Tiy_ z`pvPW11VT_5uiyIKpw!?GuiV%b>j{_6?D2ABw|jiRwLLh)O@}K|9>H`R>h)wt{Tbk zHk^9hnrwME2JzMiq67RiPlWH4#j1m0Bz9YyfFL3y=2x+4MO0Blk}rblY7Q?ZHX|BL z6L%$7TlVoi?s(e!`!J;C8xNZtRyE#{3Tr&y#v8F=Bc=6Q P(E5BM13Y}7Qqli^qI$m4 literal 192943 zcmeHw3$$%jdEQ>@+$)wy9uCdGWZ0qB$W^0-3mOez_Ica~C=oki+L5#+6i^TZd+~v7 zUN$r_D&brN>gX6Y`zA)=Hns|ah))s|o7UD?`$*#hk*79E)8eaCxc&b*|M`BbIoFzN z@3r??XN+_9*=w#fAOHOR?|;m>*1GzJ_kLnBnLH1E@#jqVJ!3YT?RniB4qbHKl~-Ij zoy~69o*kY}4^Ove)9EJrx;>r3H#oRConFl=ID=h2nYbng-KV;X3*RV_Q?-5q9ssef#EQiy@cv!=%5-}>#8+H)B$iY>=!aGx)G?`RC z3Y~eup^MJH?7Yjbxcst9F2CsfL+8Ej&=qgI=+HJ74qO?K)%MLd%(mBO>+3fkrGMb_ zx)03OPdxAP^Iwl`{2*_LeeQz)EBekpwDTTM$MLg<-!=RWHE-Vd&KXoa+nzi&n>@CD z_!(E70$+HOM-Q(jwu&vwpXOG#HgBXxjvhTc?Yj-a+lP4vtH*(m*5XqVL<7!oLA0pp zy$NUF*lcoaeS6)M37ZQcE*i>jlC1v#K0g^A%7#=u7!YDr>7!4PRBxaM+RPh0usXLf z+gP_ccN%r>0DSI;&KbnORgbzt8Z7k-y9Ymfkk$KmJ@u&o*puygZn;IL#e6jc~U zh2N1L)Nwv|{rEPp0DfnusbcuLG2OoTx~Z*Xw(>9~i@=PR%dURwVncBr?ct$ICV=tb(5<|dyl~9zlu|f&_G5jeqC0Sa+3*|y(u*J zTI$Pn@Of=QU$}(_2H~E8#VcB0P!Cc%@B-?Dr^?=A-x$5ZzVLm5SZaP zVP@C@%@5lcML0^Wdyf&h_bPOn;E#gUqJ^knnZU?uOd<|6MW+xaB6*l1E!+T&f;`u^ zWzG%PRHjy>pcGZGP)noS-sgtL@5*yu!P%L-pP+LGeBNgJV`%GGSPP$gTJQs@u6sbo z%ncCxxlTZLaCT56O)#ip<*%N-T3P_Gc`7iPoJRwA2YkNW9snVSEB!VNMTgdrZQYS<{uscbHlx$w_XM^jzwCt*PeYzDRi7Iq zLt`grlSp3!pO;u7)#y`dCz(R2xGYMbgWS@B$ffjtpKAX$d_EkO-a7N*nEdqMBdsk> zP&70Uk(LnJaOFkkS<>+&V>0{CrIINtv;WeUz!9J?v|XbA4}<*wIx2tAgwnmIp>*m0 zO@yDM{&VSyM)-V#rCEY^xYQ|^hW;s^1vweqX_W_sg2^yxf_Vn~ zc?f>*4^J>pWy0l*@?fG{G^uck9*ZX)A;4N%g>p3g`N`j7U7k$d0-wKXOGX59C?bwX zpcDFny{2!FB8X6h5|BX9|Aw~yDl8!M77Mj(%E_f_8h zpg{R>!Jx>XwgyH&lbkOo&vLSV&;vOjETH@VNTT0k5nA zICe%1{&=ne6a2(H9Lp0%f_s*$1FO2h(~mE+Eex4q%q#2*ltGb`O{B|sAiwsryi>bj zo5Jo$lBI}V8jJ{NGyEW~%lznQhcsI@swJ_!W=?27Rx`OGkAy=?n7jp&M z4a>B6g&>i(6v?cd7F`Z#9j%mVWV-6%ApAP+=Q;N z$w0=wL@fJhrQ=SSMlMDfT&7WjQN%5MQ@TYn&cdiu2%3~`iMYwAX2Ns8Pv$?4)?HaO zn}^2O)0PN#lucZcIx;l1OSg=W=Yb4KTk>04(!)C&Y)c#`j3}4d6FfrRmPjMywR8(i zBg?eF*4^p$W^BW^Zd&wgJw=08kVke6cw}#B^2j=>k1z?$BJk0YWk6AgQv9UD<1(9; zb`y1>$0>8Igjb(AD+H z>Job-j^?1W$U$kdYW6*GeTlATW}lHP?Z#mCT&r9Nh|U=`O9PN0rZFrR{-jv)1@VBV z<2x#IP|xB)^sc*M&%&3Qf@n?LBjg1P$xl)dsbLO*;Y|6Pf^#m`M9dW4Jl(9yxj5eP z&WfcCL82mPKCHZ7-}8J1N>7==F?(Eth;7OLqC2B^p91Np=l85R&R|AcF|+925E0ip zO&vzXVQvJ=PO{+FVkO~Z*mANI2ed+q&kUyt!>WTSta8fs8Bv#^P;jM|uraPAU7M$s zGJu5R*L5ut2#t=JhABgcmZoZIDNLMp`e>y{iP&>-*h)!sk>p%W=iEh-wLhgrl6_#M zUedFbiYN!VF*M1ZfM-;lQFRa@%2}4KttJ>OPP9`6^8~1dMk2Cxjxe&=iN;e`WPR@| z6vem2PC&QW&p(2{=Yx(%A4AT_n1n5)DOa-i0TCQd{v)rqIvJjH@Vq#A@H8TuA^O83 zPkqwtX4IlEj4||(0~C$6$ItK%SXuZ|xH9fnBuI|;-$b4>CS*2d%B19enM;m6#_wo? z~iy}DEjFKE8IO!4PB@mp}BNM?%oy$TnLR9AE z7;(@%@a|!8uk)ZaGmv@k_o(lAFsA{<9@d8fOri$qHlyZY8JR>A9UmkZ#2ygrZAM9M zuC~ybOf_(=M<#-k40SV;$d<@U1_BTC1`aDG$whExGiua}Lhu$jUB3XI=Qa7kC>ptS zMuZ#67V3h#p6dP2@cFq;u9M9$*oq;yPS5H*m-_i8_pJv)*kEpQ`E-K!{^VrZJ;B;;fPJ)%ZH?)gN?cprwA><5B2wWmDLv^ z%J@uNyxdbsZ9qx3DTad_e)KsqPr&l^**|_6-VXr+LAl^RMqp^~P@%i&@zRvaFMXMM zOGJk!Xuvzau&a|}`*Ais?}f1A*QT+v$IHRkCqK&^wZP!*TJMSv`a}pRv76Q8uIj{- z)xd+VL3#Y?@d_ubL8$QYr$e1MbnLA?MOH75$7dBso*%U5b}WZVkAJw@b30QHGte^T z->Q7V=0Eaqz-RKxFTK!QSepDE9)}-%mB#sb*Oy9 zsnFtSR${1;s#BYl`-k|;IxGWV6F`%wjN0_)|M$>eGUiUrxqViGPvF&J|7W@h~a#oETX^}?MTT`i#h~={fa-7g${EToUwQ)ecBb5;F8JZ$6DAisY z0pR`dspcEz&9AIX`t@MZ>|*Yann(FJ{=jjk%y67xibF~V8H1hX=OPHjSKd+h zCTwIyyGCjdS$#qneb^1Fljc{mkpT_VKt4R~QQKc;>kM+hF^wH z+}mcai*S-4FcFK;Y-;zKGapCus}KP&7upBR1pz|1P=Emj0p0@DDWSzn1tiw~A@3%} zLG^=iNI-oH?zAzz+LLq(a}Il*p7lQ0Q_-rI-d(R~j=#arOxUm{wUwzpMu{(!)z(Yc z`vV~jU_L3eaKq3b4`KP+K@2tQyQ%(WkVa)1DuZ;$zFbMf@NeMr{WdWW&*BH^IQwKY zAUIhR@`G?Dy`=?B5?6EhhmnEt$xZ||;N7VHgm_04m;4W{amK^5!ZzJxVhm37-=trnal`d--gd`C1T8k zRhKzO$VPw&RWo3kfUN1|oi)6Lxc;?PfLzoFO!VUW*KG94_kgqbwgcA4VoZ+VOU;X* z*QgO*la4Vn#o?v;2@!Eau*wu9q7c-{gPST@*P(MZ1z<4QeaJ?wr@@E?XW>klX7;pZ zEAevDV6+y8Yz<~^80Zl9_R%3EKawk+=J-iXl#Zs11}48vP23NkUyCbTw+5Adz_^Pn zGQ0u0{Q6|6*xs-*l$zLtVVwLK7fZDXhH=_bENLwoa?u<;!)xeu3(`kvtj~b4KHZk5 zG66i;1={AA1K?@Ch<1?S&>yq9$fP5}Q9&&0hqS2?Ib(H-iFh$}yT8eYv+F}}KhZVu zsau}G87R>L+Ni6{a$8&)(Im(Tc+UE4>m0ERfN(Q+%SYQu&0SJE>qa}N5nQLiz_S`c zLbKhnrj)675D+S9Z%^t^SUrSf-tlNWWDLd@7Mqla$@U@(axT42hMChb`fsNRJ0Ta0 z*jy$ZLve5&FkH4>sM6yJ&3mzSOrNKpxuFpIF3x<_^TDh=ub^4m-WDcGB;n9#rJ1%A z+s4oF8@I=OKOfX?*rKx=ZFN$>o^81oGQ?IUj``bMCQ%bdvBQSU^SdU_akx?~Q>Q*e zER(Htf_&LbC*hFo#rmXkfq1A+MGfC zr45XC&LRd=U=BY~R&B=-GGKQ7P2QKc|6m|P4u!2lsRlpPj)uAZu-zp(u4u&7IbinA z_Lw~|FCt?AHb#A8|6{^V3-jfv#%^Je*W542k5uusbP!mb_^Heddd0=09QXjZ&wxKxF+&ohX49rh?~@Lpif3~;3- z`s^!1Ds7+VZ2=+UbF6LjGCt63u3fniovzO|w?H^<%CGq??$urn&FWVG6u;;|lQfo3 zKd7eVuD)tJ8cr_hG&^xGyd@2e$wWCy5PtPl zSp7UqvWt|3so)5L$R66zfXJJ62priadf~!A_EC*+dqEV0NYj&mv`UF`V@2rUdf#K5LVJ@t_GT(|l9MZ;jn&It5q|S2@>BjRkaHvF3sK zibI{kfZf>IWn4_l$bXPCui8v%z+$=wb3F*Wn)8Y>=d-GLf2%*MH5ttM-+{KGe`0K2 zBA0|w0NEj&P5O>Zz?B~ff=@Gk7sqk864@w``e$De07bk>W=3J+4l#qmJVCNS`)2z< z$+%s@^;1~w1ij)$hg&9YVo+beI6X3(JObwnOT?->dv>;Pei#fybsJ=y@VZB5lSlcT z8rYy%!pDxtvz29IC*xPAw`k%#yi>ZPE(ioU_?9o78`Z}p2J!d-*_L`5MdmM zeYjTho!?ES6_;5ac2FUL2Q~T3cCfjpIj5P&sYcr(U0eMUffIozZfH2+3!t!1s*`=F zV)!aoICs5>cX$oVXY8JUgVN15u)DDCD-IIz5Kfa3V%bjUZkihQp*gFzGYfY|;Cj!# zS0;Jz>~G368 z##@t1Zq)U6!=6K15?S?XVn)XTHI*C$qwn2uLQJ4#?;SAO17S-)5dqPZp7ToK!8g{J z4idy%lc2L|6E_A3^7~7e-M_HO4}`=$Umy^$b-FJjXi+ z0uoMJ^N_hHqzsl(bO$1^NeG49 zjX_F}nazM%v&~hL&1AVdhy^!<6C5+hc6^v>&%BMK2BEDR>A^5N10lmqZe0aWEUe;B zEaZUl6XXg(R0U%R{7A5>;9j2U+PH!XlbjiF4N{Gjj1pq5g}EWtY!v zN%brMb`albTTEJ7TiCQxHu81s64*X%9oGm-TlQIb2xRjXl?56qGDP+$~rd7a<@L0ih>p@SRe_U{evP$CQmV4Q@%wYl=Ldj1o;hyqW}yEO1=5hVdur%j4-`sJI-H9P zQd+s4Mxc#Sy6x0WfI3Qm`XB)6cjpZ#<#sHIBLaq_5TKk`837eSYf(qJG-{oZL{M97 zAms8~z|p(*x54FkYHRdj+$70QA`z3kj3`C6SCok3(uooU3eJP{q89|-Trb4IQy)~z z_AP?5wxv63rMT8xd1)`iX#~`68X%{(YUi{;Mk8Y_R49+sh_v`rsnU`t7i=L42)_va zS0hgY5DkSBZ6WHg1wr%{@@sAdzvexyEkg@O*^~EFV3t}SgJ-Yp30jz7fiz$2pS(mM zi-yk%pttS3IR0iI{*AYh5Q`TZNe?J?20|zXuN;4B^v-{$HHy6$^C8ASrG?cI#BguX z2;#^s5+M-(3j*wa)ggiE$uaU8!2tkokn0FrSpVN z8=P;eAL3B0ZiGER?~Fnf*wH|qw&I6Q0~HJBRoLy&aVL}%7dQnz+D=>XQyYEQE#I1% zH14hdX=`DGQA9#IiG-AJ5im&W3`$n(=LOp0|zfY(eB-DFBs9)_S)FfQ&45{uTsXhc! zy?@?PRnDeR>1=%ns(P@%r$M$66^yY*n7JP*5*Cm2n@8YvRpHEKMT1L6jII7 z(n_z{GSyG#sH_iwlm3!!sLUf#!;9iz9k{N8zg}kZB}=@7)_gjr4Z(1RT=UL#Q+ncQ z1RAgv^%>njBUDoIJsto!@P!!!i70{NBWCB%E zSMY74HBJ{_P~aux+U(?1Wg>tYuSZ%3plAhlW zY#4vjQNDuiV6pBev3>)@8hLjpJkzrWvGOW)80R+<zKX}l?Um(p1f{ZFI*dOpkfI1B9krhGiKoCtn2 zzl9)O1`B+BO6AcpXS7Z^qk@S>p_EBJIP%{J8rZ|q^rXoOJ*3Ds4_|7a??hu6(BzxI z5j25qft_Y#{7 zu2K%t?UgDxcZsSEQq9kX$bOJx1T2m$@Bo96T|&nPExUvVk35^S58mWl-4RDuHY|Kj zx`Cu+7v7JP@ID2?`}n+t=MtMbLf{k{OKK16Zld_U|`P` zhB~q&;uAY$uLt-Yj>AugM~xQGYi%8Hd>EvLuG-qz$Q*6O$%GWxZdAW8juhrpBNoyp z8G)t1F?AvgIf;3oK~ZiC-j ziqg}nOKuNIE@4-E6X;|{PI%g@F1y@}xJS`Q{Ww*jy-Svz=aQxgO7-e|^9Efj{a%lZ z`%ZI5<{N>*cgrt5^6=*R)}1A@sEhGhJz72hxivfszF53~!L#;+lzuWq(1x}Tqn|b? z(Rw$xk2Ng0*S{b2EZR(RD0m()h6?R#a~>pwzzIdn-bgr-HK)oqHd7u_+7|lW5u_$w zS;8P^1U*3B82|-pKSPk;4Un(nkQW{WxiMz;M=69lK2%^sW>Ep#*z;v&1D!H017noI zglU;_qll>GRFX43IpXxVoSXcgJlA{7tAvQAEf+ZXKbUr#iEvB&@9shdvl19`LU9mMj2p2%N`mnoiPdb_%N8JpvKw zxw1e9C~E56OXLx{RLHfdCfnEYO%$R{bvDIu&7qchDBc1`U8SP2wdZ(csF*%EIme*~BTg$lO zcQS=t8xVG-+|c2f{g4t6`}o2xPc0*cUXN3;j2K$T?PDGYMS$q_Y<>1K&F`G9Qku#P zZTn#~9{)|g#o4C146+WFq+}gvN@>&205}3tNh~$9g@!=8v(Jcjn*(9-?5nqfAl@1k z1Our7c76|KEM7BCmmVP=^^vhxH$uA9UT3oIUrCQQvN7QsfgvM_IpgRcB-flIsMELb zs1d=45gZ~o&6#^cMuU^w=oJFtMz)4J?k(l%evEh;Uff-MAWBaJ9fc)xf2L$Ffvwfn zzUrAIxZ6Q+w?+jgB_oxl#kyUt^rAvvU&5^=cJ>@3I^M6+&I+7KWCoiNsxL;#tcBLZFflj; z36|@olhuOEDk||1McT*mLpGT){t40C&XXLfC13>yu9-xyd{$g?{f6iRM^?h(!}Gay zsKIrs_s+{Y_~99|CG+zy#eZ9Uj=?HceSFl8NmC*nq^6Y3K!LJCd#vZTcvT%w;qY%kIQ;e~ zP>4E`VG`mW?{S~ootCTX^%QueB?pn@PDt|^Lu#7&%G#2Vd-p+PXtokYbq(uLi+*y@*$UmK_?q`+RJpH=iij_d zt5!sQx$i40DnH9;G%hkYGqhmv<=*-d5ni_LF1zd&^cu#<6wDP}2`d3lqrmt92#o(c z>V^>(NE?h@or@kXc-)g?C!QBbVJF@>Jvp|)-v}DYf7+?>#Cq2^^rsJoZuc&^cRY04 zcjp06;`TT#T`beo$E12<#qh^M$|dHKO%mvu&F(IPSqltbxUYX1aY4BeAmzuje?=^2A0C z%%hRg5BqgS0s{##b6fIs+8`7^oluNV4x9T%)WE}%IBIg93n9#&oNHz-qlDtOb3;eR zwzj!Y^Oud=v`FcWlG1$;leqsIa6xOSw(|~_N~)BNC>4G=adpga=eizFL%9_Zkj3`waJApnrO@Kv52#UqJ8Dj;8HmZ~j}563=F`^lP+PiOAn?0o^UkA#LZl8l5##eu{B=0A|I zzLJ1<9suv}M1d!LJPEPpEe^rp6s-PhL;41W_~_=|BEGOEkK zj}Hx!9Ct84Ss=X7RCWn~_MX9}#BXk@#t%?Gk?kmiGJ_SNP%?&?6CP7FQDg+bl*^An zGa4-L^(xiAiftFoK5=%c#;HVv8i38RR+%ai{@O8aUM(uMJO zPUHbhF_G*Pjgk21EGicE+<&waAk@ofv=GA>s=2krD54!{-$zoo7Nqcws1zc@^)grF zd_S~2N4txMfkfM=WXPZqB$ap&@L>?oZ$-tUVBk*t(B%_Rq7bqu<^;LmPmMRNot_{c zlmuylrWk{ikC6?_%>&4MX*{uliL2AOWUJ zI_i!!gZr(tv{R-5-zYP2YZR3Uk;zRi zHEK2n3oOg*s|e0YT7(fvqOC?3Yw{f$@TD-|ixX_5r>DY~vTdht1Pc?zJ`hEmY3fgN zQPlqw+=bU9h{DgrUUy*tqG(t}ZZes+*`tlzTx6hm`%4)8tVXoiEMlN(?QwlmABje^ zMk7t)vdfvcbTOGsZPaZ`A=Sfh2EZvlTgCmjX55uRQUg};Y*F~xZY4zVT_S$CeXwfJ zc1#qGMH>L!sk^tDnSYWiiwG>1UKZj_$QJ`HE=sV1MP*_6KopEyM}6qZ^^6igkt>J@ zZRUf*8uCH~@h~yPg@B0jqllnht3b>QIN8LZn1tu+n@PZvT1Fg_7`{njcom4@f~XkO z`2GFgS#pTzMYcQPm#1~qhpO`YQ2zY z9CBr9UpYK|PCD}^4aZwa!8nZ0l)gW^ zf!J*(YMpsNIt;D+6l(<92&HF=wLw|)V}uBZ397Hh@$b$JPQq*^pdu8Zu&sBS9U;+c zR!vyQgdH00+(<~EwrXU?kNarOxFU@#-DVRZVOmJ-(IB1$rTPV2HEP(aQ5}n_hR^`n zFGZFE6@vkwCO6J5?`f4?R;#C}LtJb3$#y;Ma;NehTu!GAN>ht`%OwD$lz0j;<5vW3 zj?n-Qg=DidiU|mW@Cf|=RaB#t-{A@(?0gq3BqasYSgGPldq$VD7glKK3Fo?aFv)BV!Is+jzh`1Ed(4Hgw z8ZZ43>4yj!9STV-Jsdg@fNZ8%xVju*aA`MEaEM>dzQn`aVUS}s<=XCLAd5@7$-?$4 zmP{0N-yVe5iVTGuiqZLsB{Af?je&fs??n}aoIT~_HAHF+=TosoAJ$RTm@G*2DA_{? z*1NtTZGEHcZfGaWiNPt?9ypcv;CeW1kj)XdrZg`Hd!`haL#^)m3=4BZ0~rDd45Jq7 zsHf3n9Ep9CxH}-8_NX2ucO0ZqJrGqUPlsgxLr(Vsr7*^4FtaVBUSs==Hpo3;+lCQ{f^~`y~VBY586A5LWOKixc6i=codp zJUx*q8#p4@nmIx4qNDZB1E47V&jp z@qk-|PoBe{`ULo`qI2!hJDB5$TQrEt?(hy`x_57KY^$t`P4${L9G0GMrxDXPH0)F^ zZv?PZ^}XCYT+>m^(#N8$VvWqvo#=T_%7_TY-iQoT_|_X==7$J*tKuefciPS1_#I4- z%UIrx5Fs~i%W4R@#e>^F-H$glpW(8bRJU%12uDOZ#-<9StBVU_`u zvaW`OG^6si2Ga3oEXelLNDrLr41@=C^%NlmpaMs)dL+uZ1Oher4N0C6Q&>8$z<*G@cW^ta(Ox=#};O6ZwX1sl2LX8LD>ZhJWV7E6?n8mI8Ny{d>tP= zAyzpeMcCQ7(H+(Gta&sNdcS8|W9A)6>E}Ir8!7$Nb8jQ1^CaFzG>z{EU8djLPa9e+KOT9j)mJnV74-!LTB~E8PIWy(2%#K*^Y0+f8V-Bd|0tc^5KL_hvIkM_cr= zM@W^cS84+GODnN60K&d_y};W5`@hs0`(6Vq5zqe7m4ZwsX@F1&kKK&h{-6a87I>PN zlW8VrxBrK?qg5_#W_+3Q(gwh3g8=$$BImOKpwrd>jgT`d5-csSI3o0L$m_D%tBIeT zFs}!II&Bbmwh27&nA!TDwFXa^-Ml3^>@yNvHhfl%;7%iqz5+11zcof91UG^-`)#*v zBTI*e=ErrFczMOwA%od|-(mzuF+=GId?ITNd5Fy6(`0W>tWM!uK{P+!lf9B}TX_%! z8{hxuaWCTp-{>N*uw3ijJ-Zmp0905k{Jrd%3xYCO;AtWmtq>r0NDIy__Lv{r?RpBg znrq3ZpJMJO_x zznUKgS3j3qg?c|EUQ%8ngoCgqKR5z$qR)lQ`Ijw@#Bae^S>*ApK1>|rFVj@`fxY=2)2;~Dx6ML9cD& zDoP-!H=IEmrDHdz4WilqLR0-dnCf?Rn`#HF;((lTOHH_5puH9a!_bs&=|Ea($D8&J zAX*Lv_VDEzV`l}w4=8#Y37P!PBj^F=&HxDK|CMllGvNGRcEh=!(!5cPaA4g_Tq0k9 zNf?2ib_?th0lgx>xw;Gdo=@}vbmmeEY8S*kaG>is4$ZRqmLn-_tv(6z`&c*m*+P${;{U|T?1a>NMsb^EbKo$c|$UFRhPdsQa;AIZptJd1&5bk#k2m{MtQEB0`vsOFuH zS_RpGD~3PSU%>CZ-B{M|Qy}mL={pF=Yd;cJC@b5ROPrLDiQ;}zTeOl$eXg#DDLve6 zN}ZX*1H+$DQ`nwJWb#dd{iPtI_#4IvyEJa=hIyH3P{%_=>pkwt$))F<#Zx;B^csT& zIcR%fj3UCyGf57&f*d|j7Aqt;HAE#N4{=7$_DYWCLwa)3wUbjqHDaq%dO^K|T>Ujv zStjR9lH1)Nw=YHI)?#2R-6h8{e6cYgvV5$zQO!Ub08vYH8by>tyqF8L{`=tVpBojZ z0+gI#m{)DZ$4gpFrh>f$Sf~Q{Kx9})RXb`1<_1N>K;*jQa@~<9$+bx-Q?0)5F=RMf z_gPeKLdNKLTca%HBHAGA!P9u~r~VQ6{lO^qa+O)qlP}O5C<_{*&Yec-_mo|qk=2Ts z>j5238)PD%#nDmS4pe_@6dj5&a+oQ`DQ-O>+YqZoqEIlLr=vX>$+c6sotH4Ld2GaNuaT27*$Hpn<#L`w8` zL5W^kREZjtZq-ys@_WywsU*5(pM~no(e5oKG(=J#Ao4`As5u*n&vwM0d3%!s6`aA1 zx#TY4-?PfjPpjmeqZ@#bpNP`A$4P@ZZX4$g5+1Z~yVNeORrdv|pW@V#aNAOYZFeIA zks5JIs3!P82#E+Hw|=_Zsoewe^hhKr@1*%@p1f1FsOWB>!GF4)t4<;?Hs7$63l@fw zK@t|^h#BbEnvr(Htbr`BCR$d^D58|Y_mk+hA*FCl4@O|9vZDuO?>ECIpM-vZBy=4} z=-T;6$U{XS$B4b{h11eSln$a&`ZqWUHKj zlcG6eBS4Y@37=w6@M;e9GF*q&3b?G2(^7~&cK>gj-D^v&DFmHGksmRnYM{j&M*51IaCk{@d|03I64S=0bzG|8WL^C z-2t~hwZ$PxNbQO?UCkm`ciJGVi-&?Wr*>M|gU}8JkF!4jsLvy{qgk0E6YJ!UddLep zZ4h`0?soT^#N~nydzI(Nl$38kub}jrro&?MW6J8sD7wE5f{t6tdIb&CIz*o!Bj@%^ z5?u3k%?3G0=Sg@+4d)MCZkj3Z1svkhR38Vx-B}iJ();v@ltuO~AG0GKyA4uiSJVl7f@QW{I+Brn<458^B(14uhoaY?lAQhs- ztb6W?`2wwa{RPVE{2s*m9dA#z2~cvYWLtq|L5;3v41r`vn6DhntA!;mJr2VlxLo?L zE0(-mRDyr-^9+$W&T* znJl5Ye&Tt77g{&H%1X}T9PU5Sb}Sfa{oGhc_E`YChb*eo24U|v2zyrpFTSZ8FA5fv zG$#&>v?wOF53B01%8JlpwU8Y0P)Sk7F3mpeViqlyUvQHzaxTQ(>(v=iE+jiF{W_MG zR92aa1rgF|(ik@#_f(XfEpL7{e4}w^Pl2j^JgRD*>1=?^Du_?p_T~d0?A*bhjxSq^tF8k} z(q+;}L1Ovyvlx|5cnM`0sm4`$=Sg*wu=)Vt_1?ZzeaDGa-k*6k1a8yTVhvM(w}e!e zm|$5bpxfeBjrd)M-LM<{?Tn>fph)!^FMQA*f@WkC+U_!S+MuZae{!9yKMUaLXnsYI zFTo%VNHZ)-b|QFanHx7kAH=x4)T=$IUUSh>Tk9~;lbet7R=z^p`f7NFDE`#{34TA> znmd`Hcj6LhiAMZ`h)4W~64{QD0Xt}3zoEcw>ECIC(|@7Y*n2$$iF&CA7X9;h0k0JW zD-=QOW4tn{z7D?b1Ko&4m{BPuJm8Hj#BrC3*b%(Oa@c}bC>6MU{%2aPaDaY z?G{VWD%|AQCc1-#-U;R`?Zq6;wx-0}hz2dgUgbKR-pWfmoK7Pq>lgzlCM9lg*Ulv+ z!)-?2>!xHjmrFYnQFi^(A3L}d~*KDQKML*A*t z)UcUuS}%eFDfY|dqDYzi#~{VGk{P9lKQ z_T<|f`_-k8$8YgEyJ33?>cwpP%y`w4cQ5%ORj&bS6ZhB^1v7}j0?z~`r`AOHiA{pQ6QFw|^LroNs<349T4))%qLcEB$-$ zl|I@7RJ~plVU!Rn0PLYQPyuaaa z@>3oJKjpq2$lvS15czYqNBvk5{ukbJf~!(+mztkeR#vca$GWEI79TKH|6w=4`UM-~ z>!m~Nd_0!6X-H@9Y%C3#yXxbuymSu6X#|oI8i0#zcyijH^!&HTZ~r`K!d=}o!FH=< z3?ySs!O+V}-J>Fy_pz*yB2*jX!`ufx%st%{!EX{`wsyH9*bEP5Q5h^0_NofCF1V!X zhib@s!Q;f;g31S-Y#Db0AgS3t4_kK97l(UTR&v@PcjLX}Zv1O-H{RWiWgYz%2Yl|v zh}>~A0EZs?8(DM>Aa_EJa&-y#2d|1Em+X!t%5Kjbau}NGO^PD3m-G_WL$|mbJKj3y zH8E0iNrb}4&{tV(Jxp=FB7!%ys{4VA1!D|6Bd>7P_C*_)acZn6{;jSDfE|tktkLE= z0+Es%v|!D!*CV5v-cVZqO)wu%YAvHU_L!{j6bpT%ch*rU*@a-TTR=)whY!p+fY{xy zaBbuqYzJb%TV<;~#7=jD7JaxiLRhR8)}m#ChzQo2Uq4!xd9`9#ySyc&RzoDFZrVi| zx5ig17R`HV&%*1Z!cMvn`9U*aM&-puU>bma+Mqz>xtu3zxL>_Ky$_yPF0eN|X1whT zJG%=JMxm@>u9djQJD*t#!g z9Vz-?pz>nc7qbJ!8tK6v1XR54+a4?(M7!P+k{X+q1WRfEHUO5z#i*WDu>r7|x*H=Q zMqN|}XsDv=7Ne$WS*~mDAb)<|R(&eD3kShnh`$`5Wga!e#dw^&h5;oBDY6UY_S*8N z6BwaI4`m;UH3DsfqQ_!wP=vQvOA!2IYp>Ib73r!==iS1~h$2{?UWa9tA}JsTs`Eq9 zlxSx&pLKw}cTQAAPjyGfzm z0=)dIAc{S&d&8lN&b#u8E2p!W7`&zs+5*gxZLzdZi4CbhLT`>7c9Zq&B9GaIi_Hqv zLXS}mvN@ip^$F(!yWm`b&9DM>g?26#;vGnC3(x@TyR1SR99$^BS-_x*9ME(Gjz`nOifm&;P?~)l z1*VSaaAO6!Qb|=zxI&&w>WocDC8J)GDlwIlEF+$=B=vyTB(CLJg5T6-;kM+ps4Yr4 zWM4>ape|L&I?O~O+jLa$bua0Hqs84~H7%syul!SLMmA@Og`?$_&p6`3Q2|oJd^|h|~?Ip;?w@O5wwW(jZlA zQ4$=fUx(jcYeMmSx@JsZDxq%7HrB->J#dnMQMIVXn0sCts+cC}LYky^!sm7NBuSE# z+d9CjX1KTfGYAVvBW%GGd;_;-`t@eF=M1Gm2>?I>Kq^Ah4BoZ+T&(CKaJ zljD4EyGJzd+Z>3rM-l+?2=_##iK0caH2~9E1WfBPSRfMxBM}2L$ECqsHZIKC4v?#% z9=aQ7tB3ZQB!hZTJ+!QmQx-Klnklo}(~?9^ow};(*C7pRRl15;KY=Ua+KT}`FY+rQ zAw|QD1{`L@bQM$@Li$1{CZrD~SdZE#)0qD(*Xi;;%N@y`iQ+JIw zXPeUWBQb^+$U85TVC5PkM-!kdvB_~AeI`Dw#%vl-gVd <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ From 7bf884b7c525092db74ac2effcf1091bd3c3d46c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 14 Sep 2020 18:23:55 +0200 Subject: [PATCH 5/6] [zarith] [micromega] Bump to 1.10 and remove some hacks In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58 --- .gitlab-ci.yml | 2 +- INSTALL.md | 2 +- azure-pipelines.yml | 2 +- coq.opam | 2 +- coq.opam.docker | 2 +- dev/build/windows/makecoq_mingw.sh | 2 +- dev/ci/docker/bionic_coq/Dockerfile | 6 +++--- plugins/micromega/numCompat.ml | 13 +++++-------- plugins/micromega/numCompat.mli | 7 +++++++ 9 files changed, 21 insertions(+), 17 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cfa6f8414783..22658cc9b825 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-09-07-V22" + CACHEKEY: "bionic_coq-V2020-09-16-V38" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/INSTALL.md b/INSTALL.md index 05a92ca00567..adc0f557accc 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -18,7 +18,7 @@ To compile Coq yourself, you need: - The [num](https://github.com/ocaml/num) library; note that it is included in the OCaml distribution for OCaml versions < 4.06.0 -- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8 +- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.10 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 17228bda8a77..be9e7743811a 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -80,7 +80,7 @@ jobs: opam switch set ocaml-base-compiler.$COMPILER eval $(opam env) opam update - opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1 + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10 opam list displayName: 'Install OCaml dependencies' env: diff --git a/coq.opam b/coq.opam index f44223052dbd..342adee1f470 100644 --- a/coq.opam +++ b/coq.opam @@ -25,7 +25,7 @@ depends: [ "dune" { >= "2.5.0" } "ocamlfind" { build } "num" - "zarith" { >= "1.9.1" } + "zarith" { >= "1.10" } ] build: [ diff --git a/coq.opam.docker b/coq.opam.docker index ac1869f34452..09065fdffdd6 100644 --- a/coq.opam.docker +++ b/coq.opam.docker @@ -24,7 +24,7 @@ depends: [ "ocaml" { >= "4.05.0" } "ocamlfind" { build } "num" - "zarith" { >= "1.9.1" } + "zarith" { >= "1.10" } "conf-findutils" {build} ] diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index cde1d798a00c..fcc585117bbd 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1026,7 +1026,7 @@ function make_num { function make_zarith { make_ocaml - if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then + if build_prep https://github.com/ocaml/Zarith/archive release-1.10 tar.gz 1 zarith-1.10; then logn configure ./configure log1 make log2 make install diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index ee50d2531891..2fcd69e13023 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-07-V22" +# CACHEKEY: "bionic_coq-V2020-09-16-V38" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages, num to be removed once the migration to # micromega is complete, `num` also does not have a version number as # the right version to install varies with the compiler version. -ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ +ENV BASE_OPAM="num zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.11.0" @@ -59,7 +59,7 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa # base+32bit switch, note the zarith hack RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - i386 env CC='gcc -m32' opam install zarith.1.9.1 && \ + i386 env CC='gcc -m32' opam install zarith.1.10 && \ opam install $BASE_OPAM # EDGE switch diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml index 62f05685aa48..8cfda325435a 100644 --- a/plugins/micromega/numCompat.ml +++ b/plugins/micromega/numCompat.ml @@ -31,6 +31,8 @@ module type ZArith = sig end module Z = struct + (* Beware this only works fine in ZArith >= 1.10 due to + https://github.com/ocaml/Zarith/issues/58 *) include Z (* Constants *) @@ -39,13 +41,8 @@ module Z = struct let power_int = Big_int_Z.power_big_int_positive_int let quomod = Big_int_Z.quomod_big_int - (* Workaround https://github.com/ocaml/Zarith/issues/58 , remove - the abs when zarith 1.9.2 is released *) - let gcd x y = Z.abs (Z.gcd x y) - - (* zarith fails with division by zero if x && y == 0 *) - let lcm x y = - if Z.equal x zero && Z.equal y zero then zero else Z.abs (Z.lcm x y) + (* zarith fails with division by zero if x == 0 && y == 0 *) + let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y let ppcm x y = let g = gcd x y in @@ -144,7 +141,7 @@ module Q : QArith with module Z = Z = struct let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint let half = Q.make Z.one Z.two - (* Num round is to the nearest *) + (* We imitate Num's round which is to the nearest *) let round q = floor (Q.add half q) (* XXX: review / improve *) diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli index acc6be6ce0da..fe0a6e766012 100644 --- a/plugins/micromega/numCompat.mli +++ b/plugins/micromega/numCompat.mli @@ -25,8 +25,15 @@ module type ZArith = sig val power_int : t -> int -> t val quomod : t -> t -> t * t val ppcm : t -> t -> t + + (** [gcd x y] Greatest Common Divisor. Must always return a + positive number *) val gcd : t -> t -> t + + (** [lcm x y] Least Common Multiplier. Must always return a + positive number *) val lcm : t -> t -> t + val to_string : t -> string end From acb24a1540c33f075a83f9788614e5c2f3335b0a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 14 Sep 2020 18:26:21 +0200 Subject: [PATCH 6/6] [micromega] Use `minus_one` built-in zarith constant. --- plugins/micromega/certificate.ml | 4 ++-- plugins/micromega/mfourier.ml | 2 +- plugins/micromega/numCompat.ml | 3 +-- plugins/micromega/numCompat.mli | 4 +++- plugins/micromega/polynomial.ml | 6 +++--- plugins/micromega/simplex.ml | 9 +++++---- plugins/micromega/sos.ml | 8 ++++---- plugins/micromega/vect.ml | 4 ++-- 8 files changed, 21 insertions(+), 19 deletions(-) diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 148c1772bf6f..9008691bcaba 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -354,7 +354,7 @@ let is_linear_for v pc = *) let is_linear_substitution sys ((p, o), prf) = - let pred v = v =/ Q.one || v =/ Q.neg_one in + let pred v = v =/ Q.one || v =/ Q.minus_one in match o with | Eq -> ( match @@ -761,7 +761,7 @@ let reduce_unary psys = let is_unary_equation (cstr, prf) = if cstr.op == Eq then Vect.find - (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None) + (fun v n -> if n =/ Q.one || n =/ Q.minus_one then Some v else None) cstr.coeffs else None in diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 1c0ddd502a68..f4d17b89407e 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -570,7 +570,7 @@ module Fourier = struct (* We add a dummy (fresh) variable for vector *) let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = - {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero} + {coeffs = Vect.set fresh Q.minus_one vect; op = Eq; cst = Q.zero} in match solve fresh choose_equality_var choose_variable (cstr :: l) with | Inr prf -> None (* This is an unsatisfiability proof *) diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml index 8cfda325435a..02c4bab49794 100644 --- a/plugins/micromega/numCompat.ml +++ b/plugins/micromega/numCompat.ml @@ -61,7 +61,7 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + val minus_one : t module Notations : sig val ( // ) : t -> t -> t @@ -120,7 +120,6 @@ module Q : QArith with module Z = Z = struct let two = Q.(of_int 2) let ten = Q.(of_int 10) - let neg_one = Q.(neg one) module Notations = struct let ( // ) = Q.div diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli index fe0a6e766012..0b4d52708f02 100644 --- a/plugins/micromega/numCompat.mli +++ b/plugins/micromega/numCompat.mli @@ -47,7 +47,9 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + + (** -1 constant *) + val minus_one : t module Notations : sig val ( // ) : t -> t -> t diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index afef41d67e2c..5c0aa9ef0db2 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -156,7 +156,7 @@ let pp_mon o (m, i) = if Monomial.is_const m then if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i) else if Q.one =/ i then Monomial.pp o m - else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m + else if Q.minus_one =/ i then Printf.fprintf o "-%a" Monomial.pp m else if Q.zero =/ i then () else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m @@ -912,7 +912,7 @@ module WithProof = struct else match o with | Eq -> - Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) + Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) | Gt -> failwith "cutting_plane ignore strict constraints" | Ge -> (* This is a non-trivial common divisor *) @@ -999,7 +999,7 @@ module WithProof = struct | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p) let is_substitution strict ((p, o), prf) = - let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in + let pred v = if strict then v =/ Q.one || v =/ Q.minus_one else true in match o with Eq -> LinPoly.search_linear pred p | _ -> None let subst1 sys0 = diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index eaa26ded62d7..f59d65085a3d 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -247,8 +247,8 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t = let a = Vect.get c e in if a =/ Q.zero then failwith "Cannot solve column" else - let a' = Q.neg_one // a in - Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e)) + let a' = Q.minus_one // a in + Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e)) (** [pivot_row r c e] @param c is such that c = e @@ -364,7 +364,8 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t) if n >=/ Q.zero then Sat (t', None) else let v' = safe_find "push_real" nw t' in - Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) ) + Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v'))) + ) (** One complication is that equalities needs some pre-processing. *) @@ -399,7 +400,7 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) = elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc) | Eq -> let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in - let v2 = Vect.mul Q.neg_one v1 in + let v2 = Vect.mul Q.minus_one v1 in let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc) | Gt -> raise Strict ) diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 03d2a2d23392..aeb9d145554f 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -576,7 +576,7 @@ let eliminate_all_equations one = else let v = choose_variable eq in let a = apply eq v in - let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in + let eq' = equation_cmul (Q.minus_one // a) (undefine v eq) in let elim e = let b = tryapplyd e v Q.zero in if b =/ Q.zero then e @@ -814,7 +814,7 @@ let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero) let bmatrix_cmul c bm = if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm -let bmatrix_neg = bmatrix_cmul Q.neg_one +let bmatrix_neg = bmatrix_cmul Q.minus_one (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) @@ -943,7 +943,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = List.fold_right (fun k -> List.nth pvs (k - 1) |-> element vec k) (1 -- dim vec) - ((0, 0, 0) |=> Q.neg_one) + ((0, 0, 0) |=> Q.minus_one) in let finalassigs = foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig @@ -1166,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol = match cls with | [] -> raise Sanity | [h] -> acc - | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc + | h :: t -> List.map (fun k -> (k |-> Q.minus_one) (h |=> Q.one)) t @ acc in List.fold_right mk_eq eqvcls [] in diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 3e0b1f2cd969..4df32f2ba48a 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -52,7 +52,7 @@ let pp_var_num pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "-%a" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v @@ -60,7 +60,7 @@ let pp_var_num_smt pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v