coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The CADE-29 ATP System Competition CASC-29

From: geoff AT tptp.org
To: <coq-club AT inria.fr>
Subject: [Coq-Club] The CADE-29 ATP System Competition CASC-29
Date: Wed, 8 Feb 2023 09:48:33 -0500 (EST)
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:k0581qLoLV4HJnOGFE+Rs5ElxSXFcZb7ZxGr2PjKsXjdYENS1zxVz TEfD2vTa/yMMWD2fNx1aNu39BtQsJWDztQyHVMd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fRLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWCfg76s9JIGjhMsfnb8ks/5K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0Luf3rAxfNKEWYPftck9ddlEGxQp ddbEWVYBvyDr7reLLOTQ/Nph98/IcDneogUoTdlzDjcDLArTY2rr6fivI4CmmxpwJAfW6i2i 8kxMVKDaDzPbhpBNH8LEI4m2uCyiRETdhUE9wjM+fRmvgA/yiQq9bnnFPOJXeaGTMZkvme5o kHK1EDAV0Ry2Nu3lWPfrC7y7gPVpgvwX5tXH7ml/NZxkViLzyoSDgcXXB21u5GEZlWWUshaK lcI9yMi66MpskmqR9z8GRC0vRZooyLwRfJcEsE87iWQ7ZOXuTqWN3oVQyARQ58f4ZpeqSMR6 neFmNbgBDpKubKTSG6A+rr8kQ5eKRT5PkdYOHBfEVttD83L5dFr1EiVHr6PBYbs1rXI9SfML ydmRcTUr5AShMsKv0lQ1Quc2mn3znQloxRc2+k6dmu/6wJieIOsa8qj8h7e7P9FLcCUQkTpU Jk4dyq2t7Fm4XKlznDlrAAx8FeBvKrt3Nr02wQHInXZ327xk0NPhKgJiNy+TW8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzuVpt7kfa9S421CJg4i+aihLAqJWdrGwk1OyatM5zFySDAbIlgZ M/DIa5A815FWcyLMwZat89BiOV1mn5WKZL7WJb60Rm9yruCdTaSR/8AMVKLb4gEAFCs/G3oH hc2H5Xi9iizp8WkM3WPr9FOdAFbRZX5bLivw/Fqmie4ClIOMAkc5zX5m9vNoqQ1wPwHpfSC5 XynRE5TxXz2gHCNe03AaWluZPmrFdxzpG4yd35kd1u5+WkRUaD25ocmdrwzYeYG8s5nxqVKV PUrQZiLLclObTXlwA4jS6fBgrZsTzmRvjLWDRGZOGA+W7VCWz32/sTVe1qz1SsWUQuym8gMg 5yh8QL5GZEjfRtGCZfHWuOO1HK0h2AWw8hpbnvLI/5SWUTiy5drICrPlc0KI9kABBHA5zmC3 SOUMAgonvbMqIoL79X5v6CIgIO3Ge9YHEABPW3kwZupFCvdpEyP/JRhVbuWQDXjS2/EwqWuS uFLxfXaMvdcvlJrsZJ5Iol735AF+NrjiL9L/DtKREyRQQyQNYphBX2a0e1klK5HnOZZsDTrf HO/wIBRPLHRNf71FFIUGhEeUd2C8vMqyx3y9vU+JXvo6BBnpISnVVpgBDjSqSh/AoYsDqYb7 7YPhMok5Ta7qCIWCfedryUN922zPn0KCKomkZcBAb7UsAkgy3AcQJrmFSPWyYyFMPdKE0g1I w27gLjJqKRcy3HjLVsyNynp9shMiasevCtlyAc5GG2Ivd7el9k19hF12hYmfDR/lxlo/bp6B Tl2ChdTO66LwQZNuOFCeGKdQyd6GxyT/x3K+WsjzWH2YRGhaT3QETcbJ+2IwUE+9lBcdBh9+ JWz6j7scRTuTfHL8hoCY2xXgN29coUp7SzHot6tIOqdFZpjYTbFvL6nVVBVlzTZW/EOlG/1j sg02tYocqDqFz8ik4tiAamg6LkgYhSlJmtDfPJfwJ00DVzsIDGc5RXeKmSaWN98GPjRwErpV +1sPp1uUjq95gavrxcaJ64HJuZsl6UT4Os9Q67af0gUl77GtgtW6Yr08xb9iFQKWPRrq942c anKRgKBE0uRpHpaoHDMp896IViFYcEISQn//eKt+sALJo0zi/5tekQMzbeEhXWZHw959Rayv gmYRavp48F96IZrxa3AL75iAliqFNbNS+i4ygC/nNBQZ9fpM82VlQc0qEHiDjtGL4kqRNV7u rScguHZhHqfku4NbFnYvJ2dG41ix8a4BrNXO/2qCkhqp3KJXcu07iYT/2y9F4dyr+pcwcuZF juIMJ76MZZfXtpG33RaZhRPCxtXWey9cq7kojj7tPiWTAQU1QvcNt686Hv1didhezQVP4HlQ BrB0xp0Cgu0cKwXbPPFOx1nP3O8CFb5XKo9a9D4uX+TBXLuh1KLv7qkmBY9gd0O5r9oD+6ii a8phDCnHPhxhE0M5M1Br5Q0uQcYZJq4bS/cYWpFk+ObSFmG4KouMfwBKdMBEJ48fukeEn3nT GmlUVbOwhkRkdiJndsQLTgjssqi6jQyB+rE
Ironport-hdrordr: A9a23:YlFklaOWgL0d6cBcTj6jsMiBIKoaSvp037BN7TEMdfU1SL3kqy jN9M5w6faQslsssR4b9uxoVJPgfZqkz+8N3WBzB8bZYOCFghrLEGg41/qb/9SIIUSXnYJgPM FbE5SWY+eAbmSS4/yV3ODBKadE/PC3tIShheLF0nt3JDsaD51I3kNcAgafCFB7X01tDZ4hHJ qT4aN81l2dUEVSSsy6A2MZU/OGh/CjruOBXfaubyRXkzWzsQ==
Ironport-phdr: A9a23:pHWrXxZBiP2Bc4BrSC8eqhD/LTHi1IqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPBNiCoKoZw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtIiTanfL9/L Ai6oQrNusQWnIBvNrs/xhzVr3RHfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQ LJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4 btnRAPuhSwaMTMy7WPZhdFqjK9DvRyvuRtxzY3abo+VL/dyYr/Rcc8GSWdbQspdSypMCZ68Y YsVCOoBOP5Vr4bjqFsJoxu+CxKhBP/3yj9Unn/6x6o60/4uEQzAwQcvEM4Avm7Oo9XpKKcdT /q1zK/QwDjDb/5b3Srw5YrUfh0jvPyBXrF9fMXQxEQsCQ/IjVWepJLrMT6Uy+kAr3SX4eVjW OyhhWAqpBx9rzmzy8othYTEgJ8exF7D9SV82ok1JNu4RVZnYd68DJtQrzuWN4xsQsMtRWxjp SU0yqUetJKmeCUG1o4ryhDCZ/CdcIWF5gjvWeeXLDxlnnxqYqi/iAy38UW4yu3zSM200FFSo yVfiNnMs3EN1wfP6seZUPRy412t1iqT2ADI8O1EJEE0mrDeK54g2LI/iIccsVnbEi/3nkX5k rOWe1059uWs9ejreLvrqoKGO4J3jgzyKKUjltS6AesiMwgOW2ab+f671L3m5UD5T6tFjvo4k qnXq53aOdwbprKhAwNP1YYj8Rm/Ay+g0NsDhXYHNk5KeAqbj4j1PFHDOO30Ae+lg1uwiDdr2 +zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8un r8ZDDaEBbbcO6fPu3eJ4PguKq+CftlGliz6Lq0q6vngg1clgUMFO66z0shEIEukF+hrdh3KK UHnhc0MRD9iVmsWSeXrjAbHSjtPfzOpWLp64DgnCYWgBIOFR4a3gbXH0j3oVoZOaDVgDVaBW Wzta53CQ+0FPS2fJcFvuiAcSaDnTJUuhlm1rAGv7b1hI6LP/zEA85fq1dx7/erWwB4/8jJ6J 9iFz3nLSHt7zSsTXzFj+qd5rARmz0ubl6h1h/sNDdtI+/ZASRs3L7bV1el7EMz/Uw6HddySD lOnS9CnRzw9U7rd2vcoZEBwU5WnhxHHhG+xBqMN0qeMHNoy+77d2H74I4B8zWzH3e8vlQtuR MwHLmCgiqNlkmqbT4fUj0WUkbqrfqUAzWbM8mmE12+HoEBfVkZ5T6zEWXkVYkaeo87+4wvOS LqnCLJvNQUkq4bKJaZNZNPBkU1aXLHkItufK2O9lmGsBAqZk6uWZdmicGEc0SPBTUkcxllCp zDdbE5uV2H/8Ae8RHR0GFniYl3h67x7oXK/FQovyh2SKlZmz/yz8wIUgvqVT7US2KgFsWEvs WYRfh710tTIBt6Hvwckcr9bZIZ371pA22zxqxRhJtqnNa8o1RYONh96uU/jzUA9BYhHn8YCs Gs21Ex1M63SgzYjP3uImJv3PLPQMGz7+huiPrXX1l/p29GT4q4T6f48pj0PpSmPEUwvuzVi2 thRiD6H44nSSREVSdT3W1o28B5zo/fbZDM87sXazy8kN678qTLE198zYYltgh+9Y9dSNr+FH w7uAoUbAcapMukjh1muaFoNIulT8Kc+O87ueeGB3eanO+NpnTTuimoigsg13U+L+SRUVvbUx 9AC2f7ZlgqLWjHgjUuw58X+mIRKfzYXTSK0zSnpApIUZ7UnJNdRTzz3ZZ3mgIst4vylE2RV/ 1OiGV4cjcqgeB7JKkf4wRUVzkMP53quhSq/yTVw1TAvtKuWmiLUkIGAPFIKPHBGQG56gBLiO 4+x2poVUU+mYSA1jAe9o0HgyOII7LQ6NGTVTUpSKmL5ImZsXIOsrqaaJclV59l71EcfGPT5a lecRLnnphIc2C62BGpSygcwcDSys4n4lRh34I6EBFB0qneROcR5xBOEocfZWeYUxT0eAi9xl TjQAFG4ediv59Sd0ZnZ4Ki4UCq6W5tffDOOr8vIvTan5WBsHRy0nuyi0tzhHw8g1Cbn1t5sH SzWpRf4a4Pv2uy0K+ViNkVvAVb97YJ9FOQc2sMog4oM3HEBmpiP1XMdlGboLdhS1eT1Z2FLQ D8Cxt+T7QT4mQViIn+P24PlRyCdz89mNLzYKisd3iMw6dwPCb/Bte0e23As5Arp61yCBJo11 i0QwvYv9nMA1uQAuQ52iz6YHqhXBk5AeyrlixWP6dm66qRRfmemN7aqhy8c1ZisCq+PpgZEV TP3YJAnSGV/48JxPnrQyGHrrIb+d5ODCLBb/g3RiBrGg+VPfdgpkeEWgCN8JW/nlXQ/zu8gk RFn0dext5PBLmRk+aP/DxJFfG6QBYtb6nTmiqBQmdyT1oakE8B6GzkFa5DvSOqhDDMYsfmP3 +emGSc5q2yHFLPTWwSU8wFjrnvKEtamO2zFfBHxKP1+XAWFYktFj1JMNN3VtoIhChjsw9buI h8R2w==
Ironport-sdr: 63e3b64d_tALLh0DnjfhhP33MhSDtIVaC1L7NVP22J4WiY0IaDlc8pUm lrlkJk6LCDXqH9/GRf7PcZii7FtjP1dYLV8pFjg==

-------------------------------------------------------------------------------

CASC-29 - The CADE ATP System Competition

to be held at

The 29th International Conference on Automated Deduction
Rome, Italy, 1st-4th July 2023

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-29 will be held on the 3rd July 2023, during the
29th International Conference on Automated Deduction.

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, assisted by Martin Desharnais.
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/29/

Registration of systems for CASC-29 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!

-------------------------------------------------------------------------------

[Coq-Club] The CADE-29 ATP System Competition CASC-29, geoff, 02/08/2023