Command-Line Reference

This page documents command-line options for Prover9, Mace4, and Prooftrans. All other programs in bin/ accept help as an argument for a usage synopsis.

Prover9

prover9 [options] [-f file ...]
prover9 [options] problem.p

Basic Options

Flag	Description
`-h`	Print help message and exit.
`-t <seconds>`	Time limit. Overrides `max_seconds` in input file.
`-f <files>`	Read input from one or more files instead of stdin. Multiple files are concatenated.
`-x`	Enhanced auto mode. Maps to: `set(auto2)`.
`-p`	Fully parenthesize all output terms.
`-r <dir>`	Resume from checkpoint directory.
`-m`	Enable memory logging to stderr. Diagnostic use only.

TPTP Flags

Flag	Description
`-tptp`	Force TPTP input mode (read TPTP from stdin).
`-tptp_out`	Force TPTP/TSTP output mode. Normally auto-enabled with TPTP input.
`-ladr_out` / `-ladr-out`	Force native LADR output on TPTP input. Required for prooftrans (ivy, hints, etc.).
`-comp <n>`	Competition mode. Shorthand for `-cores <cpus> -fastPE -t n`.
`-fastPE`	5-second wall-clock timeout on predicate elimination. Also enabled by `set(fast_pred_elim)`.

Strategy Flags

Flag	Description
`-cores <n>`	Sliding-window scheduler with N concurrent children (1–64). Each child runs a different ML strategy.
`-strategy <n>`	Force single strategy index N (0–95). Deterministic single-core search. Overrides `-cores`.
`-strategies <n>`	Override Phase 1 breadth cap (clamped to [1, 96]).

SInE Flags

Flag	Description
`-nosine` / `-no-sine` / `-no_sine`	Disable SInE premise selection. Also disables multi-ordering trial.

Memory Flags

Flag	Description
`-nomem`	Disable memory limit enforcement. Sets `max_megs` to 0 (unlimited).

Positional Arguments

Argument	Description
`problem.p`	Read TPTP input from file. Auto-detected by `.p` extension.

TPTP Auto-Detection

TPTP mode is auto-enabled when any of:

A .p file is given (via -f or as positional argument).
The -tptp flag is present.

When TPTP mode is active, TSTP output is auto-enabled unless -ladr_out is specified.

Examples

prover9 -t 60 -f problem.p           # TPTP input, 60s timeout
prover9 -t 60 -f input.in            # LADR input, 60s timeout
prover9 problem.p                    # TPTP input, bare positional
prover9 -ladr_out -t 60 -f prob.p    # TPTP input, LADR output
prover9 -tptp < input.txt            # TPTP from stdin
prover9 < input.in                   # LADR from stdin
prover9 -x -t 300 -f hard.p          # Auto2 mode, 5 min timeout
prover9 -r ckpt_dir -f input.in      # Resume from checkpoint
prover9 -comp 60 problem.p           # Competition mode, 60s
prover9 -cores 4 -t 300 problem.p    # 4-core sliding window, 5 min

Mace4

mace4 [options] [-f file]
mace4 [options] problem.p

Basic Options

Flag	Description
`-f <file>`	Read input from file instead of stdin.
`-n <n>`	Start domain size. Maps to: `assign(domain_size, n)` and `assign(start_size, n)`.
`-N <n>`	End domain size. Maps to: `assign(end_size, n)`.
`-i <n>`	Domain size increment. Maps to: `assign(increment, n)`.
`-t <n>`	Time limit in seconds (overall).
`-s <n>`	Time limit per domain size.
`-m <n>`	Maximum number of models to find.
`-b <n>`	Memory limit in megabytes.

Model Output

Flag	Description
`-P <0\|1>`	Print models in standard format.
`-p <0\|1>`	Print models in tabular format.

Search Tuning

Flag	Description
`-O <n>`	Selection order (0, 1, or 2).
`-M <n>`	Selection measure (0–4).
`-L <0\|1>`	Least Number Heuristic.
`-G <0\|1>`	Negation propagation.
`-H <0\|1>`	Negative assignment.
`-I <0\|1>`	Negative assignment (near).
`-J <0\|1>`	Negative elimination.
`-K <0\|1>`	Negative elimination (near).
`-R <0\|1>`	Integer ring arithmetic.
`-S <0\|1>`	Skolems last.
`-q <0\|1>`	Iterate over prime domain sizes only.
`-Q <0\|1>`	Iterate over non-prime domain sizes only.

