Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../f4da2..
PUdgk../9d7e1..
vout
PrNUD../e3c0d.. 0.04 bars
TMYv2../19df2.. ownership of e1852.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMdfw../8bb2c.. ownership of 427c3.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUYKK../3c6ae.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem e1852.. : ∀ 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 . x63 x65 ⟶ (x65 = x64 ⟶ False) ⟶ x63 x64 ⟶ False) ⟶ (∀ x64 x65 . x0 x64 x65 ⟶ x63 x65 ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ (x64 = x62 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x0 x64 x65 ⟶ x2 x65 (x1 x66) ⟶ x63 x66 ⟶ False) ⟶ (∀ x64 x65 x66 . x0 x65 x66 ⟶ x2 x66 (x1 x64) ⟶ (x2 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x3 x65 x64 ⟶ (x2 x65 (x1 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 (x1 x64) ⟶ (x3 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x64 x65 ⟶ (x63 x65 ⟶ False) ⟶ (x0 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x0 x65 x64 ⟶ (x2 x65 x64 ⟶ False) ⟶ False) ⟶ ((x2 x62 x4 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x59 (x60 x65) (x60 x64) = x59 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x5 (x60 x65) (x60 x64) = x60 (x5 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x61 x65 ⟶ (x5 (x5 x66 x64) x65 = x5 x66 (x5 x64 x65) ⟶ False) ⟶ False) ⟶ ((x2 x7 x6 ⟶ False) ⟶ False) ⟶ ((x2 x7 x58 ⟶ False) ⟶ False) ⟶ ((x8 x7 x6 x58 ⟶ False) ⟶ False) ⟶ ((x57 x7 ⟶ False) ⟶ False) ⟶ (x63 x7 ⟶ False) ⟶ ((x2 x56 x6 ⟶ False) ⟶ False) ⟶ ((x2 x56 x58 ⟶ False) ⟶ False) ⟶ ((x8 x56 x6 x58 ⟶ False) ⟶ False) ⟶ ((x57 x56 ⟶ False) ⟶ False) ⟶ (x63 x56 ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x5 x65 (x60 x64) = x59 x65 x64 ⟶ False) ⟶ False) ⟶ ((x2 x55 x6 ⟶ False) ⟶ False) ⟶ ((x2 x55 x58 ⟶ False) ⟶ False) ⟶ ((x8 x55 x6 x58 ⟶ False) ⟶ False) ⟶ ((x63 x55 ⟶ False) ⟶ False) ⟶ ((x60 (x60 x7) = x7 ⟶ False) ⟶ False) ⟶ ((x60 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x60 x7 = x60 x7 ⟶ False) ⟶ False) ⟶ ((x60 x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x60 x55 = x55 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x7) (x60 x7) = x55 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x7) (x60 x56) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x7) x55 = x60 x7 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x56) (x60 x7) = x56 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x56) (x60 x56) = x55 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x56) x56 = x60 x7 ⟶ False) ⟶ False) ⟶ ((x59 (x60 x56) x55 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x59 x7 x7 = x55 ⟶ False) ⟶ False) ⟶ ((x59 x7 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x59 x7 x55 = x7 ⟶ False) ⟶ False) ⟶ ((x59 x56 (x60 x56) = x7 ⟶ False) ⟶ False) ⟶ ((x59 x56 x7 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x59 x56 x56 = x55 ⟶ False) ⟶ False) ⟶ ((x59 x56 x55 = x56 ⟶ False) ⟶ False) ⟶ ((x59 x55 (x60 x7) = x7 ⟶ False) ⟶ False) ⟶ ((x59 x55 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x59 x55 x7 = x60 x7 ⟶ False) ⟶ False) ⟶ ((x59 x55 x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x59 x55 x55 = x55 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x7) x7 = x55 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x7) x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x56) (x60 x56) = x60 x7 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x56) x7 = x56 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x56) x56 = x55 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x56) x55 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 x7 (x60 x7) = x55 ⟶ False) ⟶ False) ⟶ ((x5 x7 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x5 x7 x55 = x7 ⟶ False) ⟶ False) ⟶ ((x5 x56 (x60 x7) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 x56 (x60 x56) = x55 ⟶ False) ⟶ False) ⟶ ((x5 x56 x56 = x7 ⟶ False) ⟶ False) ⟶ ((x5 x56 x55 = x56 ⟶ False) ⟶ False) ⟶ ((x5 x55 (x60 x7) = x60 x7 ⟶ False) ⟶ False) ⟶ ((x5 x55 (x60 x56) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 x55 x7 = x7 ⟶ False) ⟶ False) ⟶ ((x5 x55 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x5 x55 x55 = x55 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x3 x64 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . (x63 x66 ⟶ False) ⟶ (x63 x64 ⟶ False) ⟶ x2 x64 (x1 x66) ⟶ x2 x65 x64 ⟶ (x8 x65 x66 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . (x63 x66 ⟶ False) ⟶ (x63 x64 ⟶ False) ⟶ x2 x64 (x1 x66) ⟶ x8 x65 x66 x64 ⟶ (x2 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x10 x64 ⟶ (x9 x65 x64 = x5 x65 x64 ⟶ False) ⟶ False) ⟶ ((x58 = x4 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x12 x64 = x11 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x53 x64 = x54 x64 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x63 x14 ⟶ False) ⟶ False) ⟶ ((x10 x15 ⟶ False) ⟶ False) ⟶ ((x13 x15 ⟶ False) ⟶ False) ⟶ ((x61 x15 ⟶ False) ⟶ False) ⟶ ((x63 x15 ⟶ False) ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ ((x13 x17 ⟶ False) ⟶ False) ⟶ ((x10 x18 ⟶ False) ⟶ False) ⟶ ((x16 x18 ⟶ False) ⟶ False) ⟶ ((x13 x18 ⟶ False) ⟶ False) ⟶ ((x61 x18 ⟶ False) ⟶ False) ⟶ ((x19 x20 ⟶ False) ⟶ False) ⟶ ((x52 x20 ⟶ False) ⟶ False) ⟶ (x63 x20 ⟶ False) ⟶ ((x57 x51 ⟶ False) ⟶ False) ⟶ ((x13 x51 ⟶ False) ⟶ False) ⟶ ((x10 x50 ⟶ False) ⟶ False) ⟶ ((x57 x50 ⟶ False) ⟶ False) ⟶ ((x13 x50 ⟶ False) ⟶ False) ⟶ ((x61 x50 ⟶ False) ⟶ False) ⟶ ((x61 x49 ⟶ False) ⟶ False) ⟶ (x63 x49 ⟶ False) ⟶ (x63 x48 ⟶ False) ⟶ ((x52 x21 ⟶ False) ⟶ False) ⟶ (x63 x21 ⟶ False) ⟶ ((x13 x22 ⟶ False) ⟶ False) ⟶ ((x10 x47 ⟶ False) ⟶ False) ⟶ ((x61 x23 ⟶ False) ⟶ False) ⟶ ((x63 x46 ⟶ False) ⟶ False) ⟶ ((x52 x24 ⟶ False) ⟶ False) ⟶ (x63 x24 ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x2 x64 x6 ⟶ (x12 (x25 x65 x64) = x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x2 x64 x6 ⟶ (x53 (x25 x65 x64) = x65 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 x67 . x2 x67 x6 ⟶ x2 x64 x6 ⟶ x10 x66 ⟶ x10 x65 ⟶ x67 = x66 ⟶ x64 = x65 ⟶ (x26 x67 x64 = x5 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x60 (x60 x64) = x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . (x16 x65 ⟶ False) ⟶ x10 x65 ⟶ (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ x16 (x5 x65 x64) ⟶ False) ⟶ (x45 x44 ⟶ False) ⟶ (x45 x6 ⟶ False) ⟶ (∀ x64 x65 . x10 x65 ⟶ x10 x64 ⟶ (x10 (x59 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x61 x64 ⟶ (x61 (x60 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x61 x64 ⟶ x63 (x60 x64) ⟶ False) ⟶ ((x52 x4 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x10 x65 ⟶ x10 x64 ⟶ (x10 (x5 x65 x64) ⟶ False) ⟶ False) ⟶ ((x19 x4 ⟶ False) ⟶ False) ⟶ ((x19 x6 ⟶ False) ⟶ False) ⟶ ((x19 x44 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x61 (x59 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . x10 x64 ⟶ (x10 (x60 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . x10 x64 ⟶ (x61 (x60 x64) ⟶ False) ⟶ False) ⟶ ((x27 x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x61 (x5 x65 x64) ⟶ False) ⟶ False) ⟶ (x63 x44 ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x10 (x11 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x16 x65 ⟶ x10 x65 ⟶ (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ (x57 (x59 x64 x65) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x16 x65 ⟶ x10 x65 ⟶ (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ (x16 (x59 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x57 x65 ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ (x16 (x59 x64 x65) ⟶ False) ⟶ False) ⟶ ((x63 x62 ⟶ False) ⟶ False) ⟶ (x63 x6 ⟶ False) ⟶ ((x43 x44 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x10 (x54 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x57 x65 ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ (x57 (x59 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . (x16 x65 ⟶ False) ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ x57 (x59 x64 x65) ⟶ False) ⟶ (∀ x64 x65 . (x16 x65 ⟶ False) ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ x16 (x59 x65 x64) ⟶ False) ⟶ (∀ x64 . (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ x57 (x60 x64) ⟶ False) ⟶ (∀ x64 . (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ (x61 (x60 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ x16 (x60 x64) ⟶ False) ⟶ (∀ x64 . (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ (x61 (x60 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x16 x65 ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ (x16 (x5 x64 x65) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x16 x65 ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ (x16 (x5 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x57 x65 ⟶ x10 x65 ⟶ (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ (x57 (x5 x64 x65) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x57 x65 ⟶ x10 x65 ⟶ (x16 x64 ⟶ False) ⟶ x10 x64 ⟶ (x57 (x5 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . (x57 x65 ⟶ False) ⟶ x10 x65 ⟶ (x57 x64 ⟶ False) ⟶ x10 x64 ⟶ x57 (x5 x65 x64) ⟶ False) ⟶ (∀ x64 x65 . (x63 x65 ⟶ False) ⟶ (x63 x64 ⟶ False) ⟶ x2 x64 (x1 x65) ⟶ (x8 (x42 x64 x65) x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x2 (x28 x64) x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . (x63 x66 ⟶ False) ⟶ (x63 x64 ⟶ False) ⟶ x2 x64 (x1 x66) ⟶ x8 x65 x66 x64 ⟶ (x2 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x10 x64 ⟶ (x2 (x9 x65 x64) x6 ⟶ False) ⟶ False) ⟶ ((x2 x58 (x1 x6) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x2 x64 x6 ⟶ (x2 (x25 x65 x64) x44 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x61 (x60 x64) ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x2 (x12 x64) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 . x61 x64 ⟶ (x2 (x53 x64) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x2 x64 x6 ⟶ (x2 (x26 x65 x64) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 x67 x68 x69 x70 . x61 x70 ⟶ x61 x64 ⟶ x2 x69 x6 ⟶ x2 x65 x6 ⟶ x2 x68 x6 ⟶ x2 x66 x6 ⟶ x70 = x25 x69 x65 ⟶ x64 = x25 x68 x66 ⟶ x67 = x25 (x26 x69 x68) (x26 x65 x66) ⟶ (x67 = x5 x70 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x65 = x25 (x26 (x29 x65 x64 x66) (x30 x65 x64 x66)) (x26 (x31 x65 x64 x66) (x32 x65 x64 x66)) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x64 = x25 (x30 x65 x64 x66) (x32 x65 x64 x66) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x66 = x25 (x29 x65 x64 x66) (x31 x65 x64 x66) ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x2 (x32 x65 x64 x66) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x2 (x30 x65 x64 x66) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x2 (x31 x65 x64 x66) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 x66 . x61 x66 ⟶ x61 x64 ⟶ x65 = x5 x66 x64 ⟶ (x2 (x29 x65 x64 x66) x6 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x10 x64 ⟶ (x9 x65 x64 = x9 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x61 x65 ⟶ x61 x64 ⟶ (x5 x65 x64 = x5 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x2 x65 x6 ⟶ x2 x64 x6 ⟶ (x26 x65 x64 = x26 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ (x57 x64 ⟶ False) ⟶ (x16 x64 ⟶ False) ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ (x57 x64 ⟶ False) ⟶ (x16 x64 ⟶ False) ⟶ (x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 (x1 x6) ⟶ (x27 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ x13 x64 ⟶ x16 x64 ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ x13 x64 ⟶ x57 x64 ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ x13 x64 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x13 x64 ⟶ (x57 x64 ⟶ False) ⟶ (x16 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x13 x64 ⟶ (x57 x64 ⟶ False) ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 (x1 x44) ⟶ (x43 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x16 x64 ⟶ x57 x64 ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x16 x64 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x16 x64 ⟶ x63 x64 ⟶ False) ⟶ (∀ x64 . x27 x64 ⟶ (x43 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x13 x64 ⟶ (x16 x64 ⟶ False) ⟶ (x57 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . (x63 x64 ⟶ False) ⟶ x13 x64 ⟶ (x16 x64 ⟶ False) ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x10 x64 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x27 x64 ⟶ (x33 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x57 x64 ⟶ x16 x64 ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x57 x64 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x13 x64 ⟶ x57 x64 ⟶ x63 x64 ⟶ False) ⟶ (∀ x64 . x10 x64 ⟶ (x61 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 x44 ⟶ (x61 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x34 x64 ⟶ (x27 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x41 x64 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x41 x64 ⟶ (x10 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x41 x64 ⟶ (x61 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x35 x64 ⟶ (x34 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ (x19 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 x58 ⟶ (x52 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x52 x65 ⟶ x2 x64 (x1 x65) ⟶ (x52 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x35 x65 ⟶ x2 x64 (x1 x65) ⟶ (x35 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x34 x65 ⟶ x2 x64 (x1 x65) ⟶ (x34 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x27 x65 ⟶ x2 x64 (x1 x65) ⟶ (x27 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x33 x65 ⟶ x2 x64 (x1 x65) ⟶ (x33 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 x6 ⟶ (x10 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 x6 ⟶ (x61 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x52 x64 ⟶ (x35 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x43 x65 ⟶ x2 x64 (x1 x65) ⟶ (x43 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x63 x64 ⟶ (x52 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x52 x65 ⟶ x2 x64 x65 ⟶ (x41 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x35 x65 ⟶ x2 x64 x65 ⟶ (x36 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x34 x65 ⟶ x2 x64 x65 ⟶ (x40 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x27 x65 ⟶ x2 x64 x65 ⟶ (x10 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x33 x65 ⟶ x2 x64 x65 ⟶ (x13 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x43 x65 ⟶ x2 x64 x65 ⟶ (x61 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 . x2 x64 (x1 x58) ⟶ (x52 x64 ⟶ False) ⟶ False) ⟶ (∀ x64 x65 . x0 x64 x65 ⟶ x0 x65 x64 ⟶ False) ⟶ (x12 x39 = x9 (x12 x37) (x12 x38) ⟶ False) ⟶ ((x39 = x5 x37 x38 ⟶ False) ⟶ False) ⟶ ((x61 x39 ⟶ False) ⟶ False) ⟶ ((x61 x38 ⟶ False) ⟶ False) ⟶ ((x61 x37 ⟶ False) ⟶ False) ⟶ False (proof)