Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../ee064..
PUTjN../b9161..
vout
PrPhD../fc6dc.. 3.41 bars
TMTV9../232b4.. ownership of 716c9.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMQo9../54ee7.. ownership of 546ab.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUXtc../71e59.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 716c9.. : ∀ 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 . x56 x58 ⟶ (x58 = x57 ⟶ False) ⟶ x56 x57 ⟶ False) ⟶ (∀ x57 x58 x59 x60 . x2 (x1 x60 x59) (x0 x58 x57) ⟶ (x2 (x1 x59 x60) (x0 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x57 x58 ⟶ x56 x58 ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x57 = x3 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x57 x58 ⟶ x54 x58 (x55 x59) ⟶ x56 x59 ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x58 x59 ⟶ x54 x59 (x55 x57) ⟶ (x54 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x53 x58 x57 ⟶ (x54 x58 (x55 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x54 x58 (x55 x57) ⟶ (x53 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x54 x57 x58 ⟶ (x56 x58 ⟶ False) ⟶ (x2 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 x57 ⟶ (x54 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x53 x57 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x4 (x5 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x52 (x5 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x6 (x5 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x51 (x5 x57) ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ (x56 x8 ⟶ False) ⟶ (∀ x57 x58 . (x4 (x9 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x50 (x9 x57 x58) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x52 (x9 x58 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x51 (x9 x57 x58) ⟶ False) ⟶ False) ⟶ (x10 x11 ⟶ False) ⟶ ((x4 x11 ⟶ False) ⟶ False) ⟶ ((x51 x11 ⟶ False) ⟶ False) ⟶ ((x4 x49 ⟶ False) ⟶ False) ⟶ ((x6 x49 ⟶ False) ⟶ False) ⟶ ((x51 x49 ⟶ False) ⟶ False) ⟶ (x56 x49 ⟶ False) ⟶ (∀ x57 x58 . (x50 (x48 x57 x58) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x52 (x48 x58 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x51 (x48 x57 x58) ⟶ False) ⟶ False) ⟶ ((x4 x12 ⟶ False) ⟶ False) ⟶ ((x6 x12 ⟶ False) ⟶ False) ⟶ ((x51 x12 ⟶ False) ⟶ False) ⟶ (x47 x46 ⟶ False) ⟶ (x56 x13 ⟶ False) ⟶ ((x6 x45 ⟶ False) ⟶ False) ⟶ ((x51 x45 ⟶ False) ⟶ False) ⟶ ((x44 x43 ⟶ False) ⟶ False) ⟶ ((x4 x43 ⟶ False) ⟶ False) ⟶ ((x51 x43 ⟶ False) ⟶ False) ⟶ (x56 x14 ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ ((x4 x14 ⟶ False) ⟶ False) ⟶ ((x51 x14 ⟶ False) ⟶ False) ⟶ ((x47 x15 ⟶ False) ⟶ False) ⟶ (x56 x15 ⟶ False) ⟶ ((x56 x16 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x50 (x42 x57 x58) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x52 (x42 x58 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x51 (x42 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 (x42 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x54 (x42 x57 x58) (x55 (x0 x58 x57)) ⟶ False) ⟶ False) ⟶ ((x51 x17 ⟶ False) ⟶ False) ⟶ (x56 x17 ⟶ False) ⟶ ((x4 x18 ⟶ False) ⟶ False) ⟶ ((x51 x18 ⟶ False) ⟶ False) ⟶ ((x19 x20 ⟶ False) ⟶ False) ⟶ ((x4 x20 ⟶ False) ⟶ False) ⟶ ((x51 x20 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . x54 x60 (x55 (x0 (x0 x58 x57) x59)) ⟶ (x51 (x41 x60) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x56 x57 ⟶ False) ⟶ x51 x57 ⟶ x56 (x41 x57) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x19 x58 ⟶ (x4 (x40 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x19 x58 ⟶ (x51 (x40 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . (x51 (x39 (x1 x58 x57) (x1 x60 x59)) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x51 (x0 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x51 (x38 (x1 x58 x57)) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ (x56 (x0 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ (x56 (x0 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 (x39 x57 x58) ⟶ False) ⟶ (∀ x57 . (x47 (x38 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 (x38 x57) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x51 x57 ⟶ (x47 (x41 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 (x1 x57 x58) ⟶ False) ⟶ ((x56 x3 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x4 (x38 (x1 x58 x57)) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x37 x58 ⟶ x4 x58 ⟶ (x56 (x40 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x47 x57 ⟶ False) ⟶ x51 x57 ⟶ x4 x57 ⟶ x47 (x41 x57) ⟶ False) ⟶ (∀ x57 x58 x59 . x7 x59 ⟶ x51 x57 ⟶ x50 x57 x59 ⟶ x4 x57 ⟶ (x4 (x40 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x7 x59 ⟶ x51 x57 ⟶ x50 x57 x59 ⟶ x4 x57 ⟶ (x51 (x40 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x7 (x39 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x7 (x38 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ x51 x58 ⟶ x6 x58 ⟶ x4 x58 ⟶ x54 x57 (x41 x58) ⟶ x56 (x40 x58 x57) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x56 (x41 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x54 (x36 x57) x57 ⟶ False) ⟶ False) ⟶ ((x56 x21 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x4 (x35 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x51 (x35 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x1 x58 x57 = x39 (x39 x58 x57) (x38 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 (x22 x57 x58) x57 ⟶ (x53 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x2 (x22 x57 x58) x58 ⟶ False) ⟶ (x53 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x53 x58 x59 ⟶ x2 x57 x58 ⟶ (x2 x57 x59 ⟶ False) ⟶ False) ⟶ ((x3 = x21 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x2 (x1 (x23 x57 x58) (x24 x57 x58)) (x41 x58) ⟶ False) ⟶ (x2 (x28 x57 x58) (x41 x57) ⟶ False) ⟶ x25 x57 (x26 x57 x58) (x27 x57 x58) = x25 x58 (x27 x57 x58) (x26 x57 x58) ⟶ (x57 = x35 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x2 (x1 (x23 x57 x58) (x24 x57 x58)) (x41 x58) ⟶ False) ⟶ (x2 (x28 x57 x58) (x41 x57) ⟶ False) ⟶ (x2 (x1 (x27 x57 x58) (x26 x57 x58)) (x41 x58) ⟶ False) ⟶ (x57 = x35 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x28 x57 x58 = x1 (x24 x57 x58) (x23 x57 x58) ⟶ False) ⟶ (x2 (x28 x57 x58) (x41 x57) ⟶ False) ⟶ x25 x57 (x26 x57 x58) (x27 x57 x58) = x25 x58 (x27 x57 x58) (x26 x57 x58) ⟶ (x57 = x35 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x28 x57 x58 = x1 (x24 x57 x58) (x23 x57 x58) ⟶ False) ⟶ (x2 (x28 x57 x58) (x41 x57) ⟶ False) ⟶ (x2 (x1 (x27 x57 x58) (x26 x57 x58)) (x41 x58) ⟶ False) ⟶ (x57 = x35 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . x51 x60 ⟶ x4 x60 ⟶ x51 x59 ⟶ x4 x59 ⟶ x2 (x28 x59 x60) (x41 x59) ⟶ x28 x59 x60 = x1 x57 x58 ⟶ x2 (x1 x58 x57) (x41 x60) ⟶ x25 x59 (x26 x59 x60) (x27 x59 x60) = x25 x60 (x27 x59 x60) (x26 x59 x60) ⟶ (x59 = x35 x60 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . x51 x60 ⟶ x4 x60 ⟶ x51 x59 ⟶ x4 x59 ⟶ x2 (x28 x59 x60) (x41 x59) ⟶ x28 x59 x60 = x1 x57 x58 ⟶ x2 (x1 x58 x57) (x41 x60) ⟶ (x2 (x1 (x27 x59 x60) (x26 x59 x60)) (x41 x60) ⟶ False) ⟶ (x59 = x35 x60 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . x51 x60 ⟶ x4 x60 ⟶ x51 x59 ⟶ x4 x59 ⟶ x59 = x35 x60 ⟶ x2 (x1 x57 x58) (x41 x60) ⟶ (x25 x59 x58 x57 = x25 x60 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 x61 . x51 x61 ⟶ x4 x61 ⟶ x51 x60 ⟶ x4 x60 ⟶ x60 = x35 x61 ⟶ x57 = x1 x59 x58 ⟶ x2 (x1 x58 x59) (x41 x61) ⟶ (x2 x57 (x41 x60) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x51 x59 ⟶ x4 x59 ⟶ x51 x58 ⟶ x4 x58 ⟶ x58 = x35 x59 ⟶ x2 x57 (x41 x58) ⟶ (x2 (x1 (x30 x57 x58 x59) (x29 x57 x58 x59)) (x41 x59) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x51 x59 ⟶ x4 x59 ⟶ x51 x58 ⟶ x4 x58 ⟶ x58 = x35 x59 ⟶ x2 x57 (x41 x58) ⟶ (x57 = x1 (x29 x57 x58 x59) (x30 x57 x58 x59) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x51 x59 ⟶ x4 x59 ⟶ (x25 x59 x57 x58 = x40 x59 (x1 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x39 x58 x57 = x39 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x54 x57 (x55 x58) ⟶ (x7 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ (x50 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ (x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x54 x57 x58 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x54 x57 x58 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x52 x57 x58 ⟶ (x52 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x52 x57 x58 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x51 x57 ⟶ x52 x57 x58 ⟶ (x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x7 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x51 x59 ⟶ x50 x59 x57 ⟶ x54 x58 (x55 x59) ⟶ (x50 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x10 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x51 x59 ⟶ x52 x59 x57 ⟶ x54 x58 (x55 x59) ⟶ (x52 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x10 x57 ⟶ False) ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x10 x57 ⟶ False) ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ (x10 x57 ⟶ False) ⟶ x47 x57 ⟶ False) ⟶ (∀ x57 x58 x59 . x56 x59 ⟶ x54 x57 (x55 (x0 x58 x59)) ⟶ (x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x10 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x56 x59 ⟶ x54 x57 (x55 (x0 x59 x58)) ⟶ (x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ (x37 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x4 x58 ⟶ x54 x57 (x55 x58) ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x56 x57 ⟶ (x19 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x56 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x56 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x47 x57 ⟶ False) ⟶ x56 x57 ⟶ False) ⟶ (∀ x57 x58 x59 . x54 x59 (x55 (x0 x57 x58)) ⟶ (x50 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x54 x59 (x55 (x0 x58 x57)) ⟶ (x52 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x51 x58 ⟶ x54 x57 (x55 x58) ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x44 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ x51 x57 ⟶ x4 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x19 x57 ⟶ (x31 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x19 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x51 x57 ⟶ x4 x57 ⟶ x19 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x47 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x54 x59 (x55 (x0 x57 x58)) ⟶ (x51 x59 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ x4 x57 ⟶ (x19 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ x4 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x7 x58 ⟶ x51 x57 ⟶ x50 x57 x58 ⟶ x4 x57 ⟶ (x51 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x57 x58 ⟶ x2 x58 x57 ⟶ False) ⟶ (x53 (x41 (x35 x32)) (x0 x33 x34) ⟶ False) ⟶ ((x53 (x41 x32) (x0 x34 x33) ⟶ False) ⟶ False) ⟶ ((x4 x32 ⟶ False) ⟶ False) ⟶ ((x51 x32 ⟶ False) ⟶ False) ⟶ False (proof)