8.1.4 Complex Formulae: Disjunctive Expansion
The clause of the main tableaux predicate for disjunctive expansion.
Let's finally look at conjunctions in a negative context (i.e. disjunctions). Remember that the rule 
introduces a branching. If we find a negated conjunction, we have to falsify either the first or the second conjunct. We express this ``either... or...'' in Prolog by writing two clauses, each of them covering one of the two branches:
tabl(false(A & _),InBranch,H) :-
tabl(false(A),InBranch,H).
tabl(false(_ & B),InBranch,H) :-
!,tabl(false(B),InBranch,H). In the first clause, tabl/3 is called with the first conjunct (signed false) as input. If this call succeeds, everything is fine and we get the resulting open OutBranch as output. Prolog will then simply forget about the second clause (resp. disjunct/branch). Otherwise (i.e. if the first call fails), Prolog backtracks to the next clause in the program, the second clause for negative conjunction. There tabl/3 is called with the second conjunct as input, generating the resulting OutBranch. This corresponds to the second branch of the -rule.
Note that this time we put a cut only in the second of the two clauses. The reason is that we want to allow backtracking from the first clause to the second one. But of course we still do not want to have backtracking to the clause for literals: If both of the clauses for the negative conjunction fail, the cut in the second clause prevents any further backtracking. So this call of tabl/3 fails. This is exactly as it should be, because in this situation our program has found a contradiction on both branches opened by the -rule. Hence the whole subtableaux for the negative conjunction is closed.