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