| ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 . ∀ x7 : ι → ι . ∀ x8 x9 . ∀ x10 x11 : ι → ι . ∀ x12 . ∀ x13 : ι → ι → ι → ο . ∀ x14 : ι → ι → ο . ∀ x15 . ∀ x16 x17 : ι → ι → ι . ∀ x18 x19 : ι → ι → ο . ∀ x20 . (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x18 x22 x21 ⟶ (x17 x22 (x16 x21 x22) = x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x18 x22 x21 ⟶ (x19 (x16 x21 x22) x20 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . x19 x23 x20 ⟶ x19 x21 x20 ⟶ x19 x22 x20 ⟶ (x17 x23 (x17 x21 x22) = x17 (x17 x23 x21) x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . x0 x21 x22 ⟶ x19 x22 (x1 x23) ⟶ x2 x23 ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x17 x22 x21 = x15 ⟶ (x22 = x15 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . x0 x22 x23 ⟶ x19 x23 (x1 x21) ⟶ (x19 x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x14 x22 x21 ⟶ (x19 x22 (x1 x21) ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 (x1 x21) ⟶ (x14 x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x21 x22 ⟶ (x2 x22 ⟶ False) ⟶ (x0 x21 x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x0 x22 x21 ⟶ (x19 x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x17 x22 x21 = x21 ⟶ (x22 = x15 ⟶ False) ⟶ False) ⟶ (∀ x21 . (x14 x21 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . (x2 x23 ⟶ False) ⟶ (x2 x21 ⟶ False) ⟶ x19 x21 (x1 x23) ⟶ x19 x22 x21 ⟶ (x13 x22 x23 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . (x2 x23 ⟶ False) ⟶ (x2 x21 ⟶ False) ⟶ x19 x21 (x1 x23) ⟶ x13 x22 x23 x21 ⟶ (x19 x22 x21 ⟶ False) ⟶ False) ⟶ ((x15 = x12 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . (x2 x22 ⟶ False) ⟶ (x2 x21 ⟶ False) ⟶ x19 x21 (x1 x22) ⟶ (x13 (x3 x21 x22) x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x21 . (x19 (x11 x21) x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 x23 . (x2 x23 ⟶ False) ⟶ (x2 x21 ⟶ False) ⟶ x19 x21 (x1 x23) ⟶ x13 x22 x23 x21 ⟶ (x19 x22 x23 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ (x19 (x17 x22 x21) x20 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x4 ⟶ x19 x21 x4 ⟶ (x13 (x5 x22 x21) (x1 x6) x4 ⟶ False) ⟶ False) ⟶ (∀ x21 . x19 x21 x4 ⟶ (x19 (x10 x21) x20 ⟶ False) ⟶ False) ⟶ (∀ x21 . x19 x21 x20 ⟶ (x13 (x7 x21) (x1 x6) x4 ⟶ False) ⟶ False) ⟶ ((x19 x4 (x1 (x1 x6)) ⟶ False) ⟶ False) ⟶ ((x19 x15 x6 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ (x21 = x15 ⟶ False) ⟶ (x22 = x15 ⟶ False) ⟶ (x17 x22 x21 = x10 (x5 (x7 x22) (x7 x21)) ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x22 = x15 ⟶ (x17 x22 x21 = x21 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ x21 = x15 ⟶ (x17 x22 x21 = x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ (x18 x22 x21 ⟶ False) ⟶ (x18 x21 x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x20 ⟶ x19 x21 x20 ⟶ (x17 x22 x21 = x17 x21 x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x19 x22 x4 ⟶ x19 x21 x4 ⟶ (x5 x22 x21 = x5 x21 x22 ⟶ False) ⟶ False) ⟶ (∀ x21 x22 . x0 x21 x22 ⟶ x0 x22 x21 ⟶ False) ⟶ (x8 = x9 ⟶ False) ⟶ ((x18 x9 x8 ⟶ False) ⟶ False) ⟶ ((x18 x8 x9 ⟶ False) ⟶ False) ⟶ ((x19 x9 x20 ⟶ False) ⟶ False) ⟶ ((x19 x8 x20 ⟶ False) ⟶ False) ⟶ False |
|