Abstract
The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems—the world championship for such systems. CASC-30 was the 30th competition in the CASC series. Nineteen ATP systems competed in the various divisions. This article presents an outline of the competition design and a commentated summary of the results.
Introduction
Automated Theorem Proving (ATP) deals with the task of proving theorems from axioms—the derivation of conclusions that follow inevitably from known facts (Robinson & Voronkov, 2001). The converse task of disproving conjectures is another facet of interest (Blanchette & Nipkow, 2010; Claessen & Sörensson, 2003). The axioms and conjecture are written in an appropriately expressive logic, and the solutions (proofs and models) are often similarly written in logic (Sutcliffe, 2023b). The CADE ATP System Competition (CASC) (Sutcliffe, 2016) is the annual evaluation of fully automatic, classical logic, ATP systems—the world championship for such systems. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems. Additionally, CASC aims to stimulate ATP research, motivate the development and implementation of robust ATP systems that can be easily and usefully deployed in applications, provide an inspiring environment for personal interaction between ATP researchers, and expose ATP systems within and beyond the ATP community. CASC evaluates the performance of the ATP systems in terms of the number of problems solved, the number of acceptable solutions output, and the average time taken for problems solved, in the context of a bounded number of eligible problems and specified time limits.
CASC is held at each CADE (the International Conference on Automated Deduction) and IJCAR (the International Joint Conference on Automated Reasoning) conference—the major forums for the presentation of new research in all aspects of automated deduction. CASC-30 was held on July 30, 2025, as part of the 30th International Conference on Automated Deduction (CADE-30) in Stuttgart, Germany. It was the 30th competition in the CASC series; see Sutcliffe (2025a) and citations therein, and the CASC web site https://tptp.org/CASC, for information about previous CASCs.
CASC-30 was organized by Geoff Sutcliffe, and overseen by a panel consisting of Aart Middeldorp, Cláudia Nalon, and Tjark Weber. The CASC panel has a few, but important, responsibilities:
Advise (by email) on contentious issues that arise before the competition and that cannot be agreeably resolved by the organizers and entrants. With the help of the organizers, adjudicate on the acceptability of the sample proofs and models that are submitted before the competition. Supply a seed digit for the random problem selection process. If possible, be physically present at the start of the competition, so entrants can see who they are and raise any issues they are concerned about. Be contactable during the competition to advise on contentious issues that arise and that cannot be agreeably resolved by the organizers and entrants. With the help of the organizers, adjudicate on the acceptability of the winners’ proofs and models. If possible, be physically present at the end of the competition for resolving possible open issues, confirming the final system ranking in each division, and assisting in winner announcements.
CASC-30 was run on computers provided by the StarExec project (Stump et al., 2014) at the University of Miami. The CASC-30 website https://tptp.org/CASC/30 provides access to all the resources used before, during, and after the event.
The design and organization of CASC has evolved over the years to a sophisticated state. An outline of the CASC-30 design and organization is provided here. The details areavailable in Sutcliffe (2025b) and on the CASC-30 website. Important changes for CASC-30 were (for readers already familiar with the general design of CASC):
In the competition theorem proving divisions, proofs had to be output in TPTP format, and had to pass a structural verification check. The EPR division returned from hiatus.
The CASC rules, specifications, and deadlines are absolute. Only the panel has the right to make exceptions. It is assumed that all entrants have read the documentation related to the competition, and have complied with the competition rules. Non-compliance with the rules can lead to disqualification. A catch-all rule is used to deal with any unforeseen circumstances: No cheating is allowed. The panel is allowed to disqualify entrants due to unfairness, and to adjust the competition rules in case of misuse.
Executive Summary: CASC-30 was the 30th annual evaluation of fully automatic, classical logic, and ATP systems. CASC-30 fulfilled its objectives by evaluating the relative capabilities of ATP systems, and stimulating development and interest in ATP. The highlight of CASC-30 was the structural checking of proofs, which revealed flaws in many systems proofs. Despite the continued dominance of the Vampire systems, the stimulating and interactive nature of CASC has kept the developer and user communities engaged. The experience gained from CASC-30 has prompted further focus on proof production in CASC-J13.
The rest of this article is organized as follows: Section 2 describes the competition divisions and the ATP systems that entered the various divisions. Sections 3 and 4 describe the competition infrastructure and the requirements for the ATP systems. Section 5 describes how the systems are evaluated. Section 6 provides a commentated summary of the results. Section 7 contains short descriptions of three of the ATP systems. Section 8 discusses some features of the proofs and models produced by the systems in the competition, and some possible new requirements in future CASCs. Section 9 concludes and discusses plans for future CASCs.
A Tense Note: Attentive readers will notice changes between the present and past tenses in this article. Many parts of CASC are established and stable—they are described in the present tense (the rules are the rules). Aspects that were particular to CASC-30 are described in the past tense so that they make sense when reading this after the event.
Divisions and Systems
CASC is divided into divisions according to problem and system characteristics, in a coarse version of the TPTP problem library’s Specialist Problem Classes (SPCs) (Sutcliffe & Suttner, 2001). Each division uses problems that have certain logical, language, and syntactic characteristics, so that the systems that compete in a division are, in principle, able to attempt all the problems in the division. Some divisions are further divided into problem categories that make it possible to analyze, at a more fine-grained level, which systems work well for what types of problems. Table 1 catalogs the divisions and problem categories of CASC-30. The example problems can be viewed online. 1 Sections 3.2 to 3.4 explain what problems are eligible for use in each division and category. Systems that cannot be entered into the competition divisions (e.g., the system requires special hardware, or the entrant is an organizer) can be entered into the demonstration divisions. The demonstration divisions use the same problems as the competition divisions.
Divisions and Problem Categories.
Divisions and Problem Categories.
Nineteen ATP systems competed in the various divisions of CASC-30. The division winners from the previous CASC (CASC-J12) and the Prover9 1109a system were automatically entered into the corresponding demonstration divisions to provide benchmarks against which progress can be judged. The systems, the divisions in which they were entered, and their entrants, are listed in Table 2. A division acronym in italics indicates the system was in the demonstration division. System descriptions are in the competition proceedings (Sutcliffe, 2024a) and on the CASC-30 website.
The ATP Systems and Entrants.
Computers
The StarExec computers used for the competition have two octa-core Intel(R) Xeon(R) E5-2667 v4 CPUs run at 2.10 GHz, 256 GiB memory, and the CentOS Linux release 7.4.1708 (Core) operating system Linux kernel 3.10.0-693.el7.x86_64. There were 30 computers available for CASC-30, that is, 60 CPUs. The StarExec computers are publicly available, which allows system developers to test and tune their systems in exactly the same environment as is used for the competition.
One ATP system runs on one CPU at a time. StarExec uses Linux’s
In CASC-30, a total of 2071 CPU hours were used in 431 WC hours, that is, 7.2 hours spread over the 60 CPUs, which allowed the competition to run live in one conference day. For the problems that were solved, 267 CPU hours were used in 53 WC hours.
Problems for the TPTP-Based Divisions
The problems for the THF, TFA, TFN, FOF, EPR, and UEQ divisions were taken from the Thousands of Problems for Theorem Provers (TPTP) problem library (Sutcliffe, 2017, v9.1.0). The TPTP version used for CASC is released after the competition has started, so that new problems in the release have not been seen by the entrants. The problems have to meet certain criteria to be eligible for use:
The TPTP tags problems that are designed specifically to be suited or ill-suited to some ATP system, calculus, or control strategy as biased. They are excluded from the competition. The problems must be syntactically non-propositional. The TPTP uses system performance data in the TSTP solution library (Sutcliffe, 2007) to compute problem difficulty ratings in the range 0.00 (easy) to 1.00 (unsolved) (Sutcliffe & Suttner, 2001). Problems with ratings in the range 0.21–0.99 are eligible. The upper bound of 0.99 excludes problems that probably would not be solved by any of the systems, and thus would not differentiate between the systems. The lower bound of 0.21 was chosen (many years ago, and it has worked successfully) to exclude problems that would be solved by most of the systems and thus not differentiate between the systems. Problems of lesser and greater ratings are made eligible if there are not enough problems with ratings in that range. In the CASC-30, TFN division 68 problems with rating 0.00 and 49 problems with rating 1.00 were made eligible, because there were only 47 eligible problems with rating 0.21–0.99 (there were no problems with rating 0.01–0.20). In the CASC-30 EPS problem category 191 problems with rating 0.00, two problems with rating 0.14, and 12 problems with rating 1.00 were made eligible, because there were only 46 eligible problems with rating 0.21–0.99. The organizer considered making these additional problems eligible to be acceptably useful: solving easy problems would be encouraging for weaker systems, and solving hard problems would be encouraging for stronger systems. See Sections 6.3 and 6.5 for the results on these additional problems. Systems can be submitted before the competition so that their performance data is used in computing the problem ratings—problems that are newly solved get a rating <1.00 and thus become eligible (until the rating drops below 0.21). The rating calculation also uses performance data from ATP systems that are not entered into the competition, which can produce ratings that make some problems eligible for selection but easy or unsolvable for the systems in the competition. Using problems that are solved by all or none of the competition systems does not affect the competition rankings, has the benefit of placing the systems’ performances in the context of the state-of-the-art in ATP, but does reduce the differentiation between the systems in the competition.
In order to ensure that no system receives an advantage or disadvantage due to the specific presentation of the problems in the TPTP problem library, the problems are obfuscated by stripping out all comment lines (in particular, the problem header), randomly reordering the formulae (
The number of problems used in each division and problem category are constrained by the number of eligible problems, the number of systems entered in the divisions, the number of CPUs available, the time limits, and the time available for running the competition live in one conference day, that is, in about 6 hours. The number of problems used are set within these constraints according to the judgment of the organizer. The problems used are randomly selected from the eligible problems based on a seed supplied by the competition panel:
The selection is constrained so that no division or category contains an excessive number of very similar problems, according to the “very similar problems” (VSP) lists distributed with the TPTP problem library (Sutcliffe, 2000). For each problem category in each division, if the category is going to use In order to combat excessive tuning toward problems that were in the preceding TPTP version, the selection is biased to select problems that are new in the TPTP version used until 50% of the problems in each problem category have been selected or there are no more new problems to select, after which random selection continues from old and new problems. The number of new problems used depends on how many new problems are eligible and the limitation on very similar problems. Problems with rating 0.21–0.99 are selected before problems with other ratings.
Table 3 gives the number of eligible problems, the maximal numbers that could be used after taking into account the limitation on very similar problems, and the number of problems used in each division and category. With the exception of the SLH division (which is a special case), nowhere near 50% new problems could be selected. See Section 9 for a plea to the community to submit new problems to the TPTP problem library.
Number of Eligible and Used Problems.
Number of Eligible and Used Problems.
The problems are given to the ATP systems in TPTP format, with include directives, in increasing order of TPTP difficulty rating.
For the SLH division of CASC-29, Isabelle’s Sledgehammer system (Paulson & Blanchette, 2010) was used to generate 8,400 problems that could be used, of which 1,000 appropriately difficult problems were selected based on performance data (Sutcliffe, 2023a; Sutcliffe & Desharnais, 2024). For the SLH division of CASC-J12, the same problem set was used, and 1,000 problems not used in CASC-29 were selected. For the SLH division of CASC-30, the same problem set was used, and 1,000 problems not used in CASC-29 or CASC-J12 were selected. The reuse of the problem set was announced in advance of CASC-30, so that developers could tune their systems using the CASC-29 and CASC-J12 problems. The problems are not modified by any preprocessing, thus allowing the ATP systems to take advantage of natural structure that occurs in the problems.
Of the 1,000 problems selected for CASC-30, 383 had not been solved in the testing done before CASC-29. If many of them were solved in the competition, that would indicate progress. See Section 6.7 for the results on these problems.
The problems are given in a roughly estimated increasing order of difficulty.
Problems for the ICU Division
For the ICU division each entrant had to submit 20 FOF theorems (axioms with a provable conjecture). The problems had to be provided in decreasing order of desired use in the division, for example, from hardest to easiest for other systems. The problems had to be all different, as assessed by the competition organizers. It was expected that each entrant would submit problems that are easy enough for that entrant’s system, but difficult for the other entrants’ systems, that is, each entrant is saying to the others: “I Challenge yoU!”
For CASC-30, the 10 problems chosen for the CASC-J12 winner, Vampire 4.9, were reused. Then the top 13 problems were taken from each of the entrant’s submissions, excluding duplicates. That gave a total of 101 problems. It was later noticed that one of the selected problems was satisfiable, and removed, leaving 100 problems for the competition. Eighty-four of the 100 problems are existing TPTP problems, of which 32 had difficulty rating 1.00, and the average difficulty rating over the 84 was 0.90. The remaining 16 problems were all versions of existing TPTP problems that had been modified to suit the entrant’s system.
The problems were given in reverse order of desired use, so that the “easier” problems were used before “harder” ones.
Time Limits
In the THF, TFA, TFN, FOF, EPR, UEQ, and ICU divisions, a WC time limit is imposed for each problem. The minimal time limit for each problem is 120 seconds, except for the ICU division where the minimal time limit is 300 seconds. The maximal time limit for each problem is constrained by the same factors that constrain the number of problems that are used, taking into account the phenomenon that ATP systems solve most problems quickly and very few slowly (Sutcliffe, 2024b; Sutcliffe & Suttner, 2001)—this phenomenon is evident in the performance plots from the competition, 2 and from the ratios of total times taken to solved times given in Section 3.1. The time limit is chosen value within the range allowed according to the judgment of the organizer, and is announced at the competition. In CASC-30, a 240-second WC time limit was imposed for each problem in the THF, FOF, and UEQ divisions, and a 120-second WC time limit was imposed for each problem in the TFA, TFN, and EPR divisions. No CPU time limits were imposed (so that it could be advantageous to use all the cores on the CPU).
In the SLH division, a CPU time limit is imposed for each problem. The limit is between 15 and 90 seconds, which is the range of CPU time that can be usefully allocated for a proof attempt in the Sledgehammer context. 3 The time limit is chosen within the range allowed according to the judgment of the organizer, and is announced at the competition. In CASC-30, a 15-second CPU time limit was imposed for each problem.
In the ICU division, a WC time limit is imposed for each problem. The limit is between 300 and 600 seconds, which is a range that gives the systems sufficient time (4,800-second CPU time on the octa-core CPUs) to attempt the difficult problems submitted. The time limit is chosen within the range allowed according to the judgment of the organizer, and is announced at the competition. In CASC-30, a 480-second WC time limit was imposed for each problem.
System Entry, Delivery, and Execution
Systems can be entered at only the division level, and can be entered into more than one division. A system that is entered into a division is assumed to perform better than any system that is not entered—wimping out is not an option. Entering many similar versions of the same system is deprecated, and entrants can be required to limit the number of system versions that they enter. Systems that rely essentially on running other ATP systems without adding value are deprecated; such systems might be disallowed or moved to the demonstration division.
The ATP systems entered into CASC are delivered to the competition organizers as StarExec installation packages, which the organizer installs and tests on StarExec. Source code is delivered separately, under the trusting assumption that the installation package corresponds to the source code. All competition division systems’ StarExec packages are available on StarExec, and their source code packages are available on the CASC website. This allows anyone to use the systems on StarExec, and to examine the source code. An open source license is encouraged to allow the systems to be freely used, modified, and shared. Many of the StarExec packages include statically linked binaries that provide further portability and longevity of the systems.
The ATP systems must be fully automatic. They are executed as black boxes, on one problem at a time. Any command line parameters have to be the same for all problems in each division. The systems must be sound, and are tested for soundness by submitting non-theorems to the systems in the THF, TFA, FOF, EPR, UEQ, SLH, and ICU divisions, and theorems to the systems in the TFN and EPR divisions. Claiming to have found a proof of a non-theorem or a disproof of a theorem indicates unsoundness. Two systems were found to be unsound before CASC-30, and were repaired in time for the competition.
In CASC, each ATP system is entered under one name, but it is common for the entrant to deliver multiple installation packages, each specialized to particular divisions in the competition, for example, separate packages for the TFA and TFN divisions, and separate packages for the FOF, EPR, and UEQ divisions. In some cases, multiple packages are combined into one by adding a wrapper that detects the SPC of the problem, and then call the appropriate package’s entrypoint. Requiring the use of a different package depending on the problem type is a coarse level of non-automation. Users of ATP systems can have different intentions that produce distinct tasks for the systems. Common examples are theorem proving versus disproving, and testing for unsatisfiability versus model finding (the latter is often the implementation of the former). In CASC, the theorem proving task is used in all the CASC divisions except the TFN division, the TFN division requires disproving and model finding, and the EPR division requires both. It is thus understood that different system packages can be required for these three groups of divisions. In CASC-J13, entrants will be restricted to maximally three installation packages, corresponding to those three use cases. The ATP systems will be responsible for detecting the problem type and running appropriate components. This will improve the level of automation in the ATP systems.
System Evaluation
CASC ranks the ATP systems at the division level. For each system, for each problem, four items of data are recorded: whether or not the problem was solved, whether or not a solution (proof or model) was output, and the CPU and WC times taken (as measured by StarExec’s
The competition panel decides whether or not the systems’ solutions are “acceptable.” The criteria for acceptable proofs were stricter than in CASC-J12:
Inference steps must be reasonably fine-grained. For proofs that use translations from one form to another, for example, translation of FOF problems to CNF, the translations must be adequately documented. Proofs must be in TPTP format
4
(Sutcliffe et al., 2006). In the competition theorem proving divisions—the THF, TFA, FOF, UEQ, SLH, and ICU divisions—proofs must be structurally correct:
Annotated formulae in a proof must be uniquely named. Proofs must show only relevant inference steps. Proofs must be acyclic. Proofs must have formulae from the problem as leaves, and end at the conjecture for axiomatic proofs, or end with Proofs that negate the conjecture must give the resultant formula the role Proofs that introduce new symbols in definitions must provide a Proofs that make TPTP formatting is checked using TPTP4X (Sutcliffe, 2007), and proof structure is checked using GDV (Sutcliffe & Belfiore, 2005). TPTP4X and GDV are available in SystemOnTSTP.
5
Models must be complete, documenting the domain, function maps, and predicate maps. The domain, function maps, and predicate maps may be specified by explicit ground lists (of mappings), or by any clear, terminating algorithm. Saturations are acceptable if their models are a subset of the models of the problem formulae.
In addition to the ranking data, three other performance measures are presented in the results: The state-of-the-art contribution (SotAC) quantifies the unique abilities of each system (excluding the previous year’s winners that are earlier versions of competing systems). For each problem solved by a system, its SotAC for the problem is the fraction of systems that do not solve the problem. A system’s overall SotAC is the average SotAC over the problems it solved but not solved by all the systems. The efficiency balances the number of problems solved with the time taken. It is the average solution rate over the problems solved multiplied by the fraction of problems solved (the solution rate for one problem is the reciprocal of the time taken to solve it). Efficiency is computed for both CPU time and WC time, to measure how efficiently the systems use one core and multiple cores, respectively. The core usage measures the extent to which the systems take advantage of multiple cores. The core usage is the average ratio of CPU time to WC time used over problems solved. Core usage below 1.0 for a problem is typically the result of the problem being solved in early (pre)processing before multi-core search is started. While high core usage can be seen as a strength of an ATP system, the ability to solve problems quickly before multi-core search is started is also a strength. The results present the average core usage and the number of problems solved with core usage >1.0 (the number of problems that were solved without using multiple cores is simply the difference between the number solved and the number solved with core usage >1.0). The competition ran on octa-core computers, thus the maximal core usage was 8.0.
The result tables give the number of problems solved with an acceptable solution output, the number of problems solved (without considering solution output), the average CPU or WC time taken over the problems solved, the state-of-the-art contribution, the (micro-)efficiency, the core usage/the number of problems solved with core usage >1.0, the number of new problems solved, and the number of problems solved in each problem category. In each column, the best value in the competition division is given in
The structural checking of proofs in the competition theorem proving divisions—the THF, TFA, FOF, UEQ, SLH, and ICU divisions—was new in CASC-30. It was the first step along a path to full verification of proofs in CASC. For most systems some of their proofs failed the structural checking, and as a result the number of problems solved with an acceptable solution output is less than the number of problems solved. Some developers knew in advance that their system’s proof output was not acceptable, and some of them retreated to the demonstration divisions, while some decided to tough it out in the competition divisions. In both cases the “number of problems solved with an acceptable solution output” is set to “–” rather than 0. A full analysis of the reasons for the failures is given in Section 8.
The THF Division
Table 4 summarizes the results of the THF division. Vampire 5.0 won the division, but solved less problems than the CASC-J12 winner Vampire 4.9. The developers thought there should be a minimal difference between the two versions because they use the same source code. They suggested that a different compiler version (or compiler flags) was used to build the Vampire 5.0 binary, or that, while unlikely, the randomized strategies in the schedules might have resulted in plain bad luck for Vampire 5.0. It is impressive that Vampire 5.0 was able to solve so many problems, which necessarily include more difficult problems, with the lowest average time taken (but again, Vampire 4.9 outperformed Vampire 5.0 in this respect). The versions of Vampire up to and including 5.0 have separate binaries for first-order and higher-order logics. According to the Vampire developers, the two branches of the source code are being merged so that for CASC-J13 there will be a single binary for all the competition divisions.
THF Division Results.
THF Division Results.
Vampire 5.0 has the best results over almost all measures. The exception is core usage, where Zipperposition solved more problems using multiple cores, and had the highest core usage. E solved the most problems before starting to use multiple cores, and had good core usage when it did use multiple cores. Leo-III used multiple cores for all the problems it solved. cvc5’s high average time taken is a consequence of it’s sequential strategy schedule that uses a single core (the one result that appears to use 1.5 cores is an artifact of the competition measurement harness). The problem category rankings are generally aligned with the overall ranking, with the exception that Zipperposition had better performance on problems without equality.
The detailed results show that E solved eight problems “at the time limit.” An examination of E’s logs revealed that the problems were actually solved in less time, but the proof was printed only when the time limit was reached. In two cases, one in each problem category, the claim of theoremhood was output only after the time limit, and thus not counted as solved. The developer explained: “E waits for all its children to terminate before printing the proof, so if one does not respond to the
The individual problem results (without considering proof output) show that 19 problems were unsolved, 170 problems were solved by all the systems, and 31 problems were solved by only one system (14 problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). Of the 31 unique solutions, 14 were by Vampire 5.0, seven by E, five by Zipperposition, three by cvc5, and two by Vampire 4.9. A portfolio (sharing the time between several systems) of these five systems, with 48 seconds allocated to each, would solve 474 problems.
Table 5 summarizes the results of the TFA division. The winner was Vampire 5.0. Vampire’s arithmetic reasoning capabilities have recently been improved by the ALASCA approach to reasoning over quantified linear arithmetic (Korovin et al., 2023), with further extensions by the VIRAS technique for quantifier elimination in integer-real arithmetic (Schoisswohl et al., 2024).
TFA Division Results.
TFA Division Results.
The SotAC, efficiency, category, and new problem rankings are aligned with the overall ranking. There were seven new problems in the division, all in the TFI problem category, that is, using integers. Four of the new problems are software creation problems (the TPTP
The individual problem results (without considering proof output) show that 15 problems were unsolved, 65 problems were solved by all the systems, and 23 problems were solved by only one system (16 problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). Of the 23 unique solutions, 19 were by Vampire 5.0, three by cvc5, and one by Vampire 4.9. The dominance of Vampire 5.0 means that only a little can be gained from a portfolio of the systems—a combination of the two Vampires with cvc5, with 40 seconds allocated to each, would solve 133 problems.
The CASC-J12 report said: “Over the years the TFA division has struggled to attract entrants, with the same few systems being entered each year … CASC will continue to have a TFA division in order to encourage development of ATP in this area.” Sadly, there has been no change to the situation, and the TFA division will not be run in CASC-J13 (which will be somewhat different anyway, as explained in Section 9).
Table 6 summarizes the results of the TFN division. Vampire 5.0 solved the most problems, iProver 3.9.3 came in second, and cvc5 third. All three systems output acceptable models for all the problems they solved. This is in contrast to CASC-J12 where Vampire 4.9 solved the most problems but none of its models were considered acceptable, iProver 3.9 came second but output acceptable models for only 67 of the 85 problems it solved, and cvc5 came third but output no acceptable models. This matter was closely examined after CASC-J12, and the developers of all three systems admitted to the deficiencies in their systems’ model output. It is pleasing to see the positive impact that had, leading to improved model output from all three systems in CASC-30.
TFN Division Results.
TFN Division Results.
As noted in Section 3.2, 68 problems with rating 0.00 and 49 problems with rating 1.00 were made eligible for the TFN division. Of those, 59 problems of rating 0.00 and 44 problems of rating 1.00 were selected. Of the 59 problems with rating 0.00, 41 were solved by all the systems, and all the problems were solved by Vampire 5.0. Of the 44 problems with rating 1.00, 39 were unsolved, and the other five were solved by only Vampire 5.0. One might expect all the problems with rating 0.00 and none of the problems with rating 1.00 to be solved, but this is not the case because the ratings were calculated using earlier versions of the systems. Progress in ATP is not monotonic.
The individual problem results (without considering model output) show that 40 problems were unsolved, 46 problems were solved by all the systems, and 14 problems were solved by only one system (all 14 problems were solved by only Vampire 5.0). A portfolio approach cannot improve on the individual systems’ results. Of the 14 problems solved by only Vampire 5.0, eight are hardware verification (the TPTP
Table 7 summarizes the results of the FOF division. The Vampires dominated the division again. It is noteworthy that Vampire 4.9 solved more problems than Vampire 5.0. The developers believe that the main difference is that Vampire 4.9 has a “cautiously specialized” schedule (Bártek et al., 2024) of seven branches, while Vampire 5.0 has a single monolithic schedule. The intent was for Vampire 5.0 to have a schedule that might be more general on unseen problems, but would show its strength only with longer time limits. Some new implementation features in Vampire 5.0, for example, term ordering diagrams (Hajdu, Coutelier et al., 2025), could also have had a positive influence.
FOF Division Results.
FOF Division Results.
A key differentiator between the FOF division systems is their abilities to generate acceptable proofs. There is a notable difference between the ranking by number of acceptable proofs output, and the ranking by the number of problems solved. Vampire 5.0, E, and LisaTT were the only systems to output an acceptable proof for every problem solved. It was disappointing that iProver solved so many problems, but failed to output acceptable proofs for a significant fraction of them, thus pushing iProver down to third place. Prior to the running of CASC-30 the developer of CSI_Enigma was close to completing proof output, which if completed would have placed the system second. CSE_E solved two FEQ problems close to the time limit, but did not finish proof output by the time limit. Hopefully more systems will consistently produce acceptable proofs in CASC-J13.
In terms of problems solved (without considering proof output) the ranking is similar to that of CASC-J12. The exceptions were improved performance of CSI_Enigma over that of CSI_E in CASC-J12, and iProver switching positions with CSE_E. The improved performance of CSI_Enigma over CSI_E can be attributed to the use of the Enigma system (Jakubuv & Urban, 2017) as the secondary system instead of E. Note that all of CSI_Enigma’s proofs took more than 1 second. The improvement in iProver was due to efficiency improvements and heuristic optimization. In CASC-J12, a clear separation was observed between three groups of systems: “Vampire 4.9,” the ‘‘hoi polloi,” and the ‘‘also rans.” The performance plots for the FOF division in CASC-30 7 show a more progressive separation between the systems, with only Prover9, Connect++, hopCoP, and SPASS-SCL being separated into a trailing group. While the Vampires still stand out ahead, CSI_Enigma fills the gap between them and the pair of iProver and E.
The Vampires had the lowest average WC times, and correspondingly the highest efficiencies. Vampire 5.0 had a high SotAC, thanks to it’s ability to solve problems that no other systems solved (see below). Drodi made the most use of the multiple cores thanks to its parallelization architecture. The developer explained: “Preprocessing is done only once before multi-processing is started, after which the parent process forks as many additional processes as there are cores available. The processes share basic information by sharing a small portion of memory that holds a list of strategies with an associated time slice. The processes repeatedly take a strategy off the list and run it for the associated time slice. If a proof is found all processes are stopped, otherwise the process loops to take another strategy. This way there is no need to repeat the preprocessing or start a new process for each new strategy.”
The performances in the two problem categories are well aligned with the overall performance, except for SPASS-SCL’s poor performance on problems with equality. The new problems provided different challenges for the systems. Vampire’s monolithic schedule showed its intended ability to solve unseen problems. E performed worse on the new problems, failing to solve some new logic calculi (the TPTP
The individual problem results (without considering proof output) show that 12 problems were unsolved, no problems were solved by all the systems, and 36 problems were solved by only one system (19 problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). Of the 36 unique solutions, 22 were by Vampire 5.0, eight by Vampire 4.9, five by cvc5, and one by CSI_Enigma. A portfolio of the two Vampires, cvc5, and CSI_Enigma, with 60 seconds allocated to each, would solve 484 problems.
The EPR division returned from hiatus in CASC-30. The most recent prior winner was Vampire 4.4 from CASC-27 in 2019. Unfortunately Vampire 4.4’s StarExec package has been lost, and was thus not available for the demonstration division. A comparison with iProver is a reasonably meaningful comparison system, as iProver dominated the division from CASC-J4 in 2008 through CASC-J9 in 2018. Recall also that the EPR division does not require solution output (see Section 5). With that context, Table 8 summarizes the results of the EPR division. Vampire 5.0 solved the most problems, outperforming iProver.
EPR Division Results.
EPR Division Results.
Vampire had a very high SotAC, thanks to it’s ability to solve problems that no other systems solved (see below). Vampire also had the highest efficiency, followed by Drodi. Drodi had the highest core usage. E suffered from the bug explained in Section 6.1, with five EPS problems solved but not counted because the claim of satisfiability came only after the time limit.
Most of the systems did better in the EPS problem category. While there was no requirement for acceptable solution output in the EPR division, most of the systems did output models. The question of what constitutes an acceptable model has been a topic of quite hot debate after models were deemed unacceptable in the TFN division of CASC-J12 (see Section 6.3). In particular, there are conflicting views of whether or not a saturation is acceptable, for example, Peltier (2003) claims that saturations are “useless from a practical point of view.” Given that a saturation represents a set of Herbrand models, a salient question is whether that set should be a subset of the models of the input formulae. Vampire 5.0’s preprocessing steps can lead to a saturation whose models is not a subset, but a list of “Definitions and Model Updates” is provided to convert the saturation into one whose models are a subset. The competition panel ruled that this combination of “saturation+updates” constitutes an acceptable model. Other types of model output were Vampire’s finite models with a domain and mappings, and iProver’s Herbrand models expressed as a term algebra. The distribution of the different types of models produced is interesting: Vampire produced 35 saturations without updates, 26 saturations with updates, and 29 finite models; iProver produced 26 saturations and 57 Herbrand models; the other systems produced only saturations. Vampire’s ability to find finite models gave it a clear advantage.
As noted in Section 3.2, 191 problems with rating 0.00, two problems with rating 0.14, and 11 problems with rating 1.00 were made eligible for the EPR division, all in the EPS problem category. Of those, 72 problems of rating 0.00, both problems of rating 0.14, and nine problems of rating 1.00 were selected. Of the 72 problems with rating 0.00, 42 were solved by all the systems, 62 were solved by Vampire 5.0, and all the problems were solved by at least one system. Of the nine problems with rating 1.00, only one was solved, by Vampire.
The individual problem results show that 14 problems were unsolved, 55 problems were solved by all the systems, and 13 problems were solved by only one system, all by Vampire 5.0. A portfolio approach cannot improve on the individual systems’ results.
Table 9 summarizes the results of the UEQ division. Vampire 5.0 won, with an improvement over Vampire 4.9. The recent advances in Vampire’s UEQ calculus and implementation (Hajdu, Coutelier et al., 2025, Hajdu, Kovács et al., 2025) have contributed significantly to Vampire’s strong performance. Twee 2.6.0 solved the same number of problems as Vampire 4.9, indicating improvement since Twee 2.5.0, which was convincingly beaten by Vampire 4.9 in CASC-J12. The Twee developer explained: “this year’s version has fixes for some completeness bugs, which allows some slightly more aggressive redundancy criteria to be used.” Only CSE_E and iProver failed to output acceptable proofs for all problems solved. In the case of iProver this was quite severe, moving it from a possible fourth place down to the bottom of the competition division (see Section 8 for more details).
UEQ Division Results.
UEQ Division Results.
The SotAC, efficiency, and core usage values were roughly aligned with the division ranking, with the exceptions of iProver’s higher SotAC, and Drodi’s higher efficiency and core usage. It is noteworthy that compared to the other divisions a higher fraction of problems were solved with a core usage >1.0. The exception was Toma, which makes no use of the multiple cores (the 19 results that appear to use multiple cores are an artifact of the competition measurement harness). Over the other systems, an average of 90% of the problems were solved with multiple cores used. This is in contrast to, for example, the FOF division, where the average (excluding the systems that did not try to use multiple cores) is 76%.
The individual problem results (without considering proof output) show that four problems were unsolved, 59 problems were solved by all the systems, and 17 problems were solved by only one system (four problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). Of the 17 unique solutions, seven were by Vampire 5.0, six by Twee 2.6.0, and five by Vampire 4.9. A portfolio of Vampire 5.0, Twee, and E, with 80 seconds allocated to each, would solve 285 problems. Although there were no problems that only E solved, its ability to solve problems quickly makes it a useful contributor to a portfolio. For the suggested portfolio there are 11 problems that only E can solve within 80 seconds.
Table 10 summarizes the results of the SLH division. Vampire’s improved performance on higher-order problems (see Section 6.1) showed again here. As noted in Section 3.3, 383 of the 1,000 problems had not been solved in the testing done before CASC-29, and if many of them were solved in CASC-30 that would indicate progress in the field. Of the 383 problems, five were solved in CASC-30, five by Vampire 5.0, three by Vampire 4.9, and one by E. The lack of progress might be attributed to the lack of tuning that was expected. The CASC-30 design informed the developers that the SLH problems would be taken from the same problem set as for CASC-29 and CASC-J12, so that the systems could be tuned using the problems selected for CASC-29 and CASC-J12. According to the systems’ developers, no such tuning was done.
SLH Division Results.
SLH Division Results.
The logs from Leo-III revealed that it suffered from the short 15 seconds CPU time limit. The developer explained: “Leo-III runs in a JVM. The start-up of a JVM uses quite a lot of time, and execution of the Leo-III code is slow at first as the JVM is loading the required classes on-demand. This gets better once proof search is running.” A quick experiment was done using a native build that compiles to LLVM code, on two relatively easy problems on which Leo-III timed out in the competition:
The individual problem results (without considering proof output) show that 479 problems were unsolved, 21 problems were solved by all the systems, and 102 problems were solved by only one system (41 problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). In CASC-J12, 258 problems were solved by all the systems: Vampire 4.9, E 3.2.0, cvc5 1.1.3, and the CASC-29 winner E 3.1. The impact of Leo-III in CASC-30 is evident—234 problems were solved by all the other systems. Of the 102 unique solutions, 45 were by Vampire 5.0, 36 by E, 13 by cvc5, seven by Vampire 4.9, and one by Leo-III A portfolio approach works well here—a portfolio of E, Vampire 4.9, and cvc5, with 5 seconds allocated to each, would solve 482 problems.
The SLH division has served it’s purpose, to raise awareness of the needs of the Sledgehammer system—higher-order problems to be solved within a short CPU time limit. Sadly, it has not inspired developers to tune to the problem set. The SLH division will go on hiatus from CASC-J13.
Table 11 summarizes the results of the ICU division, and Table 12 shows how many of the problems submitted by each system’s developer were solved by each system (the columns correspond to the problem submissions from the corresponding system row). As might have been expected, the Vampires were dominant (see Section 6.4 for the reasons). Most of the systems solved all or most of their submitted problems, and Vampire 5.0 additionally solved all of Drodi’s problems. CSI_Enigma and E also solved a reasonable cross-section of the other systems’ problems.
ICU Division Results.
ICU Division Results.
ICU Matrix.
The SotAC values align with the division ranking, but the efficiency values are less aligned. iProver and CSI_Enigma had lower efficiencies due to their higher average times taken. Drodi’s performance stands out thanks to its low average time taken and high core usage.
The individual problem results (without considering proof output) show that 14 problems were unsolved, no problems were solved by all the systems, and 24 problems were solved by only one system (14 problems were solved by only the two versions of Vampire, and are counted as unique solutions for Vampire 5.0). Of the 24 unique solutions, 18 were by Vampire 5.0, five by Vampire 4.9, and one by E. A portfolio approach naturally works well here because the problems were purposefully chosen for each system. A combination of the two Vampires and E, with 160 allocated to each, would solve 86 problems.
Each year the competition report features short system descriptions of systems that stand out in some way. For CASC-30, the salient systems are the newcomers: hopCoP 0.1, LisaTT 0.9.1, and SPASS-SCL 0.1. These short descriptions of the systems were written by their entrants.
Acceptable Proofs and Models
The CASC-J12 report noted the benefits of moving toward a “verified track” in CASC, and an incremental approach was suggested:
Solutions must be written in the TPTP language (Sutcliffe, 2023b). Solutions must be written in the TPTP formats for derivations (Sutcliffe et al., 2006), tableaux, and models (Steen et al., 2023). Solutions must be structurally correct, for example, derivations must be acyclic, finite models must have domains. Solutions must be for the given problem. Solutions must be logically correct. This is where most attention has been paid in proof verification, for example, Andreotti et al. (2023), McCune and Shumsky-Matlin (2000), and Wetzler et al. (2014), possibly at the expense of the preceeding requirements that are simply assumed. Verification of the logical properties of models has not received adequate attention.
It was decided that CASC-30 would check the first three items above for proofs in the THF, TFA, FOF, UEQ, SLH, and ICU competition divisions (see Section 5). The impact was interesting, as can be observed in the differences between the “Soln” and “Solved” columns of the results Tables 4, 5, 7 and 9 to 11. Table 13 summarizes the number of proofs that passed structural checking, for those systems that did output proofs. The highest fractions of success in each division are given in
Structural Checking Failures.
Structural Checking Failures.
There are 482 proofs that failed structural checking. The reasons for failure are varied: 12 because a refutation has a root node that is not
It was observed that many of the ATP systems’ proofs include “inference steps” that are calls to SAT/ATP/SMT systems, which infer
In an effort to further improve the quality of ATP systems’proofs, CASC-J13 will require the systems to aim to report only the parents that are used in each inference step of a proof. It is clear that the systems can only “aim to” comply, because precisely extracting the set of parents that were used by a SAT/ATP/SMT system might not be possible in all cases. From the organizational side, checking conformance to that requirement might not be possible in all cases. We’ll all just do the best we can.
Even with a minimization of the parents list in inference steps, it is debatable whether a successful call to a SAT/ATP/SMT system is really an “inference step.” The SAT/ATP/SMT systems typically build a proof of their own, and that proof structure is not shown in the ATP system’s proof that reports the step. It would be preferable for the SAT/ATP/SMT system’s proof to be exposed, and grafted into the ATP system’s proof. An interesting two-level example starts with Leo-III’s refutation for
These more rigorous requirements for proofs in CASC resonate with the proof verifier competition (ProoVer) that is being planned for IJCAR in 2027. ProoVer will evaluate the capabilities of proof verifiers, and the extent to which ATP systems’ proofs can be verified. In the long term a verified track will be added to CASC … baby steps.
CASC-30 was the 30th annual evaluation of fully automatic, classical logic, andATP systems. CASC-30 fulfilled its objectives by evaluating the relative capabilities of ATP systems, and stimulating development and interest in ATP. The highlight of CASC-30 was the structural checking of proofs, which revealed flaws in many systems proofs. This will lead to improvements in proof output over the next year. Despite the continued dominance of the Vampire systems, the developer and user communities have remained engaged with CASC. A key to this is CASC’s stimulating and interactive nature: a live competition run during one day of the conference; opportunities for users and observers to be involved; a social dinner where entrants and associates can interact; distinctive T-shirts that identify system developers and others who are part of the competition.
While the design of CASC is mature and stable, each year’s experiences lead to ideas for changes and improvements. Changes being planned for CASC-J13 are:
The ProoVer verifier competition will take center stage. The TFA and SLH divisions will go on hiatus. CASC will be smaller, with only the THF, FOF, and UEQ divisions. Only one installation package will be allowed for each entry—all three divisions require theorem proving/unsatisfiability checking. Systems will be required to minimize the parent list in proof inference steps, and encouraged to graft in subsystems’ proofs.
As always, the ongoing success and utility of CASC depends on ongoing contributions of problems to the TPTP. The automated reasoning community is encouraged to continue making contributions of all types of problems.
Footnotes
Author Contributions
The article, except for Section 7, was written by the article author. The three subsections of Section 7 were written by Michael Rawson (hopCoP), Simon Guilloud (Lisa’s Tableau Tactic), and Christoph Weidenbach (SPASS-SCL-FOL 0.1).
Funding
The author received no financial support for the research, authorship, and/or publication of this article.
Declaration of Conflicting Interests
The author declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.