From 1a9f4a554c81e1e8f9540fadcd0d070a823378e8 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 31 Aug 2017 16:40:14 +0200 Subject: [PATCH] Some revisions --- poster/poster.pdf | Bin 155065 -> 155064 bytes poster/poster.tex | 7 +++---- poster/solver_intf.ml | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/poster/poster.pdf b/poster/poster.pdf index 8f05dab2cba7df6deddc2e22e5ad2dc7614789c0..0e76f6ad6523b41aa6bc4e956430866aa11608e5 100644 GIT binary patch delta 8995 zcmai#Ra6uVxV2$u7&=8tIs}GB8YHAUq(M5QVaTCFTDrTt8)g7$34x)zV*n);gx~M{ z=lWdJ{8SY3T% z`0-nL$BefSMM-t7RURn3SZkq!KXR=g3Eb}DM!(xpDBY<`4x`2R5M=+t6mO698bSaz zb$EDBI%m_^9a!l4p{h9k>r^F7qaD{7%Nk|mm5Xq4b_obqD7*^hzzg=|1K-5g@r<29 zX1<$OZjb8etV(6QaKDJ<<4@RVJVcRUyKa3t0D^G{;s?T~byPihp@B`Xln%n{Hc zp6LcKE@_q?@06%@#}H_0g8v)<5rF(Ycblv?6{n%}xW#&^X~^e1&ybX${cf8coT%}L z8DKiSsiK$o^5@h?Gk?ZZPP3OWi*5_pjCU;(&HgZQI)1BSVq`#Qt5D_W!VSmi|4!h2 z!|l@(On`-d){D>Rj5-H=4CaMVvP~grFd+4=dJU4Voj3`uPO~IN>HMgHsCU$KRPIz1 zc;vnKVLG6+g&MYgHoWk^`ew`he6udj1%|00bL0J58GWwNV~9%BiBOR6ze^+D=9c}+ z{c?rKnAt}0DlK}ve$05ekP!2NTp;3z=`F;q zqem1zlH*R#Kd$9K0-u5GOJQqmFA_B0E?e!5n8TcVG*sVnLanejd21-E;^1LjZ9(Rn zsm$h1+OR1ysk7Adt4AFqozIjj>`=-Z-I8#5&O@D|U~ISts67ob9Qp=DmVHRKQi1~+ zjr|i?bgT>SRpG1b3G}X{7!fYRv}1#wNJFq9I%No<#q5n0(8GabR*xD-E5(LMoQ>|+ zq>k>quui~|a{z&>sR!2!M#uy*k}+>MHPB7Y4$4L$AJHUL>Yqtj$T80>a;h(cPJ%}! z&E8m182l9*kGK|6yMSC)gd_!}Ycy*szmH!vFVgtp9AZy^V zY^R6_Qiu>gUPK%h>TFqgST2+2n<&=ziacX-|LX*W1Dd1x>B|=a>+o5;rQB0%poZ7} za_L7!HH7*(ukIp${wIM}$%zi~8j4SJdPem#Fm}BZhu>pO*yUAnAHK+AqKEp|hWZl? zUe!V&pLE|#J2C`o1RLtb&koBY5j|l!%PFD}e8}vGL4s?ThnRn;k-7bd^)#Zf!w?Kz zyemfUvC^a}`_GHXN9kaWl3dbTyJ$uVgXypKYVk56y^)~{wI3DLm7;-sUW={ySJ@;4 zOzUC#8?KpWxYC$tJD1~NufELvQbcSZ?}N?!mDoZwhNwu1{)W|lO%S#) zhYUED6|lgnD3UFtEz8E`O`i=s=F8FvQ-Q|)>uf5ia3%oT(Ef`VQvbFaCl)vOpOKO< zd)Daq?6m#L;9+iUUDd63D(|mLAi@5w*lxTk5s`E}nopjE-40ruwC}VOm5qA9!&N`n zk#x7i;f=LW23^5WH&Ja&v`Q=Fc|#cK4T+j+sn1I?yQ_oDD;#rNG%`%ijPbt}L>lHC z(RHl6ZGm*o+#wK#h8+V0SW%6}3_YbAVGrpm6$=Rt6+HqsC0Fm9<4Oy355t=zP=T}IadvwtHei83-Uclg zfO!nt`?grELk~=~<3xX@eJq_>WViPhlElN17^`QEh6kw*MqTViqSHeyDV!@tfWB90 ze!y7NNXi!AI8nrk`BdJJ4JS58K`)N>pPg`f0nR#5ehItL>HMFZ1WbMByW5CsL#3{c zb|zc}9S!uhcP5IY)_i4HU6pJ=Ka<*PG98RewTeDvVP9X@A{Cm`X%$zif^nIOBZv;R zDKl3g5>7COl|Lm(uY7Ym*h@q^0c0d)<&_w2@~CbW3fo!4CDF)r^>hLb|0sh^G^Aog zns;Q5`#lkGfyVLeH#u~w^^mI3QlKh5k*cpO3&p`?Cu{MBA?QS7YB zy<*)M8tB9mx^$&%Si~WLKz68wT0B6c_Fq>2Sfh>|{q#SqY0RdiMO{bHg=3}?GwSWf zm9hVaJn71y#|Y(0VS>cA(HBV04Xs7a&AbvG9%{GoiaKZJ+TQwa{0COl?~qm9jKGoB z5(O$5Mk6{aI*GsTY8c$=V*wi13 z;@`0r4xpe*-<2{F0i%#E(4EkS!bxNy5pjWU-O5an#pu0Q(Nu&nceP*`&a++2+1v3N zb%{7cz7!`dU-K6U4RHBPH6hiqR7cJfhd=ZjD&49TBhoI~Ez-5;FMT|QkoZvdCEP*bl&k+7(dUZk_yw1 zB*T3Lt0A|oOL?r(y|rNA-^{9-#j)o{IAI0O{Ze_Mz{AI`;g+@%7sv%OS58cOmx1AG z<=axeI)$8*KinW+U-3Lup~QDxN*{Gs8Y*GNZGuk@zI)(xqmcCXPguflk&CFHp?mJ7 zp6Z*DG=mJ2x1M|^T=FfW!D#LRL1Lx)Epy&~Gfgc-mPmu_8skg?yWD0}mIO}THJdY! z{ahs4FVtUJTRG-=GJ)vIVfaVE%3sD=48+@3n*!R;#wU^sc_=BbZT#Zd-_nHQD>wKb z7muV#7#aI(3JGY!oR!yuPy&NrSvt>ROuQPVS)11Sb82IM;;}#wG(&5&S?h?{%?>%i z`tIOlX^_52x}6ci-_l?~1)P@}y9Ul30$k^kK8~8c!F^K>V}clAF1=|c0Q6=eIr-?e+3YhC!)cUZF_A(j$oZu6dVk;R zb(wJqR!tI&J!*-fB*w{IECjSfHEmF5kkK$cV5)edzCinxSutao99lh1V@$yfvePD{ z;S-$pZu;*SEFr7-Z`?;AXnv!RgEZOulosWBc1>k+y)omO(usOzqmysEF^=)|tQF;> zCJK7TK?5wroeI9^tf!GGb7hK|^{#0nkvaky%vb?eS#4$w>GvgTbJLZ_*&On2^dyMI zjBRNHN7ZwOP}-Hn{fZO67VrJ!M{N=8jD91lY4_-PX^2@7JZV>1={;85r{{}?nnm+n zP6QmVX8?7Ds|6j)XF7u#eftj>CDQ$0C*bs$?>1u$)HE}84v`rooT_!W5w-;G$7qiy z>RF^=BgC>M=PBnbYG23WT>cKz-r^G~Sy}a=kf-a%H$gIo&SR~+4hImZ^^JOHPTG9w zkGJ;{fS9djZu{~2?_ys0*D9XX%-wqF>Jw;UR*O!slO|SuWIxq@0dVl^4^#=@%gCma zw0)FkTaW67iV%at^Jyh(nLm+}>wJ@Epj&I7XE5R3j3&{KhbxkiYwfVtZZyfn|Dkgi zcvY7{@mDh;1m#x)0Pw`yeT4C*e3FiSQj1$&64L2BH90y&4T4#23iW5kRh&hkOI~DQ zeg_ojQ^>{lkAiVLr_qq(2hBE3;{_*u>o_T#whxufjLcuzdJI0V zM|D)T#Jup{);hoJMHRm!Cn3ci9>-*m@R&<3@ZebFhP&BL)UV;2xKVhbWo7`nF##+h z5Ynttd@rVLwLSMLgc5Cyq#2hvGhM}=D#X^3o-^i`1WNjdar}JZPLH<84~2e;I`HD> zCOv^KS5fjYiedg9LaUvI)G30LOpKiCW=J8m#l=EeS`LMV{ z#7qiCD_ViI?8Oq9ABUvV5e0&eVivRkSu-Se7#L{hMV8vxqD9~{_YdFl2T;6&FI}uH z(|fd{33avOyC%*&v1~dS^vJyNn-z3sK&i0x7xE&`5q>GM$S0@nW7=gTcu^B_6!Oa9 zUV5zn=)q(!==0i=KfAs0=J}a6$nU}TF@83EcL`z1m)EuBauJ#{irGmaSk;CE@kwNg z1&g+av~Q{jl`Qe8>zH_##wUIFN(uEIfmO zMxIrAwW7q1t%x?mNUHW@z*lp_#WkNZT$_g|_sdUhEuNtFq>mqk5C3AX=S`CyFU-ik zUNpO=>eD0R+i@0Q@)+c#gCP;&4d?0&$Q^=4cg5~hdhRufz1ZNa;h!|K%9#Lf30uF~1tkxCM% zra`yWN0`;;!87v9c~g}jfTp3sSbQF}0CVeDpggK+ z6yPX?B-7-`GBvCT>t`wCF^Q8#+)Xx-#jM}8;6nb4(twKIg233NP8rH`If|n->O)K= z^FYXqAzbw9V8?bl`=#9^t`CA7YSJIZB2P9Z)yd`ujD=4hU{aw!zdEz5b>Co^uWodc zCd5F+qk;9l`a}_oHZk(oWQ((-#qr)(V8uxv=iYb!dH6zh6TScm(WZ13nq2vHSLctK zXkl11->_ae@+nJQMxaDh6}~NIY>pYkfK6*0kBe6XRWJ~fBmU6mb9$9*$@E-ZJ8I2$ zzUpTzm?!BijR$a2$sZo(2N8^zpR#a`%T(gcn?+Lz>^&x!;!yq6fu_n?GQT_;rnJD4 zy-#?yC3*gqcC$jFSadKcvK|bCOxt41x%K9SxHPo%XTq#8{y6atMj#f8UjwW*h#AMx z#{aM!+h(%az3ft}bimMR@O#0dpc)!*VwY258u-ZDPS$WcVpi4yJ}J#5i`;g z@EWcE&JE05J=RY@h)fvMIefbQ?MHQObtoy0PegAUME>%$ym)xStH&7en1OIw|4}{p zb`5qzSu5>bNP|CP%Y!6Kk|`L5KFEc-g4StTkzhndABk%=y&;G<9RHfaavE-;4ywLf z(Bd6IV|;JlWqwugH*QYl+tpWG#EorhQxkdSmYCnh3|wC;oM*K0FF$Izg*;63CssQx z^^8+9 z%(LIF5&OG_@u{d>{z^nk5zd)cRk{ z7&$|`s#3NjZkO(#>TR7*DgjEv0ls~CkhIv!eEcTBVJ-@qF#fYxs`<};%D}C^bx@We z$-54;Z_jYb8Dg+$U$U;AVYZ;MWjbEMisxL9uno z;ad%eGTM4Qpa<^6D_c8~F#Y}O^pZMvg(j;Pi|2laG|;^rfL6|RcE^uP!-lvLqIPrZ zm{Y`@-g<5>WNhs><+81at2fJAeXly7E7JUY^ss|GUG9vTFUt;R^uZW|{kr7qQ?Llr zibE{3EmP2j#MiLcDxV@Iu|hW?v<$}yu-ny5E;vK$o2|O7lvl5I(P-;V89AT&nAgBv zoxX8Kp%#RS zRas!L8s+m|IBBc%)O3DuO7(-*`k~igeMS_Bg7FhX%n}4EBFq8g?CifFTW|lO=XmzK z9i?PgM}l^_6xF^+wE02+Dc~yf{Jncu`CgZ^~P= z&a&d*6pOpM^|q_UVUUNl`c0vdH6MhV>otKsANQV1=xIRcIuG)xQ}<@B!!XBy_(pWW zo(LY4?j2@;V>J9^F$W(KE#5I5SMs)wuK@7A_S8-|K-R<$u0f#hroKn_s5A9TT!uOJ zERdtaqKLiDW|4equX^<-&S9~|mmR`;GFk1x3+`-r-rg_!At?ND9p+AMf0G3NjFrG_ zIkP-66P1nkwFR>vTVLLNW^R%OPm~dMiOwM+pFEqgYCp^GjX!%qJVsgfQn+&-;rK0w z_iuCf7L)J;lOmJJF2&C4ll>jKWG-U9X$gPhn-DY;BGg@DWm?;~{b>L?Nr zDx)sc-_X`sOtI(jnmwmlp2U8e;?;iI$Dqb)is;(Fw}eul*8`l&L$i6z@a(b1_SwAKP>bn8q#A|)=b_3 zHRBg{dEF`e#q!hK4f^#$9}yESawUeV*@jn7eL8BK>l<2-4t1)=(mO`r_yOBY)b0o_ zUuRA2Yv-r#>wxaeKV4YCSU2*MUiPdWCuRDRS)#&5qulHWe4A~zIMlfZPOTIt@yXb!qi7+=ChaYF%)P2og&SOsu3KAS7IIh# zV|m{7YxodC1~m)MvgtrNv+R-GST1m|;2MynX3ZL(0$PaudAdz{yKW8dGReev6vniS z{;1t3KK*Pgi-$s8DZqX35b#HPEOq=x_s>R<>Ds$hfS^$k!siBaPw-o5fxA{~W zu-P}2yCg=76@k?Ep%c^S8>4BwVe_raRnxe&o#sFO-tTSGYoSt+Xi>$Wkc1O>)bkV; z?|>ulXx4y=D&y+Cc?lap$KZ}vSRei9jVA6;%?o0c|yilE!Az88iAjH6?S7ae{nj?@`iUAx2wq12<&xd%r}^xKxU#)D z4Z@=hmPKm_Y~>W*O1`ptZqX9?)>2qteTTSp8l^au!o71&?kq`|Y?A zcNwscbW}-)YZ3g!wbgp4slF~-HJCM#oUV>}=C#cXa4b%j=t%0;Q%p0_?S!~fzsu-? zUwsL6=w83=iFm$0((l1(z3rK7P@B$T7c1vn&L=su+GeCka8;d`bnoB%{`h@qh&;cv zaogko7x5kXVJ#cua>5ieb7Y=RtN80Xmf|;nyu%khb>v!@7y@pmZWQRlUL zls=9NVZULt^dUil)aujJsz(s(=?0;a#Y6E@O6O^HY5c;xx1WW4XkEN@OitIvN2?E% zt?^&0)TAHw{h9*-aikSL}fk(>h05Qc{}L;{i9<)BN@0*&=q;lw3FGS z&zzUmN2c)S^%O^bUqcJ;rC<|&gAEL4m@MbA(W2!(^_Yt*fAvtr#=8@O!yIL^v5V$* zWV4~i*PVFZLP|n?UgQ|FAf12BTXj&zTeaopXPLckodP>GRnN|#>AMJbNiH-V@hN)W z25##KWLrSNQ3oG&Yi&ndjU?Z9UWI4m?frK7a&JpqeP1uOgH!(#A@j`R!^!r!W(N`B zg0G?-_vG&V`%jAg5NICqUcH!pDk*-_{ZCTX7XUf#{zaQ~vZ)P+yn9eSZG$D#`tgOc zOfTsLXUWE6h%wCR-p;?0nTg5<*s?zS0kQw~P-}_3s<{SR=wg$I#JXOfx41Byi=!*H z>)HPT-|~UInC}vQ0-joF;hoYH6h`nZ)#%4=zHq;8>%piQc$XWpp7PeT8?$7{|LX_gY0S{(X7V^`b%~ zFW?TK{u|PcO-m2Gl<}TE&!d%~?@={K3Kx#umV)c0u~D_Vy5YZFe*TeyWF!u}av&+V z7ElT5j#84jlecT=;jM1RU5+^l(p3IMGVyu#PdcX<$zclQH}654MGJflBh>-QsTCxG zB+;T@;CI{S_K?TbaaP%qQ19y&HOFGIgDnTd%4E^=7KWGU5_&Z{~#0D$}Y3eMmVv9~DDiLSWy33ZI}aC33<3;GsIpAew6 zLHhOZ(cobTp4V8r{pCx=7>}*NaIhNTkP5MQLtxQheNn(RMWY-`BKPIRaB#Be zNN{p)l)qr#TtAr@gOUm*v8Yi(@@70zi;~t=debC?zV8DiDy3<@6>E#1=QSGKd|Gb}kWt>^m6*~A21jS)VU-GmdY(G&a3V__Nt44>V2hlxKzr=zwOYXQo@Hmk3D1c3?R zgkkR-k8#!h{C`ai7ocMVnudA}nnwv71X6^vQP8mTP@rS=n{!BOd`+Q?#(*$1o$|e5 z<=?dXhPP>;Z4Kg|Ub z9(-#X$HCHzVVhx2WueC#IeiLSL8D;F^rASEQ2!G5u8V3qbI`~3Vt49hXUY_9J|7{t zhQ45m31yqg`15wv+5n@Lv=_@0fEZepGr(x|GDvBksWu7s8a9HhZbI%iqlC;iAfXS! zorIO?6V#n;;;y2{B-cY{e4#5o5j$>o;PDw7k%H|UpzENzo12ACe*@+Uu^hUJseFI* zxbgc3L&n9h@yW)7%&CuioQOca)!0V0f0|*}3ZEHYST$(bsaO{`xmK(_H{|PA8XeQ! zbx%}lx8gur))SsWNN+S4`z;!RJsN;f^jJI)dnGvQnV?|lz8E~e=$w7}y`uAHgy>YK z6FGmVA^}L*ylfTJ6z!OXsQMit76_f#V=_cdA-7QvBU>G&uG#ra>v*k zfbv@uJ|4adGBp6*f1=}^8UTo=%`Yq~&+|@BP(YZEhhJDoK!}H5T1E~eEDe(3k(Cw} zmY@^+KVM9+xmBz`+j`p3@$&G}(Pg}Oi_8LHn(E>m(xiy|c`u$$_a@oEa>nvy&5KJa zV%3}U*f_*dqfEnUgw%@UGg6(Bi@cIRzWQ~}k+{cna%lmh?u14NPt7ye*|GGL=0gtq z$a;wLa8(AhbN-S!_SaiN7?E79*zeOa{) zmR@X!;NSHZFi9-XMl1l#McCRPT)sx^7Le`6<|y~I-XoI(%r7vm`s0S4&IXsUoWS`x xL$&=DwJhiAhT6hc?PoTJS9f^{1qYr#tIWo|X$douOaN~%d9az7VF|_~y delta 8998 zcmai)Ra6vi)b8n)?r!On24P4+q`SMNbBKYVLk7vAyIX4L1`!aHk{%kQrNiO)U*C7m z?YVm{-iv3gy?@W%Yp)m9josOeox+AJl+}!f%mF$zKTe|=_j>u>k8+zut2^SoK_Jnt zpbhzIznuE+b@dl>oVelj!69T)`gD%hFTq_0GKt9e{5rmD_K6*b%lT(V4<7<%)X#aS z*6_c=uT;wJvWEKY~`LYcO}7R5l6VeKVM6`zmESi(dx`P+9vuUsAst z4Pk)L&a$WxT1u@{JRS@jv^q6Tm8`-p0_p9gnOdS&d6&r~)e<;!UJ6iZp4X8oVv#DA z-PEOZTS4v^3g`q<+Rm8vTm654A+lAufGq|S&Vd(=3}HC0oPb8g?;>QahjD%enZHRZ z5rX;F-|#Iq@RCwynel%Ux9*tWSy&JtLi|84+sn3-4Hj?dseNvUo@*Nmrq>~|ZyDBS zXpudN&&XjGQyc1;keA0l0jdR>mh9SK)@Vjcf&_eA$#-1$D@PM|>ZYbfM2;%eu8#ce zxP6?2{?}=%=5ldSxqi!-ss3Q6m{7TFt9()iq$(mLi&Lqst7%_RnvZ9%A+dTtYat-9 z$&RY6%0e&mw=!sL5heg$lYq=v`sdv_O~m!uCSTyFIx;{0pUzc8tv*Za`0&wHKU;IQH$!OYX`=s!0oOL)7;D z0|7L3%>J`4i5Le*$E&%ZPy`;=Qsk=sy$pT%W@}64gwraY-kcV$KsMNPUymi@2hj7p zjsYrGj!n60Cg6iUD_PDaU5Fe0?ZfMOlsbT=pPJLWjVc*Vm6Z&pt)VIxB}hoFOvr5X zcOtP?kxnxO#Wk5@#oOIsJEh@wya#_kgjKXi18fSv1_=$Ll=HyWdX%`V!0>A1E+Nr5?fx#| zBF`o)od_9p^m#o`sFi(rGKk|7IuZ&-G5U^l$(t;!IIKE${PTFuYX)h#Hm^vQ38R#8 z{n7*!2s@G}FsX+5!^g__g}QAMowW3ZTfLN3k$*ODvuzg*6%MGXjgeIc=(I%g#~5)~ z9pDohV>ONJOMd{7WS#@**KpKEPDN$zG_#*2jDs1f!$#WhHubh>ki}SmO&*7VZm}g5 zswj3t0lplZ?t?;c5iYWC^-+->w)t14Z(2HdYDBnyU@m&v@Ijmlhk0lXvmzB!>v&rk z1{I5*jD(1@L7LB#aJRfZ@24!IPp6uHPDi-LDC6`eZzPOHUA%c2#0>`D7)O;IMp-ci z4sgL$pcsgdf{ZATM^NU!{ElMhLrH;aR*{L2$uU}QurnLkMxcV34E`%k;FuN> zbNJVVn-YxfU9G$_p07JK=1PDl?$SK{8>cu{N~7;N&Z-~efjwj3wL0SuGivYfaQ)g^ z3odiWQdrj_4A;G&$FBfb=v(I#fj0}gCU2d3Q1BTA?dC=qf5PWt&o zBiV^^DrA!y-N9`BqK*~JI47;dBqxTSuFwd zhOfAAq_vP&6yI6smkqvsKOB1a8J0QETBhQ{^R+%_;kphyC3sv@e2zCik6_)z&y%l8 zVhTSI2d3$Qtbe;qWQ5Fepc4+*&6j=-4^xccgbEqYlBgGx7y<5Z*i%WiB;$#TU6`*q znin0QKuI~I{3>>yoi~|S*QI(bfI;Fef>8D}7cDF!t#SRt1QY^YxrmGkAj$=LhpTGf zXiFJ8m5jPAz-7LU{WZE>SaglaBcC;OZXw!Qgl-%t&6?{CT73L=CF+7BXEmNS z_sclla(%R#0qlBfC4gMb3EGZ(1tG511WH94nEQ}3FXt;9L81?zj}jsuq{gKsVh{>&pRcQMB(sZ& zZU<3I&R9)PYoeT?ajT=!8MQeagp<`yw1v!Cq3?L~WRKhsrRB-O*rDoG>I6n)aumvr zk~PqsR`PD_rC>(s+BlS~U?YD-1U}=y4gH|~h%*-<3~n2F1;HzR@(dcMrs!dR!1>p? zTH5dk9PwFY19T)oN(>#_uZEty)vE6xpn0Pd)Bh+!|3{I&!X{N!^hy|Jfl}FiOe&&kc6AZE<7fqOeg5MrxeY>^H9$yjd5?gve_>*yDdVy|D;#{JVl} z0ARew^|Tky6{+LE^4!xZT9;-b4`dUD2EJR;S2vz?W0ri{au`1CrSI>8x47f z-!K>b3YDfWO#njfA6CT@ik~WM{)=7u+Ga*EXM?#G6ypB>a>lW4e@q2AKrX`%We+W$ zOv1MM+rI`5BCOdAIV0i1AF(~Yec5FHtMZHeFYI$9Y6PF***9>f%=df{q(gqTF4S*S zq=HTcv`xs|iNeHkc|>vNdoi*7W9hzM=r3cO_PZ@>+?T>`P(Zo#tMVWDrb^`SgH~~Y zJ!i32K}_`PfB{C1vvfu97U95p__P%?1$^j{(hOm1nCA{xDZwuf$HoMhalvLW@?9&i zH?Zv$%u*(X6$=-xOOn637+t98*l)w!hMUqs?b-^7y6?H_e7j$@q~;WE{!~>6Lf%Ag z)LG|mhx2*~Am0vN;CzEj3E=usCKY(zQzuAuNtX)_9&)7uhd!#iCb=4aXPv{C8xh}w zs*P2{s2?o#f4B$+3+Hb>(m2c+LbAI|lIev*+d_`x=Q{i6%8UF8_K9Z<5WvtosKp0R zh&)MKxgE^w^k-C$dhHKj*CXzfrNsxwxf@%J25%evOHwE!R*+qYi`UL_kG~MFg)BWd zDv{|eb_1?5{UAr;&bKnWkc#6Yo3}ZG`O21`980HNzWjb}a+ePUpUp+f(P_A_K0!iuYb`fHAD+>hEFNo@G+GkH=3Mp6{7B4r%#K#aS1e=z zC7smMfcm9{mWHFH+{-df=^};`lm?i53XcCOu5XKH$!4kK0IHmRQ9vCIBHV?B*9L9K zA@_Q-Q@x3~kbApc&fZ#!>wJ}i)#Y4sue_YctQ@wc<-)l~r58NY zbk8WRZiK*YNmc6^lT<;ZJZk*pIWp>}XAez*ED@%JbTF)&7D?`6M*PgGA1kKzz`X{c z&g&0^G^RFQG@Xo+xeB|P!wI14f?+OhRYZkdR;X^p;@jHPPJPuh^Y`s5AIXS2sMobL z-a}RkYJdK9Ut;sr{qswE9`ZSrAdQ+`$fT^9Nq;g{6?%__wXp`j$Eo{!=-(>B(~d_z zS`GPxag6IpIi=HD^Zrd!rum1kyoN`>0WGD)B`$dDaDsK)vo&MH?&#agJWc3VXJnko|?R0 zXxl>F4s7iLCP^Ao8S;jx$-1%yvnoYO#*G4~vsNZ)DvKT6m0R==1(GD>8GtGt11{KW zHY0e1^x(WDmII0<-GgILTUQqWpSMu(Hui<|V%g2Y;bT`dHx@10f{gt_!nhqz#&tC) zf-I+Yvo!~^7=vEM*>(+|$bHxHO|AkT9xXZrv+n4)U z>?QMcdNP;v$L`FuA1*}Oy)-lZ*jS!ZhlLDL(1y}DX8vAk1iS+zNWx%w5Y9=4`~5O) zBCreSbg{!1Kg&555?_3JD3wG8I4~njDrJ;xH7vc^?pq*F67}r1w=}gQPKTBEG{T(%(UuJ!VVk|biT$cO>vDyukNC1ghmGEGRq7F>SX#!{JGL-%bhO`*w z$ou7BKJY*y{uU@8^SZbJZOuAlt6L~)cZR|T>v_+&XJa!PD)~OOXC{PI`a8j}N24zV zQ>+aIT&#PsMuP}3%OM!#*?6w(YFX=Olcp{IbM57oS9dS9N9N>&w6qrFBO`5{U@^e9 z%ixzVw7=)C^Pli`xC#4i*j`Zw-taB`a3}^UHG3elIPa{ZG5Z&RS+5F>0uJS*Jx zZ4yOU@;SSB)CDm+rg$;V-ld@DG-!2de6SyBuzqonjs??>aZOJqMv42}8x23w6XGMN z(TT`(*8SBQ7Ke(039%YX62u!|wm*GoI3v$pZtJ(uSj^p9vxGbs&gXw!&6f03D+Nsh z1x?rbZaUzJSsI7W=?n|^%=>9Z(@yKDB9a6Ql;F*GLn?+lS^7#zO@YbmYc7?BDsiMV zmxi{02B=L3`EJ6)b2GO$p_OeHYeh*!gaAgG3~!&r5UDzd$$LKO9Jp)(kE=wf;34+8 z+gvKi!%c2|A15f@(IjQCcacwu0#asQUxXO0*Brf`JfdOXsIEQu@dY(hl&bS)K1ddg zqwBSr4vx;X=KM^P*6i7WR6Q9xH87jQA0XRTOmzfx5;I%A+=-S@Z|sc4ATxtK4byV)?| zRr?tbtR32znIp)@NTqg+9{I91LpiO7!@oTH0i^6o5ghTrTe`IFrog68>4Uclv9+Rh zB<-Onw0in+ImKQJmv4A|2O`Walaag-w~lZCg8Gd+j=faSPd>(x=7Z%Le{Levy{>g~ z6GG|#9Z*VtSUo4QPidV*M4h$oLeHkzV<6uXbGpeD}A`QC;aK3(vqOTY{KuF2dIWIK_}K z%VJE!BAh#$?2*6Xr2$d&YjCu=Ub$nBL~<|D&R99mRu5T$KODxSK*%eG{mk=ZPSzwh zfpW(fQZzIAxBh`nKR|&co{@R*X2y|Q+a$%t$RtI+QoO0jW*mx6+yggkcax~BTs6l6 zoJVbC?GMRBI5A4npR0PsOVhjl8`HWl$)6nd?jk+KMVWjw&C1m;kUKP*pUVY1G30~9 zM+xx^x@3E~28{BQQ)173ZJTm-pI#}}detYz(n3dX91Qr2K^V#-szzUuNv&k=ue89u zPu|z&FUAo8W1zJbvQe31^#g3_MvIO7q0`d2oYxWScFiGAr@noC63rQ{qd<>JjMFy- zGEtSs84wMt-z&JyLzfWm1?LUZbF=}l}cOpx+R>)kAS&7_~G=VF6I z=}iaBuNU7H6dHT1^%(klCxgEcVIe~awEM$8HWh1l{bL!26zW!Y>P#)Iv$Ev@+}?IC z&LZsT2>w!H*V<>o<4~E@V41(7V7`AC3E$q$`b!cxjZo1$wmNV*|N>|FR;@nyustU$j&)nd7Js0a!ZD8 zH@;T8wEbFVMS+b0Q^|Rf4#5ar#Gp6W^y&bABXVbqqV&d@35sPxk4gyK``ndDiDc21@T%kwwB}E!lNF`M&PY4OIY%; zI8x*;<3&BANu{AjnDWVkpAD^jQ2sqBr42}5Wq1qq_s^CXFib6&7<0LDkq0EyztMJ0 zZP=5DUVWPoU_vDoHfrjtz9q`v#+Xa&9y#lqx^=`v(1S7zLw8Md4R4)O>6;E-ED?*v zmT1r;#@`!Fwg&y6>4^NrxV|qO@eJ5^*9?`k)XWqsy|lYq>2TEd=345DM2U&UxCQZs z9cx?^hAPly!6ismYu7(-n4Tu@y0p<~*~TB$`=gq?BKx#(X4KTSl3&Y7UL!p0tuLkX zRJ$HMU$2&Pk~4H;(2bjI`pSc&s(fkevW}y~P4M(XJT%&QzKZUr5r2nzcCi?I&;P4? z89rLtXj&JoE#Rg!E!ijCHEKdFZE9f|(>B!6>Uu}n?1l> z5r4@RLbYi3RLy4d^R3qF1Ar8D5!8#O<9S|;S8dTd=-aQ`Kk zrEhh6ObgK_F_1};O6JF2R`3d-+DH%#5Z4-g3i^6m(Df#1!F|eHIR>jsEhbIw;5*_v zmYNp5s}CFHJ$k)ORW9tqUpG)Yy+&q7qKp-zC~(oojqu)cb%*XMW>p-9w(11pY9C)N zO#EtHgxa>>MqBs+lq4abgmU3d7|!U{&xmP6AA*Z)DO+X|pmr-K@a+6$EfP&yWjSBn z2b)z7!=a$5ya?2NtT%gVhM2uv7S(p1EP)h9GUo!yNMz$i@iF#bJVi=oXgDLlGd&&Ir zFp~$Pebxc9FqQnfM{w@MGM9;Q^4Tok=82EasLaG)wh5v5SVPfa5Ei4TS7CyxL#$85 z5`tcp*4@$q%7?+ZB%p47#m>mKqR4>q2<#e0A-zb?G%fT({8w7LF9RHH@mR^H-TNuCRSap+ucFbYHJ0QSuUGC--z@y;@_S^SrQym zOakc=Tfmjd)gdQj65e4Z|D&H2xy}h8zXpCvtPVZg8a1;YoIEUi=Yr)Vqv!0v} zXT3A|&*DQoC;1+}N*bqgP@AXNXcT{bIU1}gvI7RAM-e$1OA(!(0}tU|Z&s_nX=fknzeN9pjaA@f$(SKM507uIts%Ec)KFsLk{uvkLxFg|@)1?kB~0R9sEs zyDG9krbVj1^b`dbtiB;Kd0fx(```2F6DDHLOcl07L3W((Q(F@;9t2Y$^=CEzy+>WG z;ilQ)0t|1OXjLJ zFVHdZ>#cd54HthitTuU*vhDePSZl~SB()rs%G&o{VRH?6@)6_`)cZ#amL_nyofRMe z!Vli-57~Bxrk>Blj7klE+S>hUbob2=-*BlQq}RAh*ZE?l5Wh22=P;U};K5t6@X@Cz4Ml%zZ-F>C|7g=%334XbaxN)G1 zJKHO=7XJeLa{;?TG%CBsyDg}?5D)v6w`cdq zonSYp-Sp}bI`H`=8&deG@}z>GkkMw+@zQC~^ZN`}*gD$=g$wlgo|-HEfuXq&QEG@${@7Y74^R$2D|L$WwOkAFWr*<7(&wVH zZhv~N9BH;Q8V$D~8kQ#s?!%6>^v;kC#&aTSI@}Kyv?^H=v|`TMDu|gi@;2zFitIcE z=hn-No6SOy6J5OT4Fq^>dKFJc!^{77eE=;8TK#Vn_%6pGzyEulj2vr)1Qi!siY@hH z29BHZ&-a!z?#glHO-9{O`uBz*l_vO}*)znv-fp=f=Cn?^O5O$-qo4oSt;DcI4}b@> z^A8(3H~HTKy1?guzu(bUVW8Fx5}LGZtp!Er7Q`&6 z&wiXT*wc>KqDI41V@`vty1=H2KB?TN#nqdmQ@GFF2` zC4qrok&ly21`Sufg(Agn1fYHX;T1UnCdRUp7Iqr~U;d#SZD|Vv*@Feg`rB|qV_|<} zLYEgNB=v5?5+o+y0PLYiL97hjU_rc0ovnlRo40rtQGP>K6V$-Sw9tQ7f#aw_`eSlJ zAq@UON!zCJoIjzIBM|i!T$>a)CQJy8O#&Ny4`ee4Wk-u1Q{d+=23a63(`3((;r5i= zAy?og1xl5B^O)uz_oMH^kap1e5(OOYvl&MZnRt_D6~=(FJCQ}>mr@)8)w{&HfeQN* z*ZyCivZMCQZ3GUpeAE1PhiZsJ*NL}KbFkMN9}!#m>Hm@5GGoCX*VrgulLR2`;0afe zRUBnSW>7jzIQbC;QWGCqKY)zQ=AFoU~4!5TjB)#Fw<)!>@r z$VF)2^KPT&W8Q}51q-J5QYEaRNoK(?>I93Cg`J%Zl>DeZAC30f2NdwAbyhC;N z#NI+-oiAwoMR{aG1}Y8ryB=mIHthqBDQaDq-i*G*d7e3K6gbp#Z?DZAG9l&Q;&7 zI$A_Jbf9F1%>?a=eBT12zBQi4-~)tW5OI-sV`{Xy;>B$+MMLB6tc|#*I37f!4B;;1 ze5S{)u-Hln*MnJJz!Pr>zk05P4*2}uu$39hU`D{bpz>Y(+UG0obL0+LzJwmQ4Bz(V zK^zpa>;AGikk_^APi_&qgH^!6jSi3z2Rwq}HqH& za~ytkdv`})Cq^MbLB{|2HNrL}p@Skvskn9Kr6eckX$dex3eY96DjIX|NSPuD#9~36 z93e5nphudV|GG9buNBxoVc1ydpqz?G)hh@W(yRMjS(m0F_ bool; ... } type ('c,'p) unsat_state = { conflict: unit -> 'c; proof : unit -> 'p }