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