Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../1a6da..
PUh3G../d2878..
vout
PrNUD../890f8.. 0.02 bars
TMN9s../b7980.. ownership of df037.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMbSr../674f0.. ownership of 267de.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUdz9../43de8.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem df037.. : ∀ 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 . x47 x49 ⟶ x47 x48 ⟶ x49 = x45 x46 ⟶ x48 = x45 x46 ⟶ (x44 x49 x48 = x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x49 = x46 ⟶ x48 = x46 ⟶ (x44 x49 x48 = x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x46 ⟶ (x48 = x46 ⟶ False) ⟶ (x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x46 ⟶ (x48 = x46 ⟶ False) ⟶ (x49 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x46 ⟶ (x49 = x46 ⟶ False) ⟶ (x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x46 ⟶ (x49 = x46 ⟶ False) ⟶ (x49 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x43 x49 ⟶ (x49 = x48 ⟶ False) ⟶ x43 x48 ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x43 x49 ⟶ False) ⟶ (∀ x48 . x43 x48 ⟶ (x48 = x42 ⟶ False) ⟶ False) ⟶ (∀ x48 . x1 x48 ⟶ (x2 x48 x46 = x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x48 x49 ⟶ x40 x49 (x41 x50) ⟶ x43 x50 ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x49 x50 ⟶ x40 x50 (x41 x48) ⟶ (x40 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x39 x49 x48 ⟶ (x40 x49 (x41 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x40 x49 (x41 x48) ⟶ (x39 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x1 x48 ⟶ (x44 x46 x48 = x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x40 x48 x49 ⟶ (x43 x49 ⟶ False) ⟶ (x0 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x40 x49 x48 ⟶ False) ⟶ False) ⟶ ((x40 x42 x3 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x49 = x46 ⟶ x48 = x45 x46 ⟶ (x44 x49 x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x49 = x45 x46 ⟶ x48 = x46 ⟶ (x44 x49 x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x45 x46 ⟶ (x48 = x46 ⟶ False) ⟶ (x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x45 x46 ⟶ (x48 = x46 ⟶ False) ⟶ (x49 = x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x45 x46 ⟶ (x49 = x45 x46 ⟶ False) ⟶ (x48 = x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x44 x49 x48 = x45 x46 ⟶ (x49 = x45 x46 ⟶ False) ⟶ (x49 = x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x1 x49 ⟶ x1 x48 ⟶ (x37 (x38 x49) (x38 x48) = x37 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x1 x50 ⟶ x1 x48 ⟶ x1 x49 ⟶ (x44 (x44 x50 x48) x49 = x44 x50 (x44 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x1 x50 ⟶ x1 x48 ⟶ x1 x49 ⟶ (x44 x50 (x2 x48 x49) = x2 (x44 x50 x48) x49 ⟶ False) ⟶ False) ⟶ ((x40 x5 x4 ⟶ False) ⟶ False) ⟶ ((x40 x5 x36 ⟶ False) ⟶ False) ⟶ ((x6 x5 x4 x36 ⟶ False) ⟶ False) ⟶ ((x35 x5 ⟶ False) ⟶ False) ⟶ (x43 x5 ⟶ False) ⟶ (∀ x48 . x1 x48 ⟶ (x44 x48 (x38 x46) = x38 x48 ⟶ False) ⟶ False) ⟶ ((x40 x46 x4 ⟶ False) ⟶ False) ⟶ ((x40 x46 x36 ⟶ False) ⟶ False) ⟶ ((x6 x46 x4 x36 ⟶ False) ⟶ False) ⟶ ((x35 x46 ⟶ False) ⟶ False) ⟶ (x43 x46 ⟶ False) ⟶ ((x40 x34 x4 ⟶ False) ⟶ False) ⟶ ((x40 x34 x36 ⟶ False) ⟶ False) ⟶ ((x6 x34 x4 x36 ⟶ False) ⟶ False) ⟶ ((x43 x34 ⟶ False) ⟶ False) ⟶ ((x38 (x2 (x38 x46) x5) = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x38 (x2 x46 x5) = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x38 (x38 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x38 (x38 x46) = x46 ⟶ False) ⟶ False) ⟶ ((x38 x5 = x38 x5 ⟶ False) ⟶ False) ⟶ ((x38 x46 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x38 x34 = x34 ⟶ False) ⟶ False) ⟶ ((x44 (x2 (x38 x46) x5) (x38 x5) = x46 ⟶ False) ⟶ False) ⟶ ((x44 (x2 (x38 x46) x5) x5 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x44 (x2 (x38 x46) x5) x46 = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x44 (x2 x46 x5) (x38 x5) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x44 (x2 x46 x5) x5 = x46 ⟶ False) ⟶ False) ⟶ ((x44 (x2 x46 x5) x46 = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x44 (x2 x46 x5) x34 = x34 ⟶ False) ⟶ False) ⟶ ((x44 (x38 x5) (x2 (x38 x46) x5) = x46 ⟶ False) ⟶ False) ⟶ ((x44 (x38 x5) (x2 x46 x5) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x44 (x38 x5) x46 = x38 x5 ⟶ False) ⟶ False) ⟶ ((x44 (x38 x5) x34 = x34 ⟶ False) ⟶ False) ⟶ ((x44 x5 (x2 (x38 x46) x5) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x44 x5 (x2 x46 x5) = x46 ⟶ False) ⟶ False) ⟶ ((x44 x5 x46 = x5 ⟶ False) ⟶ False) ⟶ ((x44 x5 x34 = x34 ⟶ False) ⟶ False) ⟶ ((x44 x46 (x2 (x38 x46) x5) = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x44 x46 (x2 x46 x5) = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x44 x46 (x38 x5) = x38 x5 ⟶ False) ⟶ False) ⟶ ((x44 x46 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x44 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x44 x46 x34 = x34 ⟶ False) ⟶ False) ⟶ ((x44 x34 (x2 x46 x5) = x34 ⟶ False) ⟶ False) ⟶ ((x44 x34 (x38 x5) = x34 ⟶ False) ⟶ False) ⟶ ((x44 x34 x5 = x34 ⟶ False) ⟶ False) ⟶ ((x44 x34 x46 = x34 ⟶ False) ⟶ False) ⟶ ((x44 x34 x34 = x34 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x5) x5 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x46) x5 = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x46) x46 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x2 x5 x5 = x46 ⟶ False) ⟶ False) ⟶ ((x2 x5 x46 = x5 ⟶ False) ⟶ False) ⟶ ((x2 x46 (x2 (x38 x46) x5) = x38 x5 ⟶ False) ⟶ False) ⟶ ((x2 x46 (x2 x46 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x2 x46 (x38 x5) = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x2 x46 (x38 x46) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x2 x46 x5 = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x2 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x37 (x2 (x38 x46) x5) (x2 (x38 x46) x5) = x34 ⟶ False) ⟶ False) ⟶ ((x37 (x2 (x38 x46) x5) (x2 x46 x5) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x37 (x2 (x38 x46) x5) (x38 x46) = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x37 (x2 (x38 x46) x5) x34 = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x37 (x2 x46 x5) (x2 (x38 x46) x5) = x46 ⟶ False) ⟶ False) ⟶ ((x37 (x2 x46 x5) (x2 x46 x5) = x34 ⟶ False) ⟶ False) ⟶ ((x37 (x2 x46 x5) x46 = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x37 (x2 x46 x5) x34 = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x5) (x38 x5) = x34 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x5) (x38 x46) = x38 x46 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x5) x34 = x38 x5 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x46) (x2 (x38 x46) x5) = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x46) (x38 x5) = x46 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x46) (x38 x46) = x34 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x46) x46 = x38 x5 ⟶ False) ⟶ False) ⟶ ((x37 (x38 x46) x34 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x37 x5 x5 = x34 ⟶ False) ⟶ False) ⟶ ((x37 x5 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x37 x5 x34 = x5 ⟶ False) ⟶ False) ⟶ ((x37 x46 (x2 x46 x5) = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x37 x46 (x38 x46) = x5 ⟶ False) ⟶ False) ⟶ ((x37 x46 x5 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x37 x46 x46 = x34 ⟶ False) ⟶ False) ⟶ ((x37 x46 x34 = x46 ⟶ False) ⟶ False) ⟶ ((x37 x34 (x2 (x38 x46) x5) = x2 x46 x5 ⟶ False) ⟶ False) ⟶ ((x37 x34 (x2 x46 x5) = x2 (x38 x46) x5 ⟶ False) ⟶ False) ⟶ ((x37 x34 (x38 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x37 x34 (x38 x46) = x46 ⟶ False) ⟶ False) ⟶ ((x37 x34 x5 = x38 x5 ⟶ False) ⟶ False) ⟶ ((x37 x34 x46 = x38 x46 ⟶ False) ⟶ False) ⟶ ((x37 x34 x34 = x34 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x39 x48 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ (x33 x49 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x43 x50 ⟶ False) ⟶ (x43 x48 ⟶ False) ⟶ x40 x48 (x41 x50) ⟶ x40 x49 x48 ⟶ (x6 x49 x50 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x43 x50 ⟶ False) ⟶ (x43 x48 ⟶ False) ⟶ x40 x48 (x41 x50) ⟶ x6 x49 x50 x48 ⟶ (x40 x49 x48 ⟶ False) ⟶ False) ⟶ ((x36 = x3 ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x4 ⟶ (x45 x48 = x38 x48 ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ (x43 x8 ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x32 x10 ⟶ False) ⟶ False) ⟶ ((x1 x10 ⟶ False) ⟶ False) ⟶ ((x43 x10 ⟶ False) ⟶ False) ⟶ ((x7 x11 ⟶ False) ⟶ False) ⟶ ((x9 x31 ⟶ False) ⟶ False) ⟶ ((x12 x31 ⟶ False) ⟶ False) ⟶ ((x32 x31 ⟶ False) ⟶ False) ⟶ ((x1 x31 ⟶ False) ⟶ False) ⟶ ((x9 x30 ⟶ False) ⟶ False) ⟶ ((x35 x30 ⟶ False) ⟶ False) ⟶ ((x32 x30 ⟶ False) ⟶ False) ⟶ ((x1 x30 ⟶ False) ⟶ False) ⟶ (x43 x29 ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x28 x14 ⟶ False) ⟶ False) ⟶ ((x15 x14 ⟶ False) ⟶ False) ⟶ (x43 x14 ⟶ False) ⟶ ((x13 x16 ⟶ False) ⟶ False) ⟶ (x43 x16 ⟶ False) ⟶ ((x40 x16 (x41 x4) ⟶ False) ⟶ False) ⟶ ((x47 x27 ⟶ False) ⟶ False) ⟶ ((x9 x17 ⟶ False) ⟶ False) ⟶ ((x43 x26 ⟶ False) ⟶ False) ⟶ ((x13 x18 ⟶ False) ⟶ False) ⟶ ((x47 x25 ⟶ False) ⟶ False) ⟶ ((x9 x25 ⟶ False) ⟶ False) ⟶ ((x1 x25 ⟶ False) ⟶ False) ⟶ ((x32 x25 ⟶ False) ⟶ False) ⟶ ((x40 x25 x4 ⟶ False) ⟶ False) ⟶ (∀ x48 . x1 x48 ⟶ (x38 (x38 x48) = x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x4 ⟶ (x45 (x45 x48) = x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x9 x49 ⟶ x9 x48 ⟶ (x9 (x2 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x9 x49 ⟶ x9 x48 ⟶ (x9 (x37 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x9 x49 ⟶ x9 x48 ⟶ (x9 (x44 x49 x48) ⟶ False) ⟶ False) ⟶ ((x13 x3 ⟶ False) ⟶ False) ⟶ (x43 x3 ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ (x47 (x37 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x9 x48 ⟶ (x9 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x9 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x47 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x35 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x2 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x2 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x2 x48 x49) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x2 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . x7 x49 ⟶ x7 x48 ⟶ (x7 (x44 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ (x47 (x44 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x44 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . (x35 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x44 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . (x35 x49 ⟶ False) ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x44 x48 x49) ⟶ False) ⟶ (∀ x48 x49 . (x35 x49 ⟶ False) ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x44 x49 x48) ⟶ False) ⟶ (∀ x48 x49 . x12 x49 ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ (x35 (x37 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x12 x49 ⟶ x9 x49 ⟶ (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ (x12 (x37 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x35 x49 ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ (x12 (x37 x48 x49) ⟶ False) ⟶ False) ⟶ ((x43 x42 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x43 x48 ⟶ False) ⟶ x7 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x43 x48 ⟶ False) ⟶ x7 x48 ⟶ x7 (x38 x48) ⟶ False) ⟶ (∀ x48 x49 . x35 x49 ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ (x35 (x37 x49 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x37 x48 x49) ⟶ False) ⟶ (∀ x48 x49 . (x12 x49 ⟶ False) ⟶ x9 x49 ⟶ (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x37 x49 x48) ⟶ False) ⟶ (∀ x48 . (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ x35 (x38 x48) ⟶ False) ⟶ (∀ x48 . (x12 x48 ⟶ False) ⟶ x9 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ x12 (x38 x48) ⟶ False) ⟶ (∀ x48 . (x35 x48 ⟶ False) ⟶ x9 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x43 x49 ⟶ False) ⟶ (x43 x48 ⟶ False) ⟶ x40 x48 (x41 x49) ⟶ (x6 (x24 x48 x49) x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x40 (x19 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x43 x50 ⟶ False) ⟶ (x43 x48 ⟶ False) ⟶ x40 x48 (x41 x50) ⟶ x6 x49 x50 x48 ⟶ (x40 x49 x50 ⟶ False) ⟶ False) ⟶ ((x40 x36 (x41 x4) ⟶ False) ⟶ False) ⟶ (∀ x48 . x1 x48 ⟶ (x1 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x4 ⟶ (x40 (x45 x48) x4 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x47 x50 ⟶ x47 x48 ⟶ x47 x49 ⟶ x48 = x44 x50 x49 ⟶ (x33 x50 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x33 x49 x48 ⟶ (x48 = x44 x49 (x20 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x47 x48 ⟶ x33 x49 x48 ⟶ (x47 (x20 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x1 x49 ⟶ x1 x48 ⟶ (x44 x49 x48 = x44 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 . x43 x48 ⟶ (x23 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x3 ⟶ (x7 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x43 x48 ⟶ (x7 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x13 x49 ⟶ x40 x48 x49 ⟶ (x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x9 x48 ⟶ (x32 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x43 x48 ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x9 x48 ⟶ (x1 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x43 x48 ⟶ (x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ x12 x48 ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x7 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x9 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x9 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x15 x48 ⟶ x28 x48 ⟶ (x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x36 ⟶ x12 x48 ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x40 x48 x4 ⟶ (x9 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x13 x48 ⟶ (x28 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x13 x48 ⟶ (x15 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x7 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x7 x48 ⟶ (x13 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x23 x49 ⟶ x40 x48 (x41 x49) ⟶ (x23 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x0 x49 x48 ⟶ False) ⟶ (x21 = x38 x46 ⟶ False) ⟶ (x21 = x46 ⟶ False) ⟶ ((x33 x21 x46 ⟶ False) ⟶ (x33 x21 (x38 x46) ⟶ False) ⟶ False) ⟶ ((x47 x21 ⟶ False) ⟶ False) ⟶ False (proof)