### Example Shell Command for Transformation

Source: https://github.com/vprover/vampire/wiki/Transforming-Vampire-proofs-with-Prolog

This command demonstrates how to pipe Vampire's TSTP output to the custom Prolog transformation script. It shows the resulting inference graph output.

```shell
$ vampire Problems/PUZ/PUZ001+1.p -p tptp | swipl transform.prolog
f15 by negated_conjecture [f14]
f16 by flattening [f15]
f17 by ennf_transformation [f5]
f18 by flattening [f17]
f19 by ennf_transformation [f6]
f20 by ennf_transformation [f7]
f21 by ennf_transformation [f8]
f22 by ennf_transformation [f9]
f23 by ennf_transformation [f10]
f24 by ennf_transformation [f11]
f26 by skolemisation [f1,f25]
f28 by skolemisation [f12,f27]
f29 by cnf_transformation [f26]
f30 by cnf_transformation [f26]
f34 by cnf_transformation [f18]
f35 by cnf_transformation [f19]
f36 by cnf_transformation [f20]
f37 by cnf_transformation [f21]
f38 by cnf_transformation [f22]
f39 by cnf_transformation [f23]
f40 by cnf_transformation [f24]
f41 by cnf_transformation [f28]
f42 by cnf_transformation [f13]

```

--------------------------------

### Example of Bypassing Allocator in a Function

Source: https://github.com/vprover/vampire/wiki/Allocation

Demonstrates the use of BYPASSING_ALLOCATOR within a function to allow calls to system's new/delete for types that cannot be registered with Vampire's allocator. This is particularly useful for external or STL classes.

```cpp
bool System::fileExists(vstring fname)
{
  CALL("System::fileExists");
  BYPASSING_ALLOCATOR;

  ifstream ifile(fname.c_str());
  return ifile;
}
```

--------------------------------

### Displaying Available Options

Source: https://context7.com/vprover/vampire/llms.txt

Explore Vampire's extensive configuration options using `--show_options` and `--show_experimental_options`. Specific options can be explained with `--explain_option`.

```shell
# Show all standard options
$ vampire --show_options on
```

```shell
# Show experimental/unstable options too
$ vampire --show_experimental_options on
```

```shell
# Explain a single specific option
$ vampire --explain_option literal_comparison_mode
```

```shell
# Print all built-in theory axioms Vampire may use
$ vampire --print_all_theory_axioms on
```

--------------------------------

### Create a New Unit Test File

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

Steps to create a new unit test file by copying an existing one, updating CMakeLists.txt, and writing the test code.

```bash
# choose a name
MY_TEST_NAME=...

# create test file
cp UnitTests/tSyntaxSugar.cpp UnitTests/t${MY_TEST_NAME}.cpp

# alter CMakeLists.txt
sed -e "{/tSyntaxSugar.cpp/p;s/tSyntaxSugar.cpp/t${MY_TEST_NAME}.cpp/;}" \
    -i '' CMakeLists.txt

# write the unit test
vim UnitTests/t${MY_TEST_NAME}.cpp
```

--------------------------------

### Create a New Unit Test File

Source: https://context7.com/vprover/vampire/llms.txt

Demonstrates the initial steps for creating a new unit test by copying an existing file and outlining the necessary CMake and C++ modifications.

```cpp
// UnitTests/tMyFeature.cpp
#include "Test/UnitTesting.hpp"
#include "Test/SyntaxSugar.hpp"
#include "Test/GenerationTester.hpp"
#include "Inferences/BinaryResolution.hpp"

using namespace Test;

#define MY_SYNTAX_SUGAR          \
  DECL_DEFAULT_VARS              \
  DECL_SORT(s)                   \
  DECL_FUNC(f, {s, s}, s)        \
  DECL_CONST(a, s)               \
  DECL_PRED(p, {s})              \
  DECL_PRED(q, {s})

// Test that binary resolution produces the expected resolvent
TEST_GENERATION(resolution_basic, 
    Generation::SymmetricTest()
      .inputs({
        clause({ selected(p(x)), f(x,y) == x }),
        clause({ selected(~p(a)),  ~q(a) })
      })
      .expected(exactly(clause({ f(a,y) == a, ~q(a) })))
    )

// Test that resolution is not applied to equalities
TEST_GENERATION(resolution_no_eq, 
    Generation::SymmetricTest()
      .inputs({
        clause({ selected(a == x) }),
        clause({ selected(a != x) })
      })
      .expected(none())
    )

// Simple assertion-based test
TEST_FUN(arithmetic_literal) {
  NUMBER_SUGAR(Real)
  DECL_DEFAULT_VARS
  // Build ~(0 < x * 3.5)
  Literal* lit = ~(num(0) < (x * frac(7, 2)));
  ASS(lit != nullptr);
}

```

