1add_herbrand_preds((Head :- Body),(Head :- Body1)) :-
    2	herbrandize_variables(Body,[],BodyVars,false,_),
    3	herbrandize_variables(Head,BodyVars,_,true,Matches),
    4        conjoin(Matches,Body,Body1).
    5	
    6
    7herbrandize_variables(Term,VarsIn,VarsOut,MatchesIn,MatchesOut) :-
    8        builtin(Term) ->
    9	        VarsOut = VarsIn,
   10                MatchesOut = MatchesIn;
   11        %true ->
   12	        nonvar(Term) ->
   13                       myfunctor(Term,_,N),
   14		       herbrandize_args(Term,VarsIn,VarsOut,MatchesIn,MatchesOut,1,N);
   15	        identical_member(Term,VarsIn) ->
   16	               VarsOut = VarsIn,
   17		       MatchesOut = MatchesIn;
   18	        %true ->
   19		       VarsOut = [Term|VarsIn],
   20		       conjoin(MatchesIn,herbrand(Term),MatchesOut).
   21
   22herbrandize_args(Term,VarsIn,VarsOut,MatchesIn,MatchesOut,I,N) :-
   23        I > N ->
   24                VarsOut = VarsIn,
   25                MatchesOut = MatchesIn;
   26        %true ->
   27                arg(I,Term,Arg),
   28                herbrandize_variables(Arg,VarsIn,Vars1,MatchesIn,Matches1),
   29                I1 is I + 1,
   30                herbrandize_args(Term,Vars1,VarsOut,Matches1,MatchesOut,I1,N).
   31
   32herbrand_universe(U) :-
   33	setof(X,herbrand(X),U).
   34
   35herbrand_preds([],true).
   36herbrand_preds([C|Cs],Wff) :-
   37	herbrand_preds(Cs,Wffs),
   38	conjoin((herbrand(C):-true),Wffs,Wff).
   39
   40add_answer_preds((query :- Query),(query :- (Query,nl,nl,write(answer:Vars),nl))) :-
   41	!,
   42	variables(Query,Vars).
   43add_answer_preds(R,R).
   44
   45%%% constants returns a list of the constants appearing in a formula.
   46
   47constants(Wff,L) :-
   48        Wff = (A :- B) ->
   49                constants(A,L1),
   50                constants(B,L2),
   51                union(L2,L1,L);
   52        Wff = (A , B) ->
   53                constants(A,L1),
   54                constants(B,L2),
   55                union(L2,L1,L);
   56        Wff = (A ; B) ->
   57                constants(A,L1),
   58                constants(B,L2),
   59                union(L2,L1,L);
   60        Wff = (A : B) ->
   61                constants(A,L1),
   62                constants(B,L2),
   63                union(L2,L1,L);
   64        myfunctor(Wff,search,_) ->        % list constants in first argument of search
   65                arg(1,Wff,X),
   66                constants(X,L);
   67        builtin(Wff) ->
   68                L = [];
   69        %true ->
   70                myfunctor(Wff,_,N),
   71                (N > 0 ->
   72		   constantize_args(Wff,[],L,1,N);
   73		 %true ->
   74                   L = []).
   75
   76constantize_args(Term,FnsIn,FnsOut,I,N) :-
   77	var(Term) ->
   78		FnsOut = FnsIn;
   79	atom(Term) ->
   80	        FnsOut = [Term|FnsIn];
   81        I > N ->
   82                FnsOut = FnsIn;
   83        %true ->
   84                arg(I,Term,ArgI),
   85		(var(ArgI) ->
   86		        Fns1 = [];
   87		%true ->
   88		        myfunctor(ArgI,_,NI),
   89                        constantize_args(ArgI,FnsIn,Fns1,1,NI)),
   90                I1 is I + 1,
   91                constantize_args(Term,Fns1,FnsOut,I1,N).
   92
   93%%% variables returns a list of the variables appearing in a formula.
   94
   95variables(Wff,L) :-
   96        Wff = (A :- B) ->
   97                variables(A,L1),
   98                variables(B,L2),
   99                union(L2,L1,L);
  100        Wff = (A , B) ->
  101                variables(A,L1),
  102                variables(B,L2),
  103                union(L2,L1,L);
  104        Wff = (A ; B) ->
  105                variables(A,L1),
  106                variables(B,L2),
  107                union(L2,L1,L);
  108        Wff = (A : B) ->
  109                variables(A,L1),
  110                variables(B,L2),
  111                union(L2,L1,L);
  112        myfunctor(Wff,search,_) ->        % list variables in first argument of search
  113                arg(1,Wff,X),
  114                variables(X,L);
  115        builtin(Wff) ->
  116                L = [];
  117        %true ->
  118                myfunctor(Wff,_,N),
  119                (N > 0 ->
  120		   variablize_args(Wff,[],L,1,N);
  121		 %true ->
  122                   L = []).
  123
  124variablize_args(Term,FnsIn,FnsOut,I,N) :-
  125	atom(Term) ->
  126		FnsOut = FnsIn;
  127	var(Term) ->
  128	        FnsOut = [Term|FnsIn];
  129        I > N ->
  130                FnsOut = FnsIn;
  131        %true ->
  132                arg(I,Term,ArgI),
  133		(var(ArgI) ->
  134		        union([ArgI],FnsIn,Fns1);
  135		%true ->
  136		        myfunctor(ArgI,_,NI),
  137                        variablize_args(ArgI,FnsIn,Fns1,1,NI)),
  138                I1 is I + 1,
  139                variablize_args(Term,Fns1,FnsOut,I1,N).
  140
  141
  142variablize_clause(Clause,Vars) :-
  143	ClauseTerm =.. [clause|Clause],
  144	variables(ClauseTerm,Vars).
  145
  146instance([],_,Clause).
  147instance(Vars,Cons,Clause) :-
  148	myselect(V,Vars,V1s),
  149	member(V,Cons),
  150	instance(V1s,Cons,Clause).
  151
  152skolem([],Term,Term).
  153skolem([Var|Vars],Term,SkTerm) :-
  154	skolem(Vars,Term,Term1),
  155	SkTerm=(Var^Term1).
  156
  157instances(Clause,Terms,Instances) :-
  158	variablize_clause(Clause,Vars),
  159	skolem(Vars,instance(Vars,Terms,Clause),DoIt),
  160	setof(Clause,DoIt,Instances).
  161
  162instantiation([],_,[]) :-
  163	!.
  164instantiation(Matrix,[],Matrix) :-
  165	!.
  166instantiation([Clause|Matrix],Terms,MatrixInstances) :-
  167	instances(Clause,Terms,Instances),
  168	instantiation(Matrix,Terms,IMatrix),
  169	combine_clauses(Instances,IMatrix,MatrixInstances)