| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 x5 . ∀ x6 : ι → ο . ∀ x7 x8 . ∀ x9 : ι → ι → ι . ∀ x10 x11 . ∀ x12 x13 : ι → ο . ∀ x14 : ι → ι → ι → ι . ∀ x15 : ι → ι → ι . ∀ x16 : ι → ι . ∀ x17 . ∀ x18 : ι → ο . ∀ x19 . ∀ x20 : ι → ι → ο . ∀ x21 . ∀ x22 : ι → ι → ο . ∀ x23 : ι → ο . (∀ x24 . x23 x24 ⟶ (x24 = x21 ⟶ False) ⟶ (x22 x21 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x0 x25 ⟶ (x25 = x24 ⟶ False) ⟶ x0 x24 ⟶ False) ⟶ (∀ x24 x25 . x22 x24 x25 ⟶ x0 x25 ⟶ False) ⟶ (∀ x24 . x0 x24 ⟶ (x24 = x21 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x20 x24 x25 ⟶ (x0 x25 ⟶ False) ⟶ (x22 x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x1 x24 x21 = x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x22 x25 x24 ⟶ (x20 x25 x24 ⟶ False) ⟶ False) ⟶ ((x2 x3 ⟶ False) ⟶ False) ⟶ (x0 x3 ⟶ False) ⟶ ((x2 x4 ⟶ False) ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ ((x23 x5 ⟶ False) ⟶ False) ⟶ ((x18 x5 ⟶ False) ⟶ False) ⟶ ((x6 x5 ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ ((x0 x7 ⟶ False) ⟶ False) ⟶ ((x23 x17 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x2 x25 ⟶ x2 x24 ⟶ (x2 (x1 x25 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x2 x25 ⟶ x2 x24 ⟶ (x23 (x1 x25 x24) ⟶ False) ⟶ False) ⟶ ((x0 x21 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x20 (x16 x24) x24 ⟶ False) ⟶ False) ⟶ ((x0 x8 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x23 x24 ⟶ (x23 (x15 x25 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x23 x24 ⟶ (x23 (x9 x25 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x23 x24 ⟶ (x23 (x1 x25 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x23 x24 ⟶ x23 x25 ⟶ x24 = x21 ⟶ x25 = x21 ⟶ (x25 = x15 x26 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x23 x24 ⟶ x23 x25 ⟶ x24 = x21 ⟶ x25 = x15 x26 x24 ⟶ (x25 = x21 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . x23 x27 ⟶ x23 x24 ⟶ x23 x26 ⟶ (x24 = x21 ⟶ False) ⟶ x23 x25 ⟶ x27 = x1 (x9 x26 x24) x25 ⟶ x22 x25 x24 ⟶ (x26 = x15 x27 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x23 x24 ⟶ x23 x25 ⟶ (x24 = x21 ⟶ False) ⟶ x25 = x15 x26 x24 ⟶ (x22 (x14 x25 x24 x26) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x23 x24 ⟶ x23 x25 ⟶ (x24 = x21 ⟶ False) ⟶ x25 = x15 x26 x24 ⟶ (x26 = x1 (x9 x25 x24) (x14 x25 x24 x26) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x23 x24 ⟶ x23 x25 ⟶ (x24 = x21 ⟶ False) ⟶ x25 = x15 x26 x24 ⟶ (x23 (x14 x25 x24 x26) ⟶ False) ⟶ False) ⟶ ((x21 = x8 ⟶ False) ⟶ False) ⟶ (∀ x24 . x0 x24 ⟶ (x13 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x0 x24 ⟶ (x2 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x2 x24 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x20 x24 x25 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x0 x24 ⟶ (x12 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x0 x24 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x20 x24 x25 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x6 x24 ⟶ x18 x24 ⟶ (x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x18 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x6 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x22 x24 x25 ⟶ x22 x25 x24 ⟶ False) ⟶ (x15 (x9 x11 x10) x10 = x11 ⟶ False) ⟶ (x10 = x21 ⟶ False) ⟶ ((x23 x11 ⟶ False) ⟶ False) ⟶ ((x23 x10 ⟶ False) ⟶ False) ⟶ False |
|