Rewrote Grounder::AssignLiterals().

Firstly, we need literals, not just terms for
Solver::EntailsComplete(). The new implementation now collects literals
from clauses and queries hopefully correctly.

Grounder::SplitTerms() also now uses fewer variables because
Grounder:Flatten() is more efficient: f(g,g,h) is now replaced with
f(x,x,z) instead of f(x,y,z).

Literal::valid() and Literal::invalid() now take sorts into account:
(t1 = t2) is invalid when t1 and t2 have different sorts, and
(t1 != t2) is valid when t1 and t2 have different sorts.