Query evaluation works.

The query evaluation differs somewhat from the paper.
We convert the formula to CNF (with all quantifiers removed) and check
subsumption for each clause. If necessary, we split k literals from the
PEL. If then still necessary, we add try positive and negative SF
literals.

Open questions are:
1. We never branch on disjunctions (rule 7). OK?
2. We use a minimal (no subsumed clauses, no split literals) setup
   after unit propagation. OK?
3. How should the split literals be chosen intelligently?

The example from the paper works (see unit test).
A few proper+ axioms for d0 are missing in the paper.