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