Fixed: comparison function in Clause::Subsumes().

The sound but incomplete comparison function of clauses shall check if
for any literal in the clause-to-be-subumsed there is one potentially
matching literal in the subsuming clause.

In the non-box case, we can take also the length of z and args into
consideration. But then neither ~P(b) '<' P(a) nor vice-versa, because
that relation would contradict the real < operator because a < b.
We therefore now only continue with the next comparison attribute
(here: sign) if the previous one (here: args) are equal (and not just
same length).