This document contains information about the:

The rules, deadlines, and specifications given here, are absolute. Only the competition panel has the right to make exceptions.

The design and procedures of CASC-JC evolved from those of previous CASCs. Important changes for CASC-JC are:

- The SEM division has not been continued.
- A new EPR division has been added to the competition divisions.
- The MIX division is divided into two classes, one ranked by the number of problems solved, and one ranked by the number of problems solved with a proof output. To be eligible to win this class, sample proofs have to be supplied in advance, and the winner's proofs are checked after the competition.
- The SAT division is divided into two categories, one with equality and one without.
- The problems are taken from an unreleased version of the TPTP.
- Incomplete and augmented TPTP problems are eligible.
- The required system properties have changed.

- ATP systems can be entered at only the division level.
- ATP systems can be entered into more than one division. A system that is not entered into a division is assumed to perform worse than the entered systems, for that type of problem.
- The ATP systems have to run on a single locally provided standard UNIX
workstation (the
*general hardware*). ATP systems that cannot run on the general hardware can be entered into the Demonstration division.

- The
**MIX**division: Mixed CNF Really-Non-Propositional Theorems

*Mixed*means Horn and non-Horn problems, with or without equality, but not unit equality problems (see the UEQ Division below).*Really-Non-Propositional*means with an infinite Herbrand universe. The MIX Division has five problem categories:- The
**HNE**category: Horn with No Equality - The
**HEQ**category: Horn with some (but not pure) Equality - The
**NNE**category: Non-Horn with No Equality - The
**NEQ**category: Non-Horn with some (but not pure) Equality - The
**PEQ**category: Pure Equality

- The
**Assurance**class: Ranked according to the number of problems solved (a "yes" output, giving an*assurance*of the existence of a proof). - The
**Proof**class: Ranked according to the number of problems solved with an acceptable proof output. The competition panel judges whether or not each system's proof format is*acceptable*.

- The
- The
**UEQ**division: Unit Equality CNF Really-Non-Propositional Theorems

- The
**SAT**division: Mixed CNF Really-Non-Propositional Non-theorems

The SAT Division has two problem categories:- The
**SNE**category: SAT with No Equality - The
**SEQ**category: SAT with Equality

- The
- The
**FOF**division: Mixed FOF Non-Propositional Theorems

The FOF Division has two problem categories:- The
**FNE**category: FOF with no Equality - The
**FEQ**category: FOF with Equality

- The
- The
**EPR**division: CNF Effectively Propositional Theorems and Non-theorems

*Effectively propositional*means non-propositional but with a finite Herbrand Universe. The EPR Division has two problem categories:- The
**EPT**category: Effectively Propositional Theorems (unsatisfiable clauses) - The
**EPS**category: Effectively Propositional non-theorems (Satisfiable clauses)

- The

- 440MHz UltraSparc-II CPU
- 256MB memory
- SunOS 5.8

The problems are taken from the TPTP Problem Library. For CASC-JC, the TPTP version is v2.4.0. The TPTP version used for the competition is not released until after the system installation deadline, so that some problems have not been previously seen by the entrants.

The problems have to meet certain criteria to be eligible for selection:

- The TPTP uses
system performance data to classify problems as one of:
- Easy: Solvable by all state-of-the-art ATP systems
- Difficult: Solvable by some state-of-the-art ATP systems
- Unsolved: Not yet solved by any ATP system
- Open: Theorem-hood unknown

- The TPTP distinguishes versions of problems as one of standard, incomplete, augmented, especial, or biased. All except biased problems are eligible.

- The selection is contrained so that no division or category contains an excessive number of very similar problems.
- The selection is biased to ensure that up to 50% of the problems in each category are unseen. (The percentage is dependent on how many new problems are eligible in the category. It is also limited by the "similar problems" constraint.)

*Number of Problems*

