Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../b26ad..
PUguL../8933e..
vout
PrPhD../f9122.. 3.41 bars
TMLar../e68e3.. ownership of d0390.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMant../8057b.. ownership of e10d3.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUcPC../d20f1.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem d0390.. : ∀ 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 . x72 x74 ⟶ (x74 = x73 ⟶ False) ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 x74 . x0 x73 x74 ⟶ x72 x74 ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x73 = x71 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x0 x73 x74 ⟶ x2 x74 (x1 x75) ⟶ x72 x75 ⟶ False) ⟶ (∀ x73 x74 x75 . x0 x74 x75 ⟶ x2 x75 (x1 x73) ⟶ (x2 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x5 (x4 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x70 x74 x73 ⟶ (x2 x74 (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x74 (x1 x73) ⟶ (x70 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x69 (x4 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x6 (x4 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x68 (x4 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 x77 x78 . (x72 x78 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x7 x77 ⟶ x13 x77 (x14 x78 x78) x78 ⟶ x2 x77 (x1 (x14 (x14 x78 x78) x78)) ⟶ x2 x74 (x3 x73) ⟶ x7 x76 ⟶ x13 x76 x73 x78 ⟶ x2 x76 (x1 (x14 x73 x78)) ⟶ x68 x77 x78 ⟶ x6 x77 x78 ⟶ x69 x77 x78 ⟶ x5 x77 x78 ⟶ x2 x75 x73 ⟶ (x11 x73 x78 x77 (x8 x73 x74 (x9 x73 x75)) x76 = x10 x78 x77 (x11 x73 x78 x77 x74 x76) (x12 x73 x78 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x73 x74 ⟶ (x72 x74 ⟶ False) ⟶ (x0 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x0 x74 x73 ⟶ (x2 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x67 x73 x71 = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x74 (x3 x75) ⟶ x2 x73 (x3 x75) ⟶ (x8 x75 x74 x73 = x67 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x7 x76 ⟶ x13 x76 (x14 x73 x73) x73 ⟶ x2 x76 (x1 (x14 (x14 x73 x73) x73)) ⟶ x2 x74 x73 ⟶ x2 x75 x73 ⟶ (x10 x73 x76 x74 x75 = x15 x76 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x7 x73 ⟶ x13 x73 x76 x75 ⟶ x2 x73 (x1 (x14 x76 x75)) ⟶ x2 x74 x76 ⟶ (x12 x76 x75 x73 x74 = x66 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x2 x73 x74 ⟶ (x9 x74 x73 = x16 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x7 x75 ⟶ x13 x75 (x14 x73 x73) x73 ⟶ x68 x75 x73 ⟶ x2 x75 (x1 (x14 (x14 x73 x73) x73)) ⟶ x2 x74 x73 ⟶ (x10 x73 x75 x74 x74 = x74 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x7 x18 ⟶ False) ⟶ False) ⟶ ((x19 x18 ⟶ False) ⟶ False) ⟶ (x72 x18 ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x65 x21 ⟶ False) ⟶ False) ⟶ (x72 x21 ⟶ False) ⟶ (∀ x73 . (x64 x73 ⟶ False) ⟶ (x65 (x63 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x64 x73 ⟶ False) ⟶ x64 (x63 x73) ⟶ False) ⟶ (∀ x73 . (x64 x73 ⟶ False) ⟶ (x2 (x63 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x64 x73 ⟶ False) ⟶ x64 (x22 x73) ⟶ False) ⟶ (∀ x73 . (x64 x73 ⟶ False) ⟶ (x2 (x22 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x65 (x23 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x7 (x23 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x24 (x23 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x62 (x23 x73 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x19 (x23 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x72 (x23 x73 x74) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x64 (x25 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x25 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x25 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x65 (x61 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x7 (x61 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x24 (x61 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x62 (x61 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x61 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x27 (x26 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x26 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x27 (x28 x73) x73 ⟶ False) ⟶ (∀ x73 . (x2 (x28 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x24 (x29 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x62 (x29 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x29 x73 x74) ⟶ False) ⟶ False) ⟶ ((x65 x60 ⟶ False) ⟶ False) ⟶ ((x7 x60 ⟶ False) ⟶ False) ⟶ ((x19 x60 ⟶ False) ⟶ False) ⟶ (x72 x60 ⟶ False) ⟶ (x72 x59 ⟶ False) ⟶ (∀ x73 . (x72 (x30 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x2 (x30 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x65 (x31 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x31 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x31 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ ((x19 x57 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x65 (x56 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x56 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x56 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ ((x72 x32 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x55 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x55 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x65 (x54 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 (x54 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x2 (x54 x73) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x24 (x33 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x62 (x33 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x33 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 (x33 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x2 (x33 x73 x74) (x1 (x14 x74 x73)) ⟶ False) ⟶ False) ⟶ ((x19 x53 ⟶ False) ⟶ False) ⟶ (x72 x53 ⟶ False) ⟶ (∀ x73 . (x68 (x52 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x13 (x52 x73) (x14 x73 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x7 (x52 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x24 (x52 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x62 (x52 x73) (x14 x73 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x19 (x52 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x2 (x52 x73) (x1 (x14 (x14 x73 x73) x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x13 (x34 x73 x74) x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x7 (x34 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x24 (x34 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x62 (x34 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x34 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x2 (x34 x73 x74) (x1 (x14 x74 x73)) ⟶ False) ⟶ False) ⟶ ((x65 x35 ⟶ False) ⟶ False) ⟶ (x72 x35 ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x74 (x3 x75) ⟶ x2 x73 (x3 x75) ⟶ (x8 x75 x74 x74 = x74 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x67 x73 x73 = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x65 x74 ⟶ x65 x73 ⟶ (x65 (x67 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x19 (x51 (x50 x74 x73) (x50 x76 x75)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x14 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x72 (x67 x73 x74) ⟶ False) ⟶ (∀ x73 x74 . (x19 (x16 (x50 x74 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x72 (x67 x74 x73) ⟶ False) ⟶ (∀ x73 x74 x75 . x19 x75 ⟶ x24 x75 x73 ⟶ x19 x74 ⟶ x24 x74 x73 ⟶ (x24 (x67 x75 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 (x51 x73 x74) ⟶ False) ⟶ (∀ x73 x74 . x19 x74 ⟶ x19 x73 ⟶ (x19 (x67 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x19 x74 ⟶ x7 x74 ⟶ x17 x74 ⟶ (x65 (x66 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x20 x74 ⟶ x20 x73 ⟶ (x20 (x67 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x65 x74 ⟶ x65 x73 ⟶ (x20 (x51 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x65 x73 ⟶ (x20 (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x65 x73 ⟶ (x20 (x16 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 (x16 x73) ⟶ False) ⟶ (∀ x73 . (x49 (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 (x3 x73) ⟶ False) ⟶ (∀ x73 x74 . (x65 (x51 x73 x74) ⟶ False) ⟶ False) ⟶ ((x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 (x1 x73) ⟶ False) ⟶ (∀ x73 x74 x75 . x19 x75 ⟶ x62 x75 x73 ⟶ x19 x74 ⟶ x62 x74 x73 ⟶ (x62 (x67 x75 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x49 (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x65 (x16 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x65 x73 ⟶ (x65 (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x65 x74 ⟶ x65 x73 ⟶ (x65 (x14 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x72 (x14 x74 x73) ⟶ False) ⟶ (∀ x73 . (x2 (x36 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x2 (x4 x73) (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73))) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x13 (x4 x73) (x14 (x3 x73) (x3 x73)) (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x7 (x4 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 x77 . (x72 x77 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x7 x76 ⟶ x13 x76 (x14 x73 x73) x73 ⟶ x2 x76 (x1 (x14 (x14 x73 x73) x73)) ⟶ x2 x74 (x3 x77) ⟶ x7 x75 ⟶ x13 x75 x77 x73 ⟶ x2 x75 (x1 (x14 x77 x73)) ⟶ (x2 (x11 x77 x73 x76 x74 x75) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x74 (x3 x75) ⟶ x2 x73 (x3 x75) ⟶ (x2 (x8 x75 x74 x73) (x3 x75) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x49 (x3 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x7 x76 ⟶ x13 x76 (x14 x73 x73) x73 ⟶ x2 x76 (x1 (x14 (x14 x73 x73) x73)) ⟶ x2 x74 x73 ⟶ x2 x75 x73 ⟶ (x2 (x10 x73 x76 x74 x75) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x7 x73 ⟶ x13 x73 x76 x75 ⟶ x2 x73 (x1 (x14 x76 x75)) ⟶ x2 x74 x76 ⟶ (x2 (x12 x76 x75 x73 x74) x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x2 x73 x74 ⟶ (x2 (x9 x74 x73) (x3 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x2 x73 (x3 x76) ⟶ x7 x75 ⟶ x13 x75 x76 (x3 x74) ⟶ x2 x75 (x1 (x14 x76 (x3 x74))) ⟶ (x2 (x37 x76 x74 x73 x75) (x3 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x50 x74 x73 = x51 (x51 x74 x73) (x16 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x2 x73 (x3 x76) ⟶ x7 x75 ⟶ x13 x75 x76 (x3 x74) ⟶ x2 x75 (x1 (x14 x76 (x3 x74))) ⟶ (x37 x76 x74 x73 x75 = x11 x76 (x3 x74) (x4 x74) x73 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x7 x74 ⟶ x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73) ⟶ x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73))) ⟶ x10 (x3 x73) x74 (x48 x74 x73) (x47 x74 x73) = x8 x73 (x48 x74 x73) (x47 x74 x73) ⟶ (x74 = x4 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x7 x74 ⟶ x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73) ⟶ x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73))) ⟶ (x2 (x47 x74 x73) (x3 x73) ⟶ False) ⟶ (x74 = x4 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x7 x74 ⟶ x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73) ⟶ x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73))) ⟶ (x2 (x48 x74 x73) (x3 x73) ⟶ False) ⟶ (x74 = x4 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x7 x76 ⟶ x13 x76 (x14 (x3 x73) (x3 x73)) (x3 x73) ⟶ x2 x76 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73))) ⟶ x76 = x4 x73 ⟶ x2 x75 (x3 x73) ⟶ x2 x74 (x3 x73) ⟶ (x10 (x3 x73) x76 x75 x74 = x8 x73 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x19 x75 ⟶ x7 x75 ⟶ (x15 x75 x73 x74 = x66 x75 (x50 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x74 (x3 x75) ⟶ x2 x73 (x3 x75) ⟶ (x8 x75 x74 x73 = x8 x75 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x67 x74 x73 = x67 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x51 x74 x73 = x51 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x17 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x24 x73 x74 ⟶ (x24 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x24 x73 x74 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x24 x73 x74 ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x2 x74 (x1 (x14 x75 x73)) ⟶ x7 x74 ⟶ x13 x74 x75 x73 ⟶ (x13 x74 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x2 x74 (x1 (x14 x75 x73)) ⟶ x7 x74 ⟶ x13 x74 x75 x73 ⟶ x72 x74 ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x2 x74 (x1 (x14 x75 x73)) ⟶ x7 x74 ⟶ x13 x74 x75 x73 ⟶ (x7 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x20 x74 ⟶ x2 x73 (x1 x74) ⟶ (x20 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x62 x73 x74 ⟶ (x62 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x62 x73 x74 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x19 x73 ⟶ x62 x73 x74 ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x20 x74 ⟶ x2 x73 x74 ⟶ (x65 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x19 x75 ⟶ x24 x75 x73 ⟶ x2 x74 (x1 x75) ⟶ (x24 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x20 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x64 x74 ⟶ x2 x73 (x1 x74) ⟶ (x64 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x19 x75 ⟶ x62 x75 x73 ⟶ x2 x74 (x1 x75) ⟶ (x62 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x65 x73 ⟶ False) ⟶ x64 x73 ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x2 x73 (x1 x74) ⟶ x27 x73 x74 ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x2 x73 (x1 (x14 x74 x75)) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x58 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x74 (x1 (x14 x73 x73)) ⟶ x13 x74 x73 x73 ⟶ (x46 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x64 x73 ⟶ (x65 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x2 x73 (x1 x74) ⟶ x72 x73 ⟶ (x27 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x2 x73 (x1 (x14 x75 x74)) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x45 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x19 x73 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ x2 x73 (x1 (x14 x74 x75)) ⟶ x13 x73 x74 x75 ⟶ (x46 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x74 (x3 x73) ⟶ (x65 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x65 x75 ⟶ x2 x73 (x1 (x14 x75 x74)) ⟶ x7 x73 ⟶ x13 x73 x75 x74 ⟶ (x65 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x65 x75 ⟶ x2 x73 (x1 (x14 x75 x74)) ⟶ x7 x73 ⟶ x13 x73 x75 x74 ⟶ (x13 x73 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x65 x75 ⟶ x2 x73 (x1 (x14 x75 x74)) ⟶ x7 x73 ⟶ x13 x73 x75 x74 ⟶ (x7 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x2 x73 (x1 x74) ⟶ (x27 x73 x74 ⟶ False) ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x75 (x1 (x14 x73 x74)) ⟶ (x24 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x75 (x1 (x14 x74 x73)) ⟶ (x62 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x19 x74 ⟶ x2 x73 (x1 x74) ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x2 x73 (x1 (x14 x75 x74)) ⟶ x13 x73 x75 x74 ⟶ (x46 x73 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 . x44 x73 ⟶ x43 x73 ⟶ (x49 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x65 x74 ⟶ x2 x73 (x1 x74) ⟶ (x65 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x2 x73 (x1 x74) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x75 (x1 (x14 x73 x74)) ⟶ (x19 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x19 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x2 x74 (x1 (x14 x75 x73)) ⟶ x46 x74 x75 ⟶ (x13 x74 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x49 x73 ⟶ (x43 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x49 x73 ⟶ (x44 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x65 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x0 x73 x74 ⟶ x0 x74 x73 ⟶ False) ⟶ (x37 x42 x38 (x8 x42 x39 (x9 x42 x40)) x41 = x8 x38 (x37 x42 x38 x39 x41) (x12 x42 (x3 x38) x41 x40) ⟶ False) ⟶ ((x2 x39 (x3 x42) ⟶ False) ⟶ False) ⟶ ((x2 x40 x42 ⟶ False) ⟶ False) ⟶ ((x2 x41 (x1 (x14 x42 (x3 x38))) ⟶ False) ⟶ False) ⟶ ((x13 x41 x42 (x3 x38) ⟶ False) ⟶ False) ⟶ ((x7 x41 ⟶ False) ⟶ False) ⟶ (x72 x42 ⟶ False) ⟶ False (proof)