p(a).
p(b).
q(b).

tprove(true) :- !.
tprove((A,B)) :- !,
   tprove(A),
   tprove(B).
tprove(A) :-
   callfail(A),            % Ausgabe call/fail-Port
   clause(A,G),
   tprove(G),
   exitredo(A).            % Ausgabe exit-redo-Port

callfail(L) :- write('Call: '), write(L), nl.
callfail(L) :- write('Fail: '), write(L), nl, fail.

exitredo(L) :- write('Exit: '), write(L), nl.
exitredo(L) :- write('Redo: '), write(L), nl, fail.
