Implemented needless split detection.

When attempting to prove c with given k, an atom a is split only if
(1) there is no unit clause [a] or [~a] in the setup AND
(2) (a) c contains a or ~a OR
    (b) some clause d from the setup contains a or ~a AND
        (i)  |d| <= k+1, i.e., it might trigger unit propagation OR
        (ii) |d\c| <= k, i.e., it might lead to subsumption.

This detection requires iteration over the whole setup and is therefore
quite expensive. Maybe an index atom -> clauses that contain the atom
would help, but maintaining this index might be expensive again, because
it needs to be updated during unit propagation and minimization.