∀x (Alien(x) → Extraterrestrial(x))
∀x (From(x, mars) → Alien(x))
∀x (Extraterrestrial(x) → ¬Human(x))
∀x (HighlyIntelligentBeing(x) ∧ From(x, earth) → Human(x))
HighlyIntelligentBeing(marvin)
¬(From(marvin, earth) ⊕ From(marvin, mars))
¬From(marvin, earth) → Extraterrestrial(marvin)
¬Human(marvin) ∧ ¬From(marvin, mars)