Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../0401e..
PUNeF../97035..
vout
PrPhD../a444f.. 102.66 bars
TMMce../cd3af.. ownership of a4380.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMdk2../23198.. ownership of 1c4dc.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUSz8../5d352.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem a4380.. : ∀ 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 ⟶ (x66 = x65 ⟶ False) ⟶ x64 x65 ⟶ False) ⟶ (∀ x65 x66 . x0 x65 x66 ⟶ x64 x66 ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x65 = x63 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x65 x66 ⟶ x2 x66 (x1 x67) ⟶ x64 x67 ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x66 x67 ⟶ x2 x67 (x1 x65) ⟶ (x2 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x3 x65 ⟶ x10 x65 ⟶ x4 x66 ⟶ x8 x66 = x9 x65 ⟶ x7 x66 x65 = x6 (x9 x66) ⟶ (x65 = x5 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 x65 ⟶ (x2 x66 (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x2 x66 (x1 x65) ⟶ (x62 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x2 x65 x66 ⟶ (x64 x66 ⟶ False) ⟶ (x0 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 x65 ⟶ (x2 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 x67 x66)) ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ x60 x67 x66 x68 x65 ⟶ (x60 x67 x66 x65 x68 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 x67 x66)) ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ (x60 x67 x66 x68 x68 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x62 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 x67 x66)) ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ x68 = x65 ⟶ (x60 x67 x66 x68 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 x67 x66)) ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ x60 x67 x66 x68 x65 ⟶ (x68 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x11 x65 = x6 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x58 x66 x65 ⟶ (x59 x65 x66 = x8 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x13 x66 x65 ⟶ (x12 x65 x66 = x9 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x10 x70 ⟶ x2 x70 (x1 (x61 x65 x66)) ⟶ x10 x69 ⟶ x2 x69 (x1 (x61 x67 x68)) ⟶ (x57 x65 x66 x67 x68 x70 x69 = x7 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x8 (x6 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x9 (x6 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x10 (x14 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x13 (x14 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x15 (x14 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x14 x65) ⟶ False) ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ (x64 x17 ⟶ False) ⟶ (∀ x65 . (x18 x65 ⟶ False) ⟶ x18 (x19 x65) ⟶ False) ⟶ (∀ x65 . (x18 x65 ⟶ False) ⟶ (x2 (x19 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x10 (x20 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x58 (x20 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x13 (x20 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x20 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x18 (x21 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ x64 (x21 x65) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x2 (x21 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (x56 x55 ⟶ False) ⟶ ((x10 x55 ⟶ False) ⟶ False) ⟶ ((x3 x55 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x23 (x22 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x2 (x22 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ ((x10 x24 ⟶ False) ⟶ False) ⟶ ((x15 x24 ⟶ False) ⟶ False) ⟶ ((x3 x24 ⟶ False) ⟶ False) ⟶ (x64 x24 ⟶ False) ⟶ (∀ x65 . x23 (x25 x65) x65 ⟶ False) ⟶ (∀ x65 . (x2 (x25 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x58 (x26 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x13 (x26 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x26 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ x64 (x54 x65 x66) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x10 (x54 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x58 (x54 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x13 (x54 x65 x66) x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x3 (x54 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ (x2 (x54 x65 x66) (x1 (x61 x66 x65)) ⟶ False) ⟶ False) ⟶ ((x10 x53 ⟶ False) ⟶ False) ⟶ ((x15 x53 ⟶ False) ⟶ False) ⟶ ((x3 x53 ⟶ False) ⟶ False) ⟶ (x64 x27 ⟶ False) ⟶ (∀ x65 . (x64 (x52 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x52 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ ((x15 x51 ⟶ False) ⟶ False) ⟶ ((x3 x51 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x50 (x49 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x28 (x49 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x48 (x49 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x29 (x49 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x47 (x49 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x58 (x49 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x13 (x49 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x49 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x49 x65) (x1 (x61 x65 x65)) ⟶ False) ⟶ False) ⟶ ((x4 x30 ⟶ False) ⟶ False) ⟶ ((x10 x30 ⟶ False) ⟶ False) ⟶ ((x3 x30 ⟶ False) ⟶ False) ⟶ ((x64 x46 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ x64 (x31 x65) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x2 (x31 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x58 (x32 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x13 (x32 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x32 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 (x32 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x2 (x32 x65 x66) (x1 (x61 x66 x65)) ⟶ False) ⟶ False) ⟶ ((x3 x45 ⟶ False) ⟶ False) ⟶ (x64 x45 ⟶ False) ⟶ (∀ x65 x66 . (x10 (x44 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x58 (x44 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x13 (x44 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x44 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x2 (x44 x65 x66) (x1 (x61 x66 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x33 (x34 x65 x66) x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x10 (x34 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x58 (x34 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x13 (x34 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x34 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x2 (x34 x65 x66) (x1 (x61 x66 x65)) ⟶ False) ⟶ False) ⟶ ((x10 x35 ⟶ False) ⟶ False) ⟶ ((x3 x35 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 x67 (x61 x65 x66))) ⟶ (x3 (x8 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ x3 x65 ⟶ x64 (x8 x65) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x61 (x61 x66 x65) x67)) ⟶ (x3 (x9 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ x3 x65 ⟶ x64 (x9 x65) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x64 x65 ⟶ False) ⟶ x64 (x6 x65) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x4 x66 ⟶ x3 x65 ⟶ x10 x65 ⟶ x4 x65 ⟶ (x4 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x4 x66 ⟶ x3 x65 ⟶ x10 x65 ⟶ x4 x65 ⟶ (x3 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x61 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ x4 x65 ⟶ (x4 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ x4 x65 ⟶ (x10 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ x4 x65 ⟶ (x3 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x9 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x4 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x28 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x48 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x29 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x10 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x13 x67 x65 ⟶ x3 x66 ⟶ (x13 (x7 x67 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x13 x67 x66 ⟶ x3 x65 ⟶ (x3 (x7 x67 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x10 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x3 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x58 x67 x65 ⟶ x3 x66 ⟶ (x58 (x7 x66 x67) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x58 x67 x66 ⟶ x3 x65 ⟶ (x3 (x7 x65 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x58 (x6 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x13 (x6 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x18 x65 ⟶ x3 x65 ⟶ (x18 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x18 x65 ⟶ x3 x65 ⟶ (x18 (x9 x65) ⟶ False) ⟶ False) ⟶ ((x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 (x1 x65) ⟶ False) ⟶ (∀ x65 . (x18 x65 ⟶ False) ⟶ x3 x65 ⟶ x10 x65 ⟶ x18 (x9 x65) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x3 x65 ⟶ x15 x65 ⟶ (x15 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x3 x65 ⟶ x15 x65 ⟶ (x3 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ (x3 (x7 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ (x64 (x7 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ x18 (x8 x65) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ (x3 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ (x64 (x7 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ x56 x65 ⟶ (x18 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ (x64 x65 ⟶ False) ⟶ x64 (x61 x66 x65) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x9 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x15 x65 ⟶ x10 x65 ⟶ (x43 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x36 x65) x65 ⟶ False) ⟶ False) ⟶ ((x64 x42 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x11 x65) (x1 (x61 x65 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x50 (x11 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x6 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x3 (x7 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x58 x66 x65 ⟶ (x2 (x59 x65 x66) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x10 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x3 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x13 x66 x65 ⟶ (x2 (x12 x65 x66) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x10 x70 ⟶ x2 x70 (x1 (x61 x65 x66)) ⟶ x10 x69 ⟶ x2 x69 (x1 (x61 x67 x68)) ⟶ (x2 (x57 x65 x66 x67 x68 x70 x69) (x1 (x61 x65 x68)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x10 x70 ⟶ x2 x70 (x1 (x61 x65 x66)) ⟶ x10 x69 ⟶ x2 x69 (x1 (x61 x67 x68)) ⟶ (x10 (x57 x65 x66 x67 x68 x70 x69) ⟶ False) ⟶ False) ⟶ ((x63 = x42 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x61 x66 x67)) ⟶ x67 = x63 ⟶ x65 = x63 ⟶ (x33 x65 x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x61 x66 x67)) ⟶ x67 = x63 ⟶ x33 x65 x66 x67 ⟶ (x65 = x63 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 (x61 x65 x67)) ⟶ (x67 = x63 ⟶ False) ⟶ x65 = x12 x65 x66 ⟶ (x33 x66 x65 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x61 x66 x67)) ⟶ (x67 = x63 ⟶ False) ⟶ x33 x65 x66 x67 ⟶ (x66 = x12 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x16 x66 ⟶ x2 x65 (x1 x66) ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x58 x65 x66 ⟶ (x58 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x58 x65 x66 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x58 x65 x66 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x16 x66 ⟶ x2 x65 x66 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x16 x66 ⟶ x2 x65 x66 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x13 x65 x66 ⟶ (x13 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x13 x65 x66 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x3 x65 ⟶ x13 x65 x66 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x58 x67 x65 ⟶ x2 x66 (x1 x67) ⟶ (x58 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x18 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x18 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x18 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x18 x66 ⟶ x2 x65 (x1 x66) ⟶ (x18 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x3 x67 ⟶ x13 x67 x65 ⟶ x2 x66 (x1 x67) ⟶ (x13 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ x18 x65 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x2 x65 (x1 x66) ⟶ x23 x65 x66 ⟶ False) ⟶ (∀ x65 x66 x67 . x64 x67 ⟶ x2 x65 (x1 (x61 x66 x67)) ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ (x15 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x2 x66 (x1 (x61 x65 x65)) ⟶ x33 x66 x65 x65 ⟶ (x50 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ x2 x65 (x1 x66) ⟶ x64 x65 ⟶ (x23 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x64 x67 ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ (x37 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x29 x65 ⟶ x28 x65 ⟶ (x47 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x3 x65 ⟶ x29 x65 ⟶ x28 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x64 x67 ⟶ False) ⟶ x2 x65 (x1 (x61 x66 x67)) ⟶ x33 x65 x66 x67 ⟶ (x50 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x10 x66 ⟶ x2 x65 (x1 x66) ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ x2 x65 (x1 x66) ⟶ (x23 x65 x66 ⟶ False) ⟶ x64 x65 ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x61 x65 x66)) ⟶ (x58 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x61 x66 x65)) ⟶ (x13 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 ⟶ x2 x65 (x1 x66) ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x64 x67 ⟶ False) ⟶ x64 x65 ⟶ x2 x66 (x1 (x61 x67 x65)) ⟶ x50 x66 x67 ⟶ False) ⟶ (∀ x65 x66 x67 . x64 x67 ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ x33 x65 x67 x66 ⟶ (x50 x65 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ x3 x65 ⟶ x10 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x2 x65 (x1 x66) ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x61 x65 x66)) ⟶ (x3 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x64 x67 ⟶ x2 x65 (x1 (x61 x67 x66)) ⟶ (x50 x65 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 (x61 x67 x65)) ⟶ x50 x66 x67 ⟶ (x33 x66 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x65 x66 ⟶ x0 x66 x65 ⟶ False) ⟶ (x39 = x5 x38 ⟶ False) ⟶ (x41 = x63 ⟶ False) ⟶ (x40 = x63 ⟶ False) ⟶ ((x4 x38 ⟶ False) ⟶ False) ⟶ ((x60 x40 x40 (x57 x40 x41 x41 x40 x38 x39) (x11 x40) ⟶ False) ⟶ False) ⟶ ((x59 x41 x38 = x41 ⟶ False) ⟶ False) ⟶ ((x2 x39 (x1 (x61 x41 x40)) ⟶ False) ⟶ False) ⟶ ((x33 x39 x41 x40 ⟶ False) ⟶ False) ⟶ ((x10 x39 ⟶ False) ⟶ False) ⟶ ((x2 x38 (x1 (x61 x40 x41)) ⟶ False) ⟶ False) ⟶ ((x33 x38 x40 x41 ⟶ False) ⟶ False) ⟶ ((x10 x38 ⟶ False) ⟶ False) ⟶ False (proof)