Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../38cee..
PUhGT../52aa9..
vout
PrNUD../16bee.. 0.04 bars
TMM3b../4eb7a.. ownership of 7853d.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMPZL../41390.. ownership of b8b5d.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUWUm../8a806.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7853d.. : ∀ 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 x82 x83 . x0 x83 ⟶ x0 x80 ⟶ x0 x82 ⟶ x0 x81 ⟶ (x2 (x2 x83 x80) (x2 x82 x81) = x2 (x1 x83 x81) (x1 x80 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x78 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x0 x83 ⟶ x0 x80 ⟶ x0 x82 ⟶ x0 x81 ⟶ (x1 (x2 x83 x80) (x2 x82 x81) = x2 (x1 x83 x82) (x1 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x77 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x2 x80 x3 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x78 x80 x81 ⟶ x75 x81 (x76 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . x78 x81 x82 ⟶ x75 x82 (x76 x80) ⟶ (x75 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x74 x81 x80 ⟶ (x75 x81 (x76 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 (x76 x80) ⟶ (x74 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x1 x3 x80 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x78 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x78 x81 x80 ⟶ (x75 x81 x80 ⟶ False) ⟶ False) ⟶ ((x75 x77 x4 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x72 (x73 x81) (x73 x80) = x72 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x5 (x73 x81) (x73 x80) = x73 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x0 x80 ⟶ x0 x81 ⟶ (x1 (x1 x82 x80) x81 = x1 x82 (x1 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x0 x80 ⟶ x0 x81 ⟶ (x5 (x5 x82 x80) x81 = x5 x82 (x5 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x0 x80 ⟶ x0 x81 ⟶ (x1 (x5 x82 x80) x81 = x5 (x1 x82 x81) (x1 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x0 x80 ⟶ x0 x81 ⟶ (x1 x82 (x2 x80 x81) = x2 (x1 x82 x80) x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x2 x3 x80 = x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x1 x80 (x73 x3) = x73 x80 ⟶ False) ⟶ False) ⟶ ((x75 x3 x70 ⟶ False) ⟶ False) ⟶ ((x75 x3 x6 ⟶ False) ⟶ False) ⟶ ((x69 x3 x70 x6 ⟶ False) ⟶ False) ⟶ ((x7 x3 ⟶ False) ⟶ False) ⟶ (x79 x3 ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x5 x81 (x73 x80) = x72 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x1 x81 (x71 x80) = x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x2 (x71 x81) (x71 x80) = x2 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x1 (x71 x81) (x71 x80) = x71 (x1 x81 x80) ⟶ False) ⟶ False) ⟶ ((x75 x8 x70 ⟶ False) ⟶ False) ⟶ ((x75 x8 x6 ⟶ False) ⟶ False) ⟶ ((x69 x8 x70 x6 ⟶ False) ⟶ False) ⟶ ((x79 x8 ⟶ False) ⟶ False) ⟶ ((x73 (x73 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x73 x3 = x73 x3 ⟶ False) ⟶ False) ⟶ ((x73 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x1 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x1 x3 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x1 x8 x3 = x8 ⟶ False) ⟶ False) ⟶ ((x1 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x2 (x73 x3) x3 = x73 x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x73 x3) = x73 x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x72 (x73 x3) (x73 x3) = x8 ⟶ False) ⟶ False) ⟶ ((x72 (x73 x3) x8 = x73 x3 ⟶ False) ⟶ False) ⟶ ((x72 x3 x3 = x8 ⟶ False) ⟶ False) ⟶ ((x72 x3 x8 = x3 ⟶ False) ⟶ False) ⟶ ((x72 x8 (x73 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x72 x8 x3 = x73 x3 ⟶ False) ⟶ False) ⟶ ((x72 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x5 (x73 x3) x3 = x8 ⟶ False) ⟶ False) ⟶ ((x5 (x73 x3) x8 = x73 x3 ⟶ False) ⟶ False) ⟶ ((x5 x3 (x73 x3) = x8 ⟶ False) ⟶ False) ⟶ ((x5 x3 x8 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x8 (x73 x3) = x73 x3 ⟶ False) ⟶ False) ⟶ ((x5 x8 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x74 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x75 x80 (x76 x82) ⟶ x75 x81 x80 ⟶ (x69 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x75 x80 (x76 x82) ⟶ x69 x81 x82 x80 ⟶ (x75 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 x70 ⟶ x67 x80 ⟶ (x68 x81 x80 = x1 x81 x80 ⟶ False) ⟶ False) ⟶ ((x6 = x4 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 x70 ⟶ x67 x80 ⟶ (x66 x81 x80 = x2 x81 x80 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x79 x10 ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ (x79 x12 ⟶ False) ⟶ (x7 x13 ⟶ False) ⟶ ((x65 x13 ⟶ False) ⟶ False) ⟶ ((x67 x13 ⟶ False) ⟶ False) ⟶ ((x0 x13 ⟶ False) ⟶ False) ⟶ ((x75 x13 x70 ⟶ False) ⟶ False) ⟶ ((x65 x64 ⟶ False) ⟶ False) ⟶ ((x79 x64 ⟶ False) ⟶ False) ⟶ ((x67 x63 ⟶ False) ⟶ False) ⟶ ((x65 x63 ⟶ False) ⟶ False) ⟶ ((x0 x63 ⟶ False) ⟶ False) ⟶ ((x79 x63 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x61 (x62 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x75 (x62 x80) (x76 x80) ⟶ False) ⟶ False) ⟶ ((x11 x60 ⟶ False) ⟶ False) ⟶ (x14 x15 ⟶ False) ⟶ ((x65 x15 ⟶ False) ⟶ False) ⟶ ((x67 x15 ⟶ False) ⟶ False) ⟶ ((x0 x15 ⟶ False) ⟶ False) ⟶ ((x75 x15 x70 ⟶ False) ⟶ False) ⟶ ((x14 x59 ⟶ False) ⟶ False) ⟶ ((x65 x59 ⟶ False) ⟶ False) ⟶ ((x67 x58 ⟶ False) ⟶ False) ⟶ ((x14 x58 ⟶ False) ⟶ False) ⟶ ((x65 x58 ⟶ False) ⟶ False) ⟶ ((x0 x58 ⟶ False) ⟶ False) ⟶ (∀ x80 . x61 (x57 x80) x80 ⟶ False) ⟶ (∀ x80 . (x75 (x57 x80) (x76 x80) ⟶ False) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ ((x16 x55 ⟶ False) ⟶ False) ⟶ (x79 x55 ⟶ False) ⟶ ((x7 x17 ⟶ False) ⟶ False) ⟶ ((x65 x17 ⟶ False) ⟶ False) ⟶ ((x67 x18 ⟶ False) ⟶ False) ⟶ ((x7 x18 ⟶ False) ⟶ False) ⟶ ((x65 x18 ⟶ False) ⟶ False) ⟶ ((x0 x18 ⟶ False) ⟶ False) ⟶ (x79 x19 ⟶ False) ⟶ (∀ x80 . (x79 (x54 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x75 (x54 x80) (x76 x80) ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ ((x20 x52 ⟶ False) ⟶ False) ⟶ ((x51 x52 ⟶ False) ⟶ False) ⟶ (x79 x52 ⟶ False) ⟶ ((x53 x50 ⟶ False) ⟶ False) ⟶ (x79 x50 ⟶ False) ⟶ ((x75 x50 (x76 x70) ⟶ False) ⟶ False) ⟶ ((x16 x21 ⟶ False) ⟶ False) ⟶ (x79 x21 ⟶ False) ⟶ ((x22 x23 ⟶ False) ⟶ False) ⟶ ((x14 x49 ⟶ False) ⟶ False) ⟶ ((x65 x49 ⟶ False) ⟶ False) ⟶ ((x67 x49 ⟶ False) ⟶ False) ⟶ ((x0 x49 ⟶ False) ⟶ False) ⟶ ((x75 x49 x70 ⟶ False) ⟶ False) ⟶ ((x65 x24 ⟶ False) ⟶ False) ⟶ ((x67 x48 ⟶ False) ⟶ False) ⟶ ((x79 x25 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x47 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x75 (x47 x80) (x76 x80) ⟶ False) ⟶ False) ⟶ ((x53 x46 ⟶ False) ⟶ False) ⟶ ((x16 x26 ⟶ False) ⟶ False) ⟶ (x79 x26 ⟶ False) ⟶ ((x22 x27 ⟶ False) ⟶ False) ⟶ ((x67 x27 ⟶ False) ⟶ False) ⟶ ((x0 x27 ⟶ False) ⟶ False) ⟶ ((x65 x27 ⟶ False) ⟶ False) ⟶ ((x75 x27 x70 ⟶ False) ⟶ False) ⟶ ((x7 x45 ⟶ False) ⟶ False) ⟶ ((x65 x45 ⟶ False) ⟶ False) ⟶ ((x67 x45 ⟶ False) ⟶ False) ⟶ ((x0 x45 ⟶ False) ⟶ False) ⟶ ((x75 x45 x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x71 (x71 x80) = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x73 (x73 x80) = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x5 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . x67 x81 ⟶ x67 x80 ⟶ (x67 (x2 x81 x80) ⟶ False) ⟶ False) ⟶ (x28 x70 ⟶ False) ⟶ (∀ x80 x81 . x67 x81 ⟶ x67 x80 ⟶ (x67 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x67 x81 ⟶ x67 x80 ⟶ (x67 (x1 x81 x80) ⟶ False) ⟶ False) ⟶ ((x53 x4 ⟶ False) ⟶ False) ⟶ (x79 x4 ⟶ False) ⟶ ((x16 x4 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x67 x81 ⟶ x67 x80 ⟶ (x67 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ ((x56 x4 ⟶ False) ⟶ False) ⟶ ((x56 x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x67 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x11 x81 ⟶ (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ x79 (x5 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . x22 x81 ⟶ x22 x80 ⟶ (x22 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x67 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x0 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x11 x81 ⟶ (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ x79 (x5 x81 x80) ⟶ False) ⟶ ((x29 x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ (x22 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ (x0 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x7 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x2 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x2 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x2 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x2 x81 x80) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x71 x80) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x11 x81 ⟶ x11 x80 ⟶ (x11 (x1 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x22 x81 ⟶ x22 x80 ⟶ (x22 (x1 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x14 x80 ⟶ x67 x80 ⟶ (x14 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x14 x80 ⟶ x67 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x71 x80) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x7 x80 ⟶ x67 x80 ⟶ (x7 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x7 x80 ⟶ x67 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x1 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x7 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x1 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x7 x81 ⟶ False) ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x1 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x7 x81 ⟶ False) ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x1 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . x14 x81 ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x7 (x72 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x14 x81 ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x14 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x14 (x72 x80 x81) ⟶ False) ⟶ False) ⟶ ((x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 (x76 x80) ⟶ False) ⟶ (x79 x70 ⟶ False) ⟶ (∀ x80 x81 . x11 x81 ⟶ x11 x80 ⟶ (x11 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x22 x81 ⟶ x22 x80 ⟶ (x22 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x7 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x72 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x14 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x72 x81 x80) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x73 x80) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x0 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x14 (x73 x80) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x0 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x14 x81 ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x14 (x5 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x14 x81 ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ (x14 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x7 (x5 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x67 x81 ⟶ (x14 x80 ⟶ False) ⟶ x67 x80 ⟶ (x7 (x5 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x7 x81 ⟶ False) ⟶ x67 x81 ⟶ (x7 x80 ⟶ False) ⟶ x67 x80 ⟶ x7 (x5 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x75 x80 (x76 x81) ⟶ (x69 (x44 x80 x81) x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x75 (x30 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x75 x80 (x76 x82) ⟶ x69 x81 x82 x80 ⟶ (x75 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 x70 ⟶ x67 x80 ⟶ (x75 (x68 x81 x80) x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x0 (x71 x80) ⟶ False) ⟶ False) ⟶ ((x75 x6 (x76 x70) ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x0 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 x70 ⟶ x67 x80 ⟶ (x75 (x66 x81 x80) x70 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x2 x81 x80 = x1 x81 (x71 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x72 x81 x80 = x5 x81 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 x70 ⟶ x67 x80 ⟶ (x68 x81 x80 = x68 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x1 x81 x80 = x1 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ x0 x80 ⟶ (x5 x81 x80 = x5 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x31 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ (x7 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ (x7 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 x4 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 (x76 x70) ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x9 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x65 x80 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x65 x80 ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x65 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x65 x80 ⟶ (x7 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x65 x80 ⟶ (x7 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x14 x80 ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x14 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x14 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x53 x81 ⟶ x75 x80 x81 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x29 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x65 x80 ⟶ (x14 x80 ⟶ False) ⟶ (x7 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x65 x80 ⟶ (x14 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x75 x80 (x76 x81) ⟶ x61 x80 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x42 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x29 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x7 x80 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x7 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x7 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x67 x80 ⟶ (x0 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x75 x80 (x76 x81) ⟶ x79 x80 ⟶ (x61 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x41 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x75 x80 (x76 x81) ⟶ (x61 x80 x81 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x51 x80 ⟶ x20 x80 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 x6 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x34 x80 ⟶ (x41 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x56 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 x6 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x16 x81 ⟶ x75 x80 (x76 x81) ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x75 x80 (x76 x81) ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x41 x81 ⟶ x75 x80 (x76 x81) ⟶ (x41 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x29 x81 ⟶ x75 x80 (x76 x81) ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x33 x81 ⟶ x75 x80 (x76 x81) ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 x70 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x75 x80 (x76 x81) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x53 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x53 x80 ⟶ (x51 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x16 x80 ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x32 x81 ⟶ x75 x80 (x76 x81) ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x16 x81 ⟶ x75 x80 x81 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x75 x80 x81 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x41 x81 ⟶ x75 x80 x81 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x29 x81 ⟶ x75 x80 x81 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x33 x81 ⟶ x75 x80 x81 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x32 x81 ⟶ x75 x80 x81 ⟶ (x0 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 (x76 x6) ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x9 x81 ⟶ x75 x80 (x76 x81) ⟶ (x9 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x31 x81 ⟶ x75 x80 (x76 x81) ⟶ (x31 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x9 x81 ⟶ x75 x80 x81 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x78 x80 x81 ⟶ x78 x81 x80 ⟶ False) ⟶ (x66 (x66 x38 x37) (x66 x36 x39) = x68 (x66 x38 x36) (x66 x39 x37) ⟶ False) ⟶ ((x75 x39 x70 ⟶ False) ⟶ False) ⟶ ((x75 x36 x70 ⟶ False) ⟶ False) ⟶ ((x75 x37 x70 ⟶ False) ⟶ False) ⟶ ((x75 x38 x70 ⟶ False) ⟶ False) ⟶ False (proof)