Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../225fa..
PUKRx../1f4ac..
vout
PrPhD../8aa72.. 3.37 bars
TMWzw../1580a.. ownership of c5192.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMKWy../84feb.. ownership of 627b6.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUcFQ../4e001.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c5192.. : ∀ 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 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ x58 x72 (x59 x71 x72) (x60 (x67 x72) (x67 x72) x71 (x59 x71 x72)) (x61 x71 x72) (x60 (x67 x72) (x67 x72) x71 (x61 x71 x72)) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ (x65 (x61 x71 x72) (x67 x72) ⟶ False) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ (x65 (x59 x71 x72) (x67 x72) ⟶ False) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x69 x74 ⟶ False) ⟶ x54 x74 ⟶ x68 x74 ⟶ x55 x71 ⟶ x66 x71 (x67 x74) (x67 x74) ⟶ x56 x71 (x67 x74) (x67 x74) ⟶ x65 x71 (x63 (x64 (x67 x74) (x67 x74))) ⟶ x57 x71 x74 ⟶ x62 x71 x74 ⟶ x65 x72 (x67 x74) ⟶ x65 x73 (x67 x74) ⟶ (x58 x74 x72 (x60 (x67 x74) (x67 x74) x71 x72) x73 (x60 (x67 x74) (x67 x74) x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 x76 . (x69 x76 ⟶ False) ⟶ x54 x76 ⟶ x68 x76 ⟶ x65 x71 (x67 x76) ⟶ x65 x75 (x67 x76) ⟶ x65 x72 (x67 x76) ⟶ x65 x74 (x67 x76) ⟶ x65 x73 (x67 x76) ⟶ x58 x76 x71 x75 x72 x74 ⟶ x58 x76 x71 x75 x72 x73 ⟶ x58 x76 x71 x72 x75 x74 ⟶ x58 x76 x71 x72 x75 x73 ⟶ (x53 x76 x71 x75 x72 ⟶ False) ⟶ (x74 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x71 = x1 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x58 x72 (x52 x71 x72) (x51 x71 x72) (x60 (x67 x72) (x67 x72) x71 (x52 x71 x72)) (x60 (x67 x72) (x67 x72) x71 (x51 x71 x72)) ⟶ (x57 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ (x65 (x51 x71 x72) (x67 x72) ⟶ False) ⟶ (x57 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ (x65 (x52 x71 x72) (x67 x72) ⟶ False) ⟶ (x57 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x69 x74 ⟶ False) ⟶ x54 x74 ⟶ x68 x74 ⟶ x55 x71 ⟶ x66 x71 (x67 x74) (x67 x74) ⟶ x56 x71 (x67 x74) (x67 x74) ⟶ x65 x71 (x63 (x64 (x67 x74) (x67 x74))) ⟶ x57 x71 x74 ⟶ x65 x73 (x67 x74) ⟶ x65 x72 (x67 x74) ⟶ (x58 x74 x73 x72 (x60 (x67 x74) (x67 x74) x71 x73) (x60 (x67 x74) (x67 x74) x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x71 x72 ⟶ x65 x72 (x63 x73) ⟶ x70 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x72 x73 ⟶ x65 x73 (x63 x71) ⟶ (x65 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x50 x72 x71 ⟶ (x65 x72 (x63 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x72 (x63 x71) ⟶ (x50 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x71 x72 ⟶ (x70 x72 ⟶ False) ⟶ (x0 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 x71 ⟶ (x65 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x55 x74 ⟶ x66 x74 x71 x72 ⟶ x65 x74 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x66 x73 x71 x72 ⟶ x65 x73 (x63 (x64 x71 x72)) ⟶ x49 x71 x72 x74 x73 ⟶ (x49 x71 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (x70 x2 ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x55 x74 ⟶ x66 x74 x71 x72 ⟶ x65 x74 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x66 x73 x71 x72 ⟶ x65 x73 (x63 (x64 x71 x72)) ⟶ (x49 x71 x72 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x50 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x55 x74 ⟶ x66 x74 x71 x72 ⟶ x65 x74 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x66 x73 x71 x72 ⟶ x65 x73 (x63 (x64 x71 x72)) ⟶ x74 = x73 ⟶ (x49 x71 x72 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x55 x74 ⟶ x66 x74 x71 x72 ⟶ x65 x74 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x66 x73 x71 x72 ⟶ x65 x73 (x63 (x64 x71 x72)) ⟶ x49 x71 x72 x74 x73 ⟶ (x74 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x48 x71 = x47 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x70 x74 ⟶ False) ⟶ x55 x71 ⟶ x66 x71 x74 x73 ⟶ x65 x71 (x63 (x64 x74 x73)) ⟶ x65 x72 x74 ⟶ (x60 x74 x73 x71 x72 = x3 x71 x72 ⟶ False) ⟶ False) ⟶ ((x46 x45 ⟶ False) ⟶ False) ⟶ (x70 x45 ⟶ False) ⟶ (∀ x71 x72 . (x55 (x44 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x4 (x44 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x43 (x44 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x44 x71 x72) ⟶ False) ⟶ False) ⟶ (x42 x41 ⟶ False) ⟶ ((x55 x41 ⟶ False) ⟶ False) ⟶ ((x5 x41 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ x70 (x7 x71) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ (x65 (x7 x71) (x63 (x67 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x70 (x9 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x55 (x9 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x4 (x9 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x43 (x9 x71 x72) x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x5 (x9 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x65 (x9 x71 x72) (x63 (x64 x72 x71)) ⟶ False) ⟶ False) ⟶ (x70 x10 ⟶ False) ⟶ (∀ x71 . (x40 (x39 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x11 (x39 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x38 (x39 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x12 (x39 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x37 (x39 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x4 (x39 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x43 (x39 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x39 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x65 (x39 x71) (x63 (x64 x71 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x56 (x13 x71) x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 (x13 x71) x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x40 (x13 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x55 (x13 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x4 (x13 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x43 (x13 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x13 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x65 (x13 x71) (x63 (x64 x71 x71)) ⟶ False) ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x55 x15 ⟶ False) ⟶ False) ⟶ ((x5 x15 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x69 x71 ⟶ False) ⟶ x8 x71 ⟶ x36 (x35 x71) ⟶ False) ⟶ (∀ x71 . (x69 x71 ⟶ False) ⟶ x8 x71 ⟶ (x65 (x35 x71) (x63 (x67 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ (x36 (x34 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ x70 (x34 x71) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ (x65 (x34 x71) (x63 (x67 x71)) ⟶ False) ⟶ False) ⟶ ((x70 x16 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x4 (x33 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x43 (x33 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x33 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 (x33 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x65 (x33 x71 x72) (x63 (x64 x72 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x55 (x17 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x4 (x17 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x43 (x17 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x17 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x65 (x17 x71 x72) (x63 (x64 x72 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x66 (x32 x71 x72) x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x55 (x32 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x4 (x32 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x43 (x32 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x32 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x65 (x32 x71 x72) (x63 (x64 x72 x71)) ⟶ False) ⟶ False) ⟶ ((x55 x31 ⟶ False) ⟶ False) ⟶ ((x5 x31 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x30 x71 ⟶ False) ⟶ x8 x71 ⟶ x29 (x67 x71) ⟶ False) ⟶ (∀ x71 . x30 x71 ⟶ x8 x71 ⟶ (x29 (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x69 x71 ⟶ x8 x71 ⟶ (x36 (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x47 x71) ⟶ False) ⟶ (∀ x71 . (x69 x71 ⟶ False) ⟶ x8 x71 ⟶ x36 (x67 x71) ⟶ False) ⟶ (∀ x71 . (x14 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x11 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x38 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x12 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x55 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x8 x71 ⟶ x70 (x67 x71) ⟶ False) ⟶ ((x70 x1 ⟶ False) ⟶ False) ⟶ (∀ x71 . x6 x71 ⟶ x8 x71 ⟶ (x70 (x67 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x46 x73 ⟶ x5 x71 ⟶ x4 x71 x73 ⟶ x55 x71 ⟶ (x55 (x3 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x46 x73 ⟶ x5 x71 ⟶ x4 x71 x73 ⟶ x55 x71 ⟶ (x5 (x3 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x40 (x47 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x55 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x43 (x47 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x65 (x18 x71) x71 ⟶ False) ⟶ False) ⟶ ((x8 x28 ⟶ False) ⟶ False) ⟶ ((x68 x19 ⟶ False) ⟶ False) ⟶ (∀ x71 . x68 x71 ⟶ (x8 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x65 (x48 x71) (x63 (x64 x71 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x40 (x48 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x47 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x70 x74 ⟶ False) ⟶ x55 x71 ⟶ x66 x71 x74 x73 ⟶ x65 x71 (x63 (x64 x74 x73)) ⟶ x65 x72 x74 ⟶ (x65 (x60 x74 x73 x71 x72) x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ (x20 x71 x72 = x60 (x67 x72) (x67 x72) x71 (x20 x71 x72) ⟶ False) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ (x65 (x20 x71 x72) (x67 x72) ⟶ False) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x57 x71 x72 ⟶ x49 (x67 x72) (x67 x72) x71 (x48 (x67 x72)) ⟶ (x62 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x69 x73 ⟶ False) ⟶ x54 x73 ⟶ x68 x73 ⟶ x55 x71 ⟶ x66 x71 (x67 x73) (x67 x73) ⟶ x56 x71 (x67 x73) (x67 x73) ⟶ x65 x71 (x63 (x64 (x67 x73) (x67 x73))) ⟶ x62 x71 x73 ⟶ (x49 (x67 x73) (x67 x73) x71 (x48 (x67 x73)) ⟶ False) ⟶ x65 x72 (x67 x73) ⟶ x72 = x60 (x67 x73) (x67 x73) x71 x72 ⟶ False) ⟶ (∀ x71 x72 . (x69 x72 ⟶ False) ⟶ x54 x72 ⟶ x68 x72 ⟶ x55 x71 ⟶ x66 x71 (x67 x72) (x67 x72) ⟶ x56 x71 (x67 x72) (x67 x72) ⟶ x65 x71 (x63 (x64 (x67 x72) (x67 x72))) ⟶ x62 x71 x72 ⟶ (x57 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x27 x71 x1 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x46 x72 ⟶ x65 x71 (x63 x72) ⟶ (x46 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x6 x71 ⟶ (x27 x71 x1 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x65 x72 (x63 (x64 x73 x71)) ⟶ x55 x72 ⟶ x66 x72 x73 x71 ⟶ (x66 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x65 x72 (x63 (x64 x73 x71)) ⟶ x55 x72 ⟶ x66 x72 x73 x71 ⟶ x70 x72 ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x65 x72 (x63 (x64 x73 x71)) ⟶ x55 x72 ⟶ x66 x72 x73 x71 ⟶ (x55 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x46 x72 ⟶ x65 x71 x72 ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x46 x72 ⟶ x65 x71 x72 ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x30 x71 ⟶ False) ⟶ x69 x71 ⟶ False) ⟶ (∀ x71 x72 . x65 x72 (x63 (x64 x71 x71)) ⟶ x37 x72 ⟶ x55 x72 ⟶ x40 x72 x71 ⟶ x66 x72 x71 x71 ⟶ (x56 x72 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x72 (x63 (x64 x71 x71)) ⟶ x37 x72 ⟶ x55 x72 ⟶ x40 x72 x71 ⟶ x66 x72 x71 x71 ⟶ (x66 x72 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x72 (x63 (x64 x71 x71)) ⟶ x37 x72 ⟶ x55 x72 ⟶ x40 x72 x71 ⟶ x66 x72 x71 x71 ⟶ (x55 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x46 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x69 x71 ⟶ (x30 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x14 x73 ⟶ x26 x73 x72 ⟶ (x56 x73 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x71 x72)) ⟶ x55 x73 ⟶ x14 x73 ⟶ x26 x73 x72 ⟶ (x55 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x36 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x42 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x36 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x36 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x30 x71 ⟶ False) ⟶ x30 x71 ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x30 x71 ⟶ False) ⟶ x6 x71 ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x72 x71)) ⟶ x55 x73 ⟶ x56 x73 x72 x71 ⟶ (x26 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x72 x71)) ⟶ x55 x73 ⟶ x56 x73 x72 x71 ⟶ (x14 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x72 x71)) ⟶ x55 x73 ⟶ x56 x73 x72 x71 ⟶ (x55 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 ⟶ x55 x71 ⟶ (x42 x71 ⟶ False) ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 ⟶ x55 x71 ⟶ (x42 x71 ⟶ False) ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 ⟶ x55 x71 ⟶ (x42 x71 ⟶ False) ⟶ x36 x71 ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x6 x71 ⟶ (x30 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x6 x71 ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x65 x71 (x63 (x64 x72 x73)) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x72 (x63 (x64 x71 x71)) ⟶ x66 x72 x71 x71 ⟶ (x40 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x42 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x65 x71 (x63 (x64 x73 x72)) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 ⟶ x12 x71 ⟶ x11 x71 ⟶ (x37 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 ⟶ x12 x71 ⟶ x11 x71 ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ x65 x71 (x63 (x64 x72 x73)) ⟶ x66 x71 x72 x73 ⟶ (x40 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 ⟶ x55 x72 ⟶ x65 x71 (x63 x72) ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x69 x71 ⟶ False) ⟶ x6 x71 ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x71 x72)) ⟶ (x4 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x72 x71)) ⟶ (x43 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ x70 x71 ⟶ x65 x72 (x63 (x64 x73 x71)) ⟶ x40 x72 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x65 x71 (x63 (x64 x73 x72)) ⟶ x66 x71 x73 x72 ⟶ (x40 x71 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x5 x71 ⟶ x55 x71 ⟶ (x5 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x6 x71 ⟶ (x69 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x73 (x63 (x64 x71 x72)) ⟶ (x5 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x65 x71 (x63 (x64 x73 x72)) ⟶ (x40 x71 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x72 (x63 (x64 x73 x71)) ⟶ x40 x72 x73 ⟶ (x66 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x55 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x69 x71 ⟶ False) ⟶ x6 x71 ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x27 x71 x2 ⟶ (x69 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ x27 x71 x2 ⟶ x6 x71 ⟶ False) ⟶ (∀ x71 . x8 x71 ⟶ (x6 x71 ⟶ False) ⟶ x69 x71 ⟶ (x27 x71 x2 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x71 x72 ⟶ x0 x72 x71 ⟶ False) ⟶ (x60 (x67 x24) (x67 x24) x21 x22 = x60 (x67 x24) (x67 x24) x23 x22 ⟶ False) ⟶ (x53 x24 x25 (x60 (x67 x24) (x67 x24) x21 x25) x22 ⟶ False) ⟶ ((x60 (x67 x24) (x67 x24) x21 x25 = x60 (x67 x24) (x67 x24) x23 x25 ⟶ False) ⟶ False) ⟶ ((x62 x23 x24 ⟶ False) ⟶ False) ⟶ ((x62 x21 x24 ⟶ False) ⟶ False) ⟶ ((x65 x23 (x63 (x64 (x67 x24) (x67 x24))) ⟶ False) ⟶ False) ⟶ ((x56 x23 (x67 x24) (x67 x24) ⟶ False) ⟶ False) ⟶ ((x66 x23 (x67 x24) (x67 x24) ⟶ False) ⟶ False) ⟶ ((x55 x23 ⟶ False) ⟶ False) ⟶ ((x65 x21 (x63 (x64 (x67 x24) (x67 x24))) ⟶ False) ⟶ False) ⟶ ((x56 x21 (x67 x24) (x67 x24) ⟶ False) ⟶ False) ⟶ ((x66 x21 (x67 x24) (x67 x24) ⟶ False) ⟶ False) ⟶ ((x55 x21 ⟶ False) ⟶ False) ⟶ ((x65 x22 (x67 x24) ⟶ False) ⟶ False) ⟶ ((x65 x25 (x67 x24) ⟶ False) ⟶ False) ⟶ ((x68 x24 ⟶ False) ⟶ False) ⟶ ((x54 x24 ⟶ False) ⟶ False) ⟶ (x69 x24 ⟶ False) ⟶ False (proof)