Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../5bf8f..
PUZbw../0ac47..
vout
PrPhD../ca920.. 3.39 bars
TMG47../5f705.. ownership of 75510.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMKNJ../9e39e.. ownership of 1ec6a.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUJsG../7edcc.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 75510.. : ∀ 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 . x55 x57 ⟶ (x57 = x56 ⟶ False) ⟶ x55 x56 ⟶ False) ⟶ (∀ x56 x57 . x0 x56 x57 ⟶ x55 x57 ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ x53 x58 ⟶ x54 x58 ⟶ x0 x58 (x51 x56 x57 x59) ⟶ (x52 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ x54 x58 ⟶ x48 x58 (x49 (x50 x56 x57)) ⟶ x0 x58 (x51 x56 x57 x59) ⟶ (x1 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x56 = x47 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ x0 x58 (x51 x56 x57 x59) ⟶ (x48 x58 (x49 (x50 x56 x57)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ x0 x58 (x51 x56 x57 x59) ⟶ (x54 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x0 x56 x57 ⟶ x48 x57 (x49 x58) ⟶ x55 x58 ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ x53 x58 ⟶ x54 x58 ⟶ x52 x60 x58 ⟶ x46 x56 x57 x59 x60 ⟶ (x52 x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x0 x57 x58 ⟶ x48 x58 (x49 x56) ⟶ (x48 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x45 x57 x56 ⟶ (x48 x57 (x49 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x48 x57 (x49 x56) ⟶ (x45 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x48 x56 x57 ⟶ (x55 x57 ⟶ False) ⟶ (x0 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 x56 ⟶ (x48 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 ⟶ x54 x57 ⟶ x53 x56 ⟶ x54 x56 ⟶ x52 x57 x56 ⟶ (x52 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x45 x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57)) ⟶ (x46 x56 x57 x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 ⟶ x54 x57 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x52 x57 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x48 x59 (x49 (x50 x58 x57)) ⟶ x45 x59 x56 ⟶ (x46 x58 x57 x59 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x48 x59 (x49 (x50 x58 x57)) ⟶ x46 x58 x57 x59 x56 ⟶ (x45 x59 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x54 (x44 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x2 (x44 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x43 (x44 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x53 (x44 x56) ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ (x55 x41 ⟶ False) ⟶ (∀ x56 . (x40 x56 ⟶ False) ⟶ x40 (x39 x56) ⟶ False) ⟶ (∀ x56 . (x40 x56 ⟶ False) ⟶ (x48 (x39 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x54 (x38 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x3 (x38 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x38 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x38 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x40 (x37 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ x55 (x37 x56) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x48 (x37 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ (x4 x5 ⟶ False) ⟶ ((x54 x5 ⟶ False) ⟶ False) ⟶ ((x53 x5 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x35 (x36 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x48 (x36 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ ((x54 x34 ⟶ False) ⟶ False) ⟶ ((x43 x34 ⟶ False) ⟶ False) ⟶ ((x53 x34 ⟶ False) ⟶ False) ⟶ (x55 x34 ⟶ False) ⟶ (∀ x56 . x35 (x33 x56) x56 ⟶ False) ⟶ (∀ x56 . (x48 (x33 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x3 (x32 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x32 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x32 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x55 (x6 x56 x57) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x54 (x6 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x3 (x6 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x2 (x6 x56 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x53 (x6 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x48 (x6 x56 x57) (x49 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ ((x54 x7 ⟶ False) ⟶ False) ⟶ ((x43 x7 ⟶ False) ⟶ False) ⟶ ((x53 x7 ⟶ False) ⟶ False) ⟶ (x55 x31 ⟶ False) ⟶ (∀ x56 . (x55 (x8 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x48 (x8 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ ((x43 x9 ⟶ False) ⟶ False) ⟶ ((x53 x9 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x54 x11 ⟶ False) ⟶ False) ⟶ ((x53 x11 ⟶ False) ⟶ False) ⟶ ((x55 x30 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ x55 (x12 x56) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x48 (x12 x56) (x49 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x3 (x13 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x13 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x13 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 (x13 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x48 (x13 x56 x57) (x49 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ ((x53 x29 ⟶ False) ⟶ False) ⟶ (x55 x29 ⟶ False) ⟶ (∀ x56 x57 . (x54 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x3 (x28 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x28 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x48 (x28 x56 x57) (x49 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x14 (x15 x56 x57) x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x54 (x15 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x3 (x15 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x15 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x15 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x48 (x15 x56 x57) (x49 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ ((x54 x16 ⟶ False) ⟶ False) ⟶ ((x53 x16 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x53 (x50 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ x55 x56 ⟶ x54 x57 ⟶ x48 x57 (x49 (x50 x58 x56)) ⟶ (x55 (x51 x58 x56 x57) ⟶ False) ⟶ False) ⟶ ((x55 x47 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 (x49 x56) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x55 (x50 x57 x56) ⟶ False) ⟶ (∀ x56 . (x48 (x27 x56) x56 ⟶ False) ⟶ False) ⟶ ((x55 x17 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ (x52 x59 (x26 x58 x59 x57 x56) ⟶ False) ⟶ (x0 (x25 x58 x59 x57 x56) x58 ⟶ False) ⟶ (x58 = x51 x56 x57 x59 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ (x1 (x26 x58 x59 x57 x56) x56 ⟶ False) ⟶ (x0 (x25 x58 x59 x57 x56) x58 ⟶ False) ⟶ (x58 = x51 x56 x57 x59 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ (x26 x58 x59 x57 x56 = x25 x58 x59 x57 x56 ⟶ False) ⟶ (x0 (x25 x58 x59 x57 x56) x58 ⟶ False) ⟶ (x58 = x51 x56 x57 x59 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ (x48 (x26 x58 x59 x57 x56) (x49 (x50 x56 x57)) ⟶ False) ⟶ (x0 (x25 x58 x59 x57 x56) x58 ⟶ False) ⟶ (x58 = x51 x56 x57 x59 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x54 x59 ⟶ x48 x59 (x49 (x50 x56 x57)) ⟶ (x54 (x26 x58 x59 x57 x56) ⟶ False) ⟶ (x0 (x25 x58 x59 x57 x56) x58 ⟶ False) ⟶ (x58 = x51 x56 x57 x59 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x0 (x25 x59 x60 x57 x56) x59 ⟶ x54 x58 ⟶ x48 x58 (x49 (x50 x56 x57)) ⟶ x58 = x25 x59 x60 x57 x56 ⟶ x1 x58 x56 ⟶ x52 x60 x58 ⟶ (x59 = x51 x56 x57 x60 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 x61 . x54 x61 ⟶ x48 x61 (x49 (x50 x56 x57)) ⟶ x60 = x51 x56 x57 x61 ⟶ x54 x58 ⟶ x48 x58 (x49 (x50 x56 x57)) ⟶ x58 = x59 ⟶ x1 x58 x56 ⟶ x52 x61 x58 ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x59 = x51 x56 x57 x60 ⟶ x0 x58 x59 ⟶ (x52 x60 (x18 x58 x59 x60 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x59 = x51 x56 x57 x60 ⟶ x0 x58 x59 ⟶ (x1 (x18 x58 x59 x60 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x59 = x51 x56 x57 x60 ⟶ x0 x58 x59 ⟶ (x18 x58 x59 x60 x57 x56 = x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x59 = x51 x56 x57 x60 ⟶ x0 x58 x59 ⟶ (x48 (x18 x58 x59 x60 x57 x56) (x49 (x50 x56 x57)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 x60 . x54 x60 ⟶ x48 x60 (x49 (x50 x56 x57)) ⟶ x59 = x51 x56 x57 x60 ⟶ x0 x58 x59 ⟶ (x54 (x18 x58 x59 x60 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 (x24 x56 x57) x56 ⟶ (x45 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x0 (x24 x56 x57) x57 ⟶ False) ⟶ (x45 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x45 x57 x58 ⟶ x0 x56 x57 ⟶ (x0 x56 x58 ⟶ False) ⟶ False) ⟶ ((x47 = x17 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x42 x57 ⟶ x48 x56 (x49 x57) ⟶ (x42 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x3 x56 x57 ⟶ (x3 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x3 x56 x57 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x3 x56 x57 ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x42 x57 ⟶ x48 x56 x57 ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x42 x57 ⟶ x48 x56 x57 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x2 x56 x57 ⟶ (x2 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x2 x56 x57 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x53 x56 ⟶ x2 x56 x57 ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x42 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x53 x58 ⟶ x3 x58 x56 ⟶ x48 x57 (x49 x58) ⟶ (x3 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x40 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x4 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x40 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x40 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x40 x57 ⟶ x48 x56 (x49 x57) ⟶ (x40 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x53 x58 ⟶ x2 x58 x56 ⟶ x48 x57 (x49 x58) ⟶ (x2 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x53 x56 ⟶ x54 x56 ⟶ (x4 x56 ⟶ False) ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x53 x56 ⟶ x54 x56 ⟶ (x4 x56 ⟶ False) ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x53 x56 ⟶ x54 x56 ⟶ (x4 x56 ⟶ False) ⟶ x40 x56 ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x48 x56 (x49 x57) ⟶ x35 x56 x57 ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x48 x56 (x49 (x50 x57 x58)) ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ (x43 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x48 x57 (x49 (x50 x56 x56)) ⟶ x14 x57 x56 x56 ⟶ (x1 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x4 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x48 x56 (x49 x57) ⟶ x55 x56 ⟶ (x35 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x48 x56 (x49 (x50 x58 x57)) ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ (x19 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ x48 x56 (x49 (x50 x57 x58)) ⟶ x14 x56 x57 x58 ⟶ (x1 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 ⟶ x54 x57 ⟶ x48 x56 (x49 x57) ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x48 x56 (x49 x57) ⟶ (x35 x56 x57 ⟶ False) ⟶ x55 x56 ⟶ False) ⟶ (∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57)) ⟶ (x3 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x48 x58 (x49 (x50 x57 x56)) ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 ⟶ x48 x56 (x49 x57) ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ x55 x56 ⟶ x48 x57 (x49 (x50 x58 x56)) ⟶ x1 x57 x58 ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x48 x56 (x49 (x50 x58 x57)) ⟶ x14 x56 x58 x57 ⟶ (x1 x56 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x10 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x53 x56 ⟶ x54 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ x48 x56 (x49 x57) ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57)) ⟶ (x53 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x53 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x48 x56 (x49 (x50 x58 x57)) ⟶ (x1 x56 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x48 x57 (x49 (x50 x58 x56)) ⟶ x1 x57 x58 ⟶ (x14 x57 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x54 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x56 x57 ⟶ x0 x57 x56 ⟶ False) ⟶ (x45 (x51 x20 x21 x23) (x51 x20 x21 x22) ⟶ False) ⟶ ((x46 x20 x21 x22 x23 ⟶ False) ⟶ False) ⟶ ((x48 x22 (x49 (x50 x20 x21)) ⟶ False) ⟶ False) ⟶ ((x54 x22 ⟶ False) ⟶ False) ⟶ ((x48 x23 (x49 (x50 x20 x21)) ⟶ False) ⟶ False) ⟶ ((x54 x23 ⟶ False) ⟶ False) ⟶ False (proof)