| ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ (x0 = x1 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 : ο . x9 x0 x1 ⟶ x10) ⟶ (∀ x10 : ο . x9 x0 x2 ⟶ x10) ⟶ (∀ x10 : ο . x9 x1 x2 ⟶ x10) ⟶ (∀ x10 : ο . x9 x0 x3 ⟶ x10) ⟶ (∀ x10 : ο . x9 x1 x3 ⟶ x10) ⟶ x9 x2 x3 ⟶ (∀ x10 : ο . x9 x0 x4 ⟶ x10) ⟶ x9 x1 x4 ⟶ (∀ x10 : ο . x9 x2 x4 ⟶ x10) ⟶ x9 x3 x4 ⟶ (∀ x10 : ο . x9 x0 x5 ⟶ x10) ⟶ x9 x1 x5 ⟶ x9 x2 x5 ⟶ (∀ x10 : ο . x9 x3 x5 ⟶ x10) ⟶ (∀ x10 : ο . x9 x4 x5 ⟶ x10) ⟶ x9 x0 x6 ⟶ (∀ x10 : ο . x9 x1 x6 ⟶ x10) ⟶ (∀ x10 : ο . x9 x2 x6 ⟶ x10) ⟶ x9 x3 x6 ⟶ (∀ x10 : ο . x9 x4 x6 ⟶ x10) ⟶ x9 x5 x6 ⟶ x9 x0 x7 ⟶ (∀ x10 : ο . x9 x1 x7 ⟶ x10) ⟶ x9 x2 x7 ⟶ (∀ x10 : ο . x9 x3 x7 ⟶ x10) ⟶ x9 x4 x7 ⟶ (∀ x10 : ο . x9 x5 x7 ⟶ x10) ⟶ (∀ x10 : ο . x9 x6 x7 ⟶ x10) ⟶ and (∀ x10 . x10 ⊆ x8 ⟶ atleastp 3 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ (x12 = x13 ⟶ ∀ x14 : ο . x14) ⟶ not (x9 x12 x13) ⟶ x11) ⟶ x11) (∀ x10 . x10 ⊆ x8 ⟶ atleastp 4 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ (x12 = x13 ⟶ ∀ x14 : ο . x14) ⟶ x9 x12 x13 ⟶ x11) ⟶ x11) |
|