∀x (WorkIn(x, office) → Commuter(x))
∀x (WorkIn(x, office) ⊕ WorkFrom(x, home))
∀x (WorkFrom(x, home) → Have(x, relaxedSchedule))
Commuter(george) ⊕ Have(george, homeOffice)
(WorkFrom(george, home) ⊕ Have(george, homeOffice)) → ¬WorkFrom(george, home) ∧ Commuter(george)
¬(WorkFrom(george, home) ∧ WorkIn(george, office)) → ¬(Commuter(george) ∨ Have(george, relaxedSchedule))