I am solving SAT instances using minisat. The syntax is `minisat inputfile outputfile`. However, it only returns one solution. To find all solutions I have to append the negation of the first solution to the original instance and solve again until it is unsolvable. The output file looks like this:

```
SAT
1 -2 3 -4 5 -6 -7 0 

```

So each natural number from one to whatever is either negated or unnegated followed by a 0. I need to multiply each number by -1 and append that (last) line (including the 0) to the end of `inputfile` and loop it until the first line of `outputfile` is `UNSAT`.