From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 055FB5D5 for ; Thu, 19 Apr 2018 18:28:25 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,297,1520895600"; d="scan'208";a="323692338" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 19 Apr 2018 20:28:24 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id BF0A782444; Thu, 19 Apr 2018 20:28:24 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 4444F8240C for ; Thu, 19 Apr 2018 20:26:32 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=geoff@cs.miami.edu; spf=Pass smtp.mailfrom=geoff@cs.miami.edu; spf=None smtp.helo=postmaster@mail-ua0-f228.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AVV0gYB9MMQjGhv9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?0+kcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hi?= =?us-ascii?q?kANDA3/mHZh9dsgK5HvB6tuwZyz5LIbIyTKfFwfrndfdQfRWdZUcZeSStBAo2y?= =?us-ascii?q?b4YUE+UBJvxUr4z8p1QUqBu+BBOgC/3yxT9VgHL9wKM00+MkEQ7c3QwgGcoDsG?= =?us-ascii?q?jMrNXpLKceS+e1zLPHzTjFcvhY2i/95ZDWfhw9pfyAR7F9fMrLxUUxCg/IjE+c?= =?us-ascii?q?pZL7Mz6WzugBrmyW4/R6We+hlmIrsQJ8rzy1yssxlIXEgJ8exEre+iVj2ok1IM?= =?us-ascii?q?W1SE5lbt6gF5tdrySaOJF3QsMmWm1opTw1xqEftZ61YiQG1pcqywTQa/yAdIiI?= =?us-ascii?q?7RbjW/iLLThkg3Jlfaqzhxe08Ue+1u3xTte43EpOoyZfkdTBtmoB2wLO5sWFUP?= =?us-ascii?q?dx4Fmt1DWX2wDW8O5EIEQ0laTBK54mx749jpUTvlrEHi/4lkX7l7OZdl4+9uit?= =?us-ascii?q?6uToeLDmpp6GO4Bqlw7+L7wimtajDuQgLggOQ2+b9Pyg27L5+E35RKxGjvk3kq?= =?us-ascii?q?nCrJDXPt8bp668Aw9NyIkv8Re/DzG80NQZh3YLNlxFeAjUx7TubgXFKfX8SPO+?= =?us-ascii?q?mEiEkTFxxvmAMKe3UbvXKX2Wn7rmc7hV4FUazQs6yNEZ6p5JWeJJG+76RkKk7I?= =?us-ascii?q?+QNRQ+KQHhm7+2WuU47ZsXXCe0OoHcNarTtVGS4ed2f7uHf8kQuT/4Kr4o6+O8?= =?us-ascii?q?1CZly29YRrGg2N4sUF79Bu5vehnLamGqh9YIFGZMswYjHrSz1Q+yFAVLbnP3ZJ?= =?us-ascii?q?oSozE2DIX8U9XGT4GpxaGIhGK1RMcGIG9BDV+IHDHjcIDWA/o=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CmBgD/3thah+TZVdFbHQEBBQELAYQjg?= =?us-ascii?q?SKMSIwZgwOUFQNTAQofhw0ZBwEENRMBAgEBAQEBAQEBARMBAQEIDQkIKCMMgjU?= =?us-ascii?q?igm8jAQEmEjs0HQgBBQEiHAsHhHKbCDyKGIMJgm8BAQWBY4MBBx1Egh0ICQEIh?= =?us-ascii?q?3SCE4EPgl2FbYJkgiSHMZA+CIgphgmBP4NdgimFE5AYDyGBBDSBcnKDEQmCCxq?= =?us-ascii?q?DToUUhVpTAZBCAQE?= X-IPAS-Result: =?us-ascii?q?A0CmBgD/3thah+TZVdFbHQEBBQELAYQjgSKMSIwZgwOUFQN?= =?us-ascii?q?TAQofhw0ZBwEENRMBAgEBAQEBAQEBARMBAQEIDQkIKCMMgjUigm8jAQEmEjs0H?= =?us-ascii?q?QgBBQEiHAsHhHKbCDyKGIMJgm8BAQWBY4MBBx1Egh0ICQEIh3SCE4EPgl2FbYJ?= =?us-ascii?q?kgiSHMZA+CIgphgmBP4NdgimFE5AYDyGBBDSBcnKDEQmCCxqDToUUhVpTAZBCA?= =?us-ascii?q?QE?= X-IronPort-AV: E=Sophos;i="5.49,297,1520895600"; d="scan'208";a="262690923" Received: from mail-ua0-f228.google.com ([209.85.217.228]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Apr 2018 20:26:31 +0200 Received: by mail-ua0-f228.google.com with SMTP id g10so4074099ual.6 for ; Thu, 19 Apr 2018 11:26:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs-miami-edu.20150623.gappssmtp.com; s=20150623; h=subject:to:message-id:date:from; bh=L+HigpXbSd9pWxBVnqEcTjai8YPVxc+EpIEjz2Rqw9g=; b=xKVzhZuosUqJhoF+Qy8cvPafKBO4XKUZuY50K2QfBk7dcHBG2UjZj8cRRB69OAO5Jf sWnZ/l0rbVYjjLp9OVcjgt4Oo/HSsK2rSKhcWIbF9d/uV7Ztvcx1lUCUk0lJ1PzDRvRm IOj/Tb+GRWeDiBzqn+aSGZlTaiVY1nmF25vbvj5xOZB4dBoiiPh2pIoBQkRqF0VnwbWP 6XGPk4BHFlPFO+ScY8z/6wYEPau1xob/JoV7ZWgi1iPAUh8ZiVP2vHGd3DPn0Z7+UMRQ yLTJingPD2qWwVyToUqxlJDvLmluKmiuoIJ2jVtcSs7kqLpSDmSm94V3d0Z1+4egUHfF wZfQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:message-id:date:from; bh=L+HigpXbSd9pWxBVnqEcTjai8YPVxc+EpIEjz2Rqw9g=; b=o+sTVWqHOWa/+aVGb2nLVff4PtExnSZnxW/C7K0q6zXcdMBXYJ9ryCA8ooqaml5D30 gcg1SG7XOJ7RxnwwaI2vp1XSV34UGksqvbFF4DqFV/YOMNg/4tnsVEKco1ToQ6mqT4A4 maqwwX6ve4rnLv4ZbYmqlol1uEtVyVzLpZUrytJTnCiNGgIZAV67/LM5s1KTElslfmB1 UovKgpXJ9EzNEsDkDFOeJaSu+r4M+tZOWN54RWNrFYrJe7MHK7AskSrNS1GE8KfxGnTO KMZZaGok4g6YnMm7YgWgnAh5hu9d7jU69CEFjY8Z+vtuOsTG1foO5ePTj3xBqMVOau36 lI1g== X-Gm-Message-State: ALQs6tB2bWlzfwd8kgvHqqgLIPEuweB6Mj8o8ZxhaDFxX12YWz4dVLQL AH498jUSwL8GTL4TBtAGSWkdQnYVid8Ro5plRXXmBpdPotPYuQ== X-Google-Smtp-Source: AIpwx48ODB+MAtx2PSSB94pCp+SjLQDaue65VVvj512KW5e5xUfVU1Iu5fnk951jGIxA/2pwPS8iajNUPT/N X-Received: by 10.159.38.228 with SMTP id 91mr5503270uay.46.1524162390500; Thu, 19 Apr 2018 11:26:30 -0700 (PDT) Received: from cs.miami.edu (ewell.cs.miami.edu. [192.31.89.12]) by smtp-relay.gmail.com with ESMTP id h1sm78112uan.0.2018.04.19.11.26.29 for ; Thu, 19 Apr 2018 11:26:30 -0700 (PDT) X-Relaying-Domain: cs.miami.edu Received: by cs.miami.edu (Postfix, from userid 3640) id 4F6A31700DF2; Thu, 19 Apr 2018 14:19:34 -0400 (EDT) To: X-Mailer: mail (GNU Mailutils 2.99.98) Message-Id: <20180419181934.4F6A31700DF2@cs.miami.edu> Date: Thu, 19 Apr 2018 14:19:34 -0400 (EDT) From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CASC-J9 - the ATP System Competition - Call for Systems Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 16833 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: ------------------------------------------------------------------------------- CASC-J9 - The CADE ATP System Competition to be held at The 9th International Joint Conference on Automated Reasoning Oxford, United Kingdom, 14th-17th July 2018 The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J9 will be held on the 14th July 2018, during the 9th International Joint Conference on Automated Reasoning. CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of: + the number of problems solved, and + the number of problems solved with a solution output, and + the average runtime for problems solved; in the context of: + a bounded number of eligible problems, chosen from the TPTP library, and + specified time limits for solution attempts. The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available at: http://www.tptp.org/CASC/J9/ Registration of systems for CASC-J9 is now invited. System registration closes on 11th June. Please register early so that adequate resources can be allocated. DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! ------------------------------------------------------------------------------- -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs