Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../9dd1c..
PUWxN../78786..
vout
PrPhD../00976.. 3.41 bars
TMTp4../9c638.. ownership of 972b2.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMStQ../6873a.. ownership of 98005.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUXoA../3d5b6.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 972b2.. : ∀ 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 x62 . x60 x62 ⟶ (x62 = x61 ⟶ False) ⟶ x60 x61 ⟶ False) ⟶ (∀ x61 x62 . x0 x61 x62 ⟶ x60 x62 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x61 = x59 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x0 x61 x62 ⟶ x2 x62 (x1 x63) ⟶ x60 x63 ⟶ False) ⟶ (∀ x61 x62 x63 . x0 x62 x63 ⟶ x2 x63 (x1 x61) ⟶ (x2 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x3 x62 x61 ⟶ (x2 x62 (x1 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 (x1 x61) ⟶ (x3 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x61 x62 ⟶ (x60 x62 ⟶ False) ⟶ (x0 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x0 x61 (x55 x62 (x57 x64 x62 x63)) ⟶ (x56 (x57 x64 x62 x63) x61 = x56 x64 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x0 x62 x61 ⟶ (x2 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x3 x61 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x5 x62 x61 ⟶ (x55 x61 x62 = x4 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x53 x62 x61 ⟶ (x52 x61 x62 = x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x5 x62 x61 ⟶ (x6 x62 x61 = x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ (x52 x61 (x52 x61 x62) = x52 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ (x52 (x7 x61) x61 = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ (x6 (x6 x62 x61) x61 = x6 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ (x6 x61 (x4 x61) = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x54 (x51 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x5 (x51 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x50 (x51 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x58 (x51 x61) ⟶ False) ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ (x60 x48 ⟶ False) ⟶ (∀ x61 . (x47 x61 ⟶ False) ⟶ x47 (x46 x61) ⟶ False) ⟶ (∀ x61 . (x47 x61 ⟶ False) ⟶ (x2 (x46 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x54 (x45 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x53 (x45 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x5 (x45 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x58 (x45 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x47 (x44 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ x60 (x44 x61) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x2 (x44 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ (x8 x9 ⟶ False) ⟶ ((x54 x9 ⟶ False) ⟶ False) ⟶ ((x58 x9 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x42 (x43 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x2 (x43 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ ((x54 x41 ⟶ False) ⟶ False) ⟶ ((x50 x41 ⟶ False) ⟶ False) ⟶ ((x58 x41 ⟶ False) ⟶ False) ⟶ (x60 x41 ⟶ False) ⟶ (∀ x61 . x42 (x40 x61) x61 ⟶ False) ⟶ (∀ x61 . (x2 (x40 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x53 (x39 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x5 (x39 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x58 (x39 x61 x62) ⟶ False) ⟶ False) ⟶ ((x54 x10 ⟶ False) ⟶ False) ⟶ ((x50 x10 ⟶ False) ⟶ False) ⟶ ((x58 x10 ⟶ False) ⟶ False) ⟶ (x60 x38 ⟶ False) ⟶ (∀ x61 . (x60 (x11 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x2 (x11 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ ((x50 x12 ⟶ False) ⟶ False) ⟶ ((x58 x12 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x54 x14 ⟶ False) ⟶ False) ⟶ ((x58 x14 ⟶ False) ⟶ False) ⟶ ((x60 x37 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ x60 (x15 x61) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x2 (x15 x61) (x1 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x53 (x16 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x5 (x16 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x58 (x16 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 (x16 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x2 (x16 x61 x62) (x1 (x17 x62 x61)) ⟶ False) ⟶ False) ⟶ ((x58 x36 ⟶ False) ⟶ False) ⟶ (x60 x36 ⟶ False) ⟶ (∀ x61 x62 . (x54 (x35 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x53 (x35 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x5 (x35 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x58 (x35 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x2 (x35 x61 x62) (x1 (x17 x62 x61)) ⟶ False) ⟶ False) ⟶ ((x54 x18 ⟶ False) ⟶ False) ⟶ ((x58 x18 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x2 x64 (x1 (x17 x63 (x17 x61 x62))) ⟶ (x58 (x7 x64) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ x58 x61 ⟶ x60 (x7 x61) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x54 (x52 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x58 (x52 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x2 x64 (x1 (x17 (x17 x62 x61) x63)) ⟶ (x58 (x4 x64) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ x58 x61 ⟶ x60 (x4 x61) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x54 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x58 (x17 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x61 ⟶ (x53 (x52 x62 x63) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x62 ⟶ (x53 (x52 x61 x63) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x62 ⟶ (x58 (x52 x61 x63) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x61 ⟶ (x5 (x52 x62 x63) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x62 ⟶ (x58 (x52 x61 x63) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x61 ⟶ (x5 (x6 x63 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x62 ⟶ (x5 (x6 x63 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x62 ⟶ (x58 (x6 x63 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x61 ⟶ (x53 (x6 x63 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x62 ⟶ (x58 (x6 x63 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x47 x61 ⟶ x58 x61 ⟶ (x47 (x7 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x47 x61 ⟶ x58 x61 ⟶ (x47 (x4 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x34 x62 ⟶ (x34 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x34 x62 ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x62 ⟶ (x60 (x33 x62 x61) ⟶ False) ⟶ False) ⟶ ((x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 (x1 x61) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x60 x61 ⟶ (x60 (x33 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x34 x62 ⟶ x54 x62 ⟶ (x60 (x56 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x60 x61 ⟶ (x58 (x52 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x60 x61 ⟶ (x60 (x52 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x47 x61 ⟶ False) ⟶ x58 x61 ⟶ x54 x61 ⟶ x47 (x4 x61) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x62 ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x62 ⟶ (x60 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x49 x63 ⟶ x58 x61 ⟶ x53 x61 x63 ⟶ x54 x61 ⟶ (x54 (x56 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x49 x63 ⟶ x58 x61 ⟶ x53 x61 x63 ⟶ x54 x61 ⟶ (x58 (x56 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x60 x61 ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x60 x61 ⟶ (x60 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ x47 (x7 x61) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x54 x61 ⟶ x8 x61 ⟶ (x47 (x7 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x58 x62 ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x1 (x4 x62)) ⟶ x60 (x33 x62 x61) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x60 (x7 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x58 x62 ⟶ x50 x62 ⟶ x54 x62 ⟶ x2 x61 (x4 x62) ⟶ x60 (x56 x62 x61) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x60 (x17 x62 x61) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x58 x62 ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x1 (x4 x62)) ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x58 x62 ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x1 (x4 x62)) ⟶ x60 (x6 x62 x61) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x60 (x4 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x50 x61 ⟶ x54 x61 ⟶ (x19 (x7 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x2 (x32 x61) x61 ⟶ False) ⟶ False) ⟶ ((x60 x20 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ (x58 (x52 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ (x58 (x6 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x2 (x57 x63 x62 x61) (x1 (x17 x62 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x54 (x57 x63 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x5 x62 x61 ⟶ (x2 (x55 x61 x62) (x1 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x21 x61 x62 x63 = x56 x63 (x22 x61 x62 x63) ⟶ False) ⟶ (x0 (x21 x61 x62 x63) x61 ⟶ False) ⟶ (x61 = x33 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x0 (x22 x61 x62 x63) x62 ⟶ False) ⟶ (x0 (x21 x61 x62 x63) x61 ⟶ False) ⟶ (x61 = x33 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x0 (x22 x61 x62 x63) (x4 x63) ⟶ False) ⟶ (x0 (x21 x61 x62 x63) x61 ⟶ False) ⟶ (x61 = x33 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x0 (x21 x63 x62 x64) x63 ⟶ x0 x61 (x4 x64) ⟶ x0 x61 x62 ⟶ x21 x63 x62 x64 = x56 x64 x61 ⟶ (x63 = x33 x64 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 x65 . x58 x65 ⟶ x54 x65 ⟶ x64 = x33 x65 x63 ⟶ x0 x61 (x4 x65) ⟶ x0 x61 x63 ⟶ x62 = x56 x65 x61 ⟶ (x0 x62 x64 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x63 = x33 x64 x62 ⟶ x0 x61 x63 ⟶ (x61 = x56 x64 (x31 x61 x63 x62 x64) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x63 = x33 x64 x62 ⟶ x0 x61 x63 ⟶ (x0 (x31 x61 x63 x62 x64) x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x63 = x33 x64 x62 ⟶ x0 x61 x63 ⟶ (x0 (x31 x61 x63 x62 x64) (x4 x64) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x0 (x23 x61 x62) x61 ⟶ (x3 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 (x23 x61 x62) x62 ⟶ False) ⟶ (x3 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x3 x62 x63 ⟶ x0 x61 x62 ⟶ (x0 x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x30 x61 x62 = x56 x62 (x29 x61 x62) ⟶ False) ⟶ (x0 (x30 x61 x62) x61 ⟶ False) ⟶ (x61 = x7 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ (x0 (x29 x61 x62) (x4 x62) ⟶ False) ⟶ (x0 (x30 x61 x62) x61 ⟶ False) ⟶ (x61 = x7 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ x0 (x30 x62 x63) x62 ⟶ x0 x61 (x4 x63) ⟶ x30 x62 x63 = x56 x63 x61 ⟶ (x62 = x7 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . x58 x64 ⟶ x54 x64 ⟶ x63 = x7 x64 ⟶ x0 x61 (x4 x64) ⟶ x62 = x56 x64 x61 ⟶ (x0 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ x62 = x7 x63 ⟶ x0 x61 x62 ⟶ (x61 = x56 x63 (x28 x61 x62 x63) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ x62 = x7 x63 ⟶ x0 x61 x62 ⟶ (x0 (x28 x61 x62 x63) (x4 x63) ⟶ False) ⟶ False) ⟶ ((x59 = x20 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x5 x62 x61 ⟶ x55 x61 x62 = x61 ⟶ (x24 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x5 x62 x61 ⟶ x24 x62 x61 ⟶ (x55 x61 x62 = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x54 x63 ⟶ (x57 x63 x62 x61 = x6 (x52 x61 x63) x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x3 (x7 x62) x61 ⟶ (x53 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x53 x62 x61 ⟶ (x3 (x7 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x49 x62 ⟶ x2 x61 (x1 x62) ⟶ (x49 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x53 x61 x62 ⟶ (x53 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x53 x61 x62 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x53 x61 x62 ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x49 x62 ⟶ x2 x61 x62 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x49 x62 ⟶ x2 x61 x62 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x5 x61 x62 ⟶ (x5 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x5 x61 x62 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x58 x61 ⟶ x5 x61 x62 ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x49 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x53 x63 x61 ⟶ x2 x62 (x1 x63) ⟶ (x53 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x47 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x47 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x47 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x47 x62 ⟶ x2 x61 (x1 x62) ⟶ (x47 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x5 x63 x61 ⟶ x2 x62 (x1 x63) ⟶ (x5 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ x47 x61 ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x2 x61 (x1 x62) ⟶ x42 x61 x62 ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x2 x61 (x1 (x17 x62 x63)) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ (x50 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x8 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x2 x61 (x1 x62) ⟶ x60 x61 ⟶ (x42 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x2 x61 (x1 (x17 x63 x62)) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ (x34 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x54 x62 ⟶ x2 x61 (x1 x62) ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x2 x61 (x1 x62) ⟶ (x42 x61 x62 ⟶ False) ⟶ x60 x61 ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 (x1 (x17 x61 x62)) ⟶ (x53 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 (x1 (x17 x62 x61)) ⟶ (x5 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x2 x61 (x1 x62) ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ x60 x61 ⟶ x2 x62 (x1 (x17 x63 x61)) ⟶ x24 x62 x63 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x13 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x58 x61 ⟶ x54 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x2 x61 (x1 x62) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 (x1 (x17 x61 x62)) ⟶ (x58 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x2 x61 (x1 (x17 x63 x62)) ⟶ (x24 x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x0 x61 x62 ⟶ x0 x62 x61 ⟶ False) ⟶ (x3 (x33 x27 x26) x25 ⟶ False) ⟶ ((x24 (x57 x27 x26 x25) x26 ⟶ False) ⟶ False) ⟶ ((x54 x27 ⟶ False) ⟶ False) ⟶ ((x58 x27 ⟶ False) ⟶ False) ⟶ False (proof)