| ∀ 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 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x19 x25 x23 x22 ⟶ x19 x25 x23 x24 ⟶ x19 x25 (x17 x23 x24 x22 x25) x23 ⟶ (x23 = x18 x25 x22 x24 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x19 x25 x23 x22 ⟶ x19 x25 x23 x24 ⟶ (x19 x25 (x17 x23 x24 x22 x25) x24 ⟶ False) ⟶ (x23 = x18 x25 x22 x24 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x19 x25 x23 x22 ⟶ x19 x25 x23 x24 ⟶ (x19 x25 (x17 x23 x24 x22 x25) x22 ⟶ False) ⟶ (x23 = x18 x25 x22 x24 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x19 x25 x23 x22 ⟶ x19 x25 x23 x24 ⟶ (x16 (x17 x23 x24 x22 x25) (x15 x25) ⟶ False) ⟶ (x23 = x18 x25 x22 x24 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 x26 . x21 x26 ⟶ x14 x26 ⟶ x20 x26 ⟶ x16 x22 (x15 x26) ⟶ x16 x25 (x15 x26) ⟶ x16 x23 (x15 x26) ⟶ x23 = x18 x26 x22 x25 ⟶ x16 x24 (x15 x26) ⟶ x19 x26 x24 x22 ⟶ x19 x26 x24 x25 ⟶ (x19 x26 x24 x23 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x23 = x18 x25 x22 x24 ⟶ (x19 x25 x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x21 x25 ⟶ x14 x25 ⟶ x20 x25 ⟶ x16 x22 (x15 x25) ⟶ x16 x24 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x23 = x18 x25 x22 x24 ⟶ (x19 x25 x23 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 . x21 x24 ⟶ x14 x24 ⟶ x20 x24 ⟶ x16 x22 (x15 x24) ⟶ x16 x23 (x15 x24) ⟶ (x18 x24 x22 x23 = x0 x24 x22 x23 ⟶ False) ⟶ False) ⟶ (∀ x22 . (x16 (x13 x22) x22 ⟶ False) ⟶ False) ⟶ ((x1 x2 ⟶ False) ⟶ False) ⟶ ((x20 x12 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x1 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 . x21 x24 ⟶ x14 x24 ⟶ x20 x24 ⟶ x16 x22 (x15 x24) ⟶ x16 x23 (x15 x24) ⟶ (x16 (x18 x24 x22 x23) (x15 x24) ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 . x20 x24 ⟶ x16 x22 (x15 x24) ⟶ x16 x23 (x15 x24) ⟶ (x16 (x0 x24 x22 x23) (x15 x24) ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ x19 x22 (x10 x22) (x11 x22) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x19 x22 (x3 x22) (x11 x22) ⟶ False) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x19 x22 (x10 x22) (x3 x22) ⟶ False) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x16 (x11 x22) (x15 x22) ⟶ False) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x16 (x3 x22) (x15 x22) ⟶ False) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ (x16 (x10 x22) (x15 x22) ⟶ False) ⟶ (x9 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 x25 . x20 x25 ⟶ x9 x25 ⟶ x16 x24 (x15 x25) ⟶ x16 x22 (x15 x25) ⟶ x16 x23 (x15 x25) ⟶ x19 x25 x24 x22 ⟶ x19 x25 x22 x23 ⟶ (x19 x25 x24 x23 ⟶ False) ⟶ False) ⟶ (∀ x22 x23 x24 . x21 x24 ⟶ x14 x24 ⟶ x20 x24 ⟶ x16 x22 (x15 x24) ⟶ x16 x23 (x15 x24) ⟶ (x18 x24 x22 x23 = x18 x24 x23 x22 ⟶ False) ⟶ False) ⟶ (∀ x22 . x20 x22 ⟶ x14 x22 ⟶ x8 x22 ⟶ False) ⟶ (x19 x4 x5 x6 ⟶ False) ⟶ ((x19 x4 x5 (x18 x4 x6 x7) ⟶ False) ⟶ False) ⟶ ((x16 x5 (x15 x4) ⟶ False) ⟶ False) ⟶ ((x16 x7 (x15 x4) ⟶ False) ⟶ False) ⟶ ((x16 x6 (x15 x4) ⟶ False) ⟶ False) ⟶ ((x20 x4 ⟶ False) ⟶ False) ⟶ ((x14 x4 ⟶ False) ⟶ False) ⟶ ((x21 x4 ⟶ False) ⟶ False) ⟶ ((x9 x4 ⟶ False) ⟶ False) ⟶ False |
|