Command-line entry point for the Shot prover, packaged as an escript.

ShotTx is the tableau component of the Shot ecosystem; the shot_tx binary is Shot's CLI.

Building

$ mix escript.build
Generated escript shot_tx

Usage

$ ./shot_tx [OPTIONS] <INPUT>

<INPUT> is either the path to a TPTP .p problem file or an inline problem string. An inline string may be a full TPTP problem (thf(...). declarations, optionally with include/1 directives — set $TPTP_ROOT) or a single THF formula (in which case the conjecture-only fragment is proved with no axioms).

A leading dash reads the problem from standard input.

Output modes

By default, the CLI prints a short human-readable line:

$ ./shot_tx problem.p
THM

With --szs, the output follows the SZS ontology (Sutcliffe 2008) that every mainstream automated theorem prover emits:

$ ./shot_tx --szs problem.p
% SZS status Theorem for problem.p

Status map

Options

All prover knobs described in ShotTx.Data.Parameters are exposed as long flags in kebab-case; e.g. --initial-gamma-limit 3 sets :initial_gamma_limit. Booleans support the --flag / --no-flag form.

Common flags:

• --szs — emit SZS-ontology status line.
• --sat — treat the input as a satisfiability check

                        (do not negate a conclusion).

• -t, --timeout MS — wall-clock limit in milliseconds.
• --proof — print the reconstructed proof tree.
• --stats — print search statistics after the result.
• -v, --verbose — enable prover debug logging on stderr.
• -V, --version — print the version and exit.
• -h, --help — show a compact help message.

TPTP_ROOT fallback

If the positional argument looks like a file path (contains / or ends in .p, .thf, .tptp, or .ax) and no such file exists locally, the CLI retries the lookup relative to the TPTP_ROOT environment variable. This lets you invoke problems by their canonical TPTP name — e.g.

$ TPTP_ROOT=/opt/TPTP shot_tx --szs Problems/PUZ/PUZ001+1.p

Exit codes

The escript returns 0 when the prover produces a definite verdict (theorem or countermodel), 1 for unknown/timeout, and 2 for any input or parsing error.