  Many applications of formal methods require automated reasoning about system
properties, such as system safety and security. To improve the performance of
automated reasoning engines, such as SAT/SMT solvers and first-order theorem
prover, it is necessary to understand both the successful and failing attempts
of these engines towards producing formal certificates, such as logical proofs
and/or models. Such an analysis is challenging due to the large number of
logical formulas generated during proof/model search. In this paper we focus on
saturation-based first-order theorem proving and introduce the SATVIS tool for
interactively visualizing saturation-based proof attempts in first-order
theorem proving. We build SATVIS on top of the world-leading theorem prover
VAMPIRE, by interactively visualizing the saturation attempts of VAMPIRE in
SATVIS. Our work combines the automatic layout and visualization of the
derivation graph induced by the saturation attempt with interactive
transformations and search functionality. As a result, we are able to analyze
and debug (failed) proof attempts of VAMPIRE. Thanks to its interactive
visualisation, we believe SATVIS helps both experts and non-experts in theorem
proving to understand first-order proofs and analyze/refine failing proof
attempts of first-order provers.
