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