Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../4e2ee..
PUUir../8cbd8..
vout
PrPhD../ba37d.. 3.34 bars
TMQwd../bec13.. ownership of b336b.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMQe4../a7c80.. ownership of e98e7.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUewz../34401.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem b336b.. : ∀ 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 : ι → ι → ο . ∀ x58 . ∀ x59 : ι → ο . (∀ x60 x61 . x59 x61 ⟶ (x61 = x60 ⟶ False) ⟶ x59 x60 ⟶ False) ⟶ (∀ x60 x61 . x0 x60 x61 ⟶ x59 x61 ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x60 = x58 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x0 x60 x61 ⟶ x2 x61 (x1 x62) ⟶ x59 x62 ⟶ False) ⟶ (∀ x60 x61 x62 . x0 x61 x62 ⟶ x2 x62 (x1 x60) ⟶ (x2 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 x63 . (x59 x63 ⟶ False) ⟶ x2 x60 x63 ⟶ x2 x62 x63 ⟶ x2 x61 (x3 x63) ⟶ (x4 x61 x60 x62 ⟶ False) ⟶ (x4 x61 x62 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x57 x61 x60 ⟶ (x2 x61 (x1 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x2 x61 (x1 x60) ⟶ (x57 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x2 x60 x61 ⟶ (x59 x61 ⟶ False) ⟶ (x0 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x0 x61 x60 ⟶ (x2 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x57 x60 x60 ⟶ False) ⟶ False) ⟶ ((x5 x6 ⟶ False) ⟶ False) ⟶ ((x56 x6 ⟶ False) ⟶ False) ⟶ (x59 x6 ⟶ False) ⟶ (∀ x60 . (x55 x60 ⟶ False) ⟶ (x56 (x54 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x55 x60 ⟶ False) ⟶ x55 (x54 x60) ⟶ False) ⟶ (∀ x60 . (x55 x60 ⟶ False) ⟶ (x2 (x54 x60) (x1 x60) ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ (x59 x8 ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x53 x10 ⟶ False) ⟶ False) ⟶ ((x11 x10 ⟶ False) ⟶ False) ⟶ ((x59 x10 ⟶ False) ⟶ False) ⟶ ((x7 x12 ⟶ False) ⟶ False) ⟶ ((x9 x52 ⟶ False) ⟶ False) ⟶ ((x13 x52 ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ ((x11 x52 ⟶ False) ⟶ False) ⟶ (x59 x51 ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x50 x15 ⟶ False) ⟶ False) ⟶ ((x16 x15 ⟶ False) ⟶ False) ⟶ (x59 x15 ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x59 x60 ⟶ False) ⟶ (x56 (x49 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x59 x60 ⟶ False) ⟶ x59 (x49 x60) ⟶ False) ⟶ (∀ x60 . (x59 x60 ⟶ False) ⟶ (x2 (x49 x60) (x1 x60) ⟶ False) ⟶ False) ⟶ ((x9 x19 ⟶ False) ⟶ False) ⟶ ((x59 x48 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x20 (x21 x60 x61) x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x47 (x21 x61 x60) x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x22 (x21 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 (x21 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x2 (x21 x60 x61) (x1 (x23 x61 x60)) ⟶ False) ⟶ False) ⟶ ((x14 x46 ⟶ False) ⟶ False) ⟶ ((x56 x24 ⟶ False) ⟶ False) ⟶ (x59 x24 ⟶ False) ⟶ (∀ x60 . x56 x60 ⟶ (x5 (x1 x60) ⟶ False) ⟶ False) ⟶ ((x59 x58 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x59 x60 ⟶ False) ⟶ x59 (x3 x60) ⟶ False) ⟶ (∀ x60 . x56 x60 ⟶ (x56 (x1 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x56 x61 ⟶ x56 x60 ⟶ (x56 (x23 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x2 (x45 x60) x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x22 x62 ⟶ x0 (x25 x61 x60) x62 ⟶ (x4 x62 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x22 x62 ⟶ x4 x62 x61 x60 ⟶ (x0 (x25 x61 x60) x62 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 x63 x64 . (x59 x64 ⟶ False) ⟶ x2 x60 x64 ⟶ x2 x63 x64 ⟶ x2 x61 x64 ⟶ x0 (x25 x60 x63) (x26 x62 x64) ⟶ x0 (x25 x63 x61) (x26 x62 x64) ⟶ (x0 (x25 x60 x61) (x26 x62 x64) ⟶ False) ⟶ (x0 (x26 x62 x64) x62 ⟶ False) ⟶ (x62 = x3 x64 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 x63 . (x59 x63 ⟶ False) ⟶ x2 x60 x63 ⟶ x2 x62 x63 ⟶ (x0 (x25 x60 x62) (x26 x61 x63) ⟶ False) ⟶ (x0 (x25 x62 x60) (x26 x61 x63) ⟶ False) ⟶ (x0 (x26 x61 x63) x61 ⟶ False) ⟶ (x61 = x3 x63 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ (x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ False) ⟶ (x0 (x26 x60 x61) x60 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ x0 (x25 (x43 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ (x0 (x25 (x27 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ (x0 (x25 (x43 x60 x61) (x27 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ (x2 (x44 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ (x2 (x27 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x41 x60 x61) (x42 x60 x61)) (x26 x60 x61) ⟶ (x2 (x43 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ x0 (x25 (x43 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ (x0 (x25 (x27 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ (x0 (x25 (x43 x60 x61) (x27 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ (x2 (x44 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ (x2 (x27 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ x0 (x25 (x42 x60 x61) (x41 x60 x61)) (x26 x60 x61) ⟶ (x2 (x43 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ x0 (x25 (x43 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ (x0 (x25 (x27 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ (x0 (x25 (x43 x60 x61) (x27 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ (x2 (x44 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ (x2 (x27 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x41 x60 x61) x61 ⟶ False) ⟶ (x2 (x43 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ x0 (x25 (x43 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ (x0 (x25 (x27 x60 x61) (x44 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ (x0 (x25 (x43 x60 x61) (x27 x60 x61)) (x26 x60 x61) ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ (x2 (x44 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ (x2 (x27 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x0 (x26 x60 x61) x60 ⟶ x2 (x26 x60 x61) (x1 (x23 x61 x61)) ⟶ (x2 (x42 x60 x61) x61 ⟶ False) ⟶ (x2 (x43 x60 x61) x61 ⟶ False) ⟶ (x60 = x3 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ x0 (x25 (x38 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ (x0 (x25 (x28 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ (x0 (x25 (x38 x61 x60 x62) (x28 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ (x2 (x37 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ (x2 (x28 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x40 x61 x60 x62) (x39 x61 x60 x62)) x61 ⟶ (x2 (x38 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ x0 (x25 (x38 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ (x0 (x25 (x28 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ (x0 (x25 (x38 x61 x60 x62) (x28 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ (x2 (x37 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ (x2 (x28 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ x0 (x25 (x39 x61 x60 x62) (x40 x61 x60 x62)) x61 ⟶ (x2 (x38 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ x0 (x25 (x38 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ (x0 (x25 (x28 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ (x0 (x25 (x38 x61 x60 x62) (x28 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x37 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x28 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x40 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x38 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ x0 (x25 (x38 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ (x0 (x25 (x28 x61 x60 x62) (x37 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ (x0 (x25 (x38 x61 x60 x62) (x28 x61 x60 x62)) x61 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x37 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x28 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x2 x61 (x1 (x23 x62 x62)) ⟶ (x2 (x39 x61 x60 x62) x62 ⟶ False) ⟶ (x2 (x38 x61 x60 x62) x62 ⟶ False) ⟶ (x0 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 x63 x64 x65 . (x59 x65 ⟶ False) ⟶ x60 = x3 x65 ⟶ x0 x64 x60 ⟶ x2 x61 x65 ⟶ x2 x63 x65 ⟶ x2 x62 x65 ⟶ x0 (x25 x61 x63) x64 ⟶ x0 (x25 x63 x62) x64 ⟶ (x0 (x25 x61 x62) x64 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 x63 x64 . (x59 x64 ⟶ False) ⟶ x60 = x3 x64 ⟶ x0 x63 x60 ⟶ x2 x61 x64 ⟶ x2 x62 x64 ⟶ (x0 (x25 x61 x62) x63 ⟶ False) ⟶ (x0 (x25 x62 x61) x63 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x59 x62 ⟶ False) ⟶ x60 = x3 x62 ⟶ x0 x61 x60 ⟶ (x2 x61 (x1 (x23 x62 x62)) ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x29 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ x22 x60 ⟶ (x36 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ x22 x60 ⟶ (x22 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x5 x61 ⟶ x2 x60 (x1 x61) ⟶ (x5 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x7 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x5 x61 ⟶ x2 x60 x61 ⟶ (x56 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x14 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x5 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x14 x61 ⟶ x2 x60 x61 ⟶ (x14 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x56 x60 ⟶ False) ⟶ x55 x60 ⟶ False) ⟶ (∀ x60 . x9 x60 ⟶ (x53 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x59 x62 ⟶ x2 x60 (x1 (x23 x61 x62)) ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x30 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x55 x60 ⟶ (x56 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x9 x60 ⟶ (x11 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x59 x62 ⟶ x2 x60 (x1 (x23 x62 x61)) ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x14 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ x13 x60 ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x7 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x17 x60 ⟶ (x9 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x9 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x2 x62 (x1 (x23 x60 x61)) ⟶ (x20 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x2 x62 (x1 (x23 x61 x60)) ⟶ (x47 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 . x16 x60 ⟶ x50 x60 ⟶ (x14 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x17 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x56 x61 ⟶ x2 x60 (x1 x61) ⟶ (x56 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x2 x62 (x1 (x23 x60 x61)) ⟶ (x22 x62 ⟶ False) ⟶ False) ⟶ (∀ x60 . x14 x60 ⟶ (x50 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x14 x60 ⟶ (x16 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x7 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x7 x60 ⟶ (x14 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x56 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x59 x61 ⟶ False) ⟶ x2 x60 (x3 x61) ⟶ (x22 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x29 x61 ⟶ x2 x60 (x1 x61) ⟶ (x29 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x0 x60 x61 ⟶ x0 x61 x60 ⟶ False) ⟶ (x4 x35 x34 x33 ⟶ False) ⟶ ((x4 x35 x31 x33 ⟶ False) ⟶ x4 x35 x33 x31 ⟶ False) ⟶ ((x4 x35 x34 x31 ⟶ False) ⟶ x4 x35 x31 x34 ⟶ False) ⟶ ((x2 x35 (x3 x32) ⟶ False) ⟶ False) ⟶ ((x2 x33 x32 ⟶ False) ⟶ False) ⟶ ((x2 x31 x32 ⟶ False) ⟶ False) ⟶ ((x2 x34 x32 ⟶ False) ⟶ False) ⟶ (x59 x32 ⟶ False) ⟶ False (proof)