ࡱ> nz,s(ݚTDS PNG  IHDR&x pHYs/tEXtSoftwareAFPL Ghostscript 7.04c(IDATxM`<(;dc,Y pPl*mOB?ClwyqGOKs6 moi}K;6ܫ--hZ~'}G{VSni%[+Xv =C=C=C=C=C=C=C=CƯ|WZ]@U+V-}S^y_Vm^Z}z衇z衇zE͖Mk5?Ɔ6K@t6%[ p+)V"^Xorn4Zk }Ե䰲t?q=jvG|06}S*&:V OEHCUU^1 A֠e:WqK_?\Ѧ]я B %=7")a!;1udTceRI;:{l%fkR`d)Yv6^68RqxU6Іi~ $o<-:;s6hVmYGօ_itkșn9!g9L73-5En9ծ9Tl~ۢCN1T莐/HZth!'Zv L{BuOȣa-Zw<ꞐG5{B:_v|GEw 9jQQt_A{-tt_At_W\<ΐF@뾐򠻺%н!_@Ww]uK`lZr}=ߔ>]mS=hsKT_.VCJl9յEg|iYz1߄nIENDB``!9*0Z0;2% $z'A$9xKIv#;{\b4 C"FEÀm(t {i/,ގ,e !V h0P`006 @oSzDa0[Je<##﫪lKrzܛ͌8'+NT猩01_y`͹I}_g;?>ÿG~[RE_}L?u;ߣwWgꃟkDo1?]|>`~_?Eoy튮^Uɵ)?S_}e=kg¿w5k/]Kw_?=bYܫ{?Ϳ7[{,i?%2Hc#x?}ϫ8~~d|b<*OƟO#C{GLxcN81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81N81NW.cJ]g )V #PE8%Ftz̥20~ i4#w'bTx`мa9 Wx _QF| 2hQ?7 0$ɽAɌ w;Y&6o0]\j`bx](뮣~)k\ʩy3 [W0b1/70 T2ݛ`0MݎC W껛70gqPbҽ>ؠ!N0F!_7}SΪB'9H,o/1$w1#%0FiCcޖ/;"`;Ő'ɗ23FU/Q V)v)S](3]`g_י_].!0|S¾ʂϾ5a;hUG-Pd.u@м6chW?N@~pa76O-HNZ7Au ud)ou4śe_aAz'(/w<`V;^(<x'$c]$ϱq1/j` Ëzhd&Jn)%~aa\5°Ġ zD_|ČI%5C߶ҟȊ̀I<|aQ ?ҳB(Ls73fd3FXZ a J"ux޼!pxFaG- Wܣeؚm/6emHngrH%W_AooA`mq=e8}9>8nZq{;粃)/}p\a%pOFlZh Lwa=1pȰٜ,ܓ`'s+`:PH=8?n ˄̂&JKjKLvaAsl9;:k"`-9@{gauҌ8::8#kZ _-X/&\fx2;GDԀcG YK䤱3A V3x4z3>:ubF;aݺ{1`|űNW],s{1bhW u~\ 4E4 "UR2e0 F32#HU*u܍AeU- ɒ5QH5 cXζ0Fsib.ƏPAhJ]p C@h#N@q" wcR_$T0H۩LPz8<ÖV'-^2.03˜*\E]unc`x< |ٸXOE*3xXMj+ܸU1I>F jW+j gUmXc{3æ>܁AvׁF`F3,LfT& Ψq&mzKpImbeAkBf8'Xr8&b`ʼ2>\%#ţWf#ƴ|ڙ ?v0&m&h;zpCPMc`Dd|'08iNn`xַ1z.LK ɸzAb\2WԔZLguP]:Tq3{3?K{ɋ~7, ?o0Nlp*`%?]pCQ3$."_ڻœ5wWҟ D%!Vŝ}Sǖ z9 -'/`\Z ǧ'#TX-ČN!a:O_Dl\p[Jc2 l)&*v M96-3꡻1(Uq5 NM`  ,\?Ա,!.xNcH)n9[M2)3pGU AVX~ G̋d9gVŒ\HฟU v)Ssi> aE dwc77D6H#xr `H+q0ȭ뛾I<0x 0}|;TKmcg1jH:\2 e*#w5na\Ej%2N1`lpoD+]bQ./orѰ7uXP))æ̌d{u"]J4 ]`3R13M80#Z&ca>;jI? C<%X1U~PUe#`55hlfWQ&9 |Nb-KR>`D ,!n b>XXQWfcR<΀[e{sG+.bPTz4˜U)z׻tAh\Ǯ7ljjK//󾠈,&㭌#dç0Mo&>Όg~% 2hbvl q]¹eQR Q긦:`$Ď%A 1B;ڎ0ipZKe-:OĨP arNL]μ1c4eyq 8=AP FԊn9dKjmP%o243 M>,r^28Ό+TحI%Vs> Xs֨eL>(J7%?yN.6\0)Rc4&M6 ?0ͱH?yuRER03Zu1ֻf53tR44F9d} >Gs]詉q֡+l. 9T99?'-I"Y$أsTQGRpuT0"3P&qiA2^2>*[ɩy"-l.0U+ЋqutXH1 g'C^S0&e b|NkAw Kh(9 ,R8fNM^mjJ \VJzT-ꔝm0 -ad^8 A)[Q <0dz |J^C`5ꦰp n;\ zTGKQ`ti~ `蕅m3d A5<Bl]ZTn4aNDvM@01TYiYӒB˾]%2j:A3MWîàoTg|1i>Apk!-46?3'o_kC6;bBFMRnd L]0-FP`$\t"Fl kVP`GױuȘ܊&y'gf(dd0} %sAG BXvhwdUՋ ݁ie:lnXPI_5^M,p.Jf< BSZѧHPUB/F0[;e=Ea/w ,AQHUsâYDUZ3eN]g{w>Dj #Ҡ ib@|Hz 6i74x[kZkE'f66il{nO>^F;-ȀOc:o ]Q/^jmn`d ߭5kH*_ n Uʊ&5ga)$= pIl thw] ub2h9 {CuLZs`LQ 0w0^;$-ل/j-0ÀQ||RSG;7FbPoq }Hӓ^wE= FP[˭݈OC1`Bg@r`n~ fc2 $fb֚*<WTmcUFN%Qqo3Q;ϩS 2#bb#ئe vU=MFU`Hp.(ڬ^3 $20hx7rF GjR_|1 @QE`tU|hѷ7ZFvCĀ44VJu7>Z}%"r$9.-XeE`%&pK}vf`NO&-1eƀ(Z#eiq%&#SAA:Qe*v $+`+1E`>Ȍkc 83 lI5ȕ.!"*# k;0"CJ̘l$e0e9gFq)yA/.Sbf5CVRڳ5Z+-{ETCQ)ЈKuVC PZ~nx"hB72ШZ[ԄflPT[/N_3Q&QGKdxԗ(l^Rid<t6lAeDxnӫU@aId} znihefjCvcؒ˒1q܎k'`)\*l缈`hdi,fF|Nn0c$ )\[:BC|*sМeh}R0_"d:DFG` F$0tlshv1ֺ4j-K 3kWeF%F2ж\+ 4h63b7[d2`LeEvȈXje]6(xދ x[w`weAmj CRA %*ce [*~R'b܈!;VUR+gxqS-wg Āφsw.6yf91ZѠ"^b `*hd2cT8MFd njH*J$m X)QDM9VʠZ7-Q 1^nr$ k;I m%U#+#TәݼO.{dm4 T,0Fa`{"I4-B8nEQQoypaha4 ᥩX+bKF0f[d .HzPdS^%?5^;',BȅQ]0ENsk'a F1k PQ@d`H|lt'AHŌ9u${uwv&wi 1D;&Kى0Y;/$O݂4YL'jH >R8{bumJh6:*ɡBRa7QB?#m2MIH{]S@^VVfWߵO./r~^|q'-vS_!pE݊dgEUh 3.-ok rN=mڋ..,NлdP pnNn㕘 9K} o0&dLu1Ʋ@Ŝ87M;.bc\/y QxeF3m}c/ܐ7zê0A,7Ƒr∯h/UQ7h}ESLQ1 FMMVW)J֬3lc؂1JBFkC>LECT9 }%6Pؿ; X%;/.ASɩ4>v PR φGJQnkVWbڔAu՘1j/GHUlp_kV+;MEQ};و^kQg38Gb 2GN7Y=AX5UMz稪ݷ- f 6"_͌d=}&UD<7ͺ BVWA') yt m+C߯G`Hm1م}/Eaי,s|wV2< t%넏! `L  k 2 3m dx |93aAdXW`;bc]fTwnN2wkca b^2$?`D>-^]ra[`Ki,;}ܝ65;3_~ F2zx|,7˂1lg y' #fm:/nS1xR21qgI`2-{Y4y$ud99plfE P0氽[g5/Դ!Gg]ۇpd8*H)lbX2sdf|'nY`>e߇ X1>|˹"z9H Đ`]du %PQ 0 ÌIy:#g‡2zTvwc oJ9*hpbC6,7j SzNvԔ #BK-e-kTZ>+ZtReAU|bRᎀu)J { ¬+(2/ Y%Ky 8]f+,ݦ;Bb, mNW#Șhգ:0i6q/G7_1^>d Ff6EN2w)FxlyCfCL1C2̀ sͥ 30ھ`}JTBfhS 2  ǝz%ѻ}hKFB2 18S'=Q fk"jqj(xhǩlg#犰˥wTfm2:SssLs0Ak 7h(q #R' ՠ`7jr3!K*gN0w;,sdJʅlgu\y%.NMXvCIq!X'>k4YG>Z؆p6V{Wlssl#`DVpՖ5JK&zIϞ'3N!VWJ1QV2k&fF/5fns_IS03ja*zF̾2ۙPq`3j-k$QF! :߽Ʌ~`h֔/vd47PcqRd~#30o QnYm0jEtZSȸ,,ю1 2'!QkYkq6?h>1YaP55 H鷁|t0`#ddnHAjdKY 6Wy%eH?5a*JGdX5A4N'mY?Ogpܫ {֏oq&7|V da?OV= D y6"C –6r0c ]j.4x`-ȹna:JFY2UI.axqV n~(VAS0(Dh@ 28bh_ijLčNg^^\VLKnJþ3Za}Gx3ʂaTiƒ] qtqWc;-ŹtGeƋYg,rXrr~qn%1:9dP#K>$S "FOKd`Q$}-wHmd8-jalLԙ SC AP#+p*9A gEsmdH.L]`-0Z:CpSfgp/>xBJVR㵕ȢV뙱ȥw "BjeFh° ]V1ZĐB(( mȇMF(szL_e0*Y3è Vu9u|NaVuxWհfB[$~k]ao7f(v1ڽ ܌lUJjt(-9y۬KxHၣ|t.agdlrM4@ ,gdaB"AƤ/1mqkiŒÓifw3 9d&r٫)S^o )h̀_͖v=m{o_Ƞg%֨u> ÌUG20AVӢdpˌ~1D0)հc/ ڕ:oJ6},7rEŌbn$R{: ~ށ2n0Pa}1#CMqQ)L<,ZaQf&xő`s K0:3tZ`OCA' 0Di$O ݅uPm6åUfF)D n<} OjfƢdyl"9廱"zp̬-59gp_jKU2MFn3Иy0VF_6| ?a1UsylA) s^MDd>l ),t`Ͱ&k&eCg#FU2̹VըgbN;30q02JO3#ɉYkdtZۂUݰ,wˌ -T뛂1'S+ALC6F-Y2fOk4u GA}V#mz"FVX2HƘcՒʗEl2Ga)+˒O4 6܍h2[YJTҾb2eFx]ΩJK֛V 9`hAt"=9e KHȆIĞ&^Dm}—Α\c`z;0_z:5xoja a1 AxĐ=ȣ ';3G~<#Dh/9X<1oX3koyDy>y2¡[0PL2EO8BngDNzqTT4-^ c GGn3.btס"jxl2Ue8 ;]ZW6R5#qCKlex(tr mr/0/idsuUȱWO ;adϙT([fwQ=It j11$JNH͍EV)vhۏq`50\fPdzj\1fz`F"\xq8;^-rt|!4Usz2 ?Ub_*~=!͌Kd`kF>1ghΒ0dL5acpԒ&jh_Fbx΍/yΟK9״F1W&yI RG5hͯw.=m2?zv੽| 3Tퟂ@&,Wy ѣIngzfGkť0uz"<593аvNTdc~VU:dt9QKIdCl;p Lu 7ufdFM͐tX8F܇hIyϷ3^䓑͚*9cޒj(_co'i2'uP_Mҟ?܁a0qb38W͌`4 R ;1\Gb|CK{(9ЫAQ-xtŚ7\vdnrM;O-2WY=G0lJV6oaߤV焫Kx^ì/S DW!O"%=1TO*q /|4ͥt$Kɧ깯/3S;,y?o+nμSqSߴ1p!uE^ɺWS>x!)[r|/Ë*x8jj^k!ga5C?UiÁ,,)+}l6vspVIMNR4' c5Q)fLlR8-uvڣKA.Qhw TcLף V9oo4 $i/# oYQثhS{3, #ylQX w-*Ac6' =b;B>r)dtsEQm~#[q %PUI>Fړ*j|u 2i?k]dXf`͏AmI#ߦ89wmǸo]9ZQk&j2 ˅j`v.853b(%6ľAL<0H'tP#aaJHǠaDރ-_(g1򱥭ASyB`<[}FFkHhgF5`ժ)K0<6>E8e0Z' USRvM0s 4Sb3oу?gx;cS%ߝoCiSJ60HJmE`f<>n41#HNU>F+ +񇤣(Vb P$~kȣ~9:W>##]W%nsͭ]0z0FCQ;(a& rlR`<ݯb YzfU'j.羊rȗIC1h-mOnc;mUd_q'vFKBHԒ7~ɲ]fU&|53m N8G!M T\H6^[ PjQk zj^oUKg,Rt6UU'bZ:^-+lYϤѾ S+G¨q,lj^os?|<״\ͧWw78~"_N[Yy;mo鏄'cE|j}A WBaX?Ӑ"80} }ք zM{k{+ݍoP] HtN6ʆTco"wcqO/]]R9V(jS118DsNA)ʘLQp1H SR  NX9QI)M p'|KswrԮArO~WޅAG.4Mr\ tHsҧdC4#=Mbƨe%3ƒs*c*u#6m]6IЌYƗ˓V:6l +ynOĠ9rr.63dԽ3 :.e cɑY1u%O:.*g'ƤOM:6U*kA/ۏwA5 ɯl܄_j2܏A2Â#A˺jѸ<:FdF_099HT̬ {9MA݅J~?hWV`ҽZ" dA cdˬ8{5ڄagFc͈ރ )erRa y2m3î1xuXɑ18F26yLc nou[cH\ߟ} XӔJ[}lsE'%mle,}.mҺ6A3)eФ|S :+-j/ch|oT#[vg_O ߭jKې37fyos*Up#o2Y|B7a ֛UL7amYvrR%s.0>2'@EM}3K<ٛ`47b1Zؚ:UyW|Cz?1|=عƝ~~Ax6),Om}[yo!֧X;7avFH clΪ>h;0Ȗ6FņFDF=z##g-WI8wb-G m5<ܝ1 28GĈ8"M=7GΌPI Eқdk7E2i!zR}ӌJ]ܙ{ͫc܋pF¶,#{2p<Vw$-~ F?tb'Ɖqb'Ɖqb:|+4:s:>Θk>ym˽nL6ABd}SߠPNG  IHDRQb^ pHYs/tEXtSoftwareAFPL Ghostscript 7.04c IDATxK09qq=%Ѓ//K-z'x (S[U$~葙GRSɿ%pEGVm1'V|t]2+CNjYR?ʕHRB ˊE,YQt.r9ԯ'~*r3JQ|<5>&[,JNMHޥl,dԤ捇&U!U_4o<Jz|4o<*Ty5&u9OZKCӼTh2Y4CCDR=s7RY>IǃVYOT捇T̺_[-W8ɬu_#0*䱈ȊGo&7RqĪ̭IU<kxJ J""+uo+ .OfSF,inMv2y)$GdyYא/+RVܺޱ u4ʝ̊k{QnC ~](y)XɮU4R!2ɱjb;hf<wFYlaoV3gMɬԐ4cӟP恽79V\e7kwϰ6 + W ;H@jRI9XR Y cŝ%>oסn@V[,X$ .Hg-WXq5u( JXVCXq3g2ߤܙ"QDVܴ`C8?jmPx?7 B̕ W}[4ZP /+2w3_Xq5,v<ʦA\gE(! t+||ٻ^e%dcP-9VuٻÂĖ^VeZfrY/+[k VJPY,o;$YSM-B͍e8TK7C2*N+mD~o6̟Ri?:VJNs;yJ"Y=+ٰF/x+VCŢd`=iҐP;tX*⼸WJ`Ӹ?C*8Dw}&[>'ll]I%2lJ$9U?WZkSZt\a8Yj;?j,8V咃n>'F XIX /.?s} NyВW58WU*Od `j/]T4s'pvhͭ#2$г0s~ygfHH5wGXZ۳@)e)lOJ郝:Imc_xnM1%V: V_<;s `-wv˥d&W߱dX)ago,Cgb:*VܚLLNxJ2ŦZzYY r^XY+vfe&yV^+q^mn_׊{BCRԴ)BX,WGl\Ibxe]oBƙ-6?۷/+vjIoZ򚿩RѦf~o?Ԓ6/RlYY=₰~ܗZšT' +9@~8OdXOR `ai Ί0ua_1a< +츬8~Bҭ@هߕjvR+СJ;6!V !+}*N}rdS~qҠ#2aXr*z>+кbA=eݫKMB0Ɣb/q=-?=+(vYmY5C`ᶌkab>ڰw5|[ْ:gDD ge\mabXO5+-(4[Q\RNjVJع +MB* J@zy v[TUԬg3+g,5%i^&+唌]@ J.+d;tLǮ:0|p맴X$VMsIYnf0X.DV ұ& +ʖ\#n|Rϭ;p[뒸ވ4+n5J~sIS%m"k>+)9Vn ʬS*&XURfű{A1|xVTQ bZPV E8b)zQ.l(z.iJW$REb,(+ Ê$+YQFIHdݥ])x47YIop(!DpVvBfX[R0-LYA++em ȳ^UQ:M$5[b)J"[.EJ fe.T Vfe%9s2 :-L:P V$i͊7JB"+=m]ˡhYinX|!AsҦ +`nvb°eX鐬CJela{ѩ.Ȼ\T|OV* + c`s`eX?t[IUD"e3 {b>Y!Y-LZYJ ;scz){.zs`eX7+p-RV<+[fyh3 ;iV, [y5+ jXI%^ tĖ|0cmZ VBt˄}j`V2fP +P3l.vhņ3p,> >u :P΄} R/+e^Yj9RVTۯ5Yf\gQ<+}E5G"]Lu.uYf\!bϚ#!N@GèJ+s]5+{_V DZۯd N,+YxԵb(=Vڊ>k+ (DTg͕^V,ųeNʰOhZ+bY2@S,bY!ˋsPcae H̳ҽ]'+%ĭSbr!pm±2%?,+VA\@Jsz]waesѥd>L*HV=/+I!XQmҦdYn𭮿!pmSpE@8Vu YƜjYIkcƻYcT tomAǢ= aAX9_9ڴ YqZxX) e=Xk>pS h̩/heF$U "/LkwߡKb/ݛQ4+{14"z fyiXV:ox+XvEV3827} VA?MA@„!4=X9fOlb;>%lV>'M.ɖ<IJ>$y, J67^DVLBoA_V^V,ŲB֑-2VƗE6 +}dc /"3 Fy'eZ/+eR,+9>DgB Jbe+ &`!ü ˊB +OqTL^o$j=L &㗕k qV|_>Ȇ;b5`ezYV`V*eXy۔,BfJyYQ`VJ}YJzY#\d pd%+̧X eŏ'R}^Vleŋra~՗k=0"e\O6dH( +M(VˊeF/++V/ʄs֓e ҡYIlMKQ&­q\opKy^O଴/+(MX_V<)V-JI#Y ): -}eRݿ/+ JX#Q'Ԏ.tt@"ji^)bRwXk^iu" Vj)N1fͱXdM)meI`2Mǝ0/Suu#"V'XDYq,fJa,ˊRLwX W+UF+vN$AwJ>pt6!Yi)xxVnxȦBXQʤ}+V|W:ǚ-1ΞFø + VDÔV Φbs!ހeg}ט @j8 +uV*bVVR5%;+wWNX)8[j95f+^ޚC<S~{U/+uwyL0V^Y="r.9+O`V uq3fa:k4ŎK8ffoKkaJiyVjĕaXniR@u똕-v\V4g{Sl7tǯ+yz=+l<+bG S+*>a/ ;!+Lk l_a& T?@1q&{3 +l}e x:\>rf S֢"b9'Vύ;(V p9վrYzjw^e (BCo@1VFvu+\bX LWȼB j_մVڂYLa/ua} hh ޳)+Ln]l0V{`e*6(SYa v͊h/GEYi'"SwMX9Ks5Jsdv;}ה+l +=D  ++VZ6pZ+ze>rR,;LֆDJy|zee uU0ce+|=7VڨX)ʝ[+6t kM┓ =+W^Z4+L5:qR +l+5r9dų~!YjѬ{J07sV~/t5 ZV~IJR*VjVgb6̎Ya+L݌l׈0׬ 0_Yh0ojQX@vfѰ8~4xa" 4dgs3YTf6k)V~#K݁Y\4)+l#cʩZ` ^ip7,+6ͬp ,r$V丌E׬r 48{n"N07u_V83e(2 K!+\&+07GV`qteŝ41Zu ;BeJ{EI4UOWX:_n +hbY(g^g弬$iX)XMsiYa}+ +VڄX1z{׋h#Vp/~w=+&nbVSa6t3?`9Ί!g񱢸<r18ƊGEŊ6;HVR=1)б™0km/M}g1լC7fEF;S):VUcĴbsϊĪܒ}cJk8r aG2]Vx42+*/XzlVS)ɬx* (X-5GbE?LVH%++Ȋk6B } .+Y17ȊlwBEcaXG~/XhpY"e4eV͊hʊV4FbL ̊YddNjRkX{YNJȆ>+l+?ڲsPVJyx0VV(XQ$+|eEUl+ԊNfT}8;!YopV.wbEs4HV@\[V"ڰŸcmbEqCmY'+IJfEE͊ruVĊ<3½,$y5+Ш3`EY`'X)Xmoz)p.6lqbY}Y]7)he}Q2"V۬X"`WAJKNJ{o,Vkbo ^=|Y) YQ\i/L])[VAR8D+R ,YRtK@VגXj4YrNYȍVbsZB-x4'ek'TMMHYNW4 VF[VZ+GjV7ı۳rgͼH[+:#BR >Zݷb|" Vtb<ԒFt9:İr'+̖rVcCBˊۦ{c87g{ʽW"a4Yǒhl.&H*E7Y>"g]5|KOBXXǒf_̫L+&׺8͕,X VN*%.-6@s4XQeE .mFvYfP4Q=UnXTB=cE|dj*8%akd9|4X9~/VǣCװU'g48,lЧ]fEq`}4{-7c*$cE3@qncAcY)xd]{E9+9FϊzgRw 4k1e7 يԇ쬴YF\;[ x*KNJz56+[#v `]hVsl|$솯[V0)\u[HV^9'+3KYdmPLBҩ?uH7՚#(,@&ۮ ZR$+`'+RtA5ʰECȬX)?)hY9͑DԚx]y}}dH‡齵0o V:[rV"ך.v~֬C+(O:.B?L]IJCY'4vK% JwQ:@1ˊ1^`zV"k3˚Msfe**)'i'tt="0+H \4 VgE0甜pE+LHZiٮEkW0pMUu3/R '9bߓCx`i^Ք.ZwYحP򑇓vV`vg^'zW]VW@_+ʜKVnU׍E+½^+L* smwW7l 6/aJʊMVn Ԗ!br%!YδV,Wd𬨼}gouG:'|۩PB+ ˊNS`E56Qa@RxJ\?+ʱ mhp  ifD{Viur +Ub")+ѵ9M]/VzAB PVJ%~ 8^އ:esVp2 DXq (7Xi6ʆΞOBiVV 5/LVg{ (֬ЇPŒ[l]ka3X/xbw7s`VeJ)V8[\?+JGV3'nf+V*G{mεUV1g Xge'n惕s7m VW2аٸw&Vl3f>8{y A2QrR[ Ӿϊrvkny.+Qbiˊ!:V]V.hXQ.muWV6YJńY^VXQG'ٳɞ+7n惕Ίz'r_OXl:fΕ-+5 RV/+KTgōyCny5{gEcIqȊVZKZ_R*~-ˊBrUABbE#+ygESV\<}6p`hgR'pW8q3femSb ȊfPc~ͷh36^VlbЬxȼX+,+w'+sX)g@VJD~ubЬn^V=o^eRfez+4%YVjϗ!2zPǼ廽n^e%tB6zYK| 0#hX^r@K_VpV.?Ƽ̄FP NXKbeGݫe!c0DJ@ā{-A{Kˊ{<)VV +3AXYlX لId ߔw<+F%:=5"#KYV&99!׎y֐0,KVo^V>V4֪{Y[,+mX V ($?c3KYVIlnftO`c`e㒕7/+ _V{bC aݼ# $+IpjԒ oDN'deHaEW<$+m4)]PHV4X)X-H\\L_YOFҪXi 4+ֱQ> /+ȇHA x.F R+<& VGccE9^°BS.YyY(x칲oc+b1Bƥ/jy~ObJ%+XIۍ*O UR3+5qaePS3{ $d+2D Te] H4'ӲLJm%<+ Q';+T75|}YPV6\l"ըY2#EYqBf/+7!<+CX)" C c%i@&UϱBJEncb`pSV&~uԬPf8EX `?XX2iJcZpV1۞JPxJ4iY)VbwfrA9Nσ0طd,P cQؗa2e~Y0/Y݉jNIV8l"t:/+6 /zOnRVoqKij2=:'eA f 33+Ԅqވ8p/+wfYLuUxV>`nA9Ȅa+'ap9sV0 ɠI%ee 4/+(QvhW BTadVjdcfrB:FJbA'VD+=,1+%J%c23+.fmc VUJq=JUds E~ٗbsTTtYYsY4n+[~L,My4n +pHw6Wr1uw0E'f^&'|b2Ѩ%]5(Yi )Wp&J~Ҳkص2䃕]?‹@򬈆o) VjVԦou{ǝ +,,vŜ9+)[[q_Ls`Z?X4A/+gEž|&(opW0ˆJ3U.3a2Ly۟&/9Rtt^V.X:Ɂҥd55 +'+9̙IK:O˷l͑]+Mr!5+X{9;+9YQEs]Lee;$]JfeI[*)] +\bpY '+W\NcE0h?Xj,bV.f߾ IDATr+N>X᭚ˀ[(V_&t$x_ڳY O`Y+YS6cy*NVjeR)SXDV濿`egˍ;"c蝬TwpQiҳĥ+FʵRG,sbEߕhd ӗ;Xw>9V.7;fqz!KV JNy7=bfȏNbEwbE42lfGRg ް V Ŀl;~V gwXpF >ndX|a] ߜF k7 eNfE˅|e84[62S#Sܹg eX9z'+o̍lUZYٱRȬ42+bG ;2ep^V\Y +c)vf@ rce2dJI.fQΝEr%`!a $/+4| ;.{YԃYQTfN(8sc/X^VQ+)jJj̰RGm#f:Vbn V KiZ"ȟ+!PnԳ}YycE.dfІ:"6rd̰"4ʈYYcU"wB꤫ Y9;oɳ0G yiqJbE!QB"CVN,VBN̎BŊdp<uS\V JI A쬜 XLrce:ͧr P6'V4XaXPbfNSɊŅbglrf/+Ly۸Y;o-+1&-?V 9VJʜƍ;m;9$  p2g$;oa?쑘$ae%Aֳ!䗕R}`dWFܹt{8XdB+P. 5+Rգ:ܹY H_wa<"mTՒE-q3cw<\Y\Yf+:oO^x_j|<$(GL ˕l~Uc?7^]^]з<\1'V| O}2)~2*u÷/r|YQ5 ~uNUJ~|H/+zYy+^V^A>JIENDB`n6g#̳^EHtPNG  IHDRc} pHYs/tEXtSoftwareAFPL Ghostscript 7.04c IDATx0߹sFsf5w;hx*0$EHa4`6.@_{Wlg/s]]$4$$ 'Ih~?˟Bӕe+CR|fVG| 'Ih>I#M7"$BAeAh~$4$$eqHh>IBIReB%4$$ '˲| 4?\BIO|,+B%4$$ '1& O|$4$eL*.$ 'Ih>I1Hh~$4$$UƤ"O|dN*.$ 'Ih>H֤"O|dM*.$ 'Ih>I֤"O|dM*.$ 'Ih>I֤"y7b*p/4RhMИvly/ʲ#a-4y/iy]ɯuRQ?nF.4j9<n̅ͤ7`w4T,4o^oCmoG~?BVޗt 'ec,4o63;TNBnjwۙ}h{yg6G\ijTSO*Rw9 _4gx>fTzN?PC9^ PBӣ^;4;BUONfkkOO*.hfp5DAx`rEЄ8Rh$4F4{5FۨeJ@(aB<4|aJvzK=-"@VTӜ( St `#sU8K=>V@[Ap &@YA27z%Ь'K%4Cgny`> 440zU]$M`IDӘB!4C<U&!j/f=Ҭ(43zTB3Dq;N¥m B3DO2~B3D΃q,UEi4+ٷ:R_p2}+L;ڡyi^Et׆f륩Ot6X_XWn؉jiF+<[pG b/)4rXRg Ϟ`G/i#ӇA ^]A;Ήޥٚ^B3H;"VܵPKRB3@Ѯ$\ރ$4 y]>]"\fIYN/\I׹4^Ф+6*hhRitŻv |]\xW xJKVރhuVSFgAl4۵=V w4_k94;ܭL h/hV˫I4KiI0=:ElDHh؃ .--z0 = p 9H>$oќFT`ës9Rߐ!o)^/ٛ4;6\Nw0hY?f|hĨ%ۧpyݹAz:SE J+ᦾfGgp*ڤ"ܧ0D90|n Ŭ} )Lf}C'9;54M]$oRlH$O"6{46D.\C(W)fM4oE9?!G)MJl@@R7G7h砓7BMld=y 9z_I DP>f-43v1 fCop+ \ʞpC>'a0^hE<&ޜ]hK@h7 OH3*ո4OnC$MǁhVY>\m)`:KhҴG%Fg2,4e])3W54_<4|5B>^Kr~\4^V|I4us)_IN1aYSKXr Mvz)z!$Pjf$i.ӹKtj:(yog5\n΋~,stjf orfBsgYzπ/HKhCsq1Lע pV|ZL*JNYiH Mb&P+MːӅ?JhVK٠s^ ܅t&15h3,eМIC1iԄ&ShZ?8G} .-J?-D!-܅ci:hޛ/[L]KivKLb M b \> 9 I08wFKX뤢nZ>dLs&Xje*@hBicۮ'YdKpp| ͞&ё&jv繓I AOpq|M$45&@ MhGu} $ MZWbkZ%ܡ$Y/uX=(Ъf@&t|MV{Bk&BAgTMwPhciVK׹yC݄,"-gbRdH9CT6 &w`Фr I=:w?HB1 hv|4{yhry M`vA(4YCIO(:o1&5Gqy=7MӬ Ĺna^OL*a4 B@@h~#Mp$&i+c=rߥIlƊ/v[&4?B'ąbݹ&AhI0GLhBi/fN9hOhB]hRf MH't=@9†74땦혉5!olg{& ?~ M z/Z64lzV3=a|*!:Gq}`wCB@chM]'$/Qj݄fM<3hϤW R,?zVUdtkҒˤɽT+if+:-&ARkN.n_&~ .MhVcoxLmxeoB3cvz*淋~,Mw]kDY[Мख़bYz d4̃.h)h)Y}49ܠnA 4K4ke?|vShV̓"\[lAw4G4y&l㞩2aʥgNy<9E#sV%Zѩho,VMY4+hsΣCf?Z49jךPiڧlZ9i `fC+k{.9xtTSYޣKvia[\~:MSf}.mx֢^@sEͩK l״ =fՁm@s~is~٣C։hޤKK2t92P TihzSj]WXhj4;w4SiV"BV:Kb(, R]]L4[%f>4Z=] Q̗qi@ .KsᏏߦqwAQMES]Gsyb,/JD3ԡƯ78Dӡf>^,8&iyoCsn 4ẹ( ͎@iJh4sŠyf~ڹr)a%\S3P(͵i띢D}/4u9۠x\d ref47o~XOaO@gmlu/V ҍEyp%Q(4m ťYO  OmZ-xe&%tڶAaEJCfm7qrKVsB?{߃kSt'@ _߄p^%:=͒/Q< ߾haKNCќ'mNCq$4Y>_HOˢ kiN[6$$5g{i8*<&="\!4gМA4Bs=$D1/f@sLMI4Y4ytKsonB8rV(Nً@f@7۠\ 4y迚gbl.ɾa5M{jفY4K.: v-5[gDnBK{x&}Xgގ7Ru";sBQi=JzIg,}e ^_'E\'M0SZ44i>1&mhz˖f]+t%ͪ0?W<̔=hz fn~ZФ]I6ܥiت&bRQ恂nϔse d'EsffZi&˺i`4A8+(~Q2ww5M俍ppMЃokxCiwѼ4 ߖ&9J .E4yÂcxiy}nm]T$WHj5W.7%Dj썀+hy}!*3"G5z#XIi\JS-O.8fRRT,Y7%u4=JjddIf?Eh7_Bӯhda&no٭M9 + i&M} gH?l sBsVFO&9ZAs!v|@sxNO4{ su@6F\4~he`6|79ܧ PV3T+RPxizM-0^YDhj/8{ zn^M27\_K꧟f5jwlH i/|>ңTTSzBŹLq5[Dpt *JsSktQ]4wOb)n&0Mjs/7`̹4wU6fJSBT7%"4wvDVG~%$4ǭR7Ty#}((퐈-^A揦 qJΛ&_7[Tٜk&NY݌&TjG/FV'*4:~;ۯr&`Phfiv:3Y:B4'7_cbBm#4 ⥩6κ*flt]-*.$MhTڴh9W M?͡~Gк M^%YLZO%4+}|9E-u,4 JNhε9М MnDzh5+4KsSkݼ_˛u~*MR tM_ ,4} M/v٘&4Y\5SɭhZ9JL4$ MV9-4U;ShEs>l>B[h<4@kUG9^كh&qT~O>BpZ]*^zYG,ֿOI]yj'TF\<"siV>H~(({F=k C}8ͥ.Mޭp=J {FBͩSikni$@4i.ԜtK9 *LMsX]C^+IBPhr+5eQv%S҄0Bts*4Yub> 4}(ͪ|mh.gMn%Y ZݗqPh*1Ainf1-4ui|45]o@ д{ ޳){ 4l{Z$ IhBgдώh&CXQif>7&V`kM5m&],4_w'4Ϡi4^`q4 M4VNThB&]Wwj MK-ԝZg"4BЄZݝD&^l&Nͳt MBC݅&bI 4ki.Y44iNjOϠ5:TMSchn74m hf~0͸)'Ь&8V.|94 #;&"4+Dz4iv8 LMTl5s=t̍㈬G`d4qƧJ ь\!7ϥi~#41y]0}3;f%4,|w/ ͍|0hћDV;4Qף841 ͭΡ 'Ip݁f"fMsS@N+4}w|[݃fY$*4;.޶A\4KD@7hqHieꅦOp9ͷG5 )PIs[2}ljY'DJӬz[etۻb wj*h;MGfUF@s@~6M΄'l\(Jh$JB7fiдaY5GN߬Σ麨i*}nrʞ"fNm`%YG\~?OC͚F6hbQi'TwiOSh t6zfy4qbx,bԐh_آi:tnFG%g&(4siz4j:8 $i}O#llG0QBi*i$ji`+J9&i6A~h40Q` .M|2$,4q4'*y4ʇ&uS|4XBm9i}4q@(fsO" +>ٝKs;egH+4ݸQ x kMUOIO<BѬ,nMm" iFvi4MMfitMi6Ƶ &q,MHћSCnpv4kMe7{*~q@?foQ/0k;_{+"M ër.Me4O oJ?chMtiFu?]hD?0ܴ4+ r͜Ьh(i99{3vw0A 9MhߡQ4lޥ&,"i6X}1M5:MߜoI4gYUOYi7aݞqa)p~4^*4}s sg42JNu2M>2( MLNe.fc&OM|vN AfneT IF禹yG94/x@ܼi47~?v]6W&OsfȉFŢ9i7cÇ;tkHDvquc'OsЬs}0RӅXm &gCVIj&Et7M'4/|<(Ogݭ>EDct4yhn:so>ED14me/lJӮ K$TNt~9MA`}%žvY6kYɛD*3D44Y*ZDC@ss~w#l4{t*-}h4s_43hNhPLHj{يN4ںDu}MʞD9h:%:Y:jNivg]d4/wځp+ |)hNih#0?wDineBWD9hN7]0Nu9? >!i򍱽8hnNe4 AYV\ѻ:M-!MiVӿ&@s&_t=b ќ=$oEUDnO4u@wCig]Dciz2wtj@i{;YTyDh5w@SLFwBijGMA48UB & 4=Ωt4f,Z%sXʊL3[st Bw\fwIV44=.fE\KPLS]DӳiT4=44۵_XDQApLBYi.C̎<]>JS9|7s](hʝIٵKJCZo\Mi _MASYMJCӈ_YxT@fGm,M_lbh?j2V~sLdv1ܮWkUdi|}S4G\>~M^^,M_; zgJ? w?&3(ϙT14wdݻx4JW4ke3|/u^Yb{lIK[M^D2lHsLZ:ۘ u1,6i4p#ޝ[A. Mf9kI?[Tr;w~4yA4/D3 YO0&IkL^J18ޟ]K[,da.?EeA b\ѝMNij-ȣhv4U>߆e4E>>@-%h4J}`pVٿO]Z5&di48#iz%9Vٿyӭ!;Ȭ$4kN3וaoyj7 Ls)&Q4siĒo :.-O !\~6ԇj"4 iTMoO\=W{4ݼf4ݮ H_ QQ`KsO%\S, Mu=Ϭ$4Y &/U֩4_KEX>pwCp nF{7hS1x58 3͹ǐl +#͊yp)o,Mi06MypKb3΢u ^iGS%T' UZcrӆy4Y]i7pNKESt;3}`hi1lT4u^͹fwNA4h*h<cЬp4h[giYF!|zK8·5 暭/.|(cהnT~ Gu=fu(Ksl]q5DhCE]LnzT9`nG"`a_=:YTsnCWs .ޣS l羟YQ47cj"\8ܮ)?GԧiihK>)2mQzAc CMGTX'-4@9(wNm "Z#0EED4@,(0QޥO9 鏋iV8_Pڪ܅V1M ˢi.ddݟ,X Ѵ4MON YɼEKClٛgьp ph/ɹ9N㡹,kv6uU{*[uH$]iJFmj5 [g-4/Mcط4Xb-jC͔;8Q"TX]lri_4 5S-"$yr ˪ >M%hD/$PN^.fKYz4;'1i(Mcy\/NG6DhȬ&B1<͆Hu2t=,<4DyiוYrh.;YKӛ(Mpi; MXfetYi*2MmJ*}Vjy"hÅYMMJ*ЧҜ?bhG@,KS9A49G!?.Y/ι^l>4}'4] MCh3C B.&P14is^0M-J*2|/YhN4l&]7 4$SiGSİ4Kbʬ uM_WڢhN*~y$̓t@ӿt[ MPi*B,|G "ME}>&pfi}i,&%4 p_\Ld^D+i֧91|{ThIN-640zV oba^Ф˦ >q~Zի4Q}" j|3354/M搽o7]0W(4t1Ҭ:yvGY4'2^H04KZM搽pAldW!Y2iQB#v} z Mְ9][c!{I9]O1K/qfOɻsW:c7S*4ϔQU,͡}1Z1͎H{WOEڛzCj<'O5,i]ҍp4МZh|>f5hZ["i曃+i4YI>Y4{溡&4 09=g!i6%Z^q4[Tri$Zhk4'|AYhK=4ÂSgRD,pEi枳4ך_~4} MC4g^|paAL𜅥m+X 84؛coрkW{s7I>46_^~B3mhG"fsc&UH4{0S+4YMs}޾^h8MЃ/~:d?q4irMiV M|#4C&47Ih}iM<+4y4&Q1f_"+647`B(pu MYy0L>)4 WGdD M݄]LKФIh&4=6b0MMIT/49ts(&$Ch2>4sH0M1IUIu!ABmJxShRUs,9Jd^2݇[PÛB,%2N0CuDžTm>BiMZɠt?"4]ir;݅&U["&Фjkv MPC(B,F9Gy<L@td M݆H3$kc&L0"4bT"#64!HsФJh2647in~ Tmw48݅&YBAi&p Mh<1`O1D>Ltti&p Mh<1dO1CLttE0My'Fٰ8&]K.f 7Ф-&Vh嶑a4EB,QF3VhFCii?f&Ab#Rps)ܴB3@O.f'4T X96A#qu@ lJY}Fn{I{CF0.RD qIܴB3@N$= yǞ G+)4"hǞ ı'4CI !bYƗc# f2cOh( Ʊ'4Co^q  4 Ż^ ŷi\AB3D}4 h"+Hh)fAi\AB3H e Rl'O<A50fb4QAB3LD ^y 4'UiB3LΠDHA" S @h)}y 4)My 4g0vMMdn 0ŽD TTT%27f,:)4ͩRպ S5)4cpM3)4cp&37fb d U08B3Tg2sSh* 37fMp&ῃC PE9aJh YpÔ n/չ|$4$$ 'Ih>ISQYIENDB`9[(h |  vPicture Word.Picture.80,Microsoft Word Picture/ 0DTimes New Roman0:A 0DComic Sans MSn0:A 0B Dcmsy10ans MSn0:A 0"0DSymbolans MSn0:A 0@DArialans MSn0:A 0"PDmsam10ans MSn0:A 0" A 0(.2  @n?" dd@  @@`` ZR8   '     '  '#0,P8 1 2' 2  *X 0)+B/(+   //# &4b"222 "9 1AF3# %  $M  1-'   "#$$&"38U$ 4M,$#%> N 1 FGH![LMO Q%RSTUVY Z[\Ob$z,s(ݚTDS 2$*0Z0;2% 9b$6ABd}SߠLBb$g#̳^EHt7\ 0e0e     A@  A5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||s " 0e@        @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5%  N E5%  N F   5%    !"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab f@ Oq0ʚ;7,(ʚ;g4KdKd :A 0pp@ <4!d!dL$ 0z<4ddddL$ 0z<4ddddL$ 0zg4>d>d :A 0vp p2DEFAULTFONTSIZE10.DEFAULTWIDTH3480DEFAULTHEIGHT2760___PPT10 ___PPT9D"(? ,O =4wWA Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function SymbolsXW =WSumit Gulwani George Necula EECS Department University of California, BerkeleyX%3$K% IntroductionProblem Check satisfiability of conjunction of literals Example: x = 2y+3 F(x-3) F(2y) Application: program verification Existing algorithms Linear arithmetic: Gaussian elimination, Simplex Uninterpreted function terms: congruence closure Combination: Nelson-Oppen, Shostak Our proposal A randomized algorithm We hope to gain: simplicity and efficiencyZuZZZ ZBZB) B >Q-OutlinedLinear arithmetic Retracting assumptions Extension to uninterpreted function symbols Experimentationy*Algebraic Interpretation of Satisfiabilityf1 : (z = x+y) (x = y) (z 0) f2 : (z = x+y) (x = y) (z 2x) f1 is satisfiable. For e.g. x=1, y=1, z=2 f2 is not satisfiable since (z=x+y) (x=y) ) (z=2x) Can we "test" the satisfiability of these formulae with low error probability? H    )"Xt   $  &/,*Geometric Interpretation of Satisfiability &Overview of the AlgorithmGenerate random assignments that satisfy all equality literals We do this incrementally Start with a set of completely random assignments Adjust them to satisfy each equality literal one by one Test them on disequality literals If the random assignments satisfy e1 = e2, then the formula & . e1 e2 & . is unsatisfiable ?" "" _?L3""                            , [ "*Adjust Operation: Algebraic InterpretationRNotation Sample S = collection of assignments S g = 0 means all assignments in S satisfy g=0 Properties of S = Adjust(S, e=0) If S g=0, then S g=0 S e=0 If S g =0, then 9 g (S g=0 and g=0 e=0 ) g =0) S satisfies exactly one more linearly independent relationship satisfied by S> V#Y" O0P   Os$*Adjust Operation: Geometric Interpretation &*The Satisfiability Procedure IsSatisfiable(f) = let f be S R, where R is a random sample for i = 1 to k: S Adjust(S,ei=0)>/  $ H +The Satisfiability Procedure IsSatisfiable(f) = let f be S R, where R is a random sample for i = 1 to k: if S ei+c=0 for some c 0, then return Unsatisfiable else if S ei=0 then S Adjust(S,ei=0) for j = 1 to m: if S ej = 0, then return Unsatisfiable return Satisfiable>a*/(  ! K      Completeness TheoremF If IsSatisfiable(f) returns true, then f is satisfiable Proof: The final sample satisfies all the equality literals and the disequality literals in the formula. VAcb>  F (Soundness Theorem\ If f is satisfiable, then IsSatisfiable(f) returns true with high-probability Error probability m: #disequalities |F|: size of set from which random values are chosen r: #assignments in the initial sample R k: #equality literals If m = k = 10, |F| 232, r = 15, then error probability e#$9&>  A & Complexity r = #assignments in the initial sample R n = #variables k = #equality literals Each adjust operation has cost O(nr) Number of adjust operations = O(k) Total cost = O(nkr) = O(nk2)0Uf>u  "Retracting Assumptions: Motivationif z=x+y then if x=y then assert (z=2x) else assert (x=z-y) ) decide satisfiability of (z=x+y) (x=y) (z2x) and (z=x+y) (xy) (xz-y) One easy way to retract is to remember old samples Space overhead lRA*3-%3S 1F*Retracting Assumptions: Unadjust Operation Remember r Unadjust(S ,e=0) = S [ { r} (S [ { r}) e=0 iff S e=0F  , " Uninterpreted Function SymbolsUse Ackerman transformation Replace uninterpreted term e with new variable Ve For any F(e) and F(e ) add if Ve = Ve then VF(e) = VF(e ) Example (x=y) (f(x)=u) (f(y)=w) ! (x=y) (v1 =u) (v2=w) (if x=y then v1 = v2) Implementation After adjusting for an equality, check if any of the conditional literals require adjustment. Pm T_/           _ K  'Experimental ResultsFComparison with Shostak s Algorithm   Symbolic manipulation vs. expression evaluation Shostak s solver adjust operation Shostak s canonizer probabilistic canonical form hA&>1   $Conclusion and Future WorkRandomization can help achieve simplicity and efficiency at the expense of making soundness probabilistic Generate proofs Can we extend these ideas to other theories  inequalities, arrays? Integrate symbolic techniques with randomized ones/xP<  ` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@x?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>f-K0 bZ(    6 @  T Click to edit Master title style! !  0` 0  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  0  `  @*   0    B*   04     B* ~B  Hp?"@@H  0޽h ? ̙33 Default Design0 0 @(    N*uu +   x*  Z,,ZZ  N,*uu  + * z*  Z,,ZZd  c $ ?  *4  N\ *uu  ][ * RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  T"*uu =h  * x*  Z,,ZZ  T #*uu = h * z*  Z,,ZZH  0Rm:> ? ̙3380___PPT10.47L P 0(    N\Kuu +  K ^*  Z,,ZZ  NKuu  + K `*  Z,,ZZ  T ? ̙3380___PPT10.47Ui2-K0 xp  (   x  c $0`  x  c $`    R  s *\; ; \h   s ,,3 A ??0  V  0޽h ?"` ̙33y___PPT10Y+D=' = @B + `-K0  h $(  h r h S (D*@  * r h S D*0 * H h 0޽h ? ̙33___PPT10i.N-;+D=' = @B + f-K0  $(   r  S  @   r  S  0   H  0޽h ? ̙33___PPT10i.VWpr+D=' = @B + Б-K0 @ P(   r  S u*@  *   S v*0<$D 0 * H  0޽h ? ̙33& TIMING |29.8___PPT10n.v+YDB' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+ -K0  ^(   x  c $*@  * x  c $* *   <$* ?"6@ NNN?N ,$ 0 RIDEA: If we choose points randomly on L, we can easily tell that L ) R1 and L ) R2S0 2C                  0H* @ f1 : (z = x+y) (x = y) (z 0) f2 : (z = x+y) (x = y) (z 2x)G    ,  Rr  s *` Rr  s *` RB  @ s *DoY XB  @ 0DoyRB  @ s *Do RB  @ s *Do[x}   B* ?"6@ NNN?N M  CL&( 2   BL* ?"6@ NNN?N70 CL&( 2 RB  s *DrRB  s *D   B * ?"6@ NNN?N<   j R2: z = 2xD ( 2    B$* ?"6@ NNN?N i R1: z = 0D ( 2    Zgֳgֳ3?"6@ NNN?N  Bܸ* ?"6@ NNN?N3  CP&( 2 RB  s *DRU P  <P* ?"6@ NNN?N   .Line L: solution space for (z = x+y) (x = y):/0( 2%        B  <DjJ?"0@NNN?N ,$D 0H  0޽h ? ̙33& TIMING |98.6____PPT10?.v+>8D' = @B D' = @BA?%,( < +O%,( < +D' =%(Du' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+8+0+ * + `-K0 `8 F(  8 x 8 c $L*@  *  8 c $*0 * " 0PpH 8 0޽h ? ̙33___PPT10i.v+D=' = @B + +-K0 \ F(  \ x \ c $*@  *  \ c $_0 * " 0PpH \ 0޽h ? ̙33___PPT10i.v+D=' = @B +[? @-K0  $d 0 A(  d x d c $xw @  * x d c $Lx P     d 0~   NAlgorithm to obtain S = Adjust(S, e=0) ('r d  fgֳgֳjJ?"6@ NNN?Na  d  `gֳgֳ3?"6@ NNN?N   d  `gֳgֳ3?"6@ NNN?N  d  `gֳgֳ?"6@ NNN?Ns(l,$@  0 d  `gֳgֳ?"6@ NNN?N- B m,$@  0  d  `gֳgֳ3?"6@ NNN?N P   d  `gֳgֳ?"6@ NNN?N8 ,$D 0B  d 6DjJ]W ,$@ 0B  d 0DjJuL H,$@ 0  d HG ?"6@ NNN?N  HS4*( 2  d HdG ?"6@ NNN?N  HS2*( 2  d H G ?"6@ NNN?N Fp  HS3*( 2  d HG ?"6@ NNN?Np  HS1*( 2 6 d HPG ?"6@ NNN?N P ,$ 0 LS 3*( 2 6 d HDG ?"6@ NNN?NP _`,$  0 LS 1*( 2 6 d HDG ?"6@ NNN?NC `  ,$  0 LS 2*( 2 B d @ 6DjJb  ,$@ 0B d @ 0DjJ$ Y,$@ 0B d @ 0DjJ ,$D 0B d @ 6DjJ* ,$@ 0B d @ 0DjJ ,$@  0B d @ 0DjJ 4) ,$@ 0B d NT$G ?"6@ NNN?N.N  Hyperplane e = 0@( 2  & d Hd+G ?"6@ NNN?N[ # ,$@ 0 <r( 2B d 6DjJ t ,$@ 0 d  `gֳgֳ3?"6@ NNN?NG( l Q d # l$0Ggֳgֳ?"6@`NNN?Nk ,$@ 0 C.&0( 2   #d 04G p  ,$D 0 `*Assignments = points Adjust = projection onto the hyperplane represented by an equality literal S satisfies e=0 and all relationships satisfied by S2 ZH d 0޽h ? ̙33&"h TIMINGL|13.1|17.6|19.6|17.|19.8|20.7|5.9|36.4!___PPT10!.v+ORD ' = @B D= ' = @BA?%,( < +O%,( < +D ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(DY' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =%(Du' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*d %(Dq' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* d %(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* d %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*#d `%(++0+d G ++0+d G ++0+d G ++0+d G +|  -K0  L(   x  c $PYG@  G   c $LZG00<$@ 0 G    pA ?txp_fig"6@ NNN?N B t  SOURCEr\documentclass{slides}\pagestyle{empty} \begin{document} $\left( \bigwedge\limits_{i=1}^{k} e_i=0 \right) \wedge \left(\bigwedge\limits_{j=1}^{m} e_j' \neq 0\right)$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH348(BOXHEIGHT276"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG False6BITMAPFORMATpngmono8 DEBUGINTERACTIVETrue(ORIGWIDTH2668PICTUREFILESIZE 19623H  0޽h ? ̙33P& TIMING |27.9___PPT10.v+ED' = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* AQ%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* Qd%(+ -K0 `X (   x  c $kG@  G   c $lG00<$@ 0 G B  <DjJ?"0@NNN?N`@   pA ?txp_fig"6@ NNN?N B t  SOURCEr\documentclass{slides}\pagestyle{empty} \begin{document} $\left( \bigwedge\limits_{i=1}^{k} e_i=0 \right) \wedge \left(\bigwedge\limits_{j=1}^{m} e_j' \neq 0\right)$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH348(BOXHEIGHT276"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG False6BITMAPFORMATpngmono8 DEBUGINTERACTIVETrue(ORIGWIDTH2668PICTUREFILESIZE 19623H  0޽h ? ̙33& TIMING |28.3___PPT10.v+EDZ' = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+  |-K0 T 0(  T x T c $~G@  G x T c $|G0 G H T 0޽h ? ̙33___PPT10i.v+D=' = @B +c  H-K0 b Z Pt  (  t x t c $G@  G x t c $|G0 G * t jA ?txp_fig"6@ NNN?N RJ SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $\frac{1}{2^{96}}$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH348(BOXHEIGHT276"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG False6BITMAPFORMATpngmono8 DEBUGINTERACTIVETrue&ORIGWIDTH296PICTUREFILESIZE2208 t  pA ?txp_fig"6@ NNN?Ny9 G. SOURCE\documentclass{slides}\pagestyle{empty} \begin{document} $(m+1) \frac{|F|}{|F|-3r} \left(\frac{3r}{|F|}\right)^{r-k}$ \end{document} 6EXTERNALNAMEtxp_fig$ BLEND False0TRANSPARENT False,KEEPFILES False.DEBUGPAUSE False,RESOLUTION1200*TIMEOUT (none)&BOXWIDTH348(BOXHEIGHT276"BOXFONT10(BOXWRAP FalseL2WORKAROUNDTRANSPARENCYBUG False6BITMAPFORMATpngmono8 DEBUGINTERACTIVETrue(ORIGWIDTH2218PICTUREFILESIZE 14058H t 0޽h ? ̙33___PPT10i.v+D=' = @B + -K0 0l $(  l r l S PG@  G r l S $G0 G H l 0޽h ? ̙33___PPT10i.Obʢ+D=' = @B + p-K0  0(   x  c $G@  G x  c $ШG0 G H  0޽h ? ̙33___PPT10i.v+D=' = @B + P-K0  @ (  @ x @ c $dG@  G x @ c $$G Pp G 8 P   @ `@P r @   `gֳgֳjJ?"6@ NNN?NA @  Zgֳgֳ3?"6@ NNN?N   @  Zgֳgֳ3?"6@ NNN?N u  @  Zgֳgֳ?"6@ NNN?N(Sl @  Zgֳgֳ?"6@ NNN?N B M  @  Zgֳgֳ3?"6@ NNN?N  P   @  Zgֳgֳ?"6@ NNN?N8 `B  @ 0DjJ=7ZB  @  s *DjJL UHn  @  B G ?"6@ NNN?N   HS4*( 2  @  BPG ?"6@ NNN?N   HS2*( 2  @  BG ?"6@ NNN?NF| P  HS3*( 2  @  BLG ?"6@ NNN?Np   HS1*( 2  @  BdG ?"6@ NNN?N P p LS 3*( 2  @  BtG ?"6@ NNN?NP m_@ LS 1*( 2  @  BG ?"6@ NNN?N #`  LS 2*( 2 `B @ B 0DjJ B ZB @ B s *DjJ$  9ZB @ B s *DjJ  `B @ B 0DjJ* ZB @ B s *DjJ  ZB @ B s *DjJ4) D @  HTG ?"6@ NNN?N.N Hyperplane e = 0@( 2   @  B4* ?"6@ NNN?N[ #  <r( 2`B @ 0DjJ st  @  Zgֳgֳ3?"6@ NNN?N( 'l e @   fGgֳgֳ?"6@`NNN?Nk   :&0( 2   @ 0G  p &S = Adjust(S, e=0) H @ 0޽h ? ̙33___PPT10i.v+D=' = @B + -K0 P (  P x P c $G@  G  P  0G "6 ?0<$@ 0 G H P 0޽h ? ̙33N$ TIMING|60.___PPT10.v+ED' = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*P T%(+9  -K0 8}8@=p 8(  p x p c $L@   |6 p\  p  #"."rrrrrp\    p  B4  ?"6@`NNN?N@ x  I9.6 @` p  B  ?"6@`NNN?N} @x  I7.5 @` p  Bv ?"6@`NNN?N  }x  I3.4 @` p  Bl  ?"6@`NNN?N  x  I1.3 @` p  B ?"6@`NNN?N`  x  I2.3 @` p  B ?"6@`NNN?Np `x  O Rand (ms)   @` p  B@ ?"6@`NNN?N@  H40 @` p  Bp ?"6@`NNN?N}@  H50 @` p  B ?"6@`NNN?N }  H40 @` p  B ?"6@`NNN?N    H20 @` p  BD ?"6@`NNN?N`   H30 @` p  Bh ?"6@`NNN?Np`  M#points @` tp  B8 ?"6@`NNN?N@ H72 @` rp  B ?"6@`NNN?N}@ H42 @` pp  B ?"6@`NNN?N } H29 @` np  Bd ?"6@`NNN?N   H14 @` lp  B ?"6@`NNN?N`  H25 @` jp  Bd ?"6@`NNN?Np` N#adjusts   @` Gp  B ?"6@ NNN?N@ \  I2.5 @` Ep  B ?"6@ NNN?N} @\  H10 @` Cp  B  ?"6@ NNN?N }\  H11 @` Ap  B ?"6@ NNN?N \  H65 @` ?p  B4 ?"6@ NNN?N`  \  I168 @` =p  B% ?"6@ NNN?Np `\  NICS/Rand   @` p  B. ?"6@ NNN?N@ dUf @`  p  B' ?"6@ NNN?N}@ S Both-sparse   @`  p  B? ?"6@ NNN?N } S Both- dense   @`& p  B@B ?"6@ NNN?N   n Arith-sparse   @`&  p  BR ?"6@ NNN?N`  n Arith- dense   @`  p  BHM ?"6@ NNN?Np` OExample @` !p  BXd ?"6@ NNN?N@x   J23.1 @` "p  Bd_ ?"6@ NNN?N}x @  J73.9 @` #p  Bdu ?"6@ NNN?N x }  J37.0 @` $p  B4} ?"6@ NNN?N x  J84.8 @` %p  B ?"6@ NNN?N`x   K386.4 @` &p  B ?"6@ NNN?Npx `  NICS (ms)   @` (p  Bp ?"6@ NNN?N@ H35 @` )p  B ?"6@ NNN?N}@ H50 @` *p  Bئ ?"6@ NNN?N } H20 @` +p  B  ?"6@ NNN?N   H25 @` ,p  B  ?"6@ NNN?N`  H26 @`  -p  Bȸ ?"6@ NNN?Np` Q #equalities   @`B .p  <o ?"0@NNN?NpB /p  61 ?"0@NNN?NpB 0p  61 ?"0@NNN?Np  B 3p  <o ?"0@NNN?Np\ \ B 4p  <o ?"0@NNN?Npp\ B 5p  61 ?"0@NNN?N``\ B 6p  61 ?"0@NNN?N  \ B 7p  61 ?"0@NNN?N  \ B 8p  61 ?"0@NNN?N}}\ B 9p  61 ?"0@NNN?N@@\ B ;p  <o ?"0@NNN?N\ B 

 ? ̙33x\e]\nPRRZTDiFD)iXR@D=u{?gӍL#faX .>~pxxc5 _1}>)CgeTc@`0``@@p"1 )9%Չw΃0000\    p@@@@Ql@bRddTT p @@@6m]=}C#&fVX888<px ܭ:O@g~; |x/6(FC#' p%rM@`__=dQ~4qWOp8w*IeT!ہ 8FC:J4@gф6ߛЀE?w\~ %s#;k{k* kTFvG]M*)k |d%~І@_;X?ݿ6?zg߆ 94̟J ?YEs1!0-s5fDj+*ClGLg x!Oฝ:u tb2 PU:G*P,9Y)/FC=:א0W:׽wmn@Ŋ Nk՜G?'TʆD->y_HV#ξ$AFduiƇ}[ra<(hL抡.})): wyRK̩!^l)̒lEHn6  \Ǫ]4nɼh=U^'u Ǻ\FS2g#h\a.o{j-66 I$ &Ec׾iy^|fN9u{z,7[+%Czbj2[ĸ./`!˟LFuq! 'KD*q96yx:]1<7"ʸtV6 8:3N\H_Yy:7吾4IHJG $ܙB/>+.,8ΠvGǐ.MdZ tL3V+^̡ipWt\fT˻cӢVRb yECiw;uQptpmy?JF: n=~6bZ덐ވv"0"pt@ΒX C,ZWMdяp|=)/TErv8pa4#mP|7E6gxg_腽ؔ*ͺܕjo(|YC܄WiU3Y{]Yj2BP~u=;>HO Y.˿ zx.ԩBk&۾6GdU T.?y4 "o`=1 AlmѰR% *Op(.7 ٭q/uٛ3Q$ziU_ERDzR+8x?FȦ%w{)Nd"[u6A)P;lICU+!Dstl45sv`Yh0fÄ>,ǯe^L wDqp~򔪠X!)/j [62j'C%<\o\F侺xw`="{:H3ߗC&k|Z z"XrB81V~n[<ow@M!>g2r\|k`ϋDӳIp$3\/F=2 􌮩r7wՉ {Cw#X aZ~8OAPci;)1YW*Aо;y)RwD_4¥t]jC_Ј!I`'^gFT\8-.KI yc\jn7 2Q#_]lwKl<|2y~)LK&h|WW,%]U/ooD#wbkFc/u)5h'f@DS5gChuőL!TCW-]~!Y0xgGl*Vsk>^՘pL1:e Ǭ sro1<?;FK/@GXϦ&dں .AM{&[v;F|l}wH8\P rh;#CW:ƮPYs1XɺЧ3fJ5 vllaXx߿oV͔T pIs1 wŽ)BJ]/Pct\B=K#2IQ$ ^gB_C[NE ,IF4:8~6 lA~u.Tҡ {~/&,*׼G%_9Fx*BO珑݁q?B׽aQH-3E'Nʇ(w;p;Y'D} sSܯmvq7BgC>EKP;|}7B 9){ٛhYV-W'A Ek^-8eV7_eyF?gֹ&،D"+ǻ$#բ,r-"rDlD. `* 0K(d˖U{G1iη6٠Pu%7Q^;Ffv q0!-/zϦI զpp.)#k #ɭm3{kozG@S.1Ys'&fRq ,wq=YTOC_/d9US $ u؏]lI7& M6N8sńcO "- 7i[Qvy<.U)cgZaP&_t̰ք}D7>143PN/zLW" RAnG1\~pi!1gU+0 4,e8I)N=-~1Z(1=ܣ*2bNI;"Xt\%,0iI^^]Ͳͯ1rxlTҢPC>v4 CF8 uM+VY};FSn(_%9t Ƨ2V~/ o7>h&#-XŒڟk9;+ƭ*N^XY~*y؋8f)ixꓹ7`2r}Dy%!&h]$?Ht'X&\Sxh3i!kaG+YW'ov.f՘Okq\IS"dd[kC>L4q/gIRn+p65lvmW8ӦMq[wҺYoSϝ3>͞j;h530Yn A#|vk_dVE":?.Çxx4$#l|o]LN`jC"åj-,h %O/W&'-/Ţ{ QsćD-"M]Z1XfD^f DGr TεZvAvd0y6.e' Nw#[INYi w#p˙؊Eϫhv``i'rk0F.<%w0Wv_DAD3T1 ^\sfLV9LcGvArҹDwD_"AdY_"(˒HH<GGP}4ޭƆXek '.B/]٘z,jwmvpZz4Ne.%IEǥ݀n!>{zk>NoIS|k {-58>+h-DxOIB̄O%t&urKěϹ ݧ)&%Xxܙdf\~IGm kJ3fG }6϶/!n% +khH _#~)@C<~Ϯ4{++,W[l d Xt兆mvޒ.|1l7⮸Hr1 !NrRf c ax*LvǒO9gV=_Z?<v2U$rY JJ^\xd9mS#ezIJK!d ޿wrfkgZɓ T~{FL3o\Eypa1C2OTgÁZ G~xWI3v.[:vM( \r 8[RQxGIZ$,MוsmP l+;=M3W,`t `ַ2Ex$cjLxX*["GsH?>jCJ,ο{wskq]o6%ORbd{%٠켜p 5G/997)vK=YW ͛]5N5 #ڲ)CD[ll;0 Dl,ܝr_ {zxE]|}sNǼ]`6c Dxe"&Ɯw#^ ^֦6==ma~MUu !]eQcVzI,$s-a|L e4©;0#CYY1i=jc̋U>c!".v0a#[l8hH5/M|JLnƛl,4Yb_%ɂHZ!Jk/1TI\|M3džTʽjc`>iN;Ltq$M.c\Ѭ}Io;>Wׂ|dGv@Ha/6VHV-|@wa3JS 8 O%k]P~sm[ƓFoZ {JtJ~s^# obtB=K b2E^"ܮh/-ǮB5)UY7݅.?e y,k ꬐ũ/z(la*2]+3.4 PX"{A[._ ߱TVs k.h-bo]Xuff W- icQ'#Ч?ǻ~$ǜ-b$椴 5>ACؼ=>ra;hm,K,~c$$ -sDe5`AAȅ̂.id~IW9).@d'yvZLK郟f9B8^ߗ:3!vPRS|>NxcpИK/44TV`, L7+. 17N<Eh.Xv \ُ JO.D=ZPz'xZA;Y3vOw?^/`B\ @jmе^T΄AqKog+^l`Kt-)%ǚ`7\(K J [qeuTD<̛G 9ʹ\WI>ƏKw>d=j*L~toJA ֌)P ,Mis{>&'f]CD]X d"F7;l^Ey`/FY} Q_ ~AjA?"KY4\@1HPgtX1i!}7rg_mUje} 96~Eqf=0rԥ +phʀoe̻\x^+.3_0jĠ7SU#!M):EZ6=߁V8j/oޯ2ڨTHȉ>d"1(n^TD/^|Kmu*{wR(F-EMΧџϔS<1NOͷqR (}a 7<#\]ce{'bݫsBs> ng ŰEs-µky7b zi;~Q<OȶnL+XY7RޮȪ ֘ƺ+ƾRUɠ&Q>ՁƐ0{C"PG~1T;r7ޜֆ-m;}mḾC6g໼ԳRҋ]YxtT:0tM9f c /m.9*T;K]U,zAP.AMqc> p RC"4]GjKލW|vW88)F5g@D} ~5yϸO&?ȫ-ł)F/Ǵ]K0N'L㹝n[e\8"ڋ1۪#.4s&,hE:y?gcX꿔/"znso\T^7q=Qvfk2SK7p, s\FE)T AjӞ'g!5|x+Q&I(D U9-ֳ:ׂ.;R)_~_|֌_<" VtʈLp]F;ݺj%monE#C_ Zc\἟̃!-gj/ F_^θ _Gc:r~0a˼S%b0B3׶y5;cNƜ{Ũ@%ZKNy@+B3{אLt1")?ؐeRb׍L vbz 3ʉeo0L|Be$VNeƤ~n^'㫀eF^%K]XfpW?ֵ^ҰM(gGw(+qF]q?-Y2^0% }̐WG }P3^Em1*Kղz_&Qo|ʙzjYp Ӥ |F={1vjM=QkBC\pDq蔌]HBn5)J zmey>Yq ]u]eJ J8SZQg,ؓaęܳ3Bf6֎"槷x7Kp}Y HwjV)AKzGvJ$.IwqNsIjZԁjߚZt> z9ט:"!Jt<^\Z-£ wΔc\NmQoªsđ޽&5:e9V8:{W¬>rBqm\P1/I-q.L#XecE$Q ZR/ɵNvao)^QX8̎Y˻jlNb+Ț3p5}sz׉ѓBAVbZ0bk)kqap #aROWZryn X&`_0%cB9!UGFyޞ&[ńȼfK79g~W]-ʼ4o sK2ٹԼm>}hajHKAB*H|&eqNηOޜB<.u<;5^VȺ03ŏn t,]Nq3,c%1 M 6.='BO-bz=q#z-{od |JfJ'R˃ӽ98[ϺMF`OQ 2 Kvlb^ZѰeK":}aٓe2Ɗ_wF˱ֹ*;vhtިNv7WN*{|kQ+ : kqܵ!dDPmrr)Y廳˷27o;fLH][I:` u5\-dtD3A!bX-}>R)Q.P[jWOp$nEtY!Ug6A:c1"a>.zbbpOe(]8gfь`lYn؞hBna!K..~tsҶbZB^&&!ZI^4uM3ˌoeZ:ڷjRQ[RL& 6n2d?LYF ;1T0-FC9LTt=suWy_t39R@nY|*JDdЬWI\YfءYTg` ͐@l IqqK矸h=ܭnn^Obr IzZØZSSHse6E)簨ذXq=v - ҆yV1{hd4(=Rf^{tLYxC&6ġ>D`gxHW:t ZA%49Y- W$!_?=Ix Olp{u ZbnsJ~pCcq˥2BL䠱"s) >7v/7|0{ `D u>Xťd2oc<{RR,U\1U=Z/+:wIAsQ_oX7[&XXS}ajWG\W'V>MsaBH|.UfssF꘯HZyO,֒g!҄rț>r<}$i_xHS G__(daxw%w4$Mz?%:>0yZ|y-i;zzOiLUR/hrG/-e&~|~Z HN%[͆ Md];fpٍHnDYC/^,GCZ&nMV4 Z/lJWCà2|6+g/@J?%޺S9Y]2fEC݇[UhA,kW.ζ]v^od{ADκE:|&`IKQdNmexKz9p?Jm\ւcbTx/ƕ'˅nV*$oSJHM49: 5'K2HtC0F[_3SoGrĂ | #TTӱʑFu6؝ [D[^olqըdvo1X/Vx)uuo[pI&C2<(Xo{:&Ot߇wiOp P'=yۺ\BpǮ.KBd[~u,5~}Jr[`)g;]mlDDuШd_v̪/ fq]sF՚XK".9 Y$[D Y'Lnn Yekm){fؚg!֘*76VAw=iQ8dtW1oXtG})g-+{RM^J6%F5 `Ւ I6eud7f3#CuJ"h!v-[Ս'筸.A4b[18rU9*P!g;\e rxI4^lb*!mH8G){V]4>\]I! QߢIi՟r_`fsH 2*F'gf.?gh&5:mpas0Qz,Pf~_(h|Dc&f,GUT۵ )hptU \6TV|;-ߥtP?YO`k{ek3׈7J\DDe>Ê3H`xK}+yX\9KK]>I)*1P }|Ѥ];ރC%+s65\I^Bv^]=f r\9D8砌PmUN֡k}( ]#w`VQNMQ%3 H~~Ut0ax/V1#FGPW\p'sW|{/aE_&2*];Ղkϡ*|ql".L{f\2E7- vuT4m)΄XQ˹!&9$ߨVAGϪ']XVQ{Uf#%6 2&ͳJqR7&B\9jАICm0R̻QVY]B+B[S\X6yb+(Q]`v m=SƐxme'c(bBPxW&4#hn8+* 0CRwϵ2qC.|x== ;{Oc-u@sP :;ݐ $YESZ[xwߩ^Ftsf؛k_BM[g;VX5-%[z}u'jvk1GEM\3Gt|%$3:щw UM|SSW7r\0/n{:|31Dl[!Wڞ{}v^t+B)c*EW\{)-- %pIxŽʇx{mkٺtלּa"}B!yn3%~ ;4nHS6>@VFc*wT鉉%k1.6X[+uQ/M,7H@6>M0S^=1&HU_n5N,(W׽ XV3!gPp:~'#9aFQ>ԍBO:/ƁюYN*xe襗nxaa_6Pߠ!46~h͐g~4PʦԝztϞXj̮ ۽XiLa[#D#m{OQҞe?o:H9n)+*y4,!krH%] 9+Lcb0h-ZͪM6TQƺL~Cm$賶5kw^2(=p<^Y NhevkBTUM]]Ne{][)ܟo:oGK5Wvj"0[v I,aZ}Ѻs0ˤƾ.8C|E@w5qf??dN'K֖C leAD3 C w]6r%rv?ta%o~OBBx  @"@@2@ @*yW((@E1@ @)@@9; J*jsu M-m]=zFF>LLߵz4 ,w:@9z"  TD.2(rCGYoEq Bt_{}G7̬ -A'>RC /Ѡ{f> UEGC:OKh`T>z prġ:CQ_QA-բ.q>{?)Q8M ?T'jgOc>8>PC5o]'z81cc$v(5`vx dQrEkUI!*h'G!ur_;Úᓺq9r}vQџ?cpǵ'4YX=nPm'TPOkjO@"c'!jXq}sEe qbǙjPxׁk] F<'ZT?}:pЏPlj!Q"n??ڠ?!>IqKQG <q4AGcuAykGl>GC#OPuvx6#D;;mTٮb ?}jw&fps]cq;\q~k 8ܱch@i{>׉f+3@w1[}?\#g8m6qI՛b*ʵ78ǍdKHJǁd ]5)h- ͧآB·C>P12<}C^޻3<:Js^ӏPԀ섌Vs+23zg МQ9UlKC(zA@`*m b_==:>H%^0 J2dM {bOG'vQƯ6KИSĺa 0rnY57 񌒫"}_F`_~7F0F*laF0>sMR4(bQOC#BQ S&X"ΛB`TԭyӪ|`$6ޗ4D}\Gx_ 3{ 0pZ#$!n z64x go5ƞ-wwcPb&)m`VnV5Y# NHgOGD-Q# aQ:O(@AIih쯊ҫ֊F v% Y^9c[SM/vXpm1untрQ'4`Hgdo&j/0*|. hYж005O 猗!yLEbRv0SF^&/slܨk>U|6YQfct!*EYM."Fа 6&*n\DK-]f5jW`q`L$)3 4zУRI*dxic$7q䃩ndA.jf0 ; 5f@Sj`,#P6n fTԤ,} E;gXiO =F\A<҈Bڠ#cbPs <o͚*΀$)PKSEH)֑_f̐2ݼL rI32B^ub8xHԙ(024o2)PRJ}Ĉ/,c6!Xy5ȫΕ2.i%.܀[Y- a GeP=vL|9C|iRm1u֒uFDC1l#|'rp ` j5{Iss`D$QzLlI cm1#<@g%4YKbR ,GO;f Y͠G}TEa? .j.e}콫pZPĸ6I4EeRE>\*!%~Ѡ+#MJiuӛ>i.{F%x5Ւ nXM%q{Ӹ!+z9e!j9YK$Wi0cBz 'S'zN9H;mF!!V]Na܋c2# =_tBU] ˄[1)%֒q_?rFb,9K Ƌ 1Тkq y?3F(0w!}Ch38jjjMFVYJap_-F-NϚD;;TZ$EfuZ3#=~b9yŽ,ꁑ;މ0e@_ٹ 20~z6NΏrrV@Y M Hk/{"D:dK(Db_3P9j+M0I4:Pa@Zb@OtA =mN X{x'cteu}n&_302 z0X|2Nu]A%,w n:rፀAKl+nc$vYPaЗ'LC,%`ZaH[0"^![%x0vUZ)k m- /+WKvfJc)Z\xCDHJݑ2:pw=EBBt]Tpi̖qG.Ie'd! xU1 Y I KA;%ZVQc] u8ӦN_XFI +(PT]d8& %YhR_QXTNUu(+<#U״oYPFҲ:h]8}(:f$32Z=~rz48OGMn%{S;BrUxɖAU ) fp̫Ѱ>} C"fr#h0v[^E/ s8#TfKd{+bBpouDEF}~yN4*mSaXf8Q'(6Xn.sOQ]c`r"a% }F:Wo܌i"xG \hGB~Pz3XrVeŒO;}*uK@goE<щu~4,3s3Nٍ#V26d4!mSgvـķX ZhelT+X۸嬁Fe +C u~FnjV) 69eI=0Q1*Co]K.; JzPo GzyLZ fR0𕢒69HK n#=⣤gnt̨2:%P^&:{osjTg~9gpA`v~)Rf%尫c蛆TYm8Ǹ69HbBm  3nf 0W<Y+:z$Au)P`!F5[*g1#_P8Sfc "ّ屏1bA3nFRgܽFg ҒQ,R-ģ i0cuSHapyO"Ub22xFÁjPe KːĻG6'&*EzQ3H#GW< |$3 ZXEH!cXv'kP:cPK8'2bFϾHG-(ՙK6@hQuH>  eS$٫ iT ⫌(b>0F3d%ct i쪯:Fm30j>x MLoF֩a%`aP'|("y[T44Fq?R$kw<1-T|ثKGc+4v5{_0hNM?jW%ajBT/rk^K2x.LKeVlH|dٍ52v3CRj e .DǤ˹0[胎Ѱ'hv̐xX%"#]{)`Īr^1>$ي1tFq> Tp594cX*tL+h9*<#K,>$Yd>pICx[ ۞_03N% S/b(3ā500* 8E{rȹ,7 XaX4Q ^DtB NQ#:/`d1f FRŤGYq챬Ӆ&mW0e*[-Y%a%T^3C_&ۿrvY!=Uc=2X:~ٸί2soP@ 1,4a?疪☱|2yU\,23^md2G P%gBr.l츬xrm3[Joiô3 ``1cSZK%pV,0ȫk!8E] U ժ:!3yٜZZ<F,538fњ r$}nBpaD}5EF7Z鼗HC' v9 F}9 r^ Fav!yg! x}"D*' #NF DUsܗ!#0TVy3#m0 3$RR=juqpmBcp|lsXXgFbEH~-1 Ui¥n?2欵zNRKtxrFS0yonlRlSaD͚}UD˜-o4† e=2WgH-0H& B~Ģ¨fhׄigTu~Ibgh8>uSƟBI5l-o /F2di0 W0`*N8j:3h <#㾲CD%3:yĨX 7&g*208FrJeu"7-Mz#Vf-j`hЫTe&Q4AԿ+.aјM룊C B5CUyX5rnj{9fHê1 ziF͔m0t=FTpn{Im͡aN8_ W?u ^C/qȻ1D&I׻WXBBj:j{ʁԆ/$IZ#XGap6tj7oOk `I^sQE0 k{ȅ09/?3{0Wa 1Ȇe |ʸ ʾ$):`Ņ4~HD!xAɄ9,YduPj:bl[/2rQ Ì}5زx vPe"/J%ˉA (8ռB ,J,QM&!#<KXș=PF'Ɂ4S4H33bHԘћtHH.)3< ]=Lg1F OU\Px,5͸ZΨ~J"O70G9`P>SSxb؅, jTބ1C]`4pA1Xpu= +w#\\DUxZJY!a'o-0Ndi& y&4,lgZvjc%(p-LS6:Zcfaa]`U>Z}[G!CgTބ>Kk\ɑլ*_y,!Cox$kS`HJ'% xp/s2%ޑF)|]^3P5Z20v##V8Jbè0؎[&C*E#N]7i,<|>ബANVN!׵ѡ3# 25]gF:=o6mp7i- bH24n|X~6v°1L2Ù/}!;f*PM8aM0{e EL _dDS\Ճ.l= R\(UmX``hy$@ׁQƋ<6*Ng{]D֔'vRHHsM/b:a:R:;Ez3RF2̎ˢYU>EN>0*hPOjqR1M,;fȥjĎ*;#]6XJFK-)3Ĵ1113:cge # n}YuGWכш,!#>h ,1V3XiG~s(P.a@GhTNy0SfZbASIRE;ևHxd(X*;f8G.,7^:Fp1/pN̹9pJ+XgpܑJ24h9в|?l+Ǩ0r;_ʠk'L}[;*lc!$`ӱna_}ٶ{@xGrb}$ x[,8M]9|MX>æQz|Z+Cߜ2?+ N(˾b3N, ֪t`G!Q`2ka֜TQn1XSyfc/2aa}3+78F.F2i~mBkpDgdIx^3Ϳde#YqTUAMGobctб27%q08#fۭ# ]2, -jhm"'K2:ZafQG1'ϋAg f >[DgJʔy5IB) %F^Sf(#UR5˙aU!wcL0!#1(Zq2ayx!cX׋VD˃v㼽e`[C\ʗCx_!#YNc9],[,eh*WXQvi^\V;X̰1kɍp0-Yc2F6 ;רc PR?.f"Ac9뫼|?,rqdl#gnLҴG28" 'vd\Kuee,00B y3e[j^ ֙o6#sCUvYTVʨ!ɉu&7Q:e R2c(F2LNH (܆1e ÌCM#z .7v9CEc>r3McޭymŌ3v=Cg˴wo`OcDѯfh:Qjue#ơM"<3Y¸ .2(+9Z5B.)I=aXRd_햋^ }8jYU8E, 9~"zc {[.xo=U0R[/#D|)ږK5ˆ<l; Qedc$K+"HF-"$.  ѳ.w>Yxpՠsʌ~`-Yzɠ*CGf`1#Q!A(3G JŘQ#1 .`(ȲeH6۔g8ul$<_/Cf$}ˆN *bL(,TYJ\zhkqM\R_| /{R~y᫻1Xɮ/-4Ҷ0JNcݵ US:iqlLs1w%63ExnKod㒗xǔ4gЧ&#Fuƽܥ~ypDV^cమkLed5 KjCI+i0Jepdkg@'2*JDQɎĉg]zFetoY ?HC% MDOIAnpr F F.c{u$omuZEU ](yR5aE9픹jd`Tn jJ zF/ cA-YdP!.VA|m'ա#Ѿ}$j  *RԺBFQ[ljw2ޙQkLj,ARp=+" Leaw7{+,P<#]Y7 Ju:#f.N 3͋K"IedVtlX~UmLmjV7 AjC㑺a柳 (땋I"3CᲮb$?Ǝ4; 够Ia6֭";, ;[ wg QXzyƐeUv'n "F,"j[07WUMb:Sxi L\>1U@nNץ>0$w#1&EMq!:^"N7 36S'Mb~z4q ţ+ݺkّ\cB& \f:ya5]*'^*RtJ˃ݲجdbugb㮜O # lHheC1ʲ$7:)ŗ H~=gc0]kOy1_mߟ>ʎC7?#Q R*өLt3s Ff0ɛnLkx>G"f ]0ds$_Ou:}gq8LKhֲ^O 82ܬ&0)~qKь.=#;rdC"CLDZ$e8}xx[s!!N Z}Fv?Jbp J69ෝ}T~. I`jQ ш~E\ĥ0JMl%\=3z .b"!DJx% 7ݪ;ft*V0̤Xs3 'cpLY D!Q!AHdqFUD+# ]9v?ohXm )h'aI\K)p,GMdk :o i6۟Qmd4,d}0ٻȆI͞;]7s22` j0H uHam E-cRc\I$LmgAvKZXCU,37{4Z#h$ˋ ;I1ZlU}_1 =3%ڴ.P.A"U|#\gav ].prY#ۓ3^`Sm;0;FѦ;4\YsY110ggjݛL"lݝ!C\0x*NGEԦ["uW>8U -h2}Mo",2f1j9 Fc*[8mma`0cFf2TRMQ޾83Zbެ`$bW[0(3K\ e`-5N}bLtԙ6QIY^yϙk\X*W1Xe6"R5uqe*jFo󵽹$ 㘡m-d5ےc!R1FTz}r[:r2{C"+u<ׯqUfmA3Z}ڼ XD!K3Zl_y F17o\vǬc3K)a 71tm5I /1\R2=ű Q-upŲGNP'd`<)84I0浹7z3q8c1gjdBQğƜyݤ-&2ؿ =Gs0OiNs'{|?{?I?O"i׼?~owGͧ_{>e,>~>X3)s Kg_e³ Rr^I_z\/4'ysnʲ4ҷk'«fK/#R55\Z,m:-|_|b̯oi~Ⱥk=}El?je4gb|kR3oR5o#N/N>h;R»JJ>?Dn2=pfoWA/>wȣ1_|O^vq^O>zC>u>ϕĕ~L/ãDOrm.O|O=荙}CGk3o^^_[;Zv1|s3.VN"wK,kp ^߾I]9Ϲ/̧0?K4\q9s=ѹ(p' )̗Oҕ~{-Οñnӡo{fTNC1|}%lj twQ 2,_> /|}E%$sp)ѢȿbΎu*3{n?t2w`\sGdMgrX;yǨݠ6V~j_P>Cg|թ߄o|vgqv%?~T9: q%`o?{>r~G{7'Ti:Y<kG{H1 ?||hJ̹&鷘?=^O~su<۷ͻ_ӾyyK>QE}s߱x{ϿlsXv&=ÏEw σ۽ rOws3T ${ǘwO ]Ԭ~Ϸ/_[R/ݧ{{M_^?\7_\ 3)E%^v=}c|X3_״\\a{|qR/_w#ix,9[qg?; i2?Y:;1?O?ߊ.ҫ'>`~y 4~6 _gǦqz^sv%:EѹLЕ7+s$g |}zw8;Ύ-ECk?KoNߪ?cFBaƈH Ӻaot%u~"yZ2!D$Cی1Π{r5؏xOݸ6|F5v㉇G=%^G|O}\֏k7駮ܵ\3gyߝƯo#x!8;Ύ8;Ύ8;Ύx3(zүƖx?ܯl5◹n/̯M#>"~?#LcA&C{_?/>zǞҕkn|yl3laΥaʇپ$}}<;Ύ8;Ύ8;Ύ8;Ύophr0A[d|kv@opmytj! 0Wg  a&p ՛@Ft=.@8|vmOh+'0T hp   PowerPoint Presentationoweowegulwani1028niMicrosoft PowerPointon@`(G@@p[GSg  )'    """)))UUUMMMBBB999|PP3f333f3333f3ffffff3f̙3ff333f333333333f33333333f33f3ff3f3f3f3333f33̙33333f333333f3333f3ffffff3f33ff3f3f3f3fff3ffffffffff3ffff̙fff3fffff3fff333f3f3ff3ff33f̙̙3̙ff̙̙̙3f̙3f333f3333f3ffffff3f̙3f3f3f333f3333f3ffffff3f̙3f3ffffffffff!___www4'A x(xKʦ """)))UUUMMMBBB999|PP3f3333f333ff3fffff3f3f̙f3333f3333333333f3333333f3f33ff3f3f3f3333f3333333f3̙33333f333ff3ffffff3f33f3ff3f3f3ffff3fffffffff3fffffff3f̙ffff3ff333f3ff33fff33f3ff̙3f3f3333f333ff3fffff̙̙3̙f̙̙̙3f̙3f3f3333f333ff3fffff3f3f̙3ffffffffff!___wwwssⒶr޼mmöޑޒmrüⒶõ’lgJmCJrmmmÒsm޼n¶rݙÓrÒm⶘Òmmn޼smsݒõmrݶmsÒm¼s’ݙssrsݼ޵lûsssmsnünnݙrsޒs՜.+,0    ?On-screen Shown-sݶ{ Times New RomanComic Sans MScmsy10SymbolArialmsam10Default DesignMicrosoft Word PictureXA Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols IntroductionOutline+Algebraic Interpretation of Satisfiability+Geometric Interpretation of SatisfiabilityOverview of the Algorithm+Adjust Operation: Algebraic Interpretation+Adjust Operation: Geometric InterpretationThe Satisfiability ProcedureThe Satisfiability ProcedureCompleteness TheoremSoundness Theorem Complexity#Retracting Assumptions: Motivation+Retracting Assumptions: Unadjust OperationUninterpreted Function SymbolsExperimental Results$Comparison with Shostaks AlgorithmConclusion and Future Work  Fonts UsedDesign TemplateEmbedded OLE Servers Slide Titles_Zgulwanigulwani  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)Pictures_Current UserSummaryInformation(]TPowerPoint Document(d~DocumentSummaryInformation8