# ebproofs Help: Proving Constructive Dilemma

Okay, I'm trying to prove the constructive dilemma:

\{p\lor q, p\to r, q\to r\} \vdash r


And I was attempting a proof tree for it in ebproofs and it is giving me some problems.

My code looks like this:

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\end{prooftree}


Up to this point it turns out fine. But when I add this:

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\end{prooftree}


I know this is an unfinished proof, but I get a problem here when I try to run the code. Apparently it's a "malformed proof tree".

MT = modus tollens here.

## 1 Answer

Well, never mind. I figured out the problem. Turns out, ebproofs can't seem to run partial proofs. Basically, completing the proof removed the problem I had.

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\Infer{2}[F]{\bot}
\end{prooftree}


So there's that...