KBO: don't mistake a sort and a term with the same functor number for the same symbol

[quickbeam123]

Type constructors and function symbols are numbered independently, so a sort and a term can share a functor number. KBO::compare (and the precedence fallback in State::result) only compared the numbers, so e.g. compare(complex, one_one(complex)) took the lexicographic path over a 0-ary sort and a 1-ary term and returned EQUAL. Cross-kind comparisons are legitimately made by TermPartialOrdering when ground joinability / term ordering diagrams relate type and term variables; the bogus EQUAL made the partial ordering inconsistent and crashed the prover.

Now both places also require the two terms to be of the same kind. This agrees with PrecedenceOrdering::comparePrecedences (type constructors below function symbols), which the term ordering diagrams already used, and makes KBO a consistent order on sorts and terms together.

Reproducer (release build, SIGSEGV after ~5 s before the fix):
vampire_z3_rel -sa otter Problems/SWV/SWV645_5.p
Unit test KBO/kbo_test24 fails before the fix on ASS(t1->arity()) in traverseLexBidir.

[mezpusz]

From the PR I cannot tell if these are all the places where we should do this, but it's definitely a good thing to start doing it in these two places!