Logical System hausman ∃D. The constant, a, must be new to the branch [here the computer will choose for you] ∀D. Any closed term, stage 1, your choice ∀D. Any closed term, stage 2, a chosen ¬∃D. ¬∀D.