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