Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../51c3d..
PUUt3../ce7bf..
vout
PrNUD../9ad3d.. 0.04 bars
TMQ2V../378a5.. ownership of 741e5.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMGSL../9690d.. ownership of 9dabc.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUVqS../49a2d.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 741e5.. : ∀ 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 . ∀ x69 : ι → ι . ∀ x70 : ι → ι → ο . ∀ x71 : ι → ι . ∀ x72 x73 : ι → ο . ∀ x74 : ι → ι → ο . ∀ x75 : ι → ο . (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ (x74 x77 x76 ⟶ False) ⟶ (x73 x76 ⟶ False) ⟶ (x72 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x0 x77 ⟶ (x77 = x76 ⟶ False) ⟶ x0 x76 ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ (x74 x77 x76 ⟶ False) ⟶ (x72 x77 ⟶ False) ⟶ (x73 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x1 x76 x77 ⟶ x0 x77 ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ (x0 x77 ⟶ False) ⟶ (x72 x76 ⟶ False) ⟶ (x73 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x76 = x2 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x1 x76 x77 ⟶ x70 x77 (x71 x78) ⟶ x0 x78 ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ (x0 x76 ⟶ False) ⟶ (x73 x77 ⟶ False) ⟶ (x72 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x74 (x69 x76) x68 ⟶ False) ⟶ x74 x68 x76 ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x74 x68 x76 ⟶ False) ⟶ x74 (x69 x76) x68 ⟶ False) ⟶ (∀ x76 x77 x78 . x1 x77 x78 ⟶ x70 x78 (x71 x76) ⟶ (x70 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ (x72 x76 ⟶ False) ⟶ x72 x77 ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x66 x76 x68 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x3 x77 x76 ⟶ (x70 x77 (x71 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 (x71 x76) ⟶ (x3 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ (x73 x77 ⟶ False) ⟶ x73 x76 ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ x74 x68 x76 ⟶ (x1 x76 x64 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x76 x77 ⟶ (x0 x77 ⟶ False) ⟶ (x1 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ x73 x76 ⟶ (x73 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x1 x77 x76 ⟶ (x70 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ x74 x77 x76 ⟶ x72 x77 ⟶ (x72 x76 ⟶ False) ⟶ False) ⟶ ((x70 x2 x4 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x63 x76 x68 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x5 x76 ⟶ x74 x77 x76 ⟶ x74 (x7 x76 x6) x77 ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x5 x76 ⟶ (x74 (x7 x76 x6) x77 ⟶ False) ⟶ (x74 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ x74 x6 x76 ⟶ (x8 x68 x76 = x68 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x67 x76 ⟶ (x66 (x69 x77) (x69 x76) = x66 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x67 x76 ⟶ (x63 (x69 x77) (x69 x76) = x69 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x67 x78 ⟶ x67 x76 ⟶ x67 x77 ⟶ (x63 (x63 x78 x76) x77 = x63 x78 (x63 x76 x77) ⟶ False) ⟶ False) ⟶ ((x70 x10 x9 ⟶ False) ⟶ False) ⟶ ((x70 x10 x64 ⟶ False) ⟶ False) ⟶ ((x11 x10 x9 x64 ⟶ False) ⟶ False) ⟶ ((x72 x10 ⟶ False) ⟶ False) ⟶ (x0 x10 ⟶ False) ⟶ ((x70 x6 x9 ⟶ False) ⟶ False) ⟶ ((x70 x6 x64 ⟶ False) ⟶ False) ⟶ ((x11 x6 x9 x64 ⟶ False) ⟶ False) ⟶ ((x72 x6 ⟶ False) ⟶ False) ⟶ (x0 x6 ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x67 x76 ⟶ (x63 x77 (x69 x76) = x66 x77 x76 ⟶ False) ⟶ False) ⟶ ((x70 x62 x9 ⟶ False) ⟶ False) ⟶ ((x70 x62 x64 ⟶ False) ⟶ False) ⟶ ((x11 x62 x9 x64 ⟶ False) ⟶ False) ⟶ ((x0 x62 ⟶ False) ⟶ False) ⟶ ((x69 (x69 x10) = x10 ⟶ False) ⟶ False) ⟶ ((x69 (x69 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x69 x10 = x69 x10 ⟶ False) ⟶ False) ⟶ ((x69 x6 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x69 x62 = x62 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x10) (x69 x10) = x62 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x10) (x69 x6) = x69 x6 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x10) x62 = x69 x10 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x6) (x69 x10) = x6 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x6) (x69 x6) = x62 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x6) x6 = x69 x10 ⟶ False) ⟶ False) ⟶ ((x66 (x69 x6) x62 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x66 x10 x10 = x62 ⟶ False) ⟶ False) ⟶ ((x66 x10 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x66 x10 x62 = x10 ⟶ False) ⟶ False) ⟶ ((x66 x6 (x69 x6) = x10 ⟶ False) ⟶ False) ⟶ ((x66 x6 x10 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x66 x6 x6 = x62 ⟶ False) ⟶ False) ⟶ ((x66 x6 x62 = x6 ⟶ False) ⟶ False) ⟶ ((x66 x62 (x69 x10) = x10 ⟶ False) ⟶ False) ⟶ ((x66 x62 (x69 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x66 x62 x10 = x69 x10 ⟶ False) ⟶ False) ⟶ ((x66 x62 x6 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x66 x62 x62 = x62 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x10) x10 = x62 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x10) x6 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x6) (x69 x6) = x69 x10 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x6) x10 = x6 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x6) x6 = x62 ⟶ False) ⟶ False) ⟶ ((x63 (x69 x6) x62 = x69 x6 ⟶ False) ⟶ False) ⟶ ((x63 x10 (x69 x10) = x62 ⟶ False) ⟶ False) ⟶ ((x63 x10 (x69 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x63 x10 x62 = x10 ⟶ False) ⟶ False) ⟶ ((x63 x6 (x69 x10) = x69 x6 ⟶ False) ⟶ False) ⟶ ((x63 x6 (x69 x6) = x62 ⟶ False) ⟶ False) ⟶ ((x63 x6 x6 = x10 ⟶ False) ⟶ False) ⟶ ((x63 x6 x62 = x6 ⟶ False) ⟶ False) ⟶ ((x63 x62 (x69 x10) = x69 x10 ⟶ False) ⟶ False) ⟶ ((x63 x62 (x69 x6) = x69 x6 ⟶ False) ⟶ False) ⟶ ((x63 x62 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x63 x62 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x63 x62 x62 = x62 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x10) (x69 x10) ⟶ False) ⟶ False) ⟶ ((x74 (x69 x10) (x69 x6) ⟶ False) ⟶ False) ⟶ ((x74 (x69 x10) x10 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x10) x6 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x10) x62 ⟶ False) ⟶ False) ⟶ (x74 (x69 x6) (x69 x10) ⟶ False) ⟶ ((x74 (x69 x6) (x69 x6) ⟶ False) ⟶ False) ⟶ ((x74 (x69 x6) x10 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x6) x6 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x6) x62 ⟶ False) ⟶ False) ⟶ (x74 x10 (x69 x10) ⟶ False) ⟶ (x74 x10 (x69 x6) ⟶ False) ⟶ ((x74 x10 x10 ⟶ False) ⟶ False) ⟶ (x74 x10 x6 ⟶ False) ⟶ (x74 x10 x62 ⟶ False) ⟶ (x74 x6 (x69 x10) ⟶ False) ⟶ (x74 x6 (x69 x6) ⟶ False) ⟶ ((x74 x6 x10 ⟶ False) ⟶ False) ⟶ ((x74 x6 x6 ⟶ False) ⟶ False) ⟶ (x74 x6 x62 ⟶ False) ⟶ (x74 x62 (x69 x10) ⟶ False) ⟶ (x74 x62 (x69 x6) ⟶ False) ⟶ ((x74 x62 x10 ⟶ False) ⟶ False) ⟶ ((x74 x62 x6 ⟶ False) ⟶ False) ⟶ ((x74 x62 x62 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x12 x77 ⟶ x12 x76 ⟶ (x74 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x3 x76 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x0 x78 ⟶ False) ⟶ (x0 x76 ⟶ False) ⟶ x70 x76 (x71 x78) ⟶ x70 x77 x76 ⟶ (x11 x77 x78 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x0 x78 ⟶ False) ⟶ (x0 x76 ⟶ False) ⟶ x70 x76 (x71 x78) ⟶ x11 x77 x78 x76 ⟶ (x70 x77 x76 ⟶ False) ⟶ False) ⟶ ((x68 = x2 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x9 ⟶ x65 x76 ⟶ (x61 x77 x76 = x60 x77 x76 ⟶ False) ⟶ False) ⟶ ((x64 = x4 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x59 x76 = x58 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x9 ⟶ x5 x76 ⟶ (x8 x77 x76 = x13 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x64 ⟶ x5 x76 ⟶ (x57 x77 x76 = x63 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x14 x76 = x69 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x70 x76 x64 ⟶ (x7 x77 x76 = x63 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x16 x76 = x15 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x64 ⟶ x70 x76 x64 ⟶ (x56 x77 x76 = x13 x77 x76 ⟶ False) ⟶ False) ⟶ ((x5 x17 ⟶ False) ⟶ False) ⟶ (x0 x17 ⟶ False) ⟶ ((x12 x18 ⟶ False) ⟶ False) ⟶ ((x0 x18 ⟶ False) ⟶ False) ⟶ ((x75 x19 ⟶ False) ⟶ False) ⟶ ((x12 x19 ⟶ False) ⟶ False) ⟶ ((x67 x19 ⟶ False) ⟶ False) ⟶ ((x0 x19 ⟶ False) ⟶ False) ⟶ ((x5 x20 ⟶ False) ⟶ False) ⟶ ((x73 x55 ⟶ False) ⟶ False) ⟶ ((x12 x55 ⟶ False) ⟶ False) ⟶ ((x75 x54 ⟶ False) ⟶ False) ⟶ ((x73 x54 ⟶ False) ⟶ False) ⟶ ((x12 x54 ⟶ False) ⟶ False) ⟶ ((x67 x54 ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ ((x21 x52 ⟶ False) ⟶ False) ⟶ (x0 x52 ⟶ False) ⟶ ((x72 x22 ⟶ False) ⟶ False) ⟶ ((x12 x22 ⟶ False) ⟶ False) ⟶ ((x75 x23 ⟶ False) ⟶ False) ⟶ ((x72 x23 ⟶ False) ⟶ False) ⟶ ((x12 x23 ⟶ False) ⟶ False) ⟶ ((x67 x23 ⟶ False) ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ ((x51 x50 ⟶ False) ⟶ False) ⟶ ((x25 x26 ⟶ False) ⟶ False) ⟶ ((x49 x26 ⟶ False) ⟶ False) ⟶ ((x27 x26 ⟶ False) ⟶ False) ⟶ (x0 x26 ⟶ False) ⟶ ((x25 x28 ⟶ False) ⟶ False) ⟶ (x0 x28 ⟶ False) ⟶ ((x70 x28 (x71 x9) ⟶ False) ⟶ False) ⟶ ((x21 x48 ⟶ False) ⟶ False) ⟶ (x0 x48 ⟶ False) ⟶ ((x65 x47 ⟶ False) ⟶ False) ⟶ ((x12 x29 ⟶ False) ⟶ False) ⟶ ((x75 x46 ⟶ False) ⟶ False) ⟶ ((x0 x30 ⟶ False) ⟶ False) ⟶ ((x51 x45 ⟶ False) ⟶ False) ⟶ ((x75 x45 ⟶ False) ⟶ False) ⟶ ((x67 x45 ⟶ False) ⟶ False) ⟶ ((x12 x45 ⟶ False) ⟶ False) ⟶ ((x70 x45 x9 ⟶ False) ⟶ False) ⟶ ((x25 x31 ⟶ False) ⟶ False) ⟶ ((x21 x44 ⟶ False) ⟶ False) ⟶ (x0 x44 ⟶ False) ⟶ ((x65 x43 ⟶ False) ⟶ False) ⟶ ((x75 x43 ⟶ False) ⟶ False) ⟶ ((x67 x43 ⟶ False) ⟶ False) ⟶ ((x12 x43 ⟶ False) ⟶ False) ⟶ ((x70 x43 x9 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x16 (x16 x76) = x16 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x15 (x15 x76) = x15 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x58 (x58 x76) = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x69 (x69 x76) = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x59 (x59 x76) = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x14 (x14 x76) = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x73 x77 ⟶ False) ⟶ x75 x77 ⟶ (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ x73 (x63 x77 x76) ⟶ False) ⟶ (x42 x9 ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ (x75 (x66 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x51 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ ((x25 x4 ⟶ False) ⟶ False) ⟶ (x0 x4 ⟶ False) ⟶ ((x21 x4 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x75 x76 ⟶ (x75 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x51 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ ((x53 x4 ⟶ False) ⟶ False) ⟶ ((x53 x9 ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x75 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x5 x76 ⟶ (x5 (x13 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ (x0 x76 ⟶ False) ⟶ x5 x76 ⟶ x0 (x63 x76 x77) ⟶ False) ⟶ (∀ x76 x77 . x65 x77 ⟶ x65 x76 ⟶ (x65 (x66 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x75 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x51 x77 ⟶ x51 x76 ⟶ (x51 (x66 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x5 x76 ⟶ (x67 (x13 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ (x0 x76 ⟶ False) ⟶ x5 x76 ⟶ x0 (x63 x77 x76) ⟶ False) ⟶ ((x41 x9 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x65 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ x73 (x58 x76) ⟶ False) ⟶ (∀ x76 . (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x51 x77 ⟶ x51 x76 ⟶ (x51 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x65 x76 ⟶ (x75 (x60 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x5 x76 ⟶ (x75 (x13 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x73 x76 ⟶ x75 x76 ⟶ (x73 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x73 x76 ⟶ x75 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ x72 (x58 x76) ⟶ False) ⟶ (∀ x76 . (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x72 x76 ⟶ x75 x76 ⟶ (x72 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x72 x76 ⟶ x75 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x73 x77 ⟶ x75 x77 ⟶ (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x72 (x66 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x73 x77 ⟶ x75 x77 ⟶ (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x73 (x66 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x72 x77 ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x73 (x66 x76 x77) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x51 (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x75 (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x75 (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x5 (x15 x76) ⟶ False) ⟶ False) ⟶ (x0 x9 ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x5 x76 ⟶ (x5 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x65 x77 ⟶ x65 x76 ⟶ (x65 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x72 x77 ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x72 (x66 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x73 x77 ⟶ False) ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ x72 (x66 x76 x77) ⟶ False) ⟶ (∀ x76 x77 . (x73 x77 ⟶ False) ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ x73 (x66 x77 x76) ⟶ False) ⟶ (∀ x76 . (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ x72 (x69 x76) ⟶ False) ⟶ (∀ x76 . (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ x73 (x69 x76) ⟶ False) ⟶ (∀ x76 . (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x73 x77 ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x73 (x63 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x73 x77 ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ (x73 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x72 x77 ⟶ x75 x77 ⟶ (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x72 (x63 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x72 x77 ⟶ x75 x77 ⟶ (x73 x76 ⟶ False) ⟶ x75 x76 ⟶ (x72 (x63 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x72 x77 ⟶ False) ⟶ x75 x77 ⟶ (x72 x76 ⟶ False) ⟶ x75 x76 ⟶ x72 (x63 x77 x76) ⟶ False) ⟶ (∀ x76 x77 . (x0 x77 ⟶ False) ⟶ (x0 x76 ⟶ False) ⟶ x70 x76 (x71 x77) ⟶ (x11 (x32 x76 x77) x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x70 (x40 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x0 x78 ⟶ False) ⟶ (x0 x76 ⟶ False) ⟶ x70 x76 (x71 x78) ⟶ x11 x77 x78 x76 ⟶ (x70 x77 x78 ⟶ False) ⟶ False) ⟶ ((x11 x68 x9 x64 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x67 (x58 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x9 ⟶ x65 x76 ⟶ (x70 (x61 x77 x76) x9 ⟶ False) ⟶ False) ⟶ ((x70 x64 (x71 x9) ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x67 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x70 (x59 x76) x9 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x9 ⟶ x5 x76 ⟶ (x70 (x8 x77 x76) x9 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x64 ⟶ x5 x76 ⟶ (x11 (x57 x77 x76) x9 x64 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x70 (x14 x76) x9 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x70 x76 x64 ⟶ (x11 (x7 x77 x76) x9 x64 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x70 (x16 x76) x64 ⟶ False) ⟶ False) ⟶ (∀ x76 . x67 x76 ⟶ (x75 (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x64 ⟶ x70 x76 x64 ⟶ (x11 (x56 x77 x76) x9 x64 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x67 x76 ⟶ (x66 x77 x76 = x63 x77 (x69 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x65 x76 ⟶ (x74 x68 x76 ⟶ False) ⟶ (x60 x77 x76 = x58 (x13 x77 (x16 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x65 x76 ⟶ x74 x68 x76 ⟶ (x60 x77 x76 = x13 x77 (x16 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x74 x68 x76 ⟶ False) ⟶ (x15 x76 = x69 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ x74 x68 x76 ⟶ (x15 x76 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x12 x77 ⟶ x12 x76 ⟶ (x74 x77 x76 ⟶ False) ⟶ (x74 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x67 x77 ⟶ x67 x76 ⟶ (x63 x77 x76 = x63 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x70 x77 x64 ⟶ x5 x76 ⟶ (x57 x77 x76 = x57 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x5 x77 ⟶ x70 x76 x64 ⟶ (x7 x77 x76 = x7 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x39 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ (x72 x76 ⟶ False) ⟶ (x73 x76 ⟶ False) ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ (x72 x76 ⟶ False) ⟶ (x73 x76 ⟶ False) ⟶ (x0 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x4 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 (x71 x9) ⟶ (x41 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ x12 x76 ⟶ x73 x76 ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ x12 x76 ⟶ x72 x76 ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ x12 x76 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x0 x76 ⟶ False) ⟶ x12 x76 ⟶ (x72 x76 ⟶ False) ⟶ (x73 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x0 x76 ⟶ False) ⟶ x12 x76 ⟶ (x72 x76 ⟶ False) ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x25 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x73 x76 ⟶ x72 x76 ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x73 x76 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x73 x76 ⟶ x0 x76 ⟶ False) ⟶ (∀ x76 x77 . x25 x77 ⟶ x70 x76 x77 ⟶ (x25 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x41 x76 ⟶ (x38 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x0 x76 ⟶ False) ⟶ x12 x76 ⟶ (x73 x76 ⟶ False) ⟶ (x72 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x0 x76 ⟶ False) ⟶ x12 x76 ⟶ (x73 x76 ⟶ False) ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x37 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x41 x76 ⟶ (x33 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x72 x76 ⟶ x73 x76 ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x72 x76 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x12 x76 ⟶ x72 x76 ⟶ x0 x76 ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x67 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x25 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ x73 x76 ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x34 x76 ⟶ (x41 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x65 x76 ⟶ (x51 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x27 x76 ⟶ x49 x76 ⟶ (x25 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x64 ⟶ x73 x76 ⟶ False) ⟶ (∀ x76 . x36 x76 ⟶ (x34 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x65 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x53 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x64 ⟶ (x21 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x21 x77 ⟶ x70 x76 (x71 x77) ⟶ (x21 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x36 x77 ⟶ x70 x76 (x71 x77) ⟶ (x36 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x34 x77 ⟶ x70 x76 (x71 x77) ⟶ (x34 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x41 x77 ⟶ x70 x76 (x71 x77) ⟶ (x41 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x33 x77 ⟶ x70 x76 (x71 x77) ⟶ (x33 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 x9 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x51 x76 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x25 x76 ⟶ (x49 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x25 x76 ⟶ (x27 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x5 x76 ⟶ (x25 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x21 x76 ⟶ (x36 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x38 x77 ⟶ x70 x76 (x71 x77) ⟶ (x38 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x0 x76 ⟶ (x21 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x21 x77 ⟶ x70 x76 x77 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x36 x77 ⟶ x70 x76 x77 ⟶ (x65 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x34 x77 ⟶ x70 x76 x77 ⟶ (x51 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x41 x77 ⟶ x70 x76 x77 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x33 x77 ⟶ x70 x76 x77 ⟶ (x12 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x38 x77 ⟶ x70 x76 x77 ⟶ (x67 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x70 x76 (x71 x64) ⟶ (x21 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x39 x77 ⟶ x70 x76 (x71 x77) ⟶ (x39 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x1 x76 x77 ⟶ x1 x77 x76 ⟶ False) ⟶ (x61 x68 x35 = x68 ⟶ False) ⟶ (x35 = x68 ⟶ False) ⟶ ((x65 x35 ⟶ False) ⟶ False) ⟶ False (proof)