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