∃x ∃y (EmployeeIn(x, jamesSTown) ∧ WorkIn(x, businessAnalysis) ∧ GoodAt(x, math) ∧ (¬(x=y)) ∧ EmployeeIn(y, jamesSTown) ∧ WorkIn(y, businessAnalysis) ∧ GoodAt(y, math))
∀x ((EmployeeIn(x, jamesSTown) ∧ WorkIn(x, businessAnalysis)) → WorkFor(x, thisCompany))
∀x ((EmployeeIn(x, jamesSTown) ∧ WorkFor(x, thisCompany)) → ¬From(x, china))
∀x (EmployeeIn(x, jamesSTown) ∧ WorkIn(x, softwareEngineering) → From(x, china))
EmployeeIn(leif, jamesSTown) ∧ WorkIn(leif, softwareEngineering)
¬(GoodAt(leif, math) ∧ WorkIn(leif, businessAnalysis)) → (¬WorkFor(x, thisCompany) ∧ ¬WorkIn(x, softwareEngineering))