  Stable infiniteness, strong finite witnessability, and smoothness are
model-theoretic properties relevant to theory combination in satisfiability
modulo theories. Theories that are strongly finitely witnessable and smooth are
called strongly polite and can be effectively combined with other theories.
Toledo, Zohar, and Barrett conjectured that stably infinite and strongly
finitely witnessable theories are smooth and therefore strongly polite. They
called counterexamples to this conjecture unicorn theories, as their existence
seemed unlikely. We prove that, indeed, unicorns do not exist. We also prove
versions of the L\"owenheim-Skolem theorem and the {\L}o\'s-Vaught test for
many-sorted logic.
