Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../b83e1..
PUKeD../f0d75..
vout
PrPhD../d70df.. 3.41 bars
TMcss../0b951.. ownership of d58dd.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMYPS../6c6a4.. ownership of 17461.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUWUZ../5f68a.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem d58dd.. : ∀ 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 : ι → ι . ∀ x76 x77 x78 : ι → ο . (∀ x79 x80 . x78 x80 ⟶ (x80 = x79 ⟶ False) ⟶ x78 x79 ⟶ False) ⟶ (∀ x79 x80 . x0 x79 x80 ⟶ x78 x80 ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ x66 x80 (x67 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x67 x79 x80)) (x69 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x69 x79 x80)) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ (x73 (x69 x79 x80) (x75 x80) ⟶ False) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ (x73 (x67 x79 x80) (x75 x80) ⟶ False) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x62 x82 ⟶ x76 x82 ⟶ x63 x79 ⟶ x74 x79 (x75 x82) (x75 x82) ⟶ x64 x79 (x75 x82) (x75 x82) ⟶ x73 x79 (x71 (x72 (x75 x82) (x75 x82))) ⟶ x65 x79 x82 ⟶ x70 x79 x82 ⟶ x73 x80 (x75 x82) ⟶ x73 x81 (x75 x82) ⟶ (x66 x82 x80 (x68 (x75 x82) (x75 x82) x79 x80) x81 (x68 (x75 x82) (x75 x82) x79 x81) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 x83 x84 . (x77 x84 ⟶ False) ⟶ x62 x84 ⟶ x76 x84 ⟶ x73 x79 (x75 x84) ⟶ x73 x83 (x75 x84) ⟶ x73 x80 (x75 x84) ⟶ x73 x82 (x75 x84) ⟶ x73 x81 (x75 x84) ⟶ x66 x84 x79 x83 x80 x82 ⟶ x66 x84 x79 x83 x80 x81 ⟶ x66 x84 x79 x80 x83 x82 ⟶ x66 x84 x79 x80 x83 x81 ⟶ (x61 x84 x79 x83 x80 ⟶ False) ⟶ (x82 = x81 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ (x79 = x1 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x66 x80 (x60 x79 x80) (x59 x79 x80) (x68 (x75 x80) (x75 x80) x79 (x60 x79 x80)) (x68 (x75 x80) (x75 x80) x79 (x59 x79 x80)) ⟶ (x65 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ (x73 (x59 x79 x80) (x75 x80) ⟶ False) ⟶ (x65 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ (x73 (x60 x79 x80) (x75 x80) ⟶ False) ⟶ (x65 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . (x77 x82 ⟶ False) ⟶ x62 x82 ⟶ x76 x82 ⟶ x63 x79 ⟶ x74 x79 (x75 x82) (x75 x82) ⟶ x64 x79 (x75 x82) (x75 x82) ⟶ x73 x79 (x71 (x72 (x75 x82) (x75 x82))) ⟶ x65 x79 x82 ⟶ x73 x81 (x75 x82) ⟶ x73 x80 (x75 x82) ⟶ (x66 x82 x81 x80 (x68 (x75 x82) (x75 x82) x79 x81) (x68 (x75 x82) (x75 x82) x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x0 x79 x80 ⟶ x73 x80 (x71 x81) ⟶ x78 x81 ⟶ False) ⟶ (∀ x79 x80 x81 . x0 x80 x81 ⟶ x73 x81 (x71 x79) ⟶ (x73 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x58 x80 x79 ⟶ (x73 x80 (x71 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x80 (x71 x79) ⟶ (x58 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x79 x80 ⟶ (x78 x80 ⟶ False) ⟶ (x0 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x0 x80 x79 ⟶ (x73 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . x63 x82 ⟶ x74 x82 x79 x80 ⟶ x73 x82 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x74 x81 x79 x80 ⟶ x73 x81 (x71 (x72 x79 x80)) ⟶ x57 x79 x80 x82 x81 ⟶ (x57 x79 x80 x81 x82 ⟶ False) ⟶ False) ⟶ (x78 x2 ⟶ False) ⟶ (∀ x79 x80 x81 x82 . x63 x82 ⟶ x74 x82 x79 x80 ⟶ x73 x82 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x74 x81 x79 x80 ⟶ x73 x81 (x71 (x72 x79 x80)) ⟶ (x57 x79 x80 x82 x82 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x58 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . x63 x82 ⟶ x74 x82 x79 x80 ⟶ x73 x82 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x74 x81 x79 x80 ⟶ x73 x81 (x71 (x72 x79 x80)) ⟶ x82 = x81 ⟶ (x57 x79 x80 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . x63 x82 ⟶ x74 x82 x79 x80 ⟶ x73 x82 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x74 x81 x79 x80 ⟶ x73 x81 (x71 (x72 x79 x80)) ⟶ x57 x79 x80 x82 x81 ⟶ (x82 = x81 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x56 x79 = x55 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . (x78 x82 ⟶ False) ⟶ x63 x79 ⟶ x74 x79 x82 x81 ⟶ x73 x79 (x71 (x72 x82 x81)) ⟶ x73 x80 x82 ⟶ (x68 x82 x81 x79 x80 = x3 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x63 (x54 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x4 (x54 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x53 (x54 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x54 x79) ⟶ False) ⟶ False) ⟶ ((x52 x51 ⟶ False) ⟶ False) ⟶ (x78 x51 ⟶ False) ⟶ (∀ x79 x80 . (x63 (x50 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x6 (x50 x79 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x4 (x50 x80 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x5 (x50 x79 x80) ⟶ False) ⟶ False) ⟶ (x49 x48 ⟶ False) ⟶ ((x63 x48 ⟶ False) ⟶ False) ⟶ ((x5 x48 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ x78 (x8 x79) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ (x73 (x8 x79) (x71 (x75 x79)) ⟶ False) ⟶ False) ⟶ ((x63 x10 ⟶ False) ⟶ False) ⟶ ((x53 x10 ⟶ False) ⟶ False) ⟶ ((x5 x10 ⟶ False) ⟶ False) ⟶ (x78 x10 ⟶ False) ⟶ (∀ x79 x80 . (x6 (x11 x79 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x4 (x11 x80 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x5 (x11 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ x78 (x47 x79 x80) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ (x63 (x47 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ (x6 (x47 x79 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ (x4 (x47 x79 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ (x5 (x47 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x78 x80 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ (x73 (x47 x79 x80) (x71 (x72 x80 x79)) ⟶ False) ⟶ False) ⟶ ((x63 x46 ⟶ False) ⟶ False) ⟶ ((x53 x46 ⟶ False) ⟶ False) ⟶ ((x5 x46 ⟶ False) ⟶ False) ⟶ (x78 x12 ⟶ False) ⟶ ((x53 x45 ⟶ False) ⟶ False) ⟶ ((x5 x45 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x44 (x43 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x13 (x43 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x42 (x43 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x14 (x43 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x41 (x43 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x6 (x43 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x4 (x43 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x43 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x73 (x43 x79) (x71 (x72 x79 x79)) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x64 (x15 x79) x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x74 (x15 x79) x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x44 (x15 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x63 (x15 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x6 (x15 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x4 (x15 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x15 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x73 (x15 x79) (x71 (x72 x79 x79)) ⟶ False) ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ ((x63 x17 ⟶ False) ⟶ False) ⟶ ((x5 x17 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x77 x79 ⟶ False) ⟶ x9 x79 ⟶ x40 (x39 x79) ⟶ False) ⟶ (∀ x79 . (x77 x79 ⟶ False) ⟶ x9 x79 ⟶ (x73 (x39 x79) (x71 (x75 x79)) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ (x40 (x38 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ x78 (x38 x79) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ (x73 (x38 x79) (x71 (x75 x79)) ⟶ False) ⟶ False) ⟶ ((x78 x18 ⟶ False) ⟶ False) ⟶ ((x5 x37 ⟶ False) ⟶ False) ⟶ (x78 x37 ⟶ False) ⟶ (∀ x79 x80 . (x63 (x36 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x6 (x36 x79 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x4 (x36 x80 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x5 (x36 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x73 (x36 x79 x80) (x71 (x72 x80 x79)) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x74 (x19 x79 x80) x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x63 (x19 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x6 (x19 x79 x80) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x4 (x19 x80 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x5 (x19 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x73 (x19 x79 x80) (x71 (x72 x80 x79)) ⟶ False) ⟶ False) ⟶ ((x63 x20 ⟶ False) ⟶ False) ⟶ ((x5 x20 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x21 x79 ⟶ False) ⟶ x9 x79 ⟶ x22 (x75 x79) ⟶ False) ⟶ (∀ x79 . x21 x79 ⟶ x9 x79 ⟶ (x22 (x75 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . x77 x79 ⟶ x9 x79 ⟶ (x40 (x75 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x77 x79 ⟶ False) ⟶ x9 x79 ⟶ x40 (x75 x79) ⟶ False) ⟶ (∀ x79 x80 . (x5 (x72 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x16 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x13 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x42 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x14 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x63 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x7 x79 ⟶ False) ⟶ x9 x79 ⟶ x78 (x75 x79) ⟶ False) ⟶ (∀ x79 . (x6 (x55 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x4 (x55 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ ((x78 x1 ⟶ False) ⟶ False) ⟶ (∀ x79 . x7 x79 ⟶ x9 x79 ⟶ (x78 (x75 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x5 x80 ⟶ x35 x80 ⟶ x63 x80 ⟶ (x78 (x3 x80 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x52 x81 ⟶ x5 x79 ⟶ x6 x79 x81 ⟶ x63 x79 ⟶ (x63 (x3 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x52 x81 ⟶ x5 x79 ⟶ x6 x79 x81 ⟶ x63 x79 ⟶ (x5 (x3 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x44 (x55 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x63 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x4 (x55 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x73 (x23 x79) x79 ⟶ False) ⟶ False) ⟶ ((x9 x34 ⟶ False) ⟶ False) ⟶ ((x76 x24 ⟶ False) ⟶ False) ⟶ (∀ x79 . x76 x79 ⟶ (x9 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x73 (x56 x79) (x71 (x72 x79 x79)) ⟶ False) ⟶ False) ⟶ (∀ x79 . (x44 (x56 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . (x5 (x55 x79) ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 x82 . (x78 x82 ⟶ False) ⟶ x63 x79 ⟶ x74 x79 x82 x81 ⟶ x73 x79 (x71 (x72 x82 x81)) ⟶ x73 x80 x82 ⟶ (x73 (x68 x82 x81 x79 x80) x81 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ (x25 x79 x80 = x68 (x75 x80) (x75 x80) x79 (x25 x79 x80) ⟶ False) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ (x73 (x25 x79 x80) (x75 x80) ⟶ False) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x65 x79 x80 ⟶ x57 (x75 x80) (x75 x80) x79 (x56 (x75 x80)) ⟶ (x70 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . (x77 x81 ⟶ False) ⟶ x62 x81 ⟶ x76 x81 ⟶ x63 x79 ⟶ x74 x79 (x75 x81) (x75 x81) ⟶ x64 x79 (x75 x81) (x75 x81) ⟶ x73 x79 (x71 (x72 (x75 x81) (x75 x81))) ⟶ x70 x79 x81 ⟶ (x57 (x75 x81) (x75 x81) x79 (x56 (x75 x81)) ⟶ False) ⟶ x73 x80 (x75 x81) ⟶ x80 = x68 (x75 x81) (x75 x81) x79 x80 ⟶ False) ⟶ (∀ x79 x80 . (x77 x80 ⟶ False) ⟶ x62 x80 ⟶ x76 x80 ⟶ x63 x79 ⟶ x74 x79 (x75 x80) (x75 x80) ⟶ x64 x79 (x75 x80) (x75 x80) ⟶ x73 x79 (x71 (x72 (x75 x80) (x75 x80))) ⟶ x70 x79 x80 ⟶ (x65 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x33 x79 x1 ⟶ (x7 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x52 x80 ⟶ x73 x79 (x71 x80) ⟶ (x52 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x7 x79 ⟶ (x33 x79 x1 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x6 x79 x80 ⟶ (x6 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x6 x79 x80 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x6 x79 x80 ⟶ (x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . (x78 x81 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ x73 x80 (x71 (x72 x81 x79)) ⟶ x63 x80 ⟶ x74 x80 x81 x79 ⟶ (x74 x80 x81 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . (x78 x81 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ x73 x80 (x71 (x72 x81 x79)) ⟶ x63 x80 ⟶ x74 x80 x81 x79 ⟶ x78 x80 ⟶ False) ⟶ (∀ x79 x80 x81 . (x78 x81 ⟶ False) ⟶ (x78 x79 ⟶ False) ⟶ x73 x80 (x71 (x72 x81 x79)) ⟶ x63 x80 ⟶ x74 x80 x81 x79 ⟶ (x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x52 x80 ⟶ x73 x79 x80 ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x52 x80 ⟶ x73 x79 x80 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x21 x79 ⟶ False) ⟶ x77 x79 ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x4 x79 x80 ⟶ (x4 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x4 x79 x80 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x78 x80 ⟶ x5 x79 ⟶ x4 x79 x80 ⟶ (x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x80 (x71 (x72 x79 x79)) ⟶ x41 x80 ⟶ x63 x80 ⟶ x44 x80 x79 ⟶ x74 x80 x79 x79 ⟶ (x64 x80 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x80 (x71 (x72 x79 x79)) ⟶ x41 x80 ⟶ x63 x80 ⟶ x44 x80 x79 ⟶ x74 x80 x79 x79 ⟶ (x74 x80 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x80 (x71 (x72 x79 x79)) ⟶ x41 x80 ⟶ x63 x80 ⟶ x44 x80 x79 ⟶ x74 x80 x79 x79 ⟶ (x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ (x52 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x77 x79 ⟶ (x21 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x5 x81 ⟶ x6 x81 x79 ⟶ x73 x80 (x71 x81) ⟶ (x6 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x81 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x16 x81 ⟶ x26 x81 x80 ⟶ (x64 x81 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x81 (x71 (x72 x79 x80)) ⟶ x63 x81 ⟶ x16 x81 ⟶ x26 x81 x80 ⟶ (x63 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 . x40 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x49 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x40 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x40 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x21 x79 ⟶ False) ⟶ x21 x79 ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x21 x79 ⟶ False) ⟶ x7 x79 ⟶ False) ⟶ (∀ x79 x80 x81 . x5 x81 ⟶ x4 x81 x79 ⟶ x73 x80 (x71 x81) ⟶ (x4 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79)) ⟶ x63 x81 ⟶ x64 x81 x80 x79 ⟶ (x26 x81 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79)) ⟶ x63 x81 ⟶ x64 x81 x80 x79 ⟶ (x16 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x81 (x71 (x72 x80 x79)) ⟶ x63 x81 ⟶ x64 x81 x80 x79 ⟶ (x63 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 . x5 x79 ⟶ x63 x79 ⟶ (x49 x79 ⟶ False) ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x5 x79 ⟶ x63 x79 ⟶ (x49 x79 ⟶ False) ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x5 x79 ⟶ x63 x79 ⟶ (x49 x79 ⟶ False) ⟶ x40 x79 ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x7 x79 ⟶ (x21 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x7 x79 ⟶ (x7 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ (x53 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x73 x80 (x71 (x72 x79 x79)) ⟶ x74 x80 x79 x79 ⟶ (x44 x80 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x49 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ (x35 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x5 x79 ⟶ x14 x79 ⟶ x13 x79 ⟶ (x41 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x5 x79 ⟶ x14 x79 ⟶ x13 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . (x78 x81 ⟶ False) ⟶ x73 x79 (x71 (x72 x80 x81)) ⟶ x74 x79 x80 x81 ⟶ (x44 x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x5 x80 ⟶ x63 x80 ⟶ x73 x79 (x71 x80) ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x77 x79 ⟶ False) ⟶ x7 x79 ⟶ False) ⟶ (∀ x79 x80 . x5 x80 ⟶ x73 x79 (x71 x80) ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . (x78 x81 ⟶ False) ⟶ x78 x79 ⟶ x73 x80 (x71 (x72 x81 x79)) ⟶ x44 x80 x81 ⟶ False) ⟶ (∀ x79 x80 x81 . x78 x81 ⟶ x73 x79 (x71 (x72 x81 x80)) ⟶ x74 x79 x81 x80 ⟶ (x44 x79 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x16 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ x5 x79 ⟶ x63 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x7 x79 ⟶ (x77 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ (x5 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x78 x81 ⟶ x73 x79 (x71 (x72 x81 x80)) ⟶ (x44 x79 x81 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 x81 . x73 x80 (x71 (x72 x81 x79)) ⟶ x44 x80 x81 ⟶ (x74 x80 x81 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x78 x79 ⟶ (x63 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x77 x79 ⟶ False) ⟶ x7 x79 ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x33 x79 x2 ⟶ (x77 x79 ⟶ False) ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ x33 x79 x2 ⟶ x7 x79 ⟶ False) ⟶ (∀ x79 . x9 x79 ⟶ (x7 x79 ⟶ False) ⟶ x77 x79 ⟶ (x33 x79 x2 ⟶ False) ⟶ False) ⟶ (∀ x79 x80 . x0 x79 x80 ⟶ x0 x80 x79 ⟶ False) ⟶ (x29 = x68 (x75 x32) (x75 x32) x31 x30 ⟶ False) ⟶ (x61 x32 x27 (x68 (x75 x32) (x75 x32) x31 x27) x30 ⟶ False) ⟶ ((x66 x32 x27 x30 (x68 (x75 x32) (x75 x32) x31 x27) x29 ⟶ False) ⟶ False) ⟶ ((x66 x32 x27 (x68 (x75 x32) (x75 x32) x31 x27) x30 x29 ⟶ False) ⟶ False) ⟶ ((x70 x31 x32 ⟶ False) ⟶ False) ⟶ ((x73 x31 (x71 (x72 (x75 x32) (x75 x32))) ⟶ False) ⟶ False) ⟶ ((x64 x31 (x75 x32) (x75 x32) ⟶ False) ⟶ False) ⟶ ((x74 x31 (x75 x32) (x75 x32) ⟶ False) ⟶ False) ⟶ ((x63 x31 ⟶ False) ⟶ False) ⟶ ((x73 x29 (x75 x32) ⟶ False) ⟶ False) ⟶ ((x73 x30 (x75 x32) ⟶ False) ⟶ False) ⟶ ((x73 x27 (x75 x32) ⟶ False) ⟶ False) ⟶ ((x76 x32 ⟶ False) ⟶ False) ⟶ ((x28 x32 ⟶ False) ⟶ False) ⟶ ((x62 x32 ⟶ False) ⟶ False) ⟶ (x77 x32 ⟶ False) ⟶ False (proof)