Equivalent

• ¬ (∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p))
• ∀ t : ¬ t ∨ F (t ∧ X t ∨ X ¬ t ∧ ¬ t) ∨ F (t ∧ ¬ p)

Complement

• ∃ t : G ((t ↔ Z ¬ t) ∧ (t → p))
• ∃ t : t ∧ G ((t → p) ∧ (t ↔ X ¬ t))
• ∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p)