From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 8961D8240C for ; Wed, 23 May 2018 23:35:52 +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-f226.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of geoff@cs.miami.edu) identity=pra; client-ip=209.85.217.226; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of geoff@cs.miami.edu designates 209.85.217.226 as permitted sender) identity=mailfrom; client-ip=209.85.217.226; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ua0-f226.google.com) identity=helo; client-ip=209.85.217.226; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="postmaster@mail-ua0-f226.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Arqou/REnsTp2xYMvDEnbPp1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78p8+wAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj?= =?us-ascii?q?8KOSMn/m/QicJ+gqJVrQm9qxBj34LYfJuYOOZicq7bYNgURXBBXsFUVyFZDYOz?= =?us-ascii?q?cYwPD+QPPetDs4b9vEECrR6/BQa2AePvyyVEiWHr0q0n1ekqDA/I3AslH90UsX?= =?us-ascii?q?TUqs34NLsKUeCp1KnE1zLDb+lZ2Tr79YPGcQghrOmSUb5sdcfd00oiGgPfglmO?= =?us-ascii?q?tIDoPSmZ2voTv2Wa9+ZsSOaih3A9pwx/vzSj3MQhh43Tio4I1FzJ8zhyzpwvKt?= =?us-ascii?q?2iUkF7ZMapEJtOuCGeMIt7WsYiTHtpuCY+07EGpIS0cDQTxJQp2RLTdf2Kf5KH?= =?us-ascii?q?4hLkU+aRLjN4i2x/dL2jgBay9FCsyuz6VsaqzFZHtjRJnsXIu3wX1BHe6tKLRu?= =?us-ascii?q?Vg8kqjwzqDyR7f5+BcLUAxj6XbKpohwrAqlpoUtETOBiD2l1vxjK+YeEUp4fSn?= =?us-ascii?q?6//9brXjp5+TLYp0igDkPqswh8O/HPw0MhISUGiD5eS8yLrj8FXlT7pQi/02lr?= =?us-ascii?q?DVsJTbJcQAuq60GBRV04Ym6xanFTiqytUYnX8dLFJEYh2LlYbpO0udaMz/WKO0?= =?us-ascii?q?ilGo1TNq3OzuP7v7A5yLIGKVw5n7erMo5ENbxgQbxssZ4pNdD7BHLf7uCRy5j8?= =?us-ascii?q?DREhJsa1/8+O3gEtgojtpPC1LKObeQNebpiXHN4+suJ+eWY4pM5GT2ML4g5vfr?= =?us-ascii?q?jDk0lUJPJPD1j6tSU2ixG7FdG2vceWDl24tTGnxMuws3Se2shVGfA2YKOiSCGp?= =?us-ascii?q?kk7zR+M7qISIfOQof33u6E1Sa/W4BfPiVIUArSV3jvcIqAVrEHbyfAesI=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DVBAC83QVbh+LZVdFdHgEGDCmDfYElj?= =?us-ascii?q?FqMBYMIlFkDUwEKH4Z2GQcBBDQUAQIBAQEBAQEBAQETAQEBCgsJCCgjDII1IoM?= =?us-ascii?q?YAQEmEjs0HQgBBQEiHAsHgwcCgX+fcDyKGIMJgm8BAQWBY4MEBx1EgXQICQEIi?= =?us-ascii?q?CSCE4EPgl+FbYJkgiSHRZEXCYhAhg6BRINvgi6FK5BwDyGBBDOBc3KDEQmCCxq?= =?us-ascii?q?DToUUhVpTAY1/AQE?= X-IPAS-Result: =?us-ascii?q?A0DVBAC83QVbh+LZVdFdHgEGDCmDfYEljFqMBYMIlFkDUwE?= =?us-ascii?q?KH4Z2GQcBBDQUAQIBAQEBAQEBAQETAQEBCgsJCCgjDII1IoMYAQEmEjs0HQgBB?= =?us-ascii?q?QEiHAsHgwcCgX+fcDyKGIMJgm8BAQWBY4MEBx1EgXQICQEIiCSCE4EPgl+FbYJ?= =?us-ascii?q?kgiSHRZEXCYhAhg6BRINvgi6FK5BwDyGBBDOBc3KDEQmCCxqDToUUhVpTAY1/A?= =?us-ascii?q?QE?= X-IronPort-AV: E=Sophos;i="5.49,434,1520895600"; d="scan'208";a="266199009" Received: from mail-ua0-f226.google.com ([209.85.217.226]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 23 May 2018 23:35:51 +0200 Received: by mail-ua0-f226.google.com with SMTP id i3-v6so15780765uad.4 for ; Wed, 23 May 2018 14:35:51 -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=xbKJwHygJbPEGee/WKWwArs9SJBqtSLdab9i9V5tOsCSaht0iWRtkBtjV4WB6oVJi0 GyQ/Qc2qmTxhpMAJrrVqhlQToMx64uWPR8cmDWNBXOK6rq0ZNzZoVHr7oVYcKbw/VqnK n809AnDKVGIfArpI6P3lJ2iQrSIrZYTaQkae7tCmfvevlln1x7TfV31Z8Kgi4+x0JKxK 9f+wUdl0Ed8O7mEfCeMvWRel4bpaK8fkUDooM16qgHpUzYjpTthxU98XT/pLcqMtmtsI u3YrX7/gPJjgmmR++IwNpI8Xsru318VDlFoA8A5lMyJ1tfLR/RUzW7oS5xyDisO+Gho0 rlvw== 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=I/KXB7pRkaS2/wtytvErkKm9oxm4jzH2GhnlOtSBhC0rJ6jzP9tdQ0RIlwsVrN38jA goAmRZsTe62bIfhh7wZZMUYBe02xdil1FeB41ov8zKO9oE9Fs5LSoFtgJpePwPeCZRKv UYyDg/p+FyfE1EFyna+E7LfznZJJFa6FOCXfHekDT4Hsr3YRBiwVhGoLByhXMS/7+uRZ 24QyPF0PovJoc6OFirmcSg67bWwmQuThvPO1iDFRwbyAph6ZB3yAtNCrDQ+YjFGaVayp UM36E3hdVeGCP5vGlrogG2aZec6CYrWQrFbbBKQO9rLgsa1ANS+wB1XwHBvdo55FUrtT E0PA== X-Gm-Message-State: ALKqPwc6/Ar+NDAmVg3xNcbzzzy49AQ5IeFK3S8kezT+P8nA8S204Jl+ ZdaThXmiZ4yMk4Vu5FNVloHHfn+Q4NZ67yb3c8whmaMn/yNhbg== X-Google-Smtp-Source: AB8JxZp1dmoPIsq1mGhe3iBKeGxbFikYxQoHufldDVOr7/HvoeCuf93YpGajHU5avbuwip+/7wMBZ2DuE+Cs X-Received: by 2002:ab0:17d2:: with SMTP id p18-v6mr3163511uaf.95.1527111350617; Wed, 23 May 2018 14:35:50 -0700 (PDT) Received: from cs.miami.edu (ewell.cs.miami.edu. [192.31.89.12]) by smtp-relay.gmail.com with ESMTP id k199-v6sm845891vka.12.2018.05.23.14.35.48 for ; Wed, 23 May 2018 14:35:50 -0700 (PDT) X-Relaying-Domain: cs.miami.edu Received: by cs.miami.edu (Postfix, from userid 3640) id 34A7F1700E7F; Wed, 23 May 2018 10:29:07 -0400 (EDT) To: X-Mailer: mail (GNU Mailutils 2.99.98) Message-Id: <20180523142907.34A7F1700E7F@cs.miami.edu> Date: Wed, 23 May 2018 10:29:07 -0400 (EDT) From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CASC-J9 - the ATP System Competition ------------------------------------------------------------------------------- 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! -------------------------------------------------------------------------------