--------------------------------

### Choosing a Saturation Algorithm

Source: https://context7.com/vprover/vampire/llms.txt

Select the core proof-finding strategy by specifying the saturation algorithm. Options include LRS (default), Otter, DISCOUNT, and FMB for satisfiable problems.

```shell
# LRS (Limited Resource Strategy) — default
$ vampire --saturation_algorithm lrs problem.p
```

```shell
# Otter loop
$ vampire --saturation_algorithm otter problem.p
```

```shell
# DISCOUNT loop
$ vampire --saturation_algorithm discount problem.p
```

```shell
# Finite Model Building (for satisfiable problems)
$ vampire --mode vampire --saturation_algorithm fmb problem.p
```

--------------------------------

### Show All Vampire Options

Source: https://github.com/vprover/vampire/blob/master/README.md

Displays a comprehensive list of all available command-line options for Vampire. Run this command to explore the full range of configurations.

```shell
$ vampire --show_options on
```

--------------------------------

### Run Vampire with Options

Source: https://github.com/vprover/vampire/wiki/Cygwin

Execute the Vampire program with the '--show_options on' flag to display available options. The '.exe' extension can be omitted when running from the command line.

```bash
./vampire_rel.exe --show_options on
```

--------------------------------

### Basic TPTP Problem Proof

Source: https://context7.com/vprover/vampire/llms.txt

Run Vampire on a TPTP file with the default 60-second time limit. Outputs an SZS status and, if successful, the proof.

```shell
# Prove a first-order problem in TPTP FOF/CNF format (default mode, 60s limit)
$ vampire problem.p

% Running Vampire on problem.p
% SZS status Theorem for problem.p
% SZS output start Proof for problem.p
fof(f1, axiom, (![X]: (p(X) => q(X)))).
...
% SZS output end Proof for problem.p
```

--------------------------------

### Configure Vampire Build with CMake

Source: https://github.com/vprover/vampire/wiki/Cygwin

Run CMake to configure the build process for Vampire. Ignore potential warnings about missing Z3 or Git repository status.

```bash
cmake ..
```

--------------------------------

### Configure and Build Vampire

Source: https://github.com/vprover/vampire/wiki/Source-Build-for-Users

Standard build process for Vampire on UNIX-like systems. Ensure you are in the source directory, create a build directory, configure with CMake, and then build with make.

```shell
cd vampire
# make a fresh directory for the build files
mkdir build && cd build

# configure and generate build files
cmake ..
-- The C compiler identification is GNU 9.3.0
-- The CXX compiler identification is GNU 9.3.0
<snip>
-- Configuring done
-- Generating done
-- Build files have been written to: /tmp/build

# build Vampire
make
<snip>

# You now have a Vampire binary
$
```

--------------------------------

### Compile Vampire using Make

Source: https://github.com/vprover/vampire/wiki/Cygwin

Execute the 'make' command to compile all Vampire source files and link them into an executable. This process can take a significant amount of time.

```bash
make
```

--------------------------------

### List Available Test Cases with vtest

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

List all available test units and test cases using the vtest command.

```bash
./vtest ls
```

--------------------------------

### Configure and Build Z3 Library

Source: https://github.com/vprover/vampire/wiki/Source-Build-for-Users

Steps to build a single-threaded release version of the Z3 library. This is an optional step for integrating Z3 with Vampire. Refer to z3/README-CMake.md for Z3-specific build details.

```shell
cd vampire
# check out a specific version of Z3
git submodule update --init
cd z3

# following is a Z3 build - refer to z3/README-CMake.md
mkdir z3/build && cd z3/build
# configure single-threaded Z3 release build
cmake .. -DZ3_SINGLE_THREADED=1 -DCMAKE_BUILD_TYPE=Release
<snip>

# build Z3
make
<snip>

# you should now have some libz3.* files in z3/build
$
```

