Hi!
The program at the bottom is supposed to return clauses that are missing for a goal to be provable. The problem is that it returns one solution “to much” as shown in the last solution in this output:
?- main.
MISSING PREMISES:
p(A,2,presenceOfFlammableMaterial)
p(B,2,johnDroppedAMatch)
true ;
MISSING PREMISES:
p(A,2,presenceOfFlammableMaterial)
p(B,1,johnWasTired)
true ;
MISSING PREMISES:
precedes(3,3)
p(A,3,presenceOfFlammableMaterial)
p(B,2,johnWasTired)
true ;
false.
What i would like is just:
MISSING PREMISES:
p(A,2,presenceOfFlammableMaterial)
p(B,2,johnDroppedAMatch)
true ;
MISSING PREMISES:
p(A,2,presenceOfFlammableMaterial)
p(B,1,johnWasTired)
true ;
I have a hard time understanding what’s wrong and would appreciate some tips for improving it 
The important predicate is missing0(G, M), where G is a goal and M a list of missing clauses.
Cheers/JCR
PROGRAM---------------------------------------------------------------------------------------------
:-use_module(library(clpr)).
precedes(1, 2).
precedes(2, 3).
p(X1, T2, johnDroppedAMatch):-
p(X2, T1, johnWasTired),
precedes(T1, T2),
{X1 = 0.5 * X2}.
p(X1, T2, fire):-
p(X2, T1, presenceOfFlammableMaterial),
p(X3, T1, johnDroppedAMatch),
precedes(T1, T2),
{X1 = 0.7 * X2 * X3}.
missing(G, M):- call(G), M = ['There are no missing premises.'].
missing(G, M):- \+clause(G, _), M = ['There are no clauses for the goal.'].
missing(G, M):- clause(G, B), \+G, missing0(B, M).
missing0(G, M):- G = (G1, G2), !, missing0(G1, M1), missing0(G2, M2), append(M1, M2, M).
missing0(G, M):- G = (G1; _), missing0(G1, M).
missing0(G, M):- G = (_; G2), missing0(G2, M).
missing0(G, M):- call(G), M = [].
missing0(G, M):- \+G, G \= (_, _), G \= (_; _), M = [G].
missing0(G, M):- \+G, G \= {_}, clause(G, B), missing0(B, M).
showMissing(M):- copy_term_nat(M, M1), numbervars(M1, 0, _, [attvar(bind)]), sort(M1, M2), nl, writeln('MISSING PREMISES:'), maplist(writeln, M2).
main:-missing(p(1, 3, fire), M), showMissing(M).