Implemented smaller setups.

The idea is to only split those literals that may be relevant for the
query. That is, the split set is the least set that contains
* the query's PEL and SF literals corresponding to actions in the query;
* if l is in the split set and occurs in a clause (possibly negated)
  in the setup, then the non-SF PEL of this clause are in the split set
  as well.

Notice that the SF literals from the query are now added in the
beginning already, whereas we added them after computing the full PEL
in the old version. I think it the ordering didn't matter for the old
version, but for the new version we add them first so that, intuitively
speaking, the RHS of the corresponding instantiated SF axioms will be
split as well.

Renamed setup_with_splits_and_sf_subsumes() to setup_entails(). Makes
more sense (it's not just subsumption) and is shorter.

Added setup_inconsistent(). Other than setup_entails() it uses the full
PEL. It's much slower. For completeness, one hence needs to evaluate
``setup_inconsistent() || setup_entails(s, c, k),'' but the idea is to
test setup_inconsistent() just once at the beginning and when it's
changed, but not for every query (or one just trusts the setup to be
consistent). This bookkeeping shall be done in query.c.

Notice that belief.c performs calls setup_inconsistent() a lot. The idea
is (and was before) to memorize these results to avoid testing
inconsistency for the first plausibility levels again and again.