∃ x0 : ι → ι → ο . ∀ x2 : ο . ((∀ x3 x4 . x0 x3 x4 ⟶ x0 x4 x3) ⟶ x0 0 1 ⟶ x0 1 2 ⟶ x0 2 3 ⟶ x0 3 4 ⟶ x0 4 0 ⟶ not (x0 0 2) ⟶ not (x0 0 3) ⟶ not (x0 1 3) ⟶ not (x0 1 4) ⟶ not (x0 2 4) ⟶ x2) ⟶ x2 |
|