Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../98b5b..
PUaeH../28e88..
vout
PrPhD../d570e.. 102.65 bars
TMUmB../de62c.. ownership of a3320.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMaFM../d4f3c.. ownership of 6ad16.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUhE5../92fff.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem a3320.. : ∀ 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 . x57 x59 ⟶ (x59 = x58 ⟶ False) ⟶ x57 x58 ⟶ False) ⟶ (∀ x58 x59 . x0 x58 x59 ⟶ x57 x59 ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ (x58 = x56 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x0 x58 x59 ⟶ x2 x59 (x1 x60) ⟶ x57 x60 ⟶ False) ⟶ (∀ x58 x59 x60 x61 x62 . (x55 x62 ⟶ False) ⟶ x44 x62 ⟶ x54 x62 ⟶ x2 x58 (x45 x62) ⟶ x2 x61 (x45 x62) ⟶ x2 x59 (x45 x62) ⟶ x53 x60 ⟶ x46 x60 (x45 x62) (x45 x62) ⟶ x52 x60 (x45 x62) (x45 x62) ⟶ x2 x60 (x1 (x47 (x45 x62) (x45 x62))) ⟶ x51 x60 x62 ⟶ x48 (x45 x62) (x45 x62) x60 x58 = x58 ⟶ x50 x62 x61 x58 (x48 (x45 x62) (x45 x62) x60 x61) ⟶ (x49 x62 x58 x61 x59 ⟶ False) ⟶ (x50 x62 x59 x58 (x48 (x45 x62) (x45 x62) x60 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x0 x59 x60 ⟶ x2 x60 (x1 x58) ⟶ (x2 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x43 x59 x58 ⟶ (x2 x59 (x1 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x2 x59 (x1 x58) ⟶ (x43 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x58 = x59 ⟶ False) ⟶ x49 x60 x58 x59 (x42 x59 x58 x60) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x58 = x59 ⟶ False) ⟶ (x2 (x42 x59 x58 x60) (x45 x60) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 x62 x63 . (x55 x63 ⟶ False) ⟶ x44 x63 ⟶ x54 x63 ⟶ x2 x58 (x45 x63) ⟶ x2 x62 (x45 x63) ⟶ x2 x59 (x45 x63) ⟶ x2 x61 (x45 x63) ⟶ x2 x60 (x45 x63) ⟶ x49 x63 x58 x62 x59 ⟶ x49 x63 x58 x62 x61 ⟶ x49 x63 x58 x62 x60 ⟶ (x58 = x62 ⟶ False) ⟶ (x49 x63 x59 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x49 x60 x58 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x49 x60 x58 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x49 x60 x58 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x55 x61 ⟶ False) ⟶ x44 x61 ⟶ x54 x61 ⟶ x2 x58 (x45 x61) ⟶ x2 x60 (x45 x61) ⟶ x2 x59 (x45 x61) ⟶ x49 x61 x58 x60 x59 ⟶ (x49 x61 x59 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x55 x61 ⟶ False) ⟶ x44 x61 ⟶ x54 x61 ⟶ x2 x58 (x45 x61) ⟶ x2 x60 (x45 x61) ⟶ x2 x59 (x45 x61) ⟶ x49 x61 x58 x60 x59 ⟶ (x49 x61 x59 x58 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x55 x61 ⟶ False) ⟶ x44 x61 ⟶ x54 x61 ⟶ x2 x58 (x45 x61) ⟶ x2 x60 (x45 x61) ⟶ x2 x59 (x45 x61) ⟶ x49 x61 x58 x60 x59 ⟶ (x49 x61 x60 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x55 x61 ⟶ False) ⟶ x44 x61 ⟶ x54 x61 ⟶ x2 x58 (x45 x61) ⟶ x2 x60 (x45 x61) ⟶ x2 x59 (x45 x61) ⟶ x49 x61 x58 x60 x59 ⟶ (x49 x61 x60 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x55 x61 ⟶ False) ⟶ x44 x61 ⟶ x54 x61 ⟶ x2 x58 (x45 x61) ⟶ x2 x60 (x45 x61) ⟶ x2 x59 (x45 x61) ⟶ x49 x61 x58 x60 x59 ⟶ (x49 x61 x58 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x2 x58 x59 ⟶ (x57 x59 ⟶ False) ⟶ (x0 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x0 x59 x58 ⟶ (x2 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x50 x60 x58 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x55 x60 ⟶ False) ⟶ x44 x60 ⟶ x54 x60 ⟶ x2 x58 (x45 x60) ⟶ x2 x59 (x45 x60) ⟶ (x50 x60 x58 x58 x59 ⟶ False) ⟶ False) ⟶ (x57 x3 ⟶ False) ⟶ (∀ x58 . (x43 x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x57 x61 ⟶ False) ⟶ x53 x58 ⟶ x46 x58 x61 x60 ⟶ x2 x58 (x1 (x47 x61 x60)) ⟶ x2 x59 x61 ⟶ (x48 x61 x60 x58 x59 = x4 x58 x59 ⟶ False) ⟶ False) ⟶ ((x41 x40 ⟶ False) ⟶ False) ⟶ (x57 x40 ⟶ False) ⟶ (∀ x58 x59 . (x53 (x39 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x5 (x39 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x38 (x39 x59 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x6 (x39 x58 x59) ⟶ False) ⟶ False) ⟶ (x37 x36 ⟶ False) ⟶ ((x53 x36 ⟶ False) ⟶ False) ⟶ ((x6 x36 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ x57 (x8 x58) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ (x2 (x8 x58) (x1 (x45 x58)) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ x57 (x10 x58 x59) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ (x53 (x10 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ (x5 (x10 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ (x38 (x10 x58 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ (x6 (x10 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 x59 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ (x2 (x10 x58 x59) (x1 (x47 x59 x58)) ⟶ False) ⟶ False) ⟶ (x57 x11 ⟶ False) ⟶ (∀ x58 . (x52 (x35 x58) x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x46 (x35 x58) x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x34 (x35 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x53 (x35 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x5 (x35 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x38 (x35 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x6 (x35 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x2 (x35 x58) (x1 (x47 x58 x58)) ⟶ False) ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x53 x32 ⟶ False) ⟶ False) ⟶ ((x6 x32 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x55 x58 ⟶ False) ⟶ x9 x58 ⟶ x12 (x13 x58) ⟶ False) ⟶ (∀ x58 . (x55 x58 ⟶ False) ⟶ x9 x58 ⟶ (x2 (x13 x58) (x1 (x45 x58)) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ (x12 (x14 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ x57 (x14 x58) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ (x2 (x14 x58) (x1 (x45 x58)) ⟶ False) ⟶ False) ⟶ ((x57 x31 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x5 (x15 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x38 (x15 x59 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x6 (x15 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x57 (x15 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x2 (x15 x58 x59) (x1 (x47 x59 x58)) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x53 (x30 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x5 (x30 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x38 (x30 x59 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x6 (x30 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x2 (x30 x58 x59) (x1 (x47 x59 x58)) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x46 (x16 x58 x59) x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x53 (x16 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x5 (x16 x58 x59) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x38 (x16 x59 x58) x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x6 (x16 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . (x2 (x16 x58 x59) (x1 (x47 x59 x58)) ⟶ False) ⟶ False) ⟶ ((x53 x17 ⟶ False) ⟶ False) ⟶ ((x6 x17 ⟶ False) ⟶ False) ⟶ (∀ x58 . (x18 x58 ⟶ False) ⟶ x9 x58 ⟶ x19 (x45 x58) ⟶ False) ⟶ (∀ x58 . x18 x58 ⟶ x9 x58 ⟶ (x19 (x45 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . x55 x58 ⟶ x9 x58 ⟶ (x12 (x45 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x55 x58 ⟶ False) ⟶ x9 x58 ⟶ x12 (x45 x58) ⟶ False) ⟶ (∀ x58 . (x7 x58 ⟶ False) ⟶ x9 x58 ⟶ x57 (x45 x58) ⟶ False) ⟶ ((x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x58 . x7 x58 ⟶ x9 x58 ⟶ (x57 (x45 x58) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x41 x60 ⟶ x6 x58 ⟶ x5 x58 x60 ⟶ x53 x58 ⟶ (x53 (x4 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x41 x60 ⟶ x6 x58 ⟶ x5 x58 x60 ⟶ x53 x58 ⟶ (x6 (x4 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x58 . (x2 (x29 x58) x58 ⟶ False) ⟶ False) ⟶ ((x9 x20 ⟶ False) ⟶ False) ⟶ ((x54 x28 ⟶ False) ⟶ False) ⟶ (∀ x58 . x54 x58 ⟶ (x9 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 x61 . (x57 x61 ⟶ False) ⟶ x53 x58 ⟶ x46 x58 x61 x60 ⟶ x2 x58 (x1 (x47 x61 x60)) ⟶ x2 x59 x61 ⟶ (x2 (x48 x61 x60 x58 x59) x60 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x21 x58 x56 ⟶ (x7 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x41 x59 ⟶ x2 x58 (x1 x59) ⟶ (x41 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x7 x58 ⟶ (x21 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 x60 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ x2 x59 (x1 (x47 x60 x58)) ⟶ x53 x59 ⟶ x46 x59 x60 x58 ⟶ (x46 x59 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 x60 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ x2 x59 (x1 (x47 x60 x58)) ⟶ x53 x59 ⟶ x46 x59 x60 x58 ⟶ x57 x59 ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 x60 ⟶ False) ⟶ (x57 x58 ⟶ False) ⟶ x2 x59 (x1 (x47 x60 x58)) ⟶ x53 x59 ⟶ x46 x59 x60 x58 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x41 x59 ⟶ x2 x58 x59 ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x41 x59 ⟶ x2 x58 x59 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x18 x58 ⟶ False) ⟶ x55 x58 ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ (x41 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x55 x58 ⟶ (x18 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x58 x59)) ⟶ x53 x60 ⟶ x33 x60 ⟶ x27 x60 x59 ⟶ (x52 x60 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x58 x59)) ⟶ x53 x60 ⟶ x33 x60 ⟶ x27 x60 x59 ⟶ (x53 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 . x12 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x12 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x12 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x18 x58 ⟶ False) ⟶ x18 x58 ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x18 x58 ⟶ False) ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x59 x58)) ⟶ x53 x60 ⟶ x52 x60 x59 x58 ⟶ (x27 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x59 x58)) ⟶ x53 x60 ⟶ x52 x60 x59 x58 ⟶ (x33 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x59 x58)) ⟶ x53 x60 ⟶ x52 x60 x59 x58 ⟶ (x53 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 . x6 x58 ⟶ x53 x58 ⟶ (x37 x58 ⟶ False) ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x6 x58 ⟶ x53 x58 ⟶ (x37 x58 ⟶ False) ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x6 x58 ⟶ x53 x58 ⟶ (x37 x58 ⟶ False) ⟶ x12 x58 ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x7 x58 ⟶ (x18 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x7 x58 ⟶ (x7 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x57 x60 ⟶ x2 x58 (x1 (x47 x59 x60)) ⟶ (x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x2 x59 (x1 (x47 x58 x58)) ⟶ x46 x59 x58 x58 ⟶ (x34 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x37 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x57 x60 ⟶ x2 x58 (x1 (x47 x60 x59)) ⟶ (x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 x60 ⟶ False) ⟶ x2 x58 (x1 (x47 x59 x60)) ⟶ x46 x58 x59 x60 ⟶ (x34 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x6 x59 ⟶ x53 x59 ⟶ x2 x58 (x1 x59) ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x55 x58 ⟶ False) ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x58 x59)) ⟶ (x5 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x59 x58)) ⟶ (x38 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . (x57 x60 ⟶ False) ⟶ x57 x58 ⟶ x2 x59 (x1 (x47 x60 x58)) ⟶ x34 x59 x60 ⟶ False) ⟶ (∀ x58 x59 x60 . x57 x60 ⟶ x2 x58 (x1 (x47 x60 x59)) ⟶ x46 x58 x60 x59 ⟶ (x34 x58 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x33 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ x6 x58 ⟶ x53 x58 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x7 x58 ⟶ (x55 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x60 (x1 (x47 x58 x59)) ⟶ (x6 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x57 x60 ⟶ x2 x58 (x1 (x47 x60 x59)) ⟶ (x34 x58 x60 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 x60 . x2 x59 (x1 (x47 x60 x58)) ⟶ x34 x59 x60 ⟶ (x46 x59 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x57 x58 ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x55 x58 ⟶ False) ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x21 x58 x3 ⟶ (x55 x58 ⟶ False) ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ x21 x58 x3 ⟶ x7 x58 ⟶ False) ⟶ (∀ x58 . x9 x58 ⟶ (x7 x58 ⟶ False) ⟶ x55 x58 ⟶ (x21 x58 x3 ⟶ False) ⟶ False) ⟶ (∀ x58 x59 . x0 x58 x59 ⟶ x0 x59 x58 ⟶ False) ⟶ (x50 x22 x25 x23 (x48 (x45 x22) (x45 x22) x24 x25) ⟶ False) ⟶ (x26 = x23 ⟶ False) ⟶ ((x50 x22 x26 x23 (x48 (x45 x22) (x45 x22) x24 x26) ⟶ False) ⟶ False) ⟶ ((x48 (x45 x22) (x45 x22) x24 x23 = x23 ⟶ False) ⟶ False) ⟶ ((x51 x24 x22 ⟶ False) ⟶ False) ⟶ ((x2 x24 (x1 (x47 (x45 x22) (x45 x22))) ⟶ False) ⟶ False) ⟶ ((x52 x24 (x45 x22) (x45 x22) ⟶ False) ⟶ False) ⟶ ((x46 x24 (x45 x22) (x45 x22) ⟶ False) ⟶ False) ⟶ ((x53 x24 ⟶ False) ⟶ False) ⟶ ((x2 x25 (x45 x22) ⟶ False) ⟶ False) ⟶ ((x2 x26 (x45 x22) ⟶ False) ⟶ False) ⟶ ((x2 x23 (x45 x22) ⟶ False) ⟶ False) ⟶ ((x54 x22 ⟶ False) ⟶ False) ⟶ ((x44 x22 ⟶ False) ⟶ False) ⟶ (x55 x22 ⟶ False) ⟶ False (proof)