Maybe don't use naive CNF?

In `Sat`, there is a `cnf` function which I wrote myself. It's the naive algorithm. Which may be ok. It's certainly easier to debug. But it may be worth, if performance becomes an issue, replacing with Tseitin.

There may be some obstacles to that. And the formulas are typically not very big, so it is not guaranteed to be a good idea.