--------------------------------

### Navigate to Vampire Executable Directory

Source: https://github.com/vprover/vampire/wiki/Cygwin

Change the current directory to the 'bin' subdirectory within the Vampire build directory to access the executable.

```bash
cd "D:\ProgMesProg\vampire\CMAKE-build\bin"
```

--------------------------------

### Build with Z3 Support

Source: https://context7.com/vprover/vampire/llms.txt

Compiles Vampire with Z3 theorem prover support. This involves updating Git submodules, configuring Z3 separately, and then configuring Vampire to detect the Z3 build.

```shell
cd vampire
git submodule update --init
cd z3 && mkdir build && cd build
cmake .. -DZ3_SINGLE_THREADED=1 -DCMAKE_BUILD_TYPE=Release
make
cd ../../build
cmake ..   # CMake auto-detects z3/build
make
```

--------------------------------

### Run Vampire in Default Mode

Source: https://github.com/vprover/vampire/blob/master/README.md

Saves the problem in TPTP format and runs Vampire with a 60-second time limit. Ensure the problem file is in TPTP format.

```shell
$ vampire problem.p
```

--------------------------------

### Random Strategy Sampling on FOL Problems

Source: https://context7.com/vprover/vampire/llms.txt

Executes Vampire with random strategy sampling for First-Order Logic (FOL) problems. Requires a sampler file.

```shell
$ ls samplers/
samplerFOL.txt  samplerIND.txt  samplerSMT.txt

# Run Vampire with random strategy sampling (FOL)
$ vampire --sample_strategy samplers/samplerFOL.txt \
          --random_seed 42 \
          Problems/FOF/ALG001+1.p
```

--------------------------------

### Vampire Portfolio Mode Shortcut

Source: https://github.com/vprover/vampire/blob/master/README.md

This command demonstrates that the `--mode casc` option is a shortcut for a more explicit combination of portfolio mode, schedule, and proof output format.

```shell
$ vampire --mode portfolio --schedule casc --proof tptp
```

--------------------------------

### Standard Vampire Build

Source: https://context7.com/vprover/vampire/llms.txt

Builds Vampire in release mode without Z3 support. The executable is produced at ./vampire.

```shell
cd vampire
mkdir build && cd build
cmake ..
make
```

--------------------------------

### Finite Model Building (FMB)

Source: https://context7.com/vprover/vampire/llms.txt

Use FMB to search for finite models by encoding domain sizes as SAT problems. Options include sort inference and limiting model size.

```shellsession
# Run FMB to find a finite model
$ vampire --mode vampire --saturation_algorithm fmb problem.p
% SZS status Satisfiable for problem.p
% SZS output start FiniteModel for problem.p
tff(domain, fi_domain, ...).
...
% SZS output end FiniteModel for problem.p
```

```shellsession
# FMB with sort inference for multi-sorted problems
$ vampire --saturation_algorithm fmb --fmb_sort_inference mono problem.p
```

```shellsession
# Limit FMB to models of size at most 10
$ vampire --saturation_algorithm fmb --fmb_size_weight_ratio 1 problem.p
```

--------------------------------

### Transform TSTP Proofs with Prolog

Source: https://context7.com/vprover/vampire/llms.txt

Produce a TPTP/TSTP proof and pipe it to SWI-Prolog for transformation. The provided Prolog script 'transform.prolog' can print the inference graph of a TSTP proof.

```shellsession
# Produce a TPTP/TSTP proof
$ vampire --proof tptp Problems/PUZ/PUZ001+1.p -p tptp | swipl transform.prolog
```

```prolog
% transform.prolog — print the inference graph of a TSTP proof
:- consult(tptp).  % load TPTP operator definitions

output(fof(Name, _, _, inference(Inference, _, Parents))) :-
  format("~w by ~w ~w\n", [Name, Inference, Parents]),
  main.
output(_).

process(end_of_file) :- !.
process(Input) :-
  output(Input),
  main.

main :- 
  read(Input),
  process(Input).

:- initialization(main, main).

% Example output:
% f15 by negated_conjecture [f14]
% f16 by flattening [f15]
% f26 by skolemisation [f1,f25]
% f29 by cnf_transformation [f26]
% f44 by resolution [f35,f30]
% f66 by avatar_split_clause [f53,f63,f59,f55]
% f97 by avatar_sat_refutation [f66,f71,f83,f96]
```

