∀x (ProfessionalTennisUmpire(x) → ¬ProfessionalTennisPlayer(x))
∀x (WorldTourPlayer(x) → ProfessionalTennisPlayer(x))
∀x (GrandSlamChampion(x) → WorldTourPlayer(x))
∀x (GrandSlamUmpire(x) → ProfessionalTennisUmpire(x))
WorldTourPlayer(nadal) ∨ GrandSlamChampion(nadal)
GrandSlamUmpire(nadal) ∨ ProfessionalTennisPlayer(nadal) → GrandSlamUmpire(nadal)