Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../d546c..
PUXuJ../21c3a..
vout
PrPhD../3d552.. 3.41 bars
TMMbG../01e9a.. ownership of 9e9e8.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMJ7X../d8e08.. ownership of 99c16.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUWxw../8a0a1.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 9e9e8.. : ∀ 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 : ι → ο . (∀ x63 x64 . x62 x64 ⟶ (x64 = x63 ⟶ False) ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x62 x64 ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x63 = x61 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x63 x64 ⟶ x2 x64 (x1 x65) ⟶ x62 x65 ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x57 x65 (x58 x65 x63 x64) = x56 (x55 x65) (x57 x65 x63) (x57 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x3 x65 (x58 x65 x63 x64) = x56 (x55 x65) (x3 x65 x63) (x3 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x57 x65 (x52 x65 x63 x64) = x51 (x55 x65) (x57 x65 x63) (x57 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x3 x65 (x52 x65 x63 x64) = x51 (x55 x65) (x3 x65 x63) (x3 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x64 x65 ⟶ x2 x65 (x1 x63) ⟶ (x2 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x4 x64 x63 ⟶ (x2 x64 (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x2 x64 (x1 x63) ⟶ (x4 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x2 x63 x64 ⟶ (x62 x64 ⟶ False) ⟶ (x0 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x50 x63 x61 = x61 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x50 x63 (x5 x63 x64) = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x64 x63 ⟶ (x2 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x5 x63 x61 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x49 x65 x63 x64 ⟶ (x49 x65 x64 x63 ⟶ False) ⟶ False) ⟶ (x62 x6 ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x49 x65 x63 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x4 x63 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x63 = x64 ⟶ (x49 x65 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x49 x65 x63 x64 ⟶ (x63 = x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x2 x63 (x1 x65) ⟶ x2 x64 x63 ⟶ (x48 x64 x65 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x2 x63 (x1 x65) ⟶ x48 x64 x65 x63 ⟶ (x2 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ (x56 x65 x63 x64 = x50 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x7 x63 = x1 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 x66 . x2 x65 (x1 x66) ⟶ x2 x64 (x1 x63) ⟶ (x46 x66 x63 x65 x64 = x47 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x51 x65 x64 x63 = x5 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x45 x63 ⟶ (x42 (x43 x63) (x44 x63) = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x44 (x42 x64 x63) = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x43 (x42 x63 x64) = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x8 x63 ⟶ False) ⟶ x8 (x9 x63) ⟶ False) ⟶ (∀ x63 . (x8 x63 ⟶ False) ⟶ (x2 (x9 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x8 (x10 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x62 (x10 x63) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x2 (x10 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x40 (x41 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x2 (x41 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ x62 (x39 x63) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ (x2 (x39 x63) (x1 (x55 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . x40 (x37 x63) x63 ⟶ False) ⟶ (∀ x63 . (x2 (x37 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (x62 x36 ⟶ False) ⟶ (∀ x63 . (x62 (x11 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x2 (x11 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x12 x63 ⟶ False) ⟶ x38 x63 ⟶ x8 (x13 x63) ⟶ False) ⟶ (∀ x63 . (x12 x63 ⟶ False) ⟶ x38 x63 ⟶ (x2 (x13 x63) (x1 (x55 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ (x8 (x14 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ x62 (x14 x63) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ (x2 (x14 x63) (x1 (x55 x63)) ⟶ False) ⟶ False) ⟶ ((x45 x35 ⟶ False) ⟶ False) ⟶ ((x62 x15 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x62 (x34 x63) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x2 (x34 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x33 (x32 x63 x64) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x16 (x32 x64 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x31 (x32 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 (x32 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x2 (x32 x63 x64) (x1 (x47 x64 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x63 (x1 x65) ⟶ (x56 x65 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x51 x65 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x50 x63 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x5 x63 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x17 x63 ⟶ False) ⟶ x38 x63 ⟶ x18 (x55 x63) ⟶ False) ⟶ (∀ x63 . x17 x63 ⟶ x38 x63 ⟶ (x18 (x55 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x12 x63 ⟶ x38 x63 ⟶ (x8 (x55 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x12 x63 ⟶ False) ⟶ x38 x63 ⟶ x8 (x55 x63) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x62 (x5 x63 x64) ⟶ False) ⟶ (∀ x63 x64 x65 . x31 x65 ⟶ x33 x65 x63 ⟶ x31 x64 ⟶ (x33 (x50 x65 x64) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x62 (x5 x64 x63) ⟶ False) ⟶ (∀ x63 x64 x65 . x31 x65 ⟶ x33 x65 x63 ⟶ x31 x64 ⟶ x33 x64 x63 ⟶ (x33 (x5 x65 x64) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x62 (x19 x63 x64) ⟶ False) ⟶ (∀ x63 . x62 (x30 x63) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x38 x63 ⟶ x62 (x55 x63) ⟶ False) ⟶ (∀ x63 x64 x65 . x31 x65 ⟶ x16 x65 x63 ⟶ x31 x64 ⟶ (x16 (x50 x65 x64) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x45 (x42 x63 x64) ⟶ False) ⟶ False) ⟶ ((x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 (x1 x63) ⟶ False) ⟶ (∀ x63 . x60 x63 ⟶ x38 x63 ⟶ (x62 (x55 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x31 x65 ⟶ x16 x65 x63 ⟶ x31 x64 ⟶ x16 x64 x63 ⟶ (x16 (x5 x65 x64) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x62 (x47 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x2 x63 (x1 x64) ⟶ (x48 (x20 x63 x64) x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x60 x63 ⟶ False) ⟶ x53 x63 ⟶ x59 x63 ⟶ (x54 (x29 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x2 (x21 x63) x63 ⟶ False) ⟶ False) ⟶ ((x38 x28 ⟶ False) ⟶ False) ⟶ ((x59 x22 ⟶ False) ⟶ False) ⟶ ((x62 x27 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x62 x65 ⟶ False) ⟶ (x62 x63 ⟶ False) ⟶ x2 x63 (x1 x65) ⟶ x48 x64 x65 x63 ⟶ (x2 x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x60 x64 ⟶ False) ⟶ x53 x64 ⟶ x59 x64 ⟶ x54 x63 x64 ⟶ (x48 x63 (x47 (x1 (x55 x64)) (x1 (x55 x64))) (x46 (x1 (x55 x64)) (x1 (x55 x64)) (x7 (x55 x64)) (x7 (x55 x64))) ⟶ False) ⟶ False) ⟶ (∀ x63 . x59 x63 ⟶ (x38 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ (x2 (x56 x65 x63 x64) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x2 (x7 x63) (x1 (x1 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 x66 . x2 x65 (x1 x66) ⟶ x2 x64 (x1 x63) ⟶ (x2 (x46 x66 x63 x65 x64) (x1 (x47 x66 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x2 (x51 x65 x64 x63) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x54 (x58 x65 x63 x64) x65 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x54 (x52 x65 x63 x64) x65 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x60 x64 ⟶ False) ⟶ x53 x64 ⟶ x59 x64 ⟶ x54 x63 x64 ⟶ (x2 (x57 x64 x63) (x1 (x55 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x60 x64 ⟶ False) ⟶ x53 x64 ⟶ x59 x64 ⟶ x54 x63 x64 ⟶ (x2 (x3 x64 x63) (x1 (x55 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x42 x64 x63 = x19 (x19 x64 x63) (x30 x64) ⟶ False) ⟶ False) ⟶ ((x61 = x27 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x58 x65 x63 x64 = x42 (x56 (x55 x65) (x3 x65 x63) (x3 x65 x64)) (x56 (x55 x65) (x57 x65 x63) (x57 x65 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ (x52 x65 x63 x64 = x42 (x51 (x55 x65) (x3 x65 x63) (x3 x65 x64)) (x51 (x55 x65) (x57 x65 x63) (x57 x65 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x3 x65 x63 = x3 x65 x64 ⟶ x57 x65 x63 = x57 x65 x64 ⟶ (x49 x65 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x49 x65 x63 x64 ⟶ (x57 x65 x63 = x57 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . (x60 x65 ⟶ False) ⟶ x53 x65 ⟶ x59 x65 ⟶ x54 x63 x65 ⟶ x54 x64 x65 ⟶ x49 x65 x63 x64 ⟶ (x3 x65 x63 = x3 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x60 x64 ⟶ False) ⟶ x53 x64 ⟶ x59 x64 ⟶ x54 x63 x64 ⟶ (x57 x64 x63 = x44 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x60 x64 ⟶ False) ⟶ x53 x64 ⟶ x59 x64 ⟶ x54 x63 x64 ⟶ (x3 x64 x63 = x43 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ (x56 x65 x63 x64 = x56 x65 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x51 x65 x64 x63 = x51 x65 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x50 x64 x63 = x50 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x5 x64 x63 = x5 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x19 x64 x63 = x19 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x26 x63 x61 ⟶ (x60 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x60 x63 ⟶ (x26 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x17 x63 ⟶ False) ⟶ x12 x63 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x12 x63 ⟶ (x17 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x2 x63 (x1 x64) ⟶ (x8 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x17 x63 ⟶ False) ⟶ x17 x63 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x17 x63 ⟶ False) ⟶ x60 x63 ⟶ False) ⟶ (∀ x63 x64 . x62 x64 ⟶ x2 x63 (x1 x64) ⟶ x40 x63 x64 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x60 x63 ⟶ (x17 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x60 x63 ⟶ (x60 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x62 x65 ⟶ x2 x63 (x1 (x47 x64 x65)) ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x2 x63 (x1 x64) ⟶ x62 x63 ⟶ (x40 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x62 x65 ⟶ x2 x63 (x1 (x47 x65 x64)) ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x2 x63 (x1 x64) ⟶ (x40 x63 x64 ⟶ False) ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x12 x63 ⟶ False) ⟶ x60 x63 ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x65 (x1 (x47 x63 x64)) ⟶ (x33 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x65 (x1 (x47 x64 x63)) ⟶ (x16 x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x62 x64 ⟶ x2 x63 (x1 x64) ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x60 x63 ⟶ (x12 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x65 (x1 (x47 x63 x64)) ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x12 x63 ⟶ False) ⟶ x60 x63 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x26 x63 x6 ⟶ (x12 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ x26 x63 x6 ⟶ x60 x63 ⟶ False) ⟶ (∀ x63 . x38 x63 ⟶ (x60 x63 ⟶ False) ⟶ x12 x63 ⟶ (x26 x63 x6 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x0 x64 x63 ⟶ False) ⟶ (x49 x23 (x58 x23 x25 (x52 x23 x25 x24)) x25 ⟶ False) ⟶ ((x54 x24 x23 ⟶ False) ⟶ False) ⟶ ((x54 x25 x23 ⟶ False) ⟶ False) ⟶ ((x59 x23 ⟶ False) ⟶ False) ⟶ ((x53 x23 ⟶ False) ⟶ False) ⟶ (x60 x23 ⟶ False) ⟶ False (proof)