 In our example, all the leaves in the proof tree are labeled with axioms. This establishes the validity of Γ → ∃xR(x) and, hence, the fact that Γ ⊨ ∃xR(x). LK takes an indirect approach at proving the conclusion and this is an important difference between LK and NK. While NK constructs an actual proof (of the conclusion from the given assumptions), LK instead constructs a proof that proves the existence of a proof (of the conclusion from the assumptions). For instance, to prove that α is entailed by Γ, NK constructs a step-by-step proof of α from Γ (assuming that one exists); in contrast, LK first constructs the sequent Γ → α which then attempts to prove valid by showing that it cannot be made false. This is done by searching for a counterexample that makes (all the sentences in) Γ true and makes α false: If the search fails then a counterexample does not exist and the sequent is therefore valid. In this respect, proof trees in LK are actually refutation proofs. Like resolution, LK is refutation complete: If Γ ⊨ α then the sequent Γ → α has a proof tree.