Using instantiate and gnt2: --------------------------- instantiate --dlp --true-negation -c t=3 bw.lp | gnt2 (Alternatively, options to instantiate can be specified int the input file bw.lp as follows "#options ... .") Using instantiate and sat solvers (such as zchaff): --------------------------------------------------- 1) Instantiate: instantiate --dlp --true-negation -c t=$1 bw.lp > bw.sm The output is in the internal gnt2 (and smodels) format. 2) Create the correponding CNF in DIMACS format: dimacs bw.sm > bw.cnf 3) Solve and interpret: zchaff bw.cnf | interpret bw.sm object destination The latter program (interpret) substitutes symbolic names for atoms that are true in the interpretation found and whose names begin with "object" or "destination" (it is easy to construct a solution to the planning problem given the true instances of these two predicates).