Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../18e6b..
PUUVQ../8fa76..
vout
PrNUD../2ec6f.. 0.02 bars
TMX9X../34fc9.. ownership of 25211.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMU96../c75ca.. ownership of c52ae.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUXhG../02b06.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 25211.. : ∀ 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 . x48 x50 ⟶ (x50 = x49 ⟶ False) ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x48 x50 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x49 = x47 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x49 x50 ⟶ x2 x50 (x1 x51) ⟶ x48 x51 ⟶ False) ⟶ (∀ x49 x50 x51 . x46 x51 ⟶ x46 x49 ⟶ x46 x50 ⟶ (x45 x51 (x45 x49 x50) = x45 (x45 x51 x49) x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x0 x50 x51 ⟶ x2 x51 (x1 x49) ⟶ (x2 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x44 x49 x43 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x3 x50 x49 ⟶ (x2 x50 (x1 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x2 x50 (x1 x49) ⟶ (x3 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x45 x4 x49 = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x2 x49 x50 ⟶ (x48 x50 ⟶ False) ⟶ (x0 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x45 x49 x43 = x43 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x0 x50 x49 ⟶ (x2 x50 x49 ⟶ False) ⟶ False) ⟶ ((x2 x47 x5 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x44 (x42 x50) (x42 x49) = x44 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . x46 x51 ⟶ x46 x49 ⟶ x46 x50 ⟶ (x45 (x45 x51 x49) x50 = x45 x51 (x45 x49 x50) ⟶ False) ⟶ False) ⟶ ((x2 x40 x41 ⟶ False) ⟶ False) ⟶ ((x2 x40 x6 ⟶ False) ⟶ False) ⟶ ((x39 x40 x41 x6 ⟶ False) ⟶ False) ⟶ ((x7 x40 ⟶ False) ⟶ False) ⟶ (x48 x40 ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x45 x49 (x42 x4) = x42 x49 ⟶ False) ⟶ False) ⟶ ((x2 x4 x41 ⟶ False) ⟶ False) ⟶ ((x2 x4 x6 ⟶ False) ⟶ False) ⟶ ((x39 x4 x41 x6 ⟶ False) ⟶ False) ⟶ ((x7 x4 ⟶ False) ⟶ False) ⟶ (x48 x4 ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x45 (x8 x50) (x8 x49) = x8 (x45 x50 x49) ⟶ False) ⟶ False) ⟶ ((x2 x38 x41 ⟶ False) ⟶ False) ⟶ ((x2 x38 x6 ⟶ False) ⟶ False) ⟶ ((x39 x38 x41 x6 ⟶ False) ⟶ False) ⟶ ((x48 x38 ⟶ False) ⟶ False) ⟶ ((x42 (x42 x40) = x40 ⟶ False) ⟶ False) ⟶ ((x42 (x42 x4) = x4 ⟶ False) ⟶ False) ⟶ ((x42 x40 = x42 x40 ⟶ False) ⟶ False) ⟶ ((x42 x4 = x42 x4 ⟶ False) ⟶ False) ⟶ ((x42 x38 = x38 ⟶ False) ⟶ False) ⟶ ((x45 (x42 x40) x4 = x42 x40 ⟶ False) ⟶ False) ⟶ ((x45 (x42 x40) x38 = x38 ⟶ False) ⟶ False) ⟶ ((x45 x40 x4 = x40 ⟶ False) ⟶ False) ⟶ ((x45 x40 x38 = x38 ⟶ False) ⟶ False) ⟶ ((x45 x4 (x42 x40) = x42 x40 ⟶ False) ⟶ False) ⟶ ((x45 x4 x40 = x40 ⟶ False) ⟶ False) ⟶ ((x45 x4 x4 = x4 ⟶ False) ⟶ False) ⟶ ((x45 x4 x38 = x38 ⟶ False) ⟶ False) ⟶ ((x45 x38 (x42 x40) = x38 ⟶ False) ⟶ False) ⟶ ((x45 x38 x40 = x38 ⟶ False) ⟶ False) ⟶ ((x45 x38 x4 = x38 ⟶ False) ⟶ False) ⟶ ((x45 x38 x38 = x38 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x40) (x42 x40) = x38 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x40) (x42 x4) = x42 x4 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x40) x38 = x42 x40 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x4) (x42 x40) = x4 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x4) (x42 x4) = x38 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x4) x4 = x42 x40 ⟶ False) ⟶ False) ⟶ ((x44 (x42 x4) x38 = x42 x4 ⟶ False) ⟶ False) ⟶ ((x44 x40 x40 = x38 ⟶ False) ⟶ False) ⟶ ((x44 x40 x4 = x4 ⟶ False) ⟶ False) ⟶ ((x44 x40 x38 = x40 ⟶ False) ⟶ False) ⟶ ((x44 x4 (x42 x4) = x40 ⟶ False) ⟶ False) ⟶ ((x44 x4 x40 = x42 x4 ⟶ False) ⟶ False) ⟶ ((x44 x4 x4 = x38 ⟶ False) ⟶ False) ⟶ ((x44 x4 x38 = x4 ⟶ False) ⟶ False) ⟶ ((x44 x38 (x42 x40) = x40 ⟶ False) ⟶ False) ⟶ ((x44 x38 (x42 x4) = x4 ⟶ False) ⟶ False) ⟶ ((x44 x38 x40 = x42 x40 ⟶ False) ⟶ False) ⟶ ((x44 x38 x4 = x42 x4 ⟶ False) ⟶ False) ⟶ ((x44 x38 x38 = x38 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x3 x49 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x2 x49 (x1 x51) ⟶ x2 x50 x49 ⟶ (x39 x50 x51 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x2 x49 (x1 x51) ⟶ x39 x50 x51 x49 ⟶ (x2 x50 x49 ⟶ False) ⟶ False) ⟶ ((x43 = x47 ⟶ False) ⟶ False) ⟶ ((x6 = x5 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x48 x10 ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x48 x12 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x11 x14 ⟶ False) ⟶ False) ⟶ ((x46 x14 ⟶ False) ⟶ False) ⟶ ((x48 x14 ⟶ False) ⟶ False) ⟶ ((x9 x15 ⟶ False) ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ ((x11 x36 ⟶ False) ⟶ False) ⟶ ((x13 x35 ⟶ False) ⟶ False) ⟶ ((x37 x35 ⟶ False) ⟶ False) ⟶ ((x11 x35 ⟶ False) ⟶ False) ⟶ ((x46 x35 ⟶ False) ⟶ False) ⟶ ((x7 x34 ⟶ False) ⟶ False) ⟶ ((x11 x34 ⟶ False) ⟶ False) ⟶ ((x13 x33 ⟶ False) ⟶ False) ⟶ ((x7 x33 ⟶ False) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ ((x46 x33 ⟶ False) ⟶ False) ⟶ ((x46 x32 ⟶ False) ⟶ False) ⟶ (x48 x32 ⟶ False) ⟶ (x48 x31 ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ ((x30 x17 ⟶ False) ⟶ False) ⟶ ((x18 x17 ⟶ False) ⟶ False) ⟶ (x48 x17 ⟶ False) ⟶ ((x11 x19 ⟶ False) ⟶ False) ⟶ ((x13 x29 ⟶ False) ⟶ False) ⟶ ((x46 x20 ⟶ False) ⟶ False) ⟶ ((x48 x28 ⟶ False) ⟶ False) ⟶ ((x16 x21 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x8 (x8 x49) = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x42 (x42 x49) = x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x48 x50 ⟶ False) ⟶ x46 x50 ⟶ (x48 x49 ⟶ False) ⟶ x46 x49 ⟶ x48 (x45 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . x13 x50 ⟶ x13 x49 ⟶ (x13 (x44 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x46 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x46 x49 ⟶ x48 (x8 x49) ⟶ False) ⟶ (∀ x49 x50 . x13 x50 ⟶ x13 x49 ⟶ (x13 (x45 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x46 x49 ⟶ (x46 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x46 x49 ⟶ x48 (x42 x49) ⟶ False) ⟶ ((x16 x5 ⟶ False) ⟶ False) ⟶ (x48 x5 ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x13 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x46 (x44 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x13 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x46 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x46 (x45 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ x37 (x8 x49) ⟶ False) ⟶ (∀ x49 . (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x37 x49 ⟶ x13 x49 ⟶ (x37 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x37 x49 ⟶ x13 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ x7 (x8 x49) ⟶ False) ⟶ (∀ x49 . (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x7 x49 ⟶ x13 x49 ⟶ (x7 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . x7 x49 ⟶ x13 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x37 x50 ⟶ False) ⟶ x13 x50 ⟶ (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ x37 (x45 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x7 x50 ⟶ False) ⟶ x13 x50 ⟶ (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ x37 (x45 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . (x7 x50 ⟶ False) ⟶ x13 x50 ⟶ (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ x7 (x45 x49 x50) ⟶ False) ⟶ (∀ x49 x50 . (x7 x50 ⟶ False) ⟶ x13 x50 ⟶ (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ x7 (x45 x50 x49) ⟶ False) ⟶ (∀ x49 x50 . x37 x50 ⟶ x13 x50 ⟶ (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ (x7 (x44 x49 x50) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x37 x50 ⟶ x13 x50 ⟶ (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ (x37 (x44 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x7 x50 ⟶ x13 x50 ⟶ (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ (x37 (x44 x49 x50) ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x7 x50 ⟶ x13 x50 ⟶ (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ (x7 (x44 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x37 x50 ⟶ False) ⟶ x13 x50 ⟶ (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ x7 (x44 x49 x50) ⟶ False) ⟶ (∀ x49 x50 . (x37 x50 ⟶ False) ⟶ x13 x50 ⟶ (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ x37 (x44 x50 x49) ⟶ False) ⟶ (∀ x49 . (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ x7 (x42 x49) ⟶ False) ⟶ (∀ x49 . (x37 x49 ⟶ False) ⟶ x13 x49 ⟶ (x46 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 . (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ x37 (x42 x49) ⟶ False) ⟶ (∀ x49 . (x7 x49 ⟶ False) ⟶ x13 x49 ⟶ (x46 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . (x48 x50 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x2 x49 (x1 x50) ⟶ (x39 (x27 x49 x50) x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x2 (x22 x49) x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 x51 . (x48 x51 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ x2 x49 (x1 x51) ⟶ x39 x50 x51 x49 ⟶ (x2 x50 x51 ⟶ False) ⟶ False) ⟶ ((x39 x43 x41 x6 ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x46 (x8 x49) ⟶ False) ⟶ False) ⟶ ((x2 x6 (x1 x41) ⟶ False) ⟶ False) ⟶ (∀ x49 . x46 x49 ⟶ (x46 (x42 x49) ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ x50 = x43 ⟶ x49 = x43 ⟶ (x49 = x8 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ x50 = x43 ⟶ x49 = x8 x50 ⟶ (x49 = x43 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x50 = x43 ⟶ False) ⟶ x45 x50 x49 = x4 ⟶ (x49 = x8 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x50 = x43 ⟶ False) ⟶ x49 = x8 x50 ⟶ (x45 x50 x49 = x4 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x46 x50 ⟶ x46 x49 ⟶ (x45 x50 x49 = x45 x49 x50 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x26 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ (x7 x49 ⟶ False) ⟶ (x37 x49 ⟶ False) ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ (x7 x49 ⟶ False) ⟶ (x37 x49 ⟶ False) ⟶ (x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x2 x49 x5 ⟶ (x9 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x11 x49 ⟶ x37 x49 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x11 x49 ⟶ x7 x49 ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ x11 x49 ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x9 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x11 x49 ⟶ (x7 x49 ⟶ False) ⟶ (x37 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x11 x49 ⟶ (x7 x49 ⟶ False) ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x9 x49 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x37 x49 ⟶ x7 x49 ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x37 x49 ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x37 x49 ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 x50 . x16 x50 ⟶ x2 x49 x50 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x11 x49 ⟶ (x37 x49 ⟶ False) ⟶ (x7 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . (x48 x49 ⟶ False) ⟶ x11 x49 ⟶ (x37 x49 ⟶ False) ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x25 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x7 x49 ⟶ x37 x49 ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x7 x49 ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x11 x49 ⟶ x7 x49 ⟶ x48 x49 ⟶ False) ⟶ (∀ x49 . x13 x49 ⟶ (x46 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x48 x49 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x9 x49 ⟶ (x11 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x9 x49 ⟶ (x13 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x9 x49 ⟶ (x46 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x18 x49 ⟶ x30 x49 ⟶ (x16 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x2 x49 x41 ⟶ (x13 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x2 x49 x41 ⟶ (x46 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x30 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 . x16 x49 ⟶ (x18 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x26 x50 ⟶ x2 x49 (x1 x50) ⟶ (x26 x49 ⟶ False) ⟶ False) ⟶ (∀ x49 x50 . x0 x49 x50 ⟶ x0 x50 x49 ⟶ False) ⟶ (x24 = x42 x4 ⟶ False) ⟶ (x23 = x43 ⟶ False) ⟶ ((x45 x24 x23 = x42 x23 ⟶ False) ⟶ False) ⟶ ((x46 x24 ⟶ False) ⟶ False) ⟶ ((x46 x23 ⟶ False) ⟶ False) ⟶ False (proof)