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