Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../46fb9..
PUdn7../77af3..
vout
PrPhD../062fd.. 102.63 bars
TMS51../76211.. ownership of 0497a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMJAt../6c63b.. ownership of 8f0f9.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUM4J../82877.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 0497a.. : ∀ 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 . x60 x66 ⟶ x60 x65 ⟶ x66 = x65 ⟶ (x58 (x57 x66 x65) = x59 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ x58 (x57 x66 x65) = x59 ⟶ (x66 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x65 x66 ⟶ x55 x66 (x56 x67) ⟶ x0 x67 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x0 x65 ⟶ False) ⟶ (x62 x66 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x66 x67 ⟶ x55 x67 (x56 x65) ⟶ (x55 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 x66 ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x57 x65 x59 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 x65 ⟶ (x55 x66 (x56 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x55 x66 (x56 x65) ⟶ (x3 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x62 x66 ⟶ False) ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x54 x53 x65 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x55 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 . x60 x65 ⟶ (x54 x65 x59 = x59 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x66 x65 ⟶ (x55 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ x61 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ ((x55 x2 x52 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x4 x65 x59 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x57 (x51 x66) (x51 x65) = x57 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x4 (x51 x66) (x51 x65) = x51 (x4 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x60 x67 ⟶ x60 x65 ⟶ x60 x66 ⟶ (x54 (x54 x67 x65) x66 = x54 x67 (x54 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x60 x67 ⟶ x60 x65 ⟶ x60 x66 ⟶ (x4 (x4 x67 x65) x66 = x4 x67 (x4 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x60 x67 ⟶ x60 x65 ⟶ x60 x66 ⟶ (x54 (x4 x67 x65) x66 = x4 (x54 x67 x66) (x54 x65 x66) ⟶ False) ⟶ False) ⟶ ((x55 x6 x5 ⟶ False) ⟶ False) ⟶ ((x55 x6 x50 ⟶ False) ⟶ False) ⟶ ((x7 x6 x5 x50 ⟶ False) ⟶ False) ⟶ ((x61 x6 ⟶ False) ⟶ False) ⟶ (x0 x6 ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x54 x65 (x51 x53) = x51 x65 ⟶ False) ⟶ False) ⟶ ((x55 x53 x5 ⟶ False) ⟶ False) ⟶ ((x55 x53 x50 ⟶ False) ⟶ False) ⟶ ((x7 x53 x5 x50 ⟶ False) ⟶ False) ⟶ ((x61 x53 ⟶ False) ⟶ False) ⟶ (x0 x53 ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x4 x66 (x51 x65) = x57 x66 x65 ⟶ False) ⟶ False) ⟶ ((x55 x8 x5 ⟶ False) ⟶ False) ⟶ ((x55 x8 x50 ⟶ False) ⟶ False) ⟶ ((x7 x8 x5 x50 ⟶ False) ⟶ False) ⟶ ((x0 x8 ⟶ False) ⟶ False) ⟶ ((x51 (x51 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x51 (x51 x53) = x53 ⟶ False) ⟶ False) ⟶ ((x51 x6 = x51 x6 ⟶ False) ⟶ False) ⟶ ((x51 x53 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x51 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x54 (x51 x6) x53 = x51 x6 ⟶ False) ⟶ False) ⟶ ((x54 (x51 x6) x8 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x6 x53 = x6 ⟶ False) ⟶ False) ⟶ ((x54 x6 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x53 (x51 x6) = x51 x6 ⟶ False) ⟶ False) ⟶ ((x54 x53 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x54 x53 x53 = x53 ⟶ False) ⟶ False) ⟶ ((x54 x53 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x8 (x51 x6) = x8 ⟶ False) ⟶ False) ⟶ ((x54 x8 x6 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x8 x53 = x8 ⟶ False) ⟶ False) ⟶ ((x54 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x6) (x51 x6) = x8 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x6) (x51 x53) = x51 x53 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x6) x8 = x51 x6 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x53) (x51 x6) = x53 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x53) (x51 x53) = x8 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x53) x53 = x51 x6 ⟶ False) ⟶ False) ⟶ ((x57 (x51 x53) x8 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x57 x6 x6 = x8 ⟶ False) ⟶ False) ⟶ ((x57 x6 x53 = x53 ⟶ False) ⟶ False) ⟶ ((x57 x6 x8 = x6 ⟶ False) ⟶ False) ⟶ ((x57 x53 (x51 x53) = x6 ⟶ False) ⟶ False) ⟶ ((x57 x53 x6 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x57 x53 x53 = x8 ⟶ False) ⟶ False) ⟶ ((x57 x53 x8 = x53 ⟶ False) ⟶ False) ⟶ ((x57 x8 (x51 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x57 x8 (x51 x53) = x53 ⟶ False) ⟶ False) ⟶ ((x57 x8 x6 = x51 x6 ⟶ False) ⟶ False) ⟶ ((x57 x8 x53 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x57 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x6) x6 = x8 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x6) x53 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x53) (x51 x53) = x51 x6 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x53) x6 = x53 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x53) x53 = x8 ⟶ False) ⟶ False) ⟶ ((x4 (x51 x53) x8 = x51 x53 ⟶ False) ⟶ False) ⟶ ((x4 x6 (x51 x6) = x8 ⟶ False) ⟶ False) ⟶ ((x4 x6 (x51 x53) = x53 ⟶ False) ⟶ False) ⟶ ((x4 x6 x8 = x6 ⟶ False) ⟶ False) ⟶ ((x4 x53 (x51 x6) = x51 x53 ⟶ False) ⟶ False) ⟶ ((x4 x53 (x51 x53) = x8 ⟶ False) ⟶ False) ⟶ ((x4 x53 x53 = x6 ⟶ False) ⟶ False) ⟶ ((x4 x53 x8 = x53 ⟶ False) ⟶ False) ⟶ ((x4 x8 (x51 x6) = x51 x6 ⟶ False) ⟶ False) ⟶ ((x4 x8 (x51 x53) = x51 x53 ⟶ False) ⟶ False) ⟶ ((x4 x8 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x4 x8 x53 = x53 ⟶ False) ⟶ False) ⟶ ((x4 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x63 (x51 x6) (x51 x6) ⟶ False) ⟶ False) ⟶ ((x63 (x51 x6) (x51 x53) ⟶ False) ⟶ False) ⟶ ((x63 (x51 x6) x6 ⟶ False) ⟶ False) ⟶ ((x63 (x51 x6) x53 ⟶ False) ⟶ False) ⟶ ((x63 (x51 x6) x8 ⟶ False) ⟶ False) ⟶ (x63 (x51 x53) (x51 x6) ⟶ False) ⟶ ((x63 (x51 x53) (x51 x53) ⟶ False) ⟶ False) ⟶ ((x63 (x51 x53) x6 ⟶ False) ⟶ False) ⟶ ((x63 (x51 x53) x53 ⟶ False) ⟶ False) ⟶ ((x63 (x51 x53) x8 ⟶ False) ⟶ False) ⟶ (x63 x6 (x51 x6) ⟶ False) ⟶ (x63 x6 (x51 x53) ⟶ False) ⟶ ((x63 x6 x6 ⟶ False) ⟶ False) ⟶ (x63 x6 x53 ⟶ False) ⟶ (x63 x6 x8 ⟶ False) ⟶ (x63 x53 (x51 x6) ⟶ False) ⟶ (x63 x53 (x51 x53) ⟶ False) ⟶ ((x63 x53 x6 ⟶ False) ⟶ False) ⟶ ((x63 x53 x53 ⟶ False) ⟶ False) ⟶ (x63 x53 x8 ⟶ False) ⟶ (x63 x8 (x51 x6) ⟶ False) ⟶ (x63 x8 (x51 x53) ⟶ False) ⟶ ((x63 x8 x6 ⟶ False) ⟶ False) ⟶ ((x63 x8 x53 ⟶ False) ⟶ False) ⟶ ((x63 x8 x8 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x49 x66 ⟶ x49 x65 ⟶ (x63 x66 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x55 x65 (x56 x67) ⟶ x55 x66 x65 ⟶ (x7 x66 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x55 x65 (x56 x67) ⟶ x7 x66 x67 x65 ⟶ (x55 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x48 x65 = x47 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x55 x66 x5 ⟶ x64 x65 ⟶ (x9 x66 x65 = x4 x66 x65 ⟶ False) ⟶ False) ⟶ ((x59 = x2 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x10 x65 = x11 x65 ⟶ False) ⟶ False) ⟶ ((x50 = x52 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x13 x65 = x12 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x45 x65 = x46 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x58 x65 = x14 x65 ⟶ False) ⟶ False) ⟶ ((x49 x44 ⟶ False) ⟶ False) ⟶ ((x0 x44 ⟶ False) ⟶ False) ⟶ ((x64 x43 ⟶ False) ⟶ False) ⟶ ((x49 x43 ⟶ False) ⟶ False) ⟶ ((x60 x43 ⟶ False) ⟶ False) ⟶ ((x0 x43 ⟶ False) ⟶ False) ⟶ ((x62 x42 ⟶ False) ⟶ False) ⟶ ((x49 x42 ⟶ False) ⟶ False) ⟶ ((x64 x41 ⟶ False) ⟶ False) ⟶ ((x62 x41 ⟶ False) ⟶ False) ⟶ ((x49 x41 ⟶ False) ⟶ False) ⟶ ((x60 x41 ⟶ False) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ ((x15 x39 ⟶ False) ⟶ False) ⟶ (x0 x39 ⟶ False) ⟶ ((x61 x16 ⟶ False) ⟶ False) ⟶ ((x49 x16 ⟶ False) ⟶ False) ⟶ ((x64 x17 ⟶ False) ⟶ False) ⟶ ((x61 x17 ⟶ False) ⟶ False) ⟶ ((x49 x17 ⟶ False) ⟶ False) ⟶ ((x60 x17 ⟶ False) ⟶ False) ⟶ ((x60 x18 ⟶ False) ⟶ False) ⟶ (x0 x18 ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ ((x15 x38 ⟶ False) ⟶ False) ⟶ (x0 x38 ⟶ False) ⟶ ((x49 x37 ⟶ False) ⟶ False) ⟶ ((x64 x20 ⟶ False) ⟶ False) ⟶ ((x60 x36 ⟶ False) ⟶ False) ⟶ ((x0 x21 ⟶ False) ⟶ False) ⟶ ((x15 x35 ⟶ False) ⟶ False) ⟶ (x0 x35 ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x58 (x58 x65) = x58 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x14 (x14 x65) = x14 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x51 (x51 x65) = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x4 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x60 x66 ⟶ (x0 x65 ⟶ False) ⟶ x60 x65 ⟶ x0 (x54 x66 x65) ⟶ False) ⟶ (x22 x5 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x54 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x60 x65 ⟶ (x60 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x60 x65 ⟶ x0 (x51 x65) ⟶ False) ⟶ ((x15 x52 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x64 (x4 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ x62 (x14 x65) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x64 (x14 x65) ⟶ False) ⟶ False) ⟶ ((x40 x52 ⟶ False) ⟶ False) ⟶ ((x40 x5 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x60 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x60 x65 ⟶ (x64 (x14 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x60 x65 ⟶ x0 (x14 x65) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x60 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x60 (x54 x66 x65) ⟶ False) ⟶ False) ⟶ ((x34 x5 ⟶ False) ⟶ False) ⟶ ((x64 (x14 x59) ⟶ False) ⟶ False) ⟶ ((x0 (x14 x59) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x60 (x4 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x11 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x64 (x12 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x54 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x54 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x54 x65 x66) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x54 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x61 (x57 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x62 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x62 (x57 x65 x66) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x60 (x11 x65) ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x64 (x46 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x61 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x57 x65 x66) ⟶ False) ⟶ (∀ x65 x66 . (x62 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x57 x66 x65) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x51 x65) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x60 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x51 x65) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x60 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x62 (x4 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x62 (x4 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x61 (x4 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x64 x66 ⟶ (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x61 (x4 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 x66 ⟶ False) ⟶ x64 x66 ⟶ (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x4 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x55 x65 (x56 x66) ⟶ (x7 (x23 x65 x66) x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x55 (x33 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x55 x65 (x56 x67) ⟶ x7 x66 x67 x65 ⟶ (x55 x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x55 (x48 x65) x5 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x55 x66 x5 ⟶ x64 x65 ⟶ (x55 (x9 x66 x65) x5 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x47 x65) ⟶ False) ⟶ False) ⟶ ((x7 x59 x5 x50 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x55 (x10 x65) x5 ⟶ False) ⟶ False) ⟶ ((x55 x50 (x56 x5) ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x60 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x55 (x13 x65) x5 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x55 (x45 x65) x5 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x55 (x58 x65) x5 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x64 (x14 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x11 x65 = x54 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x60 x65 ⟶ (x14 x65 = x48 (x9 (x10 (x45 x65)) (x10 (x13 x65))) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x49 x66 ⟶ x49 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x63 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x55 x66 x5 ⟶ x64 x65 ⟶ (x9 x66 x65 = x9 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x54 x66 x65 = x54 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x60 x66 ⟶ x60 x65 ⟶ (x4 x66 x65 = x4 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 (x56 x5) ⟶ (x34 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x49 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x49 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x49 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x49 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x49 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x62 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x62 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x62 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 . x34 x65 ⟶ (x32 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x49 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x49 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x34 x65 ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x61 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x61 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x61 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x60 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x24 x65 ⟶ (x34 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x30 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x30 x65 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x30 x65 ⟶ (x60 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x25 x65 ⟶ (x24 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x40 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x50 ⟶ (x15 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x15 x66 ⟶ x55 x65 (x56 x66) ⟶ (x15 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x25 x66 ⟶ x55 x65 (x56 x66) ⟶ (x25 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x24 x66 ⟶ x55 x65 (x56 x66) ⟶ (x24 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x34 x66 ⟶ x55 x65 (x56 x66) ⟶ (x34 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x31 x66 ⟶ x55 x65 (x56 x66) ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 x5 ⟶ (x60 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x15 x65 ⟶ (x25 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x32 x66 ⟶ x55 x65 (x56 x66) ⟶ (x32 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x15 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x15 x66 ⟶ x55 x65 x66 ⟶ (x30 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x25 x66 ⟶ x55 x65 x66 ⟶ (x26 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x24 x66 ⟶ x55 x65 x66 ⟶ (x29 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x34 x66 ⟶ x55 x65 x66 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x31 x66 ⟶ x55 x65 x66 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x32 x66 ⟶ x55 x65 x66 ⟶ (x60 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x55 x65 (x56 x50) ⟶ (x15 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x65 x66 ⟶ x1 x66 x65 ⟶ False) ⟶ ((x63 (x58 (x57 x28 x27)) x59 ⟶ False) ⟶ (x28 = x27 ⟶ False) ⟶ False) ⟶ ((x63 (x58 (x57 x28 x27)) x59 ⟶ False) ⟶ x63 (x58 (x57 x28 x27)) x59 ⟶ False) ⟶ (x28 = x27 ⟶ (x28 = x27 ⟶ False) ⟶ False) ⟶ (x28 = x27 ⟶ x63 (x58 (x57 x28 x27)) x59 ⟶ False) ⟶ ((x60 x27 ⟶ False) ⟶ False) ⟶ ((x60 x28 ⟶ False) ⟶ False) ⟶ False (proof)