--------------------------------

### Static Binary Build

Source: https://context7.com/vprover/vampire/llms.txt

Builds a static binary, meaning it will not depend on shared libraries. This is useful for deployment in environments with limited library availability.

```shell
cmake -DBUILD_SHARED_LIBS=0 ..
make
```

--------------------------------

### Using Vampire's String Alternatives

Source: https://github.com/vprover/vampire/wiki/Allocation

Replace standard library string types (string, ostringstream, istringstream, stringstream) with Vampire's equivalents (vstring, vostringstream, vistringstream, vstringstream) to ensure they are managed by the allocator.

```cpp
#include <Lib/VString.hpp>
```

--------------------------------

### Setting Time and Memory Limits

Source: https://context7.com/vprover/vampire/llms.txt

Configure resource limits for Vampire runs, including time (seconds), memory (GB), and instruction counts. Can also utilize all available CPU cores or a specified number for portfolio workers.

```shell
# 300-second time limit, 4 GB memory limit
$ vampire --time_limit 300 --memory_limit 4096 problem.p
```

```shell
# Instruction-count limit (portable, machine-independent)
$ vampire --instruction_limit 1000 problem.p
```

```shell
# Use all available CPU cores for portfolio workers
$ vampire --mode portfolio --schedule casc --multicore 0 problem.p
```

```shell
# Specify exact number of portfolio workers
$ vampire --mode portfolio --schedule casc --multicore 8 problem.p
```

--------------------------------

### Build and Run All Unit Tests

Source: https://context7.com/vprover/vampire/llms.txt

Compiles Vampire in Debug mode and then executes all unit tests using CTest. The --output-on-failure flag shows test output only for failing tests.

```shell
mkdir cmake-build && cd cmake-build
cmake -DCMAKE_BUILD_TYPE=Debug ..
make
ctest --output-on-failure
```

--------------------------------

### Interactive Metamode Commands

Source: https://context7.com/vprover/vampire/llms.txt

Enable interactive mode for incrementally loading axioms and running strategies without re-parsing. Available commands include load, tptp, smt2, list, run, pop, and exit.

```shellsession
$ vampire --interactive on
```

```shellsession
# Commands available in the interactive REPL:
load axioms.p                          # load a TPTP file into the problem
tptp fof(ax,axiom,p(a)).               # add a single TPTP formula
smt2 (assert (p a))                    # add a single SMT-LIB 2 assertion
list                                   # list all loaded pieces
run --time_limit 30 conjecture.p       # run a strategy (in a child process)
pop 1                                  # remove the last loaded piece
exit                                   # quit
```

--------------------------------

### Vampire Portfolio (CASC) Modes

Source: https://context7.com/vprover/vampire/llms.txt

Utilize portfolio mode for enhanced performance on hard problems by trying multiple strategies. Supports theorem-proving and model-finding scenarios, as well as SMT-COMP mode for SMT-LIB 2 input.

```shell
# CASC mode: portfolio for unsatisfiable (theorem-proving) problems
$ vampire --mode casc problem.p
```

```shell
# Equivalent explicit form:
$ vampire --mode portfolio --schedule casc --proof tptp problem.p
```

```shell
# For problems expected to be satisfiable (model-finding):
$ vampire --mode casc_sat problem.p
```

```shell
# SMT-COMP mode: reads SMT-LIB 2 input, uses SMT-COMP schedule
$ vampire --mode smtcomp problem.smt2
```

--------------------------------

### Run Vampire in Portfolio Mode

Source: https://github.com/vprover/vampire/blob/master/README.md

Executes Vampire using a portfolio of strategies, which often yields better performance than the default mode. This mode tries various strategies to solve the problem.

```shell
$ vampire --mode casc problem.p
```

--------------------------------

### Input Syntax Selection

Source: https://context7.com/vprover/vampire/llms.txt

Specify the input file format. Vampire supports auto-detection (default), explicit TPTP, and SMT-LIB 2. Input can also be read from standard input.

