The basic problem here is that existence is not a property. If we follow the concept of the property of existing down, we get lots of nonsense. (Including one particularly annoying "proof of God" that has been shot in the heart, the head and the liver, and just won't go lay down and die.)
In particular, we cannot logically say things like
¬Exists(x) & Predicate(Q) → ¬Q(x)
which you seem to assume. (So, proposing this is your particular mistake.)
After all, if Exists is a predicate, so is ¬Exists. Then by this logic,
¬Exists(x) & Property(¬Exists) → ¬(¬Exists)(x)
Nonexistent things just can't have the property of not existing.
And if Exists is not a predicate we don't know what the left side means, because we don't know how non-predicates get along with things like & and ¬.
Following on that, the proper way to reference non-existent objects has a long history including two mainstream approaches: modal realism, including Meinongianism, and disontologizing their descriptions, for instance by forcing them to always be stated via quantification.
My favored approach is a compromise between the two: insisting fictional objects can be meaningful only in terms of implications they would fulfill were they to exist. (This conjures up the whole machinery of modality, since "would" is a modal verb. But it does not assert modal existence, just that modal grammar has implications about real things.)
It is true that nonexistent animals cannot have one horn?
For Meinong or modal realists, no, the nonexistent things exist in another sense, (in a 'modality' like might, should or can), and still have the attributed properties of their definitions, so you cannot derive your contradiction.
You already have two versions of the forced quantification approach.
For the implication approach
Unicorn(x) → |{y: y ∈ horns(x)}| = 1
remains true if {x : Unicorn(x)} is an empty set, because a false premise implies anything. Every real unicorn has one horn, it also has none, and seventy-two. Again, you can't get your contradiction.