From 0e21f2d0180faec6ea993ed7393f26e2fa16a119 Mon Sep 17 00:00:00 2001 From: IndPrinciple Date: Mon, 20 May 2024 11:54:37 +0800 Subject: [PATCH] cuter logo --- Doc/pics/Logo.bmp | Bin 402454 -> 445014 bytes README.md | 8 ++++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Doc/pics/Logo.bmp b/Doc/pics/Logo.bmp index 9c30e0d502bb5d36b712e7903349a7b3e0295b33..3098fa6cf7b839f6c6e7a6d242cd7446c2cf05e8 100644 GIT binary patch literal 445014 zcmeI5^?Myxp5}Y^hy5G&d3K;@rU!a=W_q9@-96pY9mfz;?8HeNLrgI8_^3%81i@v=5^MgJ@KnMr{As_^VfDni$0&tFa7O%2} zfDjM@LO=)z0U_{%_=XyR5D)@FKnMr{ArNl_#5dxNu*w$#LO=)z0U;m+#5dFign$qb z0zyCt2!VJbAifcAgjK!}5CTF#2nYcoAikkCAOwVf5D)@FKnTPe0r8D^Bdqd;fDjM@ zLO=)z0r3sB0U;m+gn$qb0zx3(2#9aQ8)20%1cZPP5CTF#2#9Z}4F~}tAOwVf5D)_K zMnHTc-UzFFAs_^VfDjM@LO^^&Z9oVJ0U;m+gn$r;Hv-}t@kUtX3jrY@1cZPP5CY;G zY6C(*2nYcoAOwU!yb%!Jh&RG2UkC^RAs_^VfDjPhP#X{eLO=)z0U;m+;*Eg#M!XSL z`9eSl2mv7=1cZS2hT4D-5CTF#2nYco5N`y;H{y-3$`=AcKnMr{As__AH`E4%fDjM@ zLO=)zfp{Yzz7cPPRlX1q0zyCt2mv7=zM(cC1cZPP5CTF#2*eu!@r`&Rtn!6`5D)@F zKnMr{@eQ>BAs_^VfDjM@LLlAS9j0U;m+gn$qb0`W#b zd?Vfnt9&6K1cZPP5CTF#d_!$O2nYcoAOwVf5QsMd;v4ZsSmg@=As_^VfDjM@;u~rM zLO=)z0U;m+gh0Fz5Z{P5!YW?~2mv7=1cZPP5Z_Q65CTF#2nYcoAOzx#fcQqd5mxy^ zKnMr{As__&5P1FOP5$fGuU;4A@vopDxA0&7%YuCV<`w=c;A+8}*KhoO=H;*A8(ywG z$u0zhfDjM@-az2Zn>Ph--oPlHzRG>@GUwW}?9-3#9lm!n{m%8Y+t>Eoyt4b|75?tH zes15*D+ll1$a-++V)lbOFP=SlmHQ(9)vMPq6mPQ+@eOaZR7oiWgn$qb0^UR*|IM3c z`MLLAK0lxRaNn(~D=wa#efDVbsY4S^92lLIHZn7H__2LM4)5u=e{=7BYuj#|*>~Ui zQJJY@v(hJ@JUIRI;l&q@Z@GTq*!|nL;2wFo=tH~-!w=#c9<4ZuEd+#s5D)?-8G-ya zub;ijgCt}=xV84mnQ5mpMr5W9K9Vxv@a_Re_Vhozn}11%cJxf!&~fLormLsanmeG* z{K0KD&FQm$t98}-%l(6nqzpZ_cl^oyOD>&AyLIi#)5i~Ub08iCC_R4gjM77Vqa-(1 z$tDDZfDjM@-a-HZfLF$Y+!tshHeEY6{Zz(~qba`p!8(R%blbbO<%Sux<_)MkzD@a2 zO~0AjujBS5{W5k2-t2c~bY|MJizjwmIko@l>BqS_uRQ{g_=ZO+N@5BDAs_^VK#4{G zMFUI&&BL(=w^v*`IVLN8;5$8rFJXXD^i18*YQwB==Jc;Pw$&%Y8&w+D`rAdry6#z( zbjX=(SVi?cxV_E#8H4w&+j{N%)u)eN6y%qDHHY{{iEh3UP6!AAAs__2fB@c{&-3## zAKY1X>EyVq{Xv-qRH4s-ZJl;5tGjS`4Ou!dD9b!fVJGFFv-hj;nX67zBA zT`QWcN$zuCGrk|mr!w~3ynOrlQ=(c*GV2iE@IphDj6y&N2mv8bLJ=Trgs78iPqR1Q zxPYH$D5lXbV^`0#jZIc3SDn=HlM#(R9$FvG#uwANx85|T@4;c{?N8@yJg{w}5Gs8P))YjheIj;VJ6IVZ*mf?r*bk-d8jGc1>B+ z@BJr^%t~E#`Shiy4@u%t0)uD8H%feSmViP)2nYcoP!bU!C&u^BpRBohhOkyUQlQ`o!GwP_N9g&qU9jb2ey^lInPkSlo0sDH;TO? zUXvuhpy1W3S9wJr4)XK!Im7ux%7(Fz=h`wLKnXPeB@&QQ^DOGoZeUjHDrq(ADqOXp?Z?|9IA|CTxnhLj!I(R6?h#wq6Hpp8o12^a`0-=f*o6xhjvhTq1KYlRJFSaa z<_tB*=mNWU@7}p{CyoF3@#D1o2M-<~9=8SkdGVe^DrBQqBIM1R zH^KA7i4z$a8L6qMAbjA!fvl`7PVyF9r3(W!9Ss5y^VeZaU}Sjo=n)lt?b@}oXU|%L z3B5QiEe#~ET)AS&fVA-tpm-}H@lP)#8+k8x-Ml>dc)Dr2FN}NL+GN#~$`jgJnhhui zsWuudAJ;oQh|`6+DC;Vo8*MhvuQa|**^!MY2g8c_SKQoj$I`(^_7I;-K2jQA;^Fdp zq8Itb^XJc*i%%x-bMM~0=m!c)Kyqew#-ioRm-p+}uWsGCRjO2}P@zJZGG+ew$3Oo5 z_rL$I|N5{0{_p?(^Pm6x$tRywtXQ#T&6;i6v>7m9z|^Tz*R5N3?AS3l00RpgfT6>$ zD#QAUFpNLIxN6lZ%14q)l`0{|AO7$MO9lj}R;^mIX3fTo8N&?4kj1bT2m(~(&Ye4q zaoCk!!Uqvji z{X@zGE~J9IO`A5YXV0F9O5Z_dy3e2f^e1oz;j(4R@=~9F{&}4`b?Cw)MvS1#@87?l zMt=SJb-G^kYX@Es(#R;t$S`o=Kw$jrv(N0ogt|tUa^=cZty=Y)Z@y{Os@0S!Q(z!0 za3DW)TlmV{qv_N&BJ=xnBVL< zzCnLy`eStZzX|*>utc*GWIkmbgxC`&PGtP~cei&;R_-jA`}j*M}jjT)C3bgRv{zp#uOJsaWui9zB{-(I5#= z|Es_HtH1r*zx}s=`!}Yo88c?Ef@84t9V(f01`QhYAOGPg2@(6JKmF;y z{L8=4Ul4=l>c=0TNu4`)rey{d?-#%L1>G&&u3>%!UY41fVkb?SWC>5NM95GG)3fP8 zT%`+B5p=Yl|NQ5_`qi(#`s%A?%a%bo%#RCo6*2fNyk+LhnT;DariK60KmC(=FtLV_ zzx%tt0~RD_rGxf^Wec3mv2TVFY&8E4ZP3rj0XM;Q& z4QtKq-*r#e(I_@~pv^z>lnE-Aj^~J9%GP!p4moYt^b{Kr$#A)GScI8&SX8 zx(+6_Awz~RMF#x|Cuhx?#Y4k-J2(t|p=HaK5Q$L52A-#(vQA&Tcroq7R_kG{Xw;}t zs1C(>MhRMbSmGIOW@=`NhoaMq;SYgAx<5l_LGKiqcF0;Oz$d@{`s=^{`@eVpP`^8& zJ+L+OOF$Y!lneltf=l=n9er?X;)w%hpN)QpcA{ALVp=y_v%x|2(=N}puT~!g>@z}zCjf~ zd-iPg>ecW`*jh})ptU3=C1H^%9h5t+eT_MqJxZpN(aRW(!o1%tWo@l_1IvzRQWT9+ znAfYy#CF(Lk`8ST#R?qH;|lWKit!c3G^b2rX)&g_EUo$4sh^H%UTsQeC=l)+qq5S{ z?p#MpQ(S~Ye8bIH5dq(z3*&ClzI}U^*wGITp@a;JZ(xoeHEI-uAxe1|FtJ3;n>X*t zlP3@=EFGbinc^F99Ruyc(HqR2I~N^A#5B@sU?@5;`eXG&ZH2Z3#{*0Tq1s-!d;_%@ zri4&UCDc>w^E6tlKTVo6Ie73O)Fm@B^UE*4L}2>{--8(P4W5M!1$P$%_40kR<8cIh z1NsM_oHJ(*3?bAjJ3cq)4UkM;4L0RxuCkk!4lD#7=e=Bg=@gs7o4G+zn(;9eiZX~= ze53s6W`#bY`?r{XXu6uQtMks~pC@<4C0x^3BYQ2v^0F12?oJjg4b)PSB@3m09$NKO`A5271`h|!sQ#Z zWT;x7K7Ic4KmRkzl|s-#hAPH0e9f9Q)DiFNzKeZ0cjgqlO1pb)%<=suR#2Gvb7!j! zvn!4(bg{7hl^xOO8{9ThR=cDJLCc3H)L$~9+^E9Dq+|?huxzY*_R=GD!)KF7{Zap` z8NE=vP(GAn!THQv&!2{83XM@^i*E$&gMKH&;u~l-aL2;cAs&N+pJ49!28xJiR+oOy zwZ3B9XG;3r?|v7G!-#LhsGFLK!4sfGixviA5VY>hCz;3b5GGnA)P&B@-SZ8+eQ*#( z{bGKo%d2!Nnmt_CK%Qg8H;}x4|NaIi7MC*n-bPIk8RXu71M^m|UcGP%^(`c}$3P00 zvuDr7A=cE?KFDk2Av*o|{AMSGweJHNmDg6QmorydpGaMN?$^9`J@ z(DdTT7TfVZl#nj@21_KI{LRjjfsbGm;uCn@_YCVz!<)vCZ=gJvej{+ar)Ke`iC`*s ztXXcLat*h+=NmZr;PYc>C%!Gp%`tis{5B2V6tUtP_%`5t6^c%~5jF50aKI78CEq|T z303>(qmK*~5%`G6&OkXxzaw7`-(H5o2TRJD%csp5%V7wl_Nu>hl(jvI#Wx6mZN6@L zxEsIvkqyF98Wa}W*eVn9(7iCC_C2Ri!&h`8wdW1O#gv~nSvAQ{*)j3tK{B!90qgs+ z2{;ztaML$k@(mg%LuTkbBfb$hAmG)Brrl*g3bQcH zi3&yeM$O`ZNenV4eQV$Su}i)I11AoGR_%VqbaN;77}{h^_y&>_`s%VTBMhCCj$`#= zyZ?ePJRc2-P2S)eg9i_G!#5BBXBCVcE_<%~x(j+IuYl!Nk&4lEp_SA1!FENJJMnhJd4*WUZ&VhAV1;GO-LB4cv$g`paVYD zM8E<#`_^ONF*nd`FuN>SvV{DTiec!%)9nAqe z9eoAL1k%gk6v|)Rp9p)0N`)&Ja>j&j(D?C%cEr|_oQ_P=EqW^ro?c8BrvH*_6oeNn zSTJtfIQlR5(7#|HF5_Vd0B_s2Emh-(e9*7R304d#Bp;)*;N?OhGJLDZvBQW2AZ}n} zWr6(&VlPJytGhjUl{e>%!wxCT;CN_!J-hF_?br&PH!6*9+ivSy`-MIGhkH=ueLA}Q z$hV;`700&3m=abYNr!eeTRYVXY^ge_L$^Xl)3>^jFq;)^W5{@(sG)Z-4t+ zx*Im=n0z*D*npdQ&;j4~B;yQ&Bt#_x8&m{1)z1DEv( z%8V7?KtCh>hFzid0jdKM(wb|8T0o&ejwz;oznY~SPSU)gBDf=RXVA70^rTC^L9H>* znmYyZGYg}rAriz2cZJ@gD#YWL#F$tU%s&qlFD870wB*EL1s3ji2K5E{3No6ShX}3` zx()-uO@egFRDyP_ zFvQ29Yeo6sI5KcED=){P2K5EOCe~>0`z-qyX&F?}elRt-oS3*RR(u29j`)UM7uEqy z4kqd7mP37!A&Tq`em}RrQVv?Rv17-g197jqcgZ(c<~uSXNG!~m4kd<27aOrJiT zMY?;zn1Z9{8}u6HZt`OJu?xSiC?C*I5d9SvXLdgh z;PNZkK^rb3wDv8H!84>NrqyB36u-g?4LzIYq8Nd1u?2}CXnVa!3Z?Kmp3d>|2YOg3b3DHuNXnO6@Ec+dkwcjM@_Z3?hMA32jK+(aJgwvp78@9@K$v4)nUF$e&qxQ$R z!?YL_2iEDVxH0;;6b$jA=NkwE0mHuF2d3Xwwk%;?<42Q%zC~CkDG*Hv#uvwK3)#R@ zL-w;!=-JPuwGcOr*4NS72WK0Us1dJ*>?eBqpy18xjQcm4k^N?HzpqT_O;=AL`omYb z(O}7F+(-TH4EJm2T`Smko}3$2$z(@ww{;Uo-RlO3jic)Qxu{Vvx*y#flYZ=9#a33kiDcl5ep0 zkfR2M%&6v0fq4Z@j{98V(en*vXRIXVsTt)4_?snzl-Kzt5KI47Mr zU^b?}3eXsQI=0X|!X^fdmXF62V(SnhJLtZ5P4y|Z=SF?@KxwgVy00n3WwGz`jfS=7 z4+>PgY`<~g#jCu;)RFi`OmK!p5K3kk9~c}MD)Gj299Lr^k8dH2oOrXCi2>seBWGB{ z3sV>le&)CX9vUmYfvrk>!?#*F#?Zii?q;2TxO{_RnUdfVj!Frae1n||&5eWyu|oHI zwV+?&S45^eY7wC^(en*_v%7ZfYK{%TtAvCVZnT0yU&n9~rx(YZDkwMDKhCA*%J*5I z&3283!3qFzfnz{0cysv{So)503kvq!x;i{F)jX|t+q>4Y7uyhsQ2&<;Ty_x#L z5!9R@f{BCdlwoZmj2O5gI|fj@WQH+R{^zyHzw0!SjsCVGMoktHOnQJe4}H>j^?(9cjwjiu7rJ7u zUn0U_caBAsz8hHSUwZOzf|D_&SNg`f3kF-MJ1t_s&aG_=b8fgz{u%U67y?;ID~)Sq z)0m25TDC7tiXNV)s8u+zx~NJjj45R4~BrpXTxxcpExcDp~CKd6G==%%$=kepm zo7W4tniF)-$|Cy5MNk5E9Bj?z;e|ygj3{V|hEPvr6=t67VyNE`-w0X@WLF?W!k}2A z(wVt%K4b!QKQmG+{=nu26Dz(!a;mVHB$R^;TIS_{^n8PGGe<>AocIP-43hJh6_PA% z2y?@2ENH86JjvT3yg93hr9X*>wa8Jt;=KXBk$U^uD5uDj4%-)#P?SmBA_g4Poq!Lan>wu4+hB>mpY z@Rhk0^^4gF0TVe3y>P8ahKDBp66Sjh7Uso1HOuUbmmpq7ysR4)Rt)(DS^~3vBLcob zw5B=6HhR7R1;Xpe3~ZeE2ECQ+b_QiB70T*n_wL>938Y`k#NV43d9$4hFJC%1iz&a~ zmin)3(6;KzX;%G#)3<#lDPw1&!v{)A}EcY^gXbx&Vr$q5~hf6^bXW-aNDGl2T|!HAn}*@M)chW*D|sdnKSc* zr8JISq`(p|sW>{NLr7TF;^3E-mWHa9p~gI*eXx83hDiiLY(KOjTyWix0pH5yerT0> z^0m|y*!!4b2#17q@E|j#6yJbvkk_JE_y!fkaAD>f=u3$o@ofoV9itdw=LK_eLMRR1 zLHHzxRdOk~`DtF>^s|RaziF7_d#7*tVrthi!+%t6)R@-2^Uf8~>^sln2v#LAsV|Ko zy0-JKpnPL=R$9ir?{f>Bb7)6dzv3HF0?5zNR681}86Sw| zBXM**K1?FafaVvuc<~}C0<%4uiHT8;wIQjk38BSEL`G#a0Hg`RA(lCa51s%Vr>CdG zNl5%<9O;uQnP%eX32o<$YEUCQ?N>SQNMvpNpbOwvuDqu4z;Q*)L)cBWKK4BdBas) z&S-3O^HAk;o(0s15hFf8m(iQgpR#?bITE(brg>HpElaskZe$a3fkqz&+i}OzYEwGd zHkwaHG^)RNWUnY3P|2xIf$uCn4QtOG6g12F(4%{I-Mo^MFTUa5X;{!P*_oZ4m@yNX zUz9yiNUY&Fl^eQtl$RJc2s<_FB5)nqxN#%&{X$8j@iRi+;F9%P>6gBu}{3v5qA z6`-Xz+h|HF-@v@?9z&ORGAWbL(vdg%_lKhIY{6EeMvbsqAQeYo3oQqu63G^*S^iSX zq%@~ysd4kto|h^{zOiZ3CNmwP-7-o<5W8W+3*R7>mKlUN*;9@jIl{hm=4M0ASW?j2 z(uRA$C<@gykD@SGM$vF1o5Gc(1m1u4@%^#K(+zq9oG{Tsd{VT@yET#ODYca;o@kPl**FtRiWkhI9p=5L;mET3s;1g1B@rYjOLBeMS9^SM5>ba+Rx$&+J z={KTBm}owNJIq6qdGv_#D)T<0t64+NYqAh#Vb08ACJ9jrM$81I|U+_xx_sXoem5%0w2;v3QT z2=+E=+_-VVhWfyP2qigrhaCMLS=68%ojZ4KSle<1KFJi3`S;yHupiqL7NRaF_s<%zJc`( zwJqM`L4RI~Po~_uGUTXfPuR9w7F3}{k!wNwtIHX}Hfe*x162H<)KHqS|(*j#aNz-pw5~AQj zNsb~2ry6spqhB>e@RfNA9}hSB4M*RS2=p8H9wdNov~1b3Soj7mG~^;SR|*Rp7*Sx$ zbbki@2CT-wH_(Fe6r9uCmsvXQ+K11QFyiFE>Wf`#qRUX-2QgnuyX7VyYapKVSVM9b>_&mr;p>EWmJ44`aVJ^ z2MIjQ@hRrfBg(5peX{3;`{ct=4s66YgRxBpUg+_gn_|c}>esIy5B&x~g%Ko0DVco3 zYRPyT68g&08`goY!!V&l)9S=GKrc@EjjXIJw#+lv4(`+O_TQlKz!f7-DHi>>S}Y|n z;cmEk&fqLcDva9m2Y)iWFyh1dS7!m6k_2&z@SV-g$NdiPYQ1@Gl?iR_GK=m7X!DB~FQz>h2Bi-(J|*vU z!K%xrf@%P)lWjN8w?hg&0#2(jn#SuY^>&3l|inGVl!+9VFO6 zdF#H|QgCNpLB4@+6m3911y4?U630QJdvrO>aWrkb5@PV9LrA%iOEGkkBtBB?S`( zAHr8%e%N(o;J|_AJwVySgiKA*WE%(sffW!#4Ge^6-;*a#;?0i02!n$q+-BRhZFs06 zm^o)@4D}nhK@tGyet>mpPoYL4&~K2LfdN0ZAIRI}$&(2)39O6Qo}ry!N@Ed?0|0xU zk-5dHSyVmbcC%`h&4SGinc^Gq({IppJ9X-0c2(u+>~<8c3Ds^$G&6R;HE+RyDvV~3 zfCgzxRT2(f|6sDGkXDow7G(FbCUGK68!jJ9&hSu^xSR9c_pU|r@X2u7Q?x;i={>s? z?mllyaO!xq!;YoZeWGh|2x(c!VM3Ih12-As{o2mW_)t3>H01vvt!x9oy0_ zw$k`EBro-SwBPXz`HKc?F-$j%B<9R`^rJ-P7e!36@X`GZRu3k=Y15`fkgb~jPF``d z<`W$_mil05#rK@!updLd0k$Za*(cpGt(o=C%r%7lng?wR2LzBtpx>Y#S@*^EgS!RX z(j}XUZ@vETgCpOdi; z_kBy${abHb7!+c&HX=T1OzUAsm{w2j%p@L7TG76Tw%3{e-lq1SP43uk>%wTtgh*ga z`F7E;vhVaTu#T^0^y;>EjUUJG{W@Fmu)$hk$>bYIMGzti_E19v(>mE*;a`m^y61xy;)yp2=U-ultltzJZWv=FKW-ye`S)<7SBVeP#Ap z!=ukU^56s*!LZ}|l*o?BXpO6?VOC;HBlyL!aF=|82jRyubm&lWEIU#TD`@EFKmWNw zJhCcbhYGhw9ABpt+<-3!TjUs^gIeQP>{tsx;kdOBZmVIX%H*MriZ!p>Q&6Dw?Ag<> zexYhm9s-?vji1#lY3-0nJcJF-W>&ouPhBjdO0jpJV-IeR3c)uz?^{?3 zSiV8uM0IR1i86X%qh}uUdn3bFUY30^%wcQj5D2AD{30FMSS6XWj^G37CQE>OzQIU{ zb1ZIbckbLV^90It%xuZ7SkO5G{vYNgfWJ{y;>1E5aD=F7)23$EM^fE-mv0dD zV{V6z_yoOy?o0+hLYU300Qyb-9QS_Ih>GV1@zLgPOD|)kfah@HN0p#xB>3dTClAM; z*dJ6=!KQ2#$F;JYA_^TXmXGUuAo6_Uc!PX3lYLlz+|<72>^|N0MzvuIV&l|Wb9R!Q zk&H0gFK71ZYRrI&zskm|=bydGi#OEr7mXppjv?)+I9Ob`cVi=tpi!en1`fl>fYT$3 zbeC_zx(UMLW}0v;kVHW2)?rq>Ae);BJuJS#2#o2OP!4p?phr-|YtsVIWxj{V2H)ubO`!f4N5!Uh5 zt5;dSn2n6IVJd=67>RdwtP5^HF^CBU&6SzPP`_wSip3=?EQsQC^WB_hlTI86mhx*? zn@w}=ZRpwSr1{$ENl|Q@(t6`u-&7t%yEI*!9OXVN@Qn`J7TZb~s1X^-8Z04IX~;-e zelqOXzTG#kynI~{CrIsL#W!pyqCdb4O+Q895IDP8XPEvNe(~~h^igDRVEVwt)NHWe zSv`96V6<^5JbH3;EUa7@%?O2X&wPB#w`4=fV769Rqm~=fd{}&gVi_&*8^N%0{`~ns zA4?W-Xg`Q3G%w;{O59Uww!b`c<_uX=$gqJz306tXI!-{ob!s0I0fb7;9NbM6kdKA1 zZa0r;(xi!5zX9I}i}mr)5@Jt@E8oD&f{K7nn7IL02~Q(b3VJ|~4ytV7Bm)keW!SJ` z+-xA>)-XlK!5fWMWVebB>flBGtC?qy4h#rK#r)BH?X*wd*(oZHYt6=O7%zfqLL5($ z3gg>_Lv1Yt!~l^<+w!=OqY)#H=#Zw66 zVT8o0#Reh_zvhS@N?;O%GPw~iD3T@ZB#y5H6rf-yOB)Mb;%(Z}7N8@(tQKO$B7kAN-CSnG*UvyteS@HWw9m6#?9IH(a9~ zqkF8rfcb+OfuFFJVfDci>D07sDilVI{uApAH<%f?RTKjbH9~Wur~XxEH>f`8H)7a^8ADiRqQNll-NxWRLlk|3Q4-E6JE&O*FKSYtKoUowv|uuwA26_qPjZripkiO3)=Ow-tQ8LSwoAWkfZ ztTi%Halo|2d2A@ygK$rU2$^N$5e#mN7AC7%mNsTJIcnBg z`O*lnq0j(GlS`8@+wXvm=FLi(hU(^h;e_S_3B(Ai4I_3m`VB}a+4*S0yn^9_yC#j? ztO~#|LC_g`HbXgqmuRA7%mZ^r^r$KJDWF=-Vo)P|02yUSty;C%JCeMh^oR))CJY)h zh}8`{)R5fRTnknq{Kd^|@ZiCvM(^hca^MX#utWE5j?PT;o0OpzE!NHWbW96tHm^RV zGpV}#?s56G@4@YjS5L0+PE|sIRVKA>zkRXGpNG1Ql%&nqO#O81TL~!^Clj`JG23Vc z9NxY3;t8BZ-~8b0jui-3SZBmH!h*~3W~OOIGa^dNLj)^6=6xnglo+Y0sVt@#?V%aW zfaDow-Q>7gJkttkH{cJkI9R2Tv9bh zzClIc@#r4ODES8J2nawk%inw2nvkEHCnc{!&b zKLIr*z7cbfSwJzco2@F=;K10<;DAdQBLhovMhT8xjt`7l60s!$8->4AS4 zZ5Tok38N2^{Oo5xW4z)oAHH%PfnAPWXb%`vT{@OH@(nl=Q>V*E2fkO}8Qz5jU}>^Y zW1%CwHxv&9y1<&XD%Yx6uDXPm`&rcEmcy{@rtLZM4Vnj2p#iXs&ZbS9N>jgZ(?kRB$32*sEQPNI= zK5EWM>XEw9_XgL;yV`7?Uupc0IYlwenB!I5l#GW)%MG(CPiSMQU-(;Sqgg)QoOXkf zM`xy9c=8Z`uRt7PenxyF=8#e#P7y2^i70eAhKCvfLY;?`pc}z}?$R`Gza!dp7N?<# zjn#Q3uiCY1qZ@H!OhGnBzA<3H0DL>$SV`Qx0+TZCju?h)SW3YGuT!pExlnw=4J>Z% zp*{1Iu#&Pm23U!2n42G+2z?YCDz21+mV;|LdDKgdN0S*<^Hp|UJ;hu44UoZRN@Q7s1`SYwM&JJZ>XfhOEivz6OT~lBeMOYw zJ85HN;h1(RW6=8>skGa&z}o8szEPA2bdx=6yFVbWxNnluiep=`lNuz%eF=egqI*GS zLMV!z%>(5|-GxI*Y#w;C@0meIQqpf<%T1JTu=qxtdJUQfC|A z?b3Sg_jd3NygmX4oEVSnq8#mq;5!W>)Eu28uGB_;g9Qj72N|nSn9GerqqfknkF1FVgjwdt*I4TPS zjI%fuhgGwVGJE=l>{l;WUp_VX{f$%zNU;nS(eMqNPRZS2Sv@G{>zTc~rL2uoxzXpq z);bH`+lPe|9IZFbaSYd;aN@v~r;pu_)lt@|_(qff8h%bCvR+_4$ifp_c{FQJMi`6~ zIJsdu$IUO|v`+Y=V&!-5hT(p0LPFjV*Te|+ba3Pwgzb`(oA?waQ?_s)mLWaT9Kv8xZfv@C{z+cqV)Vo};@yK# zL=b_}wQE-*HzQ*mEXnac#ehr34E*$5Iz{f{qYxG-J3phD$aO%#m*}dx~!udWYX7oH-d!@MvOxSlB{j8ZCZ>o&@BRl9DKm zd?0>L(N_?_YjoA+Q@(rC_efpO9&NA%_(rXH10wL>XuoZ7)kz&}m(Ci~d-T}1J`{^^ zdA@hrCWNu0T__v})V5pZCuNv&kqtP!hZvl*kMAc^sU^OVfSyH#qJ<`e5OV-Qi}*b< zj5|*BOp#0+*i~T~1iY|-jm(DP_kt{Bm~#oFMNvSi3fwuEh_MU1jEk{V2Mk%zCnh7} zUORN?K!G^YN5+M4uO$r#MInaufeZP5*s8<#Eih+8Y_L@^g`^4Lswu)OayYfL(BPMB>0Py;F zSFu6BqKnVXOmNapKY4F`4Q1yx%K* z)4T2C8?Z--V;(L0ht>hsjiL?Onpu2<RC-7zeh7ZJO7FXvG#oKaonvSKg5~MGpo+#SYcKe}6O#%t}-lst@KG zhy*|ZkzdWy4w<=VcqGJV*|H_t5`2>3$zdgU2?T+V2bf{6&>vE7g_~UpPX^2ip^NNA zbX`&u!a=+2#QVm7aRNH3Wc^RC_a8q`M|&C6ueq`=>!=nEW&^_q|x#T z1^0>%Bs?7RNGawA{lx z8a|Nx7A;z!8nP97fd@FuphdwLVJIi)B?O2bSi1xZ4SE4Ag8b^RDTWbxF7=B}kB&@t z-nnxpSLqA9cx<0;i%}{MXql%U-J5dq5Y`9g=zfQHwca$>@{}OPr2F1A?&*OQLV~3O zrUBo;WwdG3$_?B^8?T&bZ|Op@?9SF?)x^F|dC`X)P1$<=;`97h39dEqjRXU(#|Z%; zQ1TH#^@lCV%s1F)gfwfKzDs^>MkC>i{QMm^E|1K5n~S5<&ZVDE?TY^f0U$-$E!-x} zfCI39y|t6tC&L;NmeSQJ^QW22Kw#Q#U05x-Gs3_$3UwyK8sc7380`|U*__{*S!a)4 zf0kYFI&qd1s|v(7qG^iytq>3br4j+ukF8s`7T+k9l^fPev5VRDr`Ze6XALZ}s^Awv zdM@l2#JG4Ns9q7ASrs2)sv$POX-!qxz@aaWk~*ih&|2nYcoU?CvBp_X7HkpJfOv4^+E9ZzRR75p=s zu1>~;QGQgjCab6PJ+Reg6o!LBT|{9H^TK4~5Cc3ny6#!s|FB!#NMOmhXEa+gwPI0n zbxXNXVN8ogE5_r|8hEqsnZZZ*F1vX0ZqD;Wt2THN}<7D49AwpV|e@2LHaE)yFYdH56~*JgSn;yH|WY zyRW?uEN&Y$ruFE&b2+*f!waoc zIf+$aAJw^Mj}qL0HKclS7czGhxo|kl@=Ww?w=BTl1LX!5kX9RJx%c`A;19dH?^|DQ z(eU!4-zM>ZzQ8n-XrQF{39tw|+LcQ@bq-9jzXrxJRFZ+eq0#Y>VX} zN`aNfw}$rg+3(=9IwCW5R#uK@h9?=1^C8N~;aCt4wVF@vy>F z8~j7d(P;VjUa1=md&>?uyn9qu8f4?{%NNCHMzN6;->{+3fe;V^Lcl^md_yh4fB=-^ z_`^GM&K(QEAjFc%#-+>tgKahq? zM;Gk?YbtP5X6m-@FWk>9p6J&=0L3=~G0_e1lSUYH2xod{4v|jgxbnb`9(kE zMuIQLh3p55&L77$A{0;He6O^PwdW1S2-1ArbVo0XpyiO5w1{kUE;GDnT}?T12r*gKM4*V&LL)LZMk5D)@F zz<>b32<-fF@#4irix#mP8apYo!6I9`vLUR!A2ED`?H85L+yG{#-})NXYb4(pZXkcrFpSMQE@^-kZ?Z0%IGe?_NJ=pZ`05n7HG>u2^k zXfook_v@UqM~~dQ`QlX`LYACb@FL$}V^FpqVmGc(AGWJzN6{$vwJbSxBuRvT5GY0j z*bwdR-MegsHf`E8cAl+Ux9;zL_dE7rWd~>NpHhtVQbHd6BtI|Z))m}2P;`)h^c__w zG_nx)O7O^+(|fnyzL>qhU)W}kLj7xq24Bh=5K zJtH#rt-gHf%G1aB3Ev*Yu|_<{HyqzcHwXbCAOzxp0K_9ZJNxwM(`=+WYt}622ixg# zG9J%TnI1wQC;!!%NB5RrI*D_puc8C*&<4xKvQ5M(!U%sF7ytp!mnrlsb!;Fuv3IQP?1OgF2efs3d6SkWVyreT9 zAOiSEJj~5Wy?u4+>5QSr-ggn$qb0&Wl}D0sbP_u-1Q`uwU~n_re|{ZXa%6&oZi z-FtA$wF?W*XHGtKknG}vj-=R3gM&T?wsqdMvi{OBC^Qyc+&~d{kN8F)CORVogn$qb0zx1H1n%B{oHTsFAF6cx zW!cvJ`&GHtosy`PqUpzkN%u)PHhwR_nbNiA(`?m}~ zx|fWgF9G-tZbLqvC8?K&By?ysoxnhC&BIKnMr{As_@IL*Pi(#X2oU6o$bTMW+0|a)%Y`_dR{~GP2T2<*&py zN@ca`rG$VG5CTFVh6vyb`sneq+xH&by#0WGckVrU^!RCRE`cV68}{K5I(yMpqET#P zO7(jE&R)1dI*w2>a4GxA^ZO5%91e86RC00zyCt2!Rh4fj4h{ zc=Gi5$un11Z%Xewd_l`@lkf=TU(2qOdJdU8eZl4(DMv3{zL|OAQrn)%AAS1Hm{P9I z_?c_5u!O?x#mn4%`;QMEx0vi4)8=owc;!}pXl4?s5YL?#-|$?ONnjx$1cZPPNB{z; z9nfPeUbXAH_GA9|Stna};d@Z-%N}idOzzlsTG<-i$?j!c`m|=ReFsj2(ptQJ^Ct7; z^{co}z@Y+`FGWZrYkpYWx_<(zXB08#nKj@ZDXbuOsn|=rL3Y zLO=)z0U=Pz5WuZs!HS&~zUpDSfSNgm@72n+`;4BlI`hP3(wo0}^-MeMm^OFGwvm%pbm%j!M#DjbrI1S0rV#c|tb;#R?f7lW;r&N0Od7GEd6x+vf6>kN z2HZjhj#+Z;<~^J`NPOA^@2h`2nYco;2wdToZKa=_f-0(Xixc~WE$u(I`y5A zb^1!q%UsLqK{V@=r!OvDy`6sO^sGhOIwj4h(P&VaFS>E3?KSGlD}o+FQSd}PbnN^G zl7m!y!+j&vokBne2mv8b>Jhko_fd!5Q-5EngG~}@H5;0G=v2^T8qkjyFLLp|ICkRF ztVLV#6eW#0))w-M+CL9^0NMDwe*X>I4?ch4zk6(HMOb{JwAQTNO9%)7As_@IK;XvB z`wiQTv13yHRIN*4ylVC{$D#;;eUbB$Sl4;Wc6J>w>+2>%KK{JxZv%Wh(1CpNW%o8c zr|dg;>O*kbuyGULu%Xa_5D)@FKnMtd2M?bN8^5${jc)Ap`uoZqTXmb1dGb<0L3n%0 z-+Pd~@4%^9i??+jIJ-u}f%tgfYx<{Zoy&gNy?N&eGZt()fAM?2(3Mh;y!b|`uVTHR z5D)@FKnS=;fYjy3PF@-^Zb`jXBRlq)wsrTB=g%YD28B46>)+o?&p17MaiM?d#F^_> zZ%R9J{u-%AOMUcfAmHK~ftcuw5D)@FKnQ%u2tYZ|azGVu%wUt0D7itQo#n+#c1wX~ zyvi?#vNZ43i};3j>rRpj0U;m+gn$t63IgIAUa2X`DFlRo5D)@Fz`F>DZ+N%vB)Jd} z0zyCt2m!AkAim+1nv$GCKnMr{As__2i-7osck51)3jrY@1cZPP@CpLr8(yg?$teVc zfDjM@LcqHSh;Mke?j*So5CTF#2nYeMARxZsm70>ALO=)z0U;m+yo-SNhIi{uk_!PL zAOwVf5bz2D;u~J6Dak1Wgn$qb0z$yM2#9ZZx9%jl5D)@FKnMr{uOJ}4;gy<_oI*ed z2mv7=1iXuY_=b1uPLc}&As_^VfDrHs0^%E9sVT`R1cZPP5CTHLy9kJHc(?8(xeyQn zLO=)z0k0q+zTuUclAJ<72nYcoAOyUNfcS=Y>rRpj0U;m+gn$t63IgIAUa2X`DFlRo z5D)@Fz`F>DZ+N%vB)Jd}0zyCt2m!AkAim+1nv$GCKnMr{As__2i-7osck51)3jrY@ z1cZPP@CpLr8(yg?$teVcfDjM@LcqHSh;Mke?j*So5CTF#2nYeMARxZsm70>ALO=)z z0U;m+yo-SNhIi{uk_!PLAOwVf5bz2D;u~J6Dak1Wgn$qb0z$yM2#9ZZx9%jl5D)@F zKnMr{uOJ}4;gy<_oI*ed2mv7=1iXuY_=b1uPLc}&As_^VfDrHs0^%E9sVT`R1cZPP z5CTHLy9kJHc(?8(xeyQnLO=)z0k0q+zTuUclAJ<72nYcoAOyUNfcS=Y>rRpj0U;m+ zgn$t63IgIAUa2X`DFlRo5D)@Fz`F>DZ+N%vB)Jd}0zyCt2m!AkAim+1nv$GCKnMr{ zAs__2i-7osck51)3jrY@1cZPP@CpLr8(yg?$teVcfDjM@LcqHSh;Mke?j*So5CTF# z2nYeMARxZsm70>ALO=)z0U;m+yo-SNhIi{uk_!PLAOwVf5bz2D;u~J6Dak1Wgn$qb z0z$yM2#9ZZx9%jl5D)@FKnMr{uOJ}4;gy<_oI*ed2mv7=1iXuY_=b1uPLc}&As_^V zfDrHs0^%E9sVT`R1cZPP5CTHLy9kJHc(?8(xeyQnLO=)z0k0q+zTuUclAJ<72nYco zAOyUNfcS=Y>rRpj0U;m+gn$t63IgIAUa2X`DFlRo5D)@Fz`F>DZ+N%vB)Jd}0zyCt z2m!AkAim+1nv$GCKnMr{As__2i-7osck51)3jrY@1cZPP@CpLr8(yg?$teVcfDjM@ LLcqHSz&HLs3MyKw literal 402454 zcmeI5dAJqDxv%%lbD#Uy%{lkv=H?;CB*sLeCW_#Q8l#{%&k>CXih>&FC`wRK5y1fg z6^$d}2xt^U#9460SyU8p1eHNlPy|H;A8%=FgV=w*mi+{z+5Qv;6;mG_~X3rlvW+x8Ga7tokR=M+8Jb1VlgtL?A~5 znwoNy8D&KTL_h>YKmY zKm`6^H4Mg&Aa1Vlgtr0uE$A|L`HAOa$gF9Oo`e3hqiBLX5I0wN#+(stDW z5fA|p5CIX$7XfK|zRFX%5djep0TB=ZX}jux2#A0Ph=2&>i-5E}U*)OXh=2%)fCz|y zv|V*T1VlgtL_h@cML^n~ukuuGL_h>YKm*6d67E(Bu{Y5fA|pXg~sWtnJa#m_FmXrk~G6-ub)uie<%m zDD!rrt9A$#2|tQOS45zV68P-1&vw~mm!_ts?YH0l^2;yhYa7i-X~`ZmXb^dS>Zzv+ z-k#lO!Jy#x7wx=E^K?AaANyU$vtUvXt5@O==x_*rnxtl-KwSN~l#E1334u;Pb|VT8R^ zO53|$5p?YmwA-**;n!^nW{(L+r0*FBP>gey2hV*GO!zn$^m&~!R{=YjvA1wN=v0*9q4N2hZufIP2_~RM9pK-<+D^}3f zZ{;90CTf9BTH;>*=YZnBox2$DPQKR`} z#^st1gB@BV-D&tA?_Sz;*393HTjZ|zj)xm-(Xr8Lgz}q6fC>2xTRyM8`f8%59Q}}8 zv9tTk5uP@j6{cwWy^vMaoz5Tibnx}cthug+w!aeuO}jVC`#YnuCZmD<4S9FfSlw6e zjV3Qc+uL0`-@oYGFRrnHpmEvFnl)>aO*X;SD#^s^haY~JIdkSIr<}6>`s*{^W6idA z@7^!H^wRg=hdaREeDlrNv17N|YAd|q`GN~B_~esMuwmjWt)@e4rd>oz)b3)X9O=z7 zqt>I3KAQBzenJpPJXr|k8Wg15&yJsRa^yf+6eas~*gJOYNKj0q@4D-**IaYW!i5V% zF{T%v@7df|;)HqDS!b{D~T>m;g+hHZ59F&hGQp zTW=+(q{0ma%TmagF=O`Jb5Ek?F7kfji6`=0MCVN?^jBVag9PnK@=55lXNjvViBZ1H+P&#n1 zx|flgA6l&Y(l?40c2oF)(__PnxmZx!*}NVBM{o<(j|F8wR8M1}hfCgl3mM zLfiLm_IY~QLw8~yG=5do%<~`KC73=wupg%dD#X0TC9pMnMdLA`^|X9mxZ65J7= zcIWKn!7*2?&R49@``&NPd(%42;cV2dIoMBM4#!)@_gBA+5q32E&(nhcJ^cNj41DuH zFP-E6ZT0xdzdRevSXxGuIl9%Jwvep3{L$FZEZKw3qrCIZJ9p~TiHDUdLx&Fa8z+2T zd+oK>+~8-s?Y6@YW?RFC4dbH!G`FI*FJHcVz<>edf{(K;Beiyg<_fbj%R3GffRxj| zvN~XR<%CNi8OyoD)Y_oUX zq36HqlU{s3`dZ`vglxq`i~IijrQ7UghiN5Fq*jF>W3`AYEDfM1YossRmx&W68XvF_ zpy|vOTWqnz4m*V8h{CdRq(FxZ8FJ>CXIl4@uOEN>u^(G@pV_s2&YU@W?6HRdx1>^? zC{wPSfByM?>=ZiBlwatsiuy+WFTVJqRV{~+T8B@&2o@J+c0_gyJ&3-2`}#>G%mWWR z@V)omb74|g0|yQ?KQ3N_Pd44-wG}tOAAR&uN+zx{Tn ziB%(i6nU*`Iy(S(w{(JTF+Vz#qDQ@WBVnq!1bvm|yuk|NQfGsp#D# zb&XvVSsb)4`%NiJ+dJPMd>5X0jENcPOaGX*kKKO_Uk`oWER3C+g5`08*bXg%+_QVL zFiz;b#*IaNc>(!t*KC&OItZ-a51q1V6dh9Rb}gIm#&%y7!|WjF#CW@%cA zdRh~_W*qtbmLd*J*fMQP9kC-Fr#>T>7{J>PUqs2v<0YdP_uuW*YwVFM9 z_6!L%^T46(SZ2{ol!}Spf{WM%eS-S*(@!TBe}2^=4LMSZFXYp{KJv&Tw9UPG^?Lg0 zr%5diW=dmy7IiUQ+hc<&Dx0AYTyzgT^pO7(g>}RcM-!2%r{qb<6Ha5!eLtbtFPABX%cM(+l00= z%A%h_2Cul{3e?zT-&)gX3<7rlkiAZxiax(wHmbc8)5 zZqZvZUU5nSpDeeab<96A2@+eovV>qO3-qU^PoM6lHY^!gw4ErfzWQoVFc;&Zi`Dj6 zpV3b5orTqwP|E$FV%;g)j{oe4EbxMvvP6dZ@39GkYKX0QyYIgH zxE_6cVgpIJ_>bq}wEgDKI_%ef(?9MI`s=XAN$p3?3kf@44|^gdhE+e6tnCk>;Z4CY z2rp~m-skWZBY7LH@76LUK7E+?b1_aQup_$%OT7+4bQRsSeZNRAz&a+e+HQyKe3Y;c zzj?;KW6*&BBNG$NmV)f$kNc^Z%;A@<>`tzu4h-oSy8DamxLI$<=i{r}>msAfm-iHL zNKqj-=%V#99u`ihr_N8&1|ucd^3f(W&(V+z$`SU0Ht9fX6#7IPr|g+3=+iueV)VcI zkW-2;nq{+)cgyTnG{c7vFQ`1xph8y)!ZiPEs>i0v?5oHT+J57WH#%hwg_-`97|%QJ zJUU-K8FPmeGO0>f_I=^a?lW4eV^eG1qA7G&Tvw>5a&&Q}YkPJ?7GS|lSt4EHqYn36 z7)b(jNi~Nh*m(>6n(^z(AA+s!32Xbtw=L_~sT-=^ahGE^8T@$r5!3nGk)VDb?3(B3APto?R9$SGS-On!nFsk`n+5hF>n+)qMYoN&E z7ki*tWMi5=l)n@eLJepXdAQx&#s+~4wB6E> z1(BcHluTJ7G1lPO59O#wj~-;l-D@OWbVj8x|Gt4#!;A zvE%OTuXro^6X)2af6CPM(8zXZ%Nn&ak7qfvsdw`bclng`R22C2&Ci3e_cojH+21iO z>-nvv?WDD-Wx76T%wHfgtAGA#W#YKK;Ced-_6`1-J$tqrnjU%Nk)fqmH}URTAcxB> z54xX<)pph)Uw(Ow37yiKHZ;X#Kqqg6?rY#*| zJ&D9&vhEF)-4wb%3GYwQ$ETq9t4VY6eqt=tlE>|h?sk@r7krMpOO<8Y>4|H;bNOMw>+Uo#)&=<;7|{ zEdh(A?slRx!y_)z@)chTR^3r;ZI23qMO;B`cLVIuY&qp+rj7n^$gl&GuGykRiySwM z%(#eoHulnXku`R%U_e3N!Fh|dd2+vIccg2(v)QhcS$P&wkVl3-i<9^0LY2*oxJ3|`Y+D@hO;KIpGNg9_I{!(I60|)Qk%eDS+a0t} zIhySTG)RvHWf_bfZCnv;e{8`jZQtjDX*V1)XiBdO?>un8q(jafe8h;(qdtmCdZ(K{ zIs3@VA3W^*2?q_B((8g-4jFXNz=zG-_;4R3Ogf{sGxiQ05pP3u-=u5;#`8_#HR?$% z7o(~hPDe4{Z*JM{R@HGk$uVpHhx&$7W}EGzh6Z7OnZDmLFJ9Y`^#2<9A@cqoBWC+c z?yR>X?2oQ)2Q$TzKToF5NHh>~dfc1Xe#Lul-Ys%V{a52lR=V1akz@aoEIA11I-9Z~yb3^yPhz;V)0>ao&J!yYI2~ z*5-4sb+)--?^7;1?BY$wExUhifh1(qcDy0)QwOgKZ8m1)EnD2Cp1C@Fvz!~f`|2yW z++aS*B7F_tkuNiX;Jzz@<(|17&wq!OOKi??F69g(D+K&faIm{PWbS!gz*%l-xH0F5gNvyUC4K_Y*=(ENYSt8v3u z7n&pB1{>}tbJ!SzoZ68ic6<$A8P~ZpPuxKwb|8u6#gCe_S!mgPntx`7$qUwIbWG^= z9DMM>1n#T7d2`q~z0CZR5`*CP0zy`Fb}#?B;bLfxzm|#1POq?ke5b<2N z)12%XBrg`Y{Tn*F27P89JISLQPd)Wi&H}PC1$?!)>@bUju#*?}P*?$RrQ|}lkl$Op zg5mlZ+Z=3K?f-k&pLRycx431o$@^yGmfqcC@X;Oi^!=Fogw6K7t;e8e=d7`*#}$Ng zWYqR6_YXR^Y#`@sHcoM|bK2M(?rhgWR&*|W9H+PJmMhJo&ZgfF;ph1}&epptMQ${&Rm$ z+vz{Q#(rEgmffdIBnN;nLu)M}|8knGKVmm;hTUS}SC)2ZbZL4IKm2e8|KAUkv#Q#**ZLjdaL3;$z(k{^c}e&Qu9i zA>df8c9o6Tsmy2;MeGNj-KS-o%ra_qN8eIL7hQA_!*V}N+&n4tyzF?~q{qkI!qY)F zgqlVoV?EpB<1_p}p7G{bp12r?Cnh5xr)8Zr8GD%v0mo#Kc~lz92YlRM3eIMT@Dty&~S< z631N`wcYg;EU4(e{ye`WX2$0MrhE48TE_4kdOM?B^Y~~k=Y12L{?;1uzIn^JbZd={ zKbP+1H4ZuuDCKEK~K$!FJJ zZ+>r&bHDvMqPAYjvTM6{Qy!e@``cS1hhyijA@3XAv+Tb{e$eTO<_+!s->~W_IIq9)O}#A&%Ou!eZUc?@Y8jBoiuam>VpZR#Vu`*GHJal<3CT^Ra~x;&HY!!MYH)rvGnttB`7gL&P1Rpk zwFF4pD_9WNd$Ekn(yNcXg5fKuC;`?uSf;_A4~xlY^^W>4c%@Bf`-}&kzIM-(qKZB4 zUpJCLmPr2EapxQM>Dy<>>&}DDjQSjU%0NSL!aj!&?|SspH?DE2e~6N_Jp`mx zzcL`-D{{j8qQ=&9S0K)2E=j#vpkq9bJVuq@1yaur8ay)*Ckt3FVGqO-pTB0vlD-|g z5j{VooP4pg$j)sn-rOp8QfS$ICWTOM*RjVk=1jMu5A~M3yr#!qX9V-4mpB%iaaPgU z3yXDNu{UP-U;do@JJVjlJU*(}OBOd9i!YqFVAtPo^Y3nFJbmPF{wDnGtf2FwVA3ZJT+`Ce*d`SUZ>`%wN5gxj8e4RcGLICl^)Q>Tw zS@7`h{`>Fm#*;QUp+$6`wz~jPKLv_i8l5SOrJ}DMsGmgUEG5orrhotb)cH1%yYjXD z`<36{+jCI2^|lX*_BBH;d+?5Xx^2GeAsg=WaIcF-|MPbK9z9~{zQ6l($mazoo%QHF z5B2GK(2l>_d}8-==1iZJg05k;J%vfD{?u<)Sli#Mz`L$mHA{+I1nQf>(xppT=BV#9 z<}Gzh!?A0_?eNcA_7d_l(@#XI4z>>Zx`6cSm_ifJP{B9 z5fFju5cu@{xl>1un{@i+x1Ba}&{3D4)n_Ds1CG4>h<@X@x^bZiyZzhws&`K~@kaB& zzXOjPIi~N(N&QFOckVTBJsy6&Wi+wU_9&B9y)xkK@VH&Cb8XcEQRE^Z0wPcq0-t^p z41OipY*K+k<~vLb&U`7DSLDo+w7n{2R(hb57OtV~hrd>OP`XnDL_h>Ypw0;_`X;#b zy`axi0UGX)+i~-r_R((#9~Y_WmS1Umos~PMNcMemmArR-KA5qz&eEskh=2%)fCyB9 z0B?6k#$W$Dcx`bo|Lb5yc?X$D+pADS^pf`SK`I0h5CIWrL;}+GMl5yZ zSp-Bt1VkXu1f=bGE?wnK1VlgtM4%A~NZT8+)Rkuu5CIVofjkqCw&%HYl{XO(0TB>^ zMkF9@Z^Tkpo<%?eL_h@cOhDS6=h9W)L_h>YKm;0*fV904OI>*u0TB=Z5y&$EX?vba zS9ucw5fA|pXhZ_i_C_pq`skhbT!bd@&|5CIVofkq@CZEwU&$EL_h>YAkPG(?RhR;5NQdgcuKmYpb-g3+Z(aem1hwU0TB>^JQI+%=ecy1HxUp45fFh! zBp_{X#8OwDML+~ZKm_tkK-!+?(pBC>KmI zc@qH<5CIWrL;}+GMl5yZSp-Bt1VkXu1f=bGE?wnK1VlgtM4%A~NZT8+)Rkuu5CIVo zfjkqCw&%HYl{XO(0TB>^MkF9@Z^Tkpo<%?eL_h@cOhDS6=h9W)L_h>YKm;0*fV904 zOI>*u0TB=Z5y&$EX?vbaS9ucw5fA|pXhZ_i_C_pq`skhbT!bd@&|5CIVofkq@CZEwU&$E zL_h>YAkPG(?RhTUHjuZKD_4I0`R5;g_~AS6yz}a-ufF{9%P+n3692yO#v8L|&;In& zPrv^9>mPpjp{Sg!Sg~T!qD9>P$}6uB8lTr*dyVkt&!10dNkJ`NzI?%g1#i9emP^B% zZ@&4#2Olh5y0q8?Bt=mt*U8RTUws7)GCO_xbVD?A=FIose}D1f#n4Mi=NDgm0g%^U zf87vKUPkqsZ@x*oC3^k4@4lmSh-=1-85Ry{Fx1q9@4x>(dP}9Qka0?L?%cUV=Q2+A zXU&>rm5q!PTh{ph^2;v?^S$@pb2%bR<4FZBALj;6o4{?|%bImo=rcGP8aAAt(xQOT} z&`lt=9s_y z^iKc*a^joy;+f|S5ZS>SWZlqr;sU$T~Qq9$$h zN(lUtOD-WIO4enZ?Em@Cf2Ovadg`fQdG^_7>3Wa=2QAh?EK8Owp;JJ)P(uzs{O~>Y z*khMncInZh$5BTe^|!zM4Yv#P$tR!u=%bHFgF_k{rY?#=1qn#oD+seSf}(+;b-D7& zD`^+cKKtxbPC2D}_wERz36wS4S^nK(i!IJN>#WN!zkK-c;pd!l4sJgG{O3OpJM6IS zw%cxl4K_e;vxMXPFm#FKfkZQ6M6dey@4x%*yZ_-2f3ODL-57G9u{-Rr!)d3TMm9hB z)J7X^M7s+vw1@#DDWr2m$h~^?La9Rj-Bwy^U<`Vh}?}h;08d_kE$@1n>TOX9e3Qp?cKU{b6pSLf5?sQK?zouUV14a zhCIen&2kYrBKA?EM)|#-Xmnd`wbe-{orF{(acB`A1oMh3uISvkGi4F-Z(k`y08*w5 zyzw7R4BQx~6E&Tt9EV7{S0ksV_+eNgF*KywTI4 z+sN&F$ii*6-9{($+i$;xGkMu^%PlRsZMWU_*kg|!H*Org6@HCH6osZMB2W$iX?r>J z>gira1vEJ{EvOc)2m`95me{q6zGKfl_q28q#bb_m{f<_au^a#et*A4}8?v*f~D_+_R^Jr zE!iZq_-B&hs;jO7dladE#qI?!J-d*qTQYbY1`ZrZ(I-6)Bx&odw;nurFkL75hIB3% zz|;AnGZGbHD$JZYbI|R*_S%c?fMY@*GXOmwZu-3yHB4!P-X5W z8gdAlzKTGZ1f=a{0<6p15jt8~#vy(ynC^Dk9?g(R8Eq}iGi{h_&(Z^oYCEky%_n^X z#-d4q(9qHZGI@@|Fm|G=!VE2)4kl)i*4=j7jd=v-v~9@kl1d8kbI2iwq)0T8($*3n zp6MMhI7H!@B4!w$au<0-oDtYvcioi%EtAp=O-}cdrSCAmT$W0CM4R09Cgs)q8~w05lN(J%$PB(hM-0Ct&+;i0-+Cy!WedLix{LG@&EP^l?PJ#>pw3O)lOc4Sad-BOAM+fwUz(^?A^OJJ&u&v`HA&gRw7&xlrf#LClD+_SVr+@_$fiAoMIW0NM@9n?eb&C%?$hz zM;sB&J00Zn&O47^V<#Fyf#|CUltw_>UK+Q$zl#|~mO#^+M!&(%qU~gwfen?v{GlUu0K|m1X6Hh!5LwcvN%;GX=Pagx*pt88Y zoT>|xb#Dgb>31<`$J);#BJXGy3Qxbl0(tuBr$OOkjJlJwoq-~zd#pZ0Z*f;BK61)r zwM%np4m1RtNV*{@{P~G_1iv4FHX_vNd`K!rWADEEt|g2@X9=1vm=Qw{S%OZV&!=2U z?)#)`JNEqa4jjx_2P-}(c9bf4A2MVJi8t9NJIp>Ddg!6C<;B#@=+UF2-8cHP)YVvk zEahMw!%~9eJqlk}DndZoUJ;D-7YJ6t*y~2e46!X77c*)*8AX&ZiejENUEY0dXKk73 z^z@DfliSE<(iqGEM&22MG8AOM#$>e(GHJz`{7lN4U1zbEVVE0~5+Dl%EaRu&g^3}v z_bzr;IvAlj0W3$`5e=*r)0gYhwacZdpo7^8mWb2mHK;0#RO!F?q0#$D=fkg5GbVKG zF6Pqd{xHRD^CJvpG0RII_G2v%M!(NxL1mfONZ~_4qs%N8q^BRlQ>H5XEIaq(k3UXX z+kyx^N~Uj;GQx5_%P!F@&?CTrGPXNFs_4{U{Xt#w>!gca4iPAmfV90#fc1KN^|YNF z(`GZ<$!vDYIM8W3B9>+H8Hr#Rlck+wsKb&wbH#`=<15m`vT(uiGtE4faDH)R(RP|` zl*iqL8v!Jpb|s6pqg_uu^;ERsXL-v;Rg2YiSOut8SQKq(2F)#s4(p4w;n2@-RNhl52%u#Qd|Dpmjg`QGU4F0h)u&Ihr zAUq~1X&~%h_*BN%4LE8~_R&AKv zA)V#$DO20IooNv|N1>V)`pPVW-!bvoGWEdR5YG{ZN3fg}y3zldqV3FZrF06I`NE#U zw{h?jAh!sVLqOVI4!t_Qx7ylH*0C^SV3RZ~F>Pnb5u^9?*?5{sX6&6{W`v4=HuGbO z%#gTd<90@IHkPwQmZM!I>up9pzBl4x^*BXjD1z8If)ccS{P^+gGtYsx1CTn#oIHJm zq}g~=c&s)s<%k`(W2}*GZOKv*2KhzxYWFhc zt8#3u{6S8vn|;^*-m)z08CJ19i#OtGd2s<(vTDw{l>qxOf%~HoW(2m0+(rdeZ6@g+2 zNZX4g)<*o-M%#hGn2_B((fMAqon1j$?3vIU-xj?Dz)Wef#+!bO3>%ebX#L60EbVSc z+e2w9N4rYX_H^5fqRu(4sop&IIq7XP%ipoTh2yj2&h^ z%OOe{IB11)LXsB$iG`i&902YgFw#)kPN#-*U9kyEnOi3rh}Rj z+i7wa%hYzl;qV{ZHCWD5pnFBYCm?P2Y2?UVGi`?%%@X#&p{Yx>ovC0>Tra5YyfuZD z@G{vmN5EDyjtxtacQlQ&M_8BXqXWJJI zw4LqEynHKt9+=k7B)5E!3^=jk!Ym*8Vs$+lFKg7yX=Ar!W>1Z#?GUCH#%X*^vak-q zYfM68c$VBb`2EpGALZaZQz~hDmZKTyQMw}!Le)5*ChR&{W5#ea->+KoG?YuLW<9A}m?K}l6IYps`u1MScY9n_=2uRy2 zg0cPrslB%If)|b-cZaCbs_}9!gtXwCJi<%c#%yrt!vr#>c)V>h>BE7Z?&xyA1ZZWk zW@nb39b=p>#tu2WJ@CK-nDk>Bh21#srRUu;y!R&ky=XMR`O|g-g~G#!&J=wdw$r`x z$}5}^fJGPYibL~RWM)%0xUjAZsZjK5zO|j>5|dVW9Ez0nc6vATm7LEc2enai^8O<% zcliXQ?d3D9%Mfa>?O@<2Sl;(yGxKOW%@v1r7Caja0bvNuSUU9K6qNKa4~Fr)%MFe4 zOMpmOR7a_J0|_6FvS%?L1w+S7^AUVTSsa7MdV%YSBsIGE({^S$*fPk``W&}nh%klZ zct5b%hC=4;S+-y@nYj;6TuUP3uIE_WsY~nuaqnPvSq?c;v^~puJ1Zj`UlXdvewCJ6 z1WF(vZ7%^@TeziFw4Jt)QJ?J@Lfg?&#@+>+M&|8fmn%^i-d-MRNByrHWy|(sQzXiS zu_)oN1Dv)N!#<{$`LOWLY&>(zEEzD5U@Pr-<}Qv;E4aNWXWGt*0KCtPGirEMJ7f$I zU8JsEyD~X~$h)`eQg(ERc)OktJl36KZAWjZPEd-?xVxC5?OAL(sH;<^Olb>^iqhDY z2uR!8QfU>D)>hGW1c9|~4x(cyg0_=fhT;Xsek_T{zKg4%ws+~$g^lrU$(;jX(eR`h zR9a|WyM@gki8PK`+TD87c233Pt*`WkvVTw~){V(B-5FjupR^5*BHMlU-8t&d$vd|Y zi&L;9M~=0fs>0Mp?9ogLiX5xyNEk!4_vyoW3+d`0SCDEY%r6|+hfv)SlH6>l2*6Jt1W7KIkk)` z!RdV|Wx-D%eeJc^T=%EJwH?~5@AT@`E8QNHcir(qSl7q&%ZR0)bbC##Q3ehi7&_|L z4?%7bD2;%$y)vwkR89Q=mLp3aNf$!#_5or`(I1bc9!uu7-!LPI(U;=LNCz zGUVU?%7RhsyWg#f>R%BknSivtWOVg?V{2(URM;JDJE)A%!i5W&bx%=Uwh&>;9>tkH zZfBK}MiC1+yODieOvtCiVht)oEEb&YmMq%7{r21QKAdRU>`FO%ys%9eFknEsF(3UG z-lAhO>PczHejQv)FZ;q0>t<^Mh6xsI7Hwy9g!3OtOgVhA>_3Zrcb%ny+sk~%tIG?v zn3#K}%y*<{J99}X$J$X{c~J~TB5tC@MJk5~lu1C^UM9eLy}cE+J&J@8Bk#dXY8_bt z#=t&$7u(mEB97G`M&Nz=^kKr^-G!MqCSnC`@{84WCb45}0W97u+C?9Po=ddx&Z1q& z0`G65ujH~>j)P7OyBK15`WK7Rb_#-Fty|^@B`*sfhP7Jt} z2HU)bJ&Kb<=CM+W`X>;~yfJdJ7m3=9G?46vOP~K_bKa3h9+`bkp0!Xm!zT?&i8qUO zk-NL@x(joFPzG6IWg$1cGs5$oE;@Qa@EOvFw4K`tlyJUndT)!+lC+(^ z4~G#am8K=5X5)4;$c{j^31W^JrH7FM$0)gauo>Y+?cTXUAgtj>*>ej!w6V;K-3Et@ zbMBoV3yo{^)wE8#FrOkKXR8;Djw@NTiycnPS#VH{GYzny81AO@EI@?v$DXd+oIs2io`pc+Bb8Y~&+ESo-(x?~i$CBboe+9RvF}VxP~BYsOb0 zyE;zDV@=-qM3G|OEl;Yr5t}o1CZ&v-=|?cpFnsv%bPH;Ps7H?;2s_;hCh(aRXLLt0 z=!0NN;OEYlEXIMzCWqwuiw-X3WjY9x!(=G}rr&*yqSM3)D!x!N4?@SpPnfy63qt_9 z9vCCK*?T`#$RK?9Y0#iS8*H#aGz9-jNZajRlEH~?bOU{#QFln&>A0~9z_v3!Owe%f zPN)tEpNm~+U~--{3!~>(U~Ddlnp`^$RF8=hCsJcwq;R7zdC)-z zu{a;<=()S(5P?b&khWKfWSxampV|&2+B_`hFcD{Rn5NEJUv!3PdD>=LM?Ne<(zG+Y zG4VkI*+s_?h>AG_VPrfj8y=1=Ry>$0(4aZ^<&&euD=O<}`cGfr}M(#0sq=0nGMS zulXlrOt^*&8N!jim;*4)flT2*+p&tXT;m6cgNBnP93&5Ks5%`bEc2o%1TUR3Y~whx zmLf=*|98PUZ6|7`V>k|&xdYB%wJU4P#vJ( zLGIXp$tLLwQh@v3~~ek%+9c`8#{I^17?5xTrjhxd04 z7S-840B4fNxpWL!5m??E!*VwXV~Eblyv&0zlaD1L{yCM1dt*C3tT1C4PL}DOP_hJ@ z4u@YEIa6230^?p5K~6pOR1EmInB`vhvyXtWv=Jb7rX+Z~3#EzdXHj^>nWgV&B1r=f zlE9L8DlpSAyl#kkWfhpYdJdnbQ$`nqr3xmG7_?KhINFfP%&Yb2PbG0nib&T*pkxBl z_L9-n_l@Q`NL6^Q7zPzn?Q;>^MU+t-H<9m+%o zeIk6~KcyhZBl8^@$(T3B`P@a4fL|0?yPfiN>A_*yp@YVlnHd4U0~I?~r^+G4(FBu= zf(2m}n2sBI&OUa^lt`()yjhrjAH5q6XryYf-Ge-qR)PJJl3N6dA|P!q3Rm0lT>skM zc33K?2}#UTWOlwu@G&PbDC2 zPsP)Af0VYj-Lg~4D@cGvc$V=wVgSpwsCAvj?G;3=pz4Z%w7ss1qjHInwpWg<d8_ zu%)+Ck3-gV()KoAw8}sN0cm>zn6`dd+TPYnQ0cEM0puNPc6O@yqjzb0Wg#oH`XL}~ zub;B0XiB8*6~(E*@<4!{ZLGcfrghTxJd~^Q5Jy1T9!Dhy*NWA44$b1F>jigr=YWi| z(69tpd&jg6J?Bgw*~vF-HE58GOWSi=(8X#yr=W5ath7C+)j`=>O@Pyo=*il`yTz$9eA@l`m~?#Nuy^ zJWJd2Sk9~~PMbE3_f+{N!70MdPrR#y!3@W7=aGl3Z(}$_W3&6HjC&pP@T}@F6r8vK%5H0wN#+ zZHR!hy$uysLQ+{jWbCnE!Gf7HXY!gcmd%F^8^)U@L&tRZN*?Rxy;;0tocDq8=BgPp zX7G+n!esVR6ZHw;by);NKm_WPfV90%3#N! + +

Type **"auto 👍"** to see whether auto is set up. @@ -6,7 +8,9 @@ Type **"auto 👍"** to see whether auto is set up. Lean-auto is an interface between Lean and automated theorem provers, based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean. Lean-auto is still under development, but it's already able to solve nontrivial problems. For example the first part of the "snake lemma" in category theory can be solved by a direct invocation to ``auto`` (and the second part can also be partly automated): -drawing +

+ drawing +

## Usage * ``auto [,*] u[,*] d[,*]``