Query CNF is now minimized.

Since the query is grounded, we can do propositional resolution and
subsumption to minimize the query CNF. Thus we can prove more clauses
with smaller k.
Added a simple unit test for the resolution. There should be more
tests.

Also removed [Atom|Literal]::DropActions because it wasn't used except
in the proper+ compiler, which now follows the pattern from
Clause::Unify().