This is the required ReadMe file for the CASC competitions.

For installation, follow the instructions in the main README file.

Translating to proper input format:

None required, E reads TPTP-3 format with includes

Command line:

eprover -xAuto -tAuto --tstp-in -s --memory-limit=384 %s

eproof -xAuto -tAuto --tstp-in --tstp-out --memory-limit=384 %s

Distinguished strings for the results:

Problem is CNF and unsatisfiable:

# TSTP exit status: Unsatisfiable

Problem is CNF and satisfiable:

# TSTP exit status: Satisfiable

Problem is FOF and a theorem:

# TSTP exit status: Theorem

Problem is FOF and not a theorem:

# TSTP exit status: CounterSatisfiable

# Failure:

The start of solution output for proofs:

# Proof object starts here.

The end of solution output for proofs:

# Proof object ends here.

The start of solution output for models/saturations:

# Saturation derivation starts here.

The end of solution output for models/saturations:

# Saturation derivation ends here.