From bb90cc2be47fa37700e9e3a227e895a0ec3d9a22 Mon Sep 17 00:00:00 2001
From: Hassan Hijazi <hlh@lanl.gov>
Date: Wed, 29 Nov 2023 09:52:23 -0700
Subject: [PATCH] adding fault location data files

---
 .../VNN/CNN_fault_location_constraint.vnnlib  | 348 ++++++++++++++++++
 data_sets/VNN/Fault_location_CNN.onnx         | Bin 0 -> 11700 bytes
 2 files changed, 348 insertions(+)
 create mode 100644 data_sets/VNN/CNN_fault_location_constraint.vnnlib
 create mode 100644 data_sets/VNN/Fault_location_CNN.onnx

diff --git a/data_sets/VNN/CNN_fault_location_constraint.vnnlib b/data_sets/VNN/CNN_fault_location_constraint.vnnlib
new file mode 100644
index 00000000..d4b43f8f
--- /dev/null
+++ b/data_sets/VNN/CNN_fault_location_constraint.vnnlib
@@ -0,0 +1,348 @@
+; Constrain the inputs with physical ranges:
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const X_4 Real)
+(declare-const X_5 Real)
+(declare-const X_6 Real)
+(declare-const X_7 Real)
+(declare-const X_8 Real)
+(declare-const X_9 Real)
+(declare-const X_10 Real)
+(declare-const X_11 Real)
+(declare-const X_12 Real)
+(declare-const X_13 Real)
+(declare-const X_14 Real)
+(declare-const X_15 Real)
+(declare-const X_16 Real)
+(declare-const X_17 Real)
+(declare-const X_18 Real)
+(declare-const X_19 Real)
+(declare-const X_20 Real)
+(declare-const X_21 Real)
+(declare-const X_22 Real)
+(declare-const X_23 Real)
+(declare-const X_24 Real)
+(declare-const X_25 Real)
+(declare-const X_26 Real)
+(declare-const X_27 Real)
+(declare-const X_28 Real)
+(declare-const X_29 Real)
+(declare-const X_30 Real)
+(declare-const X_31 Real)
+(declare-const X_32 Real)
+(declare-const X_33 Real)
+(declare-const X_34 Real)
+(declare-const X_35 Real)
+(declare-const X_36 Real)
+(declare-const X_37 Real)
+(declare-const X_38 Real)
+(declare-const X_39 Real)
+(declare-const X_40 Real)
+(declare-const X_41 Real)
+(declare-const X_42 Real)
+(declare-const X_43 Real)
+(declare-const X_44 Real)
+(declare-const X_45 Real)
+(declare-const X_46 Real)
+(declare-const X_47 Real)
+(declare-const X_48 Real)
+(declare-const X_49 Real)
+(declare-const X_50 Real)
+(declare-const X_51 Real)
+(declare-const X_52 Real)
+(declare-const X_53 Real)
+(declare-const X_54 Real)
+(declare-const X_55 Real)
+(declare-const X_56 Real)
+(declare-const X_57 Real)
+(declare-const X_58 Real)
+(declare-const X_59 Real)
+(declare-const X_60 Real)
+(declare-const X_61 Real)
+(declare-const X_62 Real)
+(declare-const X_63 Real)
+(declare-const X_64 Real)
+(declare-const X_65 Real)
+(declare-const X_66 Real)
+(declare-const X_67 Real)
+(declare-const X_68 Real)
+(declare-const X_69 Real)
+(declare-const X_70 Real)
+(declare-const X_71 Real)
+(declare-const X_72 Real)
+(declare-const X_73 Real)
+(declare-const X_74 Real)
+(declare-const X_75 Real)
+(declare-const X_76 Real)
+(declare-const X_77 Real)
+(declare-const X_78 Real)
+(declare-const X_79 Real)
+(declare-const X_80 Real)
+(declare-const X_81 Real)
+(declare-const X_82 Real)
+(declare-const X_83 Real)
+(declare-const X_84 Real)
+(declare-const X_85 Real)
+(declare-const X_86 Real)
+(declare-const X_87 Real)
+(declare-const X_88 Real)
+(declare-const X_89 Real)
+(declare-const X_90 Real)
+(declare-const X_91 Real)
+(declare-const X_92 Real)
+(declare-const X_93 Real)
+(declare-const X_94 Real)
+(declare-const X_95 Real)
+(declare-const X_96 Real)
+(declare-const X_97 Real)
+(declare-const X_98 Real)
+(declare-const X_99 Real)
+(declare-const X_100 Real)
+(declare-const X_101 Real)
+(declare-const X_102 Real)
+(declare-const X_103 Real)
+(declare-const X_104 Real)
+(declare-const X_105 Real)
+(declare-const X_106 Real)
+(declare-const X_107 Real)
+(declare-const X_108 Real)
+(declare-const X_109 Real)
+(declare-const X_110 Real)
+(declare-const X_111 Real)
+(declare-const X_112 Real)
+(declare-const X_113 Real)
+(declare-const X_114 Real)
+(declare-const X_115 Real)
+(declare-const X_116 Real)
+(declare-const X_117 Real)
+(declare-const X_118 Real)
+(declare-const X_119 Real)
+(declare-const X_120 Real)
+(declare-const X_121 Real)
+(declare-const X_122 Real)
+(declare-const X_123 Real)
+(declare-const X_124 Real)
+(declare-const X_125 Real)
+(declare-const X_126 Real)
+(declare-const X_127 Real)
+(declare-const X_128 Real)
+(declare-const X_129 Real)
+(declare-const X_130 Real)
+(declare-const X_131 Real)
+(declare-const X_132 Real)
+(declare-const X_133 Real)
+(declare-const X_134 Real)
+(declare-const X_135 Real)
+(declare-const X_136 Real)
+ 
+
+; Input constraints:
+(assert (<= X_0 0.019471729855110205))
+(assert (>= X_0 -0.013259788521870939))
+
+(assert (<= X_1 1.7193392029388745e-05))
+(assert (>= X_1 -0.01232866098185262))
+
+(assert (<= X_2 0.01862093610654811))
+(assert (>= X_2 -0.015387829791690835))
+
+(assert (<= X_3 0.008985257367865129))
+(assert (>= X_3 -0.019716454188820547))
+
+(assert (<= X_4 5.179202988486953e-05))
+(assert (>= X_4 -0.01190505334804328))
+
+(assert (<= X_5 5.309888505767635e-05))
+(assert (>= X_5 -0.011997879497362425))
+
+(assert (<= X_6 0.014507924296705546))
+(assert (>= X_6 -0.019951574704339094))
+
+(assert (<= X_7 0.016842795060237937))
+(assert (>= X_7 -0.01986580102324414))
+
+(assert (<= X_8 0.0165905336927278))
+(assert (>= X_8 -0.016353611894374794))
+
+(assert (<= X_9 3.6902374506604385e-05))
+(assert (>= X_9 -0.011699265370822116))
+
+(assert (<= X_10 4.191474770990134e-05))
+(assert (>= X_10 -0.011777394164622462))
+
+(assert (<= X_11 0.013964283205810979))
+(assert (>= X_11 -0.006841450776507908))
+
+(assert (<= X_12 3.1952773777879087e-05))
+(assert (>= X_12 -0.011810859359965351))
+
+(assert (<= X_13 2.0122995744473737e-05))
+(assert (>= X_13 -0.011880362829054985))
+
+(assert (<= X_14 0.019739942320733922))
+(assert (>= X_14 -0.016858379496340403))
+
+(assert (<= X_15 0.01972324964434205))
+(assert (>= X_15 -0.01517971246287141))
+
+(assert (<= X_16 1.8059037460442796e-05))
+(assert (>= X_16 -0.012919949064292367))
+
+(assert (<= X_17 0.0028541198156783777))
+(assert (>= X_17 -0.019964954022466036))
+
+(assert (<= X_18 3.861957380602021e-05))
+(assert (>= X_18 -0.011992557779762596))
+
+(assert (<= X_19 0.013553930294714508))
+(assert (>= X_19 -0.019992962826684092))
+
+(assert (<= X_20 0.01985519469335577))
+(assert (>= X_20 -0.019896538721798827))
+
+(assert (<= X_21 4.1353367000040996e-05))
+(assert (>= X_21 -0.01179306918367756))
+
+(assert (<= X_22 0.009400380037530173))
+(assert (>= X_22 -0.019602707105324295))
+
+(assert (<= X_23 0.013245332382963862))
+(assert (>= X_23 -0.014808504905970507))
+
+(assert (<= X_24 0.019811971180332986))
+(assert (>= X_24 -0.01978824238664879))
+
+(assert (<= X_25 0.019525315637710216))
+(assert (>= X_25 -0.019980474321790582))
+
+(assert (<= X_26 0.015605703654867251))
+(assert (>= X_26 -0.014318896745016154))
+
+(assert (<= X_27 0.014741133813770185))
+(assert (>= X_27 -0.01938675498457766))
+
+(assert (<= X_28 0.018867736384064623))
+(assert (>= X_28 -0.013355051857696207))
+
+(assert (<= X_29 2.650939680959308e-06))
+(assert (>= X_29 -0.012165432000410417))
+
+(assert (<= X_30 9.523597304068599e-06))
+(assert (>= X_30 -0.011975853792718481))
+
+(assert (<= X_31 1.0603461995994934e-05))
+(assert (>= X_31 -0.011456488249391024))
+
+(assert (<= X_32 0.016190436381284704))
+(assert (>= X_32 -0.018178448000944272))
+
+(assert (<= X_33 9.392153894505207e-07))
+(assert (>= X_33 -0.011795969523278146))
+
+(assert (<= X_34 2.406536602972409e-06))
+(assert (>= X_34 -0.011062059600756863))
+
+(assert (<= X_35 0.0022881931557924683))
+(assert (>= X_35 -0.019554602518687954))
+
+(assert (<= X_36 0.0))
+(assert (>= X_36 -0.019990573955940952))
+
+(assert (<= X_37 1.5617256102515852e-05))
+(assert (>= X_37 -0.011962623741101543))
+
+(assert (<= X_38 0.0))
+(assert (>= X_38 -0.01998303566950465))
+
+(assert (<= X_39 0.01833375092271396))
+(assert (>= X_39 -0.016339364685661883))
+
+(assert (<= X_40 0.01743908697530324))
+(assert (>= X_40 -0.007082846783812081))
+
+(assert (<= X_41 0.01816156335328304))
+(assert (>= X_41 -0.007035799337502533))
+
+(assert (<= X_42 -2.030072394806792e-05))
+(assert (>= X_42 -0.010911947713223928))
+
+(assert (<= X_43 0.0))
+(assert (>= X_43 -0.019992434034478982))
+
+(assert (<= X_44 0.01168352757031344))
+(assert (>= X_44 -0.019949079873977708))
+
+(assert (<= X_45 0.019562173493219936))
+(assert (>= X_45 -0.019419417077057532))
+
+(assert (<= X_46 0.01817587761730011))
+(assert (>= X_46 -0.019896206926303173))
+
+(assert (<= X_47 0.011511811546516598))
+(assert (>= X_47 -0.019938873085811663))
+
+(assert (<= X_48 0.013771178768402422))
+(assert (>= X_48 -0.01997067428237051))
+
+(assert (<= X_49 0.013669465917711872))
+(assert (>= X_49 -0.012780718310042145))
+
+(assert (<= X_50 0.017905746991896156))
+(assert (>= X_50 -0.018476180082104613))
+
+(assert (<= X_51 0.01989696087500432))
+(assert (>= X_51 -0.01915263159148206))
+
+(assert (<= X_52 0.0013535181734928958))
+(assert (>= X_52 -0.019955072810957996))
+
+(assert (<= X_53 0.004845028404834594))
+(assert (>= X_53 -0.017969243059148612))
+
+(assert (<= X_54 0.00414514082908445))
+(assert (>= X_54 -0.01998222680564328))
+
+(assert (<= X_55 0.0024869826698420807))
+(assert (>= X_55 -0.019110877447823915))
+
+(assert (<= X_56 0.0016675298540827477))
+(assert (>= X_56 -0.017148133544183847))
+
+(assert (<= X_57 0.0026165234973105833))
+(assert (>= X_57 -0.01817261026798122))
+
+(assert (<= X_58 0.0021859511787613696))
+(assert (>= X_58 -0.019304504596847613))
+
+(assert (<= X_59 0.0026043110115784285))
+(assert (>= X_59 -0.017348765506662606))
+
+(assert (<= X_60 0.0023647445944186287))
+(assert (>= X_60 -0.017855494052061653))
+
+(assert (<= X_61 0.00702399329790538))
+(assert (>= X_61 -0.01973466613782819))
+
+(assert (<= X_62 0.01747802953576991))
+(assert (>= X_62 -0.019981697734435328))
+
+(assert (<= X_63 0.01991301604740603))
+(assert (>= X_63 -0.016271185986760896))
+
+(assert (<= X_64 0.01999895108326845))
+(assert (>= X_64 -0.01794481808768253))
+
+(assert (<= X_65 0.005030467036323961))
+(assert (>= X_65 -0.018671367210649558))
+
+(assert (<= X_66 0.002703210637842175))
+(assert (>= X_66 -0.017472523255268938))
+
+(assert (<= X_67 0.01957973840914861))
+(assert (>= X_67 -0.019193316579627237))
+
+(assert (<= X_68 0.00972036328288359))
+(assert (>= X_68 -0.016157211870936553))
+
diff --git a/data_sets/VNN/Fault_location_CNN.onnx b/data_sets/VNN/Fault_location_CNN.onnx
new file mode 100644
index 0000000000000000000000000000000000000000..2dccd9f2cacc6dac3d5d4df5d1ba90fb043ebc64
GIT binary patch
literal 11700
zcmc(F2|ShC*T30uWDKb!kqpT^mS^vSifGV8lSGKjL#5k@jAcxPA|gq2)1)}hT8C(o
z21SV`jZ~Tkjeqyo{oUK`cl*Eh{eM31|2^k(&e?md@3Zz=>-p~etY@ExBd#bJwlXR-
zVzK`aaZ^JRL*udA=W{O#bHxKf!j?sGWkN$jqQ{PP2n|{8X<_x(uC?MQqs1X1o<UwK
zeIp{jYZ@9G{p*0xWl{Y$JdKA8`%d{?^LL!4*l%ckMXr=jK#*5dKxjxLPnaiMC@iTz
zfGfTvB6L}pYJX2eUzs}~&^IE)H^?*6-z&_QC;knjz!eMg@`>aLeS80QoIF=DGAbg#
z$M@fsxXZZz(Al2`Wok6TH)xsXe;L#_oTk`sXzn@TpN{*3Jw?6mGV@*2(9CFxSF~$r
zXwaWSYka5wuK6caQ}Xv?`ZFQ5*f$`^GdR@8S5@fmvMBOTviJ?eeJ#xW=WhOmEtbZA
z?V9{F&*uM-Jl}Bt%jEgN*`Eew`47qS4fkJ@=LdT~C6CoVC(j?y{{`~=G4>xE|0`R}
z{@OMFX`ZeBA$h*x{-4Ps`cLM}w>6Br;-@RX56&v;d^eZBYZ{su|G*yg@3h}F{|)?|
zJ{N?!|J0(Q{&!}+YZ{uE{3n4%d<Xch`5pFuib3y$x&IAE|H>K5zjm#Do^8_~IP}wO
ze*^x1AyM?tPvsBp{yZ-8f6Ah7z<<D^A1wZyMHc@J7X5+!pJLJEpOfg1vHw_y6y=O&
z{#I=KAs8a@O`s|MFFDsiQSmpvL`HdqMEwbp`a`D4`L|YIl`Fp7D`=Uo{s4JNXO7VC
zuR>ul?riRl!*Kt`s-nD+qgRx_Z^WPDNd7L-l=!C6m*$FjMF&Lw>r&5k;r_=FiUW;i
zheU=i^Y#7ZyO_9t3N@wv(0?=5UqkiR4U*hRib{V3<!SP#3)0_7zYBKAzk`+K2>%xD
z*WX{ig*%`7cV2M+)_#A`{Rv#`^<8o$f0t-VeAE0jXrKSi>FrO@57reG`lrdi>dQYv
z<osKtDfzpOTO!Q;Pasz%C?LewE8_Q(*wEN;g>S$T|0u4~k8<w-uSi9SZ?)tQEu+7v
z|Jv&>k{x}6gEhr|`_`A^ihBix`Fkk~39YAv!ovEpTrqFos6YEMT#2X%uaHRlf0fLN
z++eSO5YHtMUSa<FcSdvEIr8$t_CN8`Suncw-67ItV_^GnQ#cM6eUEjE)$u|>2Hx|X
zAm9k;337(=pd~X2r<`=ACf6;ght_jupx#rm%pw(Q?hg{2KO}}m%ePV0$LnadTs_gf
zYKeM^T38TSO|DI7!kMEc;Z4&p?6ljCJn=>{(6);3E)jgGY>s=5PG_}0Ps4qMg+yVC
z1xojQBo}<u=ydB~9P-MPHfAT`ptra2i&QN#>@iT#)PcP^0vusE0)1#L(#BQv@VRU3
zCM6-1t(ghsei`sGMv+!-T8nq=Hj&Q6BN!M1<Lb;gf{ydIAnOFd*|K$X`m#A_;rJRw
z+JzXd-6~9St3aVmQ8Z-eD!kegXFKS96YNi`0QS;oIPg}8&elIoo?g|!(d*8zd#A2u
zV(+&D`{)Rs;&u?vs=aun(1}eEPoUFsGVwx>BRO9%0zc)afyMb8yd5Nr+BceT`nzS&
zQ)xi@ZjYh)t&aHWgDj3xX(oHxPSaaM{D8_Nk}Y3c`KH@%F!MD`alM{3-W?i>Uo={<
z(m+nobLSLJ&Xz}R%mi9B(iqp)$-$8fd4?nWmQ?Q6$4{Cs&?DwNq}9694Q+)O6L5@~
zejpqZ3crxJWR76l3SU&I*okAp(`YkO3!mpFvi5g4xYEUl+9*{*aN95R`Hs)5NSBIW
zQOy~M%RUDux+d2yA2~;`>UuTKY_A8wYgg!gi)3AT346I+jb44WjpQ{Sqr+tu!i19X
zaO<%XtWTB_=$?27qE)W6Fk~K%e>Pa4TgDMw%8R4j?mf80>@KnJYbBATi_y!Rpxq-a
zf!?&&;~H@ZeNj`+j>~SrvhnHYaI&0~ZFk2fbzFh{n$y@6Iuh$%_c8O{D$usu+0c6~
zo4zm<CgulbBANA-b>4WG<Y>#1<fBWm<6;4d=RIIwTGX*sG4f>RgGyAKp(MEbDuB#Z
z8c1g4odbuBhpFGF1xyYW;r_27kjza3<I7&`yrnI8N^byi=rqd8uf?mEr=n537CyXm
z4O?A8*(|GZlnvFxYUMWCyyF&|&{cu!G-NPsv;*bs-bC0hEbdcJLLCKv8r8QJ@48;b
z$`Vst;#fdB8U|zVhpqJeXM40-k;g1-Tm_l(8mPZ|B*r>zgObc@5NkOMv&=JL+xE9?
z{FXRKyFL}P>j!|nt2L@#6UHvvdN^UUAL@r^Lh*qtXgzY1^;mxl?r!VCPl8=+TFnaB
z+_@I>_r7PlEeByBuA|MqVgl`9hJtji1eGgJATb)T7<eY0(&f6KP$mzzO6?F#Ofk99
zpU&X%87EkdkE6;+ZqNm+rXCo(UJgxFMhiS{7SThx^7K&oHtg6WM5ToF>DJTzwuDE*
zaW4tMXd4B}7<w@C9@OK_>N!-$?=l{qPU%->1B#xm2E$G#`byaVeZS_Q%&!KhOHAm_
z74m|7el+v;SQm(Va3S1`t(b4K5pFreQEvT0j4tv6XW4X|;e^Ea>MqFb%BP3&Jz>vS
zMSS1T23fVjf}%S&nS_|(0{{FP2;ItHhSMTuqMAEh9^C>r0-lkzdOLBInl?SPZaOxK
z+EV^bPts8Gj_I@I;k)s&xYGCujH<AK5Z#54SkVbwzf^d(!4wWhD?p^@5YSB0g`^#p
zxFyjD*IqpbpYlp!!TwU%q;Uc2=NJ;+VlHOYZzN6=2ax5WZ3xp-K<<zk9X@P5P98g)
ze(};}pDC#0yDDF}ZIeUOx-IY^FCB|+wSe!Yp(qmc0$TN6VU9vNp7U!&t+nao{?<fF
zBT`|^vTgKus5$oDv13QZ%HoVUw)9x`dZyjFg5CQl6N@E^NmD{LDog0&G|TnabTS7&
zyK<=PC_<T+3t;J#Vq3wR7F4$@qg@4k_-SV<dq>iqRvMc!n6eqiG-XpCBSXQhlcMyR
zTL+4{RABf(d1}6NB;Ggt1>^m;U~~0Iyc%Ccp;%ZD(mE1fc=j?ini=FtZxPW{Riy)<
z8@n$(B{lQ&u~Ni|h#T&K5LI!^+-%C|JdDAew@<M%vS-r8K~xYre>#cyoCUA4_5*+A
zT5`lToHh*97pTvc!N<BgQLTkb+isY!9a1*5^VM!LBcT!WC*Q|6rfsCtdywG%t67+I
zM~ysBPo;uQhWLSw#u-67F;Y^5*0p<}NJ<@D9y$-_xaVTVj^pf&U{`W2@;2s{*fNra
ze0=<wkJZ>t5`{-ngT1O~IkX<R&(l$mI-2^wnUAG$J|x#XAH5Qe;)|;Z%pQANR{r2B
z=((yx-PYg2;mLZKdEf~%+g_BUxIHD~m}<yfy8vy4W>QhR1-SG=I@#h`1yg3Ogao%S
zq@heqpj@a<<MV`RWTS@Qin<9lNv+_^Ufzwo*Igv(?Lm?mYKEhCFT^Xqy5O>TYY1;k
zH}lpbn5a%DgO@V;G$HX6dbXwY&woUYVGkLk5lLox=TUUi6kKf3ryl~ZF?-YqIdx<L
z*2#P(1Ea4K(Ym$l(Y7(roLxmu9kW56MLoK0J&!KsL-5x0=|pRl8r}Y}4{5bB+Ierp
zo&M9QAfpd2t0lvQHy&uw5siVI=~U{B7`^ZL4&{!;fTWW-N|-iM-m2Af=(1*DJJbd5
z3O~TR$NlTl!?J!Z`$JQ9Axw_W1UL8Rtb@crxbk{ER5pEKMfLP>0?!zQb3VfO(+45t
z^h$XCyb46~-UDZrBp$e&2dZ*;P|eSW^SvwK*cE9Q>~x;(`y~LJI<?{Mnqg?qj71NT
zHqdl$felCEVdCXoU_VD&;3&;tu+#*aGCBthRlPB^AOR&`Zor+n_H@dIh4f``6x!9E
zCsu=1@YhpK*kL-2?oXlA`l%jTFBKKAp6WRIXe@dw<>LDA6L``<o9KIF<M#KO^l-!u
zYP(&Fo|8IFJTA<^Cbonm`%I!qmnVWWPZ&Rnjlh)!Z4k0?7s%FL1gYvucxGS*K4)v$
z&a`Q8K~fbIo+trVeIP0?(Lpz96<i>89g-IAg?Rhzu&zB67nx1Pu<&{^b7}?--n0q5
zN+vVP4N3SkNgpmWSrLun1$0d86msx<17<HFRB}))abB(};M`DT^yWxmo|6hLmyU(4
zvc+J<%LA2-8z8?(2khMj!kf+*SRvyAS-0dc_pt@`@=9TQ>Q^wMg<#u%9sRsz4{<-Q
zhib!RaA|ov>DAdtbAks5DnA^7jHpDipO~^Qdh3u{>63_#LOh<ELb@KUVso_bW1{DN
zu&Nfq<m<9%XzK|ZWzu0^eGOzc2Ev1-j$o$J$iC8;2fp@i*|7SNXx3|v7c;Jd(ya?%
z<r@VnH5Wsf{Qx>#E1s0cX2O?G`-!}YB5i6<!re*XsB)->Nn2+|?|$fn_oZPN<G2b-
z<PU&cKr^w92*f&(131mrpB~;Uj#f&cly4RfAvU*|Jxy1^ET#-vU53;31$MR{3pT)-
z)?-L7zktZj&8YI$gq|(^6?@|pu*dxz!GjfOt|<c73S%**PL_tt1mm-X5*RPVp~3a-
zwQV~#z_P(jAhf`nb#awOp}f6h=SUNrl(CT5+*n7tk2az$tR=N#-N;iPNq+GejVtWk
zarjy_I{85*xz37E<(D&Xt+NmfcxEp6vSA`!x}ygJEym;H<PT6kOAKRI1c3a-SUBW*
z05;xR44hMjP^Z<!nr2OgAst#Ut4jwj{yGMACyL@JX@H6ab705SOxQp8BV^21!eQ%@
zq0_4fyrs5)qvHlBvK|aI@uL6=V<Es<0vw+Y#j)#*@nMKO+W)c{UcVm$ZO=;Jh4Xc0
z(%B^#7Zi>5ic-|^wj#Z7b2+N(A0agX<@nmdjfQs#(U`A_ST#A2UT;NMyEzQ^9llIh
z1xZ0FR|>UV<Z#|yPZ)AO4^FN*2}P$C!;%_1Xfn`&)&mjHSg8xkQ*|*!+8iav?T1^7
zH^IV9sc>#<ImA9}gBlIVal1Oi$(E1$@S%McJz0=WYU4~mqC^1=N@ZzKfC5e|+X}i#
zN67KT1(@NcjHxLPn3VUUf%m2kQQv{QJtIlCZBE2CWfhv!{SYNHmC^D+GQQw_A_>&1
zwr|97+*6xF$2H}FHra&DA56&Bf;5PlX@?(sPLZ57ij>>&3$7MwCaz1WkrCd3TkS_O
z`UgxfuKp%G_4LHJmFtLSt)xJ|a4#6{RYH&U<@Btz9a<jV4pY0A(2$xcTy#bVhEy%W
zn#Ydlm1~BBN)NDE@i~;rZo`xwX?o$PuHaSU7UI;HOAb|>hJei@$&QBMf=eaONxXYH
z9iaA*%!;i+;dX$p^<Qx5L=hZ#b^{emFU5c_x^%2yltAQ{o8;oK2aKNcZj{|;f!gcZ
z;Dg*LJhLa9TsWspO|*qE@k9j?9e)SoxH@>Y=nT~N*N$J7Nl}M<S%H<!RN6gkCAO{i
zr6{3-WuH44&B1Bp`mKG`;O1wd^ezd#od!`|FKK~F&sw~)FC3qZr}%tk7V(w7h_;RA
z$%LGdR9E*BMtRE8G3{D3B1jjdwp)?Zi$$!>>I@=kKA6r5NWl*0TwKv$4W>KOFzD$}
z%zajfTC>&Z7~@d<%vE4I^OX5Fvi6{ze-7?2KWV$*swt|wFQOxiYDw||A<Wv>4gMO(
z$qc>gESn(<QwEiyd2~6QQe?@L-x!0(Kg$b>mZV^b3WvUHk*Ayk6X~N6SsEN-j}@5#
z_)_TzPCk-K;yW6_=FM)BUs#PVrp%#lU;5yr`pvAQ>mC$s+KfIIj4^+(9bOv}HZJP=
zaw-s82MuvNnzTWbgv)R-Eg%3a9`rJ%)#Fencp}vl7ePhODk4@Lj}K17qFA~jrVd$8
zJFLg!j%$AOxu*|CACo7Y$~~~}L@>^9bi>Wj%c<6$EqLJ8P;9O5f)%rE=w9DX%y9Dr
z`ts2YnEZJcx%ct{Gc&*)M{B(%M<YXVFC<`%k_Bj$@57{{`6!g&f(OnvpkRbL`gAJL
zp;OYq+hYU0d?*`3q-K-m#v5pU`y+(U`f5A6$q-L2a3PJmG-;soTJYMFgsX!J@c!eC
z811(m+|$R?g)QP3S;WDa`XMmEpcodL?Svg=K5%#7V|L4NvHrDWHgFBaAg5RZKb$bb
zdRrN6Z94+_#2wm~Z-AUzo;aevb_^^axJJ~28qJ@HtM|?z?^ai#@#;-rS9y=MtDiwX
zr>$nvo`?!Ao?Hs=H|w(__KJ~+X=2p%p#Y^?VyOM+J8bRXBX}<=fVGl2h5^1Gu(Mo|
zirs4f?xD|2(=a9KD3T3<PmS?*(`}4z6-S>H^XNt6E$m@`VYt3<18JPJ5acdsQu*i@
zx^z<knw2yVgUNSUy|<QRsY@>LNYTfbIh8nL<8d71u#weX=?aCb^q|&2nkE(IW2AHr
z8F985{Z!}EK<jt7Y~x_+cWa0B+*iKz)wp9MP~H)HdjhZyWCdkR46G3j#TU8VWX0eH
zcABS@;K6=5tZv@J*ibcmbh-i_oerYm1s!~)^2cn6{VihkL=o$XqG8MA4zzOW05uIu
zD$7-%dSR<@(%@KJCU=EAnEetwO*QC?(c>^*I-bVpCK2A8X>>)U7;$?Zij@zzg1K*l
zus&H4Rtv{rL6HGnlUIT({WS%x+g<52-d$*M6BRU-D&xn9L}F|r&-PSU(0$uVz+CYz
zaUC6wUK!Qolt&ys>fObZKamv}c&gFXZN7Lr$pw9Kgapgy1i~nvb?E3|OdrUp6aV6g
zB<$=blKW*iRnQhk^YRrSe`FZ)xKn7}kV<H@bEByRBJ|v+56Ipbig(hI>FcHGxbl!O
zJrQh*nZ+W4%Yg$?GX5zslC;2uFAbsG!5E?=i;-lW!H|3o4T%aw&iRYXKF!0pyULN+
zzBqvI^V4allmUzD-5~9}JQ*mpj@ndkQDsUwhPYFl5x5dVMx<eZ^h792^&`2W*>ua3
z>BL>9m>zJSk7Y;3<G@n_JhZBmxSSNlL6?l_z^+KzIsYqus<;QmGu!a(6N0)MkJDEx
z`dB~FUMwGIB<LQ^<(X}7z`;9}1lOFa*bn8~(YG@ZQZEHlgLl%{XC6!5In=@PECw}N
zx009FUPIg6R$OxR8mt)d1uOh|$%>R7<X^ABQ_gCFmJ<Rxyf~AjOd3UnOV5Jq%7av{
zR*06pA1i>EJX*86i`e>2z`^ea(dtv_I7CW~@+Bk%t0MQo)m~>*5*|-X_dbEiYm(3d
zO>o$#J~B4Xk`51D$|_j3K#=%g%-eYs?nESkN5DyFiP{8Gr{p0mcRV;1OT!EkGkEY}
zC=PjIfg!oFh_m-WFdGbg@o`X-E`{b@_uz}tY*=H}0F%0F;LNYFu<p((h{|+;qt=^Y
zO?@$IaAPQTGiF${Yal)weh>zbM9|Mz3jsylknvF(Bljjj{?N(LcI-AJpH~I`^rK+^
z$Pvo5rh#BcDSXM)K+6;@bmI1}hp#2@OsoTJA9EHq3lBoYjXfZjS^%o@iSXuRDGc+~
zh8Kca5Vg`0LJhXV+Kdj?*^Z)3z9dSFR>G)+deF+X0;kMdu>6_=24%EDM?yNt%k=Mk
zR0EiXOn_W9TL_zJ05fLzfnt;#$Sl^vd15*^ZRm6G821U1pC-Wh`zK(toEUl@ki&`W
zL<o`J2XQ@>uwOO~GB>S)#G-+~yf*{Ar8`-@^Cq}6wZHxfY=mgdcaZfs9>jB}LvyhO
zb{-lFPxvRnRU`x2`qE*c%U!mo$^oqSMeyaRG9(4WvO5G8sH^RWE)T6R-7*p4Z*PG!
zopNycVmM9SZ$f?7gkZ<%>T#M8YUr3a9iPr}#fq)3&|asQ&GG8LV|`{qWdk-rsBa@P
zcl;(49jqv@n=_Z{_la=a`*(Q%cE8!VQ>4*TmZ!Z&3wyTo@%z@bGZLp~U}r?Ht#@G<
zeI?k;vQuN|fgOYC1C!Czd)TjJ%p8VtW%e^Ok6hqOUa=!ykC#x5^%ra=IJi>uM^b6D
zpYI%ggGBz?OT15av3G?}GW`BLukes1I_z$;MfNVKn4r$S3ET(^`uCtNOj{2R!ZZ0_
znm6-Bxa-IRKLzM4F6BR__RJ!m0zNY!55}k^^A9%7XRBMy(eZ>DE1toH3y+fd<C`-0
z0b694<tf|wjnjmQ{q9u8x^@eQ&)ovbucVoeF0bLWQ3IGZdgC#p1lTpBhef;ody*$k
z_*%uEX|HmocfTa?Yt+l(a@ZcYnbF?Au8m@ywsnx%7as#y4}<anlI*+QW>TfO4ctN=
z5$|4adNfO)4jI3TeO8jkH`mSMiyUd@kNLcZuf1^_f8(T7z8>>|zgsJZ(GTQ^afCVI
z{eO1|+yC{s8E4ma_X1w1_e;UPU+?lt*18BJXGQYj3VJYHcd}q|l8Jy_^N6S3>VPxM
z_6gQRAm&aL<y|~j$%~zRh-z2F3I>|RP-jbjI=QbMb9qOpzBWhf$6>6U<*yG)p@M^*
zM1QU_(NI0i=<g8caQfZ)Pp2%6o!5(dtSYeSjo8M7o;XPk2D|{TCDVaXTLzW`l8M`;
zJ?z}zab!%2Bn%#U9xk4ZfEKiXmDVoA{JI>_uaOY4br-WccsRVdkwI$D-eg*f3m|-U
z8Go>NzOD70PIgkod7@<9(SMrvFwd7RVB;5C1F!uFyEx-4F`kgcj*=0!1zlU#;N=?I
zy)C6gdh}+-DlZoH=JfInZ^S|A_*^!r`~-6>V-R>1y1?MxiNx*rGf+Of8^*cJV^^-P
zWA7f3=06l}WN3n#?VSVr;rdq(#;umebSqTCjn(^LXO9mMP8I9lSY4}sHH|$}ng(ZO
zPmsEUi%C9nml+knXHry?8Gh${n3S8vpE}PEWan8EYq}5asS~#S?o>GTzLfY&?je3d
z5=io>7&7wF6HvF&U>BsEAPS!@lX)X~a8G6>bIB-~Rd-6U-8sz~2CN#xycaXJRn;jW
zc2%Q*Yr2s+`lXPpKPgUzd&;s3>6eH@_Eu1RxE;39TsG4rknga+g;jF(fWV8qnw*9^
z%mn>OpgK+6*1KvbUVBzg&brkRw<H^cE&2Rer%uBfkq(eM#i7k_=7Cj%1bK5t8>EWb
z;h_0*a>O8xn41W}Y6mM~wX@Im^*u|Jdl?E^=0VKdk}Kd9a)#CP5(Aq<NzB=oS!8u`
zDZG0#3F3A%!)Nca{H{7*#v88jr-V*sCx5hri8aQym&VPty`Clv15USsgxP&|Zjv?x
zPAP|%xo=sn$zlG4gA+)&5g`vg@u0EA0m8}&yU|cEu6w{bGVQ~8R(0(j{;-NOtWD${
zX5rWejJ^ej^8<@5O`J8R9$QLX=bmTI+b7YBI#-whx<a_CeJ|B?Me4TAiR$l==w~&D
zBl;gx&C<+yy+n2GY4-D-dE}AiZb-e+%A~klWPcrrtgP>KW`E1qaRy2gAuUXf3~IX%
z!N&`1$FwYi>@*v)CQukts3P8;B~9nw^#DJkLHrYI2f~N)y<{UzU_#jq(6d|-Uz!)Q
zV+S>m<k@METCtl%glB_}`w_;Xay_;lkb=7Ni<lMTGZ-KC5OMvo0P@NNuqSU9!&xc`
zZ>Dy$hZgT)UuLPmdap|`A=eh}?Mf%|${YEmM>}D{RR@^aRad*UZ!>#~I}n~6J<WLY
z55Wj8BWA(9hwRW*^+Z_vBw1qMLA*y4LwvR~B+3)kqvRsrPX8r4H*JIMl$k<kQQ|-j
zr3o>EbflT_+1KEVJO!t_9z>*SQ~yRlDqEbK#|jNPNxI5LVcd$D{4mjKxMzBwZ+2%1
z41YHq=D!$6!o19ZzkLxol9fz8<ecSSh?9oBoBE59;=N>C2NzqEec(t>0$i~!x2@H_
z%KDnLLhSX;Y@BccIl196`SNNr|Ap&wm=yK|s%DL1dl&J@%{V!73v;2`nS~c+kz|Ey
zG*hjzfcU&(nUTASU{aEm?Yk0pTcL#|?1c7I!2Vl{;-TB%(v?KWpV;rmFb?C_9Lv~7
z>oY#C*6ft&cfgAg0zbtaB>7o9slU*|O4&RHpQl3nn{oB9XqFG~gHzzGL_7JsBNr}I
zr;rYXBxbUE0IWXn89GLY;qsC4@ad)uY+RYh)OKZoxx*Yd6g~^qc2qz&TqQ#m?}C$y
za+xagB;pl#lW}`r$jH7NNggrH;LmAbET`;dJCd^@*W@d6@n9)wJE4ka2lue|9%xao
zb#?r)ughQ?KL-{!XTdqc`>@M$24*rjOl`dx>6w&6?k}Conto6LO3T4bqJgx0G$g$a
z+u4)t^Wf#YBjmQ63)3ua3S9G@Fudq|ZQ-kKP&s^*Oo>Zk8jRIR@%1*Q*8MctL>_1B
zwVnTVR+&3%td~uu@{@w;2gxKFv?rEP)zM-?YUWafs2nQWAn|{jRhIp;%A}aX+uH(|
zxnU+xKj=A%-|vIhB0iKq#hm6Y$sh`m(ezx*6&ki-6UHhH0PA#H>?&3hJT6s3sq$o8
zIMNZKyH8Nrc4^wsy&r=bJ?V~^WYiYP!EV*Nc=`4&8p%CEAKVk*0y0dHtf<0Maec@t
z_^9A@!CSm-SxcJsU&SbI7u#ja$6>F092gqsQS(R}=sF{TPSIxQWVe(~wpl~QoK_du
zr0G(|{}StX;Q-CJC`>i8Mv+a5#yDWUCj>}0W97E7bV-o|l?gK9DGcJ$tM(7^)%^jy
zQWp^#ru+!D`W4_bSs7lzr()1Nw*cpEyhj9gZjsNC(^37Ep5VS?0%o1PMnl81N!$QE
zfd^+eH3*R>qqe>vee?ZjgwiiCqwEY3H+aR=OUxuXOT-1vYFDtko3M78xwQSt6L875
zMDZ^*#H}rqa->_S_AU;36p!O=nD>qtxy-^x>yZYn;Rvk9&ctM2f12)B!3?%~3@<8H
zV&V>EB)g;V>Ps^^u(O#I+Z|>1DS7hbR!I}1^Rd+MjvrOGzD*K;$-?%x>bySoVgGhj
zF$RQ6VDIC-wDeUvjgR)G2bash?%f~BTJsfrovoSp-2V)gz&jkT>%vCmmeVnbWo-S}
z>C~~qx~A>YR)~}wMfWe@V8q1PyhR>d3~Z4SOz1mEQa{R|N=pv)z0*b?^tI6GF1tzf
zlh1g1rxXtCt)aO>LwJoJjqu_c6Wp_A85QUZpk9p`xNh?k8raT39g__(g7j})I9#D*
zR|)J|c$G}P8jR5wbJ45$8jO2e4ozkIaNHm-HcWpAg$|a{8LPn?ZXJgE?H=Q#PZI@C
zvy~}dt%as^EkTpgQ}p__E%?EGh9J;@!Las9x~h5|y}9N#of4`<OPppSXQ&k3NW26#
zk5189vWJlC5QZu&mlq#0j_#E>2EV@TB9>8FXqA-=e|N32a@N?+mV>_b1A4TA;jQ*A
z#n)-W1k0rzDW{_dT5>YzJiXr^rB>A7s&j-Dhj0fda=pEx7W;cf2K?g772yc?f5!jz
a>#fQC{fQ7oRjx`uR`EZu?)D<`-2Ve1o|-xU

literal 0
HcmV?d00001