Issue finding the models of a formula using semantic tableux method. Using semantic tableux method, decide what kind of formula U is. If it is consistent, find its models.
U = (p V q → r) → (p V r → q).

This is the semantic tableux I got, is it correct?
DNF(U) = ( ¬ r ^ p) V (¬ r ^ q) V ( ¬ p ^ q) V ( ¬ r ^ q) by absorption law
≡ ( ¬ r ^ p) V (¬ r ^ q) V ( ¬ p ^ q)
Is it correct so far? Then how do I find its models?
 A: Yes, your tableaux is correct.
To find a model, simply take any open branch and see what literals (atomic statements or negations of atomic statements) you find on that branch.
For example, the right most branch contains $q$ as a literal, meaning that you have model by setting $q$ to true ... apparently it does not matter whether $p$ and $r$ are true of false: as soon as $q$ is true, the original sentence is true as well (it's always good to verify that fact ... if you find that this is not the case, then you know something went wrong with your tableaux)
A: Your tableau is correct, though I don't understand why afterwards you compute the DNF (is this asked in the question?).
To construct a model from an open branch, define the valuation such that it assigns all unnegated propositional variables on the branch $\text{True}$ and all negated propositoinal variables on the branch $\text{False}$. For example, for the formula $p \to (q \lor r) \land (q \to \neg r)$:

Since not all propositional variables always occur on an open branch, the resulting models may be partial models, meaning that some variables remain unspecified. In this case their truth value does not matter, so you can extend the partial model to a full model by adding arbitrary truth value assignments for the undefined variables. For instance, from $\mathcal{S}_{10}$ above you can obtain two total models by defining $\mathcal{V}_{10.1} : p \mapsto 1, q \mapsto 0, r \mapsto 1$ and $\mathcal{V}_{10.2} : p \mapsto 0, q \mapsto 0, r \mapsto 1$ respectively.
