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