Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../95d63..
PUf5Y../60df1..
vout
PrPhD../744d7.. 102.64 bars
TMWm9../d7996.. ownership of ed1ff.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMREv../23254.. ownership of 6a902.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUMYL../fca70.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem ed1ff.. : ∀ 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 . x74 x76 ⟶ (x76 = x75 ⟶ False) ⟶ x74 x75 ⟶ False) ⟶ (∀ x75 x76 . x0 x75 x76 ⟶ x74 x76 ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ (x75 = x73 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x0 x75 x76 ⟶ x2 x76 (x1 x77) ⟶ x74 x77 ⟶ False) ⟶ (∀ x75 x76 x77 x78 . x72 x78 ⟶ x69 x78 x75 x76 ⟶ x2 x78 (x1 (x70 x75 x76)) ⟶ x0 x77 x75 ⟶ (x76 = x73 ⟶ False) ⟶ (x0 (x71 x78 x77) x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . x3 x80 ⟶ x6 x75 x80 ⟶ x2 x79 (x4 x80) ⟶ x2 x76 (x4 x80) ⟶ x2 x78 (x4 x75) ⟶ x2 x77 (x4 x75) ⟶ x78 = x79 ⟶ x77 = x76 ⟶ x5 x75 x78 x77 ⟶ (x5 x80 x79 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x68 x77 ⟶ False) ⟶ x3 x77 ⟶ (x68 x76 ⟶ False) ⟶ x6 x76 x77 ⟶ x2 x75 (x4 x76) ⟶ (x2 x75 (x4 x77) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x0 x76 x77 ⟶ x2 x77 (x1 x75) ⟶ (x2 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x67 x76 x75 ⟶ (x2 x76 (x1 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x2 x76 (x1 x75) ⟶ (x67 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x2 x75 x76 ⟶ (x74 x76 ⟶ False) ⟶ (x0 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x0 x76 x75 ⟶ (x2 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . (x74 x80 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x72 x79 ⟶ x69 x79 x76 x80 ⟶ x2 x79 (x1 (x70 x76 x80)) ⟶ x72 x77 ⟶ x69 x77 x78 x75 ⟶ x2 x77 (x1 (x70 x78 x75)) ⟶ x66 x76 x80 x78 x75 x79 x77 ⟶ (x66 x76 x80 x78 x75 x77 x79 ⟶ False) ⟶ False) ⟶ (x74 x7 ⟶ False) ⟶ (∀ x75 . (x67 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . (x74 x80 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x72 x79 ⟶ x69 x79 x76 x80 ⟶ x2 x79 (x1 (x70 x76 x80)) ⟶ x72 x77 ⟶ x69 x77 x78 x75 ⟶ x2 x77 (x1 (x70 x78 x75)) ⟶ (x66 x76 x80 x78 x75 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . (x74 x80 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x72 x79 ⟶ x69 x79 x76 x80 ⟶ x2 x79 (x1 (x70 x76 x80)) ⟶ x72 x77 ⟶ x69 x77 x78 x75 ⟶ x2 x77 (x1 (x70 x78 x75)) ⟶ x79 = x77 ⟶ (x66 x76 x80 x78 x75 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . (x74 x80 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x72 x79 ⟶ x69 x79 x76 x80 ⟶ x2 x79 (x1 (x70 x76 x80)) ⟶ x72 x77 ⟶ x69 x77 x78 x75 ⟶ x2 x77 (x1 (x70 x78 x75)) ⟶ x66 x76 x80 x78 x75 x79 x77 ⟶ (x79 = x77 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x72 (x65 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x8 (x65 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x64 (x65 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x9 (x65 x75) ⟶ False) ⟶ False) ⟶ ((x63 x62 ⟶ False) ⟶ False) ⟶ (x74 x62 ⟶ False) ⟶ (∀ x75 x76 . (x72 (x61 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x10 (x61 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x8 (x61 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x9 (x61 x75 x76) ⟶ False) ⟶ False) ⟶ (x60 x59 ⟶ False) ⟶ ((x72 x59 ⟶ False) ⟶ False) ⟶ ((x9 x59 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ x74 (x11 x75) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ (x2 (x11 x75) (x1 (x4 x75)) ⟶ False) ⟶ False) ⟶ ((x72 x13 ⟶ False) ⟶ False) ⟶ ((x64 x13 ⟶ False) ⟶ False) ⟶ ((x9 x13 ⟶ False) ⟶ False) ⟶ (x74 x13 ⟶ False) ⟶ (∀ x75 . (x14 (x15 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x72 (x15 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x8 (x15 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x64 (x15 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x9 (x15 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x10 (x58 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x8 (x58 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x9 (x58 x75 x76) ⟶ False) ⟶ False) ⟶ ((x72 x16 ⟶ False) ⟶ False) ⟶ ((x64 x16 ⟶ False) ⟶ False) ⟶ ((x9 x16 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x14 (x57 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x72 (x57 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x10 (x57 x76 x75) x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x8 (x57 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x9 (x57 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 x76 ⟶ False) ⟶ (x2 (x57 x76 x75) (x1 (x70 x75 x76)) ⟶ False) ⟶ False) ⟶ (x74 x56 ⟶ False) ⟶ ((x64 x17 ⟶ False) ⟶ False) ⟶ ((x9 x17 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x72 x19 ⟶ False) ⟶ False) ⟶ ((x9 x19 ⟶ False) ⟶ False) ⟶ (x74 x55 ⟶ False) ⟶ ((x60 x55 ⟶ False) ⟶ False) ⟶ ((x72 x55 ⟶ False) ⟶ False) ⟶ ((x9 x55 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x54 x75 ⟶ False) ⟶ x12 x75 ⟶ x53 (x52 x75) ⟶ False) ⟶ (∀ x75 . (x54 x75 ⟶ False) ⟶ x12 x75 ⟶ (x2 (x52 x75) (x1 (x4 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ (x53 (x51 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ x74 (x51 x75) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ (x2 (x51 x75) (x1 (x4 x75)) ⟶ False) ⟶ False) ⟶ ((x74 x20 ⟶ False) ⟶ False) ⟶ (∀ x75 . x3 x75 ⟶ (x49 (x50 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x3 x75 ⟶ (x21 (x50 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x3 x75 ⟶ (x2 (x50 x75) (x1 (x4 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x10 (x22 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x8 (x22 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x9 (x22 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 (x22 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x2 (x22 x75 x76) (x1 (x70 x76 x75)) ⟶ False) ⟶ False) ⟶ ((x9 x48 ⟶ False) ⟶ False) ⟶ (x74 x48 ⟶ False) ⟶ (∀ x75 x76 . (x69 (x47 x75 x76) x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x72 (x47 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x10 (x47 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x8 (x47 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x9 (x47 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x2 (x47 x75 x76) (x1 (x70 x76 x75)) ⟶ False) ⟶ False) ⟶ ((x72 x46 ⟶ False) ⟶ False) ⟶ ((x9 x46 ⟶ False) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ ((x72 x44 ⟶ False) ⟶ False) ⟶ ((x9 x44 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x23 x75 ⟶ False) ⟶ x12 x75 ⟶ x24 (x4 x75) ⟶ False) ⟶ (∀ x75 . x23 x75 ⟶ x12 x75 ⟶ (x24 (x4 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x9 x76 ⟶ x72 x76 ⟶ x45 x76 ⟶ (x72 (x71 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x9 x76 ⟶ x72 x76 ⟶ x45 x76 ⟶ (x9 (x71 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x54 x75 ⟶ x12 x75 ⟶ (x53 (x4 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x54 x75 ⟶ False) ⟶ x12 x75 ⟶ x53 (x4 x75) ⟶ False) ⟶ (∀ x75 x76 . (x9 (x70 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x68 x75 ⟶ False) ⟶ x12 x75 ⟶ x74 (x4 x75) ⟶ False) ⟶ ((x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ x12 x75 ⟶ (x74 (x4 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x9 x76 ⟶ x25 x76 ⟶ x72 x76 ⟶ (x74 (x71 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x63 x77 ⟶ x9 x75 ⟶ x10 x75 x77 ⟶ x72 x75 ⟶ (x72 (x71 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x63 x77 ⟶ x9 x75 ⟶ x10 x75 x77 ⟶ x72 x75 ⟶ (x9 (x71 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 . x3 x75 ⟶ (x6 (x43 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x2 (x26 x75) x75 ⟶ False) ⟶ False) ⟶ ((x12 x42 ⟶ False) ⟶ False) ⟶ ((x3 x27 ⟶ False) ⟶ False) ⟶ ((x74 x41 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x3 x76 ⟶ x6 x75 x76 ⟶ (x3 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x3 x75 ⟶ (x12 x75 ⟶ False) ⟶ False) ⟶ ((x73 = x41 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . x3 x80 ⟶ x72 x75 ⟶ x69 x75 x79 (x4 x80) ⟶ x2 x75 (x1 (x70 x79 (x4 x80))) ⟶ x72 x78 ⟶ x69 x78 x79 (x4 x80) ⟶ x2 x78 (x1 (x70 x79 (x4 x80))) ⟶ x2 x76 (x4 x80) ⟶ x2 x77 (x4 x80) ⟶ x76 = x71 x75 (x39 x78 x75 x80 x79) ⟶ x77 = x71 x78 (x39 x78 x75 x80 x79) ⟶ x5 x80 x76 x77 ⟶ (x40 x79 x80 x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . x3 x78 ⟶ x72 x75 ⟶ x69 x75 x77 (x4 x78) ⟶ x2 x75 (x1 (x70 x77 (x4 x78))) ⟶ x72 x76 ⟶ x69 x76 x77 (x4 x78) ⟶ x2 x76 (x1 (x70 x77 (x4 x78))) ⟶ (x0 (x39 x76 x75 x78 x77) x77 ⟶ False) ⟶ (x40 x77 x78 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x3 x79 ⟶ x72 x75 ⟶ x69 x75 x78 (x4 x79) ⟶ x2 x75 (x1 (x70 x78 (x4 x79))) ⟶ x72 x77 ⟶ x69 x77 x78 (x4 x79) ⟶ x2 x77 (x1 (x70 x78 (x4 x79))) ⟶ x40 x78 x79 x75 x77 ⟶ x0 x76 x78 ⟶ (x5 x79 (x37 x76 x77 x75 x79 x78) (x38 x76 x77 x75 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x3 x79 ⟶ x72 x75 ⟶ x69 x75 x78 (x4 x79) ⟶ x2 x75 (x1 (x70 x78 (x4 x79))) ⟶ x72 x77 ⟶ x69 x77 x78 (x4 x79) ⟶ x2 x77 (x1 (x70 x78 (x4 x79))) ⟶ x40 x78 x79 x75 x77 ⟶ x0 x76 x78 ⟶ (x38 x76 x77 x75 x79 x78 = x71 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x3 x79 ⟶ x72 x75 ⟶ x69 x75 x78 (x4 x79) ⟶ x2 x75 (x1 (x70 x78 (x4 x79))) ⟶ x72 x77 ⟶ x69 x77 x78 (x4 x79) ⟶ x2 x77 (x1 (x70 x78 (x4 x79))) ⟶ x40 x78 x79 x75 x77 ⟶ x0 x76 x78 ⟶ (x37 x76 x77 x75 x79 x78 = x71 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x3 x79 ⟶ x72 x75 ⟶ x69 x75 x78 (x4 x79) ⟶ x2 x75 (x1 (x70 x78 (x4 x79))) ⟶ x72 x77 ⟶ x69 x77 x78 (x4 x79) ⟶ x2 x77 (x1 (x70 x78 (x4 x79))) ⟶ x40 x78 x79 x75 x77 ⟶ x0 x76 x78 ⟶ (x2 (x38 x76 x77 x75 x79 x78) (x4 x79) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x3 x79 ⟶ x72 x75 ⟶ x69 x75 x78 (x4 x79) ⟶ x2 x75 (x1 (x70 x78 (x4 x79))) ⟶ x72 x77 ⟶ x69 x77 x78 (x4 x79) ⟶ x2 x77 (x1 (x70 x78 (x4 x79))) ⟶ x40 x78 x79 x75 x77 ⟶ x0 x76 x78 ⟶ (x2 (x37 x76 x77 x75 x79 x78) (x4 x79) ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x28 x75 x73 ⟶ (x68 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x2 x75 (x1 x76) ⟶ (x63 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x68 x75 ⟶ (x28 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ (x10 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x2 x76 (x1 (x70 x77 x75)) ⟶ x72 x76 ⟶ x69 x76 x77 x75 ⟶ (x69 x76 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x2 x76 (x1 (x70 x77 x75)) ⟶ x72 x76 ⟶ x69 x76 x77 x75 ⟶ x74 x76 ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x2 x76 (x1 (x70 x77 x75)) ⟶ x72 x76 ⟶ x69 x76 x77 x75 ⟶ (x72 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x2 x75 x76 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x2 x75 x76 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x23 x75 ⟶ False) ⟶ x54 x75 ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x8 x75 x76 ⟶ (x8 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x8 x75 x76 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x74 x76 ⟶ x9 x75 ⟶ x8 x75 x76 ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ (x63 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x54 x75 ⟶ (x23 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x9 x77 ⟶ x10 x77 x75 ⟶ x2 x76 (x1 x77) ⟶ (x10 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x53 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x60 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x53 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x53 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x23 x75 ⟶ False) ⟶ x23 x75 ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x23 x75 ⟶ False) ⟶ x68 x75 ⟶ False) ⟶ (∀ x75 x76 x77 . x9 x77 ⟶ x8 x77 x75 ⟶ x2 x76 (x1 x77) ⟶ (x8 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ (x60 x75 ⟶ False) ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ (x60 x75 ⟶ False) ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ (x60 x75 ⟶ False) ⟶ x53 x75 ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x68 x75 ⟶ (x23 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x68 x75 ⟶ (x68 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x2 x75 (x1 (x70 x76 x77)) ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ (x64 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x2 x76 (x1 (x70 x75 x75)) ⟶ x69 x76 x75 x75 ⟶ (x14 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x60 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x2 x75 (x1 (x70 x77 x76)) ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ (x25 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ x2 x75 (x1 (x70 x76 x77)) ⟶ x69 x75 x76 x77 ⟶ (x14 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x9 x76 ⟶ x72 x76 ⟶ x2 x75 (x1 x76) ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x74 x75 ⟶ (x45 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x74 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x74 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x54 x75 ⟶ False) ⟶ x68 x75 ⟶ False) ⟶ (∀ x75 x76 x77 . x2 x77 (x1 (x70 x75 x76)) ⟶ (x10 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x2 x77 (x1 (x70 x76 x75)) ⟶ (x8 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x9 x76 ⟶ x2 x75 (x1 x76) ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x2 x75 (x1 (x70 x77 x76)) ⟶ x69 x75 x77 x76 ⟶ (x14 x75 x77 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x18 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ x9 x75 ⟶ x72 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x45 x75 ⟶ (x29 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x45 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x9 x75 ⟶ x72 x75 ⟶ x45 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x3 x76 ⟶ x2 x75 (x1 (x4 x76)) ⟶ x74 x75 ⟶ (x49 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x3 x76 ⟶ x2 x75 (x1 (x4 x76)) ⟶ x74 x75 ⟶ (x21 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x68 x75 ⟶ (x54 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x2 x77 (x1 (x70 x75 x76)) ⟶ (x9 x77 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x2 x76 (x1 (x70 x77 x75)) ⟶ x14 x76 x77 ⟶ (x69 x76 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ x72 x75 ⟶ (x45 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ x72 x75 ⟶ (x72 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x63 x76 ⟶ x9 x75 ⟶ x10 x75 x76 ⟶ x72 x75 ⟶ (x9 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x54 x75 ⟶ False) ⟶ x68 x75 ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x28 x75 x7 ⟶ (x54 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ x28 x75 x7 ⟶ x68 x75 ⟶ False) ⟶ (∀ x75 . x12 x75 ⟶ (x68 x75 ⟶ False) ⟶ x54 x75 ⟶ (x28 x75 x7 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x0 x75 x76 ⟶ x0 x76 x75 ⟶ False) ⟶ (x40 x30 x33 x32 x31 ⟶ False) ⟶ ((x40 x30 x34 x35 x36 ⟶ False) ⟶ False) ⟶ ((x66 x30 (x4 x33) x30 (x4 x34) x31 x36 ⟶ False) ⟶ False) ⟶ ((x66 x30 (x4 x33) x30 (x4 x34) x32 x35 ⟶ False) ⟶ False) ⟶ ((x2 x31 (x1 (x70 x30 (x4 x33))) ⟶ False) ⟶ False) ⟶ ((x69 x31 x30 (x4 x33) ⟶ False) ⟶ False) ⟶ ((x72 x31 ⟶ False) ⟶ False) ⟶ ((x2 x32 (x1 (x70 x30 (x4 x33))) ⟶ False) ⟶ False) ⟶ ((x69 x32 x30 (x4 x33) ⟶ False) ⟶ False) ⟶ ((x72 x32 ⟶ False) ⟶ False) ⟶ ((x2 x36 (x1 (x70 x30 (x4 x34))) ⟶ False) ⟶ False) ⟶ ((x69 x36 x30 (x4 x34) ⟶ False) ⟶ False) ⟶ ((x72 x36 ⟶ False) ⟶ False) ⟶ ((x2 x35 (x1 (x70 x30 (x4 x34))) ⟶ False) ⟶ False) ⟶ ((x69 x35 x30 (x4 x34) ⟶ False) ⟶ False) ⟶ ((x72 x35 ⟶ False) ⟶ False) ⟶ ((x6 x34 x33 ⟶ False) ⟶ False) ⟶ (x68 x34 ⟶ False) ⟶ ((x3 x33 ⟶ False) ⟶ False) ⟶ (x68 x33 ⟶ False) ⟶ False (proof)