How to use a Semantic Tableau to show satisfiable and falsifiable

Question

I'm working on using semantic tableau to prove properties of formulas. I've got the hang of building them, but there's some theory I'm unsure of.

I'm aware that to a formula can be proven unsatisfiable if all branches are closed.

I'm also aware that a formula can be proven valid if the negation of that formula is proven unsatisfiable like done so above.

But how can I prove that a formula is both satisfiable and falsifiable?

I'm sure it can be done by proving that a formula is not unsatisfiable and not valid. But is there a shorter way? Or is it common practice to prove the formula to be both not unsatisfiable and not valid?

Answer 1

This is indeed done by two trees: one where $\phi$ leads to at least one open and finished branch (showing satisfiablity of $\phi$), and one where $\neg \phi$ leads to at least one open and finished branch (showing falsifiablity of $\phi$)