coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] TPTP v8.2.0 released

From: geoff AT tptp.org
To: <coq-club AT inria.fr>
Subject: [Coq-Club] TPTP v8.2.0 released
Date: Mon, 3 Jul 2023 02:22:19 -0400 (EDT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=geoff AT tptp.org; spf=None smtp.mailfrom=geoff AT tptp.org; spf=None smtp.helo=postmaster AT armistead.ccs.miami.edu
Ironport-data: A9a23:snsIU6ndZJ4V46CfiHQpb+Po5gw1I0RdPkR7XQ2eYbSJt1+Wr1Gzt xJKXmvTb/qPY2b9ed53OduxoRgDuJWDzYNhSAI9rCBgRltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yt4GlA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1fFXofAs4g3NpqBHt89 tMaDTwNNBSc0rfeLLKTEoGAh+wqNszqJ58Ss30mxjrCS/MnSJXCBajG+Le03h9p15oIRq+YN 5tfN1KDbzyYC/FLElgaD5wwtPuwmmG5dCdXwL6QjfRvuDeIllUouFTrGOqJJdGEH55lpx2/v zPd+VX4MzA1KvXKnFJp9Vrw37WRwX2TtJgpPLa/77thhECZ7ncCDQUfE1q9u/iwzECkM++zM GQd4C8vtrQ//UDtRcK7WhyxpX/CsxIBMzZNLwEkwDCU8YProD6/OnUBVAxCR94DuM9sQSN/g zdlgOjV6SxTXKy9ECzNpuzN/G/qaUD5PkdYOHBfEVptD83L5dFr1EiVHr6PBYbv1rXI9SfML ydmRcTUr5AShMsKv0lQ1Quc2mn3znQloxRc2+k2Yo5GxlklDGJdT9b0gWU3FN4ZRGtZJ3HY1 JT+p+CQ7foVEbaGnzGXTeMGEdmBvqjVYGaG2wA/RsN8plxBHkJPm6gLuVmSw28yYq45lcPBO Sc/RCsOuccLbBNGk4coOupd9PjGPYC8TI67Cq68gitmf55wagKd5yBydAaX0SjokUEpkMkC1 WSzLa6R4LdzIfoP8QdasM9Gj+R7mHxhnTm7qFKS503P7IdyrUW9Ed8tWGZipMhghE9diFWKq 4RsJIGRxg9BUebzRCDS/MRBZRoJNHU3T9S+4cBeaufJcEIsFXADGs3h5+orW7VkuKBJycbO3 HW2AXFDxHTF2HboFASta1JYUo3JY6pRl3wAEBIJAUeJwFkmOIam07cefcA4fJ4h7+1S8sR3R PgkJeSFLOVFdTDV9xsjbavW8Y5TLzG2jz2KPyCaYyUNQKQ5Zg3W++3Lehnk2zkOAxGW6+o/g eyE/SHKTaUTQz9NCJ7tV8uu6FeqrF4fsu5WdGnZEOl5IUnD3tBjFH3ss6URPcoJFyTm+hKb8 ASnWTEjuujHpt4Owunj3Kyrgd+gLLpjIxB8AWLe0LeRMBva9EqFxatrcr6BXRLZZVPO1JSSX 8dn5NCiD6Rfh3dPiZR2LJhzx6Fn59fPma5T/j45IFr1NWaUGpFSCVjY+/kXraBc5K5riS3vU GK1x9RqE7GoOsTkLV0vGDQYftmzjfE5pz2Dwsk2cWPb5TB29oWpSU99HQeBow0DIapXMLEK+ /YAuskX5yyV0hEBb8iNiytV00+uLXUwdbotmb9HIY3siystkkpjZ76FAADIwZi/Ufd+GWh0H S213o/s3699wGjGeFoNTUn95/JX38kyiUob3W08KESssfuboP0OhTl60yk9FyZRxTV5i9NDA HBhbRBJFP/f7gVTpZZxWk63EFt8HzyfwEv6zmUJmED/T0WFUm/sLnU3Cd2S/XI2on5tQTxGw I62kGrVcy7mXMXU7BsAXURIr//CT9so+DbSx+GhPcCORKchbRTf36SBWGsvqjncO/0XunHpn +dQwbtPWfXJDhJI+6wfIKuG5IsUUyGBdTBjQ+k+3aYnHlP8WTCV2BrWIGCLZedIdu344G6jK slUPskUfQ+P5CWPiTE6BKA3PL5/msAy1ucCYr/GIW0nsaOVizhYr6Lr6Sn1gVE0T+VUkcoSL p3bcxSAGDeygUR4tnDsrs4eHEaFevgBORPB2d6q/NUzF54stP9mdWcw2OCWu1SXKA5WwAKGj jjcZqP5z/1Q9qo0ptHCSp58PgSTLc//cM+q8wrp6tRHUo7pAPf07ggQrgHqAhRSMb4vQO9Ir LWqsuCm7HOd6fxyGyrcloKaHqZE2dSqUaAFeojrJX1dhm2ZVNWq/xIH/HuiJIdUlM9GoPOqX Ba8dND6YOt9tw2xH5GJQ3M2/9ch56XLgmPIrDm4ru+QBxERlwfMN5Wi9HbsbCdWejJg11gSz OPrk67G2zyahN0k6Nw46zVOH4dkOBnkQ6ROmxgdc9WHJjHAv75B04cOUTI88S3TTH6eH64WJ H4DqgfWLHyPhU0D8D2VX0GecPHa4LaRTNTcpn4gxuM=
Ironport-hdrordr: A9a23:xf2R462s4J5wafX423JzJAqjBNgkLtp133Aq2lEZdPU7SKKlfq yV/cjzqyWatN95YhhJ8uxoU5PrfZqzz/NICPEqUYufYA==
Ironport-phdr: A9a23:oPtRlh08UixWD9YxsmDOGAAyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaBo6w0xwaRBs2bs6sC17CL9fi4GCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sL Ri6txjdutQZjYd/Nqo8xAbCrn9Ud+hL329lKkyfkhbm6sus4JJv9jlbtu48+cJHTaj1cKM0Q KBCAj87KW41/srrtRfCTQuL+HQRV3gdnwRLDQbY8hz0R4/9vSTmuOVz3imaJtD2QqsvWTu+9 adrSQTnhzkBOjUk7WzYkM1wjKZcoBK8uxxyxpPfbY+JOPZieK7WYNUXTndDUMlMTSxMGp6yY ZUIAeQCM+hWr5Lwq0cSoReiGQWhHv/jxiNOi3Tr3aM6yeMhEQTe0QwvAd0Ot3rUrNvuOacOS eC10LHIwS/Eb/NM1jfw7pXDfR89r/+WR71wbdbRxlc1FwPDllidqYzoMjeI2+kPr2SW7fdtW OGshmMoqgx8oSajy8QshITXiIwYy03J+DllzIg6JtC2RkB1bNG5HJZRqyyXNoR7T8U/SG9mv yY6z6cJuZ+9fCUS1JQn3wLfa+Sdf4iP+BLjW+CcKip7inJ9YL+zmhK//Va6xuDyS8W4ylVHo y5fntTNsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU07j7DbK5sgwr4ripocr17METLslErqk KCWbV8o+u2p6+v9Z7Xmp4WQOJFphQHjKqgum8q/DvokMgUWQmSW/fqw2Kft8EHkWrlHjfk7n rPYvZzCIMQUvK+5Awtb0oY57Ba/Ci+r0NsGknkAIlJFdgmKj5TxO1HSOPD0F/C/g06jkDtzw fDJJaXuAo/RIXjbjLfhYbF95lZBxAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y2 5gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiiptklgEOKKtwJE/aXaiH/0gLV/PM lT2hdJUHmoNsAQWUPT2kBuFSzEAND6JQ6sg62RjW8qdBoDZS9X16FTg9CKyH5kNI3tDFkjJC nDwMYONR/YLbiuWZM5niD0NE7a7GMc6zR/7kgj8xvJ8K/bMvDUCvMfs2d976cXPjQ0qsztuA JfVyHmDGkdzmG5AXDoqxOZ6qE15xE2E1P13jvtWG/RP/+9RFAAgOs2U1PR0Xvb1XA+JZdKVU BCmT9GhVCk2Vc40ysQSblxVEs+njwvf0iOmRbQejPqOBZUx8+TR02WZy99V7XHA2eFhilAnR pAKLmi6nutk8BCVAYfVkkKfnqLsdKIG3SeL+n3RhWyJ9FpVVgJ9S8CnFTgWe1fWoNLl50jDU 67mCLIpNRFEwNKDLa0CY8PgjFFPTvPucNrEZGf5l2C1DBeOjrSCCeiiM2oQ2yvTIFQcjxhV+ myJdEA/Ciqnv2PCHWl2D1u8K0jo8OR4tDa6VhptnlvMNBQnh+vzpE1w57TUUf4Y07MatT10r jx1GA34xNfKE5+boBIneqxAYNQ76VMB1GTDtgU7MIbzSsIqzlMYbQlzuFvjkhttDYAV28cnq 30k5BZqNbre10lOPWDQzdXrN7vbJ3Onth+ibKDY8k3GzM7Q/b0AoqddyR2rrESiEUws9G9i2 t9e3i6H55nEOwEVVIr4Tkc98xUSS6jyRC476suU0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL8YOot00OkaB4JJoUwvOY9It+mev2a2aWqIPconTSoin5C6Zx81UTE/jR1S+rB1 ZIIi/+C2Q7PWzD5hVan+sf5/OIMLT4fGWSx4TT8GJYXYbd9PM4KBWqoP8yr14B7jp/pVWRf8 Q3rDFcH1cm1PBuKOgWsh0sLjAJH8Dr5yk7ah3Runjokr7SSxnnLyuXmL18cP3JTAXJllRHqK JS1iNYTWA6paRIonV2r/xWfpeATqaJhIm3UWUoNcTLxKjQoXaa3uLSqf9ZT8NUvqyodA6ysJ EuXTLLwuU5Q3C7kEWV22Cgnb3etoJqzzHkYwCqNaX10qnTeY8R5wxzSscfdSfBm1T0DXCBki DPTCzBQJvGP+tOZ39fGu+G6DCe6U4FLNDLs1cWGvTe64mtjBVu+meqyk5vpC1py1yizzNRsW SjSyXS0KoD2y6S3N/5mdUh0FRf97cR9AIR3joo3gtkZx3Ebgpyf+XdPn330NJ1X3qf3bXxFQ jBuoZad+A/+xEhqNW6E3arwTHCc2ddsbtX8aWgNnCc85sVLTqqY8f0MnCd4pEa5sROEYfV5m WR4q7Nm43objucV/Qs1m3zMWPZJRA8IbGqyxHHqp5ikoa5aZXiia+213Ut6xpW6Ca2a5xpbQ DD/c4sjGil56oN+NkjN2Tv98NKBGpGYYNQNuxmTixqFgfJSLcd7mfcNiyRPJXrhpTsi0eFx3 nkMldmq+ZOKLWlg5vfzGhlDKjj8fN8e4Bnkl6Nfhdqb1ozpFZ56XDAKVZ7pC/+kDXhB0Javf xbLGzo6pHCBHLPZFgLK80ZqoUXEFJWzPm2WLn0UpT2HbAWFOFQZhxobDm1SdnERChi23Irma kgrvlj5B3bxsB5N0f5lPhW5WWzE4gKpYzI1DpWTMUgOhjw=
Ironport-sdr: 64a2692b_8GkwfPiyTmNbw8m/DeYCckK9+3k6tXaWWsD0/Nr2dftAu+r hcrnAeVh1L4QhHlNySuH15iSywNDReBgwALiiaQ==

================================================================================

The TPTP Problem Library, Release v8.2.0
----------------------------------------

Geoff Sutcliffe
geoff AT tptp.org

The TPTP (Thousands of Problems for Theorem Provers) Problem Library is
a
library of test problems for automated theorem proving (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
the
capabilities of the ATP system being considered.

TPTP v8.2.0 is now available at:
http://www.tptp.org
The TPTP-v8.2.0.tgz file contains the library, including utilities and
basic
documentation. Full documentation is online at:
http://www.tptp.org/TPTP/TR/TPTPTR.shtml

========================== What's New in TPTP v8.2.0
==========================
Changes from v8.1.2 to v8.2.0 for THF problems
2823 ratings changed

Changes from v8.1.2 to v8.2.0 for TFF problems
9 new abstract problems
218 new problems
1013 ratings changed

Changes from v8.1.2 to v8.2.0 for FOF problems
4370 ratings changed

Changes from v8.1.2 to v8.2.0 for CNF problems
4158 ratings changed

+ In SyntaxBNF:
- Separated <ntf_connective> into <nhf_connective> and <nxf_connective>.
- <nhf_key_pair> defined as <thf_definition>, and similarly <nxf_key_pair>
defined as <txf_definition>.
- Removed nhf_connective and <nxf_connective>, added <ntf_short_connective>
as a unary connective.
================================================================================

[Coq-Club] TPTP v8.2.0 released, geoff, 07/03/2023