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