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