Dimacs-output for sat-decision.
Removed superfluous output.

That preprocessing determined unsatisfiability follows from the number
of nodes being 0.
Output of Satz now similar to OKsolver-output.