Sat-Unsat inference

[Bart Bogaerts]

We should make an inference that does sat-unsat testing.

Only in this case we can do the implication-tseitin-rewriting. We cannot do this when executing mx with only one model, since then the returned model might be wrong!

[Bart Bogaerts]

see issue 112

→ 18548be96ebc

[Broes De Cat]

This is not the case. Tseitin introduction should never lead to theories which have models which are not models of the original theory when restricted to the original vocabulary.