Assumption doesn't hold true currently

With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessarily monononously decreasing
causing wrong results when in the first round the same number of nodes
got removed as added due to sat states.

Acceptance test for cores is ∃ which is safe to use when non or only
some child states are created tus far

Should actually happen when the State changes from `Expandable` to
`Open` and trigger the propagateSatMu but for now just do it in
propagateSatMu so we can observe the algorithm working.

Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable

Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints

Also accept already Satisfiable nodes when finding paths

This still produces wrong results: It assumes every node with empty
focus to be sat.

Makes morally same formulas actually the same. Removes the need to
recalculate some States that have already been fully expanded but with
different variable names only (where this is possible)

This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning

A and E are syntax elements in CTL
"Fixes" the testsuite for K