Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../cb4ff..
PUToQ../bd591..
vout
PrPhD../3a01d.. 3.41 bars
TMFyU../70cd1.. ownership of 21ac2.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMQYx../2ab9c.. ownership of 6cb5a.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUZJr../19c01.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 21ac2.. : ∀ 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 . x55 x56 ⟶ (x56 = x54 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x0 x56 x57 ⟶ x2 x57 (x1 x58) ⟶ x55 x58 ⟶ False) ⟶ (∀ x56 x57 x58 . x0 x57 x58 ⟶ x2 x58 (x1 x56) ⟶ (x2 x57 x56 ⟶ False) ⟶ False) ⟶ ((x4 = x3 x54 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 x56 ⟶ (x2 x57 (x1 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x2 x57 (x1 x56) ⟶ (x53 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x0 x57 x58 ⟶ x0 x56 x58 ⟶ x0 x56 (x52 x58 x57) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 x56 ⟶ (x0 (x52 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x2 x56 x57 ⟶ (x55 x57 ⟶ False) ⟶ (x0 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 x56 ⟶ (x2 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x51 x56) ⟶ (x2 x57 (x1 (x50 x56 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x51 x56) ⟶ (x5 x57 x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x51 x56) ⟶ (x49 x57 x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x51 x56) ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (x55 x4 ⟶ False) ⟶ (∀ x56 . (x53 x56 x56 ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ ((x6 x47 ⟶ False) ⟶ False) ⟶ ((x46 x47 ⟶ False) ⟶ False) ⟶ (x55 x47 ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ ((x7 x44 ⟶ False) ⟶ False) ⟶ (x55 x44 ⟶ False) ⟶ ((x8 x9 ⟶ False) ⟶ False) ⟶ (x55 x9 ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ (x7 (x11 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x10 (x11 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ (x2 (x11 x56) (x1 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x6 (x43 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x12 (x43 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x42 (x43 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x46 (x43 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x7 (x41 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x6 (x41 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x12 (x41 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x42 (x41 x56 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x46 (x41 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x55 (x41 x56 x57) ⟶ False) ⟶ (x40 x39 ⟶ False) ⟶ ((x6 x39 ⟶ False) ⟶ False) ⟶ ((x46 x39 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x7 (x13 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x6 (x13 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x12 (x13 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x42 (x13 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x46 (x13 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x55 (x38 x56 x57) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x6 (x38 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x12 (x38 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x42 (x38 x56 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x46 (x38 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ (x2 (x38 x56 x57) (x1 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ ((x7 x37 ⟶ False) ⟶ False) ⟶ ((x6 x37 ⟶ False) ⟶ False) ⟶ ((x46 x37 ⟶ False) ⟶ False) ⟶ (x55 x37 ⟶ False) ⟶ (x10 x36 ⟶ False) ⟶ (x55 x14 ⟶ False) ⟶ (∀ x56 . (x5 (x35 x56) x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x49 (x35 x56) x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x34 (x35 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x6 (x35 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x12 (x35 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x42 (x35 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x46 (x35 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x2 (x35 x56) (x1 (x50 x56 x56)) ⟶ False) ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x6 x32 ⟶ False) ⟶ False) ⟶ ((x46 x32 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x7 (x15 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ x55 (x15 x56) ⟶ False) ⟶ (∀ x56 . (x55 x56 ⟶ False) ⟶ (x2 (x15 x56) (x1 x56) ⟶ False) ⟶ False) ⟶ ((x10 x31 ⟶ False) ⟶ False) ⟶ (x55 x31 ⟶ False) ⟶ ((x55 x30 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x16 (x17 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x49 (x17 x56) x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x34 (x17 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x33 (x17 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x6 (x17 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x12 (x17 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x42 (x17 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x46 (x17 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x2 (x17 x56) (x1 (x50 x56 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x12 (x29 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x42 (x29 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x46 (x29 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 (x29 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x29 x56 x57) (x1 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x6 (x18 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x12 (x18 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x42 (x18 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x46 (x18 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x18 x56 x57) (x1 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x49 (x28 x56 x57) x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x6 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x12 (x28 x56 x57) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x42 (x28 x57 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x46 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x28 x56 x57) (x1 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ ((x6 x27 ⟶ False) ⟶ False) ⟶ ((x46 x27 ⟶ False) ⟶ False) ⟶ ((x7 x26 ⟶ False) ⟶ False) ⟶ (x55 x26 ⟶ False) ⟶ (∀ x56 x57 x58 . x6 x58 ⟶ x49 x58 x56 x56 ⟶ x5 x58 x56 x56 ⟶ x2 x58 (x1 (x50 x56 x56)) ⟶ x57 = x58 ⟶ (x0 x57 (x25 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x56 (x25 x57) ⟶ (x56 = x19 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x25 x56) ⟶ (x2 (x19 x56 x57) (x1 (x50 x56 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x25 x56) ⟶ (x5 (x19 x56 x57) x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x25 x56) ⟶ (x49 (x19 x56 x57) x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 (x25 x56) ⟶ (x6 (x19 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ (x55 (x50 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x55 x57 ⟶ (x55 (x50 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 . x7 x56 ⟶ (x7 (x51 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x7 x56 ⟶ (x45 (x1 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x7 x56 ⟶ (x45 (x3 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 (x3 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 (x3 x56) ⟶ False) ⟶ (∀ x56 . (x8 (x51 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 (x51 x56) ⟶ False) ⟶ ((x55 x54 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x7 (x3 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x16 (x20 x56 x54) x54 ⟶ False) ⟶ False) ⟶ (∀ x56 . x7 x56 ⟶ (x7 (x1 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x46 x56 ⟶ x6 x56 ⟶ (x8 (x3 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x7 x57 ⟶ x7 x56 ⟶ (x7 (x50 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x2 (x21 x56) x56 ⟶ False) ⟶ False) ⟶ ((x55 x24 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x2 (x20 x57 x56) (x1 (x50 x57 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 (x23 x56 x57) x56 ⟶ (x53 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x0 (x23 x56 x57) x57 ⟶ False) ⟶ (x53 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x53 x57 x58 ⟶ x0 x56 x57 ⟶ (x0 x56 x58 ⟶ False) ⟶ False) ⟶ ((x54 = x24 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x22 x57 x56 = x56 ⟶ False) ⟶ (x0 (x22 x57 x56) x57 ⟶ False) ⟶ (x57 = x3 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 (x22 x57 x56) x57 ⟶ x22 x57 x56 = x56 ⟶ (x57 = x3 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x57 = x3 x58 ⟶ x56 = x58 ⟶ (x0 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x57 = x3 x58 ⟶ x0 x56 x57 ⟶ (x56 = x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x51 x56 = x25 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x53 x57 x56 ⟶ x53 x56 x57 ⟶ (x57 = x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x56 = x57 ⟶ (x53 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x57 = x56 ⟶ (x53 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x8 x57 ⟶ x2 x56 (x1 x57) ⟶ (x8 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ (x48 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x2 x57 (x1 (x50 x58 x56)) ⟶ x6 x57 ⟶ x49 x57 x58 x56 ⟶ (x49 x57 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x2 x57 (x1 (x50 x58 x56)) ⟶ x6 x57 ⟶ x49 x57 x58 x56 ⟶ x55 x57 ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ (x55 x56 ⟶ False) ⟶ x2 x57 (x1 (x50 x58 x56)) ⟶ x6 x57 ⟶ x49 x57 x58 x56 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x8 x57 ⟶ x2 x56 x57 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x8 x57 ⟶ x2 x56 x57 ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x45 x57 ⟶ x2 x56 (x1 x57) ⟶ (x45 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x8 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x45 x57 ⟶ x2 x56 x57 ⟶ (x7 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x56 x57)) ⟶ x6 x58 ⟶ x33 x58 ⟶ x16 x58 x57 ⟶ (x5 x58 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x56 x57)) ⟶ x6 x58 ⟶ x33 x58 ⟶ x16 x58 x57 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x10 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x40 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x10 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x10 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x45 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x57 x56)) ⟶ x6 x58 ⟶ x5 x58 x57 x56 ⟶ (x16 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x57 x56)) ⟶ x6 x58 ⟶ x5 x58 x57 x56 ⟶ (x33 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x57 x56)) ⟶ x6 x58 ⟶ x5 x58 x57 x56 ⟶ (x6 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x46 x56 ⟶ x6 x56 ⟶ (x40 x56 ⟶ False) ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x46 x56 ⟶ x6 x56 ⟶ (x40 x56 ⟶ False) ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x46 x56 ⟶ x6 x56 ⟶ (x40 x56 ⟶ False) ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 . (x7 x56 ⟶ False) ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x2 x56 (x1 (x50 x57 x58)) ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x2 x57 (x1 (x50 x56 x56)) ⟶ x49 x57 x56 x56 ⟶ (x34 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x40 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x10 x56 ⟶ (x7 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ x2 x56 (x1 (x50 x57 x58)) ⟶ x49 x56 x57 x58 ⟶ (x34 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x46 x57 ⟶ x6 x57 ⟶ x2 x56 (x1 x57) ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x7 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ x6 x56 ⟶ x49 x56 x58 x57 ⟶ (x7 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x7 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ x6 x56 ⟶ x49 x56 x58 x57 ⟶ (x49 x56 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x7 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ x6 x56 ⟶ x49 x56 x58 x57 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x55 x56 ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x56 x57)) ⟶ (x12 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x57 x56)) ⟶ (x42 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x55 x58 ⟶ False) ⟶ x55 x56 ⟶ x2 x57 (x1 (x50 x58 x56)) ⟶ x34 x57 x58 ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ x49 x56 x58 x57 ⟶ (x34 x56 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x33 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ x46 x56 ⟶ x6 x56 ⟶ (x46 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x7 x57 ⟶ x2 x56 (x1 x57) ⟶ (x7 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x10 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x58 (x1 (x50 x56 x57)) ⟶ (x46 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x55 x58 ⟶ x2 x56 (x1 (x50 x58 x57)) ⟶ (x34 x56 x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x2 x57 (x1 (x50 x58 x56)) ⟶ x34 x57 x58 ⟶ (x49 x57 x58 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x7 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x56 x57 ⟶ x0 x57 x56 ⟶ False) ⟶ (x51 x54 = x4 ⟶ False) ⟶ False (proof)