Add unit tests for Tseitin CNF conversion and implement missing `equals` method for `Sym`.

As promised in #4078.

The tests already paid off: figured out that I forgot to add `equals` (shame on me)...

Review by @adriaanm