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 27A1B5D5 for ; Tue, 27 Aug 2019 15:21:50 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,437,1559512800"; d="scan'208";a="399070792" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 27 Aug 2019 17:21:48 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 81EA87EF26; Tue, 27 Aug 2019 17:21:48 +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 B63A27EC74 for ; Tue, 27 Aug 2019 17:19:33 +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-pg1-f225.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AvtXNMh/57SWbyP9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?0u8cTK2v8tzYMVDF4r011RmVBN+dsq8UwLGL+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZLebxhWiDanfL9/LBa7oQrfu8QWnIBvNrs/xhzVr3VSZu?= =?us-ascii?q?9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnY?= =?us-ascii?q?UQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gy?= =?us-ascii?q?kFKjE56nnahNFugqxcoxyvqRxxzpXIbI2JKPZyYrnQcc8GSWdHQ81fVzZBAoS5?= =?us-ascii?q?b4YXAOoOI+FYr4fzp1YVsRS+HhOgBObuyjBSg3/23Lc23Po8HgHb2gErAtwAsH?= =?us-ascii?q?PRrNrvNacSV/i4zLXQzTXfd/NawzD96JLHch0nvPqCXqpwfNLPxUUzEw7JlFad?= =?us-ascii?q?pIz/Mz+Ly+gAs3KX4/R+We+vk2IrtgV8ria1ysoil4XFnIEYx1Te+Slk3oo4I8?= =?us-ascii?q?CzRlRhbt6+CpRQsjmXN4toTcMmRGFloCM6xacHuZ6/ZSQK0JsnywPGZ/yJbYSE?= =?us-ascii?q?/BLuWPyeITd/g3Jld7a/iAio/Ue8ze38U9G40FdMriVbjtnBrm4B2wDX58SdSf?= =?us-ascii?q?Zw/l2t1SiS2w3T8O1IP144mKrDJ54k2LEwl54TsUrZHi/xnUX7lKCWeVsj+uim?= =?us-ascii?q?5eTqeanppoSGO49xiwHxKKEums2lDesmLwcOQnCX+f6g27374U35XLJKg+Uqna?= =?us-ascii?q?bDtZDaId0Xpqq4Aw9OzoYu8A2/Djej0NQAh3YLNlNFeBSdj4joIV7COv74De3s?= =?us-ascii?q?y2irxWNgzvXCe7ngGYnlL37Zkb6nc6wruGBGzw9mwt1Y6Zx8AapHJfP6X063ud?= =?us-ascii?q?DFXUxxCBC93+uyUIY17YgZQ2/aWvbFYpOXikeB46cUG8fJfJUc4WqvIONj4v/n?= =?us-ascii?q?iH5/lFMAL/HwjMknLUugF/EjGH23JH/lg9MPC2AP51ZsR/esjVyLVD8VanqvDf?= =?us-ascii?q?tlu2MLTbm+BIKGfbiDxbyM2CDhQM9Tb2FCT0iDSDLmLd/ZHfgLby2WL4lqlTlW?= =?us-ascii?q?DbU=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AdAwCcSWVdhuHXVdFlhR5TXI0dhg6bO?= =?us-ascii?q?oEQA1QBCAEDAQwjDAEBhwcbBwEENBMCCgEBBAEBAQIBAwMEARMBAQEICwsIKYU?= =?us-ascii?q?1DII6IoMHLgEBODs0HQgBBQEiEwkLDoMAAYIKD54UgQM8ijGCJYJ7AQEFgkiDF?= =?us-ascii?q?ggigSoJCQEIgSKHHIIUgkUYgX+BEYdhARIBg1yCJoxFL55/CY4OhA2EQSeCMi+?= =?us-ascii?q?HAYNjixGmLg8hgUaBCHFyToJsCYJTg1iFFIVbIzMBjQOCQwEB?= X-IPAS-Result: =?us-ascii?q?A0AdAwCcSWVdhuHXVdFlhR5TXI0dhg6bOoEQA1QBCAEDAQw?= =?us-ascii?q?jDAEBhwcbBwEENBMCCgEBBAEBAQIBAwMEARMBAQEICwsIKYU1DII6IoMHLgEBO?= =?us-ascii?q?Ds0HQgBBQEiEwkLDoMAAYIKD54UgQM8ijGCJYJ7AQEFgkiDFggigSoJCQEIgSK?= =?us-ascii?q?HHIIUgkUYgX+BEYdhARIBg1yCJoxFL55/CY4OhA2EQSeCMi+HAYNjixGmLg8hg?= =?us-ascii?q?UaBCHFyToJsCYJTg1iFFIVbIzMBjQOCQwEB?= X-IronPort-AV: E=Sophos;i="5.64,437,1559512800"; d="scan'208";a="399070288" X-MGA-submission: =?us-ascii?q?MDGVhmP2YdduhAr5zdoVQcWMvyqk9qyKplDwrK?= =?us-ascii?q?U/n/TbRUdILQaD8KqpN7x7zKCn+Iu3mQuF9Svj4FKqyUnu2rXRYNQpck?= =?us-ascii?q?3n4JlyWe0lXVpuU3W4Mb9hOHNLXBKrEsQCgnZqGXznzjJXpIxLa55Ug1?= =?us-ascii?q?1qoPwisOEIRcdQIkUlySnebg=3D=3D?= Received: from mail-pg1-f225.google.com ([209.85.215.225]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 27 Aug 2019 17:19:13 +0200 Received: by mail-pg1-f225.google.com with SMTP id x15so12883095pgg.8 for ; Tue, 27 Aug 2019 08:19:13 -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=WYcGYJ7nrFJz2ofV1quv8A6q7erVgOB3OTGPOvS5s6Q=; b=mxSgWTWTvPS8FOI0k/iizto2iXaoy5yWrln3feHou85yHF3j59PCks59RE8B0rkyny 8Ro84T5yGXh2RG0x9blVLUfbCQ92+/uc1fPjIL7o8JoPy3jFCOyGG5OCdi2VkAqGYsMC j6Iq4aJxAUinbhzIJF1OgAqVMl7PE1r8PRdJ9P1YJXG3BpgER/JRN4jeRfhnXdqBGtlu pJfO7CnyYYAwPkUVefHA4CVZwo2vmaZBlsVN4EgoBo0idxSlz9hlbRNEG6QdjndRfM4f xR6SXcBq0p1NZEAn61xa1YbmRFORuWuJyggG0of+JSpedPNKulGAMMJ3UhhFye6glSF5 fgSQ== 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=WYcGYJ7nrFJz2ofV1quv8A6q7erVgOB3OTGPOvS5s6Q=; b=eanRTH5Iuy6wUJRxqUjXntkZ6ICV8BBISjiRhBo+BD+D8YCfiLx4u7K07fuqRfPBap DC9fNHbwLNW7UTNzSwvsl1BFQGwPy8BEvOWINHNlxUjuuViZRvNaP3LQbAE9wXkxslXd v5xewZImJZ5afoVqc4DMuA8dWeIsPFaz6/G6Ymtayr/ebr8W5sELUhgY1oTch/pViCfI vSuSzdnC3NjmH+k0PMEOWGZp0BP1aXp01rlyd3VRv0aWGcbTmRofcl0rTO1BI0iFSBN+ E9YOmbC6qD3b+WeY0uc1Uup+/icVAB9NP3CojLoM2VJlOUt3532wmz33i1Q1WB+ffGAW ePjQ== X-Gm-Message-State: APjAAAWDvuRwdVO4xSjsZaaoBEBA2AZ6y6wfYxqdapFsYzIVo1yazCsk BfNqvQlXK3DyBPtsuyGnCno0zGSegotMw65fOZDrWOKm8ec0xg== X-Google-Smtp-Source: APXvYqyqqa+tLqAgD3j2fKnOAiBAnwtDC6sFz9+97VXUURtoPwd19z9gLV3yaq4o9Km3U4j7/kfHZ6jcYpIY X-Received: by 2002:a62:cec4:: with SMTP id y187mr26405304pfg.84.1566919152230; Tue, 27 Aug 2019 08:19:12 -0700 (PDT) Received: from cs.miami.edu (ewell.cs.miami.edu. [192.31.89.12]) by smtp-relay.gmail.com with ESMTP id l7sm323921pjn.5.2019.08.27.08.19.11 for ; Tue, 27 Aug 2019 08:19:12 -0700 (PDT) X-Relaying-Domain: cs.miami.edu Received: by cs.miami.edu (Postfix, from userid 3640) id 6C5A017009B3; Tue, 27 Aug 2019 11:18:53 -0400 (EDT) To: X-Mailer: mail (GNU Mailutils 2.99.99) Message-Id: <20190827151853.6C5A017009B3@cs.miami.edu> Date: Tue, 27 Aug 2019 11:18:53 -0400 (EDT) From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] TPTP v7.3.0 released Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 17782 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: ================================================================================ The TPTP Problem Library, Release v7.3.0 ---------------------------------------- Geoff Sutcliffe Dep't of Computer Science, University of Miami, USA geoff@cs.miami.edu *** NOTICE: The CADE-27 ATP System Competition (CASC-27) will run on Wednesday. *** See the action online at ... *** http://www.tptp.org/CASC/27/ The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with: + A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism. + A comprehensive list of references and other interesting information for each problem. + Arbitary size instances of generic problems (e.g., the N-queens problem). + A utility to convert the problems to existing ATP systems' formats. + General guidelines outlining the requirements for ATP system evaluation. + Standards for input and output for ATP systems. The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library. This is the first release with polymorphic THF (TH1) problems. There are 644 polymorphic TH1 problems in 14 domains. TPTP v7.3.0 is now available at: http://www.tptp.org The TPTP-v7.3.0.tgz file contains the library, including utilities and basic documentation. Full documentation is online at: http://www.tptp.org/TPTP/TR/TPTPTR.shtml The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please email Geoff Sutcliffe. ========================== What's New in TPTP v7.3.0 ========================== Release v7.3.0, Fri Aug 2 16:17:10 EDT 2019 Changes from v7.2.0 to v7.3.0 for THF problems 8 bugfixes done, in the domains LCL. Changes from v7.2.0 to v7.3.0 for TFA problems 6 new abstract problems, in the domains PLA. 7 new problems, in the domains PLA. Changes from v7.2.0 to v7.3.0 for FOF problems 286 new abstract problems, in the domains CSR NUN SEV SWW. 458 new problems, in the domains CSR NUM NUN SEV SWW. 247 bugfixes done, in the domains CSR NUN SET. Changes from v7.2.0 to v7.3.0 for CNF problems 45 new abstract problems, in the domains SYO. 196 new problems, in the domains AGT ALG ANA BOO CAT COL CSR GRP HEN KLE LAT LCL MSC NLP NUM PLA PUZ REL RNG ROB SEU SWB SWV SYN SYO. 16 bugfixes done, in the domains SET. + In SyntaxBNF - Added semantic rules for . - Split into and , and added () to . ================================================================================