Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../b5316..
PUX3F../77b51..
vout
PrPhD../40b5d.. 3.38 bars
TMaYf../dd6e7.. ownership of 09243.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMcfJ../1502f.. ownership of 2f728.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUMeG../9cb1f.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 09243.. : ∀ 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 x81 . x79 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x4 x84 ⟶ x4 x80 ⟶ x7 (x5 x84) (x8 x84) = x7 (x5 x80) (x8 x80) ⟶ x2 x81 (x5 x84) ⟶ x2 x83 (x5 x80) ⟶ x81 = x83 ⟶ x6 x84 x82 x81 ⟶ (x6 x80 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x4 x84 ⟶ x4 x80 ⟶ x7 (x5 x84) (x8 x84) = x7 (x5 x80) (x8 x80) ⟶ x2 x81 (x5 x84) ⟶ x2 x83 (x5 x80) ⟶ x81 = x83 ⟶ x77 x84 x82 x81 ⟶ (x77 x80 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . x4 x85 ⟶ x4 x80 ⟶ x7 (x5 x85) (x8 x85) = x7 (x5 x80) (x8 x80) ⟶ x2 x81 (x5 x85) ⟶ x2 x84 (x5 x85) ⟶ x2 x82 (x5 x80) ⟶ x2 x83 (x5 x80) ⟶ x81 = x82 ⟶ x84 = x83 ⟶ x76 x85 x81 x84 ⟶ (x76 x80 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . x4 x85 ⟶ x4 x80 ⟶ x7 (x5 x85) (x8 x85) = x7 (x5 x80) (x8 x80) ⟶ x2 x81 (x5 x85) ⟶ x2 x84 (x5 x85) ⟶ x2 x82 (x5 x80) ⟶ x2 x83 (x5 x80) ⟶ x81 = x82 ⟶ x84 = x83 ⟶ x9 x85 x81 x84 ⟶ (x9 x80 x82 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (x79 x10 ⟶ False) ⟶ (∀ x80 . (x3 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x11 x80 ⟶ False) ⟶ x11 (x12 x80) ⟶ False) ⟶ (∀ x80 . (x11 x80 ⟶ False) ⟶ (x2 (x12 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x11 (x13 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x13 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x13 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x74 (x75 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x75 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ x79 (x72 x80) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ (x2 (x72 x80) (x1 (x5 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x74 (x70 x80) x80 ⟶ False) ⟶ (∀ x80 . (x2 (x70 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (x79 x69 ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x15 (x14 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x68 (x14 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x17 (x14 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ x79 (x14 x80) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x2 (x14 x80) (x1 (x5 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 (x67 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x67 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x66 x65 ⟶ False) ⟶ False) ⟶ ((x18 x65 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x64 x80 ⟶ False) ⟶ x71 x80 ⟶ x11 (x63 x80) ⟶ False) ⟶ (∀ x80 . (x64 x80 ⟶ False) ⟶ x71 x80 ⟶ (x2 (x63 x80) (x1 (x5 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ (x11 (x62 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ x79 (x62 x80) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ (x2 (x62 x80) (x1 (x5 x80)) ⟶ False) ⟶ False) ⟶ ((x16 x19 ⟶ False) ⟶ False) ⟶ ((x61 x19 ⟶ False) ⟶ False) ⟶ ((x20 x19 x10 ⟶ False) ⟶ False) ⟶ ((x4 x19 ⟶ False) ⟶ False) ⟶ ((x79 x21 ⟶ False) ⟶ False) ⟶ ((x60 x59 ⟶ False) ⟶ False) ⟶ ((x22 x59 ⟶ False) ⟶ False) ⟶ ((x58 x59 ⟶ False) ⟶ False) ⟶ ((x23 x59 ⟶ False) ⟶ False) ⟶ ((x16 x59 ⟶ False) ⟶ False) ⟶ ((x61 x59 ⟶ False) ⟶ False) ⟶ ((x20 x59 x10 ⟶ False) ⟶ False) ⟶ (x73 x59 ⟶ False) ⟶ ((x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x15 (x24 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x68 (x24 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x2 (x24 x80) (x1 (x5 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x57 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x57 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x18 x56 ⟶ False) ⟶ False) ⟶ (x79 x56 ⟶ False) ⟶ (∀ x80 x81 x82 . x4 x82 ⟶ x2 x80 (x5 x82) ⟶ x2 x81 (x5 x82) ⟶ x76 x82 x80 x80 ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x82 (x1 (x25 x83 x83)) ⟶ x7 x83 x82 = x7 x81 x80 ⟶ (x82 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x82 (x1 (x25 x83 x83)) ⟶ x7 x83 x82 = x7 x80 x81 ⟶ (x83 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x26 x80 ⟶ False) ⟶ x4 x80 ⟶ x79 (x8 x80) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ x4 x80 ⟶ (x22 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x55 x80 ⟶ False) ⟶ x71 x80 ⟶ x17 (x5 x80) ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ x4 x80 ⟶ (x60 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x55 x80 ⟶ x71 x80 ⟶ (x17 (x5 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x4 x80 ⟶ (x58 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ x71 x80 ⟶ (x11 (x5 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x23 x80 ⟶ x4 x80 ⟶ (x23 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x23 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x64 x80 ⟶ False) ⟶ x71 x80 ⟶ x11 (x5 x80) ⟶ False) ⟶ (∀ x80 x81 . (x18 (x25 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x16 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x4 x80 ⟶ x73 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x71 x80 ⟶ x79 (x5 x80) ⟶ False) ⟶ ((x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 (x1 x80) ⟶ False) ⟶ (∀ x80 . x73 x80 ⟶ x71 x80 ⟶ (x79 (x5 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ x4 x80 ⟶ (x27 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x28 x80 ⟶ x4 x80 ⟶ (x28 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x28 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x29 x80 ⟶ x4 x80 ⟶ (x29 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x29 x80 ⟶ x4 x80 ⟶ (x61 (x7 (x5 x80) (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x79 (x25 x81 x80) ⟶ False) ⟶ (∀ x80 . (x2 (x54 x80) x80 ⟶ False) ⟶ False) ⟶ ((x71 x30 ⟶ False) ⟶ False) ⟶ ((x4 x53 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x2 (x8 x80) (x1 (x25 (x5 x80) (x5 x80))) ⟶ False) ⟶ False) ⟶ ((x79 x52 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 (x25 x80 x80)) ⟶ (x4 (x7 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 (x25 x80 x80)) ⟶ (x61 (x7 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x2 x80 (x5 x81) ⟶ x6 x81 (x51 x81) x80 ⟶ x9 x81 (x50 x80 x81) x80 ⟶ (x49 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x2 x80 (x5 x81) ⟶ x6 x81 (x51 x81) x80 ⟶ (x6 x81 (x51 x81) (x50 x80 x81) ⟶ False) ⟶ (x49 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x2 x80 (x5 x81) ⟶ x6 x81 (x51 x81) x80 ⟶ (x2 (x50 x80 x81) (x5 x81) ⟶ False) ⟶ (x49 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ (x2 (x51 x80) (x1 (x5 x80)) ⟶ False) ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x4 x80 ⟶ x79 (x51 x80) ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x73 x82 ⟶ False) ⟶ x16 x82 ⟶ x4 x82 ⟶ x49 x82 ⟶ (x79 x81 ⟶ False) ⟶ x2 x81 (x1 (x5 x82)) ⟶ x2 x80 (x5 x82) ⟶ x6 x82 x81 x80 ⟶ (x9 x82 x80 (x31 x81 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x49 x81 ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 (x5 x81)) ⟶ (x6 x81 x80 (x31 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x49 x81 ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 (x5 x81)) ⟶ (x2 (x31 x80 x81) (x5 x81) ⟶ False) ⟶ False) ⟶ ((x78 = x52 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x20 x80 x78 ⟶ (x73 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x73 x80 ⟶ (x20 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x35 x80 ⟶ x32 x80 ⟶ x33 x80 ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x35 x80 ⟶ x32 x80 ⟶ x33 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x35 x80 ⟶ x32 x80 ⟶ x33 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x35 x80 ⟶ x32 x80 ⟶ x33 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x35 x80 ⟶ x32 x80 ⟶ x33 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x55 x80 ⟶ False) ⟶ x64 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x32 x80 ⟶ x37 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x34 x80 ⟶ x32 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x64 x80 ⟶ x16 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x64 x80 ⟶ x16 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x64 x80 ⟶ x16 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x64 x80 ⟶ (x55 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x40 x80 ⟶ x39 x80 ⟶ (x38 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ x36 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x29 x80 ⟶ x47 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x29 x80 ⟶ x47 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x29 x80 ⟶ x47 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 x81 . x11 x81 ⟶ x2 x80 (x1 x81) ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x55 x80 ⟶ False) ⟶ x55 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x55 x80 ⟶ False) ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x38 x80 ⟶ (x39 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x38 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x27 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x64 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x48 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x48 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x48 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x48 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x33 x80 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x33 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x33 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x33 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ x74 x80 x81 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x73 x80 ⟶ (x55 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x73 x80 ⟶ (x73 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x18 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x18 x80 ⟶ (x18 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x26 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x32 x80 ⟶ (x38 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x32 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x28 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x27 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x20 x80 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x20 x80 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ x79 x80 ⟶ (x74 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x18 x80 ⟶ (x41 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x18 x80 ⟶ (x18 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x26 x80 ⟶ False) ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x20 x80 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x28 x80 ⟶ (x42 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x28 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x28 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x28 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x40 x80 ⟶ x37 x80 ⟶ x29 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x20 x80 x10 ⟶ x16 x80 ⟶ (x20 x80 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x74 x80 x81 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x64 x80 ⟶ False) ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 x81 . x18 x81 ⟶ x2 x80 (x1 x81) ⟶ (x18 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x60 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x73 x80 ⟶ (x26 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x32 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x32 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x32 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x16 x81 ⟶ x4 x81 ⟶ x2 x80 (x1 (x5 x81)) ⟶ x79 x80 ⟶ (x44 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x60 x80 ⟶ x28 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x37 x81 ⟶ x4 x81 ⟶ x2 x80 (x1 (x5 x81)) ⟶ (x15 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x73 x81 ⟶ False) ⟶ x37 x81 ⟶ x4 x81 ⟶ x2 x80 (x1 (x5 x81)) ⟶ (x68 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x37 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x37 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x37 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 x81 . x4 x81 ⟶ x2 x80 (x1 (x5 x81)) ⟶ x79 x80 ⟶ (x15 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 ⟶ x2 x80 (x1 (x5 x81)) ⟶ x79 x80 ⟶ (x68 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x73 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x18 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x22 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x64 x80 ⟶ False) ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x39 x80 ⟶ x49 x80 ⟶ (x39 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x39 x80 ⟶ x49 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x39 x80 ⟶ x49 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x39 x80 ⟶ x49 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x39 x80 ⟶ x49 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x49 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x49 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x49 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x58 x80 ⟶ x49 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x40 x80 ⟶ x29 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x40 x80 ⟶ x29 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x40 x80 ⟶ x29 x80 ⟶ (x23 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x40 x80 ⟶ x29 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x23 x80 ⟶ x58 x80 ⟶ x22 x80 ⟶ x40 x80 ⟶ x29 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x49 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x49 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x49 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x32 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x32 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x32 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ (x73 x80 ⟶ False) ⟶ x16 x80 ⟶ x32 x80 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x20 x80 x10 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x20 x80 x10 ⟶ x73 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ (x39 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x16 x80 ⟶ x22 x80 ⟶ x29 x80 ⟶ (x16 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x73 x80 ⟶ False) ⟶ x64 x80 ⟶ (x20 x80 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (∀ x80 . x4 x80 ⟶ x61 x80 ⟶ (x80 = x7 (x5 x80) (x8 x80) ⟶ False) ⟶ False) ⟶ (x49 x45 ⟶ False) ⟶ ((x49 x46 ⟶ False) ⟶ False) ⟶ ((x7 (x5 x46) (x8 x46) = x7 (x5 x45) (x8 x45) ⟶ False) ⟶ False) ⟶ ((x4 x45 ⟶ False) ⟶ False) ⟶ ((x16 x45 ⟶ False) ⟶ False) ⟶ (x73 x45 ⟶ False) ⟶ ((x4 x46 ⟶ False) ⟶ False) ⟶ ((x16 x46 ⟶ False) ⟶ False) ⟶ (x73 x46 ⟶ False) ⟶ False (proof)