Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../56401..
PUawD../ee67a..
vout
PrPhD../cb73d.. 102.64 bars
TML6P../e3feb.. ownership of d9f0a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMWMZ../3514a.. ownership of 97552.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUXQo../d6559.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem d9f0a.. : ∀ 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 . x70 x72 ⟶ (x72 = x71 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 x72 . x0 x71 x72 ⟶ x70 x72 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x71 = x69 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x71 x72 ⟶ x2 x72 (x1 x73) ⟶ x70 x73 ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 x76 . (x68 x76 ⟶ False) ⟶ x63 x76 ⟶ x67 x76 ⟶ x2 x71 (x64 x76) ⟶ x2 x75 (x64 x76) ⟶ x2 x72 (x64 x76) ⟶ x2 x74 (x64 x76) ⟶ x2 x73 (x64 x76) ⟶ x65 x76 x71 x75 x72 x74 ⟶ x65 x76 x71 x75 x72 x73 ⟶ x65 x76 x71 x72 x75 x74 ⟶ x65 x76 x71 x72 x75 x73 ⟶ (x66 x76 x71 x75 x72 ⟶ False) ⟶ (x74 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x72 x73 ⟶ x2 x73 (x1 x71) ⟶ (x2 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ x65 x72 (x57 x71 x72) (x58 (x64 x72) (x64 x72) x71 (x57 x71 x72)) (x59 x71 x72) (x58 (x64 x72) (x64 x72) x71 (x59 x71 x72)) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ (x2 (x59 x71 x72) (x64 x72) ⟶ False) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ (x2 (x57 x71 x72) (x64 x72) ⟶ False) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x68 x74 ⟶ False) ⟶ x63 x74 ⟶ x67 x74 ⟶ x54 x71 ⟶ x62 x71 (x64 x74) (x64 x74) ⟶ x55 x71 (x64 x74) (x64 x74) ⟶ x2 x71 (x1 (x61 (x64 x74) (x64 x74))) ⟶ x56 x71 x74 ⟶ x60 x71 x74 ⟶ x2 x72 (x64 x74) ⟶ x2 x73 (x64 x74) ⟶ (x65 x74 x72 (x58 (x64 x74) (x64 x74) x71 x72) x73 (x58 (x64 x74) (x64 x74) x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x53 x72 x71 ⟶ (x2 x72 (x1 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x72 (x1 x71) ⟶ (x53 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x65 x72 (x52 x71 x72) (x51 x71 x72) (x58 (x64 x72) (x64 x72) x71 (x52 x71 x72)) (x58 (x64 x72) (x64 x72) x71 (x51 x71 x72)) ⟶ (x56 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ (x2 (x51 x71 x72) (x64 x72) ⟶ False) ⟶ (x56 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ (x2 (x52 x71 x72) (x64 x72) ⟶ False) ⟶ (x56 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x68 x74 ⟶ False) ⟶ x63 x74 ⟶ x67 x74 ⟶ x54 x71 ⟶ x62 x71 (x64 x74) (x64 x74) ⟶ x55 x71 (x64 x74) (x64 x74) ⟶ x2 x71 (x1 (x61 (x64 x74) (x64 x74))) ⟶ x56 x71 x74 ⟶ x2 x73 (x64 x74) ⟶ x2 x72 (x64 x74) ⟶ (x65 x74 x73 x72 (x58 (x64 x74) (x64 x74) x71 x73) (x58 (x64 x74) (x64 x74) x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x71 x72 ⟶ (x70 x72 ⟶ False) ⟶ (x0 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 x71 ⟶ (x2 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x54 x74 ⟶ x62 x74 x71 x72 ⟶ x2 x74 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x62 x73 x71 x72 ⟶ x2 x73 (x1 (x61 x71 x72)) ⟶ x50 x71 x72 x74 x73 ⟶ (x50 x71 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (x70 x3 ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x54 x74 ⟶ x62 x74 x71 x72 ⟶ x2 x74 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x62 x73 x71 x72 ⟶ x2 x73 (x1 (x61 x71 x72)) ⟶ (x50 x71 x72 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x53 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x54 x74 ⟶ x62 x74 x71 x72 ⟶ x2 x74 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x62 x73 x71 x72 ⟶ x2 x73 (x1 (x61 x71 x72)) ⟶ x74 = x73 ⟶ (x50 x71 x72 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x54 x74 ⟶ x62 x74 x71 x72 ⟶ x2 x74 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x62 x73 x71 x72 ⟶ x2 x73 (x1 (x61 x71 x72)) ⟶ x50 x71 x72 x74 x73 ⟶ (x74 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x49 x71 = x48 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x70 x74 ⟶ False) ⟶ x54 x71 ⟶ x62 x71 x74 x73 ⟶ x2 x71 (x1 (x61 x74 x73)) ⟶ x2 x72 x74 ⟶ (x58 x74 x73 x71 x72 = x4 x71 x72 ⟶ False) ⟶ False) ⟶ ((x47 x46 ⟶ False) ⟶ False) ⟶ (x70 x46 ⟶ False) ⟶ (∀ x71 x72 . (x54 (x45 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x45 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x44 (x45 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x6 (x45 x71 x72) ⟶ False) ⟶ False) ⟶ (x43 x42 ⟶ False) ⟶ ((x54 x42 ⟶ False) ⟶ False) ⟶ ((x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ x70 (x8 x71) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ (x2 (x8 x71) (x1 (x64 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x70 (x10 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x54 (x10 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x5 (x10 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x44 (x10 x71 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x6 (x10 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x2 (x10 x71 x72) (x1 (x61 x72 x71)) ⟶ False) ⟶ False) ⟶ (x70 x11 ⟶ False) ⟶ (∀ x71 . (x41 (x40 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x12 (x40 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x39 (x40 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x13 (x40 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x38 (x40 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x40 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x44 (x40 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x40 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x2 (x40 x71) (x1 (x61 x71 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x55 (x14 x71) x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x62 (x14 x71) x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x41 (x14 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x54 (x14 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x14 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x44 (x14 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x14 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x2 (x14 x71) (x1 (x61 x71 x71)) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x54 x16 ⟶ False) ⟶ False) ⟶ ((x6 x16 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x9 x71 ⟶ x37 (x36 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x9 x71 ⟶ (x2 (x36 x71) (x1 (x64 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ (x37 (x35 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ x70 (x35 x71) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ (x2 (x35 x71) (x1 (x64 x71)) ⟶ False) ⟶ False) ⟶ ((x70 x17 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x34 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x44 (x34 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x6 (x34 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 (x34 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x2 (x34 x71 x72) (x1 (x61 x72 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x54 (x18 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x18 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x44 (x18 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x6 (x18 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x2 (x18 x71 x72) (x1 (x61 x72 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x62 (x33 x71 x72) x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x54 (x33 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x33 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x44 (x33 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x6 (x33 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x2 (x33 x71 x72) (x1 (x61 x72 x71)) ⟶ False) ⟶ False) ⟶ ((x54 x32 ⟶ False) ⟶ False) ⟶ ((x6 x32 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x31 x71 ⟶ False) ⟶ x9 x71 ⟶ x30 (x64 x71) ⟶ False) ⟶ (∀ x71 . x31 x71 ⟶ x9 x71 ⟶ (x30 (x64 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x68 x71 ⟶ x9 x71 ⟶ (x37 (x64 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x48 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x9 x71 ⟶ x37 (x64 x71) ⟶ False) ⟶ (∀ x71 . (x15 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x12 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x39 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x13 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x54 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x7 x71 ⟶ False) ⟶ x9 x71 ⟶ x70 (x64 x71) ⟶ False) ⟶ ((x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ x9 x71 ⟶ (x70 (x64 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x47 x73 ⟶ x6 x71 ⟶ x5 x71 x73 ⟶ x54 x71 ⟶ (x54 (x4 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x47 x73 ⟶ x6 x71 ⟶ x5 x71 x73 ⟶ x54 x71 ⟶ (x6 (x4 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x41 (x48 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x54 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x44 (x48 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x2 (x19 x71) x71 ⟶ False) ⟶ False) ⟶ ((x9 x29 ⟶ False) ⟶ False) ⟶ ((x67 x20 ⟶ False) ⟶ False) ⟶ (∀ x71 . x67 x71 ⟶ (x9 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x2 (x49 x71) (x1 (x61 x71 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x41 (x49 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 (x48 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x70 x74 ⟶ False) ⟶ x54 x71 ⟶ x62 x71 x74 x73 ⟶ x2 x71 (x1 (x61 x74 x73)) ⟶ x2 x72 x74 ⟶ (x2 (x58 x74 x73 x71 x72) x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ (x21 x71 x72 = x58 (x64 x72) (x64 x72) x71 (x21 x71 x72) ⟶ False) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ (x2 (x21 x71 x72) (x64 x72) ⟶ False) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x56 x71 x72 ⟶ x50 (x64 x72) (x64 x72) x71 (x49 (x64 x72)) ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x68 x73 ⟶ False) ⟶ x63 x73 ⟶ x67 x73 ⟶ x54 x71 ⟶ x62 x71 (x64 x73) (x64 x73) ⟶ x55 x71 (x64 x73) (x64 x73) ⟶ x2 x71 (x1 (x61 (x64 x73) (x64 x73))) ⟶ x60 x71 x73 ⟶ (x50 (x64 x73) (x64 x73) x71 (x49 (x64 x73)) ⟶ False) ⟶ x2 x72 (x64 x73) ⟶ x72 = x58 (x64 x73) (x64 x73) x71 x72 ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x63 x72 ⟶ x67 x72 ⟶ x54 x71 ⟶ x62 x71 (x64 x72) (x64 x72) ⟶ x55 x71 (x64 x72) (x64 x72) ⟶ x2 x71 (x1 (x61 (x64 x72) (x64 x72))) ⟶ x60 x71 x72 ⟶ (x56 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x28 x71 x69 ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x47 x72 ⟶ x2 x71 (x1 x72) ⟶ (x47 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x7 x71 ⟶ (x28 x71 x69 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x2 x72 (x1 (x61 x73 x71)) ⟶ x54 x72 ⟶ x62 x72 x73 x71 ⟶ (x62 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x2 x72 (x1 (x61 x73 x71)) ⟶ x54 x72 ⟶ x62 x72 x73 x71 ⟶ x70 x72 ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x2 x72 (x1 (x61 x73 x71)) ⟶ x54 x72 ⟶ x62 x72 x73 x71 ⟶ (x54 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x47 x72 ⟶ x2 x71 x72 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x47 x72 ⟶ x2 x71 x72 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x31 x71 ⟶ False) ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 x72 . x2 x72 (x1 (x61 x71 x71)) ⟶ x38 x72 ⟶ x54 x72 ⟶ x41 x72 x71 ⟶ x62 x72 x71 x71 ⟶ (x55 x72 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x72 (x1 (x61 x71 x71)) ⟶ x38 x72 ⟶ x54 x72 ⟶ x41 x72 x71 ⟶ x62 x72 x71 x71 ⟶ (x62 x72 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x72 (x1 (x61 x71 x71)) ⟶ x38 x72 ⟶ x54 x72 ⟶ x41 x72 x71 ⟶ x62 x72 x71 x71 ⟶ (x54 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x47 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x68 x71 ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x15 x73 ⟶ x27 x73 x72 ⟶ (x55 x73 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x71 x72)) ⟶ x54 x73 ⟶ x15 x73 ⟶ x27 x73 x72 ⟶ (x54 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x37 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x37 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x37 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x31 x71 ⟶ False) ⟶ x31 x71 ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x31 x71 ⟶ False) ⟶ x7 x71 ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x72 x71)) ⟶ x54 x73 ⟶ x55 x73 x72 x71 ⟶ (x27 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x72 x71)) ⟶ x54 x73 ⟶ x55 x73 x72 x71 ⟶ (x15 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x72 x71)) ⟶ x54 x73 ⟶ x55 x73 x72 x71 ⟶ (x54 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x54 x71 ⟶ (x43 x71 ⟶ False) ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x54 x71 ⟶ (x43 x71 ⟶ False) ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x54 x71 ⟶ (x43 x71 ⟶ False) ⟶ x37 x71 ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x7 x71 ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x7 x71 ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x2 x71 (x1 (x61 x72 x73)) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x72 (x1 (x61 x71 x71)) ⟶ x62 x72 x71 x71 ⟶ (x41 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x2 x71 (x1 (x61 x73 x72)) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x13 x71 ⟶ x12 x71 ⟶ (x38 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x13 x71 ⟶ x12 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ x2 x71 (x1 (x61 x72 x73)) ⟶ x62 x71 x72 x73 ⟶ (x41 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ x54 x72 ⟶ x2 x71 (x1 x72) ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x68 x71 ⟶ False) ⟶ x7 x71 ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x71 x72)) ⟶ (x5 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x72 x71)) ⟶ (x44 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ x70 x71 ⟶ x2 x72 (x1 (x61 x73 x71)) ⟶ x41 x72 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x2 x71 (x1 (x61 x73 x72)) ⟶ x62 x71 x73 x72 ⟶ (x41 x71 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x15 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x6 x71 ⟶ x54 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x7 x71 ⟶ (x68 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x73 (x1 (x61 x71 x72)) ⟶ (x6 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x2 x71 (x1 (x61 x73 x72)) ⟶ (x41 x71 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x2 x72 (x1 (x61 x73 x71)) ⟶ x41 x72 x73 ⟶ (x62 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x68 x71 ⟶ False) ⟶ x7 x71 ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x28 x71 x3 ⟶ (x68 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ x28 x71 x3 ⟶ x7 x71 ⟶ False) ⟶ (∀ x71 . x9 x71 ⟶ (x7 x71 ⟶ False) ⟶ x68 x71 ⟶ (x28 x71 x3 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x71 x72 ⟶ x0 x72 x71 ⟶ False) ⟶ (x58 (x64 x25) (x64 x25) x22 x23 = x58 (x64 x25) (x64 x25) x24 x23 ⟶ False) ⟶ (x66 x25 x26 (x58 (x64 x25) (x64 x25) x22 x26) x23 ⟶ False) ⟶ ((x58 (x64 x25) (x64 x25) x22 x26 = x58 (x64 x25) (x64 x25) x24 x26 ⟶ False) ⟶ False) ⟶ ((x60 x24 x25 ⟶ False) ⟶ False) ⟶ ((x60 x22 x25 ⟶ False) ⟶ False) ⟶ ((x2 x24 (x1 (x61 (x64 x25) (x64 x25))) ⟶ False) ⟶ False) ⟶ ((x55 x24 (x64 x25) (x64 x25) ⟶ False) ⟶ False) ⟶ ((x62 x24 (x64 x25) (x64 x25) ⟶ False) ⟶ False) ⟶ ((x54 x24 ⟶ False) ⟶ False) ⟶ ((x2 x22 (x1 (x61 (x64 x25) (x64 x25))) ⟶ False) ⟶ False) ⟶ ((x55 x22 (x64 x25) (x64 x25) ⟶ False) ⟶ False) ⟶ ((x62 x22 (x64 x25) (x64 x25) ⟶ False) ⟶ False) ⟶ ((x54 x22 ⟶ False) ⟶ False) ⟶ ((x2 x23 (x64 x25) ⟶ False) ⟶ False) ⟶ ((x2 x26 (x64 x25) ⟶ False) ⟶ False) ⟶ ((x67 x25 ⟶ False) ⟶ False) ⟶ ((x63 x25 ⟶ False) ⟶ False) ⟶ (x68 x25 ⟶ False) ⟶ False (proof)