:-lib(metutl).

 prove((A,B), Phi, Lits, FreeV, VarLim) :- !,     % A and B
      prove(A, [B|Phi], Lits, FreeV, VarLim).

 prove((A;B), Phi, Lits, FreeV, VarLim) :- !,     % A or B
      prove(A, Phi, Lits, FreeV, VarLim),
      prove(B, Phi, Lits, FreeV, VarLim).

 prove(all(X,A), Phi, Lits, FreeV, VarLim) :- !,  % A(x)
      \+ length(FreeV, VarLim),
      copy_term((X,A,FreeV), (X1,A1,FreeV)),
      append(Phi, [all(X,A)], Phi1),
      prove(A1, Phi1, Lits, [X1|FreeV], VarLim).

 prove(L, _, [Lit|Lits], _, _) :-                 % leaf
      (L = -N; -L = N) -> ( unify(N, Lit) ;
                            prove(L, [], Lits, _, _) ).

 prove(L, [F|Phi], Lits, FreeV, VarLim) :-
      prove(F, Phi, [L|Lits], FreeV, VarLim).

 prove(F, VarLim) :- prove(F, [], [], [], VarLim).