Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../441bc..
PUYkj../f8a25..
vout
PrPhD../2f430.. 3.40 bars
TMWiu../77070.. ownership of 498e5.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMRBi../9afb2.. ownership of 31435.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUTyN../cf9e1.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 498e5.. : ∀ 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 ⟶ x71 x72 ⟶ (x70 x73 x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x0 x73 ⟶ (x73 = x72 ⟶ False) ⟶ x0 x72 ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ (x70 x73 x72 ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x1 x73 ⟶ x1 x72 ⟶ (x70 x72 x73 ⟶ False) ⟶ (x70 (x3 x73 x2) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x67 x72 x73 ⟶ x0 x73 ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ (x0 x73 ⟶ False) ⟶ (x68 x72 ⟶ False) ⟶ (x69 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ x70 (x65 x72) x64 ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ (x72 = x4 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x67 x72 x73 ⟶ x62 x73 (x63 x74) ⟶ x0 x74 ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ (x0 x72 ⟶ False) ⟶ (x69 x73 ⟶ False) ⟶ (x68 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x67 x73 x74 ⟶ x62 x74 (x63 x72) ⟶ (x62 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ (x68 x72 ⟶ False) ⟶ x68 x73 ⟶ False) ⟶ (∀ x72 x73 . x61 x73 x72 ⟶ (x62 x73 (x63 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x62 x73 (x63 x72) ⟶ (x61 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ (x69 x73 ⟶ False) ⟶ x69 x72 ⟶ False) ⟶ (∀ x72 x73 x74 . x5 x74 ⟶ x5 x72 ⟶ x5 x73 ⟶ x70 x74 x72 ⟶ x70 x72 x73 ⟶ (x70 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x62 x72 x73 ⟶ (x0 x73 ⟶ False) ⟶ (x67 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ x69 x72 ⟶ (x69 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x70 x2 x72 ⟶ x66 x73 ⟶ x60 x72 x73 x74 ⟶ (x73 = x58 x72 x74 (x59 x74 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x67 x73 x72 ⟶ (x62 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ x70 x73 x72 ⟶ x68 x73 ⟶ (x68 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ x70 x6 x72 ⟶ x70 (x65 x72) x6 ⟶ False) ⟶ ((x62 x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x72 . x7 x72 ⟶ (x8 x72 x64 = x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x66 x72 ⟶ x70 x2 x73 ⟶ x70 x2 x72 ⟶ (x70 x73 (x56 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x7 x74 ⟶ x7 x72 ⟶ x7 x73 ⟶ (x8 (x8 x74 x72) x73 = x8 x74 (x8 x72 x73) ⟶ False) ⟶ False) ⟶ ((x62 x6 x55 ⟶ False) ⟶ False) ⟶ ((x62 x6 x9 ⟶ False) ⟶ False) ⟶ ((x54 x6 x55 x9 ⟶ False) ⟶ False) ⟶ ((x68 x6 ⟶ False) ⟶ False) ⟶ (x0 x6 ⟶ False) ⟶ ((x62 x2 x55 ⟶ False) ⟶ False) ⟶ ((x62 x2 x9 ⟶ False) ⟶ False) ⟶ ((x54 x2 x55 x9 ⟶ False) ⟶ False) ⟶ ((x68 x2 ⟶ False) ⟶ False) ⟶ (x0 x2 ⟶ False) ⟶ ((x62 x53 x55 ⟶ False) ⟶ False) ⟶ ((x62 x53 x9 ⟶ False) ⟶ False) ⟶ ((x54 x53 x55 x9 ⟶ False) ⟶ False) ⟶ ((x0 x53 ⟶ False) ⟶ False) ⟶ ((x8 x6 x53 = x6 ⟶ False) ⟶ False) ⟶ ((x8 x2 x2 = x6 ⟶ False) ⟶ False) ⟶ ((x8 x2 x53 = x2 ⟶ False) ⟶ False) ⟶ ((x8 x53 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x8 x53 x2 = x2 ⟶ False) ⟶ False) ⟶ ((x8 x53 x53 = x53 ⟶ False) ⟶ False) ⟶ ((x70 x6 x6 ⟶ False) ⟶ False) ⟶ (x70 x6 x2 ⟶ False) ⟶ (x70 x6 x53 ⟶ False) ⟶ ((x70 x2 x6 ⟶ False) ⟶ False) ⟶ ((x70 x2 x2 ⟶ False) ⟶ False) ⟶ (x70 x2 x53 ⟶ False) ⟶ ((x70 x53 x6 ⟶ False) ⟶ False) ⟶ ((x70 x53 x2 ⟶ False) ⟶ False) ⟶ ((x70 x53 x53 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x5 x73 ⟶ x5 x72 ⟶ (x70 x73 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x61 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x0 x74 ⟶ False) ⟶ (x0 x72 ⟶ False) ⟶ x62 x72 (x63 x74) ⟶ x62 x73 x72 ⟶ (x54 x73 x74 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x0 x74 ⟶ False) ⟶ (x0 x72 ⟶ False) ⟶ x62 x72 (x63 x74) ⟶ x54 x73 x74 x72 ⟶ (x62 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x11 x73 x72 ⟶ (x10 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x10 x73 x72 ⟶ (x11 x73 x72 ⟶ False) ⟶ False) ⟶ ((x64 = x4 ⟶ False) ⟶ False) ⟶ ((x9 = x57 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x62 x72 x55 ⟶ (x3 x73 x72 = x8 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x51 x72 = x52 x72 ⟶ False) ⟶ False) ⟶ ((x66 x12 ⟶ False) ⟶ False) ⟶ (x0 x12 ⟶ False) ⟶ ((x5 x13 ⟶ False) ⟶ False) ⟶ ((x0 x13 ⟶ False) ⟶ False) ⟶ ((x71 x14 ⟶ False) ⟶ False) ⟶ ((x5 x14 ⟶ False) ⟶ False) ⟶ ((x7 x14 ⟶ False) ⟶ False) ⟶ ((x0 x14 ⟶ False) ⟶ False) ⟶ ((x66 x15 ⟶ False) ⟶ False) ⟶ ((x69 x50 ⟶ False) ⟶ False) ⟶ ((x5 x50 ⟶ False) ⟶ False) ⟶ ((x71 x49 ⟶ False) ⟶ False) ⟶ ((x69 x49 ⟶ False) ⟶ False) ⟶ ((x5 x49 ⟶ False) ⟶ False) ⟶ ((x7 x49 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x48 (x47 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x16 (x47 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 . (x46 (x47 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x17 (x47 x72) ⟶ False) ⟶ False) ⟶ ((x68 x45 ⟶ False) ⟶ False) ⟶ ((x5 x45 ⟶ False) ⟶ False) ⟶ ((x71 x44 ⟶ False) ⟶ False) ⟶ ((x68 x44 ⟶ False) ⟶ False) ⟶ ((x5 x44 ⟶ False) ⟶ False) ⟶ ((x7 x44 ⟶ False) ⟶ False) ⟶ (x0 x43 ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x42 x19 ⟶ False) ⟶ False) ⟶ ((x20 x19 ⟶ False) ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ ((x18 x21 ⟶ False) ⟶ False) ⟶ (x0 x21 ⟶ False) ⟶ ((x62 x21 (x63 x55) ⟶ False) ⟶ False) ⟶ ((x1 x41 ⟶ False) ⟶ False) ⟶ ((x5 x22 ⟶ False) ⟶ False) ⟶ ((x71 x40 ⟶ False) ⟶ False) ⟶ ((x0 x23 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x46 (x39 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x24 (x39 x73 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x17 (x39 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x0 (x39 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x62 (x39 x72 x73) (x63 (x38 x73 x72)) ⟶ False) ⟶ False) ⟶ ((x18 x25 ⟶ False) ⟶ False) ⟶ ((x1 x37 ⟶ False) ⟶ False) ⟶ ((x71 x37 ⟶ False) ⟶ False) ⟶ ((x7 x37 ⟶ False) ⟶ False) ⟶ ((x5 x37 ⟶ False) ⟶ False) ⟶ ((x62 x37 x55 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x69 x73 ⟶ False) ⟶ x71 x73 ⟶ (x69 x72 ⟶ False) ⟶ x71 x72 ⟶ x69 (x8 x73 x72) ⟶ False) ⟶ (x36 x55 ⟶ False) ⟶ ((x18 x57 ⟶ False) ⟶ False) ⟶ (x0 x57 ⟶ False) ⟶ (x36 x26 ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x71 x72 ⟶ (x71 (x8 x73 x72) ⟶ False) ⟶ False) ⟶ (x0 x26 ⟶ False) ⟶ (∀ x72 x73 . x66 x73 ⟶ x66 x72 ⟶ (x66 (x56 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x66 x73 ⟶ (x0 x72 ⟶ False) ⟶ x66 x72 ⟶ x0 (x8 x72 x73) ⟶ False) ⟶ (∀ x72 x73 . x7 x73 ⟶ x66 x72 ⟶ (x7 (x56 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x66 x73 ⟶ (x0 x72 ⟶ False) ⟶ x66 x72 ⟶ x0 (x8 x73 x72) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x66 x72 ⟶ (x71 (x56 x73 x72) ⟶ False) ⟶ False) ⟶ ((x0 x4 ⟶ False) ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ (∀ x72 x73 . x66 x73 ⟶ x66 x72 ⟶ (x66 (x8 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x1 x73 ⟶ x1 x72 ⟶ (x1 (x8 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x69 x73 ⟶ x71 x73 ⟶ (x68 x72 ⟶ False) ⟶ x71 x72 ⟶ (x69 (x8 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x69 x73 ⟶ x71 x73 ⟶ (x68 x72 ⟶ False) ⟶ x71 x72 ⟶ (x69 (x8 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x68 x73 ⟶ x71 x73 ⟶ (x69 x72 ⟶ False) ⟶ x71 x72 ⟶ (x68 (x8 x72 x73) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x68 x73 ⟶ x71 x73 ⟶ (x69 x72 ⟶ False) ⟶ x71 x72 ⟶ (x68 (x8 x73 x72) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . (x68 x73 ⟶ False) ⟶ x71 x73 ⟶ (x68 x72 ⟶ False) ⟶ x71 x72 ⟶ x68 (x8 x73 x72) ⟶ False) ⟶ (∀ x72 x73 . (x0 x73 ⟶ False) ⟶ (x0 x72 ⟶ False) ⟶ x62 x72 (x63 x73) ⟶ (x54 (x35 x72 x73) x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x10 (x27 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x62 (x34 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x11 (x28 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . (x0 x74 ⟶ False) ⟶ (x0 x72 ⟶ False) ⟶ x62 x72 (x63 x74) ⟶ x54 x73 x74 x72 ⟶ (x62 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x10 x73 x72 ⟶ (x62 x73 (x63 (x38 x9 x72)) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x10 x73 x72 ⟶ (x33 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x10 x73 x72 ⟶ (x16 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x11 x73 x72 ⟶ (x33 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x11 x73 x72 ⟶ (x16 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x11 x73 x72 ⟶ (x17 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x29 x73 x74 ⟶ x11 x73 (x51 x72) ⟶ (x1 (x58 x74 x72 x73) ⟶ False) ⟶ False) ⟶ ((x54 x64 x55 x9 ⟶ False) ⟶ False) ⟶ ((x62 x9 (x63 x55) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x62 x72 x55 ⟶ (x62 (x3 x73 x72) x55 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x62 (x51 x72) (x63 x26) ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ x0 (x51 x72) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x62 (x65 x72) x9 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x66 x73 ⟶ (x10 (x59 x74 x72 x73) (x51 x74) ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x66 x73 ⟶ (x29 (x59 x74 x72 x73) x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x66 x73 ⟶ (x70 (x56 (x65 x73) x74) x72 ⟶ False) ⟶ (x60 x74 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x66 x74 ⟶ x66 x72 ⟶ x66 x73 ⟶ x60 x74 x72 x73 ⟶ x70 (x56 (x65 x73) x74) x72 ⟶ False) ⟶ (∀ x72 x73 . x5 x73 ⟶ x5 x72 ⟶ (x70 x73 x72 ⟶ False) ⟶ (x70 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x71 x73 ⟶ x62 x72 x55 ⟶ (x3 x73 x72 = x3 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x7 x73 ⟶ x7 x72 ⟶ (x8 x73 x72 = x8 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ (x30 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ (x68 x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ (x68 x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ (x0 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x62 x72 x57 ⟶ (x66 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ x5 x72 ⟶ x69 x72 ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ x5 x72 ⟶ x68 x72 ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ x5 x72 ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ (x66 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x0 x72 ⟶ False) ⟶ x5 x72 ⟶ (x68 x72 ⟶ False) ⟶ (x69 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x0 x72 ⟶ False) ⟶ x5 x72 ⟶ (x68 x72 ⟶ False) ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x69 x72 ⟶ x68 x72 ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x69 x72 ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x69 x72 ⟶ x0 x72 ⟶ False) ⟶ (∀ x72 x73 . x18 x73 ⟶ x62 x72 x73 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x0 x72 ⟶ False) ⟶ x5 x72 ⟶ (x69 x72 ⟶ False) ⟶ (x68 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . (x0 x72 ⟶ False) ⟶ x5 x72 ⟶ (x69 x72 ⟶ False) ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x74 ⟶ x62 x72 (x63 (x38 x73 x74)) ⟶ (x0 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ (x48 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x68 x72 ⟶ x69 x72 ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x68 x72 ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x5 x72 ⟶ x68 x72 ⟶ x0 x72 ⟶ False) ⟶ (∀ x72 . x71 x72 ⟶ (x7 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x0 x74 ⟶ x62 x72 (x63 (x38 x74 x73)) ⟶ (x0 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x0 x72 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ x69 x72 ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x66 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x1 x72 ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x5 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x62 x74 (x63 (x38 x72 x73)) ⟶ (x46 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x62 x74 (x63 (x38 x73 x72)) ⟶ (x24 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x72 . x20 x72 ⟶ x42 x72 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x62 x72 x9 ⟶ x69 x72 ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x1 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x62 x72 x55 ⟶ (x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 x74 . x62 x74 (x63 (x38 x72 x73)) ⟶ (x17 x74 ⟶ False) ⟶ False) ⟶ (∀ x72 . x18 x72 ⟶ (x42 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x18 x72 ⟶ (x20 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x66 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x66 x72 ⟶ (x18 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 . x62 x72 x26 ⟶ (x1 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x30 x73 ⟶ x62 x72 (x63 x73) ⟶ (x30 x72 ⟶ False) ⟶ False) ⟶ (∀ x72 x73 . x67 x72 x73 ⟶ x67 x73 x72 ⟶ False) ⟶ (x58 x31 x32 (x59 x32 x31 x2) = x2 ⟶ False) ⟶ ((x70 x6 x32 ⟶ False) ⟶ False) ⟶ ((x70 x2 x31 ⟶ False) ⟶ False) ⟶ ((x66 x32 ⟶ False) ⟶ False) ⟶ ((x66 x31 ⟶ False) ⟶ False) ⟶ False (proof)