Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../c4810..
PUact../3df84..
vout
PrNUD../83687.. 0.02 bars
TMWLj../7909e.. ownership of 2076f.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMRwP../dcebf.. ownership of 46062.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PULeR../17a63.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2076f.. : ∀ 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 . x64 x66 ⟶ x64 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x61 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ (x66 = x65 ⟶ False) ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x61 x66 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x65 x66 ⟶ x0 x66 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x0 x66 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ (x62 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x65 = x2 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x65 x66 ⟶ x59 x66 (x60 x67) ⟶ x0 x67 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x0 x65 ⟶ False) ⟶ (x62 x66 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x56 x57 x65 = x57 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x66 x67 ⟶ x59 x67 (x60 x65) ⟶ (x59 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 x66 ⟶ False) ⟶ (∀ x65 x66 . x3 x66 x65 ⟶ (x59 x66 (x60 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 (x60 x65) ⟶ (x3 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x62 x66 ⟶ False) ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 x66 . x59 x65 x66 ⟶ (x0 x66 ⟶ False) ⟶ (x1 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ x62 x65 ⟶ (x62 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x55 x65 x57 = x57 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x66 x65 ⟶ (x59 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ x61 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ ((x59 x2 x4 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x58 x67 ⟶ x58 x65 ⟶ x58 x66 ⟶ (x55 (x55 x67 x65) x66 = x55 x67 (x55 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x58 x67 ⟶ x58 x65 ⟶ x58 x66 ⟶ (x55 x67 (x56 x65 x66) = x56 (x55 x67 x65) x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x58 x66 ⟶ x58 x65 ⟶ (x55 x66 (x54 x65) = x56 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x58 x66 ⟶ x58 x65 ⟶ (x56 (x54 x66) (x54 x65) = x56 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x58 x66 ⟶ x58 x65 ⟶ (x55 (x54 x66) (x54 x65) = x54 (x55 x66 x65) ⟶ False) ⟶ False) ⟶ ((x59 x6 x5 ⟶ False) ⟶ False) ⟶ ((x59 x6 x53 ⟶ False) ⟶ False) ⟶ ((x7 x6 x5 x53 ⟶ False) ⟶ False) ⟶ ((x0 x6 ⟶ False) ⟶ False) ⟶ ((x8 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x55 x6 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x63 x6 x6 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x63 x66 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x59 x65 (x60 x67) ⟶ x59 x66 x65 ⟶ (x7 x66 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x59 x65 (x60 x67) ⟶ x7 x66 x67 x65 ⟶ (x59 x66 x65 ⟶ False) ⟶ False) ⟶ ((x57 = x2 ⟶ False) ⟶ False) ⟶ ((x53 = x4 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x51 x65 = x50 x65 ⟶ False) ⟶ False) ⟶ ((x9 = x10 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 x49 ⟶ x59 x65 x49 ⟶ (x47 x66 x65 = x48 x66 x65 ⟶ False) ⟶ False) ⟶ ((x11 = x12 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 x49 ⟶ x59 x65 x49 ⟶ (x45 x66 x65 = x46 x66 x65 ⟶ False) ⟶ False) ⟶ ((x52 x13 ⟶ False) ⟶ False) ⟶ ((x0 x13 ⟶ False) ⟶ False) ⟶ ((x64 x14 ⟶ False) ⟶ False) ⟶ ((x52 x14 ⟶ False) ⟶ False) ⟶ ((x58 x14 ⟶ False) ⟶ False) ⟶ ((x0 x14 ⟶ False) ⟶ False) ⟶ ((x62 x15 ⟶ False) ⟶ False) ⟶ ((x52 x15 ⟶ False) ⟶ False) ⟶ ((x64 x16 ⟶ False) ⟶ False) ⟶ ((x62 x16 ⟶ False) ⟶ False) ⟶ ((x52 x16 ⟶ False) ⟶ False) ⟶ ((x58 x16 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x44 x18 ⟶ False) ⟶ False) ⟶ (x0 x18 ⟶ False) ⟶ (x64 x43 ⟶ False) ⟶ ((x62 x43 ⟶ False) ⟶ False) ⟶ ((x52 x43 ⟶ False) ⟶ False) ⟶ ((x61 x19 ⟶ False) ⟶ False) ⟶ ((x52 x19 ⟶ False) ⟶ False) ⟶ ((x64 x20 ⟶ False) ⟶ False) ⟶ ((x61 x20 ⟶ False) ⟶ False) ⟶ ((x52 x20 ⟶ False) ⟶ False) ⟶ ((x58 x20 ⟶ False) ⟶ False) ⟶ (x0 x21 ⟶ False) ⟶ ((x44 x42 ⟶ False) ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ (x64 x41 ⟶ False) ⟶ ((x61 x41 ⟶ False) ⟶ False) ⟶ ((x52 x41 ⟶ False) ⟶ False) ⟶ ((x52 x22 ⟶ False) ⟶ False) ⟶ ((x64 x40 ⟶ False) ⟶ False) ⟶ ((x0 x23 ⟶ False) ⟶ False) ⟶ ((x44 x39 ⟶ False) ⟶ False) ⟶ (x0 x39 ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x38 (x38 x65) = x38 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x54 (x54 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x8 (x8 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x50 (x50 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x51 (x51 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x64 x68 ⟶ x64 x65 ⟶ x58 x67 ⟶ x58 x66 ⟶ x68 = x67 ⟶ x65 = x66 ⟶ (x48 x68 x65 = x56 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x58 x65 ⟶ x66 = x65 ⟶ (x37 x66 = x54 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x64 x68 ⟶ x64 x65 ⟶ x58 x67 ⟶ x58 x66 ⟶ x68 = x67 ⟶ x65 = x66 ⟶ (x46 x68 x65 = x55 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x58 x65 ⟶ x66 = x65 ⟶ (x50 x66 = x8 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (x36 x5 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x55 x66 x65) ⟶ False) ⟶ False) ⟶ ((x44 x4 ⟶ False) ⟶ False) ⟶ (x0 x49 ⟶ False) ⟶ ((x17 x4 ⟶ False) ⟶ False) ⟶ ((x17 x5 ⟶ False) ⟶ False) ⟶ ((x62 x10 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ ((x52 (x37 x12) ⟶ False) ⟶ False) ⟶ ((x0 (x37 x12) ⟶ False) ⟶ False) ⟶ ((x52 (x37 x10) ⟶ False) ⟶ False) ⟶ ((x0 (x37 x10) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x52 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ ((x61 x12 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x58 (x8 x65) ⟶ False) ⟶ False) ⟶ ((x35 x5 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x52 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x52 x66 ⟶ x52 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x52 x66 ⟶ x52 x65 ⟶ (x0 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x52 x66 ⟶ (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x52 x66 ⟶ (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ x0 (x46 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x62 (x48 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ x62 (x48 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x56 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 (x48 x65 x66) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x48 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x56 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 (x48 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x56 x65 x66) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ x62 (x37 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x56 x66 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 (x37 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x54 x65) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ ((x52 x10 ⟶ False) ⟶ False) ⟶ (x64 x12 ⟶ False) ⟶ ((x24 x49 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ x62 (x46 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x62 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x62 x65 ⟶ x64 x65 ⟶ (x62 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x62 x65 ⟶ x64 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x62 (x46 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x54 x65) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ x61 (x46 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ (x61 x66 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x64 x65 ⟶ (x61 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x64 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x61 x66 ⟶ x52 x65 ⟶ x61 x65 ⟶ (x61 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x61 x66 ⟶ x52 x65 ⟶ x61 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x55 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x62 x66 ⟶ x52 x65 ⟶ x62 x65 ⟶ (x61 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x62 x66 ⟶ x52 x65 ⟶ x62 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x55 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x61 x66 ⟶ x52 x65 ⟶ x62 x65 ⟶ (x62 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x61 x66 ⟶ x52 x65 ⟶ x62 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x55 x65 x66) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x55 x66 x65) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ ((x52 x12 ⟶ False) ⟶ False) ⟶ (x64 x10 ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ x62 (x38 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x62 x65 ⟶ (x61 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x62 x65 ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x61 x65 ⟶ (x62 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x61 x65 ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x8 x65) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x58 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ x61 (x50 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x8 x65) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x58 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ x62 (x50 x65) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x59 x65 (x60 x66) ⟶ (x7 (x25 x65 x66) x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x59 (x34 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x59 x65 (x60 x67) ⟶ x7 x66 x67 x65 ⟶ (x59 x66 x67 ⟶ False) ⟶ False) ⟶ ((x59 x33 x49 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x52 (x48 x66 x65) ⟶ False) ⟶ False) ⟶ ((x7 x57 x5 x53 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x52 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x58 (x54 x65) ⟶ False) ⟶ False) ⟶ ((x59 x53 (x60 x5) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x52 (x46 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x58 x65 ⟶ (x58 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x59 (x38 x65) x49 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x52 (x50 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x59 (x51 x65) x49 ⟶ False) ⟶ False) ⟶ ((x59 x9 x49 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 x49 ⟶ x59 x65 x49 ⟶ (x59 (x47 x66 x65) x49 ⟶ False) ⟶ False) ⟶ ((x59 x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 x49 ⟶ x59 x65 x49 ⟶ (x59 (x45 x66 x65) x49 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x48 x66 x65 = x46 x66 (x37 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x63 x57 x65 ⟶ False) ⟶ (x38 x65 = x51 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ x63 x57 x65 ⟶ (x38 x65 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x63 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x52 x66 ⟶ x52 x65 ⟶ (x46 x66 x65 = x46 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x58 x66 ⟶ x58 x65 ⟶ (x55 x66 x65 = x55 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x59 x66 x49 ⟶ x59 x65 x49 ⟶ (x45 x66 x65 = x45 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 (x60 x5) ⟶ (x35 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x52 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x52 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x52 x65 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 (x60 x49) ⟶ (x24 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x62 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x62 x65 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x62 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 . x35 x65 ⟶ (x32 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x35 x65 ⟶ (x24 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x61 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x61 x65 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ x61 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x58 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x26 x65 ⟶ (x35 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x31 x65 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x31 x65 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x30 x65 ⟶ (x26 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x17 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x53 ⟶ (x44 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x44 x66 ⟶ x59 x65 (x60 x66) ⟶ (x44 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x30 x66 ⟶ x59 x65 (x60 x66) ⟶ (x30 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x26 x66 ⟶ x59 x65 (x60 x66) ⟶ (x26 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x35 x66 ⟶ x59 x65 (x60 x66) ⟶ (x35 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x24 x66 ⟶ x59 x65 (x60 x66) ⟶ (x24 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x52 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x49 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 x5 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x44 x65 ⟶ (x30 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x32 x66 ⟶ x59 x65 (x60 x66) ⟶ (x32 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x44 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x44 x66 ⟶ x59 x65 x66 ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x30 x66 ⟶ x59 x65 x66 ⟶ (x29 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x26 x66 ⟶ x59 x65 x66 ⟶ (x27 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x35 x66 ⟶ x59 x65 x66 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x24 x66 ⟶ x59 x65 x66 ⟶ (x52 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x32 x66 ⟶ x59 x65 x66 ⟶ (x58 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x59 x65 (x60 x53) ⟶ (x44 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x65 x66 ⟶ x1 x66 x65 ⟶ False) ⟶ (x45 (x38 x28) (x38 (x47 x33 x28)) = x57 ⟶ False) ⟶ ((x28 = x11 ⟶ False) ⟶ (x28 = x9 ⟶ False) ⟶ False) ⟶ ((x59 x28 x49 ⟶ False) ⟶ False) ⟶ False (proof)