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

Proofgold Asset