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 A02185D4 for ; Mon, 27 Apr 2020 20:07:55 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.73,325,1583190000"; d="scan'208";a="447148664" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Apr 2020 22:07:54 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id A0DCC7F485; Mon, 27 Apr 2020 22:07:54 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id BC0507ED20 for ; Mon, 27 Apr 2020 22:01:03 +0200 (CEST) Authentication-Results: mail2-smtp-roc.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-ot1-f100.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A2uUhIhMP8KCUP/hQ1L4l6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0Lf3+rarrMEGX3/hxlliBBdydt6sZzbeH+Pm7CSQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagYb5+NhW7oAHeusULj4ZvKbs6xwfUrHdPZ+?= =?us-ascii?q?lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRne?= =?us-ascii?q?VgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gy?= =?us-ascii?q?oBKjU38nzYitZogaxGvhyvoB9xzYDUboyOKPZyYr/Rcc8ASGZdQspcUTFKDIOm?= =?us-ascii?q?b4sICuoMJelYoJf6p1sAoxuzHhWjBPj1xj9Nh3/5x6g60+U7HQ7YwQMgAtQDu2?= =?us-ascii?q?naotXyMacdS+G1zK/QwDXfd/NWxS/95JLPchA7rvGBW697f8nJyUQ3CQ/JklGd?= =?us-ascii?q?pZbmMj6VzOgBrXWX4/Z6We6yl2Irtxl9riWry8sykIXEiJ8ZxkrH+Ch92oo5OM?= =?us-ascii?q?O0RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UDuZGhfSgKzI0rxxnDa/CaaoSI?= =?us-ascii?q?7A/vWPqNLTtii3Jlf7W/hxm28Ue+0OHzSs600FNSoipElNnDqGwN2gTN5sSbTv?= =?us-ascii?q?Zx5ESs1DaV2wzN9+1IPVo4mbfHJ5I92rIwk4AcsUXHHi/4gkX2i6qWe10r+ue2?= =?us-ascii?q?7OTnbLvmq4SAOI9vkA3+N6Uulda6AeQ5KAQBQXWU+fmk2L354UL5WKlKjuExkq?= =?us-ascii?q?TBrJ/VP8EbpqqgDw9R04Yj8Aq/Aiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2x?= =?us-ascii?q?g1S2w39XwKWSNbTkBtDJL2PfuLbnZ7d0rUBGnlkd19dasp1ZDb8PCPnoHErwvd?= =?us-ascii?q?nZSBI1Ll/ni937Aclwg9tNEVmEBbWUZfuL7A24o9k3KuzJX7c7/TbwL/9/uazr?= =?us-ascii?q?hH493FgBJOynhMNPLn+/GftiLgOSZn++2o5QQ1dPhRI3SanRsHPHVDdSY3ioWK?= =?us-ascii?q?dlumMwE8SjDI7GR8agjKHThX7nTK0TXXhPDxW3KVmtb5+NAqteYznUJ85olz1C?= =?us-ascii?q?WLS8Gdcs?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0COAgDWOKdehmTSVdFmHgFDDINYgRlVX?= =?us-ascii?q?I0goxsDVAIJAQMBDB8QBAEBhm4cBwEENBMCEAEBBQEBAQIBAgMEARMBAQEICws?= =?us-ascii?q?IKYVdDII7IoMtLgEBJhKBDAgBBQEiHAsHB4I5SwGCfKZ4gQQ9jFqDAAEBBYEyA?= =?us-ascii?q?YEWgzsJJIEgCQkBCIEmh1eCHoJIGoIAgRE2giyGB4J3gi2OJRKjb4YniiuJcSm?= =?us-ascii?q?CW4hXhD6NC4RpqDAPI4FGgXhygzcJRxgNkU6DWIUUhV4lMwIzAgYIAQEDCY8cA?= =?us-ascii?q?QE?= X-IPAS-Result: =?us-ascii?q?A0COAgDWOKdehmTSVdFmHgFDDINYgRlVXI0goxsDVAIJAQM?= =?us-ascii?q?BDB8QBAEBhm4cBwEENBMCEAEBBQEBAQIBAgMEARMBAQEICwsIKYVdDII7IoMtL?= =?us-ascii?q?gEBJhKBDAgBBQEiHAsHB4I5SwGCfKZ4gQQ9jFqDAAEBBYEyAYEWgzsJJIEgCQk?= =?us-ascii?q?BCIEmh1eCHoJIGoIAgRE2giyGB4J3gi2OJRKjb4YniiuJcSmCW4hXhD6NC4Rpq?= =?us-ascii?q?DAPI4FGgXhygzcJRxgNkU6DWIUUhV4lMwIzAgYIAQEDCY8cAQE?= X-IronPort-AV: E=Sophos;i="5.73,325,1583190000"; d="scan'208";a="447147846" X-MGA-submission: =?us-ascii?q?MDGCgvBrqm87tcuyupn4l7cPLDZSIbNxtBrv3I?= =?us-ascii?q?RRBT7zIbpeMJYgfdc/YL+eKt5oII3XKCD20ZFlbmOdsbwFXsNddqdjye?= =?us-ascii?q?lBS8WZhkrkjeN0nluN2QjXSayyX6PKdKItff+oUmPZZut94ynC9V54KD?= =?us-ascii?q?Wk46zT1sqgngWt+7wYAzmiUw=3D=3D?= Received: from mail-ot1-f100.google.com ([209.85.210.100]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 27 Apr 2020 22:01:02 +0200 Received: by mail-ot1-f100.google.com with SMTP id c3so28473437otp.8 for ; Mon, 27 Apr 2020 13:01:02 -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=XOMa3TB0eJqBVeoKfh9kkD+swmY+OKkmnCElwz+CQ2I=; b=pCEsbsTkEmkLdkLE/7hfmmoB4+L/kETreE5itKn+3pEsBrsaCSPOj7SY0hss4iUCQf uz2SrQehnicQUpDH8AoTqNAD+B2tOUVXW3V/gGQmx4sdtDxSZGueH/+PmZ9Y0G0n3CEz hCbYSsmfNCFSlZoxQEODgime0iZAw1G0Ehwrd6a9llokhzxd3yw2aRo8sgYiTt+1xl8u PoX1qgz4aWuH+OAqagVYh3k8lCaHpJ6w1PtMSokWrHkh6vvaQjiDsm7wcnupLrhCi+eP Pi6cM6A/sDTWdRRM/jiO11f0lXfAE8gcxbLWnvDQRNMc7QXfx8uZT7YNVarlYOwniTul HPOA== 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=XOMa3TB0eJqBVeoKfh9kkD+swmY+OKkmnCElwz+CQ2I=; b=sZQxCbohicnt13lN4ZV3r9w5gjHjLMcArmwD/DXwyUcaSUwW8O1dvBqk6mZOhHbXrV PRXTcMNbC9pZotHH9fjRHKCiqDusKBZhX+P55XwZHEvk7nY10vMZVi+5ucNJkwwbHuf+ ejIDc+0JDmdLcAG0o24km+V2tejgpSBDwiaXFYZ/CONRkShhsAaFzEMxALkYj6tLVMdQ bGZMN76UhvUDMXDoBFni2FG8E+3dWKZebkVWeoEnf6IJn0NYbbAqqm5oKbyz0HECVKMF mpPtPdXA50DEekJCpL0BrH6MZKHdYYQNmCdTmK0fEaHxe7Aqa88B4kcEeNAynWNqs2u+ m++w== X-Gm-Message-State: AGi0PuZ+t5+Qw/HciGxec2rreyLcj0TluxNyCpA9sflXHKb8aQpMneRB WFGuyznlXUxHonTcuhJrMCbSEK9QJTlsW2KIWIz1SXfmepMkdA== X-Google-Smtp-Source: APiQypLBozMmbwCQh/MZ1NMGoJRsWtkH4QlLifbsh6r/PvlSdsr7J7A6oojgB0GQogeid9X9nMc0H+GDRjCk X-Received: by 2002:a05:6830:da:: with SMTP id x26mr20293868oto.259.1588017661601; Mon, 27 Apr 2020 13:01:01 -0700 (PDT) Received: from cs.miami.edu (ewell.cs.miami.edu. [192.31.89.12]) by smtp-relay.gmail.com with ESMTP id l22sm2076467oos.5.2020.04.27.13.01.00 for ; Mon, 27 Apr 2020 13:01:01 -0700 (PDT) X-Relaying-Domain: cs.miami.edu Received: by cs.miami.edu (Postfix, from userid 3640) id ED5581700674; Mon, 27 Apr 2020 16:00:36 -0400 (EDT) To: X-Mailer: mail (GNU Mailutils 2.99.99) Message-Id: <20200427200036.ED5581700674@cs.miami.edu> Date: Mon, 27 Apr 2020 16:00:36 -0400 (EDT) From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CASC-J10 - The CADE ATP System Competition Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 18122 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-J10 - The CADE ATP System Competition to be held at The 10th International Joint Conference on Automated Reasoning Online, Earth 29th June -6th July 2020 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-J10 will be held on the 2nd July 2020, during the 10th 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/J10/ Registration of systems for CASC-J10 is now invited. System registration closes on 5th 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! -------------------------------------------------------------------------------