Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../9eab6..
PUTju../77a06..
vout
PrPhD../225fa.. 3.39 bars
TMKd1../aeca8.. ownership of 57004.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMPH5../f51b3.. ownership of 5d0c7.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUSVC../640d6.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 57004.. : ∀ 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 . x46 x48 ⟶ (x48 = x47 ⟶ False) ⟶ x46 x47 ⟶ False) ⟶ (∀ x47 x48 . x0 x47 x48 ⟶ x46 x48 ⟶ False) ⟶ (∀ x47 . x46 x47 ⟶ (x47 = x45 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x2 x47 x3 = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x0 x47 x48 ⟶ x43 x48 (x44 x49) ⟶ x46 x49 ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x2 x4 x47 = x4 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x0 x48 x49 ⟶ x43 x49 (x44 x47) ⟶ (x43 x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x5 x47 x4 = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x42 x48 x47 ⟶ (x43 x48 (x44 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x43 x48 (x44 x47) ⟶ (x42 x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x41 x3 x47 = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x43 x47 x48 ⟶ (x46 x48 ⟶ False) ⟶ (x0 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x41 x47 x4 = x4 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x0 x48 x47 ⟶ (x43 x48 x47 ⟶ False) ⟶ False) ⟶ ((x43 x45 x40 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x6 x47 x4 = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x5 (x39 x48) (x39 x47) = x5 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x6 (x39 x48) (x39 x47) = x39 (x6 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x1 x49 ⟶ x1 x47 ⟶ x1 x48 ⟶ (x41 (x41 x49 x47) x48 = x41 x49 (x41 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x1 x49 ⟶ x1 x47 ⟶ x1 x48 ⟶ (x6 (x6 x49 x47) x48 = x6 x49 (x6 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x1 x49 ⟶ x1 x47 ⟶ x1 x48 ⟶ (x41 (x6 x49 x47) x48 = x6 (x41 x49 x48) (x41 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . x1 x49 ⟶ x1 x47 ⟶ x1 x48 ⟶ (x41 x49 (x2 x47 x48) = x2 (x41 x49 x47) x48 ⟶ False) ⟶ False) ⟶ ((x43 x37 x38 ⟶ False) ⟶ False) ⟶ ((x43 x37 x7 ⟶ False) ⟶ False) ⟶ ((x36 x37 x38 x7 ⟶ False) ⟶ False) ⟶ ((x8 x37 ⟶ False) ⟶ False) ⟶ (x46 x37 ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x41 x47 (x39 x3) = x39 x47 ⟶ False) ⟶ False) ⟶ ((x43 x3 x38 ⟶ False) ⟶ False) ⟶ ((x43 x3 x7 ⟶ False) ⟶ False) ⟶ ((x36 x3 x38 x7 ⟶ False) ⟶ False) ⟶ ((x8 x3 ⟶ False) ⟶ False) ⟶ (x46 x3 ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x6 x48 (x39 x47) = x5 x48 x47 ⟶ False) ⟶ False) ⟶ ((x43 x35 x38 ⟶ False) ⟶ False) ⟶ ((x43 x35 x7 ⟶ False) ⟶ False) ⟶ ((x36 x35 x38 x7 ⟶ False) ⟶ False) ⟶ ((x46 x35 ⟶ False) ⟶ False) ⟶ ((x39 (x2 (x39 x3) x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x39 (x2 x3 x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x39 (x39 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x39 (x39 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x39 x37 = x39 x37 ⟶ False) ⟶ False) ⟶ ((x39 x3 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x39 x35 = x35 ⟶ False) ⟶ False) ⟶ ((x41 (x2 (x39 x3) x37) (x39 x37) = x3 ⟶ False) ⟶ False) ⟶ ((x41 (x2 (x39 x3) x37) x37 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x41 (x2 (x39 x3) x37) x3 = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x41 (x2 x3 x37) (x39 x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x41 (x2 x3 x37) x37 = x3 ⟶ False) ⟶ False) ⟶ ((x41 (x2 x3 x37) x3 = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x41 (x2 x3 x37) x35 = x35 ⟶ False) ⟶ False) ⟶ ((x41 (x39 x37) (x2 (x39 x3) x37) = x3 ⟶ False) ⟶ False) ⟶ ((x41 (x39 x37) (x2 x3 x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x41 (x39 x37) x3 = x39 x37 ⟶ False) ⟶ False) ⟶ ((x41 (x39 x37) x35 = x35 ⟶ False) ⟶ False) ⟶ ((x41 x37 (x2 (x39 x3) x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x41 x37 (x2 x3 x37) = x3 ⟶ False) ⟶ False) ⟶ ((x41 x37 x3 = x37 ⟶ False) ⟶ False) ⟶ ((x41 x37 x35 = x35 ⟶ False) ⟶ False) ⟶ ((x41 x3 (x2 (x39 x3) x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x41 x3 (x2 x3 x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x41 x3 (x39 x37) = x39 x37 ⟶ False) ⟶ False) ⟶ ((x41 x3 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x41 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x41 x3 x35 = x35 ⟶ False) ⟶ False) ⟶ ((x41 x35 (x2 x3 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x41 x35 (x39 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x41 x35 x37 = x35 ⟶ False) ⟶ False) ⟶ ((x41 x35 x3 = x35 ⟶ False) ⟶ False) ⟶ ((x41 x35 x35 = x35 ⟶ False) ⟶ False) ⟶ ((x2 (x39 x37) x37 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x2 (x39 x3) x37 = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x2 (x39 x3) x3 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x2 x37 x37 = x3 ⟶ False) ⟶ False) ⟶ ((x2 x37 x3 = x37 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x2 (x39 x3) x37) = x39 x37 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x2 x3 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x39 x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x39 x3) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 x37 = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x2 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x39 x3) x37) (x2 (x39 x3) x37) = x35 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x39 x3) x37) (x2 x3 x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x39 x3) x37) (x39 x3) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x5 (x2 (x39 x3) x37) x35 = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x37) (x2 (x39 x3) x37) = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x37) (x2 x3 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x37) x3 = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x5 (x2 x3 x37) x35 = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x37) (x39 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x37) (x39 x3) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x37) x35 = x39 x37 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x3) (x2 (x39 x3) x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x3) (x39 x37) = x3 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x3) (x39 x3) = x35 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x3) x3 = x39 x37 ⟶ False) ⟶ False) ⟶ ((x5 (x39 x3) x35 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x5 x37 x37 = x35 ⟶ False) ⟶ False) ⟶ ((x5 x37 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x37 x35 = x37 ⟶ False) ⟶ False) ⟶ ((x5 x3 (x2 x3 x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x5 x3 (x39 x3) = x37 ⟶ False) ⟶ False) ⟶ ((x5 x3 x37 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x5 x3 x3 = x35 ⟶ False) ⟶ False) ⟶ ((x5 x3 x35 = x3 ⟶ False) ⟶ False) ⟶ ((x5 x35 (x2 (x39 x3) x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x5 x35 (x2 x3 x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x5 x35 (x39 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x5 x35 (x39 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x5 x35 x37 = x39 x37 ⟶ False) ⟶ False) ⟶ ((x5 x35 x3 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x5 x35 x35 = x35 ⟶ False) ⟶ False) ⟶ ((x6 (x2 (x39 x3) x37) (x2 (x39 x3) x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x6 (x2 (x39 x3) x37) (x2 x3 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x6 (x2 (x39 x3) x37) x3 = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x6 (x2 x3 x37) (x2 (x39 x3) x37) = x35 ⟶ False) ⟶ False) ⟶ ((x6 (x2 x3 x37) (x2 x3 x37) = x3 ⟶ False) ⟶ False) ⟶ ((x6 (x2 x3 x37) (x39 x3) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x6 (x2 x3 x37) x35 = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x37) x37 = x35 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x37) x3 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x3) (x2 x3 x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x3) (x39 x3) = x39 x37 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x3) x37 = x3 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x3) x3 = x35 ⟶ False) ⟶ False) ⟶ ((x6 (x39 x3) x35 = x39 x3 ⟶ False) ⟶ False) ⟶ ((x6 x37 (x39 x37) = x35 ⟶ False) ⟶ False) ⟶ ((x6 x37 (x39 x3) = x3 ⟶ False) ⟶ False) ⟶ ((x6 x37 x35 = x37 ⟶ False) ⟶ False) ⟶ ((x6 x3 (x2 (x39 x3) x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x6 x3 (x39 x37) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x6 x3 (x39 x3) = x35 ⟶ False) ⟶ False) ⟶ ((x6 x3 x3 = x37 ⟶ False) ⟶ False) ⟶ ((x6 x3 x35 = x3 ⟶ False) ⟶ False) ⟶ ((x6 x35 (x2 (x39 x3) x37) = x2 (x39 x3) x37 ⟶ False) ⟶ False) ⟶ ((x6 x35 (x2 x3 x37) = x2 x3 x37 ⟶ False) ⟶ False) ⟶ ((x6 x35 (x39 x37) = x39 x37 ⟶ False) ⟶ False) ⟶ ((x6 x35 (x39 x3) = x39 x3 ⟶ False) ⟶ False) ⟶ ((x6 x35 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x6 x35 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x6 x35 x35 = x35 ⟶ False) ⟶ False) ⟶ (∀ x47 . (x42 x47 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . (x46 x49 ⟶ False) ⟶ (x46 x47 ⟶ False) ⟶ x43 x47 (x44 x49) ⟶ x43 x48 x47 ⟶ (x36 x48 x49 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . (x46 x49 ⟶ False) ⟶ (x46 x47 ⟶ False) ⟶ x43 x47 (x44 x49) ⟶ x36 x48 x49 x47 ⟶ (x43 x48 x47 ⟶ False) ⟶ False) ⟶ ((x4 = x45 ⟶ False) ⟶ False) ⟶ ((x7 = x40 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x46 x10 ⟶ False) ⟶ ((x9 x11 ⟶ False) ⟶ False) ⟶ ((x1 x34 ⟶ False) ⟶ False) ⟶ (x46 x34 ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x12 x32 ⟶ False) ⟶ False) ⟶ ((x31 x32 ⟶ False) ⟶ False) ⟶ (x46 x32 ⟶ False) ⟶ ((x1 x30 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x33 x29 ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x39 (x39 x47) = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x13 x47 ⟶ (x28 (x28 x47) = x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x15 x48 x48 = x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x27 x48 x48 = x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . (x46 x48 ⟶ False) ⟶ x1 x48 ⟶ (x46 x47 ⟶ False) ⟶ x1 x47 ⟶ x46 (x2 x48 x47) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x13 (x26 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . (x46 x48 ⟶ False) ⟶ x1 x48 ⟶ (x46 x47 ⟶ False) ⟶ x1 x47 ⟶ x46 (x41 x48 x47) ⟶ False) ⟶ (∀ x47 . (x46 x47 ⟶ False) ⟶ x1 x47 ⟶ (x1 (x39 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 . (x46 x47 ⟶ False) ⟶ x1 x47 ⟶ x46 (x39 x47) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x13 (x25 x48 x47) ⟶ False) ⟶ False) ⟶ ((x33 x40 ⟶ False) ⟶ False) ⟶ (x46 x40 ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x1 (x2 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x13 (x24 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x1 (x5 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x13 (x15 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x1 (x41 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x13 (x27 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x1 (x6 x48 x47) ⟶ False) ⟶ False) ⟶ ((x13 x23 ⟶ False) ⟶ False) ⟶ ((x13 x16 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . (x46 x48 ⟶ False) ⟶ (x46 x47 ⟶ False) ⟶ x43 x47 (x44 x48) ⟶ (x36 (x22 x47 x48) x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . (x43 (x17 x47) x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 x49 . (x46 x49 ⟶ False) ⟶ (x46 x47 ⟶ False) ⟶ x43 x47 (x44 x49) ⟶ x36 x48 x49 x47 ⟶ (x43 x48 x49 ⟶ False) ⟶ False) ⟶ ((x36 x4 x38 x7 ⟶ False) ⟶ False) ⟶ ((x43 x7 (x44 x38) ⟶ False) ⟶ False) ⟶ (∀ x47 . x1 x47 ⟶ (x1 (x39 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 . x13 x47 ⟶ (x13 (x28 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x25 x48 x47 = x27 (x24 x48 x47) (x24 x47 x48) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x24 x48 x47 = x15 (x28 x48) x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x15 x48 x47 = x28 (x27 (x28 x48) (x28 x47)) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x27 x48 x47 = x41 x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x13 x47 ⟶ (x28 x47 = x5 x3 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x47 = x23 ⟶ (x13 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x47 = x16 ⟶ (x13 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x13 x47 ⟶ (x47 = x16 ⟶ False) ⟶ (x47 = x23 ⟶ False) ⟶ False) ⟶ ((x23 = x3 ⟶ False) ⟶ False) ⟶ ((x16 = x4 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x26 x48 x47 = x28 (x25 x48 x47) ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x25 x48 x47 = x25 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x15 x48 x47 = x15 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x27 x48 x47 = x27 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x41 x48 x47 = x41 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x1 x48 ⟶ x1 x47 ⟶ (x6 x48 x47 = x6 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x13 x48 ⟶ x13 x47 ⟶ (x26 x48 x47 = x26 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x47 . x46 x47 ⟶ (x21 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x43 x47 x40 ⟶ (x9 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x46 x47 ⟶ (x9 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x9 x47 ⟶ (x33 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x33 x48 ⟶ x43 x47 x48 ⟶ (x33 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x46 x47 ⟶ (x18 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x46 x47 ⟶ (x33 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x9 x47 ⟶ (x1 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x31 x47 ⟶ x12 x47 ⟶ (x33 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x43 x47 x38 ⟶ (x1 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x13 x47 ⟶ (x9 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x33 x47 ⟶ (x12 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 . x33 x47 ⟶ (x31 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x21 x48 ⟶ x43 x47 (x44 x48) ⟶ (x21 x47 ⟶ False) ⟶ False) ⟶ (∀ x47 x48 . x0 x47 x48 ⟶ x0 x48 x47 ⟶ False) ⟶ (x24 x19 (x26 x19 x20) = x15 (x28 x19) (x28 x20) ⟶ False) ⟶ ((x13 x20 ⟶ False) ⟶ False) ⟶ ((x13 x19 ⟶ False) ⟶ False) ⟶ False (proof)