Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition 2f869.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition 5a3b5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6
Definition 00e19.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (5a3b5.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ x0 x1 x6 ⟶ not (x0 x2 x6) ⟶ not (x0 x3 x6) ⟶ not (x0 x4 x6) ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 87c36.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 6648a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ x0 x3 x6 ⟶ not (x0 x4 x6) ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Definition cdfa5.. := λ x0 x1 . λ x2 : ι → ι → ο . ∀ x3 . x3 ⊆ x1 ⟶ atleastp x0 x3 ⟶ not (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x2 x4 x5)
Param u4 : ι
Definition 86706.. := cdfa5.. u4
Definition 35fb6.. := λ x0 . λ x1 : ι → ι → ο . 86706.. x0 (λ x2 x3 . not (x1 x2 x3))
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param UPair^UPair : ι → ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known 7204a.. : ∀ x0 x1 x2 x3 . (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ equip u4 (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3)
Known 58c12.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x0 x1 x4 ⟶ x0 x2 x3 ⟶ x0 x2 x4 ⟶ x0 x3 x4 ⟶ (∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ x0 x5 x6 ⟶ x0 x6 x5) ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x0 x5 x6
Known c88f0.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⊆ x0
Theorem d54be.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (not (x0 x2 x12) ⟶ not (x0 x2 x13) ⟶ not (x0 x2 x11) ⟶ not (x0 x2 x10) ⟶ x0 x3 x11 ⟶ not (x0 x3 x10) ⟶ False) ⟶ (not (x0 x2 x12) ⟶ not (x0 x2 x10) ⟶ not (x0 x2 x9) ⟶ not (x0 x2 x11) ⟶ not (x0 x2 x13) ⟶ x0 x3 x10 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (not (x0 x2 x10) ⟶ not (x0 x2 x11) ⟶ x0 x2 x13 ⟶ not (x0 x2 x12) ⟶ False) ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ (x0 x2 x12 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (x0 x2 x11 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x2 x9) ⟶ False) ⟶ False
Known a1242.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x4 x3 x6 x5 x7
Known de43b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x3 x5 x4 x7 x6
Theorem 8c844.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x5 x3 x7 x4 x6
Theorem db457.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x7 x5 x6 x3 x4
Theorem b6037.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x4 x6 x3 x7 x5
Theorem 787e8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x6 x7 x4 x5 x3
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 0d569.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (not (x0 x2 x10) ⟶ not (x0 x2 x12) ⟶ not (x0 x2 x13) ⟶ not (x0 x2 x9) ⟶ x0 x3 x13 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x13 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (not (x0 x2 x9) ⟶ not (x0 x2 x13) ⟶ x0 x2 x12 ⟶ not (x0 x2 x10) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ False
Known d4057.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 6648a.. x1 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. x1 x2 x7 x6 x5 x4 x3
Theorem e0399.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x13 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x12 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (not (x0 x2 x13) ⟶ not (x0 x2 x9) ⟶ x0 x2 x10 ⟶ not (x0 x2 x12) ⟶ False) ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ False
Theorem 5145e.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x10 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (x0 x2 x13 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (not (x0 x2 x11) ⟶ not (x0 x2 x10) ⟶ x0 x2 x12 ⟶ not (x0 x2 x13) ⟶ False) ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ False
Theorem 37ba9.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x13 ⟶ not (x0 x2 x12) ⟶ False) ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ False
Theorem 16f3d.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x6 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x5 x8 ⟶ not (x0 x2 x8) ⟶ False) ⟶ (x0 x4 x8 ⟶ not (x0 x3 x8) ⟶ False) ⟶ False
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Theorem 314fb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x4 x6 x3 x5
Theorem bd69a.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x2 x4 x6 x3 x5 x7
Known bfe59.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x6 x4 x5 x3
Theorem 32906.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x2 x6 x4 x5 x3 x7
Known 66a94.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x3 x5 x4 x6
Theorem e2299.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x2 x3 x5 x4 x6 x7
Theorem 0c442.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x3 x4 x2 x7 x5 x6
Theorem 9d6b5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x4 x2 x3 x6 x7 x5
Theorem d678f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ 00e19.. x1 x2 x3 x4 x5 x6 x7 ⟶ 00e19.. x1 x4 x6 x7 x2 x3 x5
Theorem b0a9c.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι → ι → ι → ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ (x0 x7 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x6 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x5 x9 ⟶ not (x0 x4 x9) ⟶ False) ⟶ False) ⟶ ∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ (x0 x6 x9 ⟶ not (x0 x4 x9) ⟶ False) ⟶ (x0 x8 x9 ⟶ not (x0 x4 x9) ⟶ False) ⟶ False
Theorem 84671.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι → ι → ι → ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ (x0 x7 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x6 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x5 x9 ⟶ not (x0 x4 x9) ⟶ False) ⟶ False) ⟶ ∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ (x0 x8 x9 ⟶ not (x0 x5 x9) ⟶ False) ⟶ False
Theorem 95c1f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι → ι → ι → ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ (x0 x7 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x6 x9 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x5 x9 ⟶ not (x0 x4 x9) ⟶ False) ⟶ False) ⟶ ∀ x2 x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x2 ⟶ ∀ x12 . x12 ∈ x2 ⟶ ∀ x13 . x13 ∈ x2 ⟶ ∀ x14 . x14 ∈ x2 ⟶ (∀ x15 . x15 ∈ x2 ⟶ ∀ x16 . x16 ∈ x2 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ x1 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ False
Theorem 917b0.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ (∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False