Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../688a1..
PUh5Z../c521d..
vout
PrPhD../84db4.. 3.41 bars
TMQhF../3a226.. ownership of 99d55.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMHZf../f158e.. ownership of fc4d3.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUL7E../7fc1b.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 99d55.. : ∀ 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 x75 . x73 x75 ⟶ (x75 = x74 ⟶ False) ⟶ x73 x74 ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x74 = x72 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x74 x75 ⟶ x2 x75 (x1 x76) ⟶ x73 x76 ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x75 x76 ⟶ x2 x76 (x1 x74) ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 x3 ⟶ x13 x74 ⟶ x4 x74 x3 (x5 x75) ⟶ x2 x74 (x1 (x12 x3 (x5 x75))) ⟶ x6 x74 ⟶ (x7 (x11 x3 (x5 x75) (x10 x75 x74) (x8 x76 x9)) (x11 x3 (x5 x75) x74 x76) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x7 x75 x74 ⟶ (x2 x75 (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 x74) ⟶ (x7 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x74 x75 ⟶ (x73 x75 ⟶ False) ⟶ (x0 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 x3 ⟶ x13 x74 ⟶ x4 x74 x3 (x5 x75) ⟶ x2 x74 (x1 (x12 x3 (x5 x75))) ⟶ (x11 x3 (x5 x75) (x10 x75 x74) x76 = x14 x75 (x5 x75) (x11 x3 (x5 x75) (x10 x75 x74) (x8 x76 x9)) (x11 x3 (x5 x75) x74 x76) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x75 x74 ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ ((x2 x72 x15 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x71 x74 x72 = x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x7 x75 x74 ⟶ (x71 x75 x74 = x74 ⟶ False) ⟶ False) ⟶ ((x2 x9 x70 ⟶ False) ⟶ False) ⟶ ((x2 x9 x3 ⟶ False) ⟶ False) ⟶ ((x69 x9 x70 x3 ⟶ False) ⟶ False) ⟶ ((x16 x9 ⟶ False) ⟶ False) ⟶ (x73 x9 ⟶ False) ⟶ (∀ x74 . (x7 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x2 x75 x74 ⟶ (x69 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x69 x75 x76 x74 ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x66 x76 x74 ⟶ x68 x76 x74 ⟶ x2 x76 (x1 (x1 x74)) ⟶ x2 x75 x76 ⟶ (x67 x75 x74 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x66 x76 x74 ⟶ x68 x76 x74 ⟶ x2 x76 (x1 (x1 x74)) ⟶ x67 x75 x74 x76 ⟶ (x2 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x5 x74 = x1 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x66 x77 x74 ⟶ x68 x77 x74 ⟶ x2 x77 (x1 (x1 x74)) ⟶ x2 x76 x77 ⟶ x2 x75 x77 ⟶ (x14 x74 x77 x76 x75 = x71 x76 x75 ⟶ False) ⟶ False) ⟶ ((x3 = x15 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x10 x74 x75 = x17 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x13 x74 ⟶ x4 x74 x77 x76 ⟶ x2 x74 (x1 (x12 x77 x76)) ⟶ x2 x75 x77 ⟶ (x11 x77 x76 x74 x75 = x65 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 x3 ⟶ x19 x74 ⟶ (x8 x75 x74 = x18 x75 x74 ⟶ False) ⟶ False) ⟶ ((x19 x64 ⟶ False) ⟶ False) ⟶ (x73 x64 ⟶ False) ⟶ ((x63 x62 ⟶ False) ⟶ False) ⟶ ((x20 x62 ⟶ False) ⟶ False) ⟶ ((x61 x62 ⟶ False) ⟶ False) ⟶ ((x73 x62 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x59 (x60 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x60 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x73 (x58 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x2 (x58 x75 x74) x75 ⟶ False) ⟶ False) ⟶ ((x19 x57 ⟶ False) ⟶ False) ⟶ (∀ x74 . x59 (x21 x74) x74 ⟶ False) ⟶ (∀ x74 . (x2 (x21 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x22 (x23 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x56 (x23 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x23 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x4 (x55 x75 x74) x3 (x5 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x13 (x55 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x22 (x55 x75 x74) (x5 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x22 (x55 x75 x74) x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x56 (x55 x75 x74) x3 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x24 (x55 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x2 (x55 x75 x74) (x1 (x12 x3 (x5 x74))) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x25 (x26 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x13 (x26 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x22 (x26 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x24 (x26 x74) ⟶ False) ⟶ False) ⟶ ((x63 x27 ⟶ False) ⟶ False) ⟶ ((x16 x27 ⟶ False) ⟶ False) ⟶ ((x20 x27 ⟶ False) ⟶ False) ⟶ ((x61 x27 ⟶ False) ⟶ False) ⟶ (x73 x28 ⟶ False) ⟶ (∀ x74 . (x73 (x54 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x54 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ ((x24 x52 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x68 (x51 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x66 (x51 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 (x51 x74) ⟶ False) ⟶ (∀ x74 . (x2 (x51 x74) (x1 (x1 x74)) ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x29 x49 ⟶ False) ⟶ False) ⟶ ((x48 x49 ⟶ False) ⟶ False) ⟶ (x73 x49 ⟶ False) ⟶ ((x63 x47 ⟶ False) ⟶ False) ⟶ ((x73 x30 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ x73 (x46 x74) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x46 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x22 (x45 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x56 (x45 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x45 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 (x45 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x45 x74 x75) (x1 (x12 x75 x74)) ⟶ False) ⟶ False) ⟶ ((x24 x31 ⟶ False) ⟶ False) ⟶ (x73 x31 ⟶ False) ⟶ (∀ x74 . (x66 (x32 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x44 (x32 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 (x32 x74) ⟶ False) ⟶ (∀ x74 . (x2 (x32 x74) (x1 (x1 x74)) ⟶ False) ⟶ False) ⟶ ((x50 x33 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x4 (x43 x74 x75) x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x13 (x43 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x22 (x43 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x56 (x43 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x43 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x43 x74 x75) (x1 (x12 x75 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x66 x77 x74 ⟶ x68 x77 x74 ⟶ x2 x77 (x1 (x1 x74)) ⟶ x2 x76 x77 ⟶ x2 x75 x77 ⟶ (x14 x74 x77 x76 x76 = x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x71 x74 x74 = x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x24 (x12 x74 x75) ⟶ False) ⟶ False) ⟶ ((x50 x15 ⟶ False) ⟶ False) ⟶ (x73 x15 ⟶ False) ⟶ (∀ x74 x75 . x63 x75 ⟶ x63 x74 ⟶ (x63 (x18 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x73 (x71 x74 x75) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x73 (x71 x75 x74) ⟶ False) ⟶ (∀ x74 x75 x76 . x24 x76 ⟶ x22 x76 x74 ⟶ x24 x75 ⟶ x22 x75 x74 ⟶ (x22 (x71 x76 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x68 (x1 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x24 x75 ⟶ x24 x74 ⟶ (x24 (x71 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x6 (x17 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x4 (x17 x75) x3 (x5 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x13 (x17 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x66 (x1 x74) x74 ⟶ False) ⟶ False) ⟶ ((x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 (x1 x74) ⟶ False) ⟶ (∀ x74 x75 x76 . x24 x76 ⟶ x56 x76 x74 ⟶ x24 x75 ⟶ x56 x75 x74 ⟶ (x56 (x71 x76 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x44 (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x16 x75 ⟶ False) ⟶ x63 x75 ⟶ (x16 x74 ⟶ False) ⟶ x63 x74 ⟶ x16 (x18 x75 x74) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x73 (x12 x75 x74) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ (x69 (x34 x74 x75) x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x42 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ x2 x75 (x1 (x1 x74)) ⟶ (x67 (x35 x75 x74) x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x69 x75 x76 x74 ⟶ (x2 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x66 x76 x74 ⟶ x68 x76 x74 ⟶ x2 x76 (x1 (x1 x74)) ⟶ x67 x75 x74 x76 ⟶ (x2 x75 (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x5 x74) (x1 (x1 x74)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x66 x77 x74 ⟶ x68 x77 x74 ⟶ x2 x77 (x1 (x1 x74)) ⟶ x2 x76 x77 ⟶ x2 x75 x77 ⟶ (x67 (x14 x74 x77 x76 x75) x74 x77 ⟶ False) ⟶ False) ⟶ ((x2 x3 (x1 x70) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x2 (x10 x74 x75) (x1 (x12 x3 (x5 x74))) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x4 (x10 x74 x75) x3 (x5 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x13 x75 ⟶ x4 x75 x3 (x5 x74) ⟶ x2 x75 (x1 (x12 x3 (x5 x74))) ⟶ (x13 (x10 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 . x24 x74 ⟶ x13 x74 ⟶ (x13 (x17 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . x24 x74 ⟶ x13 x74 ⟶ (x24 (x17 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x13 x74 ⟶ x4 x74 x77 x76 ⟶ x2 x74 (x1 (x12 x77 x76)) ⟶ x2 x75 x77 ⟶ (x2 (x11 x77 x76 x74 x75) x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 x3 ⟶ x19 x74 ⟶ (x69 (x8 x75 x74) x70 x3 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . (x73 x77 ⟶ False) ⟶ x66 x77 x74 ⟶ x68 x77 x74 ⟶ x2 x77 (x1 (x1 x74)) ⟶ x2 x76 x77 ⟶ x2 x75 x77 ⟶ (x14 x74 x77 x76 x75 = x14 x74 x77 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x61 x75 ⟶ x61 x74 ⟶ (x18 x75 x74 = x18 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x71 x75 x74 = x71 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 x3 ⟶ x19 x74 ⟶ (x8 x75 x74 = x8 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x41 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x22 x74 x75 ⟶ (x22 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x22 x74 x75 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x22 x74 x75 ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 x15 ⟶ (x19 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x12 x76 x74)) ⟶ x13 x75 ⟶ x4 x75 x76 x74 ⟶ (x4 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x12 x76 x74)) ⟶ x13 x75 ⟶ x4 x75 x76 x74 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x75 (x1 (x12 x76 x74)) ⟶ x13 x75 ⟶ x4 x75 x76 x74 ⟶ (x13 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x56 x74 x75 ⟶ (x56 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x56 x74 x75 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x24 x74 ⟶ x56 x74 x75 ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x19 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x24 x76 ⟶ x22 x76 x74 ⟶ x2 x75 (x1 x76) ⟶ (x22 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x50 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x24 x76 ⟶ x56 x76 x74 ⟶ x2 x75 (x1 x76) ⟶ (x56 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x50 x75 ⟶ x2 x74 x75 ⟶ (x50 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x63 x74 ⟶ (x20 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x2 x74 (x1 x75) ⟶ x59 x74 x75 ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x12 x75 x76)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x24 x74 ⟶ (x53 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x24 x74 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x25 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x12 x74 x74)) ⟶ x4 x75 x74 x74 ⟶ (x40 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x63 x74 ⟶ (x61 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ x73 x74 ⟶ (x59 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x12 x76 x75)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x24 x74 ⟶ (x39 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x24 x74 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x50 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x2 x74 (x1 (x12 x75 x76)) ⟶ x4 x74 x75 x76 ⟶ (x40 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x19 x74 ⟶ (x63 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ (x59 x74 x75 ⟶ False) ⟶ x73 x74 ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x12 x74 x75)) ⟶ (x22 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x12 x75 x74)) ⟶ (x56 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x24 x75 ⟶ x2 x74 (x1 x75) ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x48 x74 ⟶ x29 x74 ⟶ (x50 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x12 x76 x75)) ⟶ x4 x74 x76 x75 ⟶ (x40 x74 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 x70 ⟶ (x63 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x2 x74 (x1 x75) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x12 x74 x75)) ⟶ (x24 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x1 x74)) ⟶ (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ (x68 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x1 x74)) ⟶ (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ (x66 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x1 x74)) ⟶ (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ (x44 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 (x1 x74)) ⟶ (x73 x75 ⟶ False) ⟶ x66 x75 x74 ⟶ x68 x75 x74 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 . x50 x74 ⟶ (x29 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x50 x74 ⟶ (x48 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x75 (x1 (x12 x76 x74)) ⟶ x40 x75 x76 ⟶ (x4 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x41 x75 ⟶ x2 x74 (x1 x75) ⟶ (x41 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x0 x75 x74 ⟶ False) ⟶ (x11 x3 (x5 x36) (x10 x36 x37) x38 = x11 x3 (x5 x36) x37 x38 ⟶ False) ⟶ ((x6 x37 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x1 (x12 x3 (x5 x36))) ⟶ False) ⟶ False) ⟶ ((x4 x37 x3 (x5 x36) ⟶ False) ⟶ False) ⟶ ((x13 x37 ⟶ False) ⟶ False) ⟶ ((x2 x38 x3 ⟶ False) ⟶ False) ⟶ False (proof)