Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../d2c69..
PUbNp../1c7f8..
vout
PrPhD../e50e0.. 3.39 bars
TMKq5../5cb39.. ownership of b2d8d.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMS3k../ec23e.. ownership of 88ad8.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUUjq../bdfe7.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem b2d8d.. : ∀ 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 : ι → ο . (∀ x67 x68 . x66 x68 ⟶ (x68 = x67 ⟶ False) ⟶ x66 x67 ⟶ False) ⟶ (∀ x67 x68 . x0 x67 x68 ⟶ x66 x68 ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x67 = x65 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . x0 x67 x68 ⟶ x2 x68 (x1 x69) ⟶ x66 x69 ⟶ False) ⟶ (∀ x67 x68 x69 . x0 x68 x69 ⟶ x2 x69 (x1 x67) ⟶ (x2 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x3 x68 x67 ⟶ (x2 x68 (x1 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x2 x68 (x1 x67) ⟶ (x3 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x2 x67 x68 ⟶ (x66 x68 ⟶ False) ⟶ (x0 x67 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . (x64 x68 ⟶ False) ⟶ x56 x68 ⟶ x63 x68 ⟶ x57 x68 ⟶ x62 x68 ⟶ x58 x68 ⟶ x2 x67 (x59 x68) ⟶ (x60 x68 x67 (x61 x68) = x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x0 x68 x67 ⟶ (x2 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ (x58 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ (x62 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ (x57 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ (x56 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x60 x67 (x60 x67 (x60 x67 (x54 x67) (x55 x67)) (x60 x67 (x54 x67) (x53 x67))) (x60 x67 (x53 x67) (x55 x67)) = x61 x67 ⟶ x60 x67 (x60 x67 (x54 x67) (x60 x67 (x54 x67) (x55 x67))) (x55 x67) = x61 x67 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ (x58 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ (x62 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ (x57 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ (x56 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x53 x67) (x59 x67) ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ (x58 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ (x62 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ (x57 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ (x56 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x55 x67) (x59 x67) ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ (x58 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ (x62 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ (x57 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ (x56 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ (x2 (x54 x67) (x59 x67) ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 x68 x69 x70 . (x64 x70 ⟶ False) ⟶ x58 x70 ⟶ (x64 x70 ⟶ False) ⟶ x56 x70 ⟶ x63 x70 ⟶ x57 x70 ⟶ x62 x70 ⟶ x58 x70 ⟶ x2 x69 (x59 x70) ⟶ x2 x67 (x59 x70) ⟶ x2 x68 (x59 x70) ⟶ (x60 x70 (x60 x70 x69 (x60 x70 x69 x67)) x67 = x61 x70 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 x70 . (x64 x70 ⟶ False) ⟶ x58 x70 ⟶ (x64 x70 ⟶ False) ⟶ x56 x70 ⟶ x63 x70 ⟶ x57 x70 ⟶ x62 x70 ⟶ x58 x70 ⟶ x2 x69 (x59 x70) ⟶ x2 x67 (x59 x70) ⟶ x2 x68 (x59 x70) ⟶ (x60 x70 (x60 x70 (x60 x70 x69 x67) (x60 x70 x69 x68)) (x60 x70 x68 x67) = x61 x70 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ (x64 x67 ⟶ False) ⟶ x56 x67 ⟶ x63 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x58 x67 ⟶ (x62 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x58 x67 ⟶ (x64 x67 ⟶ False) ⟶ x56 x67 ⟶ x63 x67 ⟶ x57 x67 ⟶ x62 x67 ⟶ x58 x67 ⟶ (x57 x67 ⟶ False) ⟶ False) ⟶ (x66 x52 ⟶ False) ⟶ (∀ x67 . (x3 x67 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 x70 . x51 x70 ⟶ x48 x70 (x47 x67 x67) x67 ⟶ x2 x70 (x1 (x47 (x47 x67 x67) x67)) ⟶ x2 x68 x67 ⟶ x2 x69 x67 ⟶ (x50 x67 x70 x68 x69 = x49 x70 x68 x69 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x66 x67 ⟶ False) ⟶ (x4 (x5 x67) x52 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x66 x67 ⟶ False) ⟶ (x2 (x5 x67) (x1 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x4 (x7 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x51 (x7 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x8 (x7 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x4 (x46 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ x66 (x9 x67) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ (x2 (x9 x67) (x1 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x11 x67 ⟶ False) ⟶ x11 (x12 x67) ⟶ False) ⟶ (∀ x67 . (x11 x67 ⟶ False) ⟶ (x2 (x12 x67) (x1 x67) ⟶ False) ⟶ False) ⟶ (x11 x13 ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ ((x8 x44 ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x42 (x43 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x10 (x43 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x41 x67 ⟶ False) ⟶ x10 x67 ⟶ x40 (x39 x67) ⟶ False) ⟶ (∀ x67 . (x41 x67 ⟶ False) ⟶ x10 x67 ⟶ (x2 (x39 x67) (x1 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ (x40 (x38 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ x66 (x38 x67) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ (x2 (x38 x67) (x1 (x59 x67)) ⟶ False) ⟶ False) ⟶ ((x41 x14 ⟶ False) ⟶ False) ⟶ (x64 x14 ⟶ False) ⟶ ((x15 x14 ⟶ False) ⟶ False) ⟶ ((x8 x37 ⟶ False) ⟶ False) ⟶ (x66 x37 ⟶ False) ⟶ ((x6 x36 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x41 x67 ⟶ False) ⟶ x15 x67 ⟶ x16 (x17 x67) x67 ⟶ False) ⟶ (∀ x67 . (x41 x67 ⟶ False) ⟶ x15 x67 ⟶ (x2 (x17 x67) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x16 (x18 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x2 (x18 x67) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x19 x67 ⟶ False) ⟶ x10 x67 ⟶ x11 (x59 x67) ⟶ False) ⟶ (∀ x67 . (x11 x67 ⟶ False) ⟶ x11 (x1 x67) ⟶ False) ⟶ (∀ x67 . x19 x67 ⟶ x10 x67 ⟶ (x11 (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x41 x67 ⟶ x10 x67 ⟶ (x40 (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x41 x67 ⟶ False) ⟶ x10 x67 ⟶ x40 (x59 x67) ⟶ False) ⟶ (∀ x67 x68 . (x8 (x47 x67 x68) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x64 x67 ⟶ False) ⟶ x10 x67 ⟶ x66 (x59 x67) ⟶ False) ⟶ (∀ x67 . x64 x67 ⟶ x10 x67 ⟶ (x66 (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x6 x68 ⟶ x42 x67 x68 ⟶ x10 x67 ⟶ (x4 (x59 x67) x68 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . (x11 x68 ⟶ False) ⟶ (x66 x67 ⟶ False) ⟶ x11 (x47 x67 x68) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x16 (x61 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . (x11 x68 ⟶ False) ⟶ (x66 x67 ⟶ False) ⟶ x11 (x47 x68 x67) ⟶ False) ⟶ (∀ x67 . (x2 (x20 x67) x67 ⟶ False) ⟶ False) ⟶ ((x15 x35 ⟶ False) ⟶ False) ⟶ ((x58 x21 ⟶ False) ⟶ False) ⟶ ((x10 x34 ⟶ False) ⟶ False) ⟶ ((x22 x23 ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x2 (x33 x67) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x22 x67 ⟶ (x2 (x24 x67) (x1 (x47 (x47 (x59 x67) (x59 x67)) (x59 x67))) ⟶ False) ⟶ False) ⟶ (∀ x67 . x22 x67 ⟶ (x48 (x24 x67) (x47 (x59 x67) (x59 x67)) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . x22 x67 ⟶ (x51 (x24 x67) ⟶ False) ⟶ False) ⟶ ((x66 x32 ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x10 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x58 x67 ⟶ (x15 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x58 x67 ⟶ (x22 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x22 x67 ⟶ (x10 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 x70 . x51 x70 ⟶ x48 x70 (x47 x67 x67) x67 ⟶ x2 x70 (x1 (x47 (x47 x67 x67) x67)) ⟶ x2 x68 x67 ⟶ x2 x69 x67 ⟶ (x2 (x50 x67 x70 x68 x69) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x2 (x61 x67) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . x22 x69 ⟶ x2 x67 (x59 x69) ⟶ x2 x68 (x59 x69) ⟶ (x2 (x60 x69 x67 x68) (x59 x69) ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 x67 ⟶ (x61 x67 = x33 x67 ⟶ False) ⟶ False) ⟶ ((x65 = x32 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . x22 x69 ⟶ x2 x67 (x59 x69) ⟶ x2 x68 (x59 x69) ⟶ (x60 x69 x67 x68 = x50 (x59 x69) (x24 x69) x67 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x42 x67 x65 ⟶ (x64 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x4 x67 x52 ⟶ (x40 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x4 x67 x52 ⟶ x66 x67 ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x64 x67 ⟶ (x42 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x4 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x19 x67 ⟶ False) ⟶ x41 x67 ⟶ False) ⟶ (∀ x67 . x4 x67 x65 ⟶ (x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x41 x67 ⟶ (x19 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x25 x67 ⟶ x11 x67 ⟶ (x26 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x19 x67 ⟶ False) ⟶ x19 x67 ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x19 x67 ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x26 x67 ⟶ (x11 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x64 x67 ⟶ (x19 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x64 x67 ⟶ (x64 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ x8 x67 ⟶ (x45 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ x8 x67 ⟶ (x8 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ x8 x67 ⟶ (x27 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ x8 x67 ⟶ (x8 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x26 x67 ⟶ (x6 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x41 x67 ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 x68 . x8 x68 ⟶ x2 x67 (x1 x68) ⟶ (x8 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x6 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x64 x67 ⟶ (x41 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x8 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x6 x67 ⟶ (x25 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x41 x67 ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x42 x67 x52 ⟶ (x41 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ x42 x67 x52 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x10 x67 ⟶ (x64 x67 ⟶ False) ⟶ x41 x67 ⟶ (x42 x67 x52 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x66 x67 ⟶ False) ⟶ x40 x67 ⟶ (x4 x67 x52 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x0 x67 x68 ⟶ x0 x68 x67 ⟶ False) ⟶ (x60 x29 x30 x31 = x61 x29 ⟶ False) ⟶ ((x60 x29 x28 x31 = x61 x29 ⟶ False) ⟶ False) ⟶ ((x60 x29 x30 x28 = x61 x29 ⟶ False) ⟶ False) ⟶ ((x2 x31 (x59 x29) ⟶ False) ⟶ False) ⟶ ((x2 x28 (x59 x29) ⟶ False) ⟶ False) ⟶ ((x2 x30 (x59 x29) ⟶ False) ⟶ False) ⟶ ((x58 x29 ⟶ False) ⟶ False) ⟶ ((x62 x29 ⟶ False) ⟶ False) ⟶ ((x57 x29 ⟶ False) ⟶ False) ⟶ ((x63 x29 ⟶ False) ⟶ False) ⟶ ((x56 x29 ⟶ False) ⟶ False) ⟶ (x64 x29 ⟶ False) ⟶ False (proof)