Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../d8e65..
PUdmK../8e848..
vout
PrPhD../da506.. 102.65 bars
TMRY7../15072.. ownership of e4055.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMbrK../69a90.. ownership of acc97.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUhhJ../e7dbf.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem e4055.. : ∀ 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 . x61 x63 ⟶ (x63 = x62 ⟶ False) ⟶ x61 x62 ⟶ False) ⟶ (∀ x62 x63 . x0 x62 x63 ⟶ x61 x63 ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ (x62 = x60 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x0 x62 x63 ⟶ x2 x63 (x1 x64) ⟶ x61 x64 ⟶ False) ⟶ (∀ x62 x63 x64 x65 x66 . (x59 x66 ⟶ False) ⟶ x49 x66 ⟶ x58 x66 ⟶ x2 x62 (x50 x66) ⟶ x2 x65 (x50 x66) ⟶ x2 x63 (x50 x66) ⟶ x57 x64 ⟶ x51 x64 (x50 x66) (x50 x66) ⟶ x56 x64 (x50 x66) (x50 x66) ⟶ x2 x64 (x1 (x55 (x50 x66) (x50 x66))) ⟶ x52 x64 x66 ⟶ x54 (x50 x66) (x50 x66) x64 x62 = x62 ⟶ x53 x66 x65 x62 (x54 (x50 x66) (x50 x66) x64 x65) ⟶ (x65 = x62 ⟶ False) ⟶ (x53 x66 x63 x62 (x54 (x50 x66) (x50 x66) x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x0 x63 x64 ⟶ x2 x64 (x1 x62) ⟶ (x2 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x48 x63 x62 ⟶ (x2 x63 (x1 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x2 x63 (x1 x62) ⟶ (x48 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x59 x63 ⟶ False) ⟶ x49 x63 ⟶ x58 x63 ⟶ x57 x62 ⟶ x51 x62 (x50 x63) (x50 x63) ⟶ x56 x62 (x50 x63) (x50 x63) ⟶ x2 x62 (x1 (x55 (x50 x63) (x50 x63))) ⟶ x47 x63 (x46 x62 x63) (x45 x62 x63) (x54 (x50 x63) (x50 x63) x62 (x46 x62 x63)) (x54 (x50 x63) (x50 x63) x62 (x45 x62 x63)) ⟶ (x52 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x59 x63 ⟶ False) ⟶ x49 x63 ⟶ x58 x63 ⟶ x57 x62 ⟶ x51 x62 (x50 x63) (x50 x63) ⟶ x56 x62 (x50 x63) (x50 x63) ⟶ x2 x62 (x1 (x55 (x50 x63) (x50 x63))) ⟶ (x2 (x45 x62 x63) (x50 x63) ⟶ False) ⟶ (x52 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x59 x63 ⟶ False) ⟶ x49 x63 ⟶ x58 x63 ⟶ x57 x62 ⟶ x51 x62 (x50 x63) (x50 x63) ⟶ x56 x62 (x50 x63) (x50 x63) ⟶ x2 x62 (x1 (x55 (x50 x63) (x50 x63))) ⟶ (x2 (x46 x62 x63) (x50 x63) ⟶ False) ⟶ (x52 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 . (x59 x65 ⟶ False) ⟶ x49 x65 ⟶ x58 x65 ⟶ x57 x62 ⟶ x51 x62 (x50 x65) (x50 x65) ⟶ x56 x62 (x50 x65) (x50 x65) ⟶ x2 x62 (x1 (x55 (x50 x65) (x50 x65))) ⟶ x52 x62 x65 ⟶ x2 x64 (x50 x65) ⟶ x2 x63 (x50 x65) ⟶ (x47 x65 x64 x63 (x54 (x50 x65) (x50 x65) x62 x64) (x54 (x50 x65) (x50 x65) x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x2 x62 x63 ⟶ (x61 x63 ⟶ False) ⟶ (x0 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x0 x63 x62 ⟶ (x2 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 x66 x67 . (x59 x67 ⟶ False) ⟶ x49 x67 ⟶ x58 x67 ⟶ x2 x62 (x50 x67) ⟶ x2 x66 (x50 x67) ⟶ x2 x63 (x50 x67) ⟶ x2 x65 (x50 x67) ⟶ x2 x64 (x50 x67) ⟶ x44 x67 x66 x62 x62 x65 ⟶ x44 x67 x63 x62 x62 x64 ⟶ x47 x67 x66 x63 x65 x64 ⟶ (x43 x67 x62 x66 x63 ⟶ False) ⟶ (x44 x67 x66 x63 x64 x65 ⟶ False) ⟶ False) ⟶ (x61 x3 ⟶ False) ⟶ (∀ x62 . (x48 x62 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 . (x61 x65 ⟶ False) ⟶ x57 x62 ⟶ x51 x62 x65 x64 ⟶ x2 x62 (x1 (x55 x65 x64)) ⟶ x2 x63 x65 ⟶ (x54 x65 x64 x62 x63 = x4 x62 x63 ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ (x61 x41 ⟶ False) ⟶ (∀ x62 x63 . (x57 (x40 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x5 (x40 x62 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x39 (x40 x63 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x6 (x40 x62 x63) ⟶ False) ⟶ False) ⟶ (x38 x37 ⟶ False) ⟶ ((x57 x37 ⟶ False) ⟶ False) ⟶ ((x6 x37 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ x61 (x8 x62) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ (x2 (x8 x62) (x1 (x50 x62)) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ x61 (x10 x62 x63) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ (x57 (x10 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ (x5 (x10 x62 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ (x39 (x10 x62 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ (x6 (x10 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 x63 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ (x2 (x10 x62 x63) (x1 (x55 x63 x62)) ⟶ False) ⟶ False) ⟶ (x61 x11 ⟶ False) ⟶ (∀ x62 . (x56 (x36 x62) x62 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x51 (x36 x62) x62 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x35 (x36 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x57 (x36 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x5 (x36 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x39 (x36 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x6 (x36 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x2 (x36 x62) (x1 (x55 x62 x62)) ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ ((x57 x33 ⟶ False) ⟶ False) ⟶ ((x6 x33 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x59 x62 ⟶ False) ⟶ x9 x62 ⟶ x12 (x13 x62) ⟶ False) ⟶ (∀ x62 . (x59 x62 ⟶ False) ⟶ x9 x62 ⟶ (x2 (x13 x62) (x1 (x50 x62)) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ (x12 (x14 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ x61 (x14 x62) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ (x2 (x14 x62) (x1 (x50 x62)) ⟶ False) ⟶ False) ⟶ ((x61 x32 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x5 (x15 x62 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x39 (x15 x63 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x6 (x15 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x61 (x15 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x2 (x15 x62 x63) (x1 (x55 x63 x62)) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x57 (x31 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x5 (x31 x62 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x39 (x31 x63 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x6 (x31 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x2 (x31 x62 x63) (x1 (x55 x63 x62)) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x51 (x16 x62 x63) x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x57 (x16 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x5 (x16 x62 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x39 (x16 x63 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x6 (x16 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . (x2 (x16 x62 x63) (x1 (x55 x63 x62)) ⟶ False) ⟶ False) ⟶ ((x57 x17 ⟶ False) ⟶ False) ⟶ ((x6 x17 ⟶ False) ⟶ False) ⟶ (∀ x62 . (x18 x62 ⟶ False) ⟶ x9 x62 ⟶ x19 (x50 x62) ⟶ False) ⟶ (∀ x62 . x18 x62 ⟶ x9 x62 ⟶ (x19 (x50 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 . x59 x62 ⟶ x9 x62 ⟶ (x12 (x50 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x59 x62 ⟶ False) ⟶ x9 x62 ⟶ x12 (x50 x62) ⟶ False) ⟶ (∀ x62 . (x7 x62 ⟶ False) ⟶ x9 x62 ⟶ x61 (x50 x62) ⟶ False) ⟶ ((x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x62 . x7 x62 ⟶ x9 x62 ⟶ (x61 (x50 x62) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x42 x64 ⟶ x6 x62 ⟶ x5 x62 x64 ⟶ x57 x62 ⟶ (x57 (x4 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x42 x64 ⟶ x6 x62 ⟶ x5 x62 x64 ⟶ x57 x62 ⟶ (x6 (x4 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x62 . (x2 (x30 x62) x62 ⟶ False) ⟶ False) ⟶ ((x9 x20 ⟶ False) ⟶ False) ⟶ ((x58 x29 ⟶ False) ⟶ False) ⟶ (∀ x62 . x58 x62 ⟶ (x9 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 . (x61 x65 ⟶ False) ⟶ x57 x62 ⟶ x51 x62 x65 x64 ⟶ x2 x62 (x1 (x55 x65 x64)) ⟶ x2 x63 x65 ⟶ (x2 (x54 x65 x64 x62 x63) x64 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 . (x7 x65 ⟶ False) ⟶ x58 x65 ⟶ x2 x64 (x50 x65) ⟶ x2 x62 (x50 x65) ⟶ x2 x63 (x50 x65) ⟶ x44 x65 x64 x62 x62 x63 ⟶ (x53 x65 x64 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 x65 . (x7 x65 ⟶ False) ⟶ x58 x65 ⟶ x2 x64 (x50 x65) ⟶ x2 x62 (x50 x65) ⟶ x2 x63 (x50 x65) ⟶ x53 x65 x64 x62 x63 ⟶ (x44 x65 x64 x62 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x21 x62 x60 ⟶ (x7 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x42 x63 ⟶ x2 x62 (x1 x63) ⟶ (x42 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x7 x62 ⟶ (x21 x62 x60 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . (x61 x64 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ x2 x63 (x1 (x55 x64 x62)) ⟶ x57 x63 ⟶ x51 x63 x64 x62 ⟶ (x51 x63 x64 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . (x61 x64 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ x2 x63 (x1 (x55 x64 x62)) ⟶ x57 x63 ⟶ x51 x63 x64 x62 ⟶ x61 x63 ⟶ False) ⟶ (∀ x62 x63 x64 . (x61 x64 ⟶ False) ⟶ (x61 x62 ⟶ False) ⟶ x2 x63 (x1 (x55 x64 x62)) ⟶ x57 x63 ⟶ x51 x63 x64 x62 ⟶ (x57 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x42 x63 ⟶ x2 x62 x63 ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x42 x63 ⟶ x2 x62 x63 ⟶ (x6 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x18 x62 ⟶ False) ⟶ x59 x62 ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ (x42 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x59 x62 ⟶ (x18 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63)) ⟶ x57 x64 ⟶ x34 x64 ⟶ x28 x64 x63 ⟶ (x56 x64 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63)) ⟶ x57 x64 ⟶ x34 x64 ⟶ x28 x64 x63 ⟶ (x57 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 . x12 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x38 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x12 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x12 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x6 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x18 x62 ⟶ False) ⟶ x18 x62 ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x18 x62 ⟶ False) ⟶ x7 x62 ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62)) ⟶ x57 x64 ⟶ x56 x64 x63 x62 ⟶ (x28 x64 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62)) ⟶ x57 x64 ⟶ x56 x64 x63 x62 ⟶ (x34 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62)) ⟶ x57 x64 ⟶ x56 x64 x63 x62 ⟶ (x57 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 . x6 x62 ⟶ x57 x62 ⟶ (x38 x62 ⟶ False) ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x6 x62 ⟶ x57 x62 ⟶ (x38 x62 ⟶ False) ⟶ (x6 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x6 x62 ⟶ x57 x62 ⟶ (x38 x62 ⟶ False) ⟶ x12 x62 ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x7 x62 ⟶ (x18 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x7 x62 ⟶ (x7 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x61 x64 ⟶ x2 x62 (x1 (x55 x63 x64)) ⟶ (x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x2 x63 (x1 (x55 x62 x62)) ⟶ x51 x63 x62 x62 ⟶ (x35 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x38 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x6 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x61 x64 ⟶ x2 x62 (x1 (x55 x64 x63)) ⟶ (x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . (x61 x64 ⟶ False) ⟶ x2 x62 (x1 (x55 x63 x64)) ⟶ x51 x62 x63 x64 ⟶ (x35 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x6 x63 ⟶ x57 x63 ⟶ x2 x62 (x1 x63) ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x59 x62 ⟶ False) ⟶ x7 x62 ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63)) ⟶ (x5 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62)) ⟶ (x39 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . (x61 x64 ⟶ False) ⟶ x61 x62 ⟶ x2 x63 (x1 (x55 x64 x62)) ⟶ x35 x63 x64 ⟶ False) ⟶ (∀ x62 x63 x64 . x61 x64 ⟶ x2 x62 (x1 (x55 x64 x63)) ⟶ x51 x62 x64 x63 ⟶ (x35 x62 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x34 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ x6 x62 ⟶ x57 x62 ⟶ (x6 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x7 x62 ⟶ (x59 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63)) ⟶ (x6 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x61 x64 ⟶ x2 x62 (x1 (x55 x64 x63)) ⟶ (x35 x62 x64 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 x64 . x2 x63 (x1 (x55 x64 x62)) ⟶ x35 x63 x64 ⟶ (x51 x63 x64 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x61 x62 ⟶ (x57 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x59 x62 ⟶ False) ⟶ x7 x62 ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x21 x62 x3 ⟶ (x59 x62 ⟶ False) ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ x21 x62 x3 ⟶ x7 x62 ⟶ False) ⟶ (∀ x62 . x9 x62 ⟶ (x7 x62 ⟶ False) ⟶ x59 x62 ⟶ (x21 x62 x3 ⟶ False) ⟶ False) ⟶ (∀ x62 x63 . x0 x62 x63 ⟶ x0 x63 x62 ⟶ False) ⟶ (x44 x22 x25 x23 (x54 (x50 x22) (x50 x22) x24 x23) (x54 (x50 x22) (x50 x22) x24 x25) ⟶ False) ⟶ (x43 x22 x27 x25 x23 ⟶ False) ⟶ (x26 = x27 ⟶ False) ⟶ ((x53 x22 x26 x27 (x54 (x50 x22) (x50 x22) x24 x26) ⟶ False) ⟶ False) ⟶ ((x54 (x50 x22) (x50 x22) x24 x27 = x27 ⟶ False) ⟶ False) ⟶ ((x52 x24 x22 ⟶ False) ⟶ False) ⟶ ((x2 x24 (x1 (x55 (x50 x22) (x50 x22))) ⟶ False) ⟶ False) ⟶ ((x56 x24 (x50 x22) (x50 x22) ⟶ False) ⟶ False) ⟶ ((x51 x24 (x50 x22) (x50 x22) ⟶ False) ⟶ False) ⟶ ((x57 x24 ⟶ False) ⟶ False) ⟶ ((x2 x23 (x50 x22) ⟶ False) ⟶ False) ⟶ ((x2 x25 (x50 x22) ⟶ False) ⟶ False) ⟶ ((x2 x26 (x50 x22) ⟶ False) ⟶ False) ⟶ ((x2 x27 (x50 x22) ⟶ False) ⟶ False) ⟶ ((x58 x22 ⟶ False) ⟶ False) ⟶ ((x49 x22 ⟶ False) ⟶ False) ⟶ (x59 x22 ⟶ False) ⟶ False (proof)