% node(identifier,corresponding NNF formula,used rule,list of its sub-nodes/sons)

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) :- !, write('0'),
    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) :- !, write('1'),
    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,
    prove((Up1,B),UnExp,Lits,FreeV,VarLim, N2up, Id2, Up).

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

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

prove((_, Lit),[(and_rule(Idr), Next)|UnExp],Lits,FreeV,VarLim, [N], Id, Up) :-  write('4'),
    N = node(Id1, Next, and_rule(Idr), Proof1), Id1 is Id + 1,
    prove((Id, Next),UnExp,[(Id, Lit)|Lits],FreeV,VarLim, Proof1, Id1, Up).

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

%% proof((fact,-fact),[node(1,fact,and_rule(top),[node(2,fact,and_rule(top),[node(3,false,closed_by(2,1),[])])])])
%% proof((fact,-fact),[node(1,fact,and_rule(top),[node(2,-fact,and_rule(top),[node(3,false,closed_by(2,1),[])])])]).