Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../6a7ab..
PUgde../7edce..
vout
PrPhD../554d9.. 102.64 bars
TMHq7../3792b.. ownership of 3a9bd.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMdBD../c8e0a.. ownership of 37e8e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUZwC../aef24.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 3a9bd.. : ∀ 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 . x58 x60 ⟶ (x60 = x59 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x58 x60 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x59 = x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x59 x60 ⟶ x2 x60 (x1 x61) ⟶ x58 x61 ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x60 x61 ⟶ x2 x61 (x1 x59) ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x3 x60 x59 ⟶ (x2 x60 (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x59) ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x60 x61 ⟶ x0 x59 x61 ⟶ x0 x59 (x4 x61 x60) ⟶ False) ⟶ (∀ x59 x60 . x0 x60 x59 ⟶ (x0 (x4 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x59 x60 ⟶ (x58 x60 ⟶ False) ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x60 x59 ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ x10 x60 x59 (x9 x59 x60) = x8 x60 x59 (x9 x59 x60) ⟶ (x7 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ x10 x60 x59 (x9 x59 x60) = x8 x60 x59 (x9 x59 x60) ⟶ (x56 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x2 (x9 x59 x60) (x13 x60) ⟶ False) ⟶ (x7 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x2 (x9 x59 x60) (x13 x60) ⟶ False) ⟶ (x56 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x7 x60 x61 ⟶ x56 x60 x61 ⟶ x7 x60 x61 ⟶ x2 x59 (x13 x61) ⟶ (x10 x61 x60 x59 = x8 x61 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 . (x5 x63 ⟶ False) ⟶ x12 x63 ⟶ x6 x63 ⟶ x11 x63 ⟶ x2 x62 (x13 x63) ⟶ x7 x59 x63 ⟶ x2 x61 (x13 x63) ⟶ x60 = x54 x63 x61 x62 ⟶ x55 x59 x61 ⟶ (x0 x60 (x8 x63 x59 x62) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x8 x62 x59 x61) ⟶ (x55 x59 (x14 x59 x61 x62 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x8 x62 x59 x61) ⟶ (x60 = x54 x62 (x14 x59 x61 x62 x60) x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x8 x62 x59 x61) ⟶ (x2 (x14 x59 x61 x62 x60) (x13 x62) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 . (x5 x63 ⟶ False) ⟶ x12 x63 ⟶ x6 x63 ⟶ x11 x63 ⟶ x2 x62 (x13 x63) ⟶ x7 x59 x63 ⟶ x2 x61 (x13 x63) ⟶ x60 = x54 x63 x62 x61 ⟶ x55 x59 x61 ⟶ (x0 x60 (x10 x63 x59 x62) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x10 x62 x59 x61) ⟶ (x55 x59 (x15 x59 x61 x62 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x10 x62 x59 x61) ⟶ (x60 = x54 x62 x61 (x15 x59 x61 x62 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x12 x62 ⟶ x6 x62 ⟶ x11 x62 ⟶ x2 x61 (x13 x62) ⟶ x7 x59 x62 ⟶ x0 x60 (x10 x62 x59 x61) ⟶ (x2 (x15 x59 x61 x62 x60) (x13 x62) ⟶ False) ⟶ False) ⟶ (x58 x53 ⟶ False) ⟶ (∀ x59 . (x3 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 x60 ⟶ (x52 x60 x59 = x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ x58 (x16 x59) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ (x2 (x16 x59) (x1 (x13 x59)) ⟶ False) ⟶ False) ⟶ (x58 x18 ⟶ False) ⟶ (∀ x59 . (x50 x59 ⟶ False) ⟶ x17 x59 ⟶ x49 (x48 x59) ⟶ False) ⟶ (∀ x59 . (x50 x59 ⟶ False) ⟶ x17 x59 ⟶ (x2 (x48 x59) (x1 (x13 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ (x49 (x47 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ x58 (x47 x59) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ (x2 (x47 x59) (x1 (x13 x59)) ⟶ False) ⟶ False) ⟶ ((x58 x19 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x2 x59 (x13 x60) ⟶ (x46 x60 (x46 x60 x59) = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 x64 . (x5 x64 ⟶ False) ⟶ x11 x64 ⟶ x2 x63 (x1 (x13 x64)) ⟶ x2 x59 (x1 (x13 x64)) ⟶ x2 x62 (x13 x64) ⟶ x2 x60 (x13 x64) ⟶ x61 = x54 x64 x62 x60 ⟶ x0 x62 x63 ⟶ x0 x60 x59 ⟶ (x0 x61 (x20 x64 x63 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x11 x62 ⟶ x2 x61 (x1 (x13 x62)) ⟶ x2 x59 (x1 (x13 x62)) ⟶ x0 x60 (x20 x62 x61 x59) ⟶ (x0 (x45 x59 x61 x62 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x11 x62 ⟶ x2 x61 (x1 (x13 x62)) ⟶ x2 x59 (x1 (x13 x62)) ⟶ x0 x60 (x20 x62 x61 x59) ⟶ (x0 (x21 x59 x61 x62 x60) x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x11 x62 ⟶ x2 x61 (x1 (x13 x62)) ⟶ x2 x59 (x1 (x13 x62)) ⟶ x0 x60 (x20 x62 x61 x59) ⟶ (x60 = x54 x62 (x21 x59 x61 x62 x60) (x45 x59 x61 x62 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x11 x62 ⟶ x2 x61 (x1 (x13 x62)) ⟶ x2 x59 (x1 (x13 x62)) ⟶ x0 x60 (x20 x62 x61 x59) ⟶ (x2 (x45 x59 x61 x62 x60) (x13 x62) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x5 x62 ⟶ False) ⟶ x11 x62 ⟶ x2 x61 (x1 (x13 x62)) ⟶ x2 x59 (x1 (x13 x62)) ⟶ x0 x60 (x20 x62 x61 x59) ⟶ (x2 (x21 x59 x61 x62 x60) (x13 x62) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x22 x59 ⟶ False) ⟶ x17 x59 ⟶ x23 (x13 x59) ⟶ False) ⟶ (∀ x59 . x22 x59 ⟶ x17 x59 ⟶ (x23 (x13 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x17 x59 ⟶ (x49 (x13 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x50 x59 ⟶ False) ⟶ x17 x59 ⟶ x49 (x13 x59) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x12 x59 ⟶ x6 x59 ⟶ x11 x59 ⟶ x24 (x25 x59) x59 ⟶ False) ⟶ (∀ x59 . x58 (x51 x59) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x17 x59 ⟶ x58 (x13 x59) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x5 x59 ⟶ x17 x59 ⟶ (x58 (x13 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x44 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x5 x59 ⟶ False) ⟶ x12 x59 ⟶ x11 x59 ⟶ (x7 (x26 x59) x59 ⟶ False) ⟶ False) ⟶ ((x11 x43 ⟶ False) ⟶ False) ⟶ ((x17 x27 ⟶ False) ⟶ False) ⟶ ((x58 x42 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x11 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x12 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ x5 x59 ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x17 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x2 (x28 x60 x59) (x1 (x13 x60)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 x60 ⟶ (x2 (x52 x60 x59) (x1 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x11 x61 ⟶ x2 x59 (x13 x61) ⟶ x2 x60 (x13 x61) ⟶ (x2 (x54 x61 x59 x60) (x13 x61) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x2 (x41 x61 x60 x59) (x1 (x13 x61)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x2 (x29 x61 x60 x59) (x1 (x13 x61)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x1 (x13 x61)) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x2 (x40 x61 x60 x59) (x1 (x13 x61)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x2 x59 (x13 x60) ⟶ (x2 (x46 x60 x59) (x13 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x2 (x25 x59) (x13 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x7 x60 x61 ⟶ x2 x59 (x13 x61) ⟶ (x2 (x8 x61 x60 x59) (x1 (x13 x61)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x7 x60 x61 ⟶ x2 x59 (x13 x61) ⟶ (x2 (x10 x61 x60 x59) (x1 (x13 x61)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x28 x60 x59 = x13 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x13 x61) ⟶ x54 x61 x60 x59 = x25 x61 ⟶ x54 x61 x59 x60 = x25 x61 ⟶ (x59 = x46 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x13 x61) ⟶ x59 = x46 x61 x60 ⟶ (x54 x61 x59 x60 = x25 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x13 x61) ⟶ x59 = x46 x61 x60 ⟶ (x54 x61 x60 x59 = x25 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x41 x61 x60 x59 = x40 x61 x59 (x52 (x13 x61) x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x11 x60 ⟶ x38 x60 ⟶ x2 x59 (x13 x60) ⟶ x54 x60 (x39 x59 x60) x59 = x39 x59 x60 ⟶ x54 x60 x59 (x39 x59 x60) = x39 x59 x60 ⟶ (x59 = x25 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x11 x60 ⟶ x38 x60 ⟶ x2 x59 (x13 x60) ⟶ (x2 (x39 x59 x60) (x13 x60) ⟶ False) ⟶ (x59 = x25 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x11 x61 ⟶ x38 x61 ⟶ x2 x60 (x13 x61) ⟶ x60 = x25 x61 ⟶ x2 x59 (x13 x61) ⟶ (x54 x61 x60 x59 = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x11 x61 ⟶ x38 x61 ⟶ x2 x60 (x13 x61) ⟶ x60 = x25 x61 ⟶ x2 x59 (x13 x61) ⟶ (x54 x61 x59 x60 = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x13 x61) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x29 x61 x60 x59 = x40 x61 (x52 (x13 x61) x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ x54 x59 (x54 x59 (x32 x59) (x30 x59)) (x31 x59) = x54 x59 (x32 x59) (x54 x59 (x30 x59) (x31 x59)) ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x2 (x31 x59) (x13 x59) ⟶ False) ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x2 (x30 x59) (x13 x59) ⟶ False) ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x2 (x32 x59) (x13 x59) ⟶ False) ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . x11 x62 ⟶ x6 x62 ⟶ x2 x61 (x13 x62) ⟶ x2 x59 (x13 x62) ⟶ x2 x60 (x13 x62) ⟶ (x54 x62 (x54 x62 x61 x59) x60 = x54 x62 x61 (x54 x62 x59 x60) ⟶ False) ⟶ False) ⟶ ((x57 = x42 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x11 x61 ⟶ x2 x60 (x1 (x13 x61)) ⟶ x2 x59 (x1 (x13 x61)) ⟶ (x40 x61 x60 x59 = x20 x61 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x7 x60 x61 ⟶ x2 x59 (x13 x61) ⟶ (x8 x61 x60 x59 = x41 x61 x59 (x28 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x5 x61 ⟶ False) ⟶ x12 x61 ⟶ x6 x61 ⟶ x11 x61 ⟶ x7 x60 x61 ⟶ x2 x59 (x13 x61) ⟶ (x10 x61 x60 x59 = x29 x61 x59 (x28 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x37 x59 x57 ⟶ (x5 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x5 x59 ⟶ (x37 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x22 x59 ⟶ False) ⟶ x50 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x50 x59 ⟶ (x22 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x22 x59 ⟶ False) ⟶ x22 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x22 x59 ⟶ False) ⟶ x5 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x5 x59 ⟶ (x22 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x5 x59 ⟶ (x5 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x22 x60 ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x22 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x50 x59 ⟶ False) ⟶ x5 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x5 x59 ⟶ (x50 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x5 x60 ⟶ False) ⟶ x12 x60 ⟶ x6 x60 ⟶ x11 x60 ⟶ x7 x59 x60 ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ x12 x59 ⟶ (x38 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x50 x59 ⟶ False) ⟶ x5 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x37 x59 x53 ⟶ (x50 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x37 x59 x53 ⟶ x5 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ (x5 x59 ⟶ False) ⟶ x50 x59 ⟶ (x37 x59 x53 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x0 x60 x59 ⟶ False) ⟶ (x55 x36 (x54 x33 (x54 x33 x35 x34) (x46 x33 x35)) ⟶ False) ⟶ ((x55 x36 x34 ⟶ False) ⟶ False) ⟶ ((x7 x36 x33 ⟶ False) ⟶ False) ⟶ ((x56 x36 x33 ⟶ False) ⟶ False) ⟶ ((x2 x34 (x13 x33) ⟶ False) ⟶ False) ⟶ ((x2 x35 (x13 x33) ⟶ False) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ ((x6 x33 ⟶ False) ⟶ False) ⟶ ((x12 x33 ⟶ False) ⟶ False) ⟶ (x5 x33 ⟶ False) ⟶ False (proof)