Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../bb9cc..
PUe9v../affb3..
vout
PrNUD../1a6da.. 0.03 bars
TMLPG../cf99f.. ownership of 4f28e.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMWee../cc39b.. ownership of 603d9.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUXFL../5a746.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 4f28e.. : ∀ 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 : ι → ο . (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x73 = x67 (x68 x74 x74 (x69 x74 x73) (x70 x74 x73)) (x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ (x74 = x73 ⟶ False) ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 x74 . x64 x73 x74 ⟶ x72 x74 ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x73 = x0 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x64 x73 x74 ⟶ x66 x74 (x63 x75) ⟶ x72 x75 ⟶ False) ⟶ (∀ x73 x74 x75 . x64 x74 x75 ⟶ x66 x75 (x63 x73) ⟶ (x66 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x62 x74 x73 ⟶ (x66 x74 (x63 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x66 x74 (x63 x73) ⟶ (x62 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x64 x74 x75 ⟶ x64 x73 x75 ⟶ x64 x73 (x61 x75 x74) ⟶ False) ⟶ (∀ x73 x74 . x64 x74 x73 ⟶ (x64 (x61 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x66 x73 x74 ⟶ (x72 x74 ⟶ False) ⟶ (x64 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x67 x74 x76 = x67 x73 x75 ⟶ (x76 = x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x67 x76 x74 = x67 x75 x73 ⟶ (x76 = x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x64 x74 x73 ⟶ (x66 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x62 x73 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x66 x75 x76 ⟶ x66 x74 x73 ⟶ (x68 x76 x73 x75 x74 = x67 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 . x60 x73 ⟶ (x67 (x59 x73) (x71 x73) = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x71 (x67 x74 x73) = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x59 (x67 x73 x74) = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x1 (x2 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x58 (x2 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x3 (x2 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x57 (x2 x73) ⟶ False) ⟶ False) ⟶ ((x4 x5 ⟶ False) ⟶ False) ⟶ (x72 x5 ⟶ False) ⟶ (∀ x73 . (x6 x73 ⟶ False) ⟶ x6 (x7 x73) ⟶ False) ⟶ (∀ x73 . (x6 x73 ⟶ False) ⟶ (x66 (x7 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x1 (x8 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x56 (x8 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x58 (x8 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x8 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x6 (x9 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x9 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x66 (x9 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ (x55 x54 ⟶ False) ⟶ ((x1 x54 ⟶ False) ⟶ False) ⟶ ((x57 x54 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x11 (x10 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x66 (x10 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ ((x1 x12 ⟶ False) ⟶ False) ⟶ ((x3 x12 ⟶ False) ⟶ False) ⟶ ((x57 x12 ⟶ False) ⟶ False) ⟶ (x72 x12 ⟶ False) ⟶ (∀ x73 . x11 (x13 x73) x73 ⟶ False) ⟶ (∀ x73 . (x66 (x13 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x56 (x14 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x58 (x14 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x14 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x72 (x53 x73 x74) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x1 (x53 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x56 (x53 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x58 (x53 x73 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x57 (x53 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ (x66 (x53 x73 x74) (x63 (x15 x74 x73)) ⟶ False) ⟶ False) ⟶ ((x1 x52 ⟶ False) ⟶ False) ⟶ ((x3 x52 ⟶ False) ⟶ False) ⟶ ((x57 x52 ⟶ False) ⟶ False) ⟶ (x72 x16 ⟶ False) ⟶ (∀ x73 . (x72 (x51 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x66 (x51 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ ((x3 x50 ⟶ False) ⟶ False) ⟶ ((x57 x50 ⟶ False) ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x1 x48 ⟶ False) ⟶ False) ⟶ ((x57 x48 ⟶ False) ⟶ False) ⟶ ((x60 x17 ⟶ False) ⟶ False) ⟶ ((x72 x47 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x18 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x66 (x18 x73) (x63 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x56 (x19 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x58 (x19 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x19 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 (x19 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x66 (x19 x73 x74) (x63 (x15 x74 x73)) ⟶ False) ⟶ False) ⟶ ((x57 x46 ⟶ False) ⟶ False) ⟶ (x72 x46 ⟶ False) ⟶ (∀ x73 x74 . (x1 (x45 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x56 (x45 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x58 (x45 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x45 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x66 (x45 x73 x74) (x63 (x15 x74 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x20 (x21 x73 x74) x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x1 (x21 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x56 (x21 x73 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x58 (x21 x74 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x21 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x66 (x21 x73 x74) (x63 (x15 x74 x73)) ⟶ False) ⟶ False) ⟶ ((x1 x22 ⟶ False) ⟶ False) ⟶ ((x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 x77 . (x72 x77 ⟶ False) ⟶ x66 x73 x77 ⟶ x66 x76 x77 ⟶ x66 x74 (x24 x77) ⟶ x75 = x68 (x15 x77 x77) (x24 x77) (x68 x77 x77 x73 x76) x74 ⟶ x64 (x68 (x15 x77 x77) (x24 x77) (x68 x77 x77 x73 x76) x74) (x65 x77) ⟶ (x64 x75 (x23 x77 x73 x76) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x66 x73 x76 ⟶ x66 x75 x76 ⟶ x64 x74 (x23 x76 x73 x75) ⟶ (x64 (x68 (x15 x76 x76) (x24 x76) (x68 x76 x76 x73 x75) (x44 x75 x73 x76 x74)) (x65 x76) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x66 x73 x76 ⟶ x66 x75 x76 ⟶ x64 x74 (x23 x76 x73 x75) ⟶ (x74 = x68 (x15 x76 x76) (x24 x76) (x68 x76 x76 x73 x75) (x44 x75 x73 x76 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x66 x73 x76 ⟶ x66 x75 x76 ⟶ x64 x74 (x23 x76 x73 x75) ⟶ (x66 (x44 x75 x73 x76 x74) (x24 x76) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 x77 . (x72 x77 ⟶ False) ⟶ x66 x73 x77 ⟶ x66 x76 x77 ⟶ x66 x74 (x24 x77) ⟶ x75 = x68 (x15 x77 x77) (x24 x77) (x68 x77 x77 x73 x76) x74 ⟶ x73 = x0 ⟶ x1 x74 ⟶ x20 x74 x73 x76 ⟶ x66 x74 (x63 (x15 x73 x76)) ⟶ (x64 x75 (x25 x77) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 x77 . (x72 x77 ⟶ False) ⟶ x66 x73 x77 ⟶ x66 x76 x77 ⟶ x66 x74 (x24 x77) ⟶ x75 = x68 (x15 x77 x77) (x24 x77) (x68 x77 x77 x73 x76) x74 ⟶ (x76 = x0 ⟶ False) ⟶ x1 x74 ⟶ x20 x74 x73 x76 ⟶ x66 x74 (x63 (x15 x73 x76)) ⟶ (x64 x75 (x25 x77) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x66 (x26 x74 x73) (x63 (x15 (x27 x74 x73) (x28 x74 x73))) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x20 (x26 x74 x73) (x27 x74 x73) (x28 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x1 (x26 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ x28 x74 x73 = x0 ⟶ (x27 x74 x73 = x0 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x73 = x68 (x15 x74 x74) (x24 x74) (x68 x74 x74 (x27 x74 x73) (x28 x74 x73)) (x26 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x66 (x26 x74 x73) (x24 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x66 (x28 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x25 x74) ⟶ (x66 (x27 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ x66 x73 x76 ⟶ x66 x75 x76 ⟶ x74 = x30 x73 x75 ⟶ (x64 x74 (x29 x76) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x29 x74) ⟶ (x73 = x30 (x42 x74 x73) (x43 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x29 x74) ⟶ (x66 (x43 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x64 x73 (x29 x74) ⟶ (x66 (x42 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x57 (x31 (x67 x74 x73) (x67 x76 x75)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x15 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x57 (x32 (x67 x74 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 (x31 x73 x74) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x72 x73 ⟶ (x72 (x30 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x1 (x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x57 (x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 (x32 x73) ⟶ False) ⟶ (∀ x73 . x72 (x30 x73 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x65 x73) ⟶ False) ⟶ (∀ x73 x74 . (x60 (x67 x73 x74) ⟶ False) ⟶ False) ⟶ ((x72 x0 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 (x63 x73) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x72 (x30 x73 x74) ⟶ False) ⟶ (∀ x73 x74 . (x1 (x32 (x67 x74 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x72 (x24 x73) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x4 (x24 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x57 x74 ⟶ x1 x74 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x4 (x31 x74 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x57 x73 ⟶ x1 x73 ⟶ (x4 (x32 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x72 (x15 x74 x73) ⟶ False) ⟶ (∀ x73 x74 . (x4 (x30 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x66 (x41 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x66 (x70 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x66 (x69 x74 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x72 x76 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x66 x75 x76 ⟶ x66 x74 x73 ⟶ (x66 (x68 x76 x73 x75 x74) (x15 x76 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ x66 x73 x75 ⟶ x66 x74 x75 ⟶ (x40 x75 x73 x74 = x23 x75 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x67 x74 x73 = x31 (x31 x74 x73) (x32 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x70 x74 x73 = x71 (x59 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x65 x74) ⟶ (x69 x74 x73 = x59 (x59 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x65 x73 = x25 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x24 x73 = x33 (x29 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x31 x74 x73 = x31 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x4 x74 ⟶ x66 x73 (x63 x74) ⟶ (x4 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x56 x73 x74 ⟶ (x56 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x56 x73 x74 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x56 x73 x74 ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x66 x74 (x63 (x15 x75 x73)) ⟶ x1 x74 ⟶ x20 x74 x75 x73 ⟶ (x20 x74 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x66 x74 (x63 (x15 x75 x73)) ⟶ x1 x74 ⟶ x20 x74 x75 x73 ⟶ x72 x74 ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x66 x74 (x63 (x15 x75 x73)) ⟶ x1 x74 ⟶ x20 x74 x75 x73 ⟶ (x1 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x4 x74 ⟶ x66 x73 x74 ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x4 x74 ⟶ x66 x73 x74 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x58 x73 x74 ⟶ (x58 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x58 x73 x74 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x57 x73 ⟶ x58 x73 x74 ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x4 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x57 x75 ⟶ x56 x75 x73 ⟶ x66 x74 (x63 x75) ⟶ (x56 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x55 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x6 x74 ⟶ x66 x73 (x63 x74) ⟶ (x6 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x57 x75 ⟶ x58 x75 x73 ⟶ x66 x74 (x63 x75) ⟶ (x58 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x57 x73 ⟶ x1 x73 ⟶ (x55 x73 ⟶ False) ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x57 x73 ⟶ x1 x73 ⟶ (x55 x73 ⟶ False) ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x57 x73 ⟶ x1 x73 ⟶ (x55 x73 ⟶ False) ⟶ x6 x73 ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x66 x73 (x63 x74) ⟶ x11 x73 x74 ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x66 x73 (x63 (x15 x74 x75)) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ (x3 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x66 x74 (x63 (x15 x73 x73)) ⟶ x20 x74 x73 x73 ⟶ (x34 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x55 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x63 x74) ⟶ x72 x73 ⟶ (x11 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x66 x73 (x63 (x15 x75 x74)) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ (x35 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ x66 x73 (x63 (x15 x74 x75)) ⟶ x20 x73 x74 x75 ⟶ (x34 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x57 x74 ⟶ x1 x74 ⟶ x66 x73 (x63 x74) ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x72 x74 ⟶ False) ⟶ x66 x73 (x63 x74) ⟶ (x11 x73 x74 ⟶ False) ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 x74 x75 . x66 x75 (x63 (x15 x73 x74)) ⟶ (x56 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x66 x75 (x63 (x15 x74 x73)) ⟶ (x58 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x57 x74 ⟶ x66 x73 (x63 x74) ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x72 x75 ⟶ False) ⟶ x72 x73 ⟶ x66 x74 (x63 (x15 x75 x73)) ⟶ x34 x74 x75 ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x66 x73 (x63 (x15 x75 x74)) ⟶ x20 x73 x75 x74 ⟶ (x34 x73 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x49 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x57 x73 ⟶ x1 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x72 x74 ⟶ x66 x73 (x63 x74) ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x66 x75 (x63 (x15 x73 x74)) ⟶ (x57 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x57 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x72 x75 ⟶ x66 x73 (x63 (x15 x75 x74)) ⟶ (x34 x73 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x66 x74 (x63 (x15 x75 x73)) ⟶ x34 x74 x75 ⟶ (x20 x74 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x1 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x64 x73 x74 ⟶ x64 x74 x73 ⟶ False) ⟶ (x39 = x67 (x68 x36 x36 x38 x37) (x71 x39) ⟶ False) ⟶ ((x64 x39 (x40 x36 x38 x37) ⟶ False) ⟶ False) ⟶ ((x66 x39 (x65 x36) ⟶ False) ⟶ False) ⟶ ((x66 x37 x36 ⟶ False) ⟶ False) ⟶ ((x66 x38 x36 ⟶ False) ⟶ False) ⟶ (x72 x36 ⟶ False) ⟶ False (proof)