• ∀x.(f (x) → ∃y.((s(y, I) ∨ s(y, F )) ∧ ¬a(y, x)))
• ¬∃.x(s(x, F ) ∧ ∀y.(f (y) → a(x, y)))
• ∃x.(s(x, I) ∧ ∀y.(f (y) ∧ a(x, y) → ¬a(F, y)))