Fixed splitting-query-substitution bug

When a split sets (t = n), we need to substitute n for t in the query
in the semantics of the KR 2016 paper. Here it is insufficient,
because we possibly split before reducing quantifiers, so that
occurrences of t may occur only later. We hence wait until the query
is reduced to a clause and then substitute all n for t when there is
a unit clause [(t = n)] in the setup. This is even stronger than the
substitution from the KR 2016 paper because it also allows us to infer
from [f(n) = n], [g(n) = n] that [f(g(n)) = n] without split, whereas
the KR 2016 semantics needs an (easy) split for g(n).