```shell
# Auto-detect input syntax (default)
$ vampire --input_syntax auto problem.p
```

```shell
# Explicitly select TPTP
$ vampire --input_syntax tptp problem.p
```

```shell
# SMT-LIB 2 input
$ vampire --input_syntax smtlib2 problem.smt2
```

```shell
# Read from standard input
$ echo 'fof(ax,axiom,p(a)). fof(conj,conjecture,p(a)).' | vampire --input_syntax tptp
```

--------------------------------

### Registering a Class with Vampire Allocator

Source: https://github.com/vprover/vampire/wiki/Allocation

Decorate the class definition with CLASS_NAME and USE_ALLOCATOR macros to register it with Vampire's custom allocator. This ensures all its allocations are managed by the allocator.

```cpp
CLASS_NAME(XXX);
USE_ALLOCATOR(XXX);
```

--------------------------------

### Navigate to Build Directory in Cygwin

Source: https://github.com/vprover/vampire/wiki/Cygwin

Change the current directory to the Vampire build directory within a Cygwin terminal.

```bash
cd "D:\ProgMesProg\vampire\CMAKE-build"
```

--------------------------------

### Axiom Selection with SInE

Source: https://context7.com/vprover/vampire/llms.txt

Select relevant axioms using SInE with specified depth and tolerance. This mode is crucial for large-theory problems. It can also be used during normal proving.

```shellsession
# Select relevant axioms using SInE and output them
$ vampire --mode axiom_selection \
          --sine_selection axioms \
          --sine_depth 3 \
          --sine_tolerance 1.5 \
          large_theory_problem.p
```

```shellsession
# Use SInE selection during normal proving
$ vampire --sine_selection axioms --sine_depth 2 problem.p
```

--------------------------------

### Run Vampire in Satisfiable Mode

Source: https://github.com/vprover/vampire/blob/master/README.md

Utilizes a set of strategies optimized for satisfiable problems. Use this mode when you suspect the problem is satisfiable.

```shell
$ vampire --mode casc_sat problem.p
```

--------------------------------

### Proof Output Formats

Source: https://context7.com/vprover/vampire/llms.txt

Control the format of the proof output. Options include TPTP/TSTP (default for CASC), a compact internal format, or disabling proof output entirely. SZS-compliant output with TPTP proof is also supported.

```shell
# Output proof in TPTP/TSTP format (default for CASC mode)
$ vampire --proof tptp problem.p
```

```shell
# Suppress proof output entirely
$ vampire --proof off problem.p
```

```shell
# Output proof in a compact internal format
$ vampire --proof on problem.p
```

```shell
# SZS-compliant output with TPTP proof
$ vampire --output_mode szs --proof tptp problem.p
```

--------------------------------

### Batch Fuzz-Testing with GNU Parallel

Source: https://context7.com/vprover/vampire/llms.txt

Performs batch fuzz-testing using GNU Parallel to find crashes or errors. It pipes problem files to `parallel` and filters the output for specific error patterns.

```shell
$ find TPTP/Problems/FOF -name '*.p' | \
  parallel vampire --sample_strategy samplers/samplerFOL.txt \
                   --instruction_limit 500 \
                   --random_seed {%} {} 2>&1 | \
  grep -E 'viola|SIG|error'
```

--------------------------------

### Output CNF clauses with Clausify Mode

Source: https://context7.com/vprover/vampire/llms.txt

Use --mode clausify to output CNF clauses of the preprocessed problem. For theory axioms, use --mode tclausify. Use --mode preprocess to preprocess only, or --mode preprocess2 for preprocessing with simplification.

```shellsession
# Output CNF clauses of the preprocessed problem
$ vampire --mode clausify problem.p
% fof(ax1,axiom,...).
cnf(c1,axiom,(p(X) | ~q(X))).
...
```

```shellsession
# Output with theory axioms included (tclausify)
$ vampire --mode tclausify problem.p
```

```shellsession
# Preprocess only (no clausification, keep FOF)
$ vampire --mode preprocess problem.p
```

```shellsession
# Preprocess2: preprocess with simplification step
$ vampire --mode preprocess2 problem.p
```

--------------------------------

### Custom Prolog Transformation for TSTP Proofs

