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