| (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 x8 x9 . and (∀ x10 . x4 x9 = x10 ⟶ and (x2 x10) (x7 = x5 ⟶ and (∀ x11 . x9 = x8) (∃ x11 . x3 x10)) ⟶ ∃ x11 . x7 = x7) (not (x3 (x4 (x4 (x1 x7 x5))))) ⟶ x6 = x9) ⟶ False |
|