∀x (WantToGoTo(mr.AndMrs.Smith, x) ∧ City(x) → (California(x) ∨ Florida(x)) ∧ NeverGo(x))
City(sanFrancisco) ∧ California(sanFrancisco) ∧ WantToGoTo(mr.AndMrs.Smith, sanFrancisco) ∧ City(losAngeles) ∧ California(losAngeles) ∧ WantToGoTo(mr.AndMrs.Smith, losAngeles) ∧ City(sanDiego) ∧ California(sanDiego) ∧ WantToGoTo(mr.AndMrs.Smith, sanDiego)
City(orlando) ∧ Florida(orlando) ∧ WantToGo(mr.AndMrs.Smith, orlando) ∧ City(miami) ∧ Florida(miami) ∧ WantToGo(mr.AndMrs.Smith, miami)
∃x ∃y ∀z (¬(x=z) ∧ ¬(y=z) ∧ ¬(x=y) ∧ City(x) ∧ City(y) ∧ City(z) ∧ California(x) ∧ California(y) ∧ California(z) → Visit(mr.smith, x) ∧ Visit(mr.smith, y) ∧ ¬Visit(mr.smith, z))
∃x ∀y (¬(x=y) ∧ City(x) ∧ City(y) ∧ Florida(x) ∧ Florida(y) → Visit(mrs.smith, x) ∧ ¬Visit(mrs.smith, y))
∃x ∃y (¬(x=y) ∧ City(x) ∧ City(y) ∧ WantToGoTo(mr.AndMrs.Smith, x) ∧ California(x) ∧ WantToGoTo(mr.AndMrs.Smith, y) ∧ California(y))