The minimal numbers of problems that have to be used in each division and
category, to ensure sufficient confidence in the competition results,
are determined from the numbers of eligible problems in each division
and category
(the competition organizers have to ensure that there is sufficient CPU time
available to run the ATP systems on this minimal number of problems).
The minimal numbers of problems is used in determining the
CPU time limit imposed on each solution
attempt.

A lower bound on the total number of problems that is used is determined from the number of workstations available, the time allocated to the competition, the number of ATP systems to be run on the general hardware over all the divisions, and the CPU time limit, according to the following relationship:

Number of workstations * Time allocated Number of problems = --------------------------------------- Number of ATP systems * CPU time limitIt is a lower bound on the total number of problems because it assumes that every system uses all of the CPU time limit for each problem. Since some solution attempts succeed before the CPU time limit is reached, more problems can actually be used. The actual numbers used in each division and category is determined according to the judgement of the competition organizers.

- replace all predicate and function symbols with meaningless symbols
- randomly reorder the clauses and literals in CNF problems
- randomly reorder the formulae in FOF problems
- randomly reverse the unit equalities in the UEQ problems
- remove equality axioms that are not needed by some of the ATP systems
- add equality axioms that are needed by some of the ATP systems
- output the problems in the formats required by the ATP systems
(The clause type information, one of
`axiom`

,`hypothesis`

, or`conjecture`

, may be included in the final output of each formula.)

`CCCNNN-1.p`

for the symbolic links, with `NNN`

running from `001`

to the number of problems in the respective
division or category.
The problems are specified to the ATP systems using the symbolic link
names.
In the Demonstration division the same problems are used as for the competition divisions, with the same tptp2X transformations applied. However, the original file names are retained.

The timing is done by the UNIX `/bin/time`

command,
which returns times in units of 0.1 second.
If an ATP system cannot solve a problem, the runtime is set to the CPU time
limit.

In the Demonstration division, each entrant can choose to use either a CPU or a wall clock time limit, whose value is the CPU time limit of the competition divisions.

`perl`

script, provided by the competition organizers.
The jobs are be queued onto the workstations so that each
workstation is running one job at a time.
All attempts at the Nth problems in all the divisions and
categories are be started before any attempts at the (N+1)th problems.
During the competition a `perl`

script parses the systems'
outputs.
If an ATP system's success string is found then the timing information
from the `/bin/time`

command is extracted.
The CPU time taken, or the CPU time limit if no solution was found, is
recorded.
This data is used to generate an HTML file, and a WWW browser is
used to display the results.

The execution of the Demonstration division systems is supervised by their entrants.

If only one ATP system registers for a particular competition division, no winner can be announced for that division, but the results for the system are still presented.

At some time after the competition, all high ranking systems in each division are tested over the entire TPTP. This testing provides a final check for soundness, and any system found to be unsound is retrospectively disqualified from the Proof class. At some time after the competition, the proofs from the winner of the Proof class are checked by the panel. If any of the proofs are unacceptable, i.e., they are significantly worse than the samples provided, then that system is retrospectively disqualified from the Proof class.

Entering many similar versions of the same system is deprecated. Entrants may be required to limit the number of system versions that they enter. The division winners from the previous CASC are automatically be entered into their divisions, to provide benchmarks against which progress can be judged. After the competition all systems' source code is made publically available on the CASC WWW site.

The precomputation and storage of any information for individual TPTP
problems for usage during the competition is contrary to the spirit of
the competition, and is not allowed.
The precomputation and storage of information that is reasonably likely
to be useful in some future application is permitted.
For every problem solved, the system's solution process has to be
reproducible by running the system again.
With the exception of the MIX division Proof class, the ATP systems are
not required to output solutions (proofs or models).
However, systems that do output solutions to `stdout`

are
highlighted in the presentation of results.

It is assumed that each entrant has read all the WWW pages related
to the competition, and has complied with the competition rules.
Non-compliance with the rules could lead to disqualification.
A "catch-all" rule is used to deal with any unforseen 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.

