Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../da9ac..
PULST../0b2b6..
vout
PrPhD../7f39f.. 3.37 bars
TMQCp../4c083.. ownership of fb310.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMKZM../09641.. ownership of 765ba.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUbZm../0bfb8.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem fb310.. : ∀ 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 x75 x76 . (x1 x76 ⟶ False) ⟶ x14 x76 ⟶ x2 x76 ⟶ x12 x72 (x13 x76) ⟶ x3 x75 ⟶ x11 x75 (x13 x76) (x13 x76) ⟶ x4 x75 (x13 x76) (x13 x76) ⟶ x12 x75 (x9 (x10 (x13 x76) (x13 x76))) ⟶ x5 x75 x76 ⟶ x8 (x13 x76) (x13 x76) x75 x72 = x72 ⟶ x6 x76 x72 (x7 x75 x72 x76) x72 (x8 (x13 x76) (x13 x76) x75 (x7 x75 x72 x76)) ⟶ x12 x73 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ (x6 x76 x73 x74 (x8 (x13 x76) (x13 x76) x75 x73) (x8 (x13 x76) (x13 x76) x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x1 x76 ⟶ False) ⟶ x14 x76 ⟶ x2 x76 ⟶ x12 x72 (x13 x76) ⟶ x3 x75 ⟶ x11 x75 (x13 x76) (x13 x76) ⟶ x4 x75 (x13 x76) (x13 x76) ⟶ x12 x75 (x9 (x10 (x13 x76) (x13 x76))) ⟶ x5 x75 x76 ⟶ x8 (x13 x76) (x13 x76) x75 x72 = x72 ⟶ (x12 (x7 x75 x72 x76) (x13 x76) ⟶ False) ⟶ x12 x73 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ (x6 x76 x73 x74 (x8 (x13 x76) (x13 x76) x75 x73) (x8 (x13 x76) (x13 x76) x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x72 x73 ⟶ x12 x73 (x9 x74) ⟶ x71 x74 ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x1 x75 ⟶ False) ⟶ x14 x75 ⟶ x2 x75 ⟶ x12 x72 (x13 x75) ⟶ x12 x74 (x13 x75) ⟶ x3 x73 ⟶ x11 x73 (x13 x75) (x13 x75) ⟶ x4 x73 (x13 x75) (x13 x75) ⟶ x12 x73 (x9 (x10 (x13 x75) (x13 x75))) ⟶ x5 x73 x75 ⟶ x8 (x13 x75) (x13 x75) x73 x72 = x72 ⟶ x69 x75 x74 x72 (x8 (x13 x75) (x13 x75) x73 x74) ⟶ (x74 = x72 ⟶ False) ⟶ (x68 x73 x75 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x16 x72 x73 ⟶ (x15 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x73 x74 ⟶ x12 x74 (x9 x72) ⟶ (x12 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x17 x73 x72 ⟶ (x12 x73 (x9 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x12 x73 (x9 x72) ⟶ (x17 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x18 x73 (x19 x72 x73) (x20 x72 x73) (x8 (x13 x73) (x13 x73) x72 (x19 x72 x73)) (x8 (x13 x73) (x13 x73) x72 (x20 x72 x73)) ⟶ (x5 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ (x12 (x20 x72 x73) (x13 x73) ⟶ False) ⟶ (x5 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ (x12 (x19 x72 x73) (x13 x73) ⟶ False) ⟶ (x5 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x1 x75 ⟶ False) ⟶ x14 x75 ⟶ x2 x75 ⟶ x3 x72 ⟶ x11 x72 (x13 x75) (x13 x75) ⟶ x4 x72 (x13 x75) (x13 x75) ⟶ x12 x72 (x9 (x10 (x13 x75) (x13 x75))) ⟶ x5 x72 x75 ⟶ x12 x74 (x13 x75) ⟶ x12 x73 (x13 x75) ⟶ (x18 x75 x74 x73 (x8 (x13 x75) (x13 x75) x72 x74) (x8 (x13 x75) (x13 x75) x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x12 x72 x73 ⟶ (x71 x73 ⟶ False) ⟶ (x0 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x1 x76 ⟶ False) ⟶ x14 x76 ⟶ x2 x76 ⟶ x12 x72 (x13 x76) ⟶ x12 x75 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x6 x76 x72 x75 x73 x74 ⟶ (x6 x76 x74 x73 x75 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x1 x76 ⟶ False) ⟶ x14 x76 ⟶ x2 x76 ⟶ x12 x72 (x13 x76) ⟶ x12 x75 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x6 x76 x72 x75 x73 x74 ⟶ (x6 x76 x73 x74 x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x1 x76 ⟶ False) ⟶ x14 x76 ⟶ x2 x76 ⟶ x12 x72 (x13 x76) ⟶ x12 x75 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x6 x76 x72 x75 x73 x74 ⟶ (x6 x76 x75 x72 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x6 x73 (x21 x72 x73) (x22 x72 x73) (x8 (x13 x73) (x13 x73) x72 (x21 x72 x73)) (x8 (x13 x73) (x13 x73) x72 (x22 x72 x73)) ⟶ (x15 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ (x12 (x22 x72 x73) (x13 x73) ⟶ False) ⟶ (x15 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ (x12 (x21 x72 x73) (x13 x73) ⟶ False) ⟶ (x15 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x1 x75 ⟶ False) ⟶ x14 x75 ⟶ x2 x75 ⟶ x3 x72 ⟶ x11 x72 (x13 x75) (x13 x75) ⟶ x4 x72 (x13 x75) (x13 x75) ⟶ x12 x72 (x9 (x10 (x13 x75) (x13 x75))) ⟶ x15 x72 x75 ⟶ x12 x74 (x13 x75) ⟶ x12 x73 (x13 x75) ⟶ (x6 x75 x74 x73 (x8 (x13 x75) (x13 x75) x72 x74) (x8 (x13 x75) (x13 x75) x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x0 x73 x72 ⟶ (x12 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . x3 x75 ⟶ x11 x75 x72 x73 ⟶ x12 x75 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x11 x74 x72 x73 ⟶ x12 x74 (x9 (x10 x72 x73)) ⟶ x67 x72 x73 x75 x74 ⟶ (x67 x72 x73 x74 x75 ⟶ False) ⟶ False) ⟶ (x71 x23 ⟶ False) ⟶ (∀ x72 x73 x74 x75 . x3 x75 ⟶ x11 x75 x72 x73 ⟶ x12 x75 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x11 x74 x72 x73 ⟶ x12 x74 (x9 (x10 x72 x73)) ⟶ (x67 x72 x73 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x17 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . x3 x75 ⟶ x11 x75 x72 x73 ⟶ x12 x75 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x11 x74 x72 x73 ⟶ x12 x74 (x9 (x10 x72 x73)) ⟶ x75 = x74 ⟶ (x67 x72 x73 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . x3 x75 ⟶ x11 x75 x72 x73 ⟶ x12 x75 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x11 x74 x72 x73 ⟶ x12 x74 (x9 (x10 x72 x73)) ⟶ x67 x72 x73 x75 x74 ⟶ (x75 = x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x66 x72 = x65 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x71 x75 ⟶ False) ⟶ x3 x72 ⟶ x11 x72 x75 x74 ⟶ x12 x72 (x9 (x10 x75 x74)) ⟶ x12 x73 x75 ⟶ (x8 x75 x74 x72 x73 = x24 x72 x73 ⟶ False) ⟶ False) ⟶ ((x64 x63 ⟶ False) ⟶ False) ⟶ (x71 x63 ⟶ False) ⟶ (∀ x72 x73 . (x3 (x62 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x25 (x62 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x61 (x62 x73 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x26 (x62 x72 x73) ⟶ False) ⟶ False) ⟶ (x60 x59 ⟶ False) ⟶ ((x3 x59 ⟶ False) ⟶ False) ⟶ ((x26 x59 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ x71 (x28 x72) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ (x12 (x28 x72) (x9 (x13 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x71 (x30 x72 x73) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ (x3 (x30 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ (x25 (x30 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ (x61 (x30 x72 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ (x26 (x30 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 x73 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ (x12 (x30 x72 x73) (x9 (x10 x73 x72)) ⟶ False) ⟶ False) ⟶ (x71 x31 ⟶ False) ⟶ (∀ x72 . (x58 (x57 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x32 (x57 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x56 (x57 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x33 (x57 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x55 (x57 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x25 (x57 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x61 (x57 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x57 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x12 (x57 x72) (x9 (x10 x72 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x4 (x34 x72) x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x11 (x34 x72) x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x58 (x34 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x3 (x34 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x25 (x34 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x61 (x34 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x34 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x12 (x34 x72) (x9 (x10 x72 x72)) ⟶ False) ⟶ False) ⟶ ((x35 x36 ⟶ False) ⟶ False) ⟶ ((x3 x36 ⟶ False) ⟶ False) ⟶ ((x26 x36 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x1 x72 ⟶ False) ⟶ x29 x72 ⟶ x54 (x53 x72) ⟶ False) ⟶ (∀ x72 . (x1 x72 ⟶ False) ⟶ x29 x72 ⟶ (x12 (x53 x72) (x9 (x13 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ (x54 (x52 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ x71 (x52 x72) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ (x12 (x52 x72) (x9 (x13 x72)) ⟶ False) ⟶ False) ⟶ ((x71 x37 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x25 (x51 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x61 (x51 x73 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x26 (x51 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x71 (x51 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x12 (x51 x72 x73) (x9 (x10 x73 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x3 (x38 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x25 (x38 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x61 (x38 x73 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x26 (x38 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x12 (x38 x72 x73) (x9 (x10 x73 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x11 (x50 x72 x73) x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x3 (x50 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x25 (x50 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x61 (x50 x73 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x26 (x50 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x12 (x50 x72 x73) (x9 (x10 x73 x72)) ⟶ False) ⟶ False) ⟶ ((x3 x49 ⟶ False) ⟶ False) ⟶ ((x26 x49 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x48 x72 ⟶ False) ⟶ x29 x72 ⟶ x47 (x13 x72) ⟶ False) ⟶ (∀ x72 . x48 x72 ⟶ x29 x72 ⟶ (x47 (x13 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . x1 x72 ⟶ x29 x72 ⟶ (x54 (x13 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x71 x72 ⟶ False) ⟶ x71 (x65 x72) ⟶ False) ⟶ (∀ x72 . (x1 x72 ⟶ False) ⟶ x29 x72 ⟶ x54 (x13 x72) ⟶ False) ⟶ (∀ x72 . (x35 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x32 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x56 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x33 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x3 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x27 x72 ⟶ False) ⟶ x29 x72 ⟶ x71 (x13 x72) ⟶ False) ⟶ ((x71 x70 ⟶ False) ⟶ False) ⟶ (∀ x72 . x27 x72 ⟶ x29 x72 ⟶ (x71 (x13 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x64 x74 ⟶ x26 x72 ⟶ x25 x72 x74 ⟶ x3 x72 ⟶ (x3 (x24 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x64 x74 ⟶ x26 x72 ⟶ x25 x72 x74 ⟶ x3 x72 ⟶ (x26 (x24 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x58 (x65 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x3 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x61 (x65 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x12 (x39 x72) x72 ⟶ False) ⟶ False) ⟶ ((x29 x46 ⟶ False) ⟶ False) ⟶ ((x2 x40 ⟶ False) ⟶ False) ⟶ (∀ x72 . x2 x72 ⟶ (x29 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x12 (x66 x72) (x9 (x10 x72 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x58 (x66 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x26 (x65 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x71 x75 ⟶ False) ⟶ x3 x72 ⟶ x11 x72 x75 x74 ⟶ x12 x72 (x9 (x10 x75 x74)) ⟶ x12 x73 x75 ⟶ (x12 (x8 x75 x74 x72 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x5 x72 x73 ⟶ (x41 x72 x73 = x8 (x13 x73) (x13 x73) x72 (x41 x72 x73) ⟶ False) ⟶ (x16 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x5 x72 x73 ⟶ (x12 (x41 x72 x73) (x13 x73) ⟶ False) ⟶ (x16 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x5 x72 x73 ⟶ x67 (x13 x73) (x13 x73) x72 (x66 (x13 x73)) ⟶ (x16 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x1 x74 ⟶ False) ⟶ x14 x74 ⟶ x2 x74 ⟶ x3 x72 ⟶ x11 x72 (x13 x74) (x13 x74) ⟶ x4 x72 (x13 x74) (x13 x74) ⟶ x12 x72 (x9 (x10 (x13 x74) (x13 x74))) ⟶ x16 x72 x74 ⟶ (x67 (x13 x74) (x13 x74) x72 (x66 (x13 x74)) ⟶ False) ⟶ x12 x73 (x13 x74) ⟶ x73 = x8 (x13 x74) (x13 x74) x72 x73 ⟶ False) ⟶ (∀ x72 x73 . (x1 x73 ⟶ False) ⟶ x14 x73 ⟶ x2 x73 ⟶ x3 x72 ⟶ x11 x72 (x13 x73) (x13 x73) ⟶ x4 x72 (x13 x73) (x13 x73) ⟶ x12 x72 (x9 (x10 (x13 x73) (x13 x73))) ⟶ x16 x72 x73 ⟶ (x5 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x27 x76 ⟶ False) ⟶ x2 x76 ⟶ x12 x75 (x13 x76) ⟶ x12 x72 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x6 x76 x75 x72 x73 x74 ⟶ (x18 x76 x75 x72 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x27 x76 ⟶ False) ⟶ x2 x76 ⟶ x12 x75 (x13 x76) ⟶ x12 x72 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x6 x76 x75 x72 x74 x73 ⟶ (x18 x76 x75 x72 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 x76 . (x27 x76 ⟶ False) ⟶ x2 x76 ⟶ x12 x75 (x13 x76) ⟶ x12 x72 (x13 x76) ⟶ x12 x74 (x13 x76) ⟶ x12 x73 (x13 x76) ⟶ x18 x76 x75 x72 x74 x73 ⟶ (x6 x76 x75 x72 x74 x73 ⟶ False) ⟶ (x6 x76 x75 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x27 x75 ⟶ False) ⟶ x2 x75 ⟶ x12 x74 (x13 x75) ⟶ x12 x72 (x13 x75) ⟶ x12 x73 (x13 x75) ⟶ x6 x75 x74 x72 x72 x73 ⟶ (x69 x75 x74 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 x75 . (x27 x75 ⟶ False) ⟶ x2 x75 ⟶ x12 x74 (x13 x75) ⟶ x12 x72 (x13 x75) ⟶ x12 x73 (x13 x75) ⟶ x69 x75 x74 x72 x73 ⟶ (x6 x75 x74 x72 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x42 x72 x70 ⟶ (x27 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x64 x73 ⟶ x12 x72 (x9 x73) ⟶ (x64 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x27 x72 ⟶ (x42 x72 x70 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x12 x73 (x9 (x10 x74 x72)) ⟶ x3 x73 ⟶ x11 x73 x74 x72 ⟶ (x11 x73 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x12 x73 (x9 (x10 x74 x72)) ⟶ x3 x73 ⟶ x11 x73 x74 x72 ⟶ x71 x73 ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ (x71 x72 ⟶ False) ⟶ x12 x73 (x9 (x10 x74 x72)) ⟶ x3 x73 ⟶ x11 x73 x74 x72 ⟶ (x3 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x64 x73 ⟶ x12 x72 x73 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x64 x73 ⟶ x12 x72 x73 ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x48 x72 ⟶ False) ⟶ x1 x72 ⟶ False) ⟶ (∀ x72 x73 . x12 x73 (x9 (x10 x72 x72)) ⟶ x55 x73 ⟶ x3 x73 ⟶ x58 x73 x72 ⟶ x11 x73 x72 x72 ⟶ (x4 x73 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x12 x73 (x9 (x10 x72 x72)) ⟶ x55 x73 ⟶ x3 x73 ⟶ x58 x73 x72 ⟶ x11 x73 x72 x72 ⟶ (x11 x73 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x12 x73 (x9 (x10 x72 x72)) ⟶ x55 x73 ⟶ x3 x73 ⟶ x58 x73 x72 ⟶ x11 x73 x72 x72 ⟶ (x3 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x64 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x1 x72 ⟶ (x48 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x35 x74 ⟶ x43 x74 x73 ⟶ (x4 x74 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x72 x73)) ⟶ x3 x74 ⟶ x35 x74 ⟶ x43 x74 x73 ⟶ (x3 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . x54 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x60 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x54 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x54 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x48 x72 ⟶ False) ⟶ x48 x72 ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x48 x72 ⟶ False) ⟶ x27 x72 ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x73 x72)) ⟶ x3 x74 ⟶ x4 x74 x73 x72 ⟶ (x43 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x73 x72)) ⟶ x3 x74 ⟶ x4 x74 x73 x72 ⟶ (x35 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x73 x72)) ⟶ x3 x74 ⟶ x4 x74 x73 x72 ⟶ (x3 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . x26 x72 ⟶ x3 x72 ⟶ (x60 x72 ⟶ False) ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x26 x72 ⟶ x3 x72 ⟶ (x60 x72 ⟶ False) ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x26 x72 ⟶ x3 x72 ⟶ (x60 x72 ⟶ False) ⟶ x54 x72 ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x27 x72 ⟶ (x48 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x27 x72 ⟶ (x27 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x71 x74 ⟶ x12 x72 (x9 (x10 x73 x74)) ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x12 x73 (x9 (x10 x72 x72)) ⟶ x11 x73 x72 x72 ⟶ (x58 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x60 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x71 x74 ⟶ x12 x72 (x9 (x10 x74 x73)) ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x26 x72 ⟶ x33 x72 ⟶ x32 x72 ⟶ (x55 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x26 x72 ⟶ x33 x72 ⟶ x32 x72 ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ x12 x72 (x9 (x10 x73 x74)) ⟶ x11 x72 x73 x74 ⟶ (x58 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x26 x73 ⟶ x3 x73 ⟶ x12 x72 (x9 x73) ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x1 x72 ⟶ False) ⟶ x27 x72 ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x72 x73)) ⟶ (x25 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x73 x72)) ⟶ (x61 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x71 x74 ⟶ False) ⟶ x71 x72 ⟶ x12 x73 (x9 (x10 x74 x72)) ⟶ x58 x73 x74 ⟶ False) ⟶ (∀ x72 x73 x74 . x71 x74 ⟶ x12 x72 (x9 (x10 x74 x73)) ⟶ x11 x72 x74 x73 ⟶ (x58 x72 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x35 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ x26 x72 ⟶ x3 x72 ⟶ (x26 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x27 x72 ⟶ (x1 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x74 (x9 (x10 x72 x73)) ⟶ (x26 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x71 x74 ⟶ x12 x72 (x9 (x10 x74 x73)) ⟶ (x58 x72 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x12 x73 (x9 (x10 x74 x72)) ⟶ x58 x73 x74 ⟶ (x11 x73 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x3 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x1 x72 ⟶ False) ⟶ x27 x72 ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x42 x72 x23 ⟶ (x1 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ x42 x72 x23 ⟶ x27 x72 ⟶ False) ⟶ (∀ x72 . x29 x72 ⟶ (x27 x72 ⟶ False) ⟶ x1 x72 ⟶ (x42 x72 x23 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x0 x72 x73 ⟶ x0 x73 x72 ⟶ False) ⟶ (x68 x44 x45 ⟶ False) ⟶ (x15 x44 x45 ⟶ False) ⟶ ((x5 x44 x45 ⟶ False) ⟶ False) ⟶ ((x12 x44 (x9 (x10 (x13 x45) (x13 x45))) ⟶ False) ⟶ False) ⟶ ((x4 x44 (x13 x45) (x13 x45) ⟶ False) ⟶ False) ⟶ ((x11 x44 (x13 x45) (x13 x45) ⟶ False) ⟶ False) ⟶ ((x3 x44 ⟶ False) ⟶ False) ⟶ ((x2 x45 ⟶ False) ⟶ False) ⟶ ((x14 x45 ⟶ False) ⟶ False) ⟶ (x1 x45 ⟶ False) ⟶ False (proof)