8.1.7 Another Example
A second example of the tableaux implementation.
Suppose we are falsifying the formula:
We will abbreviate this formula as 
. Notice that the main connective of this formula is a conjunction and the first conjunct is exactly the same formula as in the last example. Expanding this conjunction (under negative polarity - we said that we want to falsify the formula) leads to the following branching tableaux and computation tree:
A Branching
The tableaux has two branches according to our rule 
. The left one is exactly as in our last example and will end up closed. The computation tree also branches, and here again the left branch is as in our last example and will end in a fail. But why does the computation tree branch? Look at the clauses of tabl/3: There are two clauses that match for a negative conjunction. One leads to a recursive call on the left subformula, the other to a recursive call on the right one. The two branches of the computation tree correspond to these two matching clauses.
Backtracking and Computation Trees
The branches of the computation tree are visited from left to right. After a while the fail on the left branch is reached (i.e. the left branch of our tableaux closes). As we know, fail triggers backtracking. On our computation tree, this means that Prolog goes upward from the fail to the next branching point above, and chooses the next branch to the right to continue its computation. The branch to the left is discarded (and so are all instantiations that took place below the branching point).
Hence the right conjunct of our original input formula is further expanded, adding to the right branch of the tableaux. Finally, when the right conjunct is fully broken down into literals, the top-level output argument Out is instantiated to [true(R), true(S)].
What is the result?
Now we know that our input formula is no theorem. Moreover, we have generated a (in fact the) counter example in OutBranch: If customer(mary) and customer(john) are true, the whole input formula is false.