TAP

prove(Fin,UnExp,Lits,FreeV,VarLim, Proof) :- !,
    prove((top,Fin),UnExp,Lits,FreeV,VarLim, Proof, 1, _).

% prove(+Fml,+UnExp,+Lits,+FreeV,+VarLim)
prove((Idp,(A,B)),UnExp,Lits,FreeV,VarLim, [N], Id, Up) :- !,
    N=node(Id, A, and_rule(Idp), Nup), Id1 is Id + 1,
    prove((Id,A),[(and_rule(Idp),B)|UnExp],Lits,FreeV,VarLim, Nup, Id1, Up).

prove((Idp,(A;B)),UnExp,Lits,FreeV,VarLim, [N1, N2], Id, Up) :- !,
    N1=node(Id, A, or_rule(Idp), N1up),
    N2=node(Up1, B, or_rule(Idp), N2up), Id1 is Id + 1,
    prove((Id,A),UnExp,Lits,FreeV,VarLim, N1up, Id1, Up1), Id2 is Up1 + 1,
    prove((Up1,B),UnExp,Lits,FreeV,VarLim, N2up, Id2, Up).

prove((Idp, all(X,Fml)),UnExp,Lits,FreeV,VarLim, [N], Id, Up) :- !,
    N=node(Id, Fml1, all_rule(Idp), Nup), Id1 is Id + 1,
    \+ length(FreeV,VarLim),
    copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
    append(UnExp,[(all_rule(Idp),all(X,Fml))],UnExp1),
    prove((Id, Fml1),UnExp1,Lits,[X1|FreeV],VarLim, Nup, Id1, Up).

prove((Idp, Lit),_,[(LId, L)|Lits],_,_, [N], Id, Up) :-
    ( Lit = -Neg; -Lit = Neg ) ->
        (((unify_with_occurs_check(Neg,L), N=node(Id, false, closed_by(Idp, LId), [])), Up is Id + 1 );
        prove((Idp, Lit),[],Lits,_,_, [N], Id, Up)).

prove((Idp, Lit),[(and_rule(Idr), Next)|UnExp],Lits,FreeV,VarLim, [N], Id, Up) :-
    N = node(Id, Next, and_rule(Idr), Nup), Id1 is Id + 1,
    prove((Id, Next),UnExp,[(Idp, Lit)|Lits],FreeV,VarLim, Nup, Id1, Up).

prove((Idp, Lit),[(all_rule(Idr), Next)|UnExp],Lits,FreeV,VarLim, N, Id, Up) :-  %write('stack all '), write('Lit = '), write(Lit), write('\n'),
    prove((Idr, Next),UnExp,[(Idp, Lit)|Lits],FreeV,VarLim, N, Id, Up).