From hogsett@csl.sri.com Fri Jan 13 11:32:16 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0DJWG6H071430 for ; Fri, 13 Jan 2006 11:32:16 -0800 (PST) (envelope-from hogsett@csl.sri.com) X-Original-Received: from [130.107.14.235] (rogue.csl.sri.com [130.107.14.235]) (authenticated bits=0) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k0DJpegb048408 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 13 Jan 2006 11:51:40 -0800 (PST) (envelope-from hogsett@csl.sri.com) Message-ID: <43C804AD.3020903@csl.sri.com> Date: Fri, 13 Jan 2006 11:51:09 -0800 From: Michael Hogsett User-Agent: Thunderbird 1.5 (Macintosh/20051201) MIME-Version: 1.0 To: smtcomp@csl.sri.com Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.030 autolearn=no version=2.64 date=Fri, 13 Jan 2006 11:32:17 -0800 Subject: [Smtcomp] test X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 13 Jan 2006 19:32:17 -0000 test From demoura@csl.sri.com Fri Jan 13 11:38:17 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0DJcH6H071560 for ; Fri, 13 Jan 2006 11:38:17 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k0DJunPj048820 for ; Fri, 13 Jan 2006 11:57:42 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.2) Content-Transfer-Encoding: 7bit Message-Id: <16AEBA36-2CB1-49A5-A9C8-A3513503B796@csl.sri.com> Content-Type: text/plain To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Fri, 13 Jan 2006 11:57:46 -0800 X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.004 autolearn=no version=2.64 date=Fri, 13 Jan 2006 11:38:18 -0800 Subject: [SMTCOMP] teste X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 13 Jan 2006 19:38:18 -0000 From demoura@csl.sri.com Fri Jan 13 11:39:31 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0DJdV6H071585 for ; Fri, 13 Jan 2006 11:39:31 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k0DJwuWQ048985 for ; Fri, 13 Jan 2006 11:58:56 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.2) Content-Transfer-Encoding: 7bit Message-Id: <86EF8C74-AC6C-4BFD-9287-0ADC07356BA3@csl.sri.com> Content-Type: text/plain; charset=US-ASCII; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Fri, 13 Jan 2006 11:58:59 -0800 X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.004 autolearn=no version=2.64 date=Fri, 13 Jan 2006 11:39:35 -0800 Subject: [SMTCOMP] Testing X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 13 Jan 2006 19:39:35 -0000 Simple test From stump@priam.cse.wustl.edu Wed Jan 25 07:59:57 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0PFxu6H065159 for ; Wed, 25 Jan 2006 07:59:57 -0800 (PST) (envelope-from stump@priam.cse.wustl.edu) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k0PGL9oe067674 for ; Wed, 25 Jan 2006 08:21:11 -0800 (PST) (envelope-from stump@priam.cse.wustl.edu) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006012508211000316 for ; Wed, 25 Jan 2006 08:21:10 -0800 X-Original-Received: from cliff.cse.wustl.edu (128.252.166.5) by mailgate-external2.sri.com with SMTP; 25 Jan 2006 16:21:09 -0000 X-Original-Received: from priam.cse.wustl.edu (priam.cse.wustl.edu [128.252.165.90]) by cliff.cse.wustl.edu (8.12.5/8.12.5) with ESMTP id k0PGL8Vr004506 for ; Wed, 25 Jan 2006 10:21:08 -0600 (CST) X-Original-Received: from priam.cse.wustl.edu (stump@localhost) by priam.cse.wustl.edu (8.11.6/8.11.6) with ESMTP id k0PGL6805641 for ; Wed, 25 Jan 2006 10:21:06 -0600 Message-Id: <200601251621.k0PGL6805641@priam.cse.wustl.edu> To: smtcomp@csl.sri.com X-Mailer: MH-E 7.82; nmh 1.0.4; GNU Emacs 21.2.1 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" Date: Wed, 25 Jan 2006 10:21:06 -0600 From: Aaron Stump X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Wed, 25 Jan 2006 08:00:00 -0800 Subject: [SMTCOMP] request for comment X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 25 Jan 2006 16:00:00 -0000 --=-=-= Dear SMT-COMP interest group, A month ago or so we sent out our current working draft of the SMT-COMP rules for 2006 for your comment. We have received very little feedback as of yet, and we would really appreciate your input. So if you haven't already done so, please take a moment to look at the draft and let us know any changes you think should be made. We will prepare the final version of the rules soon, so please give us your comments no later than February 1. The draft rules are attached below. Best wishes, Aaron Stump (writing also for Clark Barrett and Leonardo de Moura) --=-=-= Content-Type: application/pdf Content-Disposition: attachment; filename=smtcomp06rules.pdf Content-Transfer-Encoding: base64 JVBERi0xLjIKJcfsj6IKNiAwIG9iago8PC9MZW5ndGggNyAwIFIvRmlsdGVyIC9GbGF0ZURlY29k ZT4+CnN0cmVhbQp4nKVZ247bRhJd+HG+Qo8OYHHY92bebMfGemHvOp7ZDRZxHjgSZ8REEick5Yn3 6/c0u7qaGsnOZoMBRgAv3dVVp06dKpaFWJThj35Xu4tfLy4/6MXdcPHrQky30s9qt3hxjZvVQpaF tdIurm8v4mtiIaQpjFxYUxXSL653F0+v6rEdntQ37bYdP39z/fOFKKtClw6PX68vnr7r1odtF647 rCYMXb7eNF3fNsN0wxVKlYruvOx2983Yjm23DzeXsvKFd3KxlLqo7PTIx6dX767DTY03bSnpzeXL f7x7//EbWlK7tJcsS/ttuGpUobS1dPnDYRv3N7KQli/X+3W4qHThK6Xp4vu+WzXrQx9fqGy4l074 8el3H56/vo4bX34QcJIO+8jgt6X0snCwe6lM4X084bbuf5n2MIWuRFrnRd33zThOhzbBVwJvCcdv wS+HsenDfVsGA5LFV6u22a+a6UVbFaVR4cX41t+ny8IWSrCHH6ZLuiiVrujSv8MlXzijq7RqF22U srDaJlf+c99OF0Uh2O2fJouKSjud3m36gcCA4Cmr/CKf/m3T7et+PUHC+EJ7dvI62uoKoYGtBJ9D X08nE6UpSvnHXaJ9UXqXbrytb7q+Hrt+sm7pJDYTit119eHNdD5TVKVPdr3ZY499HRBZb6fXKjjP 4v4SD5bxzed1HwGrKvjaJsdejYfdPdkPTzr3J+0ndCIXZinzan/X7pumb/d3cSsliwpZmk71w+RX WSjjUtDqYYOnx2gyklnJqvp/Y3wM43ZP8HLasROKacUSATRpybfdoR0oZdQCTpHC6CllVPDUIuRA qWBVeFhQVJxnyCIqk+MkjHdCJNSuD6tEHVjYLISAK0zMRWMKYbCytIWzpUhERKe1lVfs5f0hhjrQ gJMJCSdcZ1Wh4boTrtNlUVXqHNlpLKjY3EdkZ2XhhZBMLERzEmxmfdplRnNhMWPSNtGdOHCpVMqf TbONgFGFU0zKY5cQoXnZ4f7Q05NW8JP1+hMlZSlEds8qHga+1748jvxSI6sBvCUgEPwe3MbHUEYk y4ZuG5euAHx2YUwGnMHpKnm93d1vm12zH6cUnDb2wXSdHNUx5FSVPHuD/NnsiGgReCfLtMdt1+8O 2zqGA5DwnOndLfnFeJtOdd/XQNQqwkErwIGd2wZiaIaIbi0QWJmy4/3hZtuuJgSpAlunHVY54NP+ Vgd+5OzuG3IhgGDU5EMd70xkiqImRTrGQ7PdLn/ZR7zBH5mwHqI/PI7BYNo1ddwRiLbKPTqxBg3y iYexDf4ZiU6MAxnyOl8ERAjQZAriaaw6woRAmsiMtO52nGoQ8lBXUh4fHma7UlhGarcdCvKj1pw4 ryMhaVfJBP+uPz3KtGLIet7ltzqg6Rk5zehH6D22tD6M3a4em3WMCg7tpgqUotI39dDt4adnJC9k yVwxbtJxpMz5/vzqJQXBucqcgoJKgdUM5Fs6lyusVMmwJ/0wLrt+HdPFCJSc5HG2aboDDs1VZXIm Od4bmd7YxFRAIkI5JD8NTbOnSuMzsoaxqdef6QTCOA7z7r6fgCgBOsk14lN0v7eVSU8yTlCjtJfH OIncIdScPLIflWYUDp9hyW6gvDOZapspJaOC8yEh0wZDS/UUFkrv/EmUZqufxsP7GbEQQ0E4pFXu 6j0VOG/ECfTLzN2iqixRoUFy0tUf1U8FUS8SLTkvVSao01yZrp7TopVgPrtm2rdfRpSzZxDlNHMZ 4nffDe0yhgH2Ra2SkJ7FDzi/sgzdL9sD5Dm250tkP5A6NdmQhEaPgsxorLdDR84ojbGPMYrtbcZo u2uhsAljCAhdjzmKLMpqauh28NKO2gCsolj+rvsamd+uIlMgXI4F0h8Ee2TdoMCZlm77bkd5iICn k39u6lSBZ4qGajVkDKPo/IM/yogiJFFZGOtn0Xu+b1brbowBBFsYKMFjhiyV5FT51K6T+ISYNZp1 3HC4u0O5G4g8qzIzy6YeKQOULw1fbYaGzllZzrkzNVDqXANXI4ECAje9QpgAZVh24lQSgWFUEMGh v9u3T1Z1ZBgTxD1nRI3jgzWIGSrj/aN0QDXJBBuokg5UObY8KRHKEgE0OXtEVl0fq1VgWF0lj365 WkFs5RPtuj5RlMjuavdBsNSzXBaOmYekDwypOL/PVp5NO6SuB1isWEWkhiKck6lr142pB/CCSZ4A DmVmUq6xVXLq4b9as5IKVIURbP8kZskokH/a6ll0mEPno48hcOSwIIGoSClw1leePOL5ZCa022Eb 4bzUIUOtnCVNPoTyDERZlmYyTiHHNLd5gEUdoQ6ZoiQ7AgxF23rB6ZttEaWYuWzcIDOocKMTMMx+ P6MJJvZV6JOc5bTowVDbtK/m3upH8dMziioEFmfWmVQ/E1KQ5w2taZCYOt2YkZZT8tSxIovEr4ca FVs5DvVDc4NGspkGNOjY3FHHFgqRK/U8xTbjeP/t5eXDw0OxGrbF0LcF3HZ5GFBNLuOhfVAEiceb XXegw3iuR319OVCmWfbmblymGuNSWFZ0ZoHkTdfuL8nWo+4yDH1Y5heRm1D5OXvezyGCGsgxzKUN tGxPgGOrE+BAkGdhT/4jEAvAw50BceACzsQOC/V0fPc1orHmMdFYkA8Tze+EGX7MwiUM4QoSjspz 4mSR4zIkQk9FXgclpKvnWpVxE5ve6UkupOtudUgyE9VOVixN1s2w6tsbasVx+uzHDGSfWbNPM8LQ gpvMMPs1V1pp5v5+JLwM6mcWXvdHU0QDZe257OUqNNNCv+Pgcq4Mg4MJl9UCCHGBW4BLcKOo4ES4 PSaQOIde2K8qKJwlP1ZQzQKEzZ8wJ/R4jpUujShAS3lEUU9x9UHfpPR5sm1T14W0dUpwZ9uOGzLB qeo0L4Q+Gq2k4VrQb3lOQdXbopc/bjWeQ/isE5lqJsl/xWRWQjAjN32QGRxliZaap3Ef0eURkiok ZFokTmwQ36r0WQntb9GuQGw9I7RUWQ5SGTvC+z0Yn/LFZ1+fz4wzcH7doGNMnkVm4Ixpt7fdHc0r oJokzwlfsoVkoCzZCSHEsRaKeUrzyAn4FmeHQ2KeMVdNPY7UkaswD+b24AfCCnrbXNppbFkQiI8n hyGjKwtFBizG0aecLDkaHL7aj31NsvzyA7TjvOCkR+OMMBpIvUsUQ6yb07RB+VwhpzMUDvosT9FB qMnY44yDjjMmGfU8jWxmbWgTDc2SjXV1RwJn1ln+bsm1gvHCg0JnVNaBdB6Ulsf0g6io/21uB1hK Lr3D4WbXjgltEJiahyPneuOmTWUJ2qrK8+gB6oe6kTCMNbk0r1Nzoaw61tXAGbQnGpFZdt+0+7pP swtnWFjGokdeLnM0bz5TwsosrZsd5BGZiNIhHwfE6DMqb5aA0boKmsZyvtzV+/Y/DfUNcJPKKuBF NtkW1vN+RybLkk2ePD4M3FgFEcm5sztQVQ3NLEeCxhkmzAode3Z3D3IjFQhPyko+ZuCl1tj6SDCf 1bWnkwiD1RJV1P06TgKrMKBN7+RJoMiTwNyouDzs6u4Dn5FmRvZb43nkMI2IIq1UUHkscx427WpD TOeyFH5oqZeAbLGszsg9AJ5l9/zmLfGBkp4/LLX7w28FhcTlL4ez1u8IA9OgMY9c50nF0wMaj8D/ lvP0KKleXS++D99v/cTXZajefuHCIn4h0I6F39Xu4sWbi8s37xZjf2guLn9YiIvLv4Z/L96/xM+b 7xZ/uXj1Ji509kMwXAT6cQqunX0J9gZJukAOhOjvWFagwQ0DImknRobSNZOsQDM213sIrc4fg1eH vk9TQYHWl5N5LuQgJ0WGaKQwqKvKMDRpIABpkRfo69skJS0zyj0UWBgUrokaRa5ptzxFtpLJGRhm K8JHKf4sxi1RmNGdlF6DhfWpVlYc4LDuYU+fkjQ6szyUIPXlRMmfd163aQKnQkeaFl43q5YzPpqX DCHNHkhZPpa5aO2kPpG5yGp0CshpeZQToeNg/PIA1Fueruxq4mINBuWcIAYN32pO9g/fB/UxLWJn 63l2lmgxZrALzdsjKhDhM7w56m5xZRb9J3AY1lhTVnommCnXUOpE/oQRPmfSKANul4+1FVjHe3Ny BnvGh1EnpMt/0oV1tDQoeH9sPNowcaZnB5OW+bvtuQj8rd4fUlUJny9VuqHKZ0kDODkbeNiz+mUp PAIWPlKFsjw9K5iTvr/4L878W8BlbmRzdHJlYW0KZW5kb2JqCjcgMCBvYmoKMzE0NAplbmRvYmoK MjYgMCBvYmoKPDwvUjQKNCAwIFI+PgplbmRvYmoKMjcgMCBvYmoKPDwvUjE1CjE1IDAgUi9SMTMK MTMgMCBSL1IxMQoxMSAwIFIvUjkKOSAwIFIvUjI1CjI1IDAgUi9SMjMKMjMgMCBSL1IyMQoyMSAw IFIvUjE5CjE5IDAgUi9SMTcKMTcgMCBSPj4KZW5kb2JqCjI5IDAgb2JqCjw8L0xlbmd0aCAzMCAw IFIvRmlsdGVyIC9GbGF0ZURlY29kZT4+CnN0cmVhbQp4nLVbS2/bSBIGcvSv8GWxGcDmsN/dx0yS wwA7r8S7e8mFkhiLE4nUiNQ4nl+/1ezq6qZIy84CAx8MUFQ/6vHVVw+VBbsu/R/+X++v/rj645qN z+K/9f76h7ur7z8wdc1Y4ZTi13efr8IX2LXh16a013f7q9dN+93d71dMFKK0Dj6821y97rvTcV37 50IVXCiGz9fdZnzKdaFLofDp5+64vxlfLgulmcbHw3Z8l9nClCyu0B39MwePtI673Vdt81d97P0n UhRGaoufPDS73bgfL+D1+HRffRkfloV0pcGHdVhXKM7xybGu+q6tVrvxI6UKxm08cv3ZP7OFs07Y dI2hx9uVzMSFh24un7rtT8cF+QzbahhXAInL8qIgnhPxrZSycEJc3zJZyPGjZjwdaFMLOnTbjRsy V5SKbrevUE0O1MTjoQ+n1a5ZF+OW/ihW4gc/NG11bOoof8WsSSIZVzeF5iKuUwWdMFWY7Da7P/Ec 1tGOoNMb1JRmPIpj2+E1jHDx+w81Cllr2mdcUBVWOyVowaA2Ix29Nu6g/X2MnpuNKMlsVmEPkKpl 9gWSGgUF4lAurlt9HsIJuCqUsHymXyEZJz3uD/XQDE3XFkGfpSkkN5k+fw0nl8bxqLnqOKAiONwS ronPmxZ2rvuh3oxKcgXXStNn4+684JwM9OAXWjeHamja+3EbUTDtLnzj409347Ze/ySe27e//DSe UoIGlY1qeAgqhHeFIQdcVy0ao5CFUTxa1+HYoblYpqN0/mw29Q36mlCO3LIBWR4RSsp4tE1zrNfD 7nF8Di7ObDwfmicvLNeGlq7QZlVJ2kjediuF35KPevCgiD53g2ZgGI/XrAKkcEGQEgwjnAQ8peRW 0xn74dis8OhSklxPQ0QgwQunafGvViNS2JJW+VfTnr7iu0LL+HjlHfQRRauYkWS940MOBqVID8f6 AEBGi6hkpE20XetMers/7QLsCY+QegZ7IG03M3SpSbTfhuirGjAlKsIAztrMIdL6lrMEiORIoyGz gkvCDfRpVjBJRnvftH0RbciyeKG7bd1HPRhyuOn9hab7Zxhi7DmGKO/p8c1dE/1yNFoZtUOBVSVr QJOShjOKtTU4azXUKCuuyRs29b5rwayqeHfDQfuZW4TFGMQlScbf47uAXLykTbrPiH1MJg1vUQ8K /MdM/WGKXQAeRpm41s9d8i/C76Zto75LWI3QmcTICjUTo4Tbkhg39XpXHRHgAFmsJH5x7PaIFVzx uEYFwrlHvclEDuoWBNYO8ShGiUuoN2xDUIUIxTUt/bRkA5QLbgoH8SxZ7keMf96dE3VAiTAAnJIi 9pN4uAkIND0tREm5RMsgUhriDJ6AVRF6uSUL3J/6AV3eGEKepl3vTiHsgQdqQY4zGqcpIBzxuPKH 92/e/fR+DMRgJFZHRHoVIA2MwCgyyMCzCgYULN7r62FXNS3GIAkmY2xcepEG4KNSJBbZzeXg7bMJ JwAVO8cIsdsNmjToU/KcO4EjIXEB/9eM1BExx3hakMLFMp0J7EPzxD4KlJm1JprrZVsw4IK0OSkI +IsgBeXXgzUEHevUoyQhTsH14oaTqMQ93OhcowrEyWlxZFVALVQ0k6rZUYwCLirJfj69Jv7HNR26 P9TrBmQZ9lOFS0zyadv+9B2arXEUvsI9q9ugMu7PKXMYirAHgpQJfoau20WaDnAQ7xVehS9b5dhM txlUncUT5cCVXTzrvlpvm7YO8UOB0WkTN/gxWBCBsfKck9ALLQ9whAkyxyWHWCC161NcE/wRrJnY zWcELJdA+0mijUCT8efMuFgyrpgw2IIzm6LgH6cGExrtVUQ5VBdeh2zEes6ZeVS1Xtc9BlovYMKG uyB10BqgMqnnOZYAtyzneR9ooHxB3gfMOwOts8QPgp4mj7ic+PmM6zzx4xBdbELlHEa4ojVqMByE 2lKS6fePQA0wNwbiWhpL63gMjrhoC5ZwEexzf2qbdfQLSBuMzqGM3IJDzmdSoB22eAd1GdtOq30z DCh3BTSBU6RFi/O57jlNAINhWfY6XgztBTKk8xBrUq68rgLtgmzBpYRxaadNEx+CkcQXX62BnzXo kYA2xsn4/s8vTRrhCjuw1RsStjtntBMJvYDRssRogUHWxz8RlcuSSASSKw1mAhEyhzXaUyeWe2zu tzFWK6qskAlmlOVY/w7ZEO4nHaXVVQTAjFMhGUI9MUfUEiVdQjJFGUITnMCvAMFoitHEvoHhJva9 lH41c5hkJakHAoRHjfFAnuVTar0cORaU2ZOF0Zbd/LVFMwgRa4wmhEtP29xocN9/AFTJ6me3wnl6 K3Pql1wBMJkR+G/qfn1sDkSiz0txWvqiSrzqM+k3JDiCzjyhuPAJW4J8sIyMT8QiB+P8EmBUARwV S2DabzGbBM7LAQGIGrBbjidmQsStDtV93WOs96kqUdRMGmgVQvAp7ABrA5dgZslXJqWVAD4Fho0M Ve8imwcQ1un8p90GuY2hNXISDNFAsbMMjWUi8AlePIUifyMEM5Yscak0Vp0GEGE/32lpgQv3xUCb fClRDsBVkRagNF8rimUHj1IIBP4WhPjeXZthJCDVLmgBUMEz1CzSL8TMV7tmdHHEZSDFhkVe9+OA 4CJT+SFTA1A04hckWp+I8POCKUS+JIVfjx1E9D0CsKIE4d2YrPkEgYwt5Go90RktyGr7usbYCdgT 3/8IgBoZGKCSpLUlGkPpVDzGqt51KPas+PUQbJ75VNSmII9YJVLq8rBtAlHw9EFysXTjeKwn0fuh 6bcBCG8lWHXJc15GhRvJJwlTPdSB1YJeFKFAJGs8r+8BGN8fq/0+1g6dT8ji5ruqvT+Bm4Msw6WB QdvyLAMDkBWJB/fd5+Eh4VIUZXWMxq4sibw6AgMfQCFYYIeIoyDfnvqMhDsv+IxZJCiAW8axuR1C 5kJarXZ9l3iuYTkGUc3HlITMAc5W9eYGSZSUZH0VhdGsmlQjofXIlEL2wpvpNi7Z/qrqQz16pBiE dzFowLspaPgMARUHAUkpcsvqAHpFmjqyoLh6vT+gTYMmBYXkxzqqEu4W3/30ui7ui5u4raXwuqv+ isVIzkSqgQ3RsK0mTAbjyvyNMT1Tr8gwlXgUsyyz859r0Fl7+8vhUIfimPA0JMstfdWUeAuQT+eo fh1Dn+daxAU/vkHHcanGNsrXl+hTuX28u/FlUcr4vZv2GeWByJ4KveSPWRnw/9+qHtbFp+9C1gU+ 5ux51gXMyJAjT7wg3fQ8GIOHpBZE8pARXJSzuTNERxnDftaCSNEULNSk4mZOPchDfAXhlMkLIpKm G6JTCJ8PXipG75ovCK/KJmoUON60Qn2oj2OFrA21MyBeXJizlGWy9GUyBlicEchQIAVntVQpmDDC 0go7F/t4Rw0ZckkZRhXL4mOlLU/46nbdnY4AuZsoLSVmSaqyWZKacxtpptzG+kgbRfPvD/+K3I7z rJ+LPpuVqubffahXKCXIg6Pf9Q06vAP9qfmKWR0pxTyrZ9npJoYqzVMy1O1uEGJcgv/xENOC1mmY CyWr9OpEgqmlCikPlV0OgQ0FZuMrc1SxetvtdhCaanSPscSRY9IkLTZL/hYVL61ORJw6DWyhRJ51 Kw8ddRo8iaJEGGtf4KxmVvuCcJayzGezDJkqNqBer8wbJFzCmnmty6oU4/PAKg1fuIZ5Qsc2mV5s 3k1OPW1UTHLp91X/+HZbBcoLYZiVZAS119Sxa0PgHE2J0pTxBH2f8A+S2jyFweAAuDK3YJEc+luS tk8AWO0X1HPK8IMQ/IUSucj6HeAYF4s533KCib/mt8V4AnBvAbuXU1sI0/xpIAOfkmTPE6pvZhRr LFstRg5PBVIzIpYzWOq0VcdVA7E2tEKl9Jlv5hrN0BDHpK8sFQJCVHVZhvcETQkFfzgDgMNk3MDD TYrJOadnqdKeFTGz/tRS6+vUI9UC4mAV3TaWOrLyr+/rEylLxdWUP3umNm+oTkpNh74+bbpb4Cyb YGfG+App6kfuUjoklU8j5GSf6YlWEJ22++r4pV8umABLAONQudP+Qk1+36MkyQTw7BeLJb7wZ13c 890pch0w5Hg4ahS5nCMA0FRkpwAQVqQSZLQwzVzeHDiFb4R02EB2nTpckEWPLbhQSvTQlch4kjVo dmHciYLIWdlb8peVEq1v47DF3ahaH4uIYXhI5qEpDQoxY8/qi5PZJl/XP8RmonB0vz327YH2K57d OjjqdAaha2MLgKeC2GJNLmtXl5YnsNzUr1rqBZfcXWKH/bY6pownY5+q/EdE8jTxgEA+WSG7myzN rEDjUnMjFkn9zFYKJ/ksF2OTWS4shvmZkNJcWHgS5OQkyPXVPp5OS5PneajRl/Qo3UhRoxgX0/4X 1L2tfpmxTkccFjP0VPH2YW5mkVn1IvAFZFXaLtS6JgN73ZwQPrS4v7JnVTVsCijwAD6Vw7TI0EXM OlNCWASDrUtxPYdkwSaN6DDJdRMDdBqMIy6f1Yuea2Eug+5YkJjMmr0BvtVufAq0XIxWPp5caqzE 1rxJlbfEico0HfjsHJlNFJOXpY5zVy4RCC/qOGbqTJmqXktNQYqnwrKzXCXvCWYjfRC+0khfXxMN HIch5Lx3nNUgsaG70E+foFqb2vTSlnxiEqHTECX95nSPJXtgX/AJE7nj83LYxlJLKcjzSGyAKlrP p/rccrnRpnLjrAcopJyJeTI8ua1Q/2WKQU9xK+sLvCnppMZ8Ijzdwc+ondpmGKmcct5c2bkbZPe4 X5rIeXJ7k4aAq/mB8o6GMtTRwBJ5KhkBT7U0gletupBVjkNlpFOCIIi4kH6V+bjus9wcGP9ZS6dA HwF2GT/577ah8UFIROPjLaAnTkT6mQoyglQrCHOxDFSbBkXOr+gLEJRFhgkiDwoum+GmrFkliJ86 jVHkNJROMzWbULZ++Ods4GATLgxJlVBpfAYDrOVUSa/6hKaTsZ7FtAz8Q0X/AHblnjL6ZxrfZLgm ZSDP6pSrc53GuGWIw7Q10n0IW2mKPskJkoX4kNBNJ7c7bB/7Zh0HcIAuyFTHzvs8fpaELris3Kyz vzC3HGTu+zjTsZyFpnSaN65RuFLzM8Y1SRsemidCl/Yh0eZ+9K6uNjsayjmPXKNJ6L+tjarTOPCS Li6Uq1aPkSim9CLBPWjHGvIbexMjv5gEx1jnTbL8iP0rX8USmh6m/pWvOJKGdUBNARaSJmYX+1fo X/BtNml+RAeDSFye1wJ5BqqfT9j6dKAO8uWh2ddedVFz4tonLAx4mVc15CiwAqSGfrrcjl8QyNeN pdH391+zASnj8/YzGu2Bhd6Ow3cgNFVK4qTB5+fJqfLdVwAU0LQNJ3gHJtzjCtZewoc5CzvjVL6I ReTuG6YCM6Lj5JzoZOb38gEzKhsKl4+NzsHzWzzImygGUuZogGlzomzMjwBQfFksYPlohWPZk3mB JYG/fYMSAHyM+v4PGq4tXAYZ2cEEo4N9yvxvZOt0CqZvOYttFV+5pk8+ZPPh1v/oaeGnSeVCdSdT kv9dxAmId8CIMXG8NC9VzTgMDlxiIFHp5xLTOOycnElP8uelZ3zKTOQSf04jsn4GlZdlGq1cXO2f McZYitx9uE0JBJPm5StE19J3rmnYPfyWAYBGpcbxTdCuBtMweUigKoBeaLHK3O2W3vy7yuX4rmaT bkiBkCYZkbd39QGSMXQSpX2PiF8427woBTYn5kWp8VD+Z0PzCZGsUL84YtKe9qsaiSwAX6kmTb8l c4rRM+SxMo/3ixOD5z/jAEKZj93G3nGZJjuf+G3HnCRRkxHurtPEUfUYh4FkSUXVujruGqo+Ok6e mxWysjNkZh4tKvOZiZlqP/phzuoYfjQuefZuF386YdKvA2NinRGz/pT64KSiV+smMjvhh6fmIeBy BIiEjpe+Hg2Mzt9fB7j0H7y/u/7t6rer/wEPdTzLZW5kc3RyZWFtCmVuZG9iagozMCAwIG9iago0 NDQ0CmVuZG9iagozMSAwIG9iago8PC9SMTUKMTUgMCBSL1IxMwoxMyAwIFIvUjIxCjIxIDAgUj4+ CmVuZG9iagozMyAwIG9iago8PC9MZW5ndGggMzQgMCBSL0ZpbHRlciAvRmxhdGVEZWNvZGU+Pgpz dHJlYW0KeJy1W9ly3EaWndAjX+YX6m3sCBFCbkhkv1leZhTRnpZlebojxvMAVoEkWlUABVRp+Y7W B8/J7WaiAFKUwo6OaHWDYCLzLueec/OyLNimtP8J/24PF28v3m6Yexb/2R42z19fPHvF1IaxwijF N6+vL/wvsI3mG13Wm9eHi2+O3aEtvn39zwteF3Vda/z89e7imxf9sR0P7a5rjq39aSWKShoZfjq2 02l/nOwPhCwUr+Kvve/2e7cYvilNHZ5euSWYLCrOalrCPjMFK42Iz25O+2bcf3TL6oKpKv7gbpiO 7S58ThgZP3cc3MK8wGlMfHbrv6aLumI8PPz159duW6JQjLZw+f3ffn5pH0tWMFGLeIb2aur8qYUp tKGVG3dgJgpRVtVDX9sOh7v22B27obc/vJSsLGQtN5cwgfSnP/WTs/qzV5zNPKRhzuzFF/3d6Rje nPtSVEVpahY++WOzvXUn1Hhaqq84dtsfx6Y/Pg3nljwZ5LZ15+DwFufRGu7cCl7iPJ77g39UV0bR qtsTPPc0uBRfi79+OE1Ht2hVSMMFRUWzCzvWgsXDNfZRXVSCvjR1/c3eu4gVupLRHZ01V7BDXeoY r9fDeEBsuUOXhTG0iztEMg7uY+tSImy10M781sh4wXuQqUIqE7fT+cjHS7UWtKNj0++a0S0kRWFq yRZ7qgtW0Z62t03ft3vnW6kKJUT02nc+hxgSUpRnR3BflnA9r+NPKOd4UVbLnENcxnS56WLO1ZTK 71Z81i/TtetDptV8kWl1wTn5ajv027H16ePtEI81feyPzYeQxFpREg/XIa1kwpHVpdej+a8vnnvn SUCD0lnuWJM1KaAF+WrtzOMUslVgI5ICkhUfQvKZjS6MLrEbm6YKaSbNBp/kZelDha9lKfYijDGb y/xN53NggpJ1PMZrf2D4sDaUeA8eGBEuK8Wz8GhclAEXeCmje6e7dts92TYRiyp4tSTnd1PwKhcE wnenq3239SgMB6qyjg5svNlKpKGYW1JLoyhZu31zFXITcVrTVq7H4RA3rni98LSR5Ol//TBsT5fe rYJHRAwpeUDCTp/C+tpQkZjabTzl/AchwDi+sAgwbYP8UQEGoOLJ3vMiIQUlxf/K//PltCxQECIu /Trs34W6WDOtU9C5TWC3Ndk/K6GqXqYz//p0ZpJ+dYYmyoJ9XOCfEZdLfIq8RL6DERRfGlGVVPxe jgPcfwiAinIEopFy8ge3ZySIpoB519nUm1LVjxvv+l2HyPXgLDWggCCS4Ghe+LvRbVIV3JCRp4/g DocQFZWOb+/aaTt2dzZifCWuFH6q9KMchr1U5LCskqEcUCU7+S0a7KWiqOmOt4MvBogaw8jqTR/M Ah/FdT9674ost0AsDigzl/uud5bXHCWVOFsz+joJxiJi4IUkAn1DzUtuuDm5LKIcp/eHkXCecsVh SLMPJmTGqHlklQhf2vW7bhx6u7gLRA6GoVbAgs49dgQWqhBVKvDt8Ygav06SLpk2gCGTo8LfTsf7 mBJOWKdM+sk5u5DacPXAoVORZ4oKx5dmXJkX0MRMBD9nJk+DJ7Sk5Gojo0MJL6tHElmAjjpndBGJ NfktwD78lrj3Gp2D32P2lTjLknbzRAaaI7Lszn8MVK0kUF17eWzvhvEY8B2uhCdSbAbKhR0vKReg 6h7KhUBIlGtwwUBUo4rfDZwrkF+eTgSKC/hwYSA5cIAtiYhOR8rppA0zopNUTxkjw06ovdOTGOUK 76ey8Ps3/woBq/OABWZwI3RaYC2qbX0g+3x6SngYH2VYY8NCENakI9Wp9L09DccmCRbwEBTezCmH Znwz/f5t5PEJA0Lu2MJEuQNxMzs0SAeMp7/k0G6JtWMDJgwxkk+/f1sElEXcx7j4rk+Mgq/kwmz/ h+ZjzDJWEpLupyGkGcCqWkQtOEnitaunQQnSKZNO/Zt+eN+vnUeVhdDJjwHzkYVqnj/CskWKs1AZ Q7yyJGiOt95scCCrSQd2IdcqiJ9qBptbJMQQM6XWPAbJrrX6P5QZ7FGXZXUW0N2+OzrbVcxWIcq9 B9mWWmTRPQivjAXtLAId7oGuaUkA0B1aRPi0CvrYM2PkZZLHNVDl8fLYaALTKRAChFptkggeg3NE ItWZHqsWegwAlgjcl0joUCJBgcjQKzjZ9MuvnPr90OyIRRnB4vnP+hTwI+O01AEmC/73PI7PhPF1 SHxLoCn6qGYp2xT62qqpFzz1aYB4XVJ5PN2Fk6qUPVRqTEqV0DswBkIyPHryIbwmK9Jf3jxzuWxb YwEbkGBxwX136DzPECghaftJwfGk4B5YItLpqjorywxgTdXjY3sMYJYJYYKEsqJzrul9SmLfgEH2 K0bvJzIWE9sXi7n5/D5t/0qQrfw+LyVStAIqpBQFwHbb7i5SdqWKjLuSc4RcbjpTNc04nPpdJJu1 jtZhZXB4aVKMdj1ywwOADw+Szo8XXASZAMcEmcfmTdhbpm1aH0wiC6bD4DuZyBBV6bjm9y9/I/+S ZsyCQaRgwOf7gEIVK5d9RejThxdI0QQFk6KJSG2Gw3GzlxJVw/BcmL33RwMQUt42oQ8l7dMIGfth +yYgqSwJB2lntm+3djQmylQMQqBDAZWpD7C6Qn42VtPZ7vanKSQbSnx8WZRhuzJFyNRuh343BRYk 6qTESGWzkkD6yRikHJ6yUsyjVGC7LDUb+vhmlTIoeY2nbvDU3fRBPbGilMQbfn3xn/8IcaLg+1IS ZPnwd5WGibR0/zT4Tp6LH+EBFgRK8ZWD2zPG53tk5xjCXUtqL3qAsLlJCfcGJmp3BbHoOiGddyC3 nDt6ZByOw3bw1BrAxJOKj6jGtUg8fJja2KlBcTnjOhzrJgDf74dgVOw3Wvp9WFQrRrzkngodJXuZ 6tSyobxvvOfxy7pWVCARwNuW9lk/sM02BmpmlGkIMW1zRS3FCcRPhaDKLwau2uuQowKJYHSiD1DD bi1kTUXe9PhuAdf5SYHTp57i53oYTBIGNmMMXFOTQe+xfBs79EwI+YBFprsmIHadMMWT4Pl1yRCl FzDUcJ2F1LadpnZysWlbCZxsmFWv+Iiq17wlNEV0rkvq/azfUgUejFKrNCkMqlAZKYm5j0xEWa7z RAw57Z1RWWkYzfaaVJdMmfTRx2F+jGxvcqWbn/XwfH66UIE6r4nr+mqG3BAmufIO1vzQHRApvrOr cfSyXvJzUSfcag7RdlLqBU7LgkhnVL31soE/WzGDV6kJXiHjx3S7pytqGIcAeBowDF6hvnVs/2U9 hZhsrrYJmYtXiEnXBg+0xF6xUW943IXYgw8rAnLnQOwdJnpcC3cGL+9vO8+DoRNFRZzECSNR1EIn v3T7kCOMSuzu1AZ8lhn8xwSTifKtyYfb5jQdA1RI8DNGYunQovr7rj5qf0n4PEQJg/oaT7Udm+k2 roLaxOVKeNZ8GZ5wNq0x9FMH4wajg5jWag6gYJCQYybv/dw2IXazztmaVPB5A4nNcgaykgwD9QTP BKYAqAmR5+6P1LUTlLXvujGdjPDK9TfXW41QGpwK+cMhU6MqL7v+wK9F138m5/J0UagF8iwpZo2C xhMDmRlqu2+beJ0rUsTvurHdHmOEIPTlWtcaHApE4LNda+iFsko+IHwH1CWO/GTfRhrBSnUWjhbp 6JJ9Ol3tungdBL+xvC/gt91FFYDiXz3y2sV2IxYVEOxeProCCn1eAWeabDu2oUkjXPUihPYEzwoO TRn+fgz3SfaaWJsF18hEGVnOpiZZbnXV6NbO/wbSsKxIQ+9OY0hy1/yRy6Yn59lQw2n0xdS9rM76 PcJqDz0LDOQ39I9gmbMe3/Hohj4Cf83J9Fndj4ZfU63xADPxFu5TVFYpx+yc8ROJBhiRrj6/OBBm +6GxBijdBPTTKeuW0M3TunMJpVVScw/69qoJOg0ukIRnM49nd/BJFUjsm1RB5q7Pesvn36XECrqu cmD9rn+MM9bPbbPiGKSCq9sEg4CkfURBZeK6VIlMupIKbBvUvlT14gZxJWwcBvAzK3tgrOB/AkZC 3Czn89pfpzmC1aWPwxBBnxtipySYdLpYCKDvZxmAoqmsU2Bk6bd2tlAJGEutCwer2eGUsZdEcZHg zgruFHmj4HOYqpeqAoy6XuQX9pJo9thOd5YvxFsSZKQkVZhajXW6dXVlLFIUlGdJFIU6g0ZQGyAL Li2XSQU6pJdGCXmlAajpUvohaKkz/X3T9u2IrKKqpMSyU6jS+BUscBy7bTYzBm/Iz84iJbSqTGbN ZhfT3NjWdHUeGJlGykwDvFuYJhvKOccb2C1dV/patwuJmu5X1j55N1KWanr4rhtCU8fyErr+sJNy YXtGUw9pfeYpGQPJv6bgaPiwuxlGfM5rIUhLmRzX9oi3bcg1aZU78Z17e6aOyXKRFzp/3xQbT1kq X1N7E3HF1ILgZ5Lm69mwtc/1aR+meECmEimFnfc0VGGFGEWxb2AAlE2tF7z0s9MoC75fSbUgMVnv 98sOl5Wg7W1LDQ/wb7Gx7TYGPuBovWVaEuUHRoeT7Psy1FjIx/jt522/vXVXmu7EdkjFJFK7C/Bd pv7mS0IgTeWbxlyQ3ZQGYb5F25uUZHEacDnXC5fcXn9XwFfU6bqewQPLOwXZVI20sxzV/Hv3zdNU hUrQFXF01v3+koECXpZV4BRYgOT/mEn9ZSd0duMXaJTr2yoKsdDZqmwD/FGzWM9egdHkd+F2IJIy 2H/DuEyKy9102+iA+SCfvTnm0g3yuRfFmpsQYH6CLzpoirOnki4M9kP8hntMI6lNbLkDL3kuXPKe hLQXBdn17pJXfG4WEBJqZRZQ2b5yjGyqHzVLV2ZrvOQLvvW+vYp1NXUD75qbNt6QVWkk6r+HY2wo lSYbAGxiUyi7ZE77kqlR+OkXN7zz4+vNLxdvN47UltYv9UbKSkH2b7ioKtuS2x4unr+4ePbi581x PLUXz/6+YRfP/sv+1/OX3+OfFz9s/u3ixxdunS8ZnJfS9oftZwqEup2f/7TkVShv/orRzSYTRTqA sMSRea71GaFAfICviXx+dbd2b+qS+z8CQunkSE9VCsHSBcP9Q34pZaskfN6e7P3dkzAFo2wbIe7x 8nps2wC4KGSzi3p7rQLuZQGMewD797UUwv+sU0vgXkcyprldhxmwUfnnOZJBJtfcfsZ+xTryt5/+ Egudod7kCRQTyujOTjS7REV4VYLmia5P/TZpn6VtLLpIC+62Av9xttGs/jODPNpGMxAxZ5tXP/z1 L4Gy8EQywPg8NyhtN59IYuwHlBU9vAYtiBcplhxSuXSgeY/xBOAHUuuPNp7U2iLFn208O68qnfFe BOO5y2CZNNox/eUIwd5NGCixfVGC/q81abACqzVPdtD2egxmEDBH9UeYAfBeoZ7aXklmhhryC1Zw XN5ZIUzHg9fbCywYwg1zwXxuOh7yNec+/h7qbEwHG1dKxPNTObL9IZ3PFIVyYv9YhcSs19QWphU1 B/30FBAzTVtkE4+IPpFUdiCwgDqA8ZwE2/CTSXl5GFaqJAoNyA5qAiS0TseK17wgU8sbZJk33dd2 2mxTm4qU8jv/omGMGoDpDxvsfHL6o57+dLjywYY6YpQ0D1gq6iqVZ/8UJlNcvzm++bGldvssLC4F qpu9Ar2sY5UQjwqIV5Cyobfg2o6pqXwdPGLSHyjQZIF2GiBkz9hc062TonYISVB4L/2ljveeFOmu 8F0XAsLJdTITBQQ8Tde9p5ubdooDgsAZooC7nRuy8nApsZA0KblXI4aKiv+Dt3hColDWmpqiM1Ao P4xFYzrHqAsTOIRpR3dFThwuuRdc62w0B2qqpK/fDRO1aOy4ttLi3BwwHYnsU+SbJumVB47rWZBt WLhJMw/5+2b7JrYyrMghInQ1k3DKqj2iN0Hn2Ll0ig2aDoAkSgmD0CqC5UpGZf27/TQ8DbSWFvjl eV5ZyoSoXKBQ4tSstOOifwikznIiQqqViqZEkSyZk4oA1ef/89tPAezK1CRfTeE2aiKZrpr9I2WS VL3Orl8oV6zs8+aQhc7+0GcNvx4PH5n6EVZXk/UThpxpZWb/D4DtkpuolQX55JeL/wc2qxdwZW5k c3RyZWFtCmVuZG9iagozNCAwIG9iago0NTUxCmVuZG9iago0MCAwIG9iago8PC9SMTUKMTUgMCBS L1IxMwoxMyAwIFIvUjM2CjM2IDAgUi9SMjUKMjUgMCBSL1IyMwoyMyAwIFIvUjIxCjIxIDAgUi9S MTkKMTkgMCBSL1IzOQozOSAwIFIvUjE3CjE3IDAgUj4+CmVuZG9iago0MiAwIG9iago8PC9MZW5n dGggNDMgMCBSL0ZpbHRlciAvRmxhdGVEZWNvZGU+PgpzdHJlYW0KeJy9W02T3MaR3eBxLvsX5rZU BBtCfQN27IGUpTAdklayR+vLXDDd4AzW3Y0WgCZN/w37B/vVV1ahgRkON2iHI0xFN7pQlfny5cvM mrJg16X9X/h3e7j69erXa+Y+i/9sD9dvbq6+/qOorxkraqX49c27K/8Ddl3Vhbw2ZXV9c7h6+Z9f 3fwfnmRq9iQrKl0rPH2zu3r583f2mW9vrn/Gi4R2q2xkUeEXhhe8smvJQld2L2/eXn399ofraTi3 V1//+Zpdff17+39vfvoG/7z93fV/XH371q2zvuGLbYQNM14WFact//Ld2999/xu7J8kKWSsd9nk+ dsepHU5DO7U7+7XWhRa6Dl+/Ox+3U9cfR/dLU0iN9fxXzdE9j9dwxUT40C5mP2UGxijjS+7bwX1Y FWVdxaV33Tv3oShKrVl8Xzu0x61bQpiirrkJX+z7+25beLvPPbThtYRBxfWGywKWtk9/CQfpCpYq /+UO0pUotHQ++v6Pr52HBEzKWbTTvju2zRA/L+v4+dA2++CAiuzXDN30cGinx2zFGC8Mi7Yq2Zez lqqBjn+9tVRt3+as9dZbi+uCa2nWrFVWZK3PAOYnbchFYYRyNsSJv5gFheL/BkLQwr7UGvC13RBO Lhjw5zf5y3fRqsC+MMQSzTA0H8dXzqyq4PjF/48+hHyaPh7D+hf0HvZeSFV9cbZgZf3vYAtWFtKz xZv//eU7TxdVwYTmYacv/upswkHVVbR1u9t86HbTg/OCKiSvosPvuul9sKEyJtqw3U794HwmGA6n nnLZcxEQvMHZnLu1hNVsLJkYS2+QAB4OzfAXt5ilK1ps7M/O4xwmxxLh020bF5+bjuM/uYnEMFtW ATKlil+964fDed+MwTyiJPPgG2cdXdSliNacHtrRodHuWZr48a6zn9UFA+vE37/vxoh+AbMYHa32 odt78kYy1nVc4s6DHOlMM1p2aNyHKgf5h2OIBlUySp1Dfwh8yATPNrt81H2kCqZ4RM1fu3Hqjvf2 841EiJe8vt5gI9J9+6cfbtzKolCMNrb5/u2b8L66UnGhfXc3NMPHwBSyktEUfcz2ptKGzht84iyk QTlKxedvX576E7wSUKUQbFUVD9AdSTqQTTg8GryiFD3pvYontabXnpphCjCSrBKXG8yejNarwFws HhFQD26qKWLed/3ZvYnXhS55PMS64b75nx9+IiVG72/feT6uE3wAv+n2q8J7RYpCYA/JK693u86G lpcBCrysav2YZStBliXsIbaqS+zBZ5rF44/9vtt2wQNSIhQpIxDaQOpLtFXgKkJbNEJVmJqW3vaH A6hjckhRwkZqfN6lGWNda2KI/+k0BHQijMoEKvhcO/MgqTFJPPG02TcSTjJQDNaUlirmNmHJJvdr Ie1jx+YG8px3nEnhBIhkShbYLRWdfOoDQdeSsPtUIEwPzRSoQlUlcfEQLQ2pGJ3yd6sJNx9C8AGH EdrDfvePV4HPRa3j8yGMOLxFW1mF/NgeA+WhDKp4fJZCRkmdOTa6Cs/yml8CRhdgi4p2tgy6B094 EN+cnPeeyElC7gXfyQDSQxvwxbRKDDG1xx0hl5Us2rM5nYDqxkaOcw4AVVPA9udp7Hax/lBMXoIY /KVoV+s5zSoCBkelLc5TmrCJgOSKh5NBSfYEwppu39x1+xAu0upOPt/DPPXVcF6KnhvvUmBbCaKb U997xCMP6OrSoXX5OEmDBeSlU401Ylzlw0O3dVpDCIg4LhbIAj3zBJcTxFr0BpYvS8LM/NUbCYll S51Pxi3l0Spx2VN51AVR9PTzlzw0uxgU0F8XHi0Fp5O/XzrZeXTfLvPkWkw2nmAqk6rCF8MYcxiD NnmCnIYx2FaA79Oe/GcwhwIrh8/+cD62ARMyySP2KuxIp2SViNcKTULz6/BkViGM7bb3utEqIE2g /Iytdset5wkr2Tnl3I0HBeJJlTKLtlM/NFHMIGlyTaqrOQZmQVxHx370FC/gm2iGoT01XdC/qqg1 0TpRd+ab09DDj4dY4VScKpwdFPE2Jk+3DwLTx5hrFdk+CbU6RUdKnaWhHc9TJ15ZmRXsliuy0sg1 7HL5TOyyVexySdj9w3n/MbCkMLSox88GRVdhM14WvQlFqGr4BYpQeRhC0YugcrAyCsCncnHCEJhK 8xXBzXmd6ZVjWJar0sztZVmQjH7qx+BKkJqpqd/w+nx/9pGIfAFiZLND4xCarQTN7LjfNp4tkRll TQn+blavwAEoh588y9quO8Cka/beK8jHVWkSAPzStokhU+W3C75CEQGZkIIqQBYfmwVkZ2rPRyoE Vplo4b45dn9rfUQhEuqKIiHIc6fe4s5aFPC+socLZWoCjIjq8UVEnuIWpnr21vk652P6hfOGNgBr UlBbsMou8ISCKWuSCCHOra7JdVE3BDcxYRJWAg+LvKvaHW1N6TSGczhqYpP6FiEfQ8tA7c+o613b 7u6arXMMKtEq4Qw0gzrXcxKkZklKPxXlqO+IMVGRk8KRYG5TpSw89Of7hwAIvD5yDUrgqTt547qf UGX7aJjFwlYpcuh6YQsI9oHdjCQ7fFjG+Wq5ekl4TBPhESNbiR4fb6YQUKBNmXpYj5F/NSO325de UAmdCyqAVhkybxMyD86oVE5oKFP6oVtTZAj5qtSJwlEadIEKakbV85pQAHpvvwrAM4Lg2w5D7NGU eZ+D9ANPOWq7b8axe7FNgFyKVgZ2EPWjohXlikp9mHbfbrO15kdV2I+Ui77LGNfhVJdkYAGiF+lK VCnnPfSjp2rATXJSEVlVgYyzbHqYrGyPgteKiIXgZakr0fhNIT0zguCFCC5RBZCHtv1+T4kexSXW VzpHxSXToBhcMA2rViqwTCe/60MIuaaFIgP6RaG/NWg/umf70B7aIpAI0C7XfWEHD+WiPgNJMrJP G3MTQKmpx/h4qyskyLJii2SF6kMuuw0Q3gm5WbKSiNME6vUXhvIO+BecJLBPVMhgVlWLDM/JrKz8 nGyFjJLS6RR9AHlMLc7YlbSqR8Tt3YNmT6FlXuPxaj3vlNDfqTSNzSqog8sWlLSMGB2wIlpjQ8Dp RxLf85TJbAfpImVi0+UTKRPVdkV6q23GLsvM5B5aKtv3QzPs/LMbCWmEqi7zxW08qq28BE0EIZiH Q3cMHT+wNyN4kv7g9Yr+qFOYP+XR0EtTEqvQZNF19kEqpuZqfh7bh6XzfKKVx21ZmQk9FdstqqRt dE4pMMv41JpHXg+RAK9dpIFZwt2Fx7L23OoE9cUWeTxkP2OS0o1Eo1PH9EWQDqhn0t7nkNlImxfY jM4SF3qI2I45qYhmPz1EfSE1PFgte6nP9NZSLWZcUqd8cWj+EhQQ5DOJSL+uzErm0PVeKW7mysYj rbbEST9NvVkaA9jmbEheqhLi0s6ZdFxtaK28OW2ZUpH/SNWcOlR3zb4JfUVZ2jbm5azChVT1LNT6 TihjWWSmGoVZy8cj/NgSfChcV40HL++hUx0yIG9RLVBteQxBlVWhz3RJ/KVO9htPex9O3Db3qEKn fJ4xUZbDePXcHAYBXBJyDk0sa2tDCDv2U7A3dG6q2paHROk4dognn5Btv5x8duO5B3qB1ES/pHYv t7zUkvpCVeo04/5xTY25muiRRrPrqJkqb1UmFAkpLvXULHQfN+CroNNMCscPqOja1RMAmZrkxmMn qJM66sagb4V6PHEw8fmJ43g+3PmEJe2NCoJ+gNQsGbTHaWiO0xion9UioXwXSEHXbNn5zN73+b0W nKGUSXUeTuepCU0wqwrL2UQjTYYQ45WkSfbQ2ikqaslXQX/oyix1M9e0z9hpvPQcjsgYya4fA1PB UfGH/x1+NZu/u8iuox3lmr+he1H0R5lyGtvzrt/A3Lv+4LVhhQo8yS8fHaHNZvfEzCrYIdpRNyw6 1zC3Wcpd2xQhqnBSLihNuTJH+2QbBtVL8JOdXpRVPr1ofRFl5THpj5/yM9tvjbEp2syQmvIjW9nR 2lSZJU66b4+2QxCsVhc8da7OYywqKttAUwtsZJX5OGGLEHphK6KiVb4JUsfUMl3uSKNhEKQmKMc7 AgEMJgeD7URoup/iLXL70hfEi8ITezN6NkZEkW7HlrOu49i2sXJQ+C0xxW06+uUuwFIsQXJ8ehv2 jUZQP8E9Y/B7k/lpijBTS47NypPxfHDHsOVtNnfod2dfDF5Gl+vo6Ogy7h/BV8YmLqxqd2fJEdAG AEWN1GEfFOV6HEKlbvLnvN6zQU4FOCXcrIpYbWXnoLXHJmPMFDAxYSzuHHllLgp1A7JoRemJ5vnY u1jO8+c760JNYttrPK8Px4/j1B4C0dYs5ZZxO3Qnd4flt0HvlhVtFGAKchElHs2fW8IzPKI01WM8 qt2aWj7NXeyMMcGeEkEeSG74UM+LXZhOp+SW2hdmMYJ/1j2EPLdB26bc1se+LJiB51nDSzvb+BDl Uu6jxF+T+1QoB7kfrjlgFcPzznOcKYHYF7cbnJkASF1eyAPsmxE+ZhmC21EK3fxJ7SOTmkJh3JbN 81MGsPNztTB/NsdZmdVtIYubLnavyipdE1jheZPqs5kiKdPAIJR9llx1apzSLQGpqUmYVrAvTpom C2Rq//a7mKN4wWcFXyAbuFKmNsZqjy17X215e3FRgD16+QeaK2VnamJKvWiL2SuAbOaYVyGllJzS D8GAJZXY/nomQcQ4jaeohbz6rlkDcaQ5tbRj8PKpLuLqEnTm/wrIhcYmrvd5AglTxnVv7e26X8/t PvS0rKqUebUGljxO3buPSFueHhQSgKAIPzaHlQH107c+suyz78ZY4rCsb7RSYi3uCPAkk2JFMaPs 1ffNnKlKcuaISjsk7Iu5cDiISc3/7rgdbJsqtNegHphKjd3TQ3Nnr4Z6HNh9pvq5T/0qGwGz3uEt 6XorDKmfCvkzxEmzgLjX2SUCyvBSfxI/ZWhMWeGt6F7jMzvnVdKeqSTNApXkn0qCFCmtOaCs2AUj 4a2L+UEWDk/MzVmZZlQfPPUhxZB09oXz/OUJEGxZYs7CJbscEtRcaQC7nJuyq4x0l3HbnqYA+2y2 TXGuUjH5EO76zCv7VaaJfTG6hWNvwsgqU8KTvwEIGVXngsveR0TmslOHsvSbXi17otDa5E8WgRQy xfUjXjRQmxy/MkT3gdY5kjNp1X7/PggUVGZEhcO4dMEhDLKRDHFsscCUMlUqIsOgf6644pUSISgd 5pclyezutmQYSgOrSRjPC/mNtGWUFuuEFxg0w9/48Tg1UF5bZxn7ZwEUqduHZsBX7WDvuW491UIJ pMOv3f68vJuEhKvrRyZCSLsr6Su74je1dMPW3c2jtLQElpvdpXkkrLWnYa5LAnYmnsVA2Lt9XZZ+ fAq0l7VTfyWkRduBppNvIWxh1oHu2RqtUuHauqs0gZ/C/XfmVUO4AW8stKprJFqrCr/ABXhADwLc CKAt/wMs1Gr8mtmesr//HoIIBWpt7+jYv6Hxc1oXRAKJwh3hz5GUJDUmWh9UUgihZh6zn5XZnd4p cRKZa9eN2/MY+4SIv9SaDX6wNJnJpC6GGtcpE3THeGtAGL5QoxC7ZiEkQHLlynVEbkSCaxqTo7xB QRI37Xs9RSnSra6GFJLMRMAQbwoaI1ODxZdFfr51MXkvC6XKi04DLwTKK6KKZuyPsYeFbfFUSPs/ 9TCFBvfG5+/PhzZUH+5mAWH3rg8p1fb5aRshmbh5X+VurDCLRp+1/MxEg/nSLYB7KPFwYQd7T93s kBIB9tWhNqtsS/96Yy8xyUTiLiJ+vvonsNWNRWVuZHN0cmVhbQplbmRvYmoKNDMgMCBvYmoKNDMy MQplbmRvYmoKNTMgMCBvYmoKPDwvUjE1CjE1IDAgUi9SMzYKMzYgMCBSL1IyNQoyNSAwIFIvUjIz CjIzIDAgUi9SNTIKNTIgMCBSL1IyMQoyMSAwIFIvUjE5CjE5IDAgUi9SNDkKNDkgMCBSL1I0Ngo0 NiAwIFIvUjM5CjM5IDAgUi9SMTcKMTcgMCBSPj4KZW5kb2JqCjU1IDAgb2JqCjw8L0xlbmd0aCA1 NiAwIFIvRmlsdGVyIC9GbGF0ZURlY29kZT4+CnN0cmVhbQp4nL1a23LcNhLdyqO+Yh6TWovG/ZJ9 2HKcuOLUutZxlM2LX6gZWuKaQyokx1rl67dBAA1wLtJoIqVSFVdRJNDoPn36dGNIQRfE/Rf+Xa7P fj/7fUGttQWbnpyLwiwYUaRgZqEZoQUx7rXv3p69fPtuMfab6uzlbwt69vJH97/v3r+Gf95+v/jb 2Q9vFz/DWu77aSEqJKzJiNSFgaWoVW7JxyxFJ1PjP8v14ruLs5cfGF1QWlgp2eLi05k/B10wygoi FprYQojFxfrs6w/VTdeP1eqbi/+e/XCx1zZlSKH+Atu0KKjkuXGvu753hjFRWCYVvHaxOvu6Wo7/ PGwuZ1IW4vnN5ZwWyubWvndG6YJohaZ2dTu+vKnashnvDpssXPTJiSYfAiWR7LFrHQIlEcYB4M97 kup7QKmscLs4T27aoRyPQOTTGSb3GmZsQZTMLburhiOg98x2cQmYMzS36+/0CHidYtYBeClLuDvq E8BLGdjCPD+8NOzyGHQ9oV370WVJYY3MDGu7h7H13FZxiK+ZuevcPAytk6w6BC0NJ33kWoegpeWj K/Mp0FKuPk3OOg5ZT2fWYd7SNLfrKN56brs8b+ncrmN46ySzDoFLEf1EWg2WenSFPQVcEmSoegS4 ns6sw7RlaW7XUbz1zGZNvDWz6ijeOsWqQ9AS0jyR4oKlxF+huLh0Bvua+Lntbtsj4PV0ph3gLlNw bnPb2qIsjgDYMxvGFQOAmdwwcgTATrHqEMC46zWeBmCcPLrG7ncWV/cBjJHC90Zjva66zTH09WSW 3YMv6OiSaUfC65ntmuCVWXUMtk4x6RC2qKLP6nYuCiYW0vDYsbyprzZ95U4Jf6JKuzddy0y/dc8A P1YYG569d330JGA4eEnS2F6X7TS3AKcxSXl8eWq3ay94wB6+oLpgVApnzzkDPwtpF+fQvkOb7j6Q 0xqy0EbEDX9yjwAo8ESER5vVVd1eueeQ0cYwPbcBDCOExe9/WXZ9eHvbI+eUgZqRcgGmFNpb8Nt0 ZFJoy+OyddtWfTwyZYzj8+AeStA9Vbm8DmMSZRSLfui7y6Zauz8IXnAbnfZ9Pa1AC5BV4dGXeqi7 Fo9B48Kfumn8QsFQw014eHtd++38kaNh43XlwwnHMpLI6B7/EELATYrbGEyQFJ81VTmM4RSGao3L 9lVcVnNctmrHvgyYEEAcrmQEm/tuHd6nnEWjV/Uw1u1y2oAbsJvHuPbVUJW9P9G5YLrQkFqQaS4P 4c9Xfbe58XFQhSU2Lrjs1jfVmBChNYmeuK2bZrKAF4CI+MGl94MspKsi4XDl5+mhKCShDI8WXtQk vTgpLArJozDquGD+3nU3eG+5SoHxva3H6wBypVK8pu/diAP3vq6vrqsheslwEVcYANDVixB1K0X0 XrmEP6yiG2ghKBX32DzbFNe+G0aPU64BEfHd7pMPCZCdBMJ2IXEZBH+5yelAJbgmOtAc6eAmpwPg T0tMtBBzyTC0cEZLSiRaKkKkwNlx6VcDZoeiuOaqXpZjtZqcBWqUc0wRcFVfBQyqQkqbDB9uQ7YL xxQUyQWzx2bZM61cUMlYjNut5yuXTgw/XfmpLkDBQteTf2wg94ERo4e6oR7rkDPCIpi++H2MsjKe oIr7MBYP3G7Wl9VEExw2Impf+CBtU0b56HksyYJLNA2IpYng1RzPBmmb/AYBlKkuzP0m7R6/aYF+ m5BQ/+G9IgDeVsVzXd6FXCKutQlrDEN91QZow+uQynTuxJkbqkBpVKADr0rv1skMoh50q4voPq9K seVVSCpqlMb4OYcWAVac4k4X7hGwllQyfu9l2BDIzhYKKlCWWTGDKBRMzKB+uiIYQoJSaeXMmJ0m gzsYROOyxmK7EgJrMprcHUJmHEGeCHUO6kkgnv6o+i4UFKmRbby3/hFOQwQesxyCazPr11BnoDL6 1cFeQZHly8suxJYmssliG/fzrAkkk8h0chsHetXpoHUDtDOEpDACCbapP4fvpUHimjwFOg6ErMkf yRxC/7suN0OsUBBs6iRDlofrat31d0EeSIK5EGo+d7CLflj25XAdUwHCxsRu2CAX8DTN4D0P1Grx MmTsqzLcNAFOGUFL0fPZjqFh8LAW1vFf/NOvbXAKFGtGEI0hiYxmO/rFURDqF0aIfBHQAsSNku3d RSjaAK347vnrf797H+hFWCR+WEIFAwQ3qcqGug+xTkKhbJoIlIwEbgM5msJalQUFlZFOKnfdBWEE TpOZ3krCyGoURrd958PEofBqjXV6xpRQ1pA8PMtQ13Ujr65qDzCnMeMKXiNGlqEW0+yNZxmhLUNi 2MRFLccszS2T8oBlGYc70eIrtDuKSaTv48xtivMA0PSlw6l6JtTuOfDzmdYFHNvt6IHvM5kHOVT5 WAk39+I5W0Y1Y5wEiygYuy6iQGuNwieKIcF2BZxQeGjQqb9voEp9FSgHgM9FdCtKW+1URQawIEMI qpXDAQwJxd3VQ3z7wp8DLFbSpEZjCfk6hGoJZIM1ZBj7ejm21TCEyqg0GhPqE8gkllL5uh6CZ4XC N7NbUShxnKZg5nKQo0aqQ9ECl0jLcj1R9mNzFxJaKs1npoCUIAqT/NNQjUGAWsIjMkP1BxHPsRzF 2ALFJHnsSKmpfal3Qk1h2qVOSSmeJH+7vF6X/URWEoQ6sNW8sIENbKt2aAHyOlWF8rJu6vHu2xAF 7iC4tfrkGGjjefowAzMX2y2Iq3DIcPcbonJDmiiLIcPiRutNaD3BNEWwhSn7pvbEci5clQV8Z3mz t618gH9Jjk3kX1iBmhSysg1LcE30ViBnPdZdUMEi1enb1L4SitB4ClPlrqkfXZ9QhSZBuB8SYG1P wIPKwg7FWlKM9bJrGlDHIVGVy7wt6yFpgEGzlHmw1lm9ewDomlOtS2UfqE89HtQBS9COKcSSv0Zw tS+l4e3HbwrkJh2z7UdwR+hGNYgt7Gnr9U1TOc3W+YKi3KUkiQe8LsP6hD3Y4wCck5JqoHAFMQ49 IcfS1VTlKghMYnGg4EhiegrNzT3sP4Y+23WrQsoU/TrEzLU6QFwpaq6yBJkv3ZQm+uhtGwCucs6N jTZPL1YH4zM7fxspkiYAIq9ne5TeUTY5CtrsyII6NcRIOuns3Vg2wUfxWep4AH+MbXc8s53zFhII ejfZZ8ceuuZLeGosjuiqKHN1KpHZnGR3YsETfXhFN9cVt35BAKpgsz7xYYf35VUV6pcQiKPX738N QADBDdmTC48EMVSUXRwbqdTCQv6vN42X18AMTCHLJGWsxd7JnlVp5OjxQJzWTfO0VXALkSaCt+3G 3YfZ5B+YkWk0oUsBwMD6VjOYwFVcY2oiQ5mBYKNCbAMHQetxvwhHqUVT5VuCGKpXwPqrUJ6FkWYr 6sZpMxSw00w2GCctNh6FD5MCiJKcZfcJ43hm4Kx4inxOC5HmOEo6OKiNrThPA4wMuYiIT6Ejssam EAeUUtdlb9dNAbKS7A5eoXvSO4PXF8FeTdh28hnX6jKM6LBpxtjYktRa3xsokfd7ffYTRd+q4tu7 SsUjDTxM0tQxFBbgU50KCwYTFAocnOgscvuk41fLGpS215lQZC3OOVfVsoFyuJpgsHPfACyu3eDo 3E3H/LRfhUBl9w0XIdJUJt5MUlNClmp89+Mkfz5+47eb/zjx3EJEnNhyQ3gzvf7TLuFs/LJOjyfq pMH8+fUNnT4Mr7yp+zSiZzZ+uZfSsiYru70IZO4ud3ZKlQaGxzTels4gteP5m/qyL/3ggrubGNQP N9Anh/GC+yWpiBskDWfTFGDZrZ1QKPZ60f0UVRLo9QCclh10o0cD4N0ww45344cqOQGHgnXotEBm UZXy/alcK8kB1wKUzQHXarXl2gPOchcjSkzO8pB75XmHcKrw9uxqE64V3M808C7qKNC1QSs4HrL3 Cbd+dov1Z0H3GM9EKUIFx4uvfXeTWW/r2nVseTeX63qI1sPOsDFaD43yIddz4+SvzXF6vO/NY3wP 8if5ftahW+zQV9Ww7OubMVYoBVUy8edq4xU7EJ9kZOdmyt3W4Urr8qpeBl8TgYH0EjGqGVDx22rG dSOY4TdDtVl151CtVn5sokGXJL02VK5rCi4XUExFUibh6gJyEWKXC6/Uhx3IBesu008Kh304HL9U WaM3XenKbeTG/lBLeUzuUneXrflpuSv3WgyIlFhl/xXvdF3ZZjiWK+92U2MvS6+qNYAJFEcMlKbu ggM1/PwWWEu+NW9zU3eMeCYu3ZRQ4uOkUNwvEZAjuthXZQfayxtDHpfZdPUhvEBDDe2CPA0xVD0c gAdHFTp1+n3ofMG/GIAraB/6wL5C6K3b7xgVABwRNtFoVDPZVVjdDjH9TZJ2S2jkljXeH3MnQHck 7XRNtN2PzQMwlv0enO0j/tevUGDiQPM/E7Lc+BT1tNf0VGsnTkG8scgAE+in3+X8fPZ/D/37GmVu ZHN0cmVhbQplbmRvYmoKNTYgMCBvYmoKMzMyNgplbmRvYmoKNTcgMCBvYmoKPDwvUjE1CjE1IDAg Ui9SMTMKMTMgMCBSL1IzNgozNiAwIFIvUjIxCjIxIDAgUi9SMTcKMTcgMCBSPj4KZW5kb2JqCjU5 IDAgb2JqCjw8L0xlbmd0aCA2MCAwIFIvRmlsdGVyIC9GbGF0ZURlY29kZT4+CnN0cmVhbQp4nH1W yVIjRxCN8FFfoSNEoKL2ZW4gbAcTYM8ghS/Gh0YU0I5eNOrSjP0j873OWruF5AkOCrKrsjPfe/my MSJz7P/S76adfZl9mZMQyz+bdn69nl0+EDYnClEi+Hz9MosXyFzRucJ6vm5nZw/2xe7O13/POEZa awrP18+zM9tt7ODDkELMCUFGCOpTLPK5BZVIyXD4T/KXP0oMUprplGGJQowjSRlJsetqt7POXaT3 YY5VenIXTzNksGAp9mxTBqNJznrf73dVuM80Eobleqvu2QcpRkaRnOAqJhWIUsxTbOX27RalApQQ OX5jh/q1C4kVEkTqo8RalMQPdtg3bkhlaF6a7l9SG1LK3Jp7i31oKIPkesngQlB5eHLaVeXq4afq qW5q969/LDnCjJrS+/O+6X0cSDBIA6wLQMfzAk/Xb7bf1ZE0zpEiJKO+7NutdbWr+9CfpEiaUsjj 2ep+HTpUiEud37VY/n7/KaMErKYwxVg8ngf4mOeF53e4UBeh0GPJUW23ttqls0qUPuru+GwGCbDH pfCPQHZXNQlmaOgdzBRpWmC+2ru+rZwNdAkBOqCi0FUNfVd3ryiCB6BhIUHBHLGkYHpCwTdZwUwX +dzZJCnAKp+7tqDqAKFBVBSxj8ohrCin6BzLovNV3fYdKl2KXPY6YkIJYqwwYIfBdq6umki0BqWp I1gUPlKfgi4K6aurPG0EZwaCCAgUa6QY2WahAgmjpnNfm1FOoWgJaUwu4baLpgG4TkwjliRLv/+4 t5RXMUzKVWeBbp83cr5gGtwDRtyrnCcpd8muGKQkJlfq7Spk5EhjmduMeofLWhgygtrvwnAxiaRS xwaiuc6VXm23Tb0JJQ2pVaq1eA83wUXHxyPspw3rKcgC/MVQWQh1oMxTVkuBXM7zuYt4VXGtcgFf c8gUG+ubfWtHfPJlaohJiIO+yUEDJ8iajNXdb8vV/xTHieKHxRmtVb64rV6jGS04gMoFnZoV/Pud SxV9GDxQFdGvtjuAY1xJqozj4o8AN0F0HD27a6rXizR7BvbBRLlx2Ak3SEBR02FnJ4b9l9iBZCMz 6GMeVl4m55NtGhB/0qCBySwrLGGg5UjQryccZLV3m6YOyDOCpJD5wYu9yPtO6R+ayBJdo6R2qYva IbHrUmEwkrSMcZxSIFUrOU7BsbXc2LK8mDmUmJam2JVt+m0LHpS4Ixj/yJaXV6v4JfBeZuB1cLOs 6tvUOxGsXO3bdt9N5++9CDUBWMwBAQsOy89QNjENIh7P6II9nn9Q5rvB4ZgCU9BiYnQ0ysV4SCHu 5cJ1lAs/IZdV3Xyt+7RrMSlYP1RdPdgEjZH0nb34qZzwaIdqNzlc2ImEGSFF7q3uQHh1qFERpKgm h0wyv9IKmnmlM3CasjQXd7fXaclIKvL9b/YpBAViimUpDrWz+SOLME5HmHhaoaAczPkE5Dfnth8u L2E5PNXRxNFmQPuIEfHglUK++ZD2pRXtVsg+7y+HNopK+pdmRJv6afxcYFNJe/ljBUxz8OXIlfTx n9fzz7PPs/8A+1ufzGVuZHN0cmVhbQplbmRvYmoKNjAgMCBvYmoKMTE1NwplbmRvYmoKNjEgMCBv YmoKPDwvUjE1CjE1IDAgUi9SMTMKMTMgMCBSL1IzNgozNiAwIFI+PgplbmRvYmoKNSAwIG9iago8 PC9UeXBlL1BhZ2UvTWVkaWFCb3ggWzAgMCA2MTIgNzkyXQovUm90YXRlIDAvUGFyZW50IDMgMCBS Ci9SZXNvdXJjZXM8PC9Qcm9jU2V0Wy9QREYgL0ltYWdlQiAvVGV4dF0KL0V4dEdTdGF0ZSAyNiAw IFIKL0ZvbnQgMjcgMCBSCj4+Ci9Db250ZW50cyA2IDAgUgo+PgplbmRvYmoKMjggMCBvYmoKPDwv VHlwZS9QYWdlL01lZGlhQm94IFswIDAgNjEyIDc5Ml0KL1JvdGF0ZSAwL1BhcmVudCAzIDAgUgov UmVzb3VyY2VzPDwvUHJvY1NldFsvUERGIC9UZXh0XQovRm9udCAzMSAwIFIKPj4KL0NvbnRlbnRz IDI5IDAgUgo+PgplbmRvYmoKMzIgMCBvYmoKPDwvVHlwZS9QYWdlL01lZGlhQm94IFswIDAgNjEy IDc5Ml0KL1JvdGF0ZSAwL1BhcmVudCAzIDAgUgovUmVzb3VyY2VzPDwvUHJvY1NldFsvUERGIC9J bWFnZUIgL1RleHRdCi9Gb250IDQwIDAgUgo+PgovQ29udGVudHMgMzMgMCBSCj4+CmVuZG9iago0 MSAwIG9iago8PC9UeXBlL1BhZ2UvTWVkaWFCb3ggWzAgMCA2MTIgNzkyXQovUm90YXRlIDAvUGFy ZW50IDMgMCBSCi9SZXNvdXJjZXM8PC9Qcm9jU2V0Wy9QREYgL0ltYWdlQiAvVGV4dF0KL0ZvbnQg NTMgMCBSCj4+Ci9Db250ZW50cyA0MiAwIFIKPj4KZW5kb2JqCjU0IDAgb2JqCjw8L1R5cGUvUGFn ZS9NZWRpYUJveCBbMCAwIDYxMiA3OTJdCi9Sb3RhdGUgMC9QYXJlbnQgMyAwIFIKL1Jlc291cmNl czw8L1Byb2NTZXRbL1BERiAvSW1hZ2VCIC9UZXh0XQovRm9udCA1NyAwIFIKPj4KL0NvbnRlbnRz IDU1IDAgUgo+PgplbmRvYmoKNTggMCBvYmoKPDwvVHlwZS9QYWdlL01lZGlhQm94IFswIDAgNjEy IDc5Ml0KL1JvdGF0ZSAwL1BhcmVudCAzIDAgUgovUmVzb3VyY2VzPDwvUHJvY1NldFsvUERGIC9U ZXh0XQovRm9udCA2MSAwIFIKPj4KL0NvbnRlbnRzIDU5IDAgUgo+PgplbmRvYmoKMyAwIG9iago8 PCAvVHlwZSAvUGFnZXMgL0tpZHMgWwo1IDAgUgoyOCAwIFIKMzIgMCBSCjQxIDAgUgo1NCAwIFIK NTggMCBSCl0gL0NvdW50IDYKPj4KZW5kb2JqCjEgMCBvYmoKPDwvVHlwZSAvQ2F0YWxvZyAvUGFn ZXMgMyAwIFIKPj4KZW5kb2JqCjQgMCBvYmoKPDwvVHlwZS9FeHRHU3RhdGUvTmFtZS9SNC9UUi9J ZGVudGl0eT4+CmVuZG9iagozOCAwIG9iago8PC9UeXBlL0ZvbnREZXNjcmlwdG9yL0ZvbnROYW1l L0xMSENVQitDTVNZMTAvRm9udEJCb3hbMCAwIDQ0MyA0NDRdL0ZsYWdzIDQKL0FzY2VudCA0NDQK L0NhcEhlaWdodCA0NDQKL0Rlc2NlbnQgMAovSXRhbGljQW5nbGUgMAovU3RlbVYgNjYKL0NoYXJT ZXQoL2J1bGxldCkKL0ZvbnRGaWxlMyAzNyAwIFI+PgplbmRvYmoKMzcgMCBvYmoKPDwvTGVuZ3Ro IDYyIDAgUi9TdWJ0eXBlL1R5cGUxQy9MZW5ndGgxIDIzNz4+c3RyZWFtCgEABAIAAQEBDkxMSENV QitDTVNZMTAAAQEBH/gbAfgcAvgdA27+VPrw+ZsFpPdmEvc6Efc3D/cwEAADAQFGTFtDb3B5cmln aHQgKEMpIDE5OTcgQW1lcmljYW4gTWF0aGVtYXRpY2FsIFNvY2lldHkuIEFsbCBSaWdodHMgUmVz ZXJ2ZWRDTVNZMTBDb21wdXRlciBNb2Rlcm4AAIABDwGyAHQAAHQAAgEBAicO+IjDoPfvnwGL+BcD +E/3jhX2M+Ii+wE2MiIg4zT09wHg5PQeDnWh+T+hBvsQkAezCuALHgoEN58MCbOaDAwAAAplbmRz dHJlYW0KZW5kb2JqCjYyIDAgb2JqCjIzOAplbmRvYmoKNTEgMCBvYmoKPDwvVHlwZS9Gb250RGVz Y3JpcHRvci9Gb250TmFtZS9LQU1UWVgrQ01SOC9Gb250QkJveFs0MSAtMjEgNDg5IDY2NV0vRmxh Z3MgNAovQXNjZW50IDY2NQovQ2FwSGVpZ2h0IDY2NQovRGVzY2VudCAtMjEKL0l0YWxpY0FuZ2xl IDAKL1N0ZW1WIDczCi9NaXNzaW5nV2lkdGggMzU0Ci9DaGFyU2V0KC96ZXJvL3RocmVlKQovRm9u dEZpbGUzIDUwIDAgUj4+CmVuZG9iago1MCAwIG9iago8PC9MZW5ndGggNjMgMCBSL1N1YnR5cGUv VHlwZTFDL0xlbmd0aDEgNDc4Pj5zdHJlYW0KAQAEAgABAQEMS0FNVFlYK0NNUjgAAQEBH/gbAfgc AvgdA2f7jvrC+YIFrvhNEvc1EfcwD/csEAADAQFGSllDb3B5cmlnaHQgKEMpIDE5OTcgQW1lcmlj YW4gTWF0aGVtYXRpY2FsIFNvY2lldHkuIEFsbCBSaWdodHMgUmVzZXJ2ZWRDTVI4Q29tcHV0ZXIg TW9kZXJuAAAAAjAzAAARABQAAwIAAQAHAIYBDv8BYiqgDv8CE0AAdqf5CqcBi+T3ouQD+H330xWL 9oDMastf4zqhVIv7EotdLX1vZ0KJKItXi0mOJrs7uUHVeMCLu4vhmr3usNOO5IvMCPt0+8wVaYtG m3b0gMSL6Yu/i9CL0ZbCoPHZlaSLrYvQep8wl1SLQItHi1CLMX9TdiJGfWqLCA7/AhNAAHap1PcD 97HyxaUBqfH3YvMD95H34hXavVEi+xFEZlZUQJ/AaB+vpKKsq3Sia3BvemMs8U33BvcZ6Ofv3knX JaEf2qfGz4vbCNsxxCMgOlE/ZqR7paqfoagei7BrmXWMtcLYjp2LCKXXgyRFbmF9ex9tbHSJTod4 ioOKi34IfZSLnB4OdqD5P6D7pZr3b5UG+2GWB6wK1wseCgQ3nwwJp5AMDNebDA0AAAplbmRzdHJl YW0KZW5kb2JqCjYzIDAgb2JqCjQ3OQplbmRvYmoKNDggMCBvYmoKPDwvVHlwZS9Gb250RGVzY3Jp cHRvci9Gb250TmFtZS9IUVdPQkcrQ01SMTIvRm9udEJCb3hbMjcgMCA0NjIgNjc1XS9GbGFncyA0 Ci9Bc2NlbnQgNjc1Ci9DYXBIZWlnaHQgNjc1Ci9EZXNjZW50IDAKL0l0YWxpY0FuZ2xlIDAKL1N0 ZW1WIDY5Ci9NaXNzaW5nV2lkdGggMzI2Ci9DaGFyU2V0KC90d28vZm91cikKL0ZvbnRGaWxlMyA0 NyAwIFI+PgplbmRvYmoKNDcgMCBvYmoKPDwvTGVuZ3RoIDY0IDAgUi9TdWJ0eXBlL1R5cGUxQy9M ZW5ndGgxIDQxNj4+c3RyZWFtCgEABAIAAQEBDUhRV09CRytDTVIxMgABAQEf+BsB+BwC+B0DafuP +nD5ggWu+A8S9zcR9zIP9y4QAAMBAUZLWkNvcHlyaWdodCAoQykgMTk5NyBBbWVyaWNhbiBNYXRo ZW1hdGljYWwgU29jaWV0eS4gQWxsIFJpZ2h0cyBSZXNlcnZlZENNUjEyQ29tcHV0ZXIgTW9kZXJu AAAAAjI0AAATABUAAwEBB3rS/wFGYnAO/wHpk3CL0vf66fcFqAGL6fdq3gP4TPc8FXUGiHqDVIF7 hIJSi22LCPtNBqaiyMulo/cs9yDDv4vuCPcHMNj7CPsIRyg1WLeLjqClmquneJ5vHoKLiYuIip7P wbnMiwjgv0QvNlpBUksf+177dgVz+AEHDv8B6ZNwi6j3Hqj4X58B96DNA/f9+R8VnouQfR6Di4iL g3/7wfxnGG73mzAHZomBQh53bgaijdqLp4uni9uLookIqHcHQ4iVsB/m8KgmB0n4DRX8DfuHBw52 oPk/oPulmvdvlQb7YZYHqArMCx4KBDefDAmflAwMzJsMDQAACmVuZHN0cmVhbQplbmRvYmoKNjQg MCBvYmoKNDE3CmVuZG9iago0NSAwIG9iago8PC9UeXBlL0ZvbnREZXNjcmlwdG9yL0ZvbnROYW1l L0lJVlNSUStDTU1JMTIvRm9udEJCb3hbNDYgLTI1MCA4NTggNzUwXS9GbGFncyA0Ci9Bc2NlbnQg NzUwCi9DYXBIZWlnaHQgNzUwCi9EZXNjZW50IC0yNTAKL0l0YWxpY0FuZ2xlIDAKL1N0ZW1WIDEy OAovTWlzc2luZ1dpZHRoIDMzMwovQ2hhclNldCgvc2xhc2gvTikKL0ZvbnRGaWxlMyA0NCAwIFI+ PgplbmRvYmoKNDQgMCBvYmoKPDwvTGVuZ3RoIDY1IDAgUi9TdWJ0eXBlL1R5cGUxQy9MZW5ndGgx IDQ3MT4+c3RyZWFtCgEABAIAAQEBDklJVlNSUStDTU1JMTIAAQEBH/gbAfgcAvgdA237jvqW+YIF qfhLEvc5Efc0D/cwEAADAQFGTFtDb3B5cmlnaHQgKEMpIDE5OTcgQW1lcmljYW4gTWF0aGVtYXRp Y2FsIFNvY2lldHkuIEFsbCBSaWdodHMgUmVzZXJ2ZWRDTU1JMTJDb21wdXRlciBNb2Rlcm4AAAAC Tj0AAC8AEAADAgABAAcAyAEI/wFNVVAO/wMQFDCLqPkFqAGL+cAD+Xj41hWWtpup144IjpeMnJaC i4d3WImLdx9bBn2LeY19iwiFf4t4gZOLkh/HiY90i3mLgoqIiH37BfxXGPtq+KiEm4qMdYsZ+w4G d4KLeIGSi56QxouCiYmDiogf+xn8pn9ac3ZJiBmGgYp5gZWLjp++jYufH7sGmYuciZmLCJKWi56U gYyHH2qMa5GLr4uTjZSNk/cb+KsYkYGLiY+C94L85RiQf42FlIuVi4yOj5wIDv8B6ZNg+46g+lOf AYv4EQP4QfldFYuMkZqLjQiXgZKDHoaLgouDdfvj/kEYi4qFfIuJCH+VhJMekYuUjJKgCA52oPk/ oPullZaWBvtglQehCswLHgoEN58MCaGSDAwAAAplbmRzdHJlYW0KZW5kb2JqCjY1IDAgb2JqCjQ3 MgplbmRvYmoKMTUgMCBvYmoKPDwvU3VidHlwZS9UeXBlMS9CYXNlRm9udC9UaW1lcy1Sb21hbi9U eXBlL0ZvbnQvTmFtZS9SMTUvRmlyc3RDaGFyIDEvTGFzdENoYXIgMjU1L1dpZHRoc1sgMzMzIDU1 MiA1NTYgMTY3IDMzMyA2MTEgMjc4IDMzMyAzMzMgMTAwMCAzMzMgNTY0IDEwMDAgNjExIDQ0NAoz MzMgMjc4IDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAg MTAwMCAxMDAwIDMzMyAxODAKMjUwIDMzMyA0MDggNTAwIDUwMCA4MzMgNzc4IDMzMSAzMzEgMzMx IDUwMCA1NjIgMjUwIDMzMSAyNTAgMjgxCjUwMSA1MDEgNTAxIDUwMSA1MDEgNTAxIDUwMSA1MDEg NTAxIDUwMSAyODEgMjgxIDU2NCA1NjQgNTY0IDQ0NAo5MjEgNzIyIDY2MiA2NjIgNzIyIDYxMiA1 NTIgNzIyIDcyMiAzMzEgMzkxIDcyMiA2MTIgODkzIDcyMiA3MjIKNTUyIDcyMiA2NjIgNTUyIDYx MiA3MjIgNzIyIDk0MyA3MjIgNzIyIDYxMSAzMzEgMjc4IDMzMSA0NjkgNTAwCjMzMyA0NDEgNTAx IDQ0MSA1MDEgNDQxIDMzMSA1MDEgNTAxIDI4MSAyODEgNTAxIDI4MSA3ODIgNTAxIDUwMQo1MDEg NTAxIDMzMSAzOTEgMjgxIDUwMSA1MDEgNzIyIDUwMSA1MDEgNDQxIDQ4MCAyMDAgNDgwIDU0MSAx MDAwCjUwMCAxMDAwIDMzMyA1MDAgNDQ0IDEwMDAgNTAwIDUwMCAzMzMgMTAwMCA1NTYgMzMzIDg4 OSAxMDAwIDEwMDAgMTAwMAoxMDAwIDEwMDAgMTAwMCA0NDEgNDQxIDM1MCA1MDEgMTAwMCAzMzMg OTgwIDM4OSAzMzMgNzIyIDEwMDAgMTAwMCA3MjIKMTAwMCAzMzMgNTAwIDUwMCA1MDAgNTAwIDIw MCA1MDAgMzMzIDc2MCAyNzYgNTAwIDU2NCAzMzEgNzYwIDMzMwo0MDAgNTY0IDMwMCAzMDAgMzMz IDUwMCA0NTMgMjUwIDMzMyAzMDAgMzEwIDUwMCA3NTAgNzUwIDc1MCA0NDQKNzIyIDcyMiA3MjIg NzIyIDcyMiA3MjIgODg5IDY2NyA2MTEgNjExIDYxMSA2MTEgMzMzIDMzMyAzMzMgMzMzCjcyMiA3 MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA1NjQgNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgNTU2IDUw MAo0NDQgNDQ0IDQ0NCA0NDQgNDQ0IDQ0NCA2NjcgNDQ0IDQ0NCA0NDQgNDQ0IDQ0NCAyNzggMjc4 IDI3OCAyNzgKNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDU2NCA1MDAgNTAwIDUwMCA1MDAg NTAwIDUwMCA1MDAgNTAwXQovRW5jb2RpbmcgNjYgMCBSPj4KZW5kb2JqCjY2IDAgb2JqCjw8L1R5 cGUvRW5jb2RpbmcvRGlmZmVyZW5jZXNbCjIvZmkKMTQ3L3F1b3RlZGJsbGVmdC9xdW90ZWRibHJp Z2h0CjE1MC9lbmRhc2hdPj4KZW5kb2JqCjEzIDAgb2JqCjw8L1N1YnR5cGUvVHlwZTEvQmFzZUZv bnQvVGltZXMtQm9sZC9UeXBlL0ZvbnQvTmFtZS9SMTMvRmlyc3RDaGFyIDEvTGFzdENoYXIgMjU1 L1dpZHRoc1sgMzMzIDU1NiA1NTYgMTY3IDMzMyA2NjcgMjc4IDMzMyAzMzMgMTAwMCAzMzMgNTcw IDEwMDAgNjY3IDQ0NAozMzMgMjc4IDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAg MTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDMzMyAyNzgKMjUwIDMzMyA1NTUgNTAwIDUwMCAxMDAw IDgzMyAzMzMgMzM0IDMzNCA1MDAgNTcwIDI1MCAzMzMgMjUwIDI3OAo1MDEgNTAxIDUwMSA1MDEg NTAxIDUwMSA1MDEgNTAwIDUwMCA1MDAgMzMzIDMzMyA1NzAgNTcwIDU3MCA1MDAKOTMwIDcyMiA2 NjkgNzIyIDcyNCA2NjkgNjExIDc3OCA3NzggMzkwIDUwMSA3NzggNjY3IDk0NCA3MjIgNzc4CjYx MyA3NzggNzI0IDU1NyA2NjkgNzIyIDcyMiAxMDAwIDcyMiA3MjIgNjY3IDMzMyAyNzggMzMzIDU4 MSA1MDAKMzMzIDUwMSA1NTcgNDQ2IDU1NyA0NDYgMzM0IDUwMSA1NTcgMjc4IDMzMyA1NTcgMjc4 IDgzNiA1NTcgNTAxCjU1NiA1NTYgNDQ2IDM5MCAzMzQgNTU3IDUwMSA3MjIgNTAxIDUwMCA0NDQg Mzk0IDIyMCAzOTQgNTIwIDEwMDAKNTAwIDEwMDAgMzMzIDUwMCA1MDAgMTAwMCA1MDAgNTAwIDMz MyAxMDAwIDU1NiAzMzMgMTAwMCAxMDAwIDEwMDAgMTAwMAoxMDAwIDEwMDAgMTAwMCA1MDAgNTAw IDM1MCA1MDAgMTAwMCAzMzMgMTAwMCAzODkgMzMzIDcyMiAxMDAwIDEwMDAgNzIyCjEwMDAgMzMz IDUwMCA1MDAgNTAwIDUwMCAyMjAgNTAwIDMzMyA3NDcgMzAwIDUwMCA1NzAgMzMzIDc0NyAzMzMK NDAwIDU3MCAzMDAgMzAwIDMzMyA1NTYgNTQwIDI1MCAzMzMgMzAwIDMzMCA1MDAgNzUwIDc1MCA3 NTAgNTAwCjcyMiA3MjIgNzIyIDcyMiA3MjIgNzIyIDEwMDAgNzIyIDY2NyA2NjcgNjY3IDY2NyAz ODkgMzg5IDM4OSAzODkKNzIyIDcyMiA3NzggNzc4IDc3OCA3NzggNzc4IDU3MCA3NzggNzIyIDcy MiA3MjIgNzIyIDcyMiA2MTEgNTU2CjUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDcyMiA0NDQgNDQ0 IDQ0NCA0NDQgNDQ0IDI3OCAyNzggMjc4IDI3OAo1MDAgNTU2IDUwMCA1MDAgNTAwIDUwMCA1MDAg NTcwIDUwMCA1NTYgNTU2IDU1NiA1NTYgNTAwIDU1NiA1MDBdCj4+CmVuZG9iagoxMSAwIG9iago8 PC9TdWJ0eXBlL1R5cGUxL0Jhc2VGb250L1RpbWVzLVJvbWFuL1R5cGUvRm9udC9OYW1lL1IxMS9G aXJzdENoYXIgMS9MYXN0Q2hhciAyNTUvV2lkdGhzWyAzMzMgNTU2IDU1NiAxNjcgMzMzIDYxMSAy NzggMzMzIDMzMyAxMDAwIDMzMyA1NjQgMTAwMCA2MTEgNDQ0CjMzMyAyNzggMTAwMCAxMDAwIDEw MDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMzMzIDE4MAoy NTAgMzMzIDQwOCA1MDAgNTAwIDgzMyA3NzggMzMzIDMzMyAzMzMgNTAwIDU2NCAyNTAgMzMzIDI1 MCAyNzgKNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDI3OCAyNzggNTY0 IDU2NCA1NjQgNDQ0CjkyMSA3MTkgNjY5IDY2OSA3MjIgNjEwIDU1NiA3MjIgNzIyIDMzNCAzODkg NzIyIDYxMCA4ODYgNzE5IDcyMgo1NTYgNzIyIDY2OSA1NTIgNjExIDcxOSA3MjIgOTQ1IDcyMiA3 MTkgNjExIDMzMyAyNzggMzMzIDQ2OSA1MDAKMzMzIDQ0MyA1MDEgNDQzIDUwMSA0NDMgMzMzIDUw MSA1MDEgMjc2IDI3OCA1MDEgMjc2IDc3NyA1MDEgNTAxCjUwMSA1MDAgMzM0IDM5MyAyNzYgNTAx IDUwMSA3MTkgNTAwIDUwMSA0NDQgNDgwIDIwMCA0ODAgNTQxIDEwMDAKNTAwIDEwMDAgMzMzIDUw MCA0NDQgMTAwMCA1MDAgNTAwIDMzMyAxMDAwIDU1NiAzMzMgODg5IDEwMDAgMTAwMCAxMDAwCjEw MDAgMTAwMCAxMDAwIDQ0NCA0NDQgMzUwIDUwMCAxMDAwIDMzMyA5ODAgMzg5IDMzMyA3MjIgMTAw MCAxMDAwIDcyMgoxMDAwIDMzMyA1MDAgNTAwIDUwMCA1MDAgMjAwIDUwMCAzMzMgNzYwIDI3NiA1 MDAgNTY0IDMzMyA3NjAgMzMzCjQwMCA1NjQgMzAwIDMwMCAzMzMgNTAwIDQ1MyAyNTAgMzMzIDMw MCAzMTAgNTAwIDc1MCA3NTAgNzUwIDQ0NAo3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA4ODkgNjY3 IDYxMSA2MTEgNjExIDYxMSAzMzMgMzMzIDMzMyAzMzMKNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIg NzIyIDU2NCA3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA1NTYgNTAwCjQ0NCA0NDQgNDQ0IDQ0NCA0 NDQgNDQ0IDY2NyA0NDQgNDQ0IDQ0NCA0NDQgNDQ0IDI3OCAyNzggMjc4IDI3OAo1MDAgNTAwIDUw MCA1MDAgNTAwIDUwMCA1MDAgNTY0IDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDBdCj4+ CmVuZG9iagozNSAwIG9iago8PC9UeXBlL0ZvbnREZXNjcmlwdG9yL0ZvbnROYW1lL1RpbWVzLUl0 YWxpYz4+CmVuZG9iagozNiAwIG9iago8PC9TdWJ0eXBlL1R5cGUxL0Jhc2VGb250L1RpbWVzLUl0 YWxpYy9UeXBlL0ZvbnQvTmFtZS9SMzYvRmlyc3RDaGFyIDEvTGFzdENoYXIgMjU1L1dpZHRoc1sg MzMzIDUwMSA1MDAgMTY3IDMzMyA1NTYgMjc4IDMzMyAzMzMgMTAwMCAzMzMgNjc1IDEwMDAgNTU2 IDM4OQozMzMgMjc4IDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAw IDEwMDAgMTAwMCAxMDAwIDMzMyAyMTQKMjUwIDMzMyA0MjAgNTAwIDUwMCA4MzMgNzc4IDMzMyAz MzMgMzMzIDUwMCA2NzUgMjUwIDMzMyAyNTAgMjc4CjUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUw MCA1MDAgNTAwIDUwMCAzMzMgMzMzIDY3NSA2NzUgNjc1IDUwMAo5MjAgNjEyIDYxMSA2NjIgNzIy IDYxMSA2MTEgNzIyIDcyMiAzMzEgNDQ0IDY2NyA1NTIgODMzIDY2MiA3MjIKNjExIDcyMiA2MTEg NTAxIDU1MiA3MjIgNjExIDgzMyA2MTEgNTU2IDU1NiAzODkgMjc4IDM4OSA0MjIgNTAwCjMzMyA1 MDEgNTAxIDQ0MSA1MDEgNDQxIDI4MSA1MDEgNTAxIDI4MSAyNzggNDQ0IDI4MSA3MjIgNTAxIDUw MQo1MDEgNTAwIDM5MSAzOTEgMjgxIDUwMSA0NDQgNjY3IDQ0MSA0NDEgMzg5IDQwMCAyNzUgNDAw IDU0MSAxMDAwCjUwMCAxMDAwIDMzMyA1MDAgNTU2IDg4OSA1MDAgNTAwIDMzMyAxMDAwIDUwMCAz MzMgOTQ0IDEwMDAgMTAwMCAxMDAwCjEwMDAgMTAwMCAxMDAwIDU1NiA1NTYgMzUwIDUwMCA4ODkg MzMzIDk4MCAzODkgMzMzIDY2NyAxMDAwIDEwMDAgNTU2CjEwMDAgMzg5IDUwMCA1MDAgNTAwIDUw MCAyNzUgNTAwIDMzMyA3NjAgMjc2IDUwMCA2NzUgMzMzIDc2MCAzMzMKNDAwIDY3NSAzMDAgMzAw IDMzMyA1MDAgNTIzIDI1MCAzMzMgMzAwIDMxMCA1MDAgNzUwIDc1MCA3NTAgNTAwCjYxMSA2MTEg NjExIDYxMSA2MTEgNjExIDg4OSA2NjcgNjExIDYxMSA2MTEgNjExIDMzMyAzMzMgMzMzIDMzMwo3 MjIgNjY3IDcyMiA3MjIgNzIyIDcyMiA3MjIgNjc1IDcyMiA3MjIgNzIyIDcyMiA3MjIgNTU2IDYx MSA1MDAKNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDAgNjY3IDQ0NCA0NDQgNDQ0IDQ0NCA0NDQgMjc4 IDI3OCAyNzggMjc4CjUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA2NzUgNTAwIDUwMCA1MDAg NTAwIDUwMCA0NDQgNTAwIDQ0NF0KL0VuY29kaW5nIDY3IDAgUj4+CmVuZG9iago2NyAwIG9iago8 PC9UeXBlL0VuY29kaW5nL0RpZmZlcmVuY2VzWwoyL2ZpXT4+CmVuZG9iago5IDAgb2JqCjw8L1N1 YnR5cGUvVHlwZTEvQmFzZUZvbnQvVGltZXMtUm9tYW4vVHlwZS9Gb250L05hbWUvUjkvRmlyc3RD aGFyIDEvTGFzdENoYXIgMjU1L1dpZHRoc1sgMzMzIDU1NyA1NTYgMTY3IDMzMyA2MTEgMjc4IDMz MyAzMzMgMTAwMCAzMzMgNTY0IDEwMDAgNjExIDQ0NAozMzMgMjc4IDEwMDAgMTAwMCAxMDAwIDEw MDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDMzMyAxODAKMjUwIDMz MyA0MDggNTAwIDUwMCA4MzMgNzc4IDMzMyAzMzEgMzMxIDUwMCA1NjQgMjUwIDMzMSAyNTAgMjc4 CjQ5OSA1MDAgNDk5IDUwMCA1MDAgNTAwIDQ5OSA1MDAgNTAwIDUwMCAyNzggMjc4IDU2NCA1NjQg NTY0IDQ0NAo5MjEgNzIwIDY2NyA2NjcgNzIwIDYxMSA1NTcgNzIyIDcyMiAzMzMgMzg5IDcyMiA2 MTEgODg4IDcyMiA3MjAKNTU3IDcyMiA2NjcgNTU3IDYwOSA3MjIgNzIyIDk0NCA3MjIgNzIyIDYx MSAzMzMgMjc4IDMzMyA0NjkgNTAwCjMzMyA0NDEgNDk5IDQ0MSA0OTkgNDQxIDMzMyA1MDAgNDk5 IDI3OCAyNzggNTAwIDI3OCA3NzggNDk5IDQ5OQo0OTkgNTAwIDMzMSAzODkgMjc4IDQ5OSA1MDAg NzIyIDUwMCA0OTkgNDQ0IDQ4MCAyMDAgNDgwIDU0MSAxMDAwCjUwMCAxMDAwIDMzMyA1MDAgNDQ0 IDEwMDAgNTAwIDUwMCAzMzMgMTAwMCA1NTYgMzMzIDg4OSAxMDAwIDEwMDAgMTAwMAoxMDAwIDEw MDAgMTAwMCA0NDQgNDQ0IDM1MCA1MDAgMTAwMCAzMzMgOTgwIDM4OSAzMzMgNzIyIDEwMDAgMTAw MCA3MjIKMTAwMCAzMzMgNTAwIDUwMCA1MDAgNTAwIDIwMCA1MDAgMzMzIDc2MCAyNzYgNTAwIDU2 NCAzMzEgNzYwIDMzMwo0MDAgNTY0IDMwMCAzMDAgMzMzIDUwMCA0NTMgMjUwIDMzMyAzMDAgMzEw IDUwMCA3NTAgNzUwIDc1MCA0NDQKNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgODg5IDY2NyA2MTEg NjExIDYxMSA2MTEgMzMzIDMzMyAzMzMgMzMzCjcyMiA3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA1 NjQgNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgNTU2IDUwMAo0NDQgNDQ0IDQ0NCA0NDQgNDQ0IDQ0 NCA2NjcgNDQ0IDQ0NCA0NDQgNDQ0IDQ0NCAyNzggMjc4IDI3OCAyNzgKNTAwIDUwMCA1MDAgNTAw IDUwMCA1MDAgNTAwIDU2NCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwXQovRW5jb2Rp bmcgNjggMCBSPj4KZW5kb2JqCjY4IDAgb2JqCjw8L1R5cGUvRW5jb2RpbmcvRGlmZmVyZW5jZXNb CjIvZmldPj4KZW5kb2JqCjI1IDAgb2JqCjw8L1N1YnR5cGUvVHlwZTEvQmFzZUZvbnQvVGltZXMt Um9tYW4vVHlwZS9Gb250L05hbWUvUjI1L0ZpcnN0Q2hhciAxL0xhc3RDaGFyIDI1NS9XaWR0aHNb IDMzMyA1NTQgNTU2IDE2NyAzMzMgNjExIDI3OCAzMzMgMzMzIDEwMDAgMzMzIDU2NCAxMDAwIDYx MSA0NDQKMzMzIDI3OCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAw MCAxMDAwIDEwMDAgMTAwMCAzMzMgMTgwCjI1MCAzMzMgNDA4IDUwMCA1MDAgODMzIDc3OCAzMzMg MzMzIDMzMyA1MDAgNTY0IDI1MiAzMzcgMjUyIDI3OAo1MDUgNTAwIDUwNSA1MDUgNTAwIDUwMCA1 MDUgNTAwIDUwMCA1MDAgMjc4IDI3OCA1NjQgNTY0IDU2NCA0NDQKOTIxIDcyMiA2NjIgNjY3IDcy MiA2MTEgNTU0IDcyMiA3MjIgMzM3IDM4NSA3MjIgNjE0IDg5MSA3MjIgNzIyCjU1NiA3MjIgNjYy IDU1NCA2MTQgNzIyIDcyMiA5MzkgNzIyIDcyMiA2MTEgMzMzIDI3OCAzMzMgNDY5IDUwMAozMzMg NDQ1IDUwNSA0NDUgNTA1IDQ0NSAzMzcgNTA1IDUwNSAyNzcgMjc4IDUwNSAyNzcgNzgyIDUwNSA1 MDUKNTA1IDUwMCAzMzcgMzg1IDI3NyA1MDUgNTA1IDcyMiA1MDUgNTA1IDQ0NSA0ODAgMjAwIDQ4 MCA1NDEgMTAwMAo1MDAgMTAwMCAzMzMgNTAwIDQ0NCAxMDAwIDUwMCA1MDAgMzMzIDEwMDAgNTU2 IDMzMyA4ODkgMTAwMCAxMDAwIDEwMDAKMTAwMCAxMDAwIDEwMDAgNDQ0IDQ0NCAzNTAgNTAwIDEw MDAgMzMzIDk4MCAzODkgMzMzIDcyMiAxMDAwIDEwMDAgNzIyCjEwMDAgMzMzIDUwMCA1MDAgNTAw IDUwMCAyMDAgNTAwIDMzMyA3NjAgMjc2IDUwMCA1NjQgMzM3IDc2MCAzMzMKNDAwIDU2NCAzMDAg MzAwIDMzMyA1MDAgNDUzIDI1MCAzMzMgMzAwIDMxMCA1MDAgNzUwIDc1MCA3NTAgNDQ0CjcyMiA3 MjIgNzIyIDcyMiA3MjIgNzIyIDg4OSA2NjcgNjExIDYxMSA2MTEgNjExIDMzMyAzMzMgMzMzIDMz Mwo3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgNTY0IDcyMiA3MjIgNzIyIDcyMiA3MjIgNzIy IDU1NiA1MDAKNDQ0IDQ0NCA0NDQgNDQ0IDQ0NCA0NDQgNjY3IDQ0NCA0NDQgNDQ0IDQ0NCA0NDQg Mjc4IDI3OCAyNzggMjc4CjUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1NjQgNTAwIDUwMCA1 MDAgNTAwIDUwMCA1MDAgNTAwIDUwMF0KL0VuY29kaW5nIDY5IDAgUj4+CmVuZG9iago2OSAwIG9i ago8PC9UeXBlL0VuY29kaW5nL0RpZmZlcmVuY2VzWwoyL2ZpXT4+CmVuZG9iagoyMyAwIG9iago8 PC9TdWJ0eXBlL1R5cGUxL0Jhc2VGb250L1RpbWVzLVJvbWFuL1R5cGUvRm9udC9OYW1lL1IyMy9G aXJzdENoYXIgMS9MYXN0Q2hhciAyNTUvV2lkdGhzWyAzMzMgNTU2IDU1NiAxNjcgMzMzIDYxMSAy NzggMzMzIDMzMyAxMDAwIDMzMyA1NjQgMTAwMCA2MTEgNDQ0CjMzMyAyNzggMTAwMCAxMDAwIDEw MDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMzMzIDE4MAoy NTAgMzMzIDQwOCA1MDAgNTAwIDgzMyA3NzggMzMzIDMzMyAzMzMgNTAwIDU2NCAyNTAgMzMzIDI1 MCAyNzgKNTAwIDQ5OSA0OTkgNDk5IDQ5OSA1MDAgNTAwIDUwMCA1MDAgNTAwIDI3OCAyNzggNTY0 IDU2NCA1NjQgNDQ0CjkyMSA3MjIgNjY3IDY2NyA3MjIgNjExIDU1NiA3MjIgNzIyIDMzMyAzODkg NzIyIDYxMSA4ODkgNzIyIDcyMgo1NTYgNzIyIDY2NyA1NTYgNjExIDcyMiA3MjIgOTQ0IDcyMiA3 MjIgNjExIDMzMyAyNzggMzMzIDQ2OSA1MDAKMzMzIDQ0NCA1MDAgNDQ0IDUwMCA0NDQgMzMzIDUw MCA1MDAgMjc4IDI3OCA1MDAgMjc4IDc3OCA1MDAgNTAwCjUwMCA1MDAgMzMzIDM4OSAyNzggNTAw IDUwMCA3MjIgNTAwIDUwMCA0NDQgNDgwIDIwMCA0ODAgNTQxIDEwMDAKNTAwIDEwMDAgMzMzIDUw MCA0NDQgMTAwMCA1MDAgNTAwIDMzMyAxMDAwIDU1NiAzMzMgODg5IDEwMDAgMTAwMCAxMDAwCjEw MDAgMTAwMCAxMDAwIDQ0NCA0NDQgMzUwIDUwMCAxMDAwIDMzMyA5ODAgMzg5IDMzMyA3MjIgMTAw MCAxMDAwIDcyMgoxMDAwIDMzMyA1MDAgNTAwIDUwMCA1MDAgMjAwIDUwMCAzMzMgNzYwIDI3NiA1 MDAgNTY0IDMzMyA3NjAgMzMzCjQwMCA1NjQgMzAwIDMwMCAzMzMgNTAwIDQ1MyAyNTAgMzMzIDMw MCAzMTAgNTAwIDc1MCA3NTAgNzUwIDQ0NAo3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA4ODkgNjY3 IDYxMSA2MTEgNjExIDYxMSAzMzMgMzMzIDMzMyAzMzMKNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIg NzIyIDU2NCA3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA1NTYgNTAwCjQ0NCA0NDQgNDQ0IDQ0NCA0 NDQgNDQ0IDY2NyA0NDQgNDQ0IDQ0NCA0NDQgNDQ0IDI3OCAyNzggMjc4IDI3OAo1MDAgNTAwIDUw MCA1MDAgNTAwIDUwMCA1MDAgNTY0IDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDBdCj4+ CmVuZG9iagoyNCAwIG9iago8PC9UeXBlL0ZvbnREZXNjcmlwdG9yL0ZvbnROYW1lL1RpbWVzLVJv bWFuPj4KZW5kb2JqCjIyIDAgb2JqCjw8L1R5cGUvRm9udERlc2NyaXB0b3IvRm9udE5hbWUvVGlt ZXMtUm9tYW4+PgplbmRvYmoKMTggMCBvYmoKPDwvVHlwZS9Gb250RGVzY3JpcHRvci9Gb250TmFt ZS9UaW1lcy1Sb21hbj4+CmVuZG9iagoxNCAwIG9iago8PC9UeXBlL0ZvbnREZXNjcmlwdG9yL0Zv bnROYW1lL1RpbWVzLVJvbWFuPj4KZW5kb2JqCjEwIDAgb2JqCjw8L1R5cGUvRm9udERlc2NyaXB0 b3IvRm9udE5hbWUvVGltZXMtUm9tYW4+PgplbmRvYmoKOCAwIG9iago8PC9UeXBlL0ZvbnREZXNj cmlwdG9yL0ZvbnROYW1lL1RpbWVzLVJvbWFuPj4KZW5kb2JqCjIwIDAgb2JqCjw8L1R5cGUvRm9u dERlc2NyaXB0b3IvRm9udE5hbWUvVGltZXMtQm9sZD4+CmVuZG9iagoxMiAwIG9iago8PC9UeXBl L0ZvbnREZXNjcmlwdG9yL0ZvbnROYW1lL1RpbWVzLUJvbGQ+PgplbmRvYmoKMjEgMCBvYmoKPDwv U3VidHlwZS9UeXBlMS9CYXNlRm9udC9UaW1lcy1Cb2xkL1R5cGUvRm9udC9OYW1lL1IyMS9GaXJz dENoYXIgMS9MYXN0Q2hhciAyNTUvV2lkdGhzWyAzMzMgNTU2IDU1NiAxNjcgMzMzIDY2NyAyNzgg MzMzIDMzMyAxMDAwIDMzMyA1NzAgMTAwMCA2NjcgNDQ0CjMzMyAyNzggMTAwMCAxMDAwIDEwMDAg MTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMzMzIDI3OAoyNTAg MzMzIDU1NSA1MDAgNTAwIDEwMDAgODMzIDMzMyAzMzMgMzMzIDUwMCA1NzAgMjUwIDMzMyAyNTAg MjgxCjUwMCA1MDEgNTAwIDUwMCA1MDAgNTAxIDUwMSA1MDAgNTAxIDUwMSAzMzMgMzMzIDU3MCA1 NzAgNTcwIDUwMQo5MzAgNzIyIDY2MiA3MjIgNzIyIDY2MiA2MTEgNzc4IDc3OCAzOTEgNTAxIDc3 OCA2NjcgOTQ0IDcyMiA3ODIKNjEyIDc3OCA3MjIgNTUyIDY2MiA3MjIgNzIyIDEwMDAgNzIyIDcy MiA2NjcgMzMzIDI3OCAzMzMgNTgxIDUwMAozMzMgNTAxIDU1MiA0NDEgNTUyIDQ0MSAzMzEgNTAx IDU1MiAyODEgMzMzIDU1MiAyODEgODMzIDU1MiA1MDEKNTUyIDU1NiA0NDEgMzkxIDMzMSA1NTIg NTAxIDcyMiA1MDAgNTAxIDQ0NCAzOTQgMjIwIDM5NCA1MjAgMTAwMAo1MDAgMTAwMCAzMzMgNTAw IDUwMCAxMDAwIDUwMCA1MDAgMzMzIDEwMDAgNTU2IDMzMyAxMDAwIDEwMDAgMTAwMCAxMDAwCjEw MDAgMTAwMCAxMDAwIDUwMCA1MDAgMzUwIDUwMCAxMDAwIDMzMyAxMDAwIDM4OSAzMzMgNzIyIDEw MDAgMTAwMCA3MjIKMTAwMCAzMzMgNTAwIDUwMCA1MDAgNTAwIDIyMCA1MDAgMzMzIDc0NyAzMDAg NTAwIDU3MCAzMzMgNzQ3IDMzMwo0MDAgNTcwIDMwMCAzMDAgMzMzIDU1NiA1NDAgMjUwIDMzMyAz MDAgMzMwIDUwMCA3NTAgNzUwIDc1MCA1MDAKNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgMTAwMCA3 MjIgNjY3IDY2NyA2NjcgNjY3IDM4OSAzODkgMzg5IDM4OQo3MjIgNzIyIDc3OCA3NzggNzc4IDc3 OCA3NzggNTcwIDc3OCA3MjIgNzIyIDcyMiA3MjIgNzIyIDYxMSA1NTYKNTAwIDUwMCA1MDAgNTAw IDUwMCA1MDAgNzIyIDQ0NCA0NDQgNDQ0IDQ0NCA0NDQgMjc4IDI3OCAyNzggMjc4CjUwMCA1NTYg NTAwIDUwMCA1MDAgNTAwIDUwMCA1NzAgNTAwIDU1NiA1NTYgNTU2IDU1NiA1MDAgNTU2IDUwMF0K Pj4KZW5kb2JqCjUyIDAgb2JqCjw8L1N1YnR5cGUvVHlwZTEvQmFzZUZvbnQvS0FNVFlYK0NNUjgv VHlwZS9Gb250L05hbWUvUjUyL0ZvbnREZXNjcmlwdG9yIDUxIDAgUi9GaXJzdENoYXIgNDgvTGFz dENoYXIgNTEvV2lkdGhzWwo1MjYgMzU0IDM1NCA1MjZdCj4+CmVuZG9iagoxOSAwIG9iago8PC9T dWJ0eXBlL1R5cGUxL0Jhc2VGb250L1RpbWVzLVJvbWFuL1R5cGUvRm9udC9OYW1lL1IxOS9GaXJz dENoYXIgMS9MYXN0Q2hhciAyNTUvV2lkdGhzWyAzMzMgNTU2IDU1NiAxNjcgMzMzIDYxMSAyNzgg MzMzIDMzMyAxMDAwIDMzMyA1NjQgMTAwMCA2MTEgNDQ0CjMzMyAyNzggMTAwMCAxMDAwIDEwMDAg MTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMzMzIDE4MAoyNTAg MzMzIDQwOCA1MDAgNTAwIDgzMyA3NzggMzMzIDMzMyAzMzMgNTAwIDU2NCAyNTAgMzMzIDI1MCAy NzgKNTAwIDQ5NiA0OTYgNDk2IDQ5NiA1MDAgNTAwIDUwMCA1MDAgNTAwIDI3OCAyNzggNTY0IDU2 NCA1NjQgNDQ0CjkyMSA3MjIgNjY3IDY2NyA3MjIgNjExIDU1NiA3MjIgNzIyIDMzMyAzODkgNzIy IDYxMSA4ODkgNzIyIDcyMgo1NTYgNzIyIDY2NyA1NTYgNjExIDcyMiA3MjIgOTQ0IDcyMiA3MjIg NjExIDMzMyAyNzggMzMzIDQ2OSA1MDAKMzMzIDQ0NCA1MDAgNDQ0IDUwMCA0NDQgMzMzIDUwMCA1 MDAgMjc4IDI3OCA1MDAgMjc4IDc3OCA1MDAgNTAwCjUwMCA1MDAgMzMzIDM4OSAyNzggNTAwIDUw MCA3MjIgNTAwIDUwMCA0NDQgNDgwIDIwMCA0ODAgNTQxIDEwMDAKNTAwIDEwMDAgMzMzIDUwMCA0 NDQgMTAwMCA1MDAgNTAwIDMzMyAxMDAwIDU1NiAzMzMgODg5IDEwMDAgMTAwMCAxMDAwCjEwMDAg MTAwMCAxMDAwIDQ0NCA0NDQgMzUwIDUwMCAxMDAwIDMzMyA5ODAgMzg5IDMzMyA3MjIgMTAwMCAx MDAwIDcyMgoxMDAwIDMzMyA1MDAgNTAwIDUwMCA1MDAgMjAwIDUwMCAzMzMgNzYwIDI3NiA1MDAg NTY0IDMzMyA3NjAgMzMzCjQwMCA1NjQgMzAwIDMwMCAzMzMgNTAwIDQ1MyAyNTAgMzMzIDMwMCAz MTAgNTAwIDc1MCA3NTAgNzUwIDQ0NAo3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA4ODkgNjY3IDYx MSA2MTEgNjExIDYxMSAzMzMgMzMzIDMzMyAzMzMKNzIyIDcyMiA3MjIgNzIyIDcyMiA3MjIgNzIy IDU2NCA3MjIgNzIyIDcyMiA3MjIgNzIyIDcyMiA1NTYgNTAwCjQ0NCA0NDQgNDQ0IDQ0NCA0NDQg NDQ0IDY2NyA0NDQgNDQ0IDQ0NCA0NDQgNDQ0IDI3OCAyNzggMjc4IDI3OAo1MDAgNTAwIDUwMCA1 MDAgNTAwIDUwMCA1MDAgNTY0IDUwMCA1MDAgNTAwIDUwMCA1MDAgNTAwIDUwMCA1MDBdCj4+CmVu ZG9iago0OSAwIG9iago8PC9TdWJ0eXBlL1R5cGUxL0Jhc2VGb250L0hRV09CRytDTVIxMi9UeXBl L0ZvbnQvTmFtZS9SNDkvRm9udERlc2NyaXB0b3IgNDggMCBSL0ZpcnN0Q2hhciA1MC9MYXN0Q2hh ciA1Mi9XaWR0aHNbIDQ5MSAzMjYgNDkxXQo+PgplbmRvYmoKNDYgMCBvYmoKPDwvU3VidHlwZS9U eXBlMS9CYXNlRm9udC9JSVZTUlErQ01NSTEyL1R5cGUvRm9udC9OYW1lL1I0Ni9Gb250RGVzY3Jp cHRvciA0NSAwIFIvRmlyc3RDaGFyIDYxL0xhc3RDaGFyIDc4L1dpZHRoc1sgNDkxIDMzMyAzMzMK MzMzIDMzMyAzMzMgMzMzIDMzMyAzMzMgMzMzIDMzMyAzMzMgMzMzIDMzMyAzMzMgMzMzIDMzMyA3 ODJdCj4+CmVuZG9iagozOSAwIG9iago8PC9TdWJ0eXBlL1R5cGUxL0Jhc2VGb250L0xMSENVQitD TVNZMTAvVHlwZS9Gb250L05hbWUvUjM5L0ZvbnREZXNjcmlwdG9yIDM4IDAgUi9GaXJzdENoYXIg MTUvTGFzdENoYXIgMTc4L1dpZHRoc1sgNTAxCjAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAw IDAKMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMAowIDAgMCAwIDAgMCAwIDAgMCAwIDAg MCAwIDAgMCAwCjAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAKMCAwIDAgMCAwIDAgMCAw IDAgMCAwIDAgMCAwIDAgMAowIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwCjAgMCAwIDAg MCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAKMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMAow IDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwCjAgMCAwIDAgMCAwIDAgMCAwIDAgMCAwIDAg MCAwIDAKMCAwIDUwMV0KPj4KZW5kb2JqCjE2IDAgb2JqCjw8L1R5cGUvRm9udERlc2NyaXB0b3Iv Rm9udE5hbWUvQ291cmllcj4+CmVuZG9iagoxNyAwIG9iago8PC9TdWJ0eXBlL1R5cGUxL0Jhc2VG b250L0NvdXJpZXIvVHlwZS9Gb250L05hbWUvUjE3L0ZpcnN0Q2hhciAxL0xhc3RDaGFyIDI1NS9X aWR0aHNbIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDEwMDAgNjAwIDYwMCAx MDAwIDYwMCA2MDAKNjAwIDYwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEwMDAgMTAwMCAxMDAwIDEw MDAgMTAwMCAxMDAwIDEwMDAgMTAwMCA2MDAgNjAwCjYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYw MCA2MDAgNjAyIDYwMiA2MDAgNjAwIDYwMCA2MDIgNjAyIDYwMgo2MDAgNjAwIDYwMCA2MDAgNjAw IDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAyIDYwMCA2MDAgNjAwIDYwMCA2MDAKNjAwIDYwMCA2MDAg NjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwCjYwMCA2 MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYw MAo2MDAgNjAyIDYwMCA2MDIgNjAyIDYwMiA2MDAgNjAwIDYwMiA2MDIgNjAwIDYwMiA2MDIgNjAy IDYwMiA2MDIKNjAyIDYwMCA2MDIgNjAyIDYwMiA2MDIgNjAwIDYwMiA2MDAgNjAwIDYwMCA2MDAg NjAwIDYwMCA2MDAgMTAwMAo2MDAgMTAwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAw IDYwMCA2MDAgNjAwIDEwMDAgMTAwMCAxMDAwCjEwMDAgMTAwMCAxMDAwIDYwMCA2MDAgNjAwIDYw MCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCAxMDAwIDEwMDAgNjAwCjEwMDAgNjAwIDYwMCA2MDAg NjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAyIDYwMCA2MDAKNjAwIDYwMCA2 MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwCjYw MCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAw IDYwMAo2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAg NjAwIDYwMCA2MDAKNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2 MDAgNjAwIDYwMCA2MDAgNjAwCjYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYw MCA2MDAgNjAwIDYwMCA2MDAgNjAwIDYwMF0KPj4KZW5kb2JqCjIgMCBvYmoKPDwvUHJvZHVjZXIg KEdOVSBHaG9zdHNjcmlwdCA2LjUyKQo+PmVuZG9iagp4cmVmCjAgNzAKMDAwMDAwMDAwMCA2NTUz NSBmIAowMDAwMDIzMTEzIDAwMDAwIG4gCjAwMDAwMzk1MzggMDAwMDAgbiAKMDAwMDAyMzAxOSAw MDAwMCBuIAowMDAwMDIzMTYxIDAwMDAwIG4gCjAwMDAwMjIxMDcgMDAwMDAgbiAKMDAwMDAwMDAx NSAwMDAwMCBuIAowMDAwMDAzMjI5IDAwMDAwIG4gCjAwMDAwMzQ4NjAgMDAwMDAgbiAKMDAwMDAz MDkzOCAwMDAwMCBuIAowMDAwMDM0Nzk4IDAwMDAwIG4gCjAwMDAwMjg0OTAgMDAwMDAgbiAKMDAw MDAzNDk4MiAwMDAwMCBuIAowMDAwMDI3MzI4IDAwMDAwIG4gCjAwMDAwMzQ3MzYgMDAwMDAgbiAK MDAwMDAyNjA1OCAwMDAwMCBuIAowMDAwMDM4MzI5IDAwMDAwIG4gCjAwMDAwMzgzODcgMDAwMDAg biAKMDAwMDAzNDY3NCAwMDAwMCBuIAowMDAwMDM2MzUzIDAwMDAwIG4gCjAwMDAwMzQ5MjEgMDAw MDAgbiAKMDAwMDAzNTA0MyAwMDAwMCBuIAowMDAwMDM0NjEyIDAwMDAwIG4gCjAwMDAwMzMzOTIg MDAwMDAgbiAKMDAwMDAzNDU1MCAwMDAwMCBuIAowMDAwMDMyMTY0IDAwMDAwIG4gCjAwMDAwMDMy NDkgMDAwMDAgbiAKMDAwMDAwMzI3OSAwMDAwMCBuIAowMDAwMDIyMjc1IDAwMDAwIG4gCjAwMDAw MDMzOTcgMDAwMDAgbiAKMDAwMDAwNzkxMyAwMDAwMCBuIAowMDAwMDA3OTM0IDAwMDAwIG4gCjAw MDAwMjI0MTkgMDAwMDAgbiAKMDAwMDAwNzk4OCAwMDAwMCBuIAowMDAwMDEyNjExIDAwMDAwIG4g CjAwMDAwMjk2NDggMDAwMDAgbiAKMDAwMDAyOTcxMSAwMDAwMCBuIAowMDAwMDIzNDA5IDAwMDAw IG4gCjAwMDAwMjMyMTYgMDAwMDAgbiAKMDAwMDAzNzg2MiAwMDAwMCBuIAowMDAwMDEyNjMyIDAw MDAwIG4gCjAwMDAwMjI1NzEgMDAwMDAgbiAKMDAwMDAxMjc1MiAwMDAwMCBuIAowMDAwMDE3MTQ1 IDAwMDAwIG4gCjAwMDAwMjU0ODggMDAwMDAgbiAKMDAwMDAyNTI2OCAwMDAwMCBuIAowMDAwMDM3 NjU2IDAwMDAwIG4gCjAwMDAwMjQ3NTMgMDAwMDAgbiAKMDAwMDAyNDU0MCAwMDAwMCBuIAowMDAw MDM3NTExIDAwMDAwIG4gCjAwMDAwMjM5NjMgMDAwMDAgbiAKMDAwMDAyMzc0NSAwMDAwMCBuIAow MDAwMDM2MjA1IDAwMDAwIG4gCjAwMDAwMTcxNjYgMDAwMDAgbiAKMDAwMDAyMjcyMyAwMDAwMCBu IAowMDAwMDE3MzA4IDAwMDAwIG4gCjAwMDAwMjA3MDYgMDAwMDAgbiAKMDAwMDAyMDcyNyAwMDAw MCBuIAowMDAwMDIyODc1IDAwMDAwIG4gCjAwMDAwMjA4MDMgMDAwMDAgbiAKMDAwMDAyMjAzMiAw MDAwMCBuIAowMDAwMDIyMDUzIDAwMDAwIG4gCjAwMDAwMjM3MjUgMDAwMDAgbiAKMDAwMDAyNDUy MCAwMDAwMCBuIAowMDAwMDI1MjQ4IDAwMDAwIG4gCjAwMDAwMjYwMzggMDAwMDAgbiAKMDAwMDAy NzIzMiAwMDAwMCBuIAowMDAwMDMwODg0IDAwMDAwIG4gCjAwMDAwMzIxMTAgMDAwMDAgbiAKMDAw MDAzMzMzOCAwMDAwMCBuIAp0cmFpbGVyCjw8IC9TaXplIDcwIC9Sb290IDEgMCBSIC9JbmZvIDIg MCBSCj4+CnN0YXJ0eHJlZgozOTU5MAolJUVPRgo= --=-=-=-- From hsheini@eecs.umich.edu Tue Jan 31 15:36:18 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0VNaG6H040710 for ; Tue, 31 Jan 2006 15:36:16 -0800 (PST) (envelope-from hsheini@eecs.umich.edu) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k0VNvDSl026222 for ; Tue, 31 Jan 2006 15:58:28 -0800 (PST) (envelope-from hsheini@eecs.umich.edu) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006013115582824308 for ; Tue, 31 Jan 2006 15:58:28 -0800 X-Original-Received: from newman.eecs.umich.edu (141.213.4.11) by mailgate-external2.sri.com with SMTP; 31 Jan 2006 23:58:27 -0000 X-Original-Received: from mail.eecs.umich.edu (mail.eecs.umich.edu [141.213.4.15]) by newman.eecs.umich.edu (8.13.2/8.13.0) with ESMTP id k0VNwKFv015859 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=OK); Tue, 31 Jan 2006 18:58:20 -0500 X-Original-Received: from mail.eecs.umich.edu (localhost [127.0.0.1]) by mail.eecs.umich.edu (8.13.2/8.13.2) with ESMTP id k0VNwKpH021286 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 31 Jan 2006 18:58:20 -0500 X-Original-Received: (from apache@localhost) by mail.eecs.umich.edu (8.13.2/8.13.1/Submit) id k0VNwJMg021285; Tue, 31 Jan 2006 18:58:19 -0500 X-Authentication-Warning: mail.eecs.umich.edu: apache set sender to hsheini@eecs.umich.edu using -f X-Original-Received: from ashtad.eecs.umich.edu (ashtad.eecs.umich.edu [141.212.106.93]) by mail.eecs.umich.edu (IMP) with HTTP for ; Tue, 31 Jan 2006 18:58:19 -0500 Message-ID: <1138751899.43dff99bd5155@mail.eecs.umich.edu> Date: Tue, 31 Jan 2006 18:58:19 -0500 From: Hossein Sheini To: Aaron Stump Subject: Re: [SMTCOMP] request for comment MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: Internet Messaging Program (IMP) 3.2.8 X-Originating-IP: 141.212.106.93 X-Virus-Scan: : UVSCAN at UoM/EECS X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Tue, 31 Jan 2006 15:36:21 -0800 Cc: smtcomp@csl.sri.com X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 31 Jan 2006 23:36:21 -0000 Dear Aaron, First I would like to thank all of you for the very successful competition you held in 2005. I participated in SMT-COMP'05 with my solver, Ario. I just have a few comments/suggestions for the SMT-COMP'06, as follows: 1. I think it is very helpful to have your method for selecting benchmarks from the benchmark pool as described in your "Benchmark Selection" section. However, I do have a question on how the organizers are going to determine the difficulty of each benchmark considering that different solvers perform differently on those benchmarks. My suggestion is to use the average data as collected in SMT-COMP'05 to regulate that decision. 2. There were instances in SMT-COMP'05 that were added at the last minute, not included in the released final version of benchmarks suites, i.e. check/int_incompleteness2.smt. I just wanted to suggest that if the same could happen this time, it is better to be mentioned in the documents that all solvers are required to be able to read the SMT header format (like note, comment, etc sections) correctly. 3. In SMT-COMP'05, there were a few solvers that performed buggy in many instances. My suggestion is to set up a rule that if a solver passed a threshold in the number of bugs, it should be eliminated from the competition because I dont know how its performance on those instances that it had no bugs can be trusted. (example of such solver is the performance of HTP in QF_LRA category considering its buggy performance in other categories) 4. I am very much excited about the short presentation as suggested for SMT-COMP'06. I think it is a very good idea and gives everyone an opportunity to get to know the spec of other solvers after seeing their performance. I do appreciate your effort and would like to say that it played an important role for me to get to know the weaknesses and advantages of my solver better and to focus my work accordingly. I also would like to express my interest to get more involved in the SMT community and help by any means in any of these activities. with best wishes, Hossein Sheini EECS PhD Candidate University of Michigan at Ann Arbor www.eecs.umich.edu/~hsheini Quoting Aaron Stump : > Dear SMT-COMP interest group, > > A month ago or so we sent out our current working draft of the SMT-COMP > rules for 2006 for your comment. We have received very little feedback > as of yet, and we would really appreciate your input. So if you haven't > already done so, please take a moment to look at the draft and let us > know any changes you think should be made. We will prepare the final > version of the rules soon, so please give us your comments no later than > February 1. The draft rules are attached below. > > Best wishes, > Aaron Stump > (writing also for Clark Barrett and Leonardo de Moura) > > From tinelli@cs.uiowa.edu Wed Feb 1 21:49:37 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k125nY6H073550 for ; Wed, 1 Feb 2006 21:49:35 -0800 (PST) (envelope-from tinelli@cs.uiowa.edu) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k126BxHa074236 for ; Wed, 1 Feb 2006 22:11:59 -0800 (PST) (envelope-from tinelli@cs.uiowa.edu) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006020122115832331 for ; Wed, 01 Feb 2006 22:11:58 -0800 X-Original-Received: from serv07.divms.uiowa.edu (128.255.44.97) by mailgate-external2.sri.com with SMTP; 2 Feb 2006 06:11:57 -0000 X-Original-Received: from [10.0.1.3] (12-215-116-89.client.mchsi.com [12.215.116.89]) by serv07.divms.uiowa.edu with id k126BrdV016099; Thu, 2 Feb 2006 00:11:55 -0600 Message-ID: <43E1A2A8.2080408@cs.uiowa.edu> Date: Thu, 02 Feb 2006 00:11:52 -0600 From: Cesare Tinelli User-Agent: Thunderbird 1.5 (Macintosh/20051201) MIME-Version: 1.0 To: Aaron Stump Subject: Re: [SMTCOMP] request for comment References: <200601251621.k0PGL6805641@priam.cse.wustl.edu> In-Reply-To: <200601251621.k0PGL6805641@priam.cse.wustl.edu> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam-Score: 3.701 (***) RCVD_IN_NJABL_DUL,RCVD_IN_SORBS_DUL X-Scanned-By: MIMEDefang 2.51 on 128.255.44.22 X-Virus-Scanned: ClamAV 0.88/1266/Wed Feb 1 16:21:42 2006 on serv07.divms.uiowa.edu X-Virus-Status: Clean X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Wed, 01 Feb 2006 21:49:40 -0800 Cc: smtcomp@csl.sri.com X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 02 Feb 2006 05:49:41 -0000 Hi Aaron, I went over the draft. I find it quite good already and I notice that it already incorporated some of major changes suggested by various people since SMT-COMP'05. Here are some further comments or questions in the hope that you may find them useful. page 2 Is the decision to allow people to submit the results of their solver to the demonstration section a nod to the Microsoft people? Just curious. page 2 I'm not sure how you are going to tell that two versions of the same solvers are not to be allowed if those versions are submitted in binary format. page 2 The session for system presentations on the 21st is a good idea. Is it going to be part of CAV's program? If it after CAV's sessions that day, have you already secured a room with the organizers? Just checking. I would propose that you also informally organize an SMT-COMP dinner on the 21 or the day before, compatibly with the rest of the FloC schedule. I think it would a great way for the participants to get to know one another, and for building a sense of community. CASC does that and it has worked rather well, although I would not go as far as organizing an official dinner, with a dinner registration and fee, as they do. page 3 The new version of SMT-LIB will will be 1.2. It will be a minor revision of the current one. I think it will be available by the end of March, together with updated theories, logics and benchmarks as needed. For the bitvectors, Silvio and I will propose a temporary theory and logic that does not need the introduction of dependent types, so that we can already have the bitvectors division at this SMT-COMP. Clark already has a good number of benchmarks in CVCL format that should be easy to translate in SMT-LIB 1.2. page 3 this should be first discussed with Clark I guess. But he has made good progress with CVCL in solving the majority of a very large set of quantified benchmarks from NASA. It might be good to have a division for these benchmarks, to stimulate work on quantifiers. CVCL would not be the only one here. Clark and one of his students have also defined a translator for Simplify, so Simplify could be entered as well. In addition, I think that the Vampire and the SPASS people might be interested in participating as they have been working on those benchmarks too. page 4 The classification into hard and easy benchmarks might be a source of trouble and contention, because there are no clear objective measures. You may want to spend more time here in devising a clean procedure for deciding the difficulty of a benchmark. Apart from that, the algorithm for choosing the benchmarks seems like a reasonably good one, which should shield you from accusations of favoritism. Methodologically though, the problem I see in your proposal is that if SMT-LIB happens to have for a given division a disproportionately large number of benchmarks from the same class of problems (such as synthetic benchmarks), picking randomly with a uniform distribution will give you a biased sampling set. I'm not sure how to address that properly though. About the scrambling issue, scrambling might be hard to justify if it changes the structure of the problem, given that structure is an important factor in practice. On the other hand, the only reasonable structure preserving transformations might be renamings of free symbols, which is probably not a deterrent for cheaters. I suppose that the only good deterrent would be to have a large enough number of benchmarks in SMT-LIB. So, we need more benchmarks! Page 5 I see you now propose to give the same penalty to wrong unsat and sat answers. Any reasons for the change? I'm not sure that disqualifying a system after three wrong answers makes a lot of sense. You either allow any number of wrong answers, and rely on the scoring system to penalize, on average, buggy systems, or you completely discount the results of a system as soon as it gives you a wrong result. It is possible to make a good argument in favor of each of these two choices, but I cannot see how to justify your compromise solution. Given that - this is not the first edition of the competition, - you plan to have benchmarks available well in advance, - we expect to have a correct classification of the benchmarks, and - a solver has the option to answer "unknown" (or timeout), I would propose to go for immediate disqualification after the first wrong answer. Perhaps though not a disqualification from all divisions but only from those where wrong answers were given. The rationale here is that, since SMT solvers will most likely have specialized mechanisms for each divisions it is possible that a solver is correct for one division and buggy for another. Finally, in case you are not aware of it, you may want to take a look of what people are doing for the pseudo-boolean solver evaluation (http://www.cril.univ-artois.fr/PB06). It might be another useful source of suggestions. Cheers, Cesare From kendroe@hotmail.com Mon Feb 6 18:55:19 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k172tJ6H095314 for ; Mon, 6 Feb 2006 18:55:19 -0800 (PST) (envelope-from kendroe@hotmail.com) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k173IJiC008019 for ; Mon, 6 Feb 2006 19:18:29 -0800 (PST) (envelope-from kendroe@hotmail.com) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006020619182832350 for ; Mon, 06 Feb 2006 19:18:28 -0800 X-Original-Received: from bay112-f31.bay112.hotmail.com (HELO hotmail.com) (64.4.26.41) by mailgate-external2.sri.com with SMTP; 7 Feb 2006 03:18:28 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 6 Feb 2006 19:18:28 -0800 Message-ID: X-Original-Received: from 64.4.26.200 by by112fd.bay112.hotmail.msn.com with HTTP; Tue, 07 Feb 2006 03:18:27 GMT X-Originating-IP: [68.164.155.76] X-Originating-Email: [kendroe@hotmail.com] X-Sender: kendroe@hotmail.com From: "Kenneth Roe" To: smtcomp@csl.sri.com Date: Mon, 06 Feb 2006 19:18:27 -0800 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 07 Feb 2006 03:18:28.0291 (UTC) FILETIME=[2A170130:01C62B95] X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.8 required=4.0 tests=MSGID_FROM_MTA_HEADER=0.762 autolearn=no version=2.64 date=Mon, 06 Feb 2006 18:55:22 -0800 Subject: [SMTCOMP] Bit vector problems X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 07 Feb 2006 02:55:22 -0000 Since we do not have a bit vector division currently, I think it would be good to get some of the problems well before the June 1st date proposed in the SMT-COMP rules. I know CVC Lite has a substantial library of problems. However, they all look like small test cases. It would be nice to get a few large test cases within a month or two. I've heard rumors that Intel might donate some test cases. Can someone fill me in on the plans? Also, I've heard noises about quantifier problems and adding substantially to the other sections. What is the story here? - Ken From demoura@csl.sri.com Thu Feb 9 14:48:15 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k19MmF6H075418 for ; Thu, 9 Feb 2006 14:48:15 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.98.252] (wvc-118.csl.sri.com [130.107.97.118]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k19NBpN2031128 for ; Thu, 9 Feb 2006 15:11:51 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.2) Content-Transfer-Encoding: 7bit Message-Id: Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Thu, 9 Feb 2006 15:11:53 -0800 X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Thu, 09 Feb 2006 14:48:16 -0800 Subject: [SMTCOMP] WiSA benchmarks X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 09 Feb 2006 22:48:16 -0000 Hi I'm looking for more benchmarks from the Wisconsin Safety Analyzer (WiSA) project. SMT-LIB has only five instances of these benchmarks. Does anyone know where I can find them? Thanks, Leonardo From stump@priam.cse.wustl.edu Tue Feb 21 10:32:35 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k1LIWZ6H003321 for ; Tue, 21 Feb 2006 10:32:35 -0800 (PST) (envelope-from stump@priam.cse.wustl.edu) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k1LIw03C034308 for ; Tue, 21 Feb 2006 10:58:00 -0800 (PST) (envelope-from stump@priam.cse.wustl.edu) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006022110575900284 for ; Tue, 21 Feb 2006 10:57:59 -0800 X-Original-Received: from cliff.cse.wustl.edu (128.252.166.5) by mailgate-external1.sri.com with SMTP; 21 Feb 2006 18:57:58 -0000 X-Original-Received: from priam.cse.wustl.edu (priam.cse.wustl.edu [128.252.165.90]) by cliff.cse.wustl.edu (8.12.5/8.12.5) with ESMTP id k1LIvuMo022787 for ; Tue, 21 Feb 2006 12:57:56 -0600 (CST) X-Original-Received: from priam.cse.wustl.edu (stump@localhost) by priam.cse.wustl.edu (8.11.6/8.11.6) with ESMTP id k1LIuJQ06553 for ; Tue, 21 Feb 2006 12:56:19 -0600 Message-Id: <200602211856.k1LIuJQ06553@priam.cse.wustl.edu> To: smtcomp@csl.sri.com X-Mailer: MH-E 7.82; nmh 1.0.4; GNU Emacs 21.2.1 Date: Tue, 21 Feb 2006 12:56:19 -0600 From: Aaron Stump X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Tue, 21 Feb 2006 10:32:38 -0800 Subject: [SMTCOMP] final rules posted X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 21 Feb 2006 18:32:38 -0000 This is just to announce that we have revised the SMT-COMP 2006 rules according to the community feedback we received. Thanks to all who gave us suggestions on this. The rules are posted on the SMT-COMP 2006 site: http://www.csl.sri.com/users/demoura/smt-comp/ Below is copied a summary of the suggestions we received ("--") and our responses ("**"). Best wishes, Aaron for Clark and Leonardo, too. ---------------------------------------------------------------------- Windows -- could we also support Windows in addition to linux. ** no, we should not try to support Windows. Running the competition on multiple platforms is likely to provoke criticism, and isn't it the case that for remote execution machines need to be running Remote Desktop Server? Other results -- Results reported to the organizers by tools in a demonstration division should not be reported unverified to the public. ** well, that is a point. We are dropping the "demonstration division". Benchmarks -- Make *all* benchmarks available in advance ** yes, we should definitely do this, and not spring any new benchmarks on people that they haven't had a chance to run. Scrambling -- do perform simple formula scrambling. -- do not scramble structure; also there may be no point because simple scrambling can be easily defeated by an adversary ** we will design a simple pseudo-random scrambler, and publish it enough in advance so that people can make sure their tools handle its output. Buggy solvers: -- do eliminate solvers with more than some number of bugs. -- either disqualify solvers with even one buggy answer, or else just use the point system to penalize them out of contention. The compromise we suggest is hard to justify. ** We respectfully disagree with the last point, and will stick with the proposed scheme (disqualify a tool from all divisions if in any one division it gets more than three wrong answers; penalize by 8 points for each wrong answer). Benchmark selection -- do allow secret benchmarks -- uniformly random selection will be biased if the set of benchmarks contain a disproportionate number of benchmarks of a particular kind (e.g., "synthetic") ** no secret benchmarks, although it would be an intriguing twist to the competition; also, we must try to avoid skewing the selection to one kind of benchmark, as much as possible. Community building -- organize an informal dinner at FLoC. ** sounds good. Bitvectors -- the theory will probably be specified by end of March Quantifiers -- try to add a division with quantified formulas ** ok, if we have some formulas (as it sounds like we will). From demoura@csl.sri.com Wed Feb 22 07:53:03 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k1MFr36H030957 for ; Wed, 22 Feb 2006 07:53:03 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.5] (ovc-191.csl.sri.com [130.107.97.191]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k1MGIaEv027532 for ; Wed, 22 Feb 2006 08:18:36 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.2) Content-Transfer-Encoding: 7bit Message-Id: Content-Type: text/plain; charset=US-ASCII; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Wed, 22 Feb 2006 08:18:36 -0800 X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Wed, 22 Feb 2006 07:53:04 -0800 Subject: [SMTCOMP] Scrambler X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Feb 2006 15:53:04 -0000 This is just to announce that we have posted the benchmark scrambler is available on the SMT-COMP website. http://www.csl.sri.com/users/demoura/smt-comp/ From demoura@csl.sri.com Wed Feb 22 10:49:19 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k1MInJ6H038173 for ; Wed, 22 Feb 2006 10:49:19 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.5] (ovc-191.csl.sri.com [130.107.97.191]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k1MJEqwu043763 for ; Wed, 22 Feb 2006 11:14:53 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.2) Content-Transfer-Encoding: 7bit Message-Id: Content-Type: text/plain; charset=US-ASCII; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Wed, 22 Feb 2006 11:14:52 -0800 X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.013 autolearn=no version=2.64 date=Wed, 22 Feb 2006 10:49:19 -0800 Subject: [SMTCOMP] Scrambler updated X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Feb 2006 18:49:20 -0000 The benchmark scrambler has been updated. This update fixes a bug in examples that contain big numbers. From demoura@csl.sri.com Sun Mar 19 12:41:08 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2JKf86H054053 for ; Sun, 19 Mar 2006 12:41:08 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-194.csl.sri.com [130.107.97.194]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k2JKf8Mp066798 for ; Sun, 19 Mar 2006 12:41:08 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.3) Content-Transfer-Encoding: 7bit Message-Id: <2BE8E22F-C7CB-4E5B-8D7B-76111A59A9AE@csl.sri.com> Content-Type: text/plain; charset=US-ASCII; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Sun, 19 Mar 2006 12:41:12 -0800 X-Mailer: Apple Mail (2.746.3) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.012 autolearn=no version=2.64 date=Sun, 19 Mar 2006 12:41:09 -0800 Subject: [SMTCOMP] New benchmarks X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 19 Mar 2006 20:41:09 -0000 Hi, There are 480 new benchmarks available on the website for the following divisions: QF_RDL, QF_IDL, QF_UFIDL, and QF_LRA. There are several SAT instances in this new suite. More benchmarks will be available later. The following people contributed directly or indirectly: Bruno Dutertre, Geoffrey Brown, Lee Pike, Rick Butler, Kazuhiro Ogata, and Pete Manolios. Leonardo From kendroe@hotmail.com Mon Mar 20 23:14:59 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2L7Ex6H090880 for ; Mon, 20 Mar 2006 23:14:59 -0800 (PST) (envelope-from kendroe@hotmail.com) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k2L7Exhl099370 for ; Mon, 20 Mar 2006 23:14:59 -0800 (PST) (envelope-from kendroe@hotmail.com) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006032023145812051 for ; Mon, 20 Mar 2006 23:14:58 -0800 X-Original-Received: from bay112-f5.bay112.hotmail.com (HELO hotmail.com) (64.4.26.15) by mailgate-external2.sri.com with SMTP; 21 Mar 2006 07:14:58 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 20 Mar 2006 23:14:57 -0800 Message-ID: X-Original-Received: from 64.4.26.200 by by112fd.bay112.hotmail.msn.com with HTTP; Tue, 21 Mar 2006 07:14:56 GMT X-Originating-IP: [68.164.91.99] X-Originating-Email: [kendroe@hotmail.com] X-Sender: kendroe@hotmail.com From: "Kenneth Roe" To: smtcomp@csl.sri.com Date: Mon, 20 Mar 2006 23:14:56 -0800 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 21 Mar 2006 07:14:57.0915 (UTC) FILETIME=[291D4CB0:01C64CB7] X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.8 required=4.0 tests=MSGID_FROM_MTA_HEADER=0.762 autolearn=no version=2.64 date=Mon, 20 Mar 2006 23:15:00 -0800 Subject: [SMTCOMP] HTP website X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 21 Mar 2006 07:15:00 -0000 I have created a website that contains information on HTP including recent results on many of the SMTLIB problems, papers and talks, and a downloadable executable. The website is located at www.fordocsys.com or www.fordocsys.com/htp.htm. One item that might be of interest to the other developers is the preprocessing mode for HTP. It simplifies SMTLIB problems and then prints them out in SMTLIB format. This will likely be a useful source for additional test cases. I might donate some of the preprocessor outputs to the competition. - Ken From demoura@csl.sri.com Tue Mar 21 16:14:36 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44 autolearn=disabled version=3.1.1 date=Tue, 21 Mar 2006 16:14:37 -0800 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.12.9) with ESMTP id k2M0EaVo027289 for ; Tue, 21 Mar 2006 16:14:36 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-194.csl.sri.com [130.107.97.194]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k2M0Ea98069391 for ; Tue, 21 Mar 2006 16:14:36 -0800 (PST) (envelope-from demoura@csl.sri.com) Mime-Version: 1.0 (Apple Message framework v746.3) Content-Transfer-Encoding: 7bit Message-Id: <50D0D70E-EB8B-44A8-8879-1C511E6B5CE5@csl.sri.com> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: smtcomp@csl.sri.com From: Leonardo de Moura Date: Tue, 21 Mar 2006 16:14:35 -0800 X-Mailer: Apple Mail (2.746.3) Subject: [SMTCOMP] n-queens SMT benchmarks available X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Mar 2006 00:14:37 -0000 Hi, Hyondeuk (Univ. Colorado at Boulder) submitted several benchmarks based on the n-queens problem. They can be downloaded at: http://www.csl.sri.com/users/demoura/smt-comp/benchmarks.shtml Leonardo From pocmatos@gmail.com Wed Mar 29 12:15:22 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=DK_SIGNED=0.001 autolearn=disabled version=3.1.1 date=Wed, 29 Mar 2006 12:15:25 -0800 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k2TKFMRJ035038 for ; Wed, 29 Mar 2006 12:15:22 -0800 (PST) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k2TKFKjI003398 for ; Wed, 29 Mar 2006 12:15:22 -0800 (PST) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006032912152111341 for ; Wed, 29 Mar 2006 12:15:21 -0800 X-Original-Received: from wproxy.gmail.com (64.233.184.225) by mailgate-external1.sri.com with SMTP; 29 Mar 2006 20:15:19 -0000 X-Original-Received: by wproxy.gmail.com with SMTP id i7so524894wra for ; Wed, 29 Mar 2006 12:15:18 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=ERC5v7YnBLEkbm6sAiEvFHN0gsC0/TbwkbtCp0ykUE2SkFi4lx3K1tOBVil1o0tBSOFv5pieQ8k3pvRnPUNgL66NxC29k2ANRu7bfDWIxYREhFMlKRTI2R0BceAKKw7thJCjf+5sfpVJ2yMNjtA9smXBxfYDP6BjuvNwGPYVdkc= X-Original-Received: by 10.64.193.19 with SMTP id q19mr346664qbf; Wed, 29 Mar 2006 12:15:11 -0800 (PST) X-Original-Received: by 10.65.216.14 with HTTP; Wed, 29 Mar 2006 12:15:11 -0800 (PST) Message-ID: <11b141710603291215k5659d57eve7c836381a0f400e@mail.gmail.com> Date: Wed, 29 Mar 2006 21:15:11 +0100 From: "Paulo J. Matos" To: smtcomp@csl.sri.com MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by postal.csl.sri.com id k2TKFMRJ035038 Subject: [SMTCOMP] Timeline doubt X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: pocm@sat.inesc-id.pt List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 29 Mar 2006 20:15:25 -0000 Hi all, Systems should be sent in until 8th August? Seems too late compared to last year. Still I can't see anything resembling a deadline for solver registration. Cheers, -- Paulo Jorge Matos - pocm at sat inesc-id pt Web: http://sat.inesc-id.pt/~pocm Computer and Software Engineering INESC-ID - SAT Group From barrett@dept.cs.nyu.edu Wed Mar 29 12:18:46 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=none autolearn=disabled version=3.1.1 date=Wed, 29 Mar 2006 12:18:47 -0800 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k2TKIkNr035093 for ; Wed, 29 Mar 2006 12:18:46 -0800 (PST) (envelope-from barrett@dept.cs.nyu.edu) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k2TKIk2d003666 for ; Wed, 29 Mar 2006 12:18:46 -0800 (PST) (envelope-from barrett@dept.cs.nyu.edu) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006032912184511522 for ; Wed, 29 Mar 2006 12:18:45 -0800 X-Original-Received: from dept.cs.nyu.edu (128.122.80.31) by mailgate-external1.sri.com with SMTP; 29 Mar 2006 20:18:46 -0000 X-Original-Received: from dept.cs.nyu.edu (localhost [127.0.0.1]) by dept.cs.nyu.edu (8.13.6+Sun/8.13.6) with ESMTP id k2TKIiEV000781; Wed, 29 Mar 2006 15:18:45 -0500 (EST) X-Original-Received: (from barrett@localhost) by dept.cs.nyu.edu (8.13.6+Sun/8.12.2/Submit) id k2TKIi8M000779; Wed, 29 Mar 2006 15:18:44 -0500 (EST) From: Clark Barrett Message-Id: <200603292018.k2TKIi8M000779@dept.cs.nyu.edu> Subject: Re: [SMTCOMP] Timeline doubt To: pocm@sat.inesc-id.pt Date: Wed, 29 Mar 2006 15:18:44 -0500 (EST) In-Reply-To: <11b141710603291215k5659d57eve7c836381a0f400e@mail.gmail.com> X-Mailer: ELM [version 2.5 PL7] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Cc: smtcomp@csl.sri.com X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 29 Mar 2006 20:18:47 -0000 Paulo, We are still finalizing a couple of new divisions for this year. Once those are finalized, we will issue a broad call for benchmarks and solvers. This should occur within the next month or so. We encourage people to submit solvers early, but we will accept solvers up until August 8. -Clark > > Hi all, > > Systems should be sent in until 8th August? Seems too late compared to > last year. > Still I can't see anything resembling a deadline for solver registration. > > Cheers, > -- > Paulo Jorge Matos - pocm at sat inesc-id pt > Web: http://sat.inesc-id.pt/~pocm > Computer and Software Engineering > INESC-ID - SAT Group > > From pocmatos@gmail.com Wed Mar 29 15:19:34 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.7 required=4.0 tests=AWL=-0.666,DK_SIGNED=0.001, RCVD_IN_BL_SPAMCOP_NET=1.332 autolearn=disabled version=3.1.1 date=Wed, 29 Mar 2006 15:19:36 -0800 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k2TNJYS5037794 for ; Wed, 29 Mar 2006 15:19:34 -0800 (PST) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k2TNJYOC015476 for ; Wed, 29 Mar 2006 15:19:34 -0800 (PST) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006032915193402074 for ; Wed, 29 Mar 2006 15:19:34 -0800 X-Original-Received: from wproxy.gmail.com (64.233.184.236) by mailgate-external1.sri.com with SMTP; 29 Mar 2006 23:19:33 -0000 X-Original-Received: by wproxy.gmail.com with SMTP id i7so559539wra for ; Wed, 29 Mar 2006 15:19:32 -0800 (PST) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=iJvcY0C2Ia+xnKOmhgU1erFn5/Uu8tR5A5DBTOVqBqaak0dTABNyRTDk3c3nIKUrnn2Dj6PbSvXFz/jCH/LzGWXSfLyo5e554XhebUvyVsGWRabGuaRX5tRzsMRSqw7mEqvCgMBL8A1LZ7SE6FmsQHDzAdNtly5z1Ysy3+8GE3o= X-Original-Received: by 10.65.183.5 with SMTP id k5mr121334qbp; Wed, 29 Mar 2006 15:19:32 -0800 (PST) X-Original-Received: by 10.65.216.14 with HTTP; Wed, 29 Mar 2006 15:19:32 -0800 (PST) Message-ID: <11b141710603291519r6b0269b2ne29a58556022bd0f@mail.gmail.com> Date: Thu, 30 Mar 2006 00:19:32 +0100 From: "Paulo J. Matos" To: "Clark Barrett" , smtcomp@csl.sri.com Subject: Re: [SMTCOMP] Timeline doubt In-Reply-To: <200603292018.k2TKIi8M000779@dept.cs.nyu.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Disposition: inline References: <11b141710603291215k5659d57eve7c836381a0f400e@mail.gmail.com> <200603292018.k2TKIi8M000779@dept.cs.nyu.edu> Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by postal.csl.sri.com id k2TNJYS5037794 Cc: X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: pocm@sat.inesc-id.pt List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 29 Mar 2006 23:19:37 -0000 On 29/03/06, Clark Barrett wrote: > Paulo, > > We are still finalizing a couple of new divisions for this year. Once those > are finalized, we will issue a broad call for benchmarks and solvers. This > should occur within the next month or so. We encourage people to submit > solvers early, but we will accept solvers up until August 8. > Ah, thanks for the reply. Hopefully I didn't miss any deadline then. Thanks, Paulo Matos > -Clark > > > > > Hi all, > > > > Systems should be sent in until 8th August? Seems too late compared to > > last year. > > Still I can't see anything resembling a deadline for solver registration. > > > > Cheers, > > -- > > Paulo Jorge Matos - pocm at sat inesc-id pt > > Web: http://sat.inesc-id.pt/~pocm > > Computer and Software Engineering > > INESC-ID - SAT Group > > > > > > -- Paulo Jorge Matos - pocm at sat inesc-id pt Web: http://sat.inesc-id.pt/~pocm Computer and Software Engineering INESC-ID - SAT Group From pocmatos@gmail.com Thu Apr 27 08:51:43 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.3 required=4.0 tests=AWL=0.333,DK_SIGNED=0.001 autolearn=disabled version=3.1.1 date=Thu, 27 Apr 2006 08:51:46 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3RFphQu097262 for ; Thu, 27 Apr 2006 08:51:43 -0700 (PDT) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3RFpefn095969 for ; Thu, 27 Apr 2006 08:51:43 -0700 (PDT) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006042708514313859 for ; Thu, 27 Apr 2006 08:51:43 -0700 X-Original-Received: from nz-out-0102.google.com (64.233.162.198) by mailgate-external1.sri.com with SMTP; 27 Apr 2006 15:51:42 -0000 X-Original-Received: by nz-out-0102.google.com with SMTP id q3so2586551nzb for ; Thu, 27 Apr 2006 08:51:31 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=LNHDJpS25qt2fVykh0dSJJ3n5/SmVY+77WDFVZOgqoyIY1I06wFEuIO0yZ/di2uxYY0BYrufdm7ugP6VuWBj6YuTY8ib7SIN2rlsUYvzI9skJrBBFdbjfKJOaGsKgBxjsikAzXTJSw1phHDEaolg1C0ezv92F+i49riOHmgf+Qs= X-Original-Received: by 10.64.193.11 with SMTP id q11mr742963qbf; Thu, 27 Apr 2006 08:51:31 -0700 (PDT) X-Original-Received: by 10.65.73.13 with HTTP; Thu, 27 Apr 2006 08:51:31 -0700 (PDT) Message-ID: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> Date: Thu, 27 Apr 2006 16:51:31 +0100 From: "Paulo J. Matos" To: smtcomp@csl.sri.com MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by postal.csl.sri.com id k3RFphQu097262 Subject: [SMTCOMP] Sudoku based instances X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: pocm@sat.inesc-id.pt List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 27 Apr 2006 15:51:47 -0000 Hi all, I have generated some sudoku based instances. Would those be interesting for SMTCOMP? Want me to send them in? Cheers, -- Paulo Jorge Matos - pocm at sat inesc-id pt Web: http://sat.inesc-id.pt/~pocm Computer and Software Engineering INESC-ID - SAT Group From hhkim@colorado.edu Thu Apr 27 10:00:27 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Thu, 27 Apr 2006 10:00:27 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3RH0RJX098951 for ; Thu, 27 Apr 2006 10:00:27 -0700 (PDT) (envelope-from hhkim@colorado.edu) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3RH0RMw001495 for ; Thu, 27 Apr 2006 10:00:27 -0700 (PDT) (envelope-from hhkim@colorado.edu) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006042710002710876 for ; Thu, 27 Apr 2006 10:00:27 -0700 X-Original-Received: from farley1.colorado.edu (128.138.129.102) by mailgate-external2.sri.com with SMTP; 27 Apr 2006 17:00:26 -0000 X-Original-Received: (from nobody@localhost) by farley1.Colorado.EDU (8.13.6/8.13.6/ITS-6.0/webmail) id k3RH0MMk003472; Thu, 27 Apr 2006 11:00:22 -0600 (MDT) From: Hyondeuk.Kim@colorado.edu X-Original-Received: from dizzy.colorado.edu (dizzy.colorado.edu [128.138.189.48]) by webmail.colorado.edu (IMP) with HTTP for ; Thu, 27 Apr 2006 11:00:22 -0600 Message-ID: <1146157222.4450f8a6afb59@webmail.colorado.edu> Date: Thu, 27 Apr 2006 11:00:22 -0600 To: pocm@sat.inesc-id.pt, "Paulo J. Matos" Subject: Re: [SMTCOMP] Sudoku based instances References: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> In-Reply-To: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: Internet Messaging Program (IMP) 3.2-cvs Cc: smtcomp@csl.sri.com X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 27 Apr 2006 17:00:28 -0000 Yeah, I think they are interesting. Hyondeuk Quoting "Paulo J. Matos" : > Hi all, > > I have generated some sudoku based instances. Would those be > interesting for SMTCOMP? > Want me to send them in? > > Cheers, > -- > Paulo Jorge Matos - pocm at sat inesc-id pt > Web: http://sat.inesc-id.pt/~pocm > Computer and Software Engineering > INESC-ID - SAT Group > From bruno@csl.sri.com Thu Apr 27 10:57:51 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44 autolearn=disabled version=3.1.1 date=Thu, 27 Apr 2006 10:57:51 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3RHvpZp000965 for ; Thu, 27 Apr 2006 10:57:51 -0700 (PDT) (envelope-from bruno@csl.sri.com) X-Original-Received: from [130.107.15.210] (box.csl.sri.com [130.107.15.210]) by mx1.csl.sri.com (8.13.4/8.12.11) with ESMTP id k3RHvpco006668; Thu, 27 Apr 2006 10:57:51 -0700 (PDT) (envelope-from bruno@csl.sri.com) Message-ID: <4451061F.2010704@csl.sri.com> Date: Thu, 27 Apr 2006 10:57:51 -0700 From: Bruno Dutertre User-Agent: Mozilla Thunderbird 0.7.3 (X11/20040803) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Hyondeuk.Kim@colorado.edu Subject: Re: [SMTCOMP] Sudoku based instances References: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> <1146157222.4450f8a6afb59@webmail.colorado.edu> In-Reply-To: <1146157222.4450f8a6afb59@webmail.colorado.edu> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Cc: smtcomp@csl.sri.com, pocm@sat.inesc-id.pt X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 27 Apr 2006 17:57:51 -0000 Hyondeuk.Kim@colorado.edu wrote: > Yeah, I think they are interesting. > > Hyondeuk > Well, I'm not so sure these kinds of puzzles are particularly relevant to SMT: - they can be encoded as a big conjunction (no Boolean structure). - they do not require combination of decision procedures - they are probably easy to solve using CSP or pure Boolean SAT techniques and encoding them in arithmetic is likely to be much less efficient. I doubt anybody who really cares about solving Soduku (if such a person exists) would think of using SMT solvers for it. Because of this, I don't think performance of an SMT solver on Sudoku is likely to tell us a lot about performance of the same solver on more realistic applications (e.g., verification problems). We should try to evaluate SMT solvers on problems that require decision procedures, not on problems that can be solved faster/better using other methods. Bruno > Quoting "Paulo J. Matos" : > > >>Hi all, >> >>I have generated some sudoku based instances. Would those be >>interesting for SMTCOMP? >>Want me to send them in? >> >>Cheers, >>-- >>Paulo Jorge Matos - pocm at sat inesc-id pt >>Web: http://sat.inesc-id.pt/~pocm >>Computer and Software Engineering >>INESC-ID - SAT Group >> > > > -- Bruno Dutertre | bruno@csl.sri.com CSL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717 From tinelli@cs.uiowa.edu Thu Apr 27 16:31:59 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=none autolearn=disabled version=3.1.1 date=Thu, 27 Apr 2006 16:31:59 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3RNVxvp023962 for ; Thu, 27 Apr 2006 16:31:59 -0700 (PDT) (envelope-from tinelli@cs.uiowa.edu) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3RNVwLB051880 for ; Thu, 27 Apr 2006 16:31:59 -0700 (PDT) (envelope-from tinelli@cs.uiowa.edu) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006042716315831206 for ; Thu, 27 Apr 2006 16:31:58 -0700 X-Original-Received: from serv07.divms.uiowa.edu (128.255.44.97) by mailgate-external2.sri.com with SMTP; 27 Apr 2006 23:31:58 -0000 X-Original-Received: from [10.0.1.2] (12-215-116-89.client.mchsi.com [12.215.116.89]) by serv07.divms.uiowa.edu with id k3RNVmtE024062; Thu, 27 Apr 2006 18:31:51 -0500 Message-ID: <44515464.1020300@cs.uiowa.edu> Date: Thu, 27 Apr 2006 18:31:48 -0500 From: Cesare Tinelli User-Agent: Thunderbird 1.5.0.2 (Macintosh/20060308) MIME-Version: 1.0 To: pocm@sat.inesc-id.pt Subject: Re: [SMTCOMP] Sudoku based instances References: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> In-Reply-To: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Scanned-By: MIMEDefang 2.55 on 128.255.44.22 X-Virus-Scanned: ClamAV version 0.88.1, clamav-milter version 0.88.1 on serv07.divms.uiowa.edu X-Virus-Status: Clean Cc: smtcomp@csl.sri.com X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 27 Apr 2006 23:31:59 -0000 Hi Paulo, Paulo J. Matos wrote: > Hi all, > > I have generated some sudoku based instances. Would those be > interesting for SMTCOMP? > Want me to send them in? > Thanks a lot for the offer. But I think that the goals of SMT-LIB and SMT-COMP would be better served by different classes of benchmarks, as nicely explained by Bruno in his reply. Best, Cesare > Cheers, > -- > Paulo Jorge Matos - pocm at sat inesc-id pt > Web: http://sat.inesc-id.pt/~pocm > Computer and Software Engineering > INESC-ID - SAT Group > From pocmatos@gmail.com Fri Apr 28 03:37:21 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=0.222,DK_SIGNED=0.001 autolearn=disabled version=3.1.1 date=Fri, 28 Apr 2006 03:37:22 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3SAbL0R034143 for ; Fri, 28 Apr 2006 03:37:21 -0700 (PDT) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3SAbLKT090921 for ; Fri, 28 Apr 2006 03:37:21 -0700 (PDT) (envelope-from pocmatos@gmail.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006042803372128351 for ; Fri, 28 Apr 2006 03:37:21 -0700 X-Original-Received: from wproxy.gmail.com (64.233.184.224) by mailgate-external1.sri.com with SMTP; 28 Apr 2006 10:37:20 -0000 X-Original-Received: by wproxy.gmail.com with SMTP id 58so90616wri for ; Fri, 28 Apr 2006 03:37:20 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=FUW3+VwwNT2TjBwMCV2+3ca+GCqFQbjnWr3lF0MvYKxQ+NgIbJBMneT//DDdmHxoE4m8eLfFZA3Q7Z/rBKHRTyDQkYR+bkFRxHfUiIBYkJJk84ToDIPZTmE2AGo7QT+54pj9EjsfWZZ2EO9+gTdB0Xh8RmkPQtztBX4BqvIoaqI= X-Original-Received: by 10.65.72.6 with SMTP id z6mr1323985qbk; Fri, 28 Apr 2006 03:37:20 -0700 (PDT) X-Original-Received: by 10.65.73.13 with HTTP; Fri, 28 Apr 2006 03:37:20 -0700 (PDT) Message-ID: <11b141710604280337h482b64a9tde74559593165269@mail.gmail.com> Date: Fri, 28 Apr 2006 11:37:20 +0100 From: "Paulo J. Matos" To: "Bruno Dutertre" Subject: Re: [SMTCOMP] Sudoku based instances In-Reply-To: <4451061F.2010704@csl.sri.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Disposition: inline References: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> <1146157222.4450f8a6afb59@webmail.colorado.edu> <4451061F.2010704@csl.sri.com> Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by postal.csl.sri.com id k3SAbL0R034143 Cc: smtcomp@csl.sri.com, Hyondeuk.Kim@colorado.edu X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: pocm@sat.inesc-id.pt List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 28 Apr 2006 10:37:22 -0000 On 27/04/06, Bruno Dutertre wrote: > Hyondeuk.Kim@colorado.edu wrote: > > Yeah, I think they are interesting. > > > > Hyondeuk > > > > Well, I'm not so sure these kinds of puzzles are particularly > relevant to SMT: In fact I don't think they are relevant for the SMT Competition... I've sent the email initially to know if would be interesting for anyone in this mailing list. > - they can be encoded as a big conjunction (no Boolean structure). Indeed, I agree with you although we can also make the encoding as complex as we wish adding additional redundant information. Still, the benchmarks were generated to test my solver and not to make interesting benchmarks. > - they do not require combination of decision procedures That's not really a problem, right? IDL doesn't require a combination of decision procedures. Only a Boolean enumerator and a decision procedure for difference constraints are needed. > - they are probably easy to solve using CSP or pure Boolean > SAT techniques and encoding them in arithmetic is likely > to be much less efficient. I doubt anybody who really cares > about solving Soduku (if such a person exists) would think > of using SMT solvers for it. I don't think people use solvers, be it CSPs or SAT solvers, in the daily life to solve sudoku anyways. As I said they were interesting at least for me because I can make them as hard as I want and test not only the performance of the solver but also its memory usage and its data structures. > > Because of this, I don't think performance of an SMT solver > on Sudoku is likely to tell us a lot about performance of the > same solver on more realistic applications (e.g., verification > problems). Agree, but not all examples in SMTCOMP are 'realistic' anyways. > We should try to evaluate SMT solvers on problems that > require decision procedures, not on problems that can be solved > faster/better using other methods. > Indeed! Probably I was misunderstood, I don't think they should be used for SMT Solver comparison or evaluation or even to be used for sudoku solving. Just though someone might be interested in them just for hobby, testing or any other non-pratical motif. Anyway, I agree with you when you say that they are not useful for the competition. :) Cheers, Paulo Matos > Bruno > > > > Quoting "Paulo J. Matos" : > > > > > >>Hi all, > >> > >>I have generated some sudoku based instances. Would those be > >>interesting for SMTCOMP? > >>Want me to send them in? > >> > >>Cheers, > >>-- > >>Paulo Jorge Matos - pocm at sat inesc-id pt > >>Web: http://sat.inesc-id.pt/~pocm > >>Computer and Software Engineering > >>INESC-ID - SAT Group > >> > > > > > > > -- > Bruno Dutertre | bruno@csl.sri.com > CSL, SRI International | fax: 650 859-2844 > 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717 > > -- Paulo Jorge Matos - pocm at sat inesc-id pt Web: http://sat.inesc-id.pt/~pocm Computer and Software Engineering INESC-ID - SAT Group From hhkim@colorado.edu Sat Apr 29 21:36:46 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Sat, 29 Apr 2006 21:36:49 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3U4akNU079513 for ; Sat, 29 Apr 2006 21:36:46 -0700 (PDT) (envelope-from hhkim@colorado.edu) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3U4ajlU043289 for ; Sat, 29 Apr 2006 21:36:46 -0700 (PDT) (envelope-from hhkim@colorado.edu) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006042921364510321 for ; Sat, 29 Apr 2006 21:36:45 -0700 X-Original-Received: from farley1.colorado.edu (128.138.129.102) by mailgate-external1.sri.com with SMTP; 30 Apr 2006 04:36:44 -0000 X-Original-Received: (from nobody@localhost) by farley1.Colorado.EDU (8.13.6/8.13.6/ITS-6.0/webmail) id k3U4ahwd003492; Sat, 29 Apr 2006 22:36:43 -0600 (MDT) From: Hyondeuk.Kim@colorado.edu X-Original-Received: from dizzy.colorado.edu (dizzy.colorado.edu [128.138.189.48]) by webmail.colorado.edu (IMP) with HTTP for ; Sat, 29 Apr 2006 22:36:43 -0600 Message-ID: <1146371803.44543edb78a83@webmail.colorado.edu> Date: Sat, 29 Apr 2006 22:36:43 -0600 To: pocm@sat.inesc-id.pt, "Paulo J. Matos" Subject: Re: [SMTCOMP] Sudoku based instances References: <11b141710604270851l16d7270djace5e1a2ef4917db@mail.gmail.com> <1146157222.4450f8a6afb59@webmail.colorado.edu> <4451061F.2010704@csl.sri.com> <11b141710604280337h482b64a9tde74559593165269@mail.gmail.com> In-Reply-To: <11b141710604280337h482b64a9tde74559593165269@mail.gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: Internet Messaging Program (IMP) 3.2-cvs Cc: Bruno Dutertre , smtcomp@csl.sri.com, Hyondeuk.Kim@colorado.edu X-BeenThere: smtcomp@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SMTCOMP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: