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