Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../970a6..
PUNyY../b5e72..
vout
PrNUD../591b6.. 0.03 bars
TMdx1../7019f.. ownership of 9e379.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMVk1../b2ce2.. ownership of fde12.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUaQ3../7381b.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 9e379.. : ∀ 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 : ι → ο . (∀ x80 x81 . x79 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x74 x82 ⟶ (x77 x81 ⟶ False) ⟶ x75 x81 x82 ⟶ x2 x80 (x76 x81) ⟶ (x2 x80 (x76 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x73 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x73 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (x79 x72 ⟶ False) ⟶ (∀ x80 . (x73 x80 x80 ⟶ False) ⟶ False) ⟶ ((x71 x70 ⟶ False) ⟶ False) ⟶ (x79 x70 ⟶ False) ⟶ (∀ x80 x81 . (x69 (x68 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x3 (x68 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x67 (x68 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x4 (x68 x80 x81) ⟶ False) ⟶ False) ⟶ (x66 x65 ⟶ False) ⟶ ((x69 x65 ⟶ False) ⟶ False) ⟶ ((x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x5 (x6 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x64 (x6 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ x77 (x6 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x75 (x6 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ x79 (x7 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ (x2 (x7 x80) (x1 (x76 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x5 (x9 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x64 (x9 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x75 (x9 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x74 x80 ⟶ (x62 (x63 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x74 x80 ⟶ (x10 (x63 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x74 x80 ⟶ (x60 (x63 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x74 x80 ⟶ x79 (x63 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x74 x80 ⟶ (x2 (x63 x80) (x1 (x76 x80)) ⟶ False) ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x69 x12 ⟶ False) ⟶ False) ⟶ ((x4 x12 ⟶ False) ⟶ False) ⟶ (x79 x59 ⟶ False) ⟶ ((x66 x59 ⟶ False) ⟶ False) ⟶ ((x69 x59 ⟶ False) ⟶ False) ⟶ ((x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x58 x80 ⟶ False) ⟶ x8 x80 ⟶ x57 (x56 x80) ⟶ False) ⟶ (∀ x80 . (x58 x80 ⟶ False) ⟶ x8 x80 ⟶ (x2 (x56 x80) (x1 (x76 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ (x57 (x55 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ x79 (x55 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ (x2 (x55 x80) (x1 (x76 x80)) ⟶ False) ⟶ False) ⟶ ((x61 x13 ⟶ False) ⟶ False) ⟶ ((x64 x13 ⟶ False) ⟶ False) ⟶ ((x14 x13 x72 ⟶ False) ⟶ False) ⟶ ((x74 x13 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x62 (x15 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x10 (x15 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x2 (x15 x80) (x1 (x76 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x3 (x54 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x67 (x54 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x4 (x54 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 (x54 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x2 (x54 x80 x81) (x1 (x53 x81 x80)) ⟶ False) ⟶ False) ⟶ ((x69 x16 ⟶ False) ⟶ False) ⟶ ((x4 x16 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x69 x18 ⟶ False) ⟶ False) ⟶ ((x4 x18 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x82 (x1 (x53 x83 x83)) ⟶ x52 x83 x82 = x52 x81 x80 ⟶ (x82 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x82 (x1 (x53 x83 x83)) ⟶ x52 x83 x82 = x52 x80 x81 ⟶ (x83 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x51 x80 ⟶ False) ⟶ x8 x80 ⟶ x60 (x76 x80) ⟶ False) ⟶ (∀ x80 . x51 x80 ⟶ x8 x80 ⟶ (x60 (x76 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x49 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x64 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x77 (x50 x80) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x8 x80 ⟶ (x57 (x76 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x48 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x19 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x61 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x64 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x77 (x50 x80) ⟶ False) ⟶ (∀ x80 . (x58 x80 ⟶ False) ⟶ x8 x80 ⟶ x57 (x76 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x8 x80 ⟶ x79 (x76 x80) ⟶ False) ⟶ (∀ x80 . x77 x80 ⟶ x8 x80 ⟶ (x79 (x76 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x75 (x47 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x20 x80) x80 ⟶ False) ⟶ False) ⟶ ((x8 x46 ⟶ False) ⟶ False) ⟶ ((x74 x21 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x2 (x45 x80) (x1 (x53 (x76 x80) (x76 x80))) ⟶ False) ⟶ False) ⟶ ((x79 x22 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ x75 x80 x81 ⟶ (x74 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x8 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x75 (x44 x80) (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x5 (x44 x80) (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ (x64 (x44 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x74 x80 ⟶ x77 (x44 x80) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x74 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x64 (x50 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x77 (x50 x80) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 (x53 x80 x80)) ⟶ (x74 (x52 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 (x53 x80 x80)) ⟶ (x64 (x52 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x5 x80 (x50 x81) ⟶ x75 x80 (x50 x81) ⟶ (x5 (x23 x80 x81) x81 ⟶ False) ⟶ (x2 (x23 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x44 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x5 x80 (x50 x81) ⟶ x75 x80 (x50 x81) ⟶ (x43 (x23 x80 x81) x81 ⟶ False) ⟶ (x2 (x23 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x44 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x5 x80 (x50 x81) ⟶ x75 x80 (x50 x81) ⟶ x2 (x23 x80 x81) (x76 x80) ⟶ x43 (x23 x80 x81) x81 ⟶ x5 (x23 x80 x81) x81 ⟶ (x80 = x44 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x5 x80 (x50 x81) ⟶ x75 x80 (x50 x81) ⟶ (x75 (x23 x80 x81) x81 ⟶ False) ⟶ (x80 = x44 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x5 x80 (x50 x81) ⟶ x75 x80 (x50 x81) ⟶ (x64 (x23 x80 x81) ⟶ False) ⟶ (x80 = x44 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x74 x82 ⟶ (x77 x81 ⟶ False) ⟶ x64 x81 ⟶ x5 x81 (x50 x82) ⟶ x75 x81 (x50 x82) ⟶ x81 = x44 x82 ⟶ x64 x80 ⟶ x75 x80 x82 ⟶ x43 x80 x82 ⟶ x5 x80 x82 ⟶ (x2 x80 (x76 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x74 x82 ⟶ (x77 x81 ⟶ False) ⟶ x64 x81 ⟶ x5 x81 (x50 x82) ⟶ x75 x81 (x50 x82) ⟶ x81 = x44 x82 ⟶ x64 x80 ⟶ x75 x80 x82 ⟶ x2 x80 (x76 x81) ⟶ (x5 x80 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x74 x82 ⟶ (x77 x81 ⟶ False) ⟶ x64 x81 ⟶ x5 x81 (x50 x82) ⟶ x75 x81 (x50 x82) ⟶ x81 = x44 x82 ⟶ x64 x80 ⟶ x75 x80 x82 ⟶ x2 x80 (x76 x81) ⟶ (x43 x80 x82 ⟶ False) ⟶ False) ⟶ ((x78 = x22 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x81) x81 ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x75 (x41 x80 x81) (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x81) x81 ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x38 x80 x81 = x40 x80 x81 ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x81) x81 ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x74 (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x82) x82 ⟶ False) ⟶ (x2 (x42 x80 x82) (x76 x80) ⟶ False) ⟶ x39 x80 (x41 x80 x82) (x38 x80 x82) ⟶ x74 x81 ⟶ x38 x80 x82 = x81 ⟶ x75 (x41 x80 x82) x81 ⟶ (x80 = x50 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x81) x81 ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x2 (x38 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x75 (x42 x80 x81) x81 ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x2 (x41 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x81) ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x75 (x41 x80 x81) (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x81) ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x38 x80 x81 = x40 x80 x81 ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x81) ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x74 (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x82) ⟶ False) ⟶ (x2 (x42 x80 x82) (x76 x80) ⟶ False) ⟶ x39 x80 (x41 x80 x82) (x38 x80 x82) ⟶ x74 x81 ⟶ x38 x80 x82 = x81 ⟶ x75 (x41 x80 x82) x81 ⟶ (x80 = x50 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x81) ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x2 (x38 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ (x64 (x42 x80 x81) ⟶ False) ⟶ (x2 (x42 x80 x81) (x76 x80) ⟶ False) ⟶ (x2 (x41 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x81) (x76 x80) ⟶ x64 (x42 x80 x81) ⟶ x75 (x42 x80 x81) x81 ⟶ (x75 (x41 x80 x81) (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x81) (x76 x80) ⟶ x64 (x42 x80 x81) ⟶ x75 (x42 x80 x81) x81 ⟶ (x38 x80 x81 = x40 x80 x81 ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x81) (x76 x80) ⟶ x64 (x42 x80 x81) ⟶ x75 (x42 x80 x81) x81 ⟶ (x74 (x40 x80 x81) ⟶ False) ⟶ (x39 x80 (x41 x80 x81) (x38 x80 x81) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x82) (x76 x80) ⟶ x64 (x42 x80 x82) ⟶ x75 (x42 x80 x82) x82 ⟶ x39 x80 (x41 x80 x82) (x38 x80 x82) ⟶ x74 x81 ⟶ x38 x80 x82 = x81 ⟶ x75 (x41 x80 x82) x81 ⟶ (x80 = x50 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x81) (x76 x80) ⟶ x64 (x42 x80 x81) ⟶ x75 (x42 x80 x81) x81 ⟶ (x2 (x38 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x2 (x42 x80 x81) (x76 x80) ⟶ x64 (x42 x80 x81) ⟶ x75 (x42 x80 x81) x81 ⟶ (x2 (x41 x80 x81) (x76 x80) ⟶ False) ⟶ (x80 = x50 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x74 x84 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x84 ⟶ x2 x81 (x76 x80) ⟶ x2 x83 (x76 x80) ⟶ x74 x82 ⟶ x83 = x82 ⟶ x75 x81 x82 ⟶ (x39 x80 x81 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x74 x83 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x83 ⟶ x2 x81 (x76 x80) ⟶ x2 x82 (x76 x80) ⟶ x39 x80 x81 x82 ⟶ (x75 x81 (x24 x82 x81 x80 x83) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x74 x83 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x83 ⟶ x2 x81 (x76 x80) ⟶ x2 x82 (x76 x80) ⟶ x39 x80 x81 x82 ⟶ (x82 = x24 x82 x81 x80 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x74 x83 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x83 ⟶ x2 x81 (x76 x80) ⟶ x2 x82 (x76 x80) ⟶ x39 x80 x81 x82 ⟶ (x74 (x24 x82 x81 x80 x83) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x82 ⟶ x64 x81 ⟶ x75 x81 x82 ⟶ (x2 x81 (x76 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x82 ⟶ x2 x81 (x76 x80) ⟶ (x75 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x74 x82 ⟶ (x77 x80 ⟶ False) ⟶ x64 x80 ⟶ x74 x80 ⟶ x80 = x50 x82 ⟶ x2 x81 (x76 x80) ⟶ (x64 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x43 x80 x81 ⟶ (x25 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x14 x80 x78 ⟶ (x77 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x2 x80 (x1 x81) ⟶ (x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x48 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x5 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x48 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x77 x80 ⟶ (x14 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x2 x80 x81 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x2 x80 x81 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x5 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x51 x80 ⟶ False) ⟶ x58 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x61 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x5 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x61 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x5 x80 x81 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x58 x80 ⟶ x61 x80 ⟶ (x26 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x58 x80 ⟶ x61 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x58 x80 ⟶ x61 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x58 x80 ⟶ (x51 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x35 x80 ⟶ x36 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x51 x80 ⟶ False) ⟶ x51 x80 ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x51 x80 ⟶ False) ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ (x66 x80 ⟶ False) ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ (x66 x80 ⟶ False) ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ (x66 x80 ⟶ False) ⟶ x57 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x37 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x37 x80 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x77 x80 ⟶ (x51 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x77 x80 ⟶ (x77 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x53 x81 x82)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x49 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x49 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x53 x82 x81)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 ⟶ x69 x81 ⟶ x2 x80 (x1 x81) ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x79 x80 ⟶ (x17 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x79 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x79 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x14 x80 x72 ⟶ x61 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x14 x80 x72 ⟶ x61 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x14 x80 x72 ⟶ x61 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x14 x80 x72 ⟶ x61 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x14 x80 x72 ⟶ x61 x80 ⟶ (x14 x80 x72 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x43 x80 x81 ⟶ (x34 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x61 x81 ⟶ x19 x81 ⟶ x48 x81 ⟶ x28 x81 ⟶ x27 x81 ⟶ x49 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ x43 x80 x81 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x58 x80 ⟶ False) ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x53 x80 x81)) ⟶ (x3 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x53 x81 x80)) ⟶ (x67 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x27 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x4 x80 ⟶ x69 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x17 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x17 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x69 x80 ⟶ x17 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x33 x80 ⟶ x32 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x33 x80 ⟶ x32 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x33 x80 ⟶ x32 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x33 x80 ⟶ x32 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x33 x80 ⟶ x32 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x49 x80 ⟶ (x27 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x49 x80 ⟶ (x28 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x49 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ x2 x80 (x1 (x76 x81)) ⟶ x79 x80 ⟶ (x62 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 ⟶ x2 x80 (x1 (x76 x81)) ⟶ x79 x80 ⟶ (x10 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x77 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x53 x80 x81)) ⟶ (x4 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x28 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x4 x80 ⟶ x3 x80 x81 ⟶ x69 x80 ⟶ (x17 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x4 x80 ⟶ x3 x80 x81 ⟶ x69 x80 ⟶ (x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x4 x80 ⟶ x3 x80 x81 ⟶ x69 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x58 x80 ⟶ False) ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x32 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x32 x80 ⟶ (x28 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x32 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x32 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x36 x80 ⟶ x32 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x32 x80 ⟶ (x27 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x32 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x32 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x48 x80 ⟶ x32 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x28 x80 ⟶ x35 x80 ⟶ x33 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x28 x80 ⟶ x35 x80 ⟶ x33 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x28 x80 ⟶ x35 x80 ⟶ x33 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x28 x80 ⟶ x35 x80 ⟶ x33 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x19 x80 ⟶ x48 x80 ⟶ x28 x80 ⟶ x35 x80 ⟶ x33 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x32 x80 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x32 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x32 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x48 x81 ⟶ x27 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ (x77 x80 ⟶ False) ⟶ x5 x80 x81 ⟶ x25 x80 x81 ⟶ (x25 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x48 x81 ⟶ x27 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ (x77 x80 ⟶ False) ⟶ x5 x80 x81 ⟶ x25 x80 x81 ⟶ (x5 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x48 x81 ⟶ x27 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ (x77 x80 ⟶ False) ⟶ x5 x80 x81 ⟶ x25 x80 x81 ⟶ (x27 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x19 x81 ⟶ x48 x81 ⟶ x27 x81 ⟶ x74 x81 ⟶ x75 x80 x81 ⟶ (x77 x80 ⟶ False) ⟶ x5 x80 x81 ⟶ x25 x80 x81 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x49 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x49 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x49 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ (x77 x80 ⟶ False) ⟶ x61 x80 ⟶ x49 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x14 x80 x72 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ x14 x80 x72 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x61 x80 ⟶ x28 x80 ⟶ x33 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x61 x80 ⟶ x28 x80 ⟶ x33 x80 ⟶ (x28 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x61 x80 ⟶ x28 x80 ⟶ x33 x80 ⟶ (x61 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x77 x80 ⟶ False) ⟶ x58 x80 ⟶ (x14 x80 x72 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x64 x80 ⟶ (x80 = x52 (x76 x80) (x45 x80) ⟶ False) ⟶ False) ⟶ ((x75 x30 x31 ⟶ False) ⟶ (x2 x30 (x76 (x44 x31)) ⟶ False) ⟶ False) ⟶ ((x43 x30 x31 ⟶ False) ⟶ (x2 x30 (x76 (x44 x31)) ⟶ False) ⟶ False) ⟶ ((x5 x30 x31 ⟶ False) ⟶ (x2 x30 (x76 (x44 x31)) ⟶ False) ⟶ False) ⟶ ((x64 x30 ⟶ False) ⟶ (x2 x30 (x76 (x44 x31)) ⟶ False) ⟶ False) ⟶ (x2 x30 (x76 (x44 x31)) ⟶ x64 x30 ⟶ x5 x30 x31 ⟶ x43 x30 x31 ⟶ x75 x30 x31 ⟶ False) ⟶ ((x74 x31 ⟶ False) ⟶ False) ⟶ (x77 x31 ⟶ False) ⟶ False (proof)