Using instantiate and gnt2:
---------------------------

instantiate -c t=3 bw.sat sussman.dat | gnt2

(Certain options are delivered in the input file bw.sat 
 using a "#options ... ." declaration).

For debugging purposes, you may want to check the output of instantiate
in symbolic form to see that it contains correct instances.

instantiate -text -c t=3 bw.sat sussman.dat | less

(Note that implications a_1, ..., a_n -> b_1 | ... | b_m
 are then printed backwards in a PROLOG style syntax
 {b_1, ..., b_m} :- a_1, ..., a_n. in the output).

Using instantiate and sat solvers (such as zchaff):
---------------------------------------------------

1) Instantiate:

   instantiate -c t=3 bw.sat sussman.dat > bws.dlp

   The output is in the internal gnt2 format.

2) Create the correponding CNF in DIMACS format:

   dimacs bws.dlp > bws.cnf

3) Solve and interpret:

   zchaff bws.cnf | intp bws.cnf

   The latter program (intp) substitutes symbolic names for atoms
   that are true in the interpretation found.