Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrS5Z../100d3..
PUZrh../bd98a..
vout
PrS5Z../f8ff7.. 24.99 bars
TMEnW../1226d.. ownership of cd3d8.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0
TMWvF../e9770.. ownership of 4f333.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0
PUf7b../8cd41.. doc published by PrDsC..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem cd3d8..t5_radix_1 : ∀ 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 x84 x85 x86 . (x79 (x80 (x81 x85 x86) (x81 x84 x86)) (x81 x83 x86) = x81 (x79 (x80 x85 x84) x83) x86 ⟶ False) ⟶ x82 x86 ⟶ x82 x83 ⟶ x82 x84 ⟶ x82 x85 ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 x84 x85 ⟶ False) ⟶ (x0 x83 x2 ⟶ False) ⟶ x1 x84 ⟶ x1 x85 ⟶ x1 x83 ⟶ x0 (x81 x84 x83) (x81 x85 x83) ⟶ False) ⟶ (∀ x83 x84 . (x77 (x75 x84 (x76 x83 x84)) (x74 x83 x84) = x83 ⟶ False) ⟶ (x0 x84 x2 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 x85 . (x3 x85 ⟶ False) ⟶ (x3 x83 ⟶ False) ⟶ (x4 x84 x83 ⟶ False) ⟶ x6 x84 x83 x85 ⟶ x4 x85 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 x85 . (x3 x85 ⟶ False) ⟶ (x3 x83 ⟶ False) ⟶ (x4 x84 x85 ⟶ False) ⟶ x6 x84 x83 x85 ⟶ x4 x85 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 x84 x85 ⟶ False) ⟶ x1 x85 ⟶ x1 x83 ⟶ x1 x84 ⟶ x0 (x79 x84 x83) (x79 x85 x83) ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 x84 x85 ⟶ False) ⟶ x1 x85 ⟶ x1 x83 ⟶ x1 x84 ⟶ x0 (x80 x84 x83) (x80 x85 x83) ⟶ False) ⟶ (∀ x83 x84 . (x7 x83 (x75 x84 (x76 x83 x84)) = x74 x83 x84 ⟶ False) ⟶ (x0 x84 x2 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 x85 . (x85 = x2 ⟶ False) ⟶ (x74 (x74 x84 (x73 x85 x83)) x83 = x74 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ x78 x85 ⟶ False) ⟶ (∀ x83 x84 x85 . (x80 (x73 x83 x85) (x73 x84 x85) = x73 (x80 x83 x84) x85 ⟶ False) ⟶ x82 x85 ⟶ x82 x84 ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ (x3 x83 ⟶ False) ⟶ (x6 (x72 x83 x84) x83 x84 ⟶ False) ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 x85 . (x3 x85 ⟶ False) ⟶ (x3 x83 ⟶ False) ⟶ (x6 x84 x85 x83 ⟶ False) ⟶ x4 x84 x83 ⟶ x4 x83 (x5 x85) ⟶ False) ⟶ (∀ x83 x84 . (x6 (x70 x84 x83) x69 x71 ⟶ False) ⟶ x4 x83 x71 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x84 = x2 ⟶ False) ⟶ (x83 = x2 ⟶ False) ⟶ (x73 x83 (x10 x83 (x9 x84 x8)) = x10 x83 x84 ⟶ False) ⟶ x78 x84 ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 (x79 x84 x85) (x79 x83 x85) ⟶ False) ⟶ x1 x85 ⟶ x1 x83 ⟶ x1 x84 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 (x80 x84 x85) (x80 x83 x85) ⟶ False) ⟶ x1 x85 ⟶ x1 x83 ⟶ x1 x84 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x6 (x75 x83 x84) x69 x71 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x6 (x77 x84 x83) x69 x71 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 x85 . (x73 (x73 x83 x84) x85 = x73 x83 (x73 x84 x85) ⟶ False) ⟶ x82 x85 ⟶ x82 x84 ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 x84 x85 . (x80 (x80 x83 x84) x85 = x80 x83 (x80 x84 x85) ⟶ False) ⟶ x82 x85 ⟶ x82 x84 ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 x84 x85 . (x81 (x73 x83 x84) x85 = x73 x83 (x81 x84 x85) ⟶ False) ⟶ x82 x85 ⟶ x82 x84 ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 x84 . (x0 x84 x2 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ x0 x84 (x74 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x0 x84 x2 ⟶ False) ⟶ x78 x83 ⟶ x1 x84 ⟶ x0 (x10 x84 x83) x2 ⟶ False) ⟶ (∀ x83 x84 x85 . (x0 x84 x85 ⟶ False) ⟶ x11 x85 ⟶ x11 x83 ⟶ x11 x84 ⟶ x0 x83 x85 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . x83 = x68 x84 ⟶ x1 x84 ⟶ x67 x83 ⟶ x0 x83 (x7 x84 x8) ⟶ False) ⟶ (∀ x83 x84 . (x83 = x68 x84 ⟶ False) ⟶ (x0 x83 (x7 x84 x8) ⟶ False) ⟶ x1 x84 ⟶ x67 x83 ⟶ x0 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 (x80 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 (x81 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 (x73 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x66 (x79 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x66 (x81 x84 x83) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x66 (x81 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x12 (x79 x84 x83) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 (x73 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 (x73 x84 x83) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 (x81 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 (x73 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 (x80 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x80 (x65 x84) (x65 x83) = x65 (x80 x84 x83) ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 x85 . (x4 x84 x85 ⟶ False) ⟶ x13 x84 x83 ⟶ x4 x83 (x5 x85) ⟶ False) ⟶ (∀ x83 x84 . (x70 x84 x83 = x10 x84 x83 ⟶ False) ⟶ x4 x83 x71 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ x78 x84 ⟶ x78 x83 ⟶ x3 (x80 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ x78 x84 ⟶ x78 x83 ⟶ x3 (x80 x84 x83) ⟶ False) ⟶ (∀ x83 x84 . (x4 (x7 x83 x84) x69 ⟶ False) ⟶ x1 x83 ⟶ x4 x84 x69 ⟶ False) ⟶ (∀ x83 x84 x85 . x3 x85 ⟶ x13 x84 x83 ⟶ x4 x83 (x5 x85) ⟶ False) ⟶ (∀ x83 x84 . x1 x84 ⟶ x1 x83 ⟶ x12 (x14 x83 x84) ⟶ False) ⟶ (∀ x83 x84 . (x68 (x81 x84 x83) = x64 x84 x83 ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x84 = x2 ⟶ False) ⟶ (x81 (x73 x83 x84) x84 = x83 ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x66 (x79 x83 x84) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x12 (x79 x84 x83) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x12 (x80 x83 x84) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ (x12 (x80 x84 x83) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 (x79 x84 x83) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 (x80 x83 x84) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 (x80 x84 x83) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x12 (x79 x83 x84) ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 x84 . (x7 x83 x84 = x79 x83 x84 ⟶ False) ⟶ x1 x83 ⟶ x4 x84 x69 ⟶ False) ⟶ (∀ x83 x84 . (x75 x83 x84 = x73 x83 x84 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x75 x83 x84 = x75 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x77 x84 x83 = x80 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x77 x84 x83 = x77 x83 x84 ⟶ False) ⟶ x78 x83 ⟶ x4 x84 x71 ⟶ False) ⟶ (∀ x83 x84 . (x79 (x65 x84) (x65 x83) = x79 x83 x84 ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x4 (x76 x84 x83) x71 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x4 (x9 x84 x83) x71 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x4 (x74 x84 x83) x71 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ (x66 x84 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x0 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ x0 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x66 x84 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ x66 x83 ⟶ x0 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x12 x83 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ x12 x83 ⟶ x0 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x80 x84 (x65 x83) = x79 x84 x83 ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x63 x84 x83 ⟶ False) ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . x13 x83 x84 ⟶ x13 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x67 (x79 x84 x83) ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x67 (x15 x84 x83) ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x67 (x64 x84 x83) ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x67 (x73 x84 x83) ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x67 (x80 x84 x83) ⟶ False) ⟶ x67 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x14 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x14 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x79 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x81 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x73 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x80 x84 x83) ⟶ False) ⟶ x1 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x1 (x10 x84 x83) ⟶ False) ⟶ x78 x83 ⟶ x1 x84 ⟶ False) ⟶ (∀ x83 x84 . (x82 (x10 x84 x83) ⟶ False) ⟶ x78 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x78 (x73 x84 x83) ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x78 (x80 x84 x83) ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x78 (x10 x84 x83) ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x62 x84 ⟶ False) ⟶ x62 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x16 x84 ⟶ False) ⟶ x16 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x61 x84 ⟶ False) ⟶ x61 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x17 x84 ⟶ False) ⟶ x17 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x60 x84 ⟶ False) ⟶ x60 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x18 x84 ⟶ False) ⟶ x18 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x59 x84 ⟶ False) ⟶ x59 x83 ⟶ x4 x84 (x5 x83) ⟶ False) ⟶ (∀ x83 x84 . (x0 x83 x84 ⟶ False) ⟶ (x0 x84 x83 ⟶ False) ⟶ x11 x83 ⟶ x11 x84 ⟶ False) ⟶ (∀ x83 x84 . (x4 x84 (x5 x83) ⟶ False) ⟶ x63 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x14 x84 x83 = x9 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x15 x84 x83 = x74 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x64 x84 x83 = x76 x84 x83 ⟶ False) ⟶ x78 x83 ⟶ x78 x84 ⟶ False) ⟶ (∀ x83 x84 . (x73 x84 x83 = x73 x83 x84 ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x80 x84 x83 = x80 x83 x84 ⟶ False) ⟶ x82 x83 ⟶ x82 x84 ⟶ False) ⟶ (∀ x83 x84 . (x3 x84 ⟶ False) ⟶ (x13 x83 x84 ⟶ False) ⟶ x4 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ (x0 x83 x84 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 x84 . (x12 x84 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ (x0 x83 x84 ⟶ False) ⟶ x1 x84 ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 x84 . (x0 x84 x83 ⟶ False) ⟶ x84 = x68 x83 ⟶ x1 x83 ⟶ x67 x84 ⟶ False) ⟶ (∀ x83 x84 . (x4 x84 x83 ⟶ False) ⟶ x13 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x67 x84 ⟶ False) ⟶ x62 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x58 x84 ⟶ False) ⟶ x16 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x1 x84 ⟶ False) ⟶ x61 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x11 x84 ⟶ False) ⟶ x17 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x82 x84 ⟶ False) ⟶ x60 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x57 x84 ⟶ False) ⟶ x59 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 x84 . (x78 x84 ⟶ False) ⟶ x18 x83 ⟶ x4 x84 x83 ⟶ False) ⟶ (∀ x83 . (x61 x83 ⟶ False) ⟶ x4 x83 (x5 x69) ⟶ False) ⟶ (∀ x83 . (x18 x83 ⟶ False) ⟶ x4 x83 (x5 x71) ⟶ False) ⟶ (∀ x83 . (x56 x83 ⟶ False) ⟶ (x4 (x55 x83) (x5 x83) ⟶ False) ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x4 (x19 x83) (x5 x83) ⟶ False) ⟶ False) ⟶ (∀ x83 x84 . x3 x84 ⟶ x13 x83 x84 ⟶ False) ⟶ (∀ x83 x84 . (x0 x84 x84 ⟶ False) ⟶ x11 x83 ⟶ x11 x84 ⟶ False) ⟶ (∀ x83 . (x66 x83 ⟶ False) ⟶ x1 x83 ⟶ x12 (x65 x83) ⟶ False) ⟶ (∀ x83 . (x12 x83 ⟶ False) ⟶ x1 x83 ⟶ x66 (x65 x83) ⟶ False) ⟶ (∀ x83 . (x73 x83 (x65 x8) = x65 x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x21 (x22 x83) x83 ⟶ False) ⟶ x20 x83 ⟶ False) ⟶ (∀ x83 . x12 x83 ⟶ x4 x83 x71 ⟶ False) ⟶ (∀ x83 . x3 x83 ⟶ x21 x83 x8 ⟶ False) ⟶ (∀ x83 . (x56 x83 ⟶ False) ⟶ x4 x83 x54 ⟶ False) ⟶ (∀ x83 . (x1 x83 ⟶ False) ⟶ x4 x83 x69 ⟶ False) ⟶ (∀ x83 . (x18 x83 ⟶ False) ⟶ x4 x83 x71 ⟶ False) ⟶ (∀ x83 . (x23 x83 ⟶ False) ⟶ x21 x83 x8 ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ x21 x83 x53 ⟶ False) ⟶ (∀ x83 . (x78 x83 ⟶ False) ⟶ x13 x83 x54 ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x21 x83 x8 ⟶ False) ⟶ x23 x83 ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x21 (x19 x83) x8 ⟶ False) ⟶ False) ⟶ (∀ x83 . (x66 x83 ⟶ False) ⟶ (x82 (x65 x83) ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x12 x83 ⟶ False) ⟶ (x82 (x65 x83) ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x68 (x68 x83) = x68 x83 ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . x11 x83 ⟶ x12 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 . x11 x83 ⟶ x12 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 . x3 x83 ⟶ x11 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 . x3 x83 ⟶ x11 x83 ⟶ x66 x83 ⟶ False) ⟶ (∀ x83 . x3 x83 ⟶ x11 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 . x3 x83 ⟶ x11 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 . (x56 x83 ⟶ False) ⟶ x56 (x55 x83) ⟶ False) ⟶ (∀ x83 . (x56 x83 ⟶ False) ⟶ x56 (x5 x83) ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x11 x83 ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x11 x83 ⟶ False) ⟶ (∀ x83 . (x3 x83 ⟶ False) ⟶ (x12 x83 ⟶ False) ⟶ (x66 x83 ⟶ False) ⟶ x11 x83 ⟶ False) ⟶ (∀ x83 . (x73 x8 x83 = x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x79 x83 x2 = x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x81 x83 x8 = x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x80 x83 x2 = x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x21 x83 x53 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (∀ x83 . (x13 x83 x54 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x81 x2 x83 = x2 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x73 x83 x2 = x2 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x78 x83 ⟶ False) ⟶ x52 x83 ⟶ x56 x83 ⟶ False) ⟶ (∀ x83 . (x65 (x65 x83) = x83 ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 . (x67 (x65 x83) ⟶ False) ⟶ x67 x83 ⟶ False) ⟶ (∀ x83 . (x67 (x68 x83) ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x1 (x65 x83) ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x82 (x65 x83) ⟶ False) ⟶ x67 x83 ⟶ False) ⟶ (∀ x83 . (x82 (x65 x83) ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x82 (x65 x83) ⟶ False) ⟶ x82 x83 ⟶ False) ⟶ (∀ x83 x84 . (x84 = x83 ⟶ False) ⟶ x3 x83 ⟶ x3 x84 ⟶ False) ⟶ (∀ x83 . x78 x83 ⟶ x12 x83 ⟶ False) ⟶ (∀ x83 . (x51 x83 ⟶ False) ⟶ x59 x83 ⟶ False) ⟶ (∀ x83 . (x56 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x50 x83 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (∀ x83 . (x52 x83 ⟶ False) ⟶ x20 x83 ⟶ False) ⟶ (∀ x83 . (x52 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x20 x83 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (∀ x83 . (x20 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x67 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x62 x83 ⟶ False) ⟶ x18 x83 ⟶ False) ⟶ (∀ x83 . (x16 x83 ⟶ False) ⟶ x62 x83 ⟶ False) ⟶ (∀ x83 . (x1 x83 ⟶ False) ⟶ x67 x83 ⟶ False) ⟶ (∀ x83 . (x1 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x61 x83 ⟶ False) ⟶ x16 x83 ⟶ False) ⟶ (∀ x83 . (x11 x83 ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x11 x83 ⟶ False) ⟶ x78 x83 ⟶ False) ⟶ (∀ x83 . (x17 x83 ⟶ False) ⟶ x61 x83 ⟶ False) ⟶ (∀ x83 . (x82 x83 ⟶ False) ⟶ x1 x83 ⟶ False) ⟶ (∀ x83 . (x60 x83 ⟶ False) ⟶ x61 x83 ⟶ False) ⟶ (∀ x83 . (x18 x83 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (∀ x83 . (x59 x83 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (∀ x83 . (x83 = x53 ⟶ False) ⟶ x3 x83 ⟶ False) ⟶ (x0 (x81 x8 x25) x24 ⟶ False) ⟶ (x0 x25 (x81 x8 x25) ⟶ False) ⟶ (x0 x8 (x81 x8 x25) ⟶ False) ⟶ (x0 (x65 x8) (x65 x25) ⟶ False) ⟶ (x0 x25 (x65 x25) ⟶ False) ⟶ (x0 x25 (x65 x8) ⟶ False) ⟶ (x0 x24 (x65 x25) ⟶ False) ⟶ (x0 x24 (x65 x8) ⟶ False) ⟶ (x0 x8 (x65 x25) ⟶ False) ⟶ (x0 x8 (x65 x8) ⟶ False) ⟶ (x0 x25 x24 ⟶ False) ⟶ (x0 x25 x8 ⟶ False) ⟶ (x0 x8 x24 ⟶ False) ⟶ (x56 x49 ⟶ False) ⟶ (x56 x54 ⟶ False) ⟶ (x56 x69 ⟶ False) ⟶ (x3 x26 ⟶ False) ⟶ (x3 x48 ⟶ False) ⟶ (x3 x27 ⟶ False) ⟶ (x3 x47 ⟶ False) ⟶ (x3 x28 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ (x3 x25 ⟶ False) ⟶ (x3 x69 ⟶ False) ⟶ (x3 x8 ⟶ False) ⟶ (x45 = x2 ⟶ False) ⟶ (x29 = x2 ⟶ False) ⟶ ((x0 x29 (x76 (x74 x44 (x10 x29 x45)) (x10 x29 (x9 x45 x8))) ⟶ False) ⟶ False) ⟶ ((x79 (x81 (x65 x8) x25) (x81 (x65 x8) x25) = x24 ⟶ False) ⟶ False) ⟶ ((x79 (x81 (x65 x8) x25) (x81 x8 x25) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x80 (x81 (x65 x8) x25) (x81 x8 x25) = x24 ⟶ False) ⟶ False) ⟶ ((x79 (x81 x8 x25) (x81 (x65 x8) x25) = x8 ⟶ False) ⟶ False) ⟶ ((x80 (x81 x8 x25) (x81 (x65 x8) x25) = x24 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x8) (x81 (x65 x8) x25) = x81 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x79 (x81 (x65 x8) x25) (x65 x8) = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x73 (x81 (x65 x8) x25) x8 = x81 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x0 (x81 x8 x25) (x81 x8 x25) ⟶ False) ⟶ False) ⟶ ((x79 (x81 x8 x25) (x81 x8 x25) = x24 ⟶ False) ⟶ False) ⟶ ((x80 (x81 x8 x25) (x81 x8 x25) = x8 ⟶ False) ⟶ False) ⟶ ((x80 (x81 (x65 x8) x25) x8 = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x80 x8 (x81 (x65 x8) x25) = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x6 x25 x69 x71 ⟶ False) ⟶ False) ⟶ ((x6 x24 x69 x71 ⟶ False) ⟶ False) ⟶ ((x6 x8 x69 x71 ⟶ False) ⟶ False) ⟶ ((x6 x2 x69 x71 ⟶ False) ⟶ False) ⟶ ((x79 (x81 x8 x25) x8 = x81 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x79 x24 (x81 x8 x25) = x81 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x73 (x81 (x65 x8) x25) (x65 x25) = x8 ⟶ False) ⟶ False) ⟶ ((x73 (x65 x25) (x81 (x65 x8) x25) = x8 ⟶ False) ⟶ False) ⟶ ((x81 x8 (x81 (x65 x8) x25) = x65 x25 ⟶ False) ⟶ False) ⟶ ((x73 x25 (x81 (x65 x8) x25) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x65 (x81 (x65 x8) x25) = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x73 (x81 x8 x25) x8 = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x79 x8 (x81 x8 x25) = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x73 x8 (x81 x8 x25) = x81 x8 x25 ⟶ False) ⟶ False) ⟶ ((x73 (x81 x8 x25) (x65 x25) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x73 (x65 x25) (x81 x8 x25) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x65 (x81 x8 x25) = x81 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x0 (x81 x8 x25) x25 ⟶ False) ⟶ False) ⟶ ((x0 (x81 x8 x25) x8 ⟶ False) ⟶ False) ⟶ ((x0 x24 (x81 x8 x25) ⟶ False) ⟶ False) ⟶ ((x73 (x81 x8 x25) x25 = x8 ⟶ False) ⟶ False) ⟶ ((x81 x8 (x81 x8 x25) = x25 ⟶ False) ⟶ False) ⟶ ((x73 x25 (x81 x8 x25) = x8 ⟶ False) ⟶ False) ⟶ ((x73 x24 (x81 x8 x25) = x24 ⟶ False) ⟶ False) ⟶ ((x81 (x65 x8) x25 = x81 x8 (x65 x25) ⟶ False) ⟶ False) ⟶ ((x79 (x65 x25) (x65 x8) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x80 (x65 x8) (x65 x8) = x65 x25 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x25) (x65 x25) ⟶ False) ⟶ False) ⟶ ((x0 (x65 x25) (x65 x8) ⟶ False) ⟶ False) ⟶ ((x0 (x65 x8) (x65 x8) ⟶ False) ⟶ False) ⟶ ((x79 (x65 x25) (x65 x25) = x24 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x8) (x65 x25) = x8 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x8) (x65 x8) = x24 ⟶ False) ⟶ False) ⟶ (∀ x83 . (x4 (x30 x83) x83 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x25) x24 = x65 x25 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x8) x24 = x65 x8 ⟶ False) ⟶ False) ⟶ ((x79 (x65 x8) x8 = x65 x25 ⟶ False) ⟶ False) ⟶ ((x73 (x65 x25) x8 = x65 x25 ⟶ False) ⟶ False) ⟶ ((x80 (x65 x25) x8 = x65 x8 ⟶ False) ⟶ False) ⟶ ((x80 (x65 x8) x24 = x65 x8 ⟶ False) ⟶ False) ⟶ ((x81 x8 (x65 x8) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x73 x8 (x65 x25) = x65 x25 ⟶ False) ⟶ False) ⟶ ((x80 x24 (x65 x8) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x80 x8 (x65 x25) = x65 x8 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x25) x25 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x25) x24 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x25) x8 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x8) x25 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x8) x24 ⟶ False) ⟶ False) ⟶ ((x0 (x65 x8) x8 ⟶ False) ⟶ False) ⟶ ((x4 x47 (x5 x69) ⟶ False) ⟶ False) ⟶ ((x4 x71 (x5 x69) ⟶ False) ⟶ False) ⟶ ((x80 (x65 x25) x25 = x24 ⟶ False) ⟶ False) ⟶ ((x80 (x65 x8) x25 = x8 ⟶ False) ⟶ False) ⟶ ((x80 (x65 x8) x8 = x24 ⟶ False) ⟶ False) ⟶ ((x79 x24 (x65 x25) = x25 ⟶ False) ⟶ False) ⟶ ((x79 x24 (x65 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x79 x8 (x65 x8) = x25 ⟶ False) ⟶ False) ⟶ ((x80 x25 (x65 x25) = x24 ⟶ False) ⟶ False) ⟶ ((x80 x25 (x65 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x80 x8 (x65 x8) = x24 ⟶ False) ⟶ False) ⟶ (∀ x83 . (x63 x83 x83 ⟶ False) ⟶ False) ⟶ ((x79 x24 x25 = x65 x25 ⟶ False) ⟶ False) ⟶ ((x79 x24 x8 = x65 x8 ⟶ False) ⟶ False) ⟶ ((x79 x8 x25 = x65 x8 ⟶ False) ⟶ False) ⟶ ((x4 x31 x69 ⟶ False) ⟶ False) ⟶ ((x4 x25 x69 ⟶ False) ⟶ False) ⟶ ((x4 x25 x71 ⟶ False) ⟶ False) ⟶ ((x4 x24 x69 ⟶ False) ⟶ False) ⟶ ((x4 x24 x71 ⟶ False) ⟶ False) ⟶ ((x4 x53 x54 ⟶ False) ⟶ False) ⟶ ((x4 x8 x69 ⟶ False) ⟶ False) ⟶ ((x4 x8 x71 ⟶ False) ⟶ False) ⟶ ((x0 x25 x25 ⟶ False) ⟶ False) ⟶ ((x0 x24 x25 ⟶ False) ⟶ False) ⟶ ((x0 x24 x24 ⟶ False) ⟶ False) ⟶ ((x0 x24 x8 ⟶ False) ⟶ False) ⟶ ((x0 x8 x25 ⟶ False) ⟶ False) ⟶ ((x0 x8 x8 ⟶ False) ⟶ False) ⟶ ((x79 x25 x25 = x24 ⟶ False) ⟶ False) ⟶ ((x79 x25 x24 = x25 ⟶ False) ⟶ False) ⟶ ((x79 x25 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x79 x8 x24 = x8 ⟶ False) ⟶ False) ⟶ ((x79 x8 x8 = x24 ⟶ False) ⟶ False) ⟶ ((x81 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x73 x25 x24 = x24 ⟶ False) ⟶ False) ⟶ ((x73 x25 x8 = x25 ⟶ False) ⟶ False) ⟶ ((x73 x24 x25 = x24 ⟶ False) ⟶ False) ⟶ ((x73 x24 x24 = x24 ⟶ False) ⟶ False) ⟶ ((x73 x24 x8 = x24 ⟶ False) ⟶ False) ⟶ ((x73 x8 x25 = x25 ⟶ False) ⟶ False) ⟶ ((x73 x8 x24 = x24 ⟶ False) ⟶ False) ⟶ ((x73 x8 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x80 x25 x24 = x25 ⟶ False) ⟶ False) ⟶ ((x80 x24 x25 = x25 ⟶ False) ⟶ False) ⟶ ((x80 x24 x24 = x24 ⟶ False) ⟶ False) ⟶ ((x80 x24 x8 = x8 ⟶ False) ⟶ False) ⟶ ((x80 x8 x24 = x8 ⟶ False) ⟶ False) ⟶ ((x80 x8 x8 = x25 ⟶ False) ⟶ False) ⟶ ((x65 (x65 x25) = x25 ⟶ False) ⟶ False) ⟶ ((x65 (x65 x8) = x8 ⟶ False) ⟶ False) ⟶ ((x32 x54 ⟶ False) ⟶ False) ⟶ ((x66 x43 ⟶ False) ⟶ False) ⟶ ((x66 x33 ⟶ False) ⟶ False) ⟶ ((x66 x25 ⟶ False) ⟶ False) ⟶ ((x66 x8 ⟶ False) ⟶ False) ⟶ ((x12 x42 ⟶ False) ⟶ False) ⟶ ((x12 x34 ⟶ False) ⟶ False) ⟶ ((x50 x48 ⟶ False) ⟶ False) ⟶ ((x50 x54 ⟶ False) ⟶ False) ⟶ ((x50 x69 ⟶ False) ⟶ False) ⟶ ((x52 x47 ⟶ False) ⟶ False) ⟶ ((x20 x41 ⟶ False) ⟶ False) ⟶ ((x20 x54 ⟶ False) ⟶ False) ⟶ ((x67 x40 ⟶ False) ⟶ False) ⟶ ((x67 x31 ⟶ False) ⟶ False) ⟶ ((x1 x39 ⟶ False) ⟶ False) ⟶ ((x1 x34 ⟶ False) ⟶ False) ⟶ ((x1 x33 ⟶ False) ⟶ False) ⟶ ((x1 x35 ⟶ False) ⟶ False) ⟶ ((x1 x31 ⟶ False) ⟶ False) ⟶ ((x61 x69 ⟶ False) ⟶ False) ⟶ ((x11 x38 ⟶ False) ⟶ False) ⟶ ((x11 x39 ⟶ False) ⟶ False) ⟶ ((x11 x42 ⟶ False) ⟶ False) ⟶ ((x11 x34 ⟶ False) ⟶ False) ⟶ ((x11 x43 ⟶ False) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ ((x11 x37 ⟶ False) ⟶ False) ⟶ ((x11 x31 ⟶ False) ⟶ False) ⟶ ((x82 x39 ⟶ False) ⟶ False) ⟶ ((x82 x34 ⟶ False) ⟶ False) ⟶ ((x82 x33 ⟶ False) ⟶ False) ⟶ ((x82 x31 ⟶ False) ⟶ False) ⟶ ((x18 x48 ⟶ False) ⟶ False) ⟶ ((x18 x28 ⟶ False) ⟶ False) ⟶ ((x18 x46 ⟶ False) ⟶ False) ⟶ ((x18 x54 ⟶ False) ⟶ False) ⟶ ((x59 x26 ⟶ False) ⟶ False) ⟶ ((x3 x38 ⟶ False) ⟶ False) ⟶ ((x3 x39 ⟶ False) ⟶ False) ⟶ ((x3 x36 ⟶ False) ⟶ False) ⟶ ((x3 x24 ⟶ False) ⟶ False) ⟶ ((x3 x53 ⟶ False) ⟶ False) ⟶ ((x78 x44 ⟶ False) ⟶ False) ⟶ ((x78 x45 ⟶ False) ⟶ False) ⟶ ((x78 x29 ⟶ False) ⟶ False) ⟶ ((x65 x24 = x24 ⟶ False) ⟶ False) ⟶ ((x2 = x53 ⟶ False) ⟶ False) ⟶ ((x54 = x71 ⟶ False) ⟶ False) ⟶ False (proof)