Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../80f40..
PUYzZ../ed47d..
vout
PrPhD../cc7a3.. 3.41 bars
TMRJC../e4d53.. ownership of 68a30.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMQ63../021a1.. ownership of 8c648.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUftc../c5b56.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 68a30.. : ∀ 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 x78 . x76 x78 ⟶ x76 x77 ⟶ (x75 x78 x77 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x78 ⟶ (x78 = x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ (x75 x78 x77 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x1 x77 x78 ⟶ x0 x78 ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ (x0 x78 ⟶ False) ⟶ (x73 x77 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x77 = x2 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x71 x77 x70 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x1 x77 x78 ⟶ x4 x78 (x3 x79) ⟶ x0 x79 ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ (x0 x77 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ (x73 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x71 x5 x77 = x5 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x66 x77 ⟶ (x75 x78 x5 ⟶ False) ⟶ (x67 x70 (x69 x78 x77) = x69 x78 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x66 x77 ⟶ x66 x78 ⟶ (x75 x79 x5 ⟶ False) ⟶ (x6 (x69 x79 x77) (x69 x79 x78) = x69 x79 (x7 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x1 x78 x79 ⟶ x4 x79 (x3 x77) ⟶ (x4 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ (x73 x77 ⟶ False) ⟶ x73 x78 ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x65 x77 x5 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x8 x78 x77 ⟶ (x4 x78 (x3 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x4 x78 (x3 x77) ⟶ (x8 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ (x74 x78 ⟶ False) ⟶ x74 x77 ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x6 x70 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x4 x77 x78 ⟶ (x0 x78 ⟶ False) ⟶ (x1 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ x74 x77 ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x6 x77 x5 = x5 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x1 x78 x77 ⟶ (x4 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ x75 x78 x77 ⟶ x73 x78 ⟶ (x73 x77 ⟶ False) ⟶ False) ⟶ ((x4 x2 x64 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x7 x77 x5 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x65 (x68 x78) (x68 x77) = x65 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x7 (x68 x78) (x68 x77) = x68 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x72 x79 ⟶ x72 x77 ⟶ x72 x78 ⟶ (x6 (x6 x79 x77) x78 = x6 x79 (x6 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x72 x79 ⟶ x72 x77 ⟶ x72 x78 ⟶ (x7 (x7 x79 x77) x78 = x7 x79 (x7 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x72 x79 ⟶ x72 x77 ⟶ x72 x78 ⟶ (x6 (x7 x79 x77) x78 = x7 (x6 x79 x78) (x6 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x72 x79 ⟶ x72 x77 ⟶ x72 x78 ⟶ (x6 x79 (x71 x77 x78) = x71 (x6 x79 x77) x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x71 x70 x77 = x63 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x6 x77 (x68 x70) = x68 x77 ⟶ False) ⟶ False) ⟶ ((x4 x70 x62 ⟶ False) ⟶ False) ⟶ ((x4 x70 x9 ⟶ False) ⟶ False) ⟶ ((x61 x70 x62 x9 ⟶ False) ⟶ False) ⟶ ((x73 x70 ⟶ False) ⟶ False) ⟶ (x0 x70 ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x7 x78 (x68 x77) = x65 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x6 x78 (x63 x77) = x71 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x71 (x63 x78) (x63 x77) = x71 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x6 (x63 x78) (x63 x77) = x63 (x6 x78 x77) ⟶ False) ⟶ False) ⟶ ((x4 x10 x62 ⟶ False) ⟶ False) ⟶ ((x4 x10 x9 ⟶ False) ⟶ False) ⟶ ((x61 x10 x62 x9 ⟶ False) ⟶ False) ⟶ ((x0 x10 ⟶ False) ⟶ False) ⟶ ((x68 (x68 x70) = x70 ⟶ False) ⟶ False) ⟶ ((x68 x70 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x68 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x6 x70 x70 = x70 ⟶ False) ⟶ False) ⟶ ((x6 x70 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x6 x10 x70 = x10 ⟶ False) ⟶ False) ⟶ ((x6 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 (x68 x70) x70 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x71 x70 (x68 x70) = x68 x70 ⟶ False) ⟶ False) ⟶ ((x71 x70 x70 = x70 ⟶ False) ⟶ False) ⟶ ((x65 (x68 x70) (x68 x70) = x10 ⟶ False) ⟶ False) ⟶ ((x65 (x68 x70) x10 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x65 x70 x70 = x10 ⟶ False) ⟶ False) ⟶ ((x65 x70 x10 = x70 ⟶ False) ⟶ False) ⟶ ((x65 x10 (x68 x70) = x70 ⟶ False) ⟶ False) ⟶ ((x65 x10 x70 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x65 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x68 x70) x70 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x68 x70) x10 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x7 x70 (x68 x70) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x70 x10 = x70 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x68 x70) = x68 x70 ⟶ False) ⟶ False) ⟶ ((x7 x10 x70 = x70 ⟶ False) ⟶ False) ⟶ ((x7 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x75 (x68 x70) (x68 x70) ⟶ False) ⟶ False) ⟶ ((x75 (x68 x70) x70 ⟶ False) ⟶ False) ⟶ ((x75 (x68 x70) x10 ⟶ False) ⟶ False) ⟶ (x75 x70 (x68 x70) ⟶ False) ⟶ ((x75 x70 x70 ⟶ False) ⟶ False) ⟶ (x75 x70 x10 ⟶ False) ⟶ (x75 x10 (x68 x70) ⟶ False) ⟶ ((x75 x10 x70 ⟶ False) ⟶ False) ⟶ ((x75 x10 x10 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x60 x78 ⟶ x60 x77 ⟶ (x75 x78 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x8 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ x4 x77 (x3 x79) ⟶ x4 x78 x77 ⟶ (x61 x78 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ x4 x77 (x3 x79) ⟶ x61 x78 x79 x77 ⟶ (x4 x78 x77 ⟶ False) ⟶ False) ⟶ ((x5 = x2 ⟶ False) ⟶ False) ⟶ ((x9 = x64 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x4 x77 x62 ⟶ (x59 x78 x77 = x6 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x11 x78 x77 = x71 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x4 x78 x62 ⟶ x76 x77 ⟶ (x67 x78 x77 = x71 x78 x77 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ (x0 x13 ⟶ False) ⟶ ((x60 x14 ⟶ False) ⟶ False) ⟶ ((x0 x14 ⟶ False) ⟶ False) ⟶ ((x76 x15 ⟶ False) ⟶ False) ⟶ ((x60 x15 ⟶ False) ⟶ False) ⟶ ((x72 x15 ⟶ False) ⟶ False) ⟶ ((x0 x15 ⟶ False) ⟶ False) ⟶ ((x12 x16 ⟶ False) ⟶ False) ⟶ ((x74 x58 ⟶ False) ⟶ False) ⟶ ((x60 x58 ⟶ False) ⟶ False) ⟶ ((x76 x57 ⟶ False) ⟶ False) ⟶ ((x74 x57 ⟶ False) ⟶ False) ⟶ ((x60 x57 ⟶ False) ⟶ False) ⟶ ((x72 x57 ⟶ False) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ ((x17 x55 ⟶ False) ⟶ False) ⟶ (x0 x55 ⟶ False) ⟶ ((x73 x18 ⟶ False) ⟶ False) ⟶ ((x60 x18 ⟶ False) ⟶ False) ⟶ ((x76 x19 ⟶ False) ⟶ False) ⟶ ((x73 x19 ⟶ False) ⟶ False) ⟶ ((x60 x19 ⟶ False) ⟶ False) ⟶ ((x72 x19 ⟶ False) ⟶ False) ⟶ (x0 x20 ⟶ False) ⟶ ((x66 x54 ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x53 x22 ⟶ False) ⟶ False) ⟶ ((x23 x22 ⟶ False) ⟶ False) ⟶ (x0 x22 ⟶ False) ⟶ ((x21 x24 ⟶ False) ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ ((x4 x24 (x3 x62) ⟶ False) ⟶ False) ⟶ ((x17 x52 ⟶ False) ⟶ False) ⟶ (x0 x52 ⟶ False) ⟶ ((x51 x50 ⟶ False) ⟶ False) ⟶ ((x60 x25 ⟶ False) ⟶ False) ⟶ ((x76 x49 ⟶ False) ⟶ False) ⟶ ((x0 x26 ⟶ False) ⟶ False) ⟶ ((x66 x48 ⟶ False) ⟶ False) ⟶ ((x76 x48 ⟶ False) ⟶ False) ⟶ ((x72 x48 ⟶ False) ⟶ False) ⟶ ((x60 x48 ⟶ False) ⟶ False) ⟶ ((x4 x48 x62 ⟶ False) ⟶ False) ⟶ ((x21 x27 ⟶ False) ⟶ False) ⟶ ((x17 x47 ⟶ False) ⟶ False) ⟶ (x0 x47 ⟶ False) ⟶ ((x51 x46 ⟶ False) ⟶ False) ⟶ ((x76 x46 ⟶ False) ⟶ False) ⟶ ((x72 x46 ⟶ False) ⟶ False) ⟶ ((x60 x46 ⟶ False) ⟶ False) ⟶ ((x4 x46 x62 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x63 (x63 x77) = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x68 (x68 x77) = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x7 x78 x77) ⟶ False) ⟶ (x45 x44 ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ (x76 (x71 x78 x77) ⟶ False) ⟶ False) ⟶ (x45 x62 ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ (x76 (x65 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ (x76 (x6 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x66 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ ((x21 x64 ⟶ False) ⟶ False) ⟶ (x0 x64 ⟶ False) ⟶ ((x17 x64 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x76 x77 ⟶ (x76 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x66 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ ((x56 x64 ⟶ False) ⟶ False) ⟶ ((x56 x62 ⟶ False) ⟶ False) ⟶ ((x56 x44 ⟶ False) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x76 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x66 x78 ⟶ x66 x77 ⟶ (x66 (x71 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x12 x78 ⟶ (x0 x77 ⟶ False) ⟶ x12 x77 ⟶ x0 (x7 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . x51 x78 ⟶ x51 x77 ⟶ (x51 (x65 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x76 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x66 x78 ⟶ x66 x77 ⟶ (x66 (x65 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x66 x77 ⟶ (x76 (x69 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x12 x78 ⟶ (x0 x77 ⟶ False) ⟶ x12 x77 ⟶ x0 (x7 x78 x77) ⟶ False) ⟶ ((x43 x62 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x51 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x71 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x71 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x71 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x71 x78 x77) ⟶ False) ⟶ (∀ x77 . (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x63 x77) ⟶ False) ⟶ (∀ x77 . (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x66 x78 ⟶ x66 x77 ⟶ (x66 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x51 x77 ⟶ (x76 (x42 x78 x77) ⟶ False) ⟶ False) ⟶ (x0 x44 ⟶ False) ⟶ (∀ x77 x78 . x12 x78 ⟶ x12 x77 ⟶ (x12 (x6 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x51 x78 ⟶ x51 x77 ⟶ (x51 (x6 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x74 x77 ⟶ x76 x77 ⟶ (x74 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x74 x77 ⟶ x76 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x63 x77) ⟶ False) ⟶ (∀ x77 . (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x73 x77 ⟶ x76 x77 ⟶ (x73 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x73 x77 ⟶ x76 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x6 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x6 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 ⟶ False) ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x6 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 ⟶ False) ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x6 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . x74 x78 ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x73 (x65 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x74 x78 ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x74 (x65 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x73 x78 ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x74 (x65 x77 x78) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x66 x78 ⟶ x66 x77 ⟶ (x66 (x6 x78 x77) ⟶ False) ⟶ False) ⟶ (x0 x62 ⟶ False) ⟶ (∀ x77 x78 . x12 x78 ⟶ x12 x77 ⟶ (x12 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ ((x28 x44 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x51 x78 ⟶ x51 x77 ⟶ (x51 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x73 x78 ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x73 (x65 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x65 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x65 x78 x77) ⟶ False) ⟶ (∀ x77 . (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x68 x77) ⟶ False) ⟶ (∀ x77 . (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x74 (x68 x77) ⟶ False) ⟶ (∀ x77 . (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x74 x78 ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x74 (x7 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x74 x78 ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ (x74 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x73 x78 ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x73 (x7 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x73 x78 ⟶ x76 x78 ⟶ (x74 x77 ⟶ False) ⟶ x76 x77 ⟶ (x73 (x7 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 ⟶ False) ⟶ x76 x78 ⟶ (x73 x77 ⟶ False) ⟶ x76 x77 ⟶ x73 (x7 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ x4 x77 (x3 x78) ⟶ (x61 (x29 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x4 (x41 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ x4 x77 (x3 x79) ⟶ x61 x78 x79 x77 ⟶ (x4 x78 x79 ⟶ False) ⟶ False) ⟶ ((x61 x5 x62 x9 ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x72 (x63 x77) ⟶ False) ⟶ False) ⟶ ((x4 x9 (x3 x62) ⟶ False) ⟶ False) ⟶ (∀ x77 . x72 x77 ⟶ (x72 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x4 x77 x62 ⟶ (x4 (x59 x78 x77) x62 ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x51 (x30 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x12 x78 ⟶ x76 x77 ⟶ (x76 (x40 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x61 (x31 x77) x62 x9 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x4 (x11 x78 x77) x44 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x4 x78 x62 ⟶ x76 x77 ⟶ (x4 (x67 x78 x77) x62 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x71 x78 x77 = x6 x78 (x63 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x65 x78 x77 = x7 x78 (x68 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x66 x77 ⟶ (x69 x78 x77 = x40 (x31 x77) (x42 x78 (x30 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x60 x78 ⟶ x60 x77 ⟶ (x75 x78 x77 ⟶ False) ⟶ (x75 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x76 x78 ⟶ x4 x77 x62 ⟶ (x59 x78 x77 = x59 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x6 x78 x77 = x6 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x72 x78 ⟶ x72 x77 ⟶ (x7 x78 x77 = x7 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x32 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ (x73 x77 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ (x73 x77 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 x64 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 (x3 x62) ⟶ (x43 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ x60 x77 ⟶ x74 x77 ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ x60 x77 ⟶ x73 x77 ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ x60 x77 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ x60 x77 ⟶ (x73 x77 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ x60 x77 ⟶ (x73 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 (x3 x44) ⟶ (x28 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x74 x77 ⟶ x73 x77 ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x74 x77 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x74 x77 ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 x78 . x21 x78 ⟶ x4 x77 x78 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x43 x77 ⟶ (x28 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ x60 x77 ⟶ (x74 x77 ⟶ False) ⟶ (x73 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ x60 x77 ⟶ (x74 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x39 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x43 x77 ⟶ (x33 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x73 x77 ⟶ x74 x77 ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x73 x77 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x60 x77 ⟶ x73 x77 ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x72 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ x74 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x34 x77 ⟶ (x43 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x66 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x23 x77 ⟶ x53 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 x9 ⟶ x74 x77 ⟶ False) ⟶ (∀ x77 . x38 x77 ⟶ (x34 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x56 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 x9 ⟶ (x17 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x17 x78 ⟶ x4 x77 (x3 x78) ⟶ (x17 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x38 x78 ⟶ x4 x77 (x3 x78) ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x34 x78 ⟶ x4 x77 (x3 x78) ⟶ (x34 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x43 x78 ⟶ x4 x77 (x3 x78) ⟶ (x43 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x33 x78 ⟶ x4 x77 (x3 x78) ⟶ (x33 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 x62 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x66 x77 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x53 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x23 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x17 x77 ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x28 x78 ⟶ x4 x77 (x3 x78) ⟶ (x28 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x17 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x17 x78 ⟶ x4 x77 x78 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x38 x78 ⟶ x4 x77 x78 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x34 x78 ⟶ x4 x77 x78 ⟶ (x66 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x43 x78 ⟶ x4 x77 x78 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x33 x78 ⟶ x4 x77 x78 ⟶ (x60 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x28 x78 ⟶ x4 x77 x78 ⟶ (x72 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x4 x77 (x3 x9) ⟶ (x17 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x32 x78 ⟶ x4 x77 (x3 x78) ⟶ (x32 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x1 x77 x78 ⟶ x1 x78 x77 ⟶ False) ⟶ (x11 (x69 x37 x36) (x69 x37 x35) = x69 x37 (x65 x36 x35) ⟶ False) ⟶ (x75 x37 x5 ⟶ False) ⟶ ((x66 x35 ⟶ False) ⟶ False) ⟶ ((x66 x36 ⟶ False) ⟶ False) ⟶ ((x76 x37 ⟶ False) ⟶ False) ⟶ False (proof)