Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../8e9d6..
PUg4P../acf13..
vout
PrPhD../a9e0e.. 102.63 bars
TMRSU../38528.. ownership of a5502.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMbHv../4959a.. ownership of fc8ba.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUefL../cf464.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem a5502.. : ∀ 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 . x73 x75 ⟶ (x75 = x74 ⟶ False) ⟶ x73 x74 ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x74 = x72 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x74 x75 ⟶ x2 x75 (x1 x76) ⟶ x73 x76 ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x75 x76 ⟶ x2 x76 (x1 x74) ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 x74 ⟶ (x2 x75 (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 x74) ⟶ (x3 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x75 x76 ⟶ x0 x74 x76 ⟶ x0 x74 (x4 x76 x75) ⟶ False) ⟶ (∀ x74 x75 . x0 x75 x74 ⟶ (x0 (x4 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x74 x75 ⟶ (x73 x75 ⟶ False) ⟶ (x0 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x75 x74 ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (x73 x5 ⟶ False) ⟶ (∀ x74 . (x3 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x10 x74 x77 x76 ⟶ (x11 x77 x76 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x68 x75 x74 = x69 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x17 x75 x74 = x16 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x63 x74 ⟶ x67 x74 x77 x76 ⟶ x2 x74 (x1 (x66 x77 x76)) ⟶ x2 x75 x77 ⟶ (x65 x77 x76 x74 x75 = x64 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ x73 (x18 x74) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ (x2 (x18 x74) (x1 (x62 x74)) ⟶ False) ⟶ False) ⟶ (x15 x20 ⟶ False) ⟶ (x6 x20 ⟶ False) ⟶ ((x12 x20 ⟶ False) ⟶ False) ⟶ (x61 x60 ⟶ False) ⟶ ((x21 x60 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x59 x74 ⟶ False) ⟶ x19 x74 ⟶ x58 (x57 x74) ⟶ False) ⟶ (∀ x74 . (x59 x74 ⟶ False) ⟶ x19 x74 ⟶ (x2 (x57 x74) (x1 (x62 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ (x58 (x56 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ x73 (x56 x74) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ (x2 (x56 x74) (x1 (x62 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x22 (x23 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x55 (x23 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x23 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 (x23 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x23 x74 x75) (x1 (x66 x75 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x67 (x54 x74 x75) x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x63 (x54 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x22 (x54 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x55 (x54 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x54 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x54 x74 x75) (x1 (x66 x75 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 . (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x12 x78 ⟶ x2 x74 (x62 x78) ⟶ x2 x77 (x62 x78) ⟶ x2 x75 (x70 x78) ⟶ x76 = x75 ⟶ x17 x78 x75 = x74 ⟶ x68 x78 x75 = x77 ⟶ (x0 x76 (x53 x78 x74 x77) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ x0 x75 (x53 x77 x74 x76) ⟶ (x68 x77 (x25 x76 x74 x77 x75) = x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ x0 x75 (x53 x77 x74 x76) ⟶ (x17 x77 (x25 x76 x74 x77 x75) = x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ x0 x75 (x53 x77 x74 x76) ⟶ (x75 = x25 x76 x74 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ x0 x75 (x53 x77 x74 x76) ⟶ (x2 (x25 x76 x74 x77 x75) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x26 x74 ⟶ False) ⟶ x19 x74 ⟶ x27 (x62 x74) ⟶ False) ⟶ (∀ x74 . x26 x74 ⟶ x19 x74 ⟶ (x27 (x62 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . x59 x74 ⟶ x19 x74 ⟶ (x58 (x62 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x59 x74 ⟶ False) ⟶ x19 x74 ⟶ x58 (x62 x74) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x13 x75 ⟶ x12 x75 ⟶ x2 x74 (x62 x75) ⟶ x73 (x28 x75 x74 x74) ⟶ False) ⟶ (∀ x74 . (x6 x74 ⟶ False) ⟶ x19 x74 ⟶ x73 (x62 x74) ⟶ False) ⟶ (∀ x74 . (x61 x74 ⟶ False) ⟶ x21 x74 ⟶ x58 (x70 x74) ⟶ False) ⟶ (∀ x74 . x61 x74 ⟶ x21 x74 ⟶ (x58 (x70 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . x6 x74 ⟶ x19 x74 ⟶ (x73 (x62 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x15 x74 ⟶ False) ⟶ x21 x74 ⟶ x73 (x70 x74) ⟶ False) ⟶ (∀ x74 . x15 x74 ⟶ x21 x74 ⟶ (x73 (x70 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ (x6 x74 ⟶ False) ⟶ (x15 x74 ⟶ False) ⟶ x7 x74 ⟶ x14 x74 ⟶ x8 x74 ⟶ x13 x74 ⟶ x9 x74 ⟶ x12 x74 ⟶ (x10 (x52 x74 x75) x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x29 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x10 x74 x77 x76 ⟶ (x51 (x50 x74 x75 x76 x77) x77 x76 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x12 x76 ⟶ x2 x74 (x62 x76) ⟶ x2 x75 (x62 x76) ⟶ (x30 (x31 x75 x74 x76) x76 x74 x75 ⟶ False) ⟶ False) ⟶ ((x21 x49 ⟶ False) ⟶ False) ⟶ ((x19 x32 ⟶ False) ⟶ False) ⟶ ((x71 x48 ⟶ False) ⟶ False) ⟶ ((x12 x33 ⟶ False) ⟶ False) ⟶ ((x73 x47 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x10 x74 x76 x75 ⟶ (x2 x74 (x1 (x66 (x70 x76) (x70 x75))) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x10 x74 x76 x75 ⟶ (x67 x74 (x70 x76) (x70 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x10 x74 x76 x75 ⟶ (x63 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 . (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x7 x78 ⟶ x14 x78 ⟶ x8 x78 ⟶ x13 x78 ⟶ x9 x78 ⟶ x12 x78 ⟶ (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ x10 x76 x78 x77 ⟶ x10 x74 x78 x77 ⟶ x51 x75 x78 x77 x76 x74 ⟶ (x2 x75 (x1 (x66 (x62 x78) (x70 x77))) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 . (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x7 x78 ⟶ x14 x78 ⟶ x8 x78 ⟶ x13 x78 ⟶ x9 x78 ⟶ x12 x78 ⟶ (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ x10 x76 x78 x77 ⟶ x10 x74 x78 x77 ⟶ x51 x75 x78 x77 x76 x74 ⟶ (x67 x75 (x62 x78) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 . (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x7 x78 ⟶ x14 x78 ⟶ x8 x78 ⟶ x13 x78 ⟶ x9 x78 ⟶ x12 x78 ⟶ (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ x10 x76 x78 x77 ⟶ x10 x74 x78 x77 ⟶ x51 x75 x78 x77 x76 x74 ⟶ (x63 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ x30 x75 x77 x74 x76 ⟶ (x2 x75 (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ (x19 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x71 x74 ⟶ (x21 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x71 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x2 x74 (x62 x77) ⟶ (x2 (x34 x77 x76 x75 x74) (x62 x76) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x63 x74 ⟶ x67 x74 (x70 x76) (x70 x75) ⟶ x2 x74 (x1 (x66 (x70 x76) (x70 x75))) ⟶ (x2 (x46 x76 x75 x74) (x1 (x66 (x62 x76) (x62 x75))) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x63 x74 ⟶ x67 x74 (x70 x76) (x70 x75) ⟶ x2 x74 (x1 (x66 (x70 x76) (x70 x75))) ⟶ (x67 (x46 x76 x75 x74) (x62 x76) (x62 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x7 x75 ⟶ x14 x75 ⟶ x8 x75 ⟶ x13 x75 ⟶ x9 x75 ⟶ x12 x75 ⟶ x63 x74 ⟶ x67 x74 (x70 x76) (x70 x75) ⟶ x2 x74 (x1 (x66 (x70 x76) (x70 x75))) ⟶ (x63 (x46 x76 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 x79 . (x6 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x7 x79 ⟶ x14 x79 ⟶ x8 x79 ⟶ x13 x79 ⟶ x9 x79 ⟶ x12 x79 ⟶ (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x7 x78 ⟶ x14 x78 ⟶ x8 x78 ⟶ x13 x78 ⟶ x9 x78 ⟶ x12 x78 ⟶ x10 x77 x79 x78 ⟶ x10 x74 x79 x78 ⟶ x51 x76 x79 x78 x77 x74 ⟶ x2 x75 (x62 x79) ⟶ (x30 (x35 x79 x78 x77 x74 x76 x75) x78 (x34 x79 x78 x77 x75) (x34 x79 x78 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x2 (x68 x75 x74) (x62 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x6 x75 ⟶ False) ⟶ (x15 x75 ⟶ False) ⟶ x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x2 (x17 x75 x74) (x62 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x63 x74 ⟶ x67 x74 x77 x76 ⟶ x2 x74 (x1 (x66 x77 x76)) ⟶ x2 x75 x77 ⟶ (x2 (x65 x77 x76 x74 x75) x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x2 (x69 x75 x74) (x62 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x12 x76 ⟶ x2 x74 (x62 x76) ⟶ x2 x75 (x62 x76) ⟶ (x2 (x28 x76 x74 x75) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x71 x75 ⟶ x2 x74 (x70 x75) ⟶ (x2 (x16 x75 x74) (x62 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ (x28 x77 x74 x76 = x72 ⟶ False) ⟶ x2 x75 (x70 x77) ⟶ x0 x75 (x28 x77 x74 x76) ⟶ (x30 x75 x77 x74 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x12 x77 ⟶ x2 x74 (x62 x77) ⟶ x2 x76 (x62 x77) ⟶ (x28 x77 x74 x76 = x72 ⟶ False) ⟶ x2 x75 (x70 x77) ⟶ x30 x75 x77 x74 x76 ⟶ (x0 x75 (x28 x77 x74 x76) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x12 x76 ⟶ x2 x74 (x62 x76) ⟶ x2 x75 (x62 x76) ⟶ (x28 x76 x74 x75 = x53 x76 x74 x75 ⟶ False) ⟶ False) ⟶ ((x72 = x47 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x10 x74 x77 x76 ⟶ (x28 x76 (x34 x77 x76 x75 (x45 x74 x75 x76 x77)) (x34 x77 x76 x74 (x45 x74 x75 x76 x77)) = x72 ⟶ False) ⟶ (x11 x77 x76 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x10 x74 x77 x76 ⟶ (x2 (x45 x74 x75 x76 x77) (x62 x77) ⟶ False) ⟶ (x11 x77 x76 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 x78 . (x6 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x7 x78 ⟶ x14 x78 ⟶ x8 x78 ⟶ x13 x78 ⟶ x9 x78 ⟶ x12 x78 ⟶ (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ x10 x76 x78 x77 ⟶ x10 x74 x78 x77 ⟶ x11 x78 x77 x76 x74 ⟶ x2 x75 (x62 x78) ⟶ x28 x77 (x34 x78 x77 x76 x75) (x34 x78 x77 x74 x75) = x72 ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x6 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x7 x77 ⟶ x14 x77 ⟶ x8 x77 ⟶ x13 x77 ⟶ x9 x77 ⟶ x12 x77 ⟶ (x6 x76 ⟶ False) ⟶ (x15 x76 ⟶ False) ⟶ x7 x76 ⟶ x14 x76 ⟶ x8 x76 ⟶ x13 x76 ⟶ x9 x76 ⟶ x12 x76 ⟶ x10 x75 x77 x76 ⟶ x2 x74 (x62 x77) ⟶ (x34 x77 x76 x75 x74 = x65 (x62 x77) (x62 x76) (x46 x77 x76 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x44 x74 x72 ⟶ (x6 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x6 x74 ⟶ (x44 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x66 x76 x74)) ⟶ x63 x75 ⟶ x67 x75 x76 x74 ⟶ (x67 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x66 x76 x74)) ⟶ x63 x75 ⟶ x67 x75 x76 x74 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x66 x76 x74)) ⟶ x63 x75 ⟶ x67 x75 x76 x74 ⟶ (x63 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x26 x74 ⟶ False) ⟶ x59 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x59 x74 ⟶ (x26 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x26 x74 ⟶ False) ⟶ x26 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x26 x74 ⟶ False) ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x6 x74 ⟶ (x26 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x6 x74 ⟶ (x6 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x66 x75 x76)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x66 x74 x74)) ⟶ x67 x75 x74 x74 ⟶ (x43 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x66 x76 x75)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x2 x74 (x1 (x66 x75 x76)) ⟶ x67 x74 x75 x76 ⟶ (x43 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x59 x74 ⟶ False) ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x66 x74 x75)) ⟶ (x22 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x66 x75 x74)) ⟶ (x55 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x66 x76 x75)) ⟶ x67 x74 x76 x75 ⟶ (x43 x74 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ (x15 x74 ⟶ False) ⟶ x61 x74 ⟶ (x9 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ (x15 x74 ⟶ False) ⟶ x61 x74 ⟶ (x8 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ (x15 x74 ⟶ False) ⟶ x61 x74 ⟶ x15 x74 ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ (x15 x74 ⟶ False) ⟶ x61 x74 ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x6 x74 ⟶ (x59 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x66 x74 x75)) ⟶ (x24 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x75 (x1 (x66 x76 x74)) ⟶ x43 x75 x76 ⟶ (x67 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ x59 x74 ⟶ (x15 x74 ⟶ False) ⟶ (x13 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ x59 x74 ⟶ (x15 x74 ⟶ False) ⟶ (x14 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ x59 x74 ⟶ (x15 x74 ⟶ False) ⟶ x15 x74 ⟶ False) ⟶ (∀ x74 . x12 x74 ⟶ (x6 x74 ⟶ False) ⟶ x59 x74 ⟶ (x15 x74 ⟶ False) ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x59 x74 ⟶ False) ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ x15 x74 ⟶ (x61 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ (x15 x74 ⟶ False) ⟶ x42 x74 ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ x6 x74 ⟶ x42 x74 ⟶ (x15 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ x15 x74 ⟶ (x42 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x21 x74 ⟶ (x6 x74 ⟶ False) ⟶ (x42 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x44 x74 x5 ⟶ (x59 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ x44 x74 x5 ⟶ x6 x74 ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x6 x74 ⟶ False) ⟶ x59 x74 ⟶ (x44 x74 x5 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x0 x75 x74 ⟶ False) ⟶ (x0 (x35 x37 x41 x40 x39 x36 x38) (x28 x41 (x34 x37 x41 x40 x38) (x34 x37 x41 x39 x38)) ⟶ False) ⟶ ((x2 x38 (x62 x37) ⟶ False) ⟶ False) ⟶ ((x51 x36 x37 x41 x40 x39 ⟶ False) ⟶ False) ⟶ ((x11 x37 x41 x40 x39 ⟶ False) ⟶ False) ⟶ ((x10 x39 x37 x41 ⟶ False) ⟶ False) ⟶ ((x10 x40 x37 x41 ⟶ False) ⟶ False) ⟶ ((x12 x41 ⟶ False) ⟶ False) ⟶ ((x9 x41 ⟶ False) ⟶ False) ⟶ ((x13 x41 ⟶ False) ⟶ False) ⟶ ((x8 x41 ⟶ False) ⟶ False) ⟶ ((x14 x41 ⟶ False) ⟶ False) ⟶ ((x7 x41 ⟶ False) ⟶ False) ⟶ (x15 x41 ⟶ False) ⟶ (x6 x41 ⟶ False) ⟶ ((x12 x37 ⟶ False) ⟶ False) ⟶ ((x9 x37 ⟶ False) ⟶ False) ⟶ ((x13 x37 ⟶ False) ⟶ False) ⟶ ((x8 x37 ⟶ False) ⟶ False) ⟶ ((x14 x37 ⟶ False) ⟶ False) ⟶ ((x7 x37 ⟶ False) ⟶ False) ⟶ (x15 x37 ⟶ False) ⟶ (x6 x37 ⟶ False) ⟶ False (proof)