Source: https://github.com/vprover/vampire/wiki/Transforming-Vampire-proofs-with-Prolog

This Prolog code defines a custom transformation for TSTP proofs. It imports operators from 'tptp.prolog', defines an 'output' predicate to process and print inference steps, and a 'main' predicate to read and process inputs until end-of-file. Use this as 'transform.prolog'.

```prolog
% import operators from Geoff
:- consult(tptp).

% this is our transform - anything you like
% here we are ignoring any non-FOF input and just printing the inference graph
output(fof(Name, _, _, inference(Inference, _, Parents))) :-
  format("~w by ~w ~w\n", [Name, Inference, Parents]),
  main.
output(_).

% this predicate keeps reading inputs and producing the corresponding output until EOF
process(end_of_file) :- !.
process(Input) :-
  output(Input),
  main.

% this is the entry point
main :-
  % magic happens here: each line of a TSTP proof can be parsed with read/1
  read(Input),
  % once read, the line is just a Prolog term and can be manipulated as usual
  process(Input).

% tell the runtime that this is the entry point
:-initialization(main, main).

```

--------------------------------

### Check Exit Code for Success

Source: https://context7.com/vprover/vampire/llms.txt

Demonstrates how to check the exit status of a Vampire run. An exit code of 0 indicates success (refutation found or satisfiability established).

```shell
# Exit 0  → Success: refutation found or satisfiability established
$ vampire problem.p; echo $?
```

--------------------------------

### Debug Build for Unit Tests and Assertions

Source: https://context7.com/vprover/vampire/llms.txt

Enables debug symbols, unit tests, and assertions. Use this configuration for development and testing.

```shell
cmake -DCMAKE_BUILD_TYPE=Debug ..
make
```

--------------------------------

### Run Vampire on a Problem File

Source: https://github.com/vprover/vampire/wiki/Cygwin

Execute Vampire on a specified problem file (e.g., 'problem.fof') located in the same directory as the executable. The executable can be moved to other directories.

```bash
./vampire_rel problem.fof
```

--------------------------------

### Random Sampling with Internal Options and Instruction Limit

Source: https://context7.com/vprover/vampire/llms.txt

Runs Vampire with random strategy sampling, randomized internal options, and a specified instruction limit. A different random seed is used.

```shell
$ vampire --sample_strategy samplers/samplerFOL.txt \
          -si on -rtra on \
          --random_seed 7 \
          --instruction_limit 1000 \
          problem.p
```

--------------------------------

### Code Coverage Build

Source: https://context7.com/vprover/vampire/llms.txt

Configures and builds Vampire with code coverage instrumentation enabled. Requires a Debug build type.

```shell
cmake -DCMAKE_BUILD_TYPE=Debug -DCOVERAGE=ON ..
make
```

--------------------------------

### Output Mode: Re-print in TPTP Format

Source: https://context7.com/vprover/vampire/llms.txt

Uses the 'output' mode to parse an input file (e.g., SMT-LIB 2) and re-print it in TPTP format. Useful for syntax conversion.

```shell
$ vampire --mode output --input_syntax smtlib2 problem.smt2
```

--------------------------------

### Include Unit Testing Header

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

Include the necessary header file for unit testing in C++ test files.

```cpp
#include "Test/UnitTesting.hpp"
```

--------------------------------

### Run a Single Test Case with vtest

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

Execute a specific test case from a unit test without launching a separate process, useful for debugging with tools like lldb.

```bash
mkdir cmake-build
cd cmake-build
cmake ..
make 
./vtest run <unit_id> <test_case>
```

--------------------------------

### Encode and Decode Vampire Strategies

Source: https://context7.com/vprover/vampire/llms.txt

Encode current options as a compact strategy string or decode a strategy string to run it. Options can also be read from a semicolon-separated string.

```shellsession
# Encode current options as a strategy string
$ vampire --encode_strategy on --saturation_algorithm lrs \
          --literal_comparison_mode predicate \
          --symbol_precedence occurrence \
          problem.p
# Output: lrs+1_10_lcm=predicate:sp=occurrence_60
```

```shellsession
# Decode and run a strategy string
$ vampire --decode lrs+1_10_lcm=predicate:sp=occurrence_60 problem.p
```

