\documentclass[fleqn]{article}
\usepackage{fullpage,latexsym}
\newenvironment{VampireProof}{%
   \section{Proof}}{}
\newenvironment{VampireInference}{%
   \begin{array}{c}}{\end{array}}
\newenvironment{VampireInferencePremises}{}{}
\newenvironment{VampirePremise}%
   {\begin{array}{l}}%
   {\end{array}}
\newenvironment{VampireConclusion}%
   {\begin{array}{l}}%
   {\end{array}}
\newcommand{\VampireUnit}[3]{%
   #1.~#2~[#3]}
\newcommand{\VPremiseSeparator}{\\}
\newcommand{\VConclusionSeparator}{\\ \hline}
\newcommand{\Vor}{\vee}
\newcommand{\Vand}{\wedge}
\newcommand{\Vimp}{\rightarrow}
\newcommand{\Viff}{\leftrightarrow}
\newcommand{\Vxor}{\not\Viff}
\newcommand{\VEmptyClause}{\Box}
\begin{document}
\begin{VampireProof}
[$12,9\rightarrow 13$, subsumption resolution]\\*[-2ex]
\[\begin{VampireInference}
\begin{VampirePremise}%
~~\mathit{b} \neq \mathit{u}
\end{VampirePremise}
\VPremiseSeparator
\begin{VampirePremise}%
~~\mathit{u} = x_{0}
\end{VampirePremise}
\VConclusionSeparator
\begin{VampireConclusion}
~~\VEmptyClause
\end{VampireConclusion}
\end{VampireInference}
\]
[$2\rightarrow 9$, cnf transformation]\\*[-2ex]
\[\begin{VampireInference}
\begin{VampirePremise}%
~~(\forall x_{0} )\mathit{u} = x_{0}
\end{VampirePremise}
\VConclusionSeparator
\begin{VampireConclusion}
~~\mathit{u} = x_{0}
\end{VampireConclusion}
\end{VampireInference}
\]
[$3\rightarrow 12$, cnf transformation]\\*[-2ex]
\[\begin{VampireInference}
\begin{VampirePremise}%
~~\mathit{a} \neq \mathit{b} \Vand \mathit{a} \neq \mathit{u} \Vand \mathit{b} \neq \mathit{u}
\end{VampirePremise}
\VConclusionSeparator
\begin{VampireConclusion}
~~\mathit{b} \neq \mathit{u}
\end{VampireConclusion}
\end{VampireInference}
\]
[$3$, input]\\*[-2ex]
\[\begin{VampireInference}
\begin{VampireConclusion}
~~\mathit{a} \neq \mathit{b} \Vand \mathit{a} \neq \mathit{u} \Vand \mathit{b} \neq \mathit{u}
\end{VampireConclusion}
\end{VampireInference}
\]
[$2$, input]\\*[-2ex]
\[\begin{VampireInference}
\begin{VampireConclusion}
~~(\forall x_{0} )\mathit{u} = x_{0}
\end{VampireConclusion}
\end{VampireInference}
\]
\end{VampireProof}
\end{document}
