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.

翻译：稳定无穷性、强有限可见证性以及光滑性是满足性模理论中与理论组合相关的模型论性质。具有强有限可见证性且光滑的理论被称为强礼貌理论，并能有效地与其他理论组合。Toledo、Zohar和Barrett猜想：稳定无穷且强有限可见证的理论是光滑的，因而是强礼貌的。他们将此猜想的反例称为独角兽理论，因其存在性似乎极不可能。我们证明了独角兽理论确实不存在。同时，我们还证明了多类逻辑下的勒文海姆-斯科伦定理与Łoś-Vaught测试的若干形式。