Search for blocks/addresses/...

Proofgold Asset

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