Diagnostic

Flag	Description
`-v <0\|1>`	Verbose output.
`-T <0\|1>`	Trace search (very verbose).
`-A`	Enable memory logging to stderr.
`-e <n>`	Progress reports to stderr every n seconds.

Checkpoint and TPTP Flags

Flag	Description
`-r <dir>`	Resume from checkpoint directory.
`-tptp`	Force TPTP input mode.
`-ladr_out` / `-ladr-out`	Force LADR-format model output with TPTP input. Compatible with interpformat, isofilter, and other LADR tools.
`-c`	Compatibility mode. Ignore unrecognized set/clear/assign commands. Useful for running Mace4 on Prover9 input files.

Positional Arguments

Argument	Description
`problem.p`	TPTP input, auto-detected by `.p` extension.
`axioms.ax`	TPTP input, auto-detected by `.ax` extension.

Examples

mace4 -f problem.p                   # TPTP input, default sizes
mace4 -n 2 -N 10 -t 60 -f prob.p    # Sizes 2-10, 60s timeout
mace4 -n 6 -m 1 -f group.in         # LADR input, size 6, 1 model
mace4 -t 300 -b 4096 -f big.p       # 5 min, 4 GB memory limit
mace4 -c -f prover9_input.in        # Compat mode, ignore P9 opts
mace4 < input.in                     # LADR from stdin
mace4 -r mace4_12345_ckpt_50000     # Resume from checkpoint

Prooftrans

prooftrans [format] [transforms] [-f <file>]

Prooftrans reads Prover9 output (from stdin or -f) and transforms or reformats the proofs. Input must be native LADR format (use -ladr_out when running Prover9 on TPTP files).

Output Formats

At most one format may be specified:

Format	Description
(none)	Default: print proofs as-is (with optional transforms).
`parents_only`	Condensed proof: show only clause and parent IDs.
`xml`	XML format.
`ivy`	Ivy proof object format (for Ivy/ACL2 checker).
`hints`	Extract hints for reuse in subsequent searches.
`tagged`	Tagged proof format (Bob Veroff format).
`tstp`	TSTP format (TPTP standard for proof exchange).

Transforms

Transforms can be combined; order matters:

Transform	Description
`expand`	Expand abbreviated inference steps into primitive steps.
`renumber`	Renumber clause IDs sequentially from 1.
`striplabels`	Remove label attributes from clauses.

Other Options

Flag	Description
`-f <file>`	Read input from file instead of stdin.
`-label <label>`	Add label prefix to hints (with `hints` format only).

Examples

prooftrans < proof.out                     # Print proofs as-is
prooftrans ivy < proof.out                 # Ivy proof object
prooftrans hints < proof.out               # Extract hints
prooftrans parents_only < proof.out        # Condensed proof
prooftrans expand renumber < proof.out     # Expand + renumber
prooftrans tstp < proof.out                # Convert to TSTP
prooftrans hints -label round2 < p.out     # Hints with label
prooftrans ivy -f proof.out                # Ivy, from file

Other Programs

All other programs in bin/ accept help as a command-line argument for a usage synopsis.

Commonly Used Programs

Program	Description
`clausefilter <interps> <test> < clauses`	Filter clauses by evaluation in interpretations. Tests: `true_in_all`, `true_in_some`, `false_in_all`, `false_in_some`.
`interpfilter <clauses> <test> < interps`	Filter interpretations by clause evaluation. Tests: `all_true`, `some_true`, `all_false`, `some_false`.
`interpformat [format] < interps`	Reformat interpretations. Formats: standard, standard2, portable, tabular, raw, cooked, tex, xml.
`isofilter [options] < interps`	Remove isomorphic interpretations.
`get_interps < mace4_output`	Extract interpretations from Mace4 output.
`tptp_to_ladr < problem.p`	Convert TPTP format to LADR format.
`ladr_to_tptp [-p] [-q] < input.in`	Convert LADR format to TPTP format. `-p`: fully parenthesize. `-q`: single-quote TPTP symbols.
`gvizify < proof.out > proof.dot`	Convert proof to Graphviz dot format for visualization.

Next Section: All Prover9 Options