Fixed: split literals were deleted too aggressively from PEL

Suppose we need to split p and q to show c.
Before, the following would happen:
1. p
 2. q
 3. ~q
4. ~p
because during 2./3., q was deleted from PEL.
Now, the following happens:
1. p
 2. q
 3. ~q
4. ~p
 5. q
 6. ~q
7. q
8. ~q
Sadly, this is much more expensive, obviously.
Added map_[lazy_]copy().
SF literals are not split anymore.

Important: the recursion then needs to stop when k <= 0.
Before, it was k < 0.

A better way to introduce splitting of SF literals that don't count
towards the k-limit would be to use clause_sf() when k == 0 is reached.

For some reason, the unit test test_morri_example() takes very long and
fails due to timeout. The unit test test_morri_example_with_context()
still works. This issue only occurs when setup_clause_small_pel() uses
clause_pel() which also adds SF literals. It is independent of
consistency checks.
SF literals are split for free again.

Only the SF literals due to actions are split.
The new way to implement that is more elegant and fully compatible to
standard ESL.
Fixed: timeout in belief unit test.

The unit test called bsetup_init_beliefs() for the static+dynamic setup,
but it is sufficient to call it for the static setup alone and add the
dynamic setup afterwards.
Added stdvec_is_ground().
vector_clear() clears the buffer.

That's not necessary but may help the garbage collection.
Added ewff_cmp(), slightly changed ewff_eval().

ewff_eval() now returns true if t1==t2 for EWFF_EQ. This is obviously
correct, in particular, if t1, t2 are variables.
Since ewff_true abbreviates x==x and x may not be bounded by the varmap
(for technical reasons, logically it is universally quantified, of
course), the old implementation was just correct because varmap_lookup()
deterministically returned the ((term_t) 0).
Queries are converted to CNF (again).

This was the original solution which was only used if USE_QUERY_CNF was
defined for the last time. The alternative procedure followed the
paper's semantics / decision procedure more closely. Unfortunately, it
was not complete. Roughly, the reason is that the paper
nondeterministically chooses when to split literals during query
decomposition, but in the implementation, splitting only happens
per-clause. Because I'm dumb as soup, I didn't realize it is relevant
when a literal is split.

For example, consider (p v q v (~p ^ ~q)). That's a taugology. It should
be provable for k = 2: First split p, then split q. If neither p or q
are negative, p v q holds. Otherwise (~p ^ ~q) holds.
Our implementation didn't find that because it first tried to prove the
(p v q) (by splitting p, q), then tries to prove ~p (by splitting p),
and then tries to prove ~q (by splitting q), and fails for all of them.

When we first compute the CNF, we obtain ((p v q v ~p) ^ (p v q v ~q)).
Then we first prove (p v q v ~p) by splitting p, and then prove
(p v q v ~q) by splitting q. Note that k = 1 is already sufficient.

Observe that we also ground quantifiers. Originally this was more of a
hack, but it seems to be quite a good idea. Suppose KB = {} and the
query is (E x) (P(x) v ~P(x)). That's grounded to get P(#1) v ~P(#1),
which can be proved for k = 1.
With our old procedure, we would have first tried to prove P(#1) and
then ~P(#1), and both would have failed, which is again because P(#1)
must be split *before* processing the quantifier.

Added unit tests to show (p v q v (~p ^ ~q)) and to show
(E x) (P(x) v ~P(x)).