```shellsession
# Read options from a string (semicolon-separated key=value)
$ vampire --read_options "saturation_algorithm=otter;time_limit=10" problem.p
```

--------------------------------

### Profile Mode: Classify Problem

Source: https://context7.com/vprover/vampire/llms.txt

Uses the 'profile' mode to analyze a problem file and output its TPTP category, properties bitmask, and atom count. This mode does not attempt to solve the problem.

```shell
$ vampire --mode profile problem.p
# Output: FOF 1234 56   (category, props bitmask, atom count)
```

--------------------------------

### Model Check Mode: Verify a Model

Source: https://context7.com/vprover/vampire/llms.txt

Uses the 'model_check' mode to verify a proposed model against the axioms of a given problem. This mode checks satisfiability with respect to the provided model.

```shell
$ vampire --mode model_check problem_with_model.p
```

--------------------------------

### Compile and Run Unit Tests with CTest

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

Compile unit tests in Debug mode and run them using CTest. Ensure tests are compiled in Debug mode for CTest execution.

```bash
mkdir cmake-build
cd cmake-build 
cmake -DCMAKE_BUILD_TYPE=Debug ..
make 
ctest --output-on-failure
```

--------------------------------

### Run Unit Tests Matching a Pattern

Source: https://context7.com/vprover/vampire/llms.txt

Filters and runs unit tests whose names match the provided regular expression. Use -R for inclusion.

```shell
ctest -R "BinaryResolution" --output-on-failure
```

--------------------------------

### Add Linker Flags in CMakeLists.txt

Source: https://github.com/vprover/vampire/wiki/Cygwin

Add these lines to D:\ProgMesProg\vampire\CMakeLists.txt to resolve linker errors related to multiple symbol definitions. It's suggested to add them around line 10, after the includes.

```cmake
set(CMAKE_MODULE_LINKER_FLAGS -Wl,--allow-multiple-definition)
set(CMAKE_EXE_LINKER_FLAGS -Wl,--allow-multiple-definition)
set(CMAKE_STATIC_LINKER_FLAGS -Wl,--allow-multiple-definition)
```

--------------------------------

### Define a Test Function

Source: https://github.com/vprover/vampire/wiki/Testing-with-CTest-and-vtest

Define a test function using the TEST_FUN macro for unit tests. Test functions are run as separate processes.

```cpp
TEST_FUN(<test_name>) {
  /* testing code goes here */
}
```

--------------------------------

### Check Exit Code for Failure

Source: https://context7.com/vprover/vampire/llms.txt

Illustrates that a non-zero exit code signifies a failure in Vampire's execution, such as time limits, memory limits, interruptions, or exceptions. Lists common non-zero status codes.

```shell
# Non-zero → Failure: time limit, memory limit, unknown, interrupted, or exception
# Typical non-zero codes (see Lib/System.hpp):
#   VAMP_RESULT_STATUS_UNKNOWN            (no conclusion reached)
#   VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION
#   VAMP_RESULT_STATUS_INTERRUPTED
#   VAMP_RESULT_STATUS_OTHER_SIGNAL
```

--------------------------------

### Check SZS Status in Vampire Output

Source: https://context7.com/vprover/vampire/llms.txt

Use this command to filter Vampire's output and specifically check the SZS status, which helps distinguish between a theorem being proven and a problem being satisfiable. This is useful for parsing results from automated theorem proving tasks.

```bash
$ vampire --mode casc problem.p | grep "SZS status"
% SZS status Theorem for problem.p
```

--------------------------------

### AVATAR Clause Splitting

Source: https://context7.com/vprover/vampire/llms.txt

Enable or disable AVATAR for coordinating clause splitting with a SAT solver to prune unsatisfiable branches. Specify the SAT solver (e.g., CaDiCaL) or SMT solver (e.g., Z3).

```shellsession
# Enable AVATAR (default: on)
$ vampire --avatar on problem.p
```

```shellsession
# AVATAR with CaDiCaL SAT solver
$ vampire --avatar on --sat_solver cadical problem.p
```

```shellsession
# AVATAR with Z3 SMT solver (requires Z3 build)
$ vampire --avatar on --sat_solver z3 problem.p
```

```shellsession
# Disable AVATAR
$ vampire --avatar off problem.p
```

--------------------------------

### Define TPTP Operators in Prolog

