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

% tprove(G) is satisfied if "?- G." is provable and it shows the tracing
% computation of G.

tprove(true) :- !.    % true is the body of facts
tprove( (G1, G2) ) :- !, tprove(G1), tprove(G2). % both parts must be provable
tprove(L) :-
        callfail(L),
        clause(L,G), % search for unifiable rule
        tprove(G),    % proof the body
        exitredo(L).

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.