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