least a branch of the tableau. This can be done by using a variable instead of a term, so that generates , and then allowing substitutions to later replace with a term. The rule for universal quantifiers becomes: where is a variable not occurring everywhere else in the tableau While the initial set of formulae is supposed not to contain free variables, a formula of the tableau may contain the free variables generated by this rule. These free variables are implicitly considered universally quantified. This rule employs a variable instead of a ground term. What is gained by this change is that these variables can be then given a value when a branch of the tableau can be closed, solving the problem of generating terms that might be useless. {| |- | | if is the most general unifier of two literals and , where and the negation of occur in the same branch of the tableau, can be applied at the same time to all formulae of the tableau |} As an example, can be proved unsatisfiable by first generating ; the negation of this literal is unifiable with , the most general unifier being the substitution that replaces with ; applying this substitution results in replacing with , which closes the tableau. This rule closes at least a branch of the tableau—the one containing the considered pair of literals. However, the substitution has to be applied to the whole tableau, not only on these two literals. This is expressed by saying that the free variables of the tableau are rigid: if an occurrence of a variable is replaced by something else, all other occurrences of the same variable must be replaced in the same way. Formally, the free variables are (implicitly) universally quantified and all formulae of the tableau are within the scope of these quantifiers. Existential quantifiers are dealt with by Skolemization. Contrary to the tableau without unification, Skolem terms may not be simple constants. Indeed, formulae in a tableau with unification may contain free variables, which are implicitly considered universally quantified. As a result, a formula like may be within the scope of universal quantifiers; if this is the case, the Skolem term is not a simple constant but a term made of a new function symbol and the free variables of the formula. where is a new function symbol and the free variables of This