Source: https://github.com/vprover/vampire/wiki/Transforming-Vampire-proofs-with-Prolog

This code defines the operators used by the TPTP format, which are necessary for parsing TPTP/TSTP files in Prolog. Save this as 'tptp.prolog'.

```prolog
%==============================================================================
%----The tptp2X  utility is used  to make transformations on the 
%----clauses in TPTP problem, and to output the clauses in formats 
%----accepted  by existing ATP systems. 
%----
%----Written by Geoff Sutcliffe, July 1992.
%----Updated by Geoff Sutcliffe, November 1992.
%----Updated by Geoff Sutcliffe, March 1993.
%----Revised by Geoff Sutcliffe, January, 1994.
%----Updated by Geoff Sutcliffe, April, 1994.
%----Revised by Geoff Sutcliffe, May-August 1994, with ideas from
%----    Gerd Neugebauer
%----Revised by Geoff Sutcliffe, May, 1995.
%----Extensions for FOF by Geoff Sutcliffe, October 1996.
%==============================================================================
%------------------------------------------------------------------------------
%------------------------------------------------------------------------------
%----These are used in the TPTP and need to exist before the 
%----transformations and formats are loaded. They are also declared at 
%----runtime in tptp2X/4.
:-op(70,fx,'$$').
:-op(80,fx,'$').
:-op(80,fx,'#').
:-op(90,xfx,/).     %----Rationals need to bind tighter than = 
:-op(100,fx,++).
:-op(100,fx,--).
%----Postfix for !=
:-op(100,xf,'!').
%---- .. used for range in tptp2X. Needs to be stronger than : 
:-op(400,xfx,'..').
%----! and ? are of higher precedence than : so ![X]:p(X) is :(![X],p(X))
%----Otherwise ![X]:![Y]:p(X,Y) cannot be parsed.
%----! is fy so Prolog can read !! (blah) as !(!(blah)) and it gets fixed
:-op(400,fy,!).
:-op(400,fx,?).
:-op(400,fx,^).
:-op(400,fx,'!>').
:-op(400,fx,'?*').
:-op(400,fx,'@-').
:-op(400,fx,'@+').
:-op(401,fx,'@@-').
:-op(401,fx,'@@+').
:-op(402,fx,'!!').
:-op(402,fx,'??').
:-op(403,yfx,*).     %----X product
:-op(403,yfx,+).     %----Union
%----= must bind more tightly than : for ! [X] : a = X. = must binder looser
%----than quantifiers for otherwise X = ! [Y] : ... is a syntax error (the =
%----grabs the quantifier). That means for THF it is necessary to bracket 
%----formula terms, e.g., a = (! [X] : p(X))
:-op(405,xfx,'=').
%---!= not possible because ! is special - see postfix cheat :-op(405,xfx,'!=').
:-op(440,xfy,'>').     %----Type arrow
%----Made @ stronger than : for TH1 type construction, e.g., rs: stream @ rule
%----Need : stronger than binary connectives for ! [X] : p(X) <=> !Y ...
%----Need ~ and : equal and right-assoc for ![X] : ~p and for ~![X] : ...
:-op(450,fy,~).      %----Logical negation
:-op(450,xfy, :). 
:-op(501,yfx,@).
:-op(1102,xfy,'|').
:-op(1102,xfx,'~|').
:-op(1103,xfy,'&').
:-op(1103,xfx,'~&').
:-op(1104,xfx,'=>').
:-op(1104,xfx,'<=').
:-op(1105,xfx,'<=>').
:-op(1105,xfx,'<~>').
:-op(1110,xfx,'-->').
:-op(1150,xfx,':=').

```

--------------------------------

### Registering a Class for Array Allocations

Source: https://github.com/vprover/vampire/wiki/Allocation

Use USE_ALLOCATOR_ARRAY for classes where array allocations (new[]) are expected. This is less common than single object allocations.

```cpp
USE_ALLOCATOR_ARRAY(XXX);
```

--------------------------------

### Run a Specific Test Case Directly

Source: https://context7.com/vprover/vampire/llms.txt

Executes a single, named test case using the `vtest` runner. This is particularly useful when attaching a debugger to a specific test.

```shell
./vtest run tInferences_BinaryResolution test01
```