Definition
Open Branch (First-Order Tableaux)
A branch in a first-order tableau is open when it is complete (no further rules can be applied) and contains no pair
and for the same formula . An open branch certifies that the initial formula is satisfiable.