- Architecture. This section introduces the ATP system, and describes the calculus, inference rules, and search control used.
- Implementation. This section describes the implementation of the ATP system, including the programming language used, important internal data structures, and any special code libraries used.
- Expected competition performance. This section makes some predictions about the performance of the ATP system in each of the divisions and categories the system is competing in. Any tuning of the system for the TPTP problems must be clearly described.
- References.

In the MIX division, the system that outputs the most acceptable proof
objects (maximally one per problem solved) to `stdout`

is
the winner of the Proof class.
Entrants who wish to be eligible for winning the Proof class have to
email representative samples of their
proofs to the competition organizers before
the sample proofs deadline.
The competition panel decides whether or not each system's proof
objects are acceptable.

The ATP systems have to be executable by a single command line, using an absolute path to the executable that may not be in the current directory. The command line arguments are the absolute path name for a symbolic link as the problem file name, the time limit (if required by the entrant), and entrant specified system switches (the same for all problems). No shell features, such as input or output redirection, may be used in the command line. No assumptions may be made about the format of the problem file name.

- Check: The ATP system can be run by an absolute path to the executable.
For example:
prompt> pwd /home/tptp prompt> which MyATPSystem /home/tptp/bin/MyATPSystem prompt> /home/tptp/bin/MyATPSystem /home/tptp/TPTP/Problems/PUZ/PUZ031-1.p Proof found in 147 seconds.

- Check: The ATP system accepts an absolute path name for a symbolic
link as the problem file name. For example:
prompt> cd /home/tptp/tmp prompt> ln -s /home/tptp/TPTP/Problems/PUZ/PUZ031-1.p CCC001-1.p prompt> cd /home/tptp prompt> /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p Proof found in 147 seconds.

- Check: The ATP system makes no assumptions about the format of the
problem file name. For example:
prompt> cp /home/tptp/TPTP/Problems/PUZ/PUZ031-1.p _foo-Blah prompt> /home/tptp/bin/MyATPSystem _foo-Blah Proof found in 147 seconds.

- Check: The ATP system's CPU time can be limited using the
`TimeLimitedRun.c`

program. For example:prompt> which TimeLimitedRun /home/tptp/bin/TimeLimitedRun prompt> /home/tptp/bin/TimeLimitedRun -q0 10 20 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 10s TimeLimitedRun: WC time limit is 20s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- CPU time limit exceeded

- Check: The ATP system's wall clock time can be limited using the
`TimeLimitedRun.c`

program. For example:prompt> /home/tptp/bin/TimeLimitedRun -q0 20 10 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 20s TimeLimitedRun: WC time limit is 10s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- Alarm clock

`stdout`

indicating the result, one of:
- A solution exists (for CNF problems, the clause set is unsatisfiable, for FOF problems, the conjecture is a theorem)
- No solution exists (for CNF problems, the clause set is satisfiable, for FOF problems, the conjecture is a non-theorem)
- No conclusion reached.

- Check: The system outputs a distinguished string when terminating of
its own accord.
For example, here the entrant has specified that the distinguished string
`Proof found`

indicates that a solution exists. If appropriate, similar checks should be made for the cases where no solution exists and where no conclusion is reached.prompt> /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- Proof found in 147 seconds.

- Check: The system outputs distinguished strings at the start and end
of its proof.
For example, here the entrant has specified that the distinguished strings
`START OF PROOF`

and`END OF PROOF`

identify the start and end of the proof.prompt> /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem -output_proof /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- Proof found in 147 seconds. START OF PROOF ... acceptable proof here ... END OF PROOF

`/bin/time`

command.
- Check: The CPU time taken by a time limited run can be measured by
`/bin/time`

. For example:prompt> /bin/time /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- Proof found in 147 seconds. real 3:04.2 user 2:19.3 sys 7.6

`/tmp`

