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