Search for blocks/addresses/...

Proofgold Asset

asset id
0ad1a51e6c63e73ca15821a1f22797c55e544cdc0f5748c147029cd2f561c779
asset hash
d377051e697ee70d02761b71bf3775bc606c5121c3dff0d9f5cdb0120d940393
bday / block
35134
tx
c4cc2..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7a1d8.. : ∀ 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 . ∀ x55 : ι → ι . ∀ x56 . ∀ x57 x58 : ι → ι . ∀ x59 : ι → ο . ∀ x60 x61 : ι → ι . ∀ x62 x63 : ι → ο . ∀ x64 x65 . ∀ x66 : ι → ι → ι . ∀ x67 : ι → ι . ∀ x68 : ι → ι → ο . ∀ x69 : ι → ο . ∀ x70 . ∀ x71 : ι → ο . (∀ x72 x73 . x71 x73 ⟶ (x73 = x72 ⟶ False) ⟶ x71 x72 ⟶ False) ⟶ (∀ x72 x73 . x0 x72 x73 ⟶ x71 x73 ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x72 = x70 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x72 x73 ⟶ x2 x73 (x1 x74) ⟶ x71 x74 ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x73 x74 ⟶ x2 x74 (x1 x72) ⟶ (x2 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x0 (x5 x72) (x6 (x4 x73)) ⟶ (x0 x72 (x6 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x0 x72 (x6 x73) ⟶ (x0 (x5 x72) (x6 (x4 x73)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x3 x74 ⟶ x7 x73 x72 ⟶ x0 x72 (x6 x74) ⟶ (x0 x73 (x6 x74) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x7 x73 x72 ⟶ (x2 x73 (x1 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x2 x73 (x1 x72) ⟶ (x7 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x69 x73 ⟶ x7 x72 (x6 (x67 x73)) ⟶ (x68 x72 (x6 (x67 x73)) ⟶ False) ⟶ (x0 x72 (x6 (x67 x73)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x3 x74 ⟶ x8 x74 ⟶ (x74 = x70 ⟶ False) ⟶ x3 x72 ⟶ x0 x72 x74 ⟶ x0 x73 (x6 x72) ⟶ (x0 x73 (x6 x74) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x8 x73 ⟶ (x73 = x70 ⟶ False) ⟶ x0 x72 (x6 x73) ⟶ (x0 x72 (x6 (x66 x72 x73)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x8 x73 ⟶ (x73 = x70 ⟶ False) ⟶ x0 x72 (x6 x73) ⟶ (x0 (x66 x72 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x8 x73 ⟶ (x73 = x70 ⟶ False) ⟶ x0 x72 (x6 x73) ⟶ (x3 (x66 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x2 x72 x73 ⟶ (x71 x73 ⟶ False) ⟶ (x0 x72 x73 ⟶ False) ⟶ False) ⟶ ((x6 x70 = x70 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ x0 (x4 (x9 x72)) x72 ⟶ (x8 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x0 (x9 x72) x72 ⟶ False) ⟶ (x8 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x3 (x9 x72) ⟶ False) ⟶ (x8 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x8 x73 ⟶ x3 x72 ⟶ x0 x72 x73 ⟶ (x0 (x4 x72) x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x0 x73 x72 ⟶ (x2 x73 x72 ⟶ False) ⟶ False) ⟶ ((x2 x70 x65 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x10 x72 x70 = x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x69 x72 ⟶ (x8 (x67 x72) ⟶ False) ⟶ False) ⟶ ((x2 x12 x11 ⟶ False) ⟶ False) ⟶ ((x2 x12 x64 ⟶ False) ⟶ False) ⟶ ((x13 x12 x11 x64 ⟶ False) ⟶ False) ⟶ ((x63 x12 ⟶ False) ⟶ False) ⟶ (x71 x12 ⟶ False) ⟶ (∀ x72 . (x7 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x2 x72 (x1 x74) ⟶ x2 x73 x72 ⟶ (x13 x73 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x2 x72 (x1 x74) ⟶ x13 x73 x74 x72 ⟶ (x2 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x5 x72 = x1 x72 ⟶ False) ⟶ False) ⟶ ((x64 = x65 ⟶ False) ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ (x71 x15 ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x16 (x17 x72) x12 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x2 (x17 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x18 x72 ⟶ False) ⟶ x18 (x19 x72) ⟶ False) ⟶ (∀ x72 . (x18 x72 ⟶ False) ⟶ (x2 (x19 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ (x16 (x21 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ (x62 (x21 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ (x22 (x21 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x18 (x61 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ x71 (x61 x72) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x2 (x61 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ ((x23 x24 ⟶ False) ⟶ False) ⟶ (x71 x24 ⟶ False) ⟶ (x25 x26 ⟶ False) ⟶ ((x62 x26 ⟶ False) ⟶ False) ⟶ ((x22 x26 ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ (x16 (x60 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x28 (x27 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x2 (x27 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ ((x23 x29 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x59 x72 ⟶ False) ⟶ x59 (x58 x72) ⟶ False) ⟶ (∀ x72 . (x59 x72 ⟶ False) ⟶ (x2 (x58 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x28 (x57 x72) x72 ⟶ False) ⟶ (∀ x72 . (x2 (x57 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ (x59 x56 ⟶ False) ⟶ (x71 x30 ⟶ False) ⟶ (∀ x72 . (x71 (x55 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x2 (x55 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ ((x3 x54 ⟶ False) ⟶ False) ⟶ ((x31 x54 ⟶ False) ⟶ False) ⟶ ((x53 x54 ⟶ False) ⟶ False) ⟶ (x71 x54 ⟶ False) ⟶ ((x52 x51 ⟶ False) ⟶ False) ⟶ ((x62 x51 ⟶ False) ⟶ False) ⟶ ((x22 x51 ⟶ False) ⟶ False) ⟶ ((x20 x32 ⟶ False) ⟶ False) ⟶ ((x59 x32 ⟶ False) ⟶ False) ⟶ ((x3 x32 ⟶ False) ⟶ False) ⟶ ((x31 x32 ⟶ False) ⟶ False) ⟶ ((x53 x32 ⟶ False) ⟶ False) ⟶ ((x71 x50 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ x71 (x33 x72) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x2 (x33 x72) (x1 x72) ⟶ False) ⟶ False) ⟶ ((x3 x34 ⟶ False) ⟶ False) ⟶ ((x62 x49 ⟶ False) ⟶ False) ⟶ ((x22 x49 ⟶ False) ⟶ False) ⟶ ((x20 x48 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x67 (x67 x72) = x67 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x10 x72 x72 = x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x59 x72 ⟶ False) ⟶ x59 (x1 x72) ⟶ False) ⟶ (∀ x72 . (x59 x72 ⟶ False) ⟶ (x20 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x59 x72 ⟶ False) ⟶ x59 (x67 x72) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ x23 x72 ⟶ (x23 (x4 x72) ⟶ False) ⟶ False) ⟶ (x59 x65 ⟶ False) ⟶ ((x3 x65 ⟶ False) ⟶ False) ⟶ (x71 x65 ⟶ False) ⟶ (∀ x72 . x59 x72 ⟶ (x20 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x59 x72 ⟶ (x59 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ x71 (x10 x72 x73) ⟶ False) ⟶ ((x35 x65 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ x71 (x10 x73 x72) ⟶ False) ⟶ ((x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 (x47 x72) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x3 (x4 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ x71 (x4 x72) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x53 (x6 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x20 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ x71 (x67 x72) ⟶ False) ⟶ ((x71 x70 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 (x1 x72) ⟶ False) ⟶ (∀ x72 . x71 (x4 x72) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x20 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x71 (x67 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x22 x72 ⟶ x62 x72 ⟶ (x14 (x47 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x16 (x47 x72) x12 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x2 x72 (x1 x73) ⟶ (x13 (x36 x72 x73) x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x2 (x46 x72) x72 ⟶ False) ⟶ False) ⟶ ((x71 x37 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x2 x72 (x1 x74) ⟶ x13 x73 x74 x72 ⟶ (x2 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x2 (x5 x72) (x1 (x1 x72)) ⟶ False) ⟶ False) ⟶ ((x2 x64 (x1 x11) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x20 (x67 x72) ⟶ False) ⟶ False) ⟶ ((x70 = x37 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ x0 (x5 (x39 x72)) x72 ⟶ x0 (x40 x72) x72 ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ x0 (x5 (x39 x72)) x72 ⟶ x68 (x40 x72) x72 ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ x0 (x5 (x39 x72)) x72 ⟶ (x7 (x40 x72) x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ (x0 (x39 x72) x72 ⟶ False) ⟶ x0 (x40 x72) x72 ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ (x0 (x39 x72) x72 ⟶ False) ⟶ x68 (x40 x72) x72 ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x38 x72 ⟶ (x0 (x39 x72) x72 ⟶ False) ⟶ (x7 (x40 x72) x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x69 x73 ⟶ x7 x72 x73 ⟶ (x68 x72 x73 ⟶ False) ⟶ (x0 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x69 x73 ⟶ x0 x72 x73 ⟶ (x0 (x5 x72) x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x69 x72 ⟶ (x38 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x4 x72 = x10 x72 (x47 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 (x41 x72) x72 ⟶ (x38 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x7 (x41 x72) (x45 x72) ⟶ False) ⟶ (x38 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x0 (x45 x72) x72 ⟶ False) ⟶ (x38 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x38 x74 ⟶ x0 x72 x74 ⟶ x7 x73 x72 ⟶ (x0 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x10 x73 x72 = x10 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x44 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x14 x73 ⟶ x2 x72 (x1 x73) ⟶ (x14 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x16 x72 x12 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x16 x72 x12 ⟶ x71 x72 ⟶ False) ⟶ (∀ x72 . x2 x72 x65 ⟶ (x23 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x14 x73 ⟶ x2 x72 x73 ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x14 x73 ⟶ x2 x72 x73 ⟶ (x22 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x16 x72 x70 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x23 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x14 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x16 x72 x70 ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x23 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x18 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x25 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x18 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x18 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x22 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ x59 x72 ⟶ (x23 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x18 x73 ⟶ x2 x72 (x1 x73) ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x3 x73 ⟶ x2 x72 x73 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x22 x72 ⟶ x62 x72 ⟶ (x25 x72 ⟶ False) ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x22 x72 ⟶ x62 x72 ⟶ (x25 x72 ⟶ False) ⟶ (x22 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x22 x72 ⟶ x62 x72 ⟶ (x25 x72 ⟶ False) ⟶ x18 x72 ⟶ False) ⟶ (∀ x72 . x23 x72 ⟶ (x59 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x2 x72 (x1 x73) ⟶ x28 x72 x73 ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x42 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x25 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x22 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x2 x72 x65 ⟶ (x59 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ x2 x72 (x1 x73) ⟶ x71 x72 ⟶ (x28 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x22 x73 ⟶ x62 x73 ⟶ x2 x72 (x1 x73) ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x23 x72 ⟶ (x20 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ x2 x72 (x1 x73) ⟶ (x28 x72 x73 ⟶ False) ⟶ x71 x72 ⟶ False) ⟶ (∀ x72 . x53 x72 ⟶ x31 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x52 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x22 x72 ⟶ x62 x72 ⟶ (x22 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x20 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x2 x72 (x1 x73) ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x31 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x3 x72 ⟶ (x53 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x62 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x69 x72 ⟶ (x38 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x44 x73 ⟶ x2 x72 (x1 x73) ⟶ (x44 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ x18 x72 ⟶ (x16 x72 x12 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x0 x72 x73 ⟶ x0 x73 x72 ⟶ False) ⟶ (x69 (x6 (x67 x43)) ⟶ False) ⟶ ((x69 x43 ⟶ False) ⟶ False) ⟶ False (proof)