to and disregard the case in which it is first applied to . This is a global restriction because what allows neglecting this second expansion is the presence of the other tableau, where expansion is applied to first and afterwards. Clause tableaux When applied to sets of clauses (rather than of arbitrary formulae), tableaux methods allow for a number of efficiency improvements. A first-order clause is a formula that does not contain free variables and such that each is a literal. The universal quantifiers are often omitted for clarity, so that for example actually means . Note that, if taken literally, these two formulae are not the same as for satisfiability: rather, the satisfiability is the same as that of . That free variables are universally quantified is not a consequence of the definition of first-order satisfiability; it is rather used as an implicit common assumption when dealing with clauses. The only expansion rules that are applicable to a clause are and ; these two rules can be replaced by their combination without losing completeness. In particular, the following rule corresponds to applying in sequence the rules and of the first-order calculus with unification. where is obtained by replacing every variable with a new one in When the set to be checked for satisfiability is only composed of clauses, this and the unification rules are sufficient to prove unsatisfiability. In other worlds, the tableau calculi composed of and is complete. Since the clause expansion rule only generates literals and never new clauses, the clauses to which it can be applied are only clauses of the input set. As a result, the clause expansion rule can be further restricted to the case where the clause is in the input set. where is obtained by replacing every variable with a new one in , which is a clause of the input set Since this rule directly exploits the clauses in the input set there is no need to initialize the tableau to the chain of the input clauses. The initial tableau can therefore be initialize with the single node labeled ; this label is often omitted as implicit. As a result of this further simplification, every node of the tableau (apart from the root) is labeled with a literal. A number of optimizations can be used for clause tableau. These optimization are aimed at reducing the number of possible tableaux to be