Search for blocks/addresses/...

Proofgold Asset

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