Skip to main content

Proof Search Visualization

Run Vampire in manual clause-selection mode and explore the evolving clause graph.
Click a node to select the next clause.

Layout
NewActivePassiveSelectedSubsumedNegated conjecture
Awaiting run
Idle

Tip: Use --show_everything on for the fullest clause stream.

Tip: Remove --manual_cs on to let Vampire select clauses automatically.

Ready.
You can double‑click a passive clause node or type an id to answer the prompt.