Splitting SF literals like ordinary literals works now.

All splitting is now in a single function, and SF's are split iff k=0.
The crucial "fix" was not to add SF literals (from the sense axioms) to
PEL, as this would allow further splits of these SF literals which are
not split in the semantics from the paper. Splitting these SF literals
would still be sound, of course, but it's a "fix" as it keeps the
implementation equivalent to the paper.
More efficient use of unit propagation.

We don't manage a split set, but remove from the PEL instead and create
copies of the setups. This allows to memorize the unit propagation.