Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../44bb5..
PUWPs../73c14..
vout
PrNUD../f83ce.. 0.00 bars
TMTFC../78e87.. ownership of 7c33d.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMJvp../36666.. ownership of 0cc04.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUgmg../6c42e.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7c33d.. : ∀ 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 . x80 x82 ⟶ x80 x81 ⟶ (x79 x82 x81 ⟶ False) ⟶ (x78 x81 ⟶ False) ⟶ (x77 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x0 x82 ⟶ (x82 = x81 ⟶ False) ⟶ x0 x81 ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ (x79 x82 x81 ⟶ False) ⟶ (x77 x82 ⟶ False) ⟶ (x78 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x9 x82 ⟶ x79 x81 (x8 x82 x7) ⟶ (x4 (x3 x84) (x5 x84 x83 x81 x82) (x6 x84 x83 (x8 x82 x7)) = x6 x84 x83 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x76 x81 x82 ⟶ x0 x82 ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ (x0 x82 ⟶ False) ⟶ (x77 x81 ⟶ False) ⟶ (x78 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ (x81 = x75 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x76 x81 x82 ⟶ x1 x82 (x2 x83) ⟶ x0 x83 ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ (x0 x81 ⟶ False) ⟶ (x78 x82 ⟶ False) ⟶ (x77 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x76 x82 x83 ⟶ x1 x83 (x2 x81) ⟶ (x1 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ (x77 x81 ⟶ False) ⟶ x77 x82 ⟶ False) ⟶ (∀ x81 x82 . x10 x82 x81 ⟶ (x1 x82 (x2 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x1 x82 (x2 x81) ⟶ (x10 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ (x78 x82 ⟶ False) ⟶ x78 x81 ⟶ False) ⟶ (∀ x81 x82 x83 . x76 x82 x83 ⟶ x76 x81 x83 ⟶ x76 x81 (x74 x83 x82) ⟶ False) ⟶ (∀ x81 x82 . x76 x82 x81 ⟶ (x76 (x74 x81 x82) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x1 x81 x82 ⟶ (x0 x82 ⟶ False) ⟶ (x76 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ x78 x81 ⟶ (x78 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x76 x82 x81 ⟶ (x1 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ x79 x82 x81 ⟶ x77 x82 ⟶ (x77 x81 ⟶ False) ⟶ False) ⟶ ((x1 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x11 x81 x75 = x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x72 x81 ⟶ (x8 x81 x71 = x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x3 x83)) ⟶ x9 x81 ⟶ x81 = x71 ⟶ (x6 x83 x82 x81 = x12 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x3 x83)) ⟶ x9 x81 ⟶ x76 (x70 x83) x82 ⟶ (x6 x83 x82 x81 = x12 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x3 x83)) ⟶ x9 x81 ⟶ x6 x83 x82 x81 = x12 x83 x82 ⟶ (x76 (x70 x83) x82 ⟶ False) ⟶ (x81 = x71 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x72 x83 ⟶ x72 x81 ⟶ x72 x82 ⟶ (x8 (x8 x83 x81) x82 = x8 x83 (x8 x81 x82) ⟶ False) ⟶ False) ⟶ ((x1 x7 x13 ⟶ False) ⟶ False) ⟶ ((x1 x7 x69 ⟶ False) ⟶ False) ⟶ ((x14 x7 x13 x69 ⟶ False) ⟶ False) ⟶ ((x77 x7 ⟶ False) ⟶ False) ⟶ (x0 x7 ⟶ False) ⟶ ((x1 x68 x13 ⟶ False) ⟶ False) ⟶ ((x1 x68 x69 ⟶ False) ⟶ False) ⟶ ((x14 x68 x13 x69 ⟶ False) ⟶ False) ⟶ ((x0 x68 ⟶ False) ⟶ False) ⟶ ((x8 x7 x68 = x7 ⟶ False) ⟶ False) ⟶ ((x8 x68 x7 = x7 ⟶ False) ⟶ False) ⟶ ((x8 x68 x68 = x68 ⟶ False) ⟶ False) ⟶ ((x79 x7 x7 ⟶ False) ⟶ False) ⟶ (x79 x7 x68 ⟶ False) ⟶ ((x79 x68 x7 ⟶ False) ⟶ False) ⟶ ((x79 x68 x68 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x15 x82 ⟶ x15 x81 ⟶ (x79 x82 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x10 x81 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . (x0 x83 ⟶ False) ⟶ (x0 x81 ⟶ False) ⟶ x1 x81 (x2 x83) ⟶ x1 x82 x81 ⟶ (x14 x82 x83 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . (x0 x83 ⟶ False) ⟶ (x0 x81 ⟶ False) ⟶ x1 x81 (x2 x83) ⟶ x14 x82 x83 x81 ⟶ (x1 x82 x81 ⟶ False) ⟶ False) ⟶ ((x71 = x75 ⟶ False) ⟶ False) ⟶ ((x69 = x73 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 x83) ⟶ x1 x81 (x2 x83) ⟶ (x4 x83 x82 x81 = x11 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x67 x81 = x3 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x70 x81 = x16 x81 ⟶ False) ⟶ False) ⟶ ((x9 x66 ⟶ False) ⟶ False) ⟶ (x0 x66 ⟶ False) ⟶ ((x15 x65 ⟶ False) ⟶ False) ⟶ ((x0 x65 ⟶ False) ⟶ False) ⟶ ((x80 x64 ⟶ False) ⟶ False) ⟶ ((x15 x64 ⟶ False) ⟶ False) ⟶ ((x72 x64 ⟶ False) ⟶ False) ⟶ ((x0 x64 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x62 (x63 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x1 (x63 x81) (x2 x81) ⟶ False) ⟶ False) ⟶ ((x9 x61 ⟶ False) ⟶ False) ⟶ ((x78 x17 ⟶ False) ⟶ False) ⟶ ((x15 x17 ⟶ False) ⟶ False) ⟶ ((x80 x18 ⟶ False) ⟶ False) ⟶ ((x78 x18 ⟶ False) ⟶ False) ⟶ ((x15 x18 ⟶ False) ⟶ False) ⟶ ((x72 x18 ⟶ False) ⟶ False) ⟶ (∀ x81 . x62 (x19 x81) x81 ⟶ False) ⟶ (∀ x81 . (x1 (x19 x81) (x2 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x20 (x21 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x60 (x21 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x22 (x21 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x59 (x21 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x24 (x23 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x0 (x23 x81) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x60 (x23 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x20 (x23 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x22 (x23 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x59 (x23 x81) ⟶ False) ⟶ False) ⟶ ((x77 x25 ⟶ False) ⟶ False) ⟶ ((x15 x25 ⟶ False) ⟶ False) ⟶ ((x80 x26 ⟶ False) ⟶ False) ⟶ ((x77 x26 ⟶ False) ⟶ False) ⟶ ((x15 x26 ⟶ False) ⟶ False) ⟶ ((x72 x26 ⟶ False) ⟶ False) ⟶ (x0 x27 ⟶ False) ⟶ (∀ x81 . (x0 (x58 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x1 (x58 x81) (x2 x81) ⟶ False) ⟶ False) ⟶ ((x57 x56 ⟶ False) ⟶ False) ⟶ ((x28 x56 ⟶ False) ⟶ False) ⟶ ((x55 x56 ⟶ False) ⟶ False) ⟶ (x0 x56 ⟶ False) ⟶ ((x57 x54 ⟶ False) ⟶ False) ⟶ (x0 x54 ⟶ False) ⟶ ((x1 x54 (x2 x13) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x24 (x29 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 (x29 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x60 (x29 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x20 (x29 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x22 (x29 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x59 (x29 x81) ⟶ False) ⟶ False) ⟶ ((x15 x30 ⟶ False) ⟶ False) ⟶ ((x80 x53 ⟶ False) ⟶ False) ⟶ ((x0 x31 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x0 (x52 x81) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ (x1 (x52 x81) (x2 x81) ⟶ False) ⟶ False) ⟶ ((x57 x51 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x24 (x32 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x60 (x32 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x20 (x32 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x22 (x32 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x59 (x32 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 x83) ⟶ x1 x81 (x2 x83) ⟶ (x4 x83 x82 x82 = x82 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x11 x81 x81 = x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 x85 x86 . x1 x85 (x2 (x3 x86)) ⟶ x9 x81 ⟶ x1 x84 (x2 (x3 x86)) ⟶ x82 = x84 ⟶ x9 x83 ⟶ x79 x81 x83 ⟶ x84 = x50 x86 x85 x83 ⟶ (x76 x82 (x49 x86 x85 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x76 x82 (x49 x84 x83 x81) ⟶ (x33 x81 x83 x84 x82 = x50 x84 x83 (x34 x81 x83 x84 x82) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x76 x82 (x49 x84 x83 x81) ⟶ (x79 x81 (x34 x81 x83 x84 x82) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x76 x82 (x49 x84 x83 x81) ⟶ (x9 (x34 x81 x83 x84 x82) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x76 x82 (x49 x84 x83 x81) ⟶ (x82 = x33 x81 x83 x84 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x76 x82 (x49 x84 x83 x81) ⟶ (x1 (x33 x81 x83 x84 x82) (x2 (x3 x84)) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x78 x82 ⟶ False) ⟶ x80 x82 ⟶ (x78 x81 ⟶ False) ⟶ x80 x81 ⟶ x78 (x8 x82 x81) ⟶ False) ⟶ ((x57 x73 ⟶ False) ⟶ False) ⟶ (x0 x73 ⟶ False) ⟶ (∀ x81 x82 . x80 x82 ⟶ x80 x81 ⟶ (x80 (x8 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x0 x82 ⟶ False) ⟶ x0 (x11 x81 x82) ⟶ False) ⟶ (∀ x81 x82 . (x0 x82 ⟶ False) ⟶ x0 (x11 x82 x81) ⟶ False) ⟶ (∀ x81 x82 . x9 x82 ⟶ (x0 x81 ⟶ False) ⟶ x9 x81 ⟶ x0 (x8 x81 x82) ⟶ False) ⟶ (∀ x81 . (x24 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x60 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x20 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x22 (x16 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x59 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . x57 x81 ⟶ (x57 (x35 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x9 x82 ⟶ (x0 x81 ⟶ False) ⟶ x9 x81 ⟶ x0 (x8 x82 x81) ⟶ False) ⟶ (∀ x81 . (x36 (x3 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 (x3 x81) ⟶ False) ⟶ ((x0 x75 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 (x2 x81) ⟶ False) ⟶ (∀ x81 x82 . x9 x82 ⟶ x9 x81 ⟶ (x9 (x8 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x78 x82 ⟶ x80 x82 ⟶ (x77 x81 ⟶ False) ⟶ x80 x81 ⟶ (x78 (x8 x81 x82) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x78 x82 ⟶ x80 x82 ⟶ (x77 x81 ⟶ False) ⟶ x80 x81 ⟶ (x78 (x8 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x77 x82 ⟶ x80 x82 ⟶ (x78 x81 ⟶ False) ⟶ x80 x81 ⟶ (x77 (x8 x81 x82) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x77 x82 ⟶ x80 x82 ⟶ (x78 x81 ⟶ False) ⟶ x80 x81 ⟶ (x77 (x8 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x77 x82 ⟶ False) ⟶ x80 x82 ⟶ (x77 x81 ⟶ False) ⟶ x80 x81 ⟶ x77 (x8 x82 x81) ⟶ False) ⟶ (∀ x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x81 ⟶ False) ⟶ x1 x81 (x2 x82) ⟶ (x14 (x37 x81 x82) x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x1 (x48 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x38 (x39 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . (x0 x83 ⟶ False) ⟶ (x0 x81 ⟶ False) ⟶ x1 x81 (x2 x83) ⟶ x14 x82 x83 x81 ⟶ (x1 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x38 x82 x81 ⟶ (x36 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x38 x82 x81 ⟶ x0 x82 ⟶ False) ⟶ (∀ x81 x82 . x1 x82 (x2 (x67 x81)) ⟶ (x1 (x12 x81 x82) (x2 (x67 x81)) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x67 x83)) ⟶ x9 x81 ⟶ (x1 (x50 x83 x82 x81) (x2 (x67 x83)) ⟶ False) ⟶ False) ⟶ ((x14 x71 x13 x69 ⟶ False) ⟶ False) ⟶ ((x1 x69 (x2 x13) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 x83) ⟶ x1 x81 (x2 x83) ⟶ (x1 (x4 x83 x82 x81) (x2 x83) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x24 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x60 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x20 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x22 (x16 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x59 (x16 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 . (x38 (x67 x81) x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x1 (x70 x81) (x67 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x3 x83)) ⟶ x9 x81 ⟶ (x1 (x6 x83 x82 x81) (x2 (x3 x83)) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 x84 . x1 x83 (x2 (x3 x84)) ⟶ x9 x81 ⟶ x9 x82 ⟶ (x1 (x5 x84 x83 x81 x82) (x2 (x3 x84)) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 (x3 x83)) ⟶ x9 x81 ⟶ (x6 x83 x82 x81 = x35 (x49 x83 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x15 x82 ⟶ x15 x81 ⟶ (x79 x82 x81 ⟶ False) ⟶ (x79 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 x83 . x1 x82 (x2 x83) ⟶ x1 x81 (x2 x83) ⟶ (x4 x83 x82 x81 = x4 x83 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x72 x82 ⟶ x72 x81 ⟶ (x8 x82 x81 = x8 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x11 x82 x81 = x11 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ (x47 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x41 x81 x69 ⟶ x60 x81 ⟶ x24 x81 ⟶ x40 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x41 x81 x69 ⟶ x60 x81 ⟶ x24 x81 ⟶ x40 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x41 x81 x69 ⟶ x60 x81 ⟶ x24 x81 ⟶ x40 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ (x77 x81 ⟶ False) ⟶ (x78 x81 ⟶ False) ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ (x77 x81 ⟶ False) ⟶ (x78 x81 ⟶ False) ⟶ (x0 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x1 x81 x73 ⟶ (x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x24 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x41 x81 x69 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ x15 x81 ⟶ x78 x81 ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ x15 x81 ⟶ x77 x81 ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ x15 x81 ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ (x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x40 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x24 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x15 x81 ⟶ (x77 x81 ⟶ False) ⟶ (x78 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x15 x81 ⟶ (x77 x81 ⟶ False) ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x57 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x40 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x78 x81 ⟶ x77 x81 ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x78 x81 ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x78 x81 ⟶ x0 x81 ⟶ False) ⟶ (∀ x81 x82 . x57 x82 ⟶ x1 x81 x82 ⟶ (x57 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x42 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x24 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x22 x81 x69 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x69 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x15 x81 ⟶ (x78 x81 ⟶ False) ⟶ (x77 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . (x0 x81 ⟶ False) ⟶ x15 x81 ⟶ (x78 x81 ⟶ False) ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x80 x81 ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x0 x82 ⟶ x1 x81 (x2 x82) ⟶ x62 x81 x82 ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x46 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x24 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x22 x81 x13 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x22 x81 x13 ⟶ x20 x81 ⟶ x60 x81 ⟶ x24 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x77 x81 ⟶ x78 x81 ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x77 x81 ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x15 x81 ⟶ x77 x81 ⟶ x0 x81 ⟶ False) ⟶ (∀ x81 . x80 x81 ⟶ (x72 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x0 x82 ⟶ False) ⟶ x1 x81 (x2 x82) ⟶ x0 x81 ⟶ (x62 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 . x0 x81 ⟶ (x57 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ x78 x81 ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x15 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . (x0 x82 ⟶ False) ⟶ x1 x81 (x2 x82) ⟶ (x62 x81 x82 ⟶ False) ⟶ x0 x81 ⟶ False) ⟶ (∀ x81 . x55 x81 ⟶ x28 x81 ⟶ (x57 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x1 x81 x69 ⟶ x78 x81 ⟶ False) ⟶ (∀ x81 . x1 x81 x13 ⟶ (x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x0 x82 ⟶ x1 x81 (x2 x82) ⟶ (x0 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x57 x81 ⟶ (x28 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x57 x81 ⟶ (x55 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x9 x81 ⟶ (x57 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x60 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x20 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 . x59 x81 ⟶ x60 x81 ⟶ x0 x81 ⟶ (x59 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x47 x82 ⟶ x1 x81 (x2 x82) ⟶ (x47 x81 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x1 x82 (x3 x81) ⟶ (x24 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x1 x82 (x3 x81) ⟶ (x20 x82 ⟶ False) ⟶ False) ⟶ (∀ x81 x82 . x76 x81 x82 ⟶ x76 x82 x81 ⟶ False) ⟶ (x12 x43 x44 = x4 (x3 x43) (x5 x43 x44 x71 x45) (x6 x43 x44 (x8 x45 x7)) ⟶ False) ⟶ ((x9 x45 ⟶ False) ⟶ False) ⟶ ((x1 x44 (x2 (x3 x43)) ⟶ False) ⟶ False) ⟶ False (proof)