| ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 86fe8.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 732e2.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ efbf0.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ c13a7.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ bae07.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ f982a.. x2 x14 x15 x3 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ be274.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 0e6a7.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 0809e.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ fa7d9.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 6f07c.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ d8b5d.. x2 x14 x15 x16 x17 x3 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 51ac7.. x2 x14 x15 x16 x17 x18 x19 x20 x3 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ f9d60.. x2 x14 x15 x16 x17 x18 x19 x3 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ c2a1e.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 7861e.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 8a782.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 47dfa.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ x13 |
|