.
Multiple copies of the ATP systems have to be executable concurrently on different machines but in the same (NFS cross mounted) directory. It is therefore necessary to avoid producing temporary files that do not have unique names, with respect to the machines and other processes. An adequate solution is a file name including the host machine name and the process id.

For practical reasons excessive output from the ATP systems is not allowed.
A limit, dependent on the disk space available, is imposed on the amount
of `stdout`

and `stderr`

output that can be produced.
The limit is at least 10KB per problem (averaged over all problems so
that it is possible to produce *some* long proofs).

- Check: No temporary or other files are left if the system terminates
of its own accord, and no temporary or other files are left anywhere
other than in
`/tmp`

if the system is terminated by a SIGXCPU or SIGALRM. Check in the current directory, the ATP system's directory, the directory where the problem's symbolic link is located, and the directory where the actual problem file is located.prompt> pwd /home/tptp prompt> /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 13526 TimeLimitedRun: ---------------------------------------------------------- Proof found in 147 seconds. prompt> ls /home/tptp ... no temporary or other files left here ... prompt> ls /home/tptp/bin ... no temporary or other files left here ... prompt> ls /home/tptp/tmp ... no temporary or other files left here ... prompt> ls /home/tptp/TPTP/Problems/PUZ ... no temporary or other files left here ... prompt> ls /tmp ... no temporary or other files left here by decent systems ...

- Check: Multiple concurrent executions do not clash. For example:
prompt> (/bin/time /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p) & (/bin/time /home/tptp/bin/TimeLimitedRun -q0 200 400 /home/tptp/bin/MyATPSystem /home/tptp/tmp/CCC001-1.p) TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 5827 TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: ---------------------------------------------------------- TimeLimitedRun: /home/tptp/bin/MyATPSystem TimeLimitedRun: CPU time limit is 200s TimeLimitedRun: WC time limit is 400s TimeLimitedRun: PID is 5829 TimeLimitedRun: ---------------------------------------------------------- Proof found in 147 seconds. Proof found in 147 seconds. real 3:04.2 user 2:19.3 sys 7.6 real 3:04.2 user 2:19.3 sys 7.6

For systems entered in the competition divisions, entrants have to deliver an
installation package to the competition organizers by the
installation deadline.
The installation package must be a `.tar.gz`

file containing
the system source code, any other files required for installation, and
a `ReadMe`

file with instructions for installation.
The installation procedure may require changing path variables, invoking
`make`

or something similar, etc, but nothing unreasonably
complicated.
All system binaries must be created in the installation process; they
cannot be delivered as part of the installation package.
The system is reinstalled onto the general hardware by the competition
organizers, following the instructions in the `ReadMe`

file.
Installation failures before the installation deadline are passed
back to the entrant.
After the installation deadline access to the general hardware is
denied, and no further changes or late systems are accepted
(i.e., deliver your installation package before the installation deadline
so if the installation fails you have a chance to fix it!).
If you are in doubt about your installation package or procedure, please
email the competition organizers.

After the installation deadline the organizers test the ATP systems, first to check that the systems execute correctly (according to the above checks), and secondly to test for soundness. For the soundness testing, non-theorems (satisfiable variants of the eligible problems, e.g., without the conjecture clause, and satisfiable problems selected from the TPTP) are submitted to the systems participating in the MIX, UEQ, FOF, and EPR divisions, and theorems (selected from the TPTP) are submitted to the systems participating in the SAT and EPR divisions. Finding a proof of a non-theorem or a disproof for a theorem indicates unsoundness. If an ATP system fails the soundness testing it is disqualified. The soundness testing has a secondary aim of eliminating the possibility of an ATP system simply delaying for some amount of time and then claiming to have found a solution. Further soundness testing is performed after the competition, as described in the section on performance evaluation.

In the Demonstration division the systems are installed on the respective hardware by the entrants, and no soundness testing has to be performed.