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)).