ask may be cited by
usage: ask [OPTIONS] <file with one formula> [<output file>]
Apply a Skolemization transformation to the input file.
It is assumed that bound variables are named apart, and that there are no free variables.
<file with one formula> can be either a file name or '-' (without parentheses) for stdin.
If <output file> is specified, write result to <output file>, otherwise to stdout.
If no options are provided, all the existentials in the formula are Skolemized,
using some fixed symbol suffixed with _NN, NN=00-99.
If only -s is provided and <Skolem symbol to use> is of the form
<something>_NN, Skolemize all the existentials in the formula, using
the symbol <something> replacing NN with 00-99.
If only -s is provided and <Skolem symbol to use> is not of the form
<something>_NN, Skolemize the leftmost existentially quantified variable
in the formula, using the <Skolem symbol to use>.
If only -v is provided, Skolemize the <variable to Skolemize>, using
some fixed symbol suffixed with _00.
If both -s and -v are provided, Skolemize the <variable to Skolemize> using
the symbol <Skolem symbol to use>.
If -e is specified, also output the equality between the Skolem term and
an epsilon term.
Options:
-v <variable to Skolemize>
The existential variable to Skolemize.
-s <Skolem symbol to use>
The Skolem symbol base name to use for the Skolemization symbols.
Defaults to "aSk" if omitted.
-e Output a choice term for the Skolem term.
--no-tstp
Disable TSTP-compatible output: The output in <output file> (or stdout) will
not start with a SZS status value and the output will not be wrapped within
SZS BEGIN and SZS END block delimiters.
--version
Prints the version number of the executable and terminates.
--help
Prints this description and terminates.```