Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../acf28..
PUMd4../fcbaf..
vout
PrPhD../d7730.. 3.41 bars
TMH9f../6a4d1.. ownership of 95a21.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMZCS../29da6.. ownership of 9cfac.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUMgb../3901a.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 95a21.. : ∀ 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 : ι → ι → ο . ∀ x65 : ι → ι → ι . ∀ x66 : ι → ι → ο . ∀ x67 : ι → ι . ∀ x68 : ι → ι → ι . ∀ x69 : ι → ι → ο . ∀ x70 : ι → ο . (∀ x71 x72 . x70 x72 ⟶ (x72 = x71 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 x72 . x0 x71 x72 ⟶ x70 x72 ⟶ False) ⟶ (∀ x71 x72 . (x69 (x68 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x71 = x1 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x71 x72 ⟶ x66 x72 (x67 x73) ⟶ x70 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x72 x73 ⟶ x66 x73 (x67 x71) ⟶ (x66 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x68 x1 x71 = x1 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x72 x73 ⟶ x0 x72 x71 ⟶ x69 x73 x71 ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 x71 ⟶ False) ⟶ (x0 (x65 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x71 x72 ⟶ False) ⟶ (x0 (x65 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x64 x72 x71 ⟶ (x66 x72 (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x66 x72 (x67 x71) ⟶ (x64 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x0 x71 (x62 x72) ⟶ (x0 (x61 x72 x71) (x60 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x68 x71 x1 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 x71 ⟶ (x64 (x58 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x64 (x58 x72) x71 ⟶ (x0 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x66 x71 x72 ⟶ (x70 x72 ⟶ False) ⟶ (x0 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x2 x71 x1 = x1 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ x57 x72 ⟶ x57 x71 ⟶ (x61 x71 (x55 x71 x72) = x61 x72 (x54 x71 x72) ⟶ False) ⟶ (x57 (x56 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ x57 x72 ⟶ x57 x71 ⟶ (x0 (x54 x71 x72) (x3 (x62 x72) (x62 x71)) ⟶ False) ⟶ (x57 (x56 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ x57 x72 ⟶ x57 x71 ⟶ (x0 (x55 x71 x72) (x62 x71) ⟶ False) ⟶ (x57 (x56 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 x71 ⟶ (x66 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x64 (x2 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x69 x71 x72 ⟶ (x69 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x3 x71 x72 = x68 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x53 x71 ⟶ False) ⟶ x53 (x52 x71) ⟶ False) ⟶ (∀ x71 . (x53 x71 ⟶ False) ⟶ (x66 (x52 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x53 (x51 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x51 x71) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x66 (x51 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ ((x4 x5 ⟶ False) ⟶ False) ⟶ (x70 x5 ⟶ False) ⟶ ((x6 x5 ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x70 x49 ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ ((x50 x47 ⟶ False) ⟶ False) ⟶ ((x46 x47 ⟶ False) ⟶ False) ⟶ ((x70 x47 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x44 (x45 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x66 (x45 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ ((x43 x42 ⟶ False) ⟶ False) ⟶ ((x50 x42 ⟶ False) ⟶ False) ⟶ ((x48 x41 ⟶ False) ⟶ False) ⟶ ((x43 x41 ⟶ False) ⟶ False) ⟶ ((x50 x41 ⟶ False) ⟶ False) ⟶ ((x46 x41 ⟶ False) ⟶ False) ⟶ (∀ x71 . x44 (x40 x71) x71 ⟶ False) ⟶ (∀ x71 . (x66 (x40 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ ((x7 x38 ⟶ False) ⟶ False) ⟶ (x70 x38 ⟶ False) ⟶ (x53 x8 ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ ((x50 x36 ⟶ False) ⟶ False) ⟶ ((x48 x35 ⟶ False) ⟶ False) ⟶ ((x37 x35 ⟶ False) ⟶ False) ⟶ ((x50 x35 ⟶ False) ⟶ False) ⟶ ((x46 x35 ⟶ False) ⟶ False) ⟶ (x70 x34 ⟶ False) ⟶ (∀ x71 . (x70 (x9 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 (x9 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ ((x7 x10 ⟶ False) ⟶ False) ⟶ (x70 x10 ⟶ False) ⟶ ((x53 x11 ⟶ False) ⟶ False) ⟶ (x70 x11 ⟶ False) ⟶ ((x50 x12 ⟶ False) ⟶ False) ⟶ ((x48 x33 ⟶ False) ⟶ False) ⟶ ((x70 x13 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x32 x71) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x66 (x32 x71) (x67 x71) ⟶ False) ⟶ False) ⟶ ((x7 x31 ⟶ False) ⟶ False) ⟶ (x70 x31 ⟶ False) ⟶ (∀ x71 . (x2 x71 x71 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ (x56 x72 x72 = x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x48 x71 ⟶ (x30 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ (x6 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x46 x71 ⟶ (x29 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x7 x72 ⟶ (x7 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x28 x72 ⟶ (x28 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ (x14 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x30 x72 ⟶ (x30 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ (x6 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x29 x72 ⟶ (x29 (x68 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x7 x72 ⟶ (x7 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x7 x72 ⟶ (x7 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x28 x72 ⟶ (x28 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x28 x72 ⟶ (x28 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ (x14 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ (x14 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x30 x72 ⟶ (x30 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x30 x72 ⟶ (x30 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ (x6 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ (x6 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x29 x72 ⟶ (x29 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x29 x72 ⟶ (x29 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x53 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 (x58 x71) ⟶ False) ⟶ ((x70 x1 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 (x67 x71) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ x4 x72 ⟶ x6 x71 ⟶ x4 x71 ⟶ (x4 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x27 x71 ⟶ (x7 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x15 x71 ⟶ (x28 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x26 x71 ⟶ (x14 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 (x16 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x66 (x3 x71 x72) (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ (x59 (x56 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x63 x72 ⟶ x59 x72 ⟶ x63 x71 ⟶ x59 x71 ⟶ (x63 (x56 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x0 (x17 x71 x72 x73) x72 ⟶ False) ⟶ (x0 (x17 x71 x72 x73) x71 ⟶ False) ⟶ (x71 = x2 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x0 (x17 x71 x72 x73) x73 ⟶ False) ⟶ (x0 (x17 x71 x72 x73) x71 ⟶ False) ⟶ (x71 = x2 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 (x17 x71 x72 x73) x71 ⟶ x0 (x17 x71 x72 x73) x73 ⟶ x0 (x17 x71 x72 x73) x72 ⟶ (x71 = x2 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x74 = x2 x72 x73 ⟶ x0 x71 x72 ⟶ x0 x71 x73 ⟶ (x0 x71 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x72 = x2 x71 x73 ⟶ x0 x74 x72 ⟶ (x0 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x72 = x2 x73 x71 ⟶ x0 x74 x72 ⟶ (x0 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x63 x71 ⟶ x59 x71 ⟶ x18 x71 = x19 x71 ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x63 x71 ⟶ x59 x71 ⟶ (x61 x71 (x18 x71) = x61 x71 (x19 x71) ⟶ False) ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x63 x71 ⟶ x59 x71 ⟶ (x0 (x19 x71) (x62 x71) ⟶ False) ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x63 x71 ⟶ x59 x71 ⟶ (x0 (x18 x71) (x62 x71) ⟶ False) ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x63 x73 ⟶ x59 x73 ⟶ x57 x73 ⟶ x0 x71 (x62 x73) ⟶ x0 x72 (x62 x73) ⟶ x61 x73 x71 = x61 x73 x72 ⟶ (x71 = x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x25 x72 x71 = x71 ⟶ False) ⟶ (x0 (x25 x72 x71) x72 ⟶ False) ⟶ (x72 = x58 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 (x25 x72 x71) x72 ⟶ x25 x72 x71 = x71 ⟶ (x72 = x58 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x72 = x58 x73 ⟶ x71 = x73 ⟶ (x0 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x72 = x58 x73 ⟶ x0 x71 x72 ⟶ (x71 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x2 x72 x71 = x2 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x28 x71 ⟶ (x70 x71 ⟶ False) ⟶ x20 x71 ⟶ (x21 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x28 x71 ⟶ (x70 x71 ⟶ False) ⟶ x20 x71 ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x28 x71 ⟶ (x70 x71 ⟶ False) ⟶ x20 x71 ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ (x37 x71 ⟶ False) ⟶ (x43 x71 ⟶ False) ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ (x37 x71 ⟶ False) ⟶ (x43 x71 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x50 x71 ⟶ x43 x71 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x50 x71 ⟶ x37 x71 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x50 x71 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x50 x71 ⟶ (x37 x71 ⟶ False) ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x50 x71 ⟶ (x37 x71 ⟶ False) ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x43 x71 ⟶ x37 x71 ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x43 x71 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x43 x71 ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 x72 . x53 x72 ⟶ x66 x71 (x67 x72) ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x30 x71 ⟶ (x29 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x50 x71 ⟶ (x43 x71 ⟶ False) ⟶ (x37 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x50 x71 ⟶ (x43 x71 ⟶ False) ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x48 x71 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x66 x71 (x67 x72) ⟶ x44 x71 x72 ⟶ False) ⟶ (∀ x71 . x30 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x70 x71 ⟶ False) ⟶ (x21 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x70 x71 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x70 x71 ⟶ False) ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x37 x71 ⟶ x43 x71 ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x37 x71 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x50 x71 ⟶ x37 x71 ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x48 x71 ⟶ (x46 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x66 x71 (x67 x72) ⟶ x70 x71 ⟶ (x44 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ (x30 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x53 x71 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x27 x71 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x27 x71 ⟶ (x48 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x66 x71 (x67 x72) ⟶ (x44 x71 x72 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x28 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x39 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x7 x72 ⟶ x66 x71 (x67 x72) ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x28 x72 ⟶ x66 x71 (x67 x72) ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ x66 x71 (x67 x72) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x30 x72 ⟶ x66 x71 (x67 x72) ⟶ (x30 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ x66 x71 (x67 x72) ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x66 x71 (x67 x72) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x7 x71 ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x29 x72 ⟶ x66 x71 (x67 x72) ⟶ (x29 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x7 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x7 x72 ⟶ x66 x71 x72 ⟶ (x27 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x21 x71 ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x21 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x28 x72 ⟶ x66 x71 x72 ⟶ (x15 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x70 x71 ⟶ (x4 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x70 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ x66 x71 x72 ⟶ (x26 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x30 x72 ⟶ x66 x71 x72 ⟶ (x48 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ x66 x71 x72 ⟶ (x50 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x29 x72 ⟶ x66 x71 x72 ⟶ (x46 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x30 x71 ⟶ x21 x71 ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x30 x71 ⟶ x21 x71 ⟶ (x30 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x71 x72 ⟶ x0 x72 x71 ⟶ False) ⟶ (x57 (x56 x23 x22) ⟶ False) ⟶ ((x2 (x60 x23) (x60 x22) = x58 (x61 x23 x24) ⟶ False) ⟶ False) ⟶ ((x2 (x62 x23) (x62 x22) = x58 x24 ⟶ False) ⟶ False) ⟶ ((x57 x22 ⟶ False) ⟶ False) ⟶ ((x57 x23 ⟶ False) ⟶ False) ⟶ ((x59 x22 ⟶ False) ⟶ False) ⟶ ((x63 x22 ⟶ False) ⟶ False) ⟶ ((x59 x23 ⟶ False) ⟶ False) ⟶ ((x63 x23 ⟶ False) ⟶ False) ⟶ False (proof)