Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../72119..
PUQYD../5e59b..
vout
PrNUD../ebcbd.. 0.02 bars
TMRos../57ce0.. ownership of 02223.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMNZs../85280.. ownership of b0027.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PULC6../c252f.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 02223.. : ∀ 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 : ι → ο . (∀ x82 x83 . x81 x83 ⟶ (x83 = x82 ⟶ False) ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . x0 x82 x83 ⟶ x81 x83 ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x82 = x80 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x0 x82 x83 ⟶ x2 x83 (x1 x84) ⟶ x81 x84 ⟶ False) ⟶ (∀ x82 x83 x84 . x0 x83 x84 ⟶ x2 x84 (x1 x82) ⟶ (x2 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x3 x83 x82 ⟶ (x2 x83 (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x2 x83 (x1 x82) ⟶ (x3 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x2 x82 x83 ⟶ (x81 x83 ⟶ False) ⟶ (x0 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x79 x82 x80 = x80 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x3 x83 x84 ⟶ (x3 (x79 x83 x82) (x79 x84 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x3 x83 x84 ⟶ x3 x84 x82 ⟶ (x3 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x0 x83 x82 ⟶ (x2 x83 x82 ⟶ False) ⟶ False) ⟶ ((x2 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x3 x83 x84 ⟶ x3 x83 x82 ⟶ (x3 x83 (x79 x84 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x3 (x79 x82 x83) x82 ⟶ False) ⟶ False) ⟶ ((x2 x5 x4 ⟶ False) ⟶ False) ⟶ ((x2 x5 x77 ⟶ False) ⟶ False) ⟶ ((x6 x5 x4 x77 ⟶ False) ⟶ False) ⟶ ((x76 x5 ⟶ False) ⟶ False) ⟶ (x81 x5 ⟶ False) ⟶ (∀ x82 . (x3 x82 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . (x81 x84 ⟶ False) ⟶ (x81 x82 ⟶ False) ⟶ x2 x82 (x1 x84) ⟶ x2 x83 x82 ⟶ (x6 x83 x84 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . (x81 x84 ⟶ False) ⟶ (x81 x82 ⟶ False) ⟶ x2 x82 (x1 x84) ⟶ x6 x83 x84 x82 ⟶ (x2 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x2 x83 (x1 x84) ⟶ (x7 x84 x82 x83 = x79 x82 x83 ⟶ False) ⟶ False) ⟶ ((x77 = x78 ⟶ False) ⟶ False) ⟶ ((x8 x9 ⟶ False) ⟶ False) ⟶ (x81 x9 ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x10 (x11 x82) x5 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x2 (x11 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x12 (x13 x82) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ (x2 (x13 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . x14 x82 ⟶ (x10 (x15 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x14 x82 ⟶ (x75 (x15 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . x14 x82 ⟶ (x16 (x15 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . x74 x82 ⟶ (x72 (x73 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x74 x82 ⟶ (x2 (x73 x82) (x1 (x17 x82)) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x12 (x71 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ x81 (x71 x82) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x2 (x71 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ (x81 x19 ⟶ False) ⟶ (x20 x21 ⟶ False) ⟶ ((x75 x21 ⟶ False) ⟶ False) ⟶ ((x16 x21 ⟶ False) ⟶ False) ⟶ (∀ x82 . x14 x82 ⟶ (x10 (x70 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x23 (x22 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x2 (x22 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ ((x18 x24 ⟶ False) ⟶ False) ⟶ ((x75 x69 ⟶ False) ⟶ False) ⟶ ((x25 x69 ⟶ False) ⟶ False) ⟶ ((x16 x69 ⟶ False) ⟶ False) ⟶ (x81 x69 ⟶ False) ⟶ (∀ x82 . (x68 x82 ⟶ False) ⟶ x68 (x67 x82) ⟶ False) ⟶ (∀ x82 . (x68 x82 ⟶ False) ⟶ (x2 (x67 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . x23 (x66 x82) x82 ⟶ False) ⟶ (∀ x82 . (x2 (x66 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ ((x75 x65 ⟶ False) ⟶ False) ⟶ ((x25 x65 ⟶ False) ⟶ False) ⟶ ((x16 x65 ⟶ False) ⟶ False) ⟶ (x68 x26 ⟶ False) ⟶ (x12 x64 ⟶ False) ⟶ (x81 x27 ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x23 (x63 x82) x82 ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x12 (x63 x82) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x81 (x63 x82) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ (x2 (x63 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 (x62 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x2 (x62 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ ((x25 x61 ⟶ False) ⟶ False) ⟶ ((x16 x61 ⟶ False) ⟶ False) ⟶ ((x60 x59 ⟶ False) ⟶ False) ⟶ ((x28 x59 ⟶ False) ⟶ False) ⟶ ((x58 x59 ⟶ False) ⟶ False) ⟶ (x81 x59 ⟶ False) ⟶ ((x57 x56 ⟶ False) ⟶ False) ⟶ ((x75 x56 ⟶ False) ⟶ False) ⟶ ((x16 x56 ⟶ False) ⟶ False) ⟶ ((x14 x29 ⟶ False) ⟶ False) ⟶ ((x68 x29 ⟶ False) ⟶ False) ⟶ ((x60 x29 ⟶ False) ⟶ False) ⟶ ((x28 x29 ⟶ False) ⟶ False) ⟶ ((x58 x29 ⟶ False) ⟶ False) ⟶ ((x12 x55 ⟶ False) ⟶ False) ⟶ (x81 x55 ⟶ False) ⟶ ((x81 x54 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ (x23 (x30 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ (x12 (x30 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x81 (x30 x82) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ (x2 (x30 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ x81 (x31 x82) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ (x2 (x31 x82) (x1 x82) ⟶ False) ⟶ False) ⟶ ((x16 x32 ⟶ False) ⟶ False) ⟶ (x81 x32 ⟶ False) ⟶ ((x60 x33 ⟶ False) ⟶ False) ⟶ ((x75 x53 ⟶ False) ⟶ False) ⟶ ((x16 x53 ⟶ False) ⟶ False) ⟶ ((x14 x52 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x2 x82 (x1 x84) ⟶ (x7 x84 x83 x83 = x83 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x79 x82 x82 = x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x68 x82 ⟶ False) ⟶ x68 (x1 x82) ⟶ False) ⟶ (x68 x78 ⟶ False) ⟶ ((x60 x78 ⟶ False) ⟶ False) ⟶ (x81 x78 ⟶ False) ⟶ ((x34 x78 ⟶ False) ⟶ False) ⟶ ((x14 x78 ⟶ False) ⟶ False) ⟶ ((x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 (x1 x82) ⟶ False) ⟶ (∀ x82 x83 . x16 x83 ⟶ (x16 (x79 x83 x82) ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x81 x83 ⟶ False) ⟶ (x81 x82 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x6 (x51 x82 x83) x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x2 (x35 x82) x82 ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x74 x36 ⟶ False) ⟶ False) ⟶ ((x81 x48 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . (x81 x84 ⟶ False) ⟶ (x81 x82 ⟶ False) ⟶ x2 x82 (x1 x84) ⟶ x6 x83 x84 x82 ⟶ (x2 x83 x84 ⟶ False) ⟶ False) ⟶ (∀ x82 . x74 x82 ⟶ (x50 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x2 x83 (x1 x84) ⟶ (x2 (x7 x84 x82 x83) (x1 x84) ⟶ False) ⟶ False) ⟶ ((x2 x77 (x1 x4) ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x74 x84 ⟶ x2 x82 (x1 (x17 x84)) ⟶ x2 x83 (x1 (x17 x84)) ⟶ x39 x83 x84 ⟶ x7 (x17 x84) x82 x83 = x38 x82 x84 ⟶ (x37 x82 x84 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x74 x83 ⟶ x2 x82 (x1 (x17 x83)) ⟶ (x3 (x38 x82 x83) x82 ⟶ False) ⟶ (x37 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x74 x83 ⟶ x2 x82 (x1 (x17 x83)) ⟶ (x2 (x38 x82 x83) (x1 (x17 x83)) ⟶ False) ⟶ (x37 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x74 x84 ⟶ x2 x82 (x1 (x17 x84)) ⟶ x37 x82 x84 ⟶ x2 x83 (x1 (x17 x84)) ⟶ x3 x83 x82 ⟶ (x7 (x17 x84) x82 (x47 x83 x82 x84) = x83 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x74 x84 ⟶ x2 x82 (x1 (x17 x84)) ⟶ x37 x82 x84 ⟶ x2 x83 (x1 (x17 x84)) ⟶ x3 x83 x82 ⟶ (x39 (x47 x83 x82 x84) x84 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x74 x84 ⟶ x2 x82 (x1 (x17 x84)) ⟶ x37 x82 x84 ⟶ x2 x83 (x1 (x17 x84)) ⟶ x3 x83 x82 ⟶ (x2 (x47 x83 x82 x84) (x1 (x17 x84)) ⟶ False) ⟶ False) ⟶ ((x80 = x48 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x3 x83 x82 ⟶ x3 x82 x83 ⟶ (x83 = x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x82 = x83 ⟶ (x3 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x83 = x82 ⟶ (x3 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 x84 . x2 x83 (x1 x84) ⟶ (x7 x84 x82 x83 = x7 x84 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x79 x83 x82 = x79 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x40 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x8 x83 ⟶ x2 x82 (x1 x83) ⟶ (x8 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x10 x82 x5 ⟶ (x12 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x10 x82 x5 ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 . x2 x82 x78 ⟶ (x18 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x8 x83 ⟶ x2 x82 x83 ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x8 x83 ⟶ x2 x82 x83 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x10 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x18 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x8 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x10 x82 x80 ⟶ (x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x18 x82 ⟶ (x60 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x12 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x20 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x12 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x12 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x60 x82 ⟶ x68 x82 ⟶ (x18 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x12 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ (x23 x82 x83 ⟶ False) ⟶ x12 x82 ⟶ False) ⟶ (∀ x82 x83 . (x12 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ (x23 x82 x83 ⟶ False) ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . x12 x83 ⟶ x2 x82 (x1 x83) ⟶ (x12 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x60 x83 ⟶ x2 x82 x83 ⟶ (x60 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x16 x82 ⟶ x75 x82 ⟶ (x20 x82 ⟶ False) ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x16 x82 ⟶ x75 x82 ⟶ (x20 x82 ⟶ False) ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x16 x82 ⟶ x75 x82 ⟶ (x20 x82 ⟶ False) ⟶ x12 x82 ⟶ False) ⟶ (∀ x82 . x18 x82 ⟶ (x68 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x12 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ x12 x82 ⟶ (x23 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . (x12 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ x12 x82 ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . x81 x83 ⟶ x2 x82 (x1 x83) ⟶ x23 x82 x83 ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ (x25 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x46 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x20 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x2 x82 x78 ⟶ (x68 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x10 x83 x5 ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ (x23 x82 x83 ⟶ False) ⟶ (x12 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x10 x83 x5 ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ (x23 x82 x83 ⟶ False) ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . (x81 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ x81 x82 ⟶ (x23 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ (x45 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x60 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x16 x83 ⟶ x75 x83 ⟶ x2 x82 (x1 x83) ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x18 x82 ⟶ (x14 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x12 x82 ⟶ False) ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . x74 x83 ⟶ x2 x82 (x1 (x17 x83)) ⟶ x81 x82 ⟶ (x72 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x10 x83 x5 ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ x23 x82 x83 ⟶ False) ⟶ (∀ x82 x83 . (x81 x83 ⟶ False) ⟶ x2 x82 (x1 x83) ⟶ (x23 x82 x83 ⟶ False) ⟶ x81 x82 ⟶ False) ⟶ (∀ x82 x83 . x16 x83 ⟶ x2 x82 (x1 x83) ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x58 x82 ⟶ x28 x82 ⟶ (x60 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x57 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ x16 x82 ⟶ x75 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x14 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x12 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x10 x83 x5 ⟶ x2 x82 (x1 x83) ⟶ x23 x82 x83 ⟶ (x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x81 x83 ⟶ x2 x82 (x1 x83) ⟶ (x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x16 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x60 x82 ⟶ (x28 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x60 x82 ⟶ (x58 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . x81 x82 ⟶ (x75 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x74 x83 ⟶ x2 x82 (x1 (x17 x83)) ⟶ x81 x82 ⟶ (x44 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x82 . x14 x82 ⟶ (x60 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x40 x83 ⟶ x2 x82 (x1 x83) ⟶ (x40 x82 ⟶ False) ⟶ False) ⟶ (∀ x82 . (x81 x82 ⟶ False) ⟶ x12 x82 ⟶ (x10 x82 x5 ⟶ False) ⟶ False) ⟶ (∀ x82 x83 . x0 x82 x83 ⟶ x0 x83 x82 ⟶ False) ⟶ (x37 x42 x41 ⟶ False) ⟶ ((x37 x43 x41 ⟶ False) ⟶ False) ⟶ ((x3 x42 x43 ⟶ False) ⟶ False) ⟶ ((x2 x42 (x1 (x17 x41)) ⟶ False) ⟶ False) ⟶ ((x2 x43 (x1 (x17 x41)) ⟶ False) ⟶ False) ⟶ ((x74 x41 ⟶ False) ⟶ False) ⟶ False (proof)