| ∀ 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 . ∀ x34 : ι → ο . ∀ x35 : ι → ι . ∀ x36 x37 . ∀ x38 x39 : ι → ο . ∀ x40 . ∀ x41 : ι → ο . ∀ x42 . ∀ x43 : ι → ο . (∀ x44 x45 . x43 x45 ⟶ (x45 = x44 ⟶ False) ⟶ x43 x44 ⟶ False) ⟶ (∀ x44 x45 . x0 x44 x45 ⟶ x43 x45 ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x44 = x42 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x0 x44 x45 ⟶ x2 x45 (x1 x46) ⟶ x43 x46 ⟶ False) ⟶ (∀ x44 x45 x46 . x0 x45 x46 ⟶ x2 x46 (x1 x44) ⟶ (x2 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x3 x45 x44 ⟶ (x2 x45 (x1 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x45 (x1 x44) ⟶ (x3 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x2 x44 x45 ⟶ (x43 x45 ⟶ False) ⟶ (x0 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x3 x45 x46 ⟶ x3 x46 x44 ⟶ (x3 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x0 x45 x44 ⟶ (x2 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x3 x44 x44 ⟶ False) ⟶ False) ⟶ ((x4 x5 ⟶ False) ⟶ False) ⟶ (x43 x5 ⟶ False) ⟶ (∀ x44 . (x6 x44 ⟶ False) ⟶ x6 (x7 x44) ⟶ False) ⟶ (∀ x44 . (x6 x44 ⟶ False) ⟶ (x2 (x7 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ (x6 (x8 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ x43 (x8 x44) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ (x2 (x8 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ (x41 x40 ⟶ False) ⟶ ((x9 x40 ⟶ False) ⟶ False) ⟶ ((x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ (x11 (x10 x44) x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ (x2 (x10 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ ((x9 x12 ⟶ False) ⟶ False) ⟶ ((x38 x12 ⟶ False) ⟶ False) ⟶ ((x39 x12 ⟶ False) ⟶ False) ⟶ (x43 x12 ⟶ False) ⟶ (∀ x44 . x11 (x13 x44) x44 ⟶ False) ⟶ (∀ x44 . (x2 (x13 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ ((x9 x14 ⟶ False) ⟶ False) ⟶ ((x38 x14 ⟶ False) ⟶ False) ⟶ ((x39 x14 ⟶ False) ⟶ False) ⟶ (x43 x37 ⟶ False) ⟶ (∀ x44 . (x43 (x15 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . (x2 (x15 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ ((x38 x16 ⟶ False) ⟶ False) ⟶ ((x39 x16 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x9 x18 ⟶ False) ⟶ False) ⟶ ((x39 x18 ⟶ False) ⟶ False) ⟶ ((x43 x36 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ x43 (x19 x44) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ (x2 (x19 x44) (x1 x44) ⟶ False) ⟶ False) ⟶ ((x39 x20 ⟶ False) ⟶ False) ⟶ (x43 x20 ⟶ False) ⟶ ((x9 x21 ⟶ False) ⟶ False) ⟶ ((x39 x21 ⟶ False) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ x39 x44 ⟶ x43 (x22 x44) ⟶ False) ⟶ (∀ x44 . (x43 x44 ⟶ False) ⟶ x39 x44 ⟶ x43 (x35 x44) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x43 (x22 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x43 (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x6 x44 ⟶ x39 x44 ⟶ (x6 (x22 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x6 x44 ⟶ x39 x44 ⟶ (x6 (x35 x44) ⟶ False) ⟶ False) ⟶ ((x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 (x1 x44) ⟶ False) ⟶ (∀ x44 . (x6 x44 ⟶ False) ⟶ x39 x44 ⟶ x9 x44 ⟶ x6 (x35 x44) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ x6 (x22 x44) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x9 x44 ⟶ x41 x44 ⟶ (x6 (x22 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x43 (x22 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x43 (x35 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x38 x44 ⟶ x9 x44 ⟶ (x34 (x22 x44) ⟶ False) ⟶ False) ⟶ (∀ x44 . (x2 (x23 x44) x44 ⟶ False) ⟶ False) ⟶ ((x43 x33 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x0 (x24 x44 x45) x44 ⟶ (x3 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x0 (x24 x44 x45) x45 ⟶ False) ⟶ (x3 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . x3 x45 x46 ⟶ x0 x44 x45 ⟶ (x0 x44 x46 ⟶ False) ⟶ False) ⟶ ((x42 = x33 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x3 (x22 (x27 x44 x45 x46)) x45 ⟶ False) ⟶ (x0 (x26 x44 x45 x46) x44 ⟶ False) ⟶ (x44 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x35 (x27 x44 x45 x46) = x46 ⟶ False) ⟶ (x0 (x26 x44 x45 x46) x44 ⟶ False) ⟶ (x44 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x26 x44 x45 x46 = x27 x44 x45 x46 ⟶ False) ⟶ (x0 (x26 x44 x45 x46) x44 ⟶ False) ⟶ (x44 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x9 (x27 x44 x45 x46) ⟶ False) ⟶ (x0 (x26 x44 x45 x46) x44 ⟶ False) ⟶ (x44 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 . (x39 (x27 x44 x45 x46) ⟶ False) ⟶ (x0 (x26 x44 x45 x46) x44 ⟶ False) ⟶ (x44 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x0 (x26 x47 x45 x46) x47 ⟶ x39 x44 ⟶ x9 x44 ⟶ x26 x47 x45 x46 = x44 ⟶ x35 x44 = x46 ⟶ x3 (x22 x44) x45 ⟶ (x47 = x25 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 x48 . x48 = x25 x46 x47 ⟶ x39 x44 ⟶ x9 x44 ⟶ x45 = x44 ⟶ x35 x44 = x46 ⟶ x3 (x22 x44) x47 ⟶ (x0 x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x47 = x25 x45 x46 ⟶ x0 x44 x47 ⟶ (x3 (x22 (x32 x44 x47 x46 x45)) x46 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x47 = x25 x45 x46 ⟶ x0 x44 x47 ⟶ (x35 (x32 x44 x47 x46 x45) = x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x47 = x25 x45 x46 ⟶ x0 x44 x47 ⟶ (x44 = x32 x44 x47 x46 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x47 = x25 x45 x46 ⟶ x0 x44 x47 ⟶ (x9 (x32 x44 x47 x46 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 x46 x47 . x47 = x25 x45 x46 ⟶ x0 x44 x47 ⟶ (x39 (x32 x44 x47 x46 x45) ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x4 x45 ⟶ x2 x44 (x1 x45) ⟶ (x4 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x4 x45 ⟶ x2 x44 x45 ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x4 x45 ⟶ x2 x44 x45 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x4 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x6 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x6 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x6 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x6 x45 ⟶ x2 x44 (x1 x45) ⟶ (x6 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ x6 x44 ⟶ False) ⟶ (∀ x44 x45 . x43 x45 ⟶ x2 x44 (x1 x45) ⟶ x11 x44 x45 ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ (x38 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x41 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x43 x45 ⟶ False) ⟶ x2 x44 (x1 x45) ⟶ x43 x44 ⟶ (x11 x44 x45 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ (x28 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x39 x45 ⟶ x9 x45 ⟶ x2 x44 (x1 x45) ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . (x43 x45 ⟶ False) ⟶ x2 x44 (x1 x45) ⟶ (x11 x44 x45 ⟶ False) ⟶ x43 x44 ⟶ False) ⟶ (∀ x44 x45 . x39 x45 ⟶ x2 x44 (x1 x45) ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x17 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ x39 x44 ⟶ x9 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x43 x45 ⟶ x2 x44 (x1 x45) ⟶ (x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x39 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 . x43 x44 ⟶ (x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x44 x45 . x0 x44 x45 ⟶ x0 x45 x44 ⟶ False) ⟶ (x3 (x25 x31 x29) (x25 x31 x30) ⟶ False) ⟶ ((x3 x29 x30 ⟶ False) ⟶ False) ⟶ False |
|