Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5e0ce..
PUgtg../53bad..
vout
PrNUD../3320e.. 0.00 bars
TMJoq../2362b.. ownership of 2317a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMQHt../6f234.. ownership of 2892e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUfta../c959f.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2317a.. : ∀ 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 . x62 x64 ⟶ (x64 = x63 ⟶ False) ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x62 x64 ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x59 x63 = x63 ⟶ False) ⟶ (x59 x63 = x60 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x63 = x1 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x57 x63 x56 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x63 x64 ⟶ x3 x64 (x2 x65) ⟶ x62 x65 ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x64 x65 ⟶ x3 x65 (x2 x63) ⟶ (x3 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x4 x64 x63 ⟶ (x3 x64 (x2 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 (x2 x63) ⟶ (x4 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x5 x56 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x63 x64 ⟶ (x62 x64 ⟶ False) ⟶ (x0 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x64 x63 ⟶ (x3 x64 x63 ⟶ False) ⟶ False) ⟶ ((x3 x1 x55 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x6 (x60 x64) (x60 x63) = x6 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x54 (x60 x64) (x60 x63) = x60 (x54 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x58 x65 ⟶ x58 x63 ⟶ x58 x64 ⟶ (x5 (x5 x65 x63) x64 = x5 x65 (x5 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x58 x65 ⟶ x58 x63 ⟶ x58 x64 ⟶ (x54 (x54 x65 x63) x64 = x54 x65 (x54 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x58 x65 ⟶ x58 x63 ⟶ x58 x64 ⟶ (x5 (x54 x65 x63) x64 = x54 (x5 x65 x64) (x5 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x58 x65 ⟶ x58 x63 ⟶ x58 x64 ⟶ (x5 x65 (x57 x63 x64) = x57 (x5 x65 x63) x64 ⟶ False) ⟶ False) ⟶ ((x3 x8 x7 ⟶ False) ⟶ False) ⟶ ((x3 x8 x53 ⟶ False) ⟶ False) ⟶ ((x9 x8 x7 x53 ⟶ False) ⟶ False) ⟶ ((x52 x8 ⟶ False) ⟶ False) ⟶ (x62 x8 ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x5 x63 (x60 x56) = x60 x63 ⟶ False) ⟶ False) ⟶ ((x3 x56 x7 ⟶ False) ⟶ False) ⟶ ((x3 x56 x53 ⟶ False) ⟶ False) ⟶ ((x9 x56 x7 x53 ⟶ False) ⟶ False) ⟶ ((x52 x56 ⟶ False) ⟶ False) ⟶ (x62 x56 ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x54 x64 (x60 x63) = x6 x64 x63 ⟶ False) ⟶ False) ⟶ ((x3 x10 x7 ⟶ False) ⟶ False) ⟶ ((x3 x10 x53 ⟶ False) ⟶ False) ⟶ ((x9 x10 x7 x53 ⟶ False) ⟶ False) ⟶ ((x62 x10 ⟶ False) ⟶ False) ⟶ ((x60 (x57 (x60 x56) x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x60 (x57 x56 x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x60 (x60 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x60 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x60 x8 = x60 x8 ⟶ False) ⟶ False) ⟶ ((x60 x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x60 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x5 (x57 (x60 x56) x8) (x60 x8) = x56 ⟶ False) ⟶ False) ⟶ ((x5 (x57 (x60 x56) x8) x8 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 (x57 (x60 x56) x8) x56 = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x5 (x57 x56 x8) (x60 x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 (x57 x56 x8) x8 = x56 ⟶ False) ⟶ False) ⟶ ((x5 (x57 x56 x8) x56 = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x5 (x57 x56 x8) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x8) (x57 (x60 x56) x8) = x56 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x8) (x57 x56 x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x8) x56 = x60 x8 ⟶ False) ⟶ False) ⟶ ((x5 (x60 x8) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x5 x8 (x57 (x60 x56) x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x5 x8 (x57 x56 x8) = x56 ⟶ False) ⟶ False) ⟶ ((x5 x8 x56 = x8 ⟶ False) ⟶ False) ⟶ ((x5 x8 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x5 x56 (x57 (x60 x56) x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x5 x56 (x57 x56 x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x5 x56 (x60 x8) = x60 x8 ⟶ False) ⟶ False) ⟶ ((x5 x56 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x5 x56 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x5 x56 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 (x57 x56 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 (x60 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 x8 = x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 x56 = x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x57 (x60 x8) x8 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x57 (x60 x56) x8 = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x57 (x60 x56) x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x57 x8 x8 = x56 ⟶ False) ⟶ False) ⟶ ((x57 x8 x56 = x8 ⟶ False) ⟶ False) ⟶ ((x57 x56 (x57 (x60 x56) x8) = x60 x8 ⟶ False) ⟶ False) ⟶ ((x57 x56 (x57 x56 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x57 x56 (x60 x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x57 x56 (x60 x56) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x57 x56 x8 = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x57 x56 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x57 (x60 x56) x8) (x57 (x60 x56) x8) = x10 ⟶ False) ⟶ False) ⟶ ((x6 (x57 (x60 x56) x8) (x57 x56 x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x6 (x57 (x60 x56) x8) (x60 x56) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x6 (x57 (x60 x56) x8) x10 = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x6 (x57 x56 x8) (x57 (x60 x56) x8) = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x57 x56 x8) (x57 x56 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x6 (x57 x56 x8) x56 = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x6 (x57 x56 x8) x10 = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x8) (x60 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x8) (x60 x56) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x8) x10 = x60 x8 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x56) (x57 (x60 x56) x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x56) (x60 x8) = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x56) (x60 x56) = x10 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x56) x56 = x60 x8 ⟶ False) ⟶ False) ⟶ ((x6 (x60 x56) x10 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x6 x8 x8 = x10 ⟶ False) ⟶ False) ⟶ ((x6 x8 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x6 x8 x10 = x8 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x57 x56 x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x60 x56) = x8 ⟶ False) ⟶ False) ⟶ ((x6 x56 x8 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x6 x56 x56 = x10 ⟶ False) ⟶ False) ⟶ ((x6 x56 x10 = x56 ⟶ False) ⟶ False) ⟶ ((x6 x10 (x57 (x60 x56) x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x6 x10 (x57 x56 x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x6 x10 (x60 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x6 x10 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x6 x10 x8 = x60 x8 ⟶ False) ⟶ False) ⟶ ((x6 x10 x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x6 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x54 (x57 (x60 x56) x8) (x57 (x60 x56) x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x54 (x57 (x60 x56) x8) (x57 x56 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x54 (x57 (x60 x56) x8) x56 = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x54 (x57 x56 x8) (x57 (x60 x56) x8) = x10 ⟶ False) ⟶ False) ⟶ ((x54 (x57 x56 x8) (x57 x56 x8) = x56 ⟶ False) ⟶ False) ⟶ ((x54 (x57 x56 x8) (x60 x56) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x54 (x57 x56 x8) x10 = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x8) x8 = x10 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x8) x56 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x56) (x57 x56 x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x56) (x60 x56) = x60 x8 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x56) x8 = x56 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x56) x56 = x10 ⟶ False) ⟶ False) ⟶ ((x54 (x60 x56) x10 = x60 x56 ⟶ False) ⟶ False) ⟶ ((x54 x8 (x60 x8) = x10 ⟶ False) ⟶ False) ⟶ ((x54 x8 (x60 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x54 x8 x10 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x56 (x57 (x60 x56) x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x54 x56 (x60 x8) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x54 x56 (x60 x56) = x10 ⟶ False) ⟶ False) ⟶ ((x54 x56 x56 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x56 x10 = x56 ⟶ False) ⟶ False) ⟶ ((x54 x10 (x57 (x60 x56) x8) = x57 (x60 x56) x8 ⟶ False) ⟶ False) ⟶ ((x54 x10 (x57 x56 x8) = x57 x56 x8 ⟶ False) ⟶ False) ⟶ ((x54 x10 (x60 x8) = x60 x8 ⟶ False) ⟶ False) ⟶ ((x54 x10 (x60 x56) = x60 x56 ⟶ False) ⟶ False) ⟶ ((x54 x10 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x10 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x54 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x4 x63 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x3 x63 (x2 x65) ⟶ x3 x64 x63 ⟶ (x9 x64 x65 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x3 x63 (x2 x65) ⟶ x9 x64 x65 x63 ⟶ (x3 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x51 x63 = x50 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 x7 ⟶ x61 x63 ⟶ (x11 x64 x63 = x54 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x49 x63 = x48 x63 ⟶ False) ⟶ False) ⟶ ((x53 = x55 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x46 x63 = x47 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x13 x63 = x12 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x59 x63 = x45 x63 ⟶ False) ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x62 x15 ⟶ False) ⟶ False) ⟶ ((x61 x16 ⟶ False) ⟶ False) ⟶ ((x14 x16 ⟶ False) ⟶ False) ⟶ ((x58 x16 ⟶ False) ⟶ False) ⟶ ((x62 x16 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x14 x18 ⟶ False) ⟶ False) ⟶ ((x61 x19 ⟶ False) ⟶ False) ⟶ ((x17 x19 ⟶ False) ⟶ False) ⟶ ((x14 x19 ⟶ False) ⟶ False) ⟶ ((x58 x19 ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x44 x21 ⟶ False) ⟶ False) ⟶ (x62 x21 ⟶ False) ⟶ ((x52 x43 ⟶ False) ⟶ False) ⟶ ((x14 x43 ⟶ False) ⟶ False) ⟶ ((x61 x42 ⟶ False) ⟶ False) ⟶ ((x52 x42 ⟶ False) ⟶ False) ⟶ ((x14 x42 ⟶ False) ⟶ False) ⟶ ((x58 x42 ⟶ False) ⟶ False) ⟶ ((x58 x41 ⟶ False) ⟶ False) ⟶ (x62 x41 ⟶ False) ⟶ (x62 x40 ⟶ False) ⟶ ((x44 x22 ⟶ False) ⟶ False) ⟶ (x62 x22 ⟶ False) ⟶ ((x14 x23 ⟶ False) ⟶ False) ⟶ ((x61 x39 ⟶ False) ⟶ False) ⟶ ((x58 x24 ⟶ False) ⟶ False) ⟶ ((x62 x38 ⟶ False) ⟶ False) ⟶ ((x44 x25 ⟶ False) ⟶ False) ⟶ (x62 x25 ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x59 (x59 x63) = x59 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x45 (x45 x63) = x45 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x60 (x60 x63) = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x54 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x58 x64 ⟶ (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ x62 (x57 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . x61 x64 ⟶ x61 x63 ⟶ (x61 (x57 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x58 x64 ⟶ (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ x62 (x5 x64 x63) ⟶ False) ⟶ (x37 x7 ⟶ False) ⟶ (∀ x63 x64 . x61 x64 ⟶ x61 x63 ⟶ (x61 (x6 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x61 x64 ⟶ x61 x63 ⟶ (x61 (x5 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ (x58 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ x62 (x60 x63) ⟶ False) ⟶ ((x44 x55 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x61 x64 ⟶ x61 x63 ⟶ (x61 (x54 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x58 (x57 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ x17 (x45 x63) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x61 (x45 x63) ⟶ False) ⟶ False) ⟶ ((x20 x55 ⟶ False) ⟶ False) ⟶ ((x20 x7 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x58 (x6 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ (x61 (x45 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x58 x63 ⟶ x62 (x45 x63) ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x61 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x58 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x58 (x5 x64 x63) ⟶ False) ⟶ False) ⟶ ((x36 x7 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x52 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x57 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x57 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x57 x63 x64) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x57 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x58 (x54 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x61 (x48 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x61 (x47 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x5 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x52 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x5 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x52 x64 ⟶ False) ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x5 x63 x64) ⟶ False) ⟶ (∀ x63 x64 . (x52 x64 ⟶ False) ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x5 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . x17 x64 ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ (x52 (x6 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x17 x64 ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ (x17 (x6 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x52 x64 ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ (x17 (x6 x63 x64) ⟶ False) ⟶ False) ⟶ ((x62 x1 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x58 (x48 x63) ⟶ False) ⟶ False) ⟶ (x62 x7 ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x61 (x12 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x52 x64 ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ (x52 (x6 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x6 x63 x64) ⟶ False) ⟶ (∀ x63 x64 . (x17 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x6 x64 x63) ⟶ False) ⟶ (∀ x63 . (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x60 x63) ⟶ False) ⟶ (∀ x63 . (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ (x58 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x17 (x60 x63) ⟶ False) ⟶ (∀ x63 . (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ (x58 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x17 x64 ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ (x17 (x54 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x17 x64 ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ (x17 (x54 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x52 x64 ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ (x52 (x54 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x52 x64 ⟶ x61 x64 ⟶ (x17 x63 ⟶ False) ⟶ x61 x63 ⟶ (x52 (x54 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x52 x64 ⟶ False) ⟶ x61 x64 ⟶ (x52 x63 ⟶ False) ⟶ x61 x63 ⟶ x52 (x54 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x3 x63 (x2 x64) ⟶ (x9 (x26 x63 x64) x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x3 (x35 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x3 x63 (x2 x65) ⟶ x9 x64 x65 x63 ⟶ (x3 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x3 (x51 x63) x7 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 x7 ⟶ x61 x63 ⟶ (x3 (x11 x64 x63) x7 ⟶ False) ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x61 (x50 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x3 (x49 x63) x7 ⟶ False) ⟶ False) ⟶ ((x3 x53 (x2 x7) ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x58 (x60 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x3 (x46 x63) x7 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x3 (x13 x63) x7 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x3 (x59 x63) x7 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x61 (x45 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x48 x63 = x5 x63 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x58 x63 ⟶ (x45 x63 = x51 (x11 (x49 (x13 x63)) (x49 (x46 x63))) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 x7 ⟶ x61 x63 ⟶ (x11 x64 x63 = x11 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x5 x64 x63 = x5 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x58 x64 ⟶ x58 x63 ⟶ (x54 x64 x63 = x54 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ (x52 x63 ⟶ False) ⟶ (x17 x63 ⟶ False) ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ (x52 x63 ⟶ False) ⟶ (x17 x63 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 (x2 x7) ⟶ (x36 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x14 x63 ⟶ x17 x63 ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x14 x63 ⟶ x52 x63 ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x14 x63 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x14 x63 ⟶ (x52 x63 ⟶ False) ⟶ (x17 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x14 x63 ⟶ (x52 x63 ⟶ False) ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x17 x63 ⟶ x52 x63 ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x17 x63 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x17 x63 ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 . x36 x63 ⟶ (x34 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x14 x63 ⟶ (x17 x63 ⟶ False) ⟶ (x52 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x14 x63 ⟶ (x17 x63 ⟶ False) ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x36 x63 ⟶ (x33 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x52 x63 ⟶ x17 x63 ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x52 x63 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x14 x63 ⟶ x52 x63 ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 . x61 x63 ⟶ (x58 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x27 x63 ⟶ (x36 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x32 x63 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x32 x63 ⟶ (x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x32 x63 ⟶ (x58 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x28 x63 ⟶ (x27 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x20 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x53 ⟶ (x44 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x44 x64 ⟶ x3 x63 (x2 x64) ⟶ (x44 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x28 x64 ⟶ x3 x63 (x2 x64) ⟶ (x28 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x27 x64 ⟶ x3 x63 (x2 x64) ⟶ (x27 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x36 x64 ⟶ x3 x63 (x2 x64) ⟶ (x36 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x33 x64 ⟶ x3 x63 (x2 x64) ⟶ (x33 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 x7 ⟶ (x58 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x44 x63 ⟶ (x28 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x34 x64 ⟶ x3 x63 (x2 x64) ⟶ (x34 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x44 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x44 x64 ⟶ x3 x63 x64 ⟶ (x32 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x28 x64 ⟶ x3 x63 x64 ⟶ (x29 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x27 x64 ⟶ x3 x63 x64 ⟶ (x31 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x36 x64 ⟶ x3 x63 x64 ⟶ (x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x33 x64 ⟶ x3 x63 x64 ⟶ (x14 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x34 x64 ⟶ x3 x63 x64 ⟶ (x58 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x3 x63 (x2 x53) ⟶ (x44 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x0 x64 x63 ⟶ False) ⟶ (x49 (x59 x30) = x48 x30 ⟶ False) ⟶ ((x61 x30 ⟶ False) ⟶ False) ⟶ False (proof)