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.