Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../8f85e..
PUgv1../5560b..
vout
PrNUD../a1f9c.. 0.00 bars
TMZ1g../c5d1f.. ownership of 3de6d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMF4M../3b0d0.. ownership of 7399e.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUfMk../09776.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 3de6d.. : ∀ 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 x79 . x77 x79 ⟶ (x79 = x78 ⟶ False) ⟶ x77 x78 ⟶ False) ⟶ (∀ x78 x79 . x0 x78 x79 ⟶ x77 x79 ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x71 x78 ⟶ x73 x78 (x72 x78) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x71 x78 ⟶ (x3 (x72 x78) (x2 (x1 x78)) ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x71 x78 ⟶ (x69 (x72 x78) x78 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x71 x78 ⟶ x77 (x72 x78) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x70 x79 ⟶ x75 x79 ⟶ x71 x79 ⟶ x74 x79 ⟶ (x77 x78 ⟶ False) ⟶ x69 x78 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x73 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x77 x78 ⟶ (x78 = x4 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x0 x78 x79 ⟶ x3 x79 (x2 x80) ⟶ x77 x80 ⟶ False) ⟶ (∀ x78 x79 x80 . x0 x79 x80 ⟶ x3 x80 (x2 x78) ⟶ (x3 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 x81 . x71 x81 ⟶ x71 x78 ⟶ x67 (x1 x81) (x68 x81) = x67 (x1 x78) (x68 x78) ⟶ x3 x79 (x2 (x1 x81)) ⟶ x3 x80 (x2 (x1 x78)) ⟶ x79 = x80 ⟶ x69 x79 x81 ⟶ (x69 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x5 x79 x78 ⟶ (x3 x79 (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x3 x79 (x2 x78) ⟶ (x5 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x3 x78 x79 ⟶ (x77 x79 ⟶ False) ⟶ (x0 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x71 x80 ⟶ x71 x78 ⟶ x67 (x1 x80) (x68 x80) = x67 (x1 x78) (x68 x78) ⟶ x73 x80 x79 ⟶ (x66 x80 x79 = x66 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 x81 x82 x83 . x71 x83 ⟶ x71 x78 ⟶ x67 (x1 x83) (x68 x83) = x67 (x1 x78) (x68 x78) ⟶ x3 x79 (x1 x83) ⟶ x3 x82 (x1 x83) ⟶ x3 x80 (x1 x78) ⟶ x3 x81 (x1 x78) ⟶ x79 = x80 ⟶ x82 = x81 ⟶ x6 x83 x79 x82 ⟶ (x6 x78 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 x81 x82 x83 . x71 x83 ⟶ x71 x78 ⟶ x67 (x1 x83) (x68 x83) = x67 (x1 x78) (x68 x78) ⟶ x3 x79 (x1 x83) ⟶ x3 x82 (x1 x83) ⟶ x3 x80 (x1 x78) ⟶ x3 x81 (x1 x78) ⟶ x79 = x80 ⟶ x82 = x81 ⟶ x65 x83 x79 x82 ⟶ (x65 x78 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 x78 ⟶ (x3 x79 x78 ⟶ False) ⟶ False) ⟶ (x77 x64 ⟶ False) ⟶ (∀ x78 . (x5 x78 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x63 x78 ⟶ False) ⟶ x63 (x62 x78) ⟶ False) ⟶ (∀ x78 . (x63 x78 ⟶ False) ⟶ (x3 (x62 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ (x63 (x61 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ x77 (x61 x78) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ (x3 (x61 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ (x8 (x7 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ (x3 (x7 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ x77 (x9 x78) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ (x3 (x9 x78) (x2 (x1 x78)) ⟶ False) ⟶ False) ⟶ (∀ x78 . x8 (x11 x78) x78 ⟶ False) ⟶ (∀ x78 . (x3 (x11 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (x77 x12 ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x71 x78 ⟶ (x59 (x60 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x71 x78 ⟶ (x69 (x60 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x71 x78 ⟶ (x58 (x60 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x71 x78 ⟶ x77 (x60 x78) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x71 x78 ⟶ (x3 (x60 x78) (x2 (x1 x78)) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 (x13 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x3 (x13 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x14 x78 ⟶ False) ⟶ x10 x78 ⟶ x63 (x15 x78) ⟶ False) ⟶ (∀ x78 . (x14 x78 ⟶ False) ⟶ x10 x78 ⟶ (x3 (x15 x78) (x2 (x1 x78)) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ (x63 (x16 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ x77 (x16 x78) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ (x3 (x16 x78) (x2 (x1 x78)) ⟶ False) ⟶ False) ⟶ ((x70 x57 ⟶ False) ⟶ False) ⟶ ((x17 x57 ⟶ False) ⟶ False) ⟶ ((x56 x57 x64 ⟶ False) ⟶ False) ⟶ ((x71 x57 ⟶ False) ⟶ False) ⟶ ((x77 x55 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x59 (x18 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x69 (x18 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x3 (x18 x78) (x2 (x1 x78)) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ x77 (x54 x78) ⟶ False) ⟶ (∀ x78 . (x77 x78 ⟶ False) ⟶ (x3 (x54 x78) (x2 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x53 (x52 x78 x79) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x19 (x52 x79 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x51 (x52 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x77 (x52 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x3 (x52 x78 x79) (x2 (x50 x79 x78)) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x71 x80 ⟶ x3 x78 (x1 x80) ⟶ x3 x79 (x1 x80) ⟶ x6 x80 x78 x78 ⟶ False) ⟶ (∀ x78 x79 x80 x81 . x3 x80 (x2 (x50 x81 x81)) ⟶ x67 x81 x80 = x67 x79 x78 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 x81 . x3 x80 (x2 (x50 x81 x81)) ⟶ x67 x81 x80 = x67 x78 x79 ⟶ (x81 = x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x49 x78 ⟶ False) ⟶ x71 x78 ⟶ x77 (x68 x78) ⟶ False) ⟶ (∀ x78 . (x20 x78 ⟶ False) ⟶ x10 x78 ⟶ x58 (x1 x78) ⟶ False) ⟶ (∀ x78 . x20 x78 ⟶ x10 x78 ⟶ (x58 (x1 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . x14 x78 ⟶ x10 x78 ⟶ (x63 (x1 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x14 x78 ⟶ False) ⟶ x10 x78 ⟶ x63 (x1 x78) ⟶ False) ⟶ (∀ x78 . (x76 x78 ⟶ False) ⟶ x10 x78 ⟶ x77 (x1 x78) ⟶ False) ⟶ ((x77 x4 ⟶ False) ⟶ False) ⟶ (∀ x78 . x77 (x2 x78) ⟶ False) ⟶ (∀ x78 . x76 x78 ⟶ x10 x78 ⟶ (x77 (x1 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x77 x79 ⟶ False) ⟶ (x77 x78 ⟶ False) ⟶ x77 (x50 x79 x78) ⟶ False) ⟶ (∀ x78 . (x3 (x48 x78) x78 ⟶ False) ⟶ False) ⟶ ((x10 x21 ⟶ False) ⟶ False) ⟶ ((x71 x47 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x3 (x68 x78) (x2 (x50 (x1 x78) (x1 x78))) ⟶ False) ⟶ False) ⟶ ((x77 x46 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x10 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x71 x79 ⟶ (x3 (x66 x79 x78) (x1 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x3 x79 (x2 (x50 x78 x78)) ⟶ (x71 (x67 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x3 x79 (x2 (x50 x78 x78)) ⟶ (x17 (x67 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x3 x79 (x1 x80) ⟶ x0 x79 (x24 x78 x80) ⟶ x0 (x23 x79 x78 x80) x78 ⟶ (x22 x78 x80 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x3 x79 (x1 x80) ⟶ x0 x79 (x24 x78 x80) ⟶ (x65 x80 x79 (x23 x79 x78 x80) ⟶ False) ⟶ (x22 x78 x80 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x3 x79 (x1 x80) ⟶ x0 x79 (x24 x78 x80) ⟶ (x0 (x23 x79 x78 x80) (x24 x78 x80) ⟶ False) ⟶ (x22 x78 x80 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x3 x79 (x1 x80) ⟶ x0 x79 (x24 x78 x80) ⟶ (x3 (x23 x79 x78 x80) (x1 x80) ⟶ False) ⟶ (x22 x78 x80 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x70 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x0 (x66 x79 (x24 x78 x79)) x78 ⟶ False) ⟶ (x22 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x70 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x3 (x24 x78 x79) (x2 (x1 x79)) ⟶ False) ⟶ (x22 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x70 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x69 (x24 x78 x79) x79 ⟶ False) ⟶ (x22 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x70 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ x77 (x24 x78 x79) ⟶ (x22 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 x81 . (x76 x81 ⟶ False) ⟶ x70 x81 ⟶ x71 x81 ⟶ x3 x78 (x2 (x1 x81)) ⟶ x22 x78 x81 ⟶ (x77 x79 ⟶ False) ⟶ x69 x79 x81 ⟶ x3 x79 (x2 (x1 x81)) ⟶ x0 (x66 x81 x79) x78 ⟶ x3 x80 (x1 x81) ⟶ x0 x80 x79 ⟶ x65 x81 (x25 x79 x78 x81) x80 ⟶ (x0 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x22 x78 x80 ⟶ (x77 x79 ⟶ False) ⟶ x69 x79 x80 ⟶ x3 x79 (x2 (x1 x80)) ⟶ x0 (x66 x80 x79) x78 ⟶ (x0 (x25 x79 x78 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x70 x80 ⟶ x71 x80 ⟶ x3 x78 (x2 (x1 x80)) ⟶ x22 x78 x80 ⟶ (x77 x79 ⟶ False) ⟶ x69 x79 x80 ⟶ x3 x79 (x2 (x1 x80)) ⟶ x0 (x66 x80 x79) x78 ⟶ (x3 (x25 x79 x78 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x4 = x46 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x56 x78 x4 ⟶ (x76 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x76 x78 ⟶ (x56 x78 x4 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x29 x78 ⟶ x26 x78 ⟶ x27 x78 ⟶ (x28 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x29 x78 ⟶ x26 x78 ⟶ x27 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x29 x78 ⟶ x26 x78 ⟶ x27 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x29 x78 ⟶ x26 x78 ⟶ x27 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x29 x78 ⟶ x26 x78 ⟶ x27 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x20 x78 ⟶ False) ⟶ x14 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ (x31 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ (x32 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x26 x78 ⟶ x32 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ (x27 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ (x29 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x28 x78 ⟶ x26 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x14 x78 ⟶ x70 x78 ⟶ (x32 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x14 x78 ⟶ x70 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x14 x78 ⟶ x70 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x14 x78 ⟶ (x20 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x35 x78 ⟶ x34 x78 ⟶ (x33 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x45 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x44 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x35 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ x31 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x74 x78 ⟶ x43 x78 ⟶ (x27 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x74 x78 ⟶ x43 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x74 x78 ⟶ x43 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 x79 . x63 x79 ⟶ x3 x78 (x2 x79) ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x20 x78 ⟶ False) ⟶ x20 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x20 x78 ⟶ False) ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x33 x78 ⟶ (x34 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x33 x78 ⟶ (x35 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x45 x78 ⟶ (x31 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x45 x78 ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x45 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x45 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x27 x78 ⟶ (x43 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x27 x78 ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x27 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x27 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x3 x78 (x2 x79) ⟶ x8 x78 x79 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x76 x78 ⟶ (x20 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x76 x78 ⟶ (x76 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x77 x80 ⟶ x3 x78 (x2 (x50 x79 x80)) ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x49 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x26 x78 ⟶ (x33 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x26 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x31 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x56 x78 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x43 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x56 x78 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x77 x79 ⟶ False) ⟶ x3 x78 (x2 x79) ⟶ x77 x78 ⟶ (x8 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x77 x80 ⟶ x3 x78 (x2 (x50 x80 x79)) ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x49 x78 ⟶ False) ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x26 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x56 x78 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ (x32 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ (x26 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x35 x78 ⟶ x32 x78 ⟶ x74 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x36 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x29 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x56 x78 x64 ⟶ x70 x78 ⟶ (x56 x78 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x77 x79 ⟶ False) ⟶ x3 x78 (x2 x79) ⟶ (x8 x78 x79 ⟶ False) ⟶ x77 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x14 x78 ⟶ False) ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 x79 x80 . x3 x80 (x2 (x50 x78 x79)) ⟶ (x53 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x3 x80 (x2 (x50 x79 x78)) ⟶ (x19 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x37 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x76 x78 ⟶ (x49 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x26 x78 ⟶ (x37 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x26 x78 ⟶ (x44 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x26 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x32 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x59 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x76 x79 ⟶ False) ⟶ x32 x79 ⟶ x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ (x69 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x32 x78 ⟶ (x37 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x32 x78 ⟶ (x44 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x32 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 x79 . x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ x77 x78 ⟶ (x59 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x71 x79 ⟶ x3 x78 (x2 (x1 x79)) ⟶ x77 x78 ⟶ (x69 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x3 x78 (x2 x79) ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x76 x78 ⟶ (x14 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x3 x80 (x2 (x50 x78 x79)) ⟶ (x51 x80 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x44 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x14 x78 ⟶ False) ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x34 x78 ⟶ x42 x78 ⟶ (x34 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x34 x78 ⟶ x42 x78 ⟶ (x44 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x34 x78 ⟶ x42 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x34 x78 ⟶ x42 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x34 x78 ⟶ x42 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x42 x78 ⟶ (x37 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x42 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x42 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x75 x78 ⟶ x42 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x44 x78 ⟶ x35 x78 ⟶ x74 x78 ⟶ (x26 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x44 x78 ⟶ x35 x78 ⟶ x74 x78 ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x44 x78 ⟶ x35 x78 ⟶ x74 x78 ⟶ (x30 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x44 x78 ⟶ x35 x78 ⟶ x74 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x30 x78 ⟶ x75 x78 ⟶ x44 x78 ⟶ x35 x78 ⟶ x74 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x42 x78 ⟶ (x35 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x42 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x42 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x26 x78 ⟶ (x42 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x26 x78 ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x26 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ (x76 x78 ⟶ False) ⟶ x70 x78 ⟶ x26 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x56 x78 x64 ⟶ (x14 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ x56 x78 x64 ⟶ x76 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ (x34 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ (x44 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x70 x78 ⟶ x44 x78 ⟶ x74 x78 ⟶ (x70 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x76 x78 ⟶ False) ⟶ x14 x78 ⟶ (x56 x78 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x78 x79 ⟶ x0 x79 x78 ⟶ False) ⟶ (∀ x78 . x71 x78 ⟶ x17 x78 ⟶ (x78 = x67 (x1 x78) (x68 x78) ⟶ False) ⟶ False) ⟶ (x22 x39 x38 ⟶ False) ⟶ ((x22 x40 x41 ⟶ False) ⟶ False) ⟶ ((x40 = x39 ⟶ False) ⟶ False) ⟶ ((x67 (x1 x41) (x68 x41) = x67 (x1 x38) (x68 x38) ⟶ False) ⟶ False) ⟶ ((x3 x39 (x2 (x1 x38)) ⟶ False) ⟶ False) ⟶ ((x3 x40 (x2 (x1 x41)) ⟶ False) ⟶ False) ⟶ ((x71 x38 ⟶ False) ⟶ False) ⟶ ((x70 x38 ⟶ False) ⟶ False) ⟶ (x76 x38 ⟶ False) ⟶ ((x71 x41 ⟶ False) ⟶ False) ⟶ ((x74 x41 ⟶ False) ⟶ False) ⟶ ((x75 x41 ⟶ False) ⟶ False) ⟶ ((x70 x41 ⟶ False) ⟶ False) ⟶ (x76 x41 ⟶ False) ⟶ False (proof)