Proofgold Asset

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
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
Theorem 9c595.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . (x0 x6 x10 ⟶ x0 x1 x10 ⟶ x0 x6 x9 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x1 x11 ⟶ x0 x1 x10 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x2 x11 ⟶ x0 x2 x10 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x11 ⟶ x0 x4 x10 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x1 x12 ⟶ x0 x1 x10 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x6 x13 ⟶ x0 x1 x13 ⟶ x0 x6 x9 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x2 x13 ⟶ x0 x2 x11 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x13 ⟶ x0 x4 x11 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x3 x14 ⟶ x0 x4 x12 ⟶ x0 x3 x12 ⟶ False) ⟶ (x0 x2 x14 ⟶ x0 x2 x12 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x4 x12 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x3 x14 ⟶ x0 x4 x13 ⟶ x0 x3 x13 ⟶ False) ⟶ (x0 x1 x14 ⟶ x0 x1 x13 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x6 x15 ⟶ x0 x1 x15 ⟶ x0 x6 x10 ⟶ x0 x1 x10 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x3 x15 ⟶ x0 x4 x11 ⟶ x0 x3 x11 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x11 ⟶ x0 x2 x11 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x11 ⟶ x0 x2 x10 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x11 ⟶ x0 x3 x10 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x11 ⟶ x0 x4 x10 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x12 ⟶ x0 x2 x12 ⟶ False) ⟶ (x0 x6 x15 ⟶ x0 x1 x15 ⟶ x0 x6 x13 ⟶ x0 x1 x13 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x13 ⟶ x0 x2 x11 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x13 ⟶ x0 x3 x11 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x13 ⟶ x0 x4 x11 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x14 ⟶ x0 x2 x14 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x14 ⟶ x0 x2 x12 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x14 ⟶ x0 x3 x12 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x14 ⟶ x0 x4 x12 ⟶ False) ⟶ (not (x0 x3 x9) ⟶ not (x0 x2 x9) ⟶ not (x0 x1 x9) ⟶ False) ⟶ (not (x0 x3 x12) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x4 x12) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x2 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x3 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x4 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x5 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x5 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ False) ⟶ (not (x0 x4 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ False) ⟶ (not (x0 x3 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x3 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x4 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x4 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x6 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x6 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x3 x14) ⟶ not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ False) ⟶ (not (x0 x4 x14) ⟶ not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ False) ⟶ (not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x2 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x3 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x4 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x5 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x5 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x15) ⟶ not (x0 x2 x15) ⟶ not (x0 x1 x15) ⟶ False) ⟶ (not (x0 x5 x15) ⟶ not (x0 x3 x15) ⟶ not (x0 x1 x15) ⟶ False) ⟶ (not (x0 x3 x15) ⟶ not (x0 x2 x15) ⟶ not (x0 x3 x9) ⟶ not (x0 x2 x9) ⟶ False) ⟶ (not (x0 x6 x15) ⟶ not (x0 x4 x15) ⟶ not (x0 x6 x9) ⟶ not (x0 x4 x9) ⟶ False) ⟶ (x0 x1 x11 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x1 x12 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x1 x13 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x1 x9) ⟶ False) ⟶ (x0 x3 x9 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (not (x0 x1 x11) ⟶ not (x0 x1 x12) ⟶ x0 x1 x14 ⟶ not (x0 x1 x13) ⟶ False) ⟶ (x0 x1 x9 ⟶ x0 x1 x15 ⟶ x0 x3 x15 ⟶ not (x0 x2 x9) ⟶ False) ⟶ False