Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../1bc91..
PUXC2../2c753..
vout
PrNUD../c9859.. 0.01 bars
TMFPG../9a4f4.. ownership of 8c099.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMSpD../1818f.. ownership of c3c1a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PURos../8619e.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 8c099.. : ∀ 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 . x68 x70 ⟶ (x70 = x69 ⟶ False) ⟶ x68 x69 ⟶ False) ⟶ (∀ x69 x70 . x0 x69 x70 ⟶ x68 x70 ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x69 = x67 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x6 x69 (x5 x70) ⟶ (x7 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x7 x69 x70 ⟶ (x6 x69 (x5 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x0 x69 x70 ⟶ x2 x70 (x4 x71) ⟶ x68 x71 ⟶ False) ⟶ (∀ x69 x70 x71 . x0 x70 x71 ⟶ x2 x71 (x4 x69) ⟶ (x2 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x69 (x4 (x4 x70)) ⟶ (x6 x69 (x8 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x6 x70 x69 ⟶ (x2 x70 (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 x69) ⟶ (x6 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x69 x70 ⟶ (x68 x70 ⟶ False) ⟶ (x0 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x6 x70 x71 ⟶ x6 x71 x69 ⟶ (x6 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x0 x70 x69 ⟶ (x2 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x69 (x4 (x4 x70)) ⟶ (x6 x69 (x9 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 (x4 x70)) ⟶ (x2 x69 (x4 (x4 (x3 (x66 x70 (x9 x70 x69))))) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 (x4 x70)) ⟶ (x10 x69 (x66 x70 (x9 x70 x69)) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 (x4 x70)) ⟶ (x7 x69 (x66 x70 (x9 x70 x69)) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x6 x69 x69 ⟶ False) ⟶ False) ⟶ ((x65 x64 ⟶ False) ⟶ False) ⟶ ((x11 x64 ⟶ False) ⟶ False) ⟶ ((x63 x64 ⟶ False) ⟶ False) ⟶ (x68 x64 ⟶ False) ⟶ ((x62 x61 ⟶ False) ⟶ False) ⟶ ((x12 x61 ⟶ False) ⟶ False) ⟶ (x68 x61 ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ (x68 x14 ⟶ False) ⟶ (∀ x69 . (x15 x69 ⟶ False) ⟶ (x12 (x16 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x15 x69 ⟶ False) ⟶ x15 (x16 x69) ⟶ False) ⟶ (∀ x69 . (x15 x69 ⟶ False) ⟶ (x2 (x16 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x15 x69 ⟶ False) ⟶ x15 (x60 x69) ⟶ False) ⟶ (∀ x69 . (x15 x69 ⟶ False) ⟶ (x2 (x60 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ (x12 x59 ⟶ False) ⟶ ((x11 x59 ⟶ False) ⟶ False) ⟶ ((x63 x59 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x15 (x17 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ x68 (x17 x69) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x2 (x17 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ (x58 x57 ⟶ False) ⟶ ((x11 x57 ⟶ False) ⟶ False) ⟶ ((x63 x57 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x55 (x56 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x2 (x56 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x55 (x54 x69) x69 ⟶ False) ⟶ (∀ x69 . (x2 (x54 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ ((x12 x53 ⟶ False) ⟶ False) ⟶ ((x11 x53 ⟶ False) ⟶ False) ⟶ ((x63 x53 ⟶ False) ⟶ False) ⟶ (x68 x53 ⟶ False) ⟶ (x68 x52 ⟶ False) ⟶ (∀ x69 . (x68 (x20 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x2 (x20 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x11 x22 ⟶ False) ⟶ False) ⟶ ((x63 x22 ⟶ False) ⟶ False) ⟶ (x68 x51 ⟶ False) ⟶ ((x58 x51 ⟶ False) ⟶ False) ⟶ ((x11 x51 ⟶ False) ⟶ False) ⟶ ((x63 x51 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x12 (x50 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ x68 (x50 x69) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x2 (x50 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x24 (x23 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x7 (x23 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x2 (x23 x69) (x4 (x4 (x3 x69))) ⟶ False) ⟶ False) ⟶ ((x68 x49 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x7 (x25 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x2 (x25 x69) (x4 (x4 (x3 x69))) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ x68 (x26 x69) ⟶ False) ⟶ (∀ x69 . (x68 x69 ⟶ False) ⟶ (x2 (x26 x69) (x4 x69) ⟶ False) ⟶ False) ⟶ ((x27 x28 ⟶ False) ⟶ False) ⟶ ((x1 x28 ⟶ False) ⟶ False) ⟶ ((x11 x29 ⟶ False) ⟶ False) ⟶ ((x63 x29 ⟶ False) ⟶ False) ⟶ ((x30 x31 ⟶ False) ⟶ False) ⟶ ((x11 x31 ⟶ False) ⟶ False) ⟶ ((x63 x31 ⟶ False) ⟶ False) ⟶ ((x12 x48 ⟶ False) ⟶ False) ⟶ (x68 x48 ⟶ False) ⟶ ((x47 x46 ⟶ False) ⟶ False) ⟶ ((x11 x46 ⟶ False) ⟶ False) ⟶ ((x63 x46 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x10 (x32 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x7 (x32 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x2 (x32 x69) (x4 (x4 (x3 x69))) ⟶ False) ⟶ False) ⟶ ((x27 x45 ⟶ False) ⟶ False) ⟶ ((x33 x45 ⟶ False) ⟶ False) ⟶ ((x1 x45 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 . x2 x71 (x4 (x4 x72)) ⟶ x66 x72 x71 = x66 x70 x69 ⟶ (x71 = x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 . x2 x71 (x4 (x4 x72)) ⟶ x66 x72 x71 = x66 x69 x70 ⟶ (x72 = x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 (x4 x70)) ⟶ (x27 (x66 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 (x4 x70)) ⟶ x33 (x66 x70 x69) ⟶ False) ⟶ (∀ x69 . (x33 x69 ⟶ False) ⟶ x1 x69 ⟶ (x27 (x66 (x3 x69) (x5 x69)) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x33 x69 ⟶ False) ⟶ x1 x69 ⟶ x33 (x66 (x3 x69) (x5 x69)) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x24 (x5 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x12 x69 ⟶ (x62 (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 (x4 x69)) ⟶ x68 (x8 x69 x70) ⟶ False) ⟶ ((x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x7 (x5 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 (x4 x69) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x10 (x5 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x12 x69 ⟶ (x12 (x4 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . (x2 (x34 x69) x69 ⟶ False) ⟶ False) ⟶ ((x44 x43 ⟶ False) ⟶ False) ⟶ ((x1 x35 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x2 (x5 x69) (x4 (x4 (x3 x69))) ⟶ False) ⟶ False) ⟶ ((x68 x36 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x44 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 (x4 x69)) ⟶ (x2 (x8 x69 x70) (x4 (x4 x69)) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 (x4 x69)) ⟶ (x2 (x9 x69 x70) (x4 (x4 x69)) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 (x4 x69)) ⟶ (x1 (x66 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x2 x70 (x4 (x4 x69)) ⟶ (x27 (x66 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x1 x71 ⟶ x2 x69 (x4 (x4 (x3 x71))) ⟶ x7 x70 x71 ⟶ x10 x70 x71 ⟶ x2 x70 (x4 (x4 (x3 x71))) ⟶ x6 x70 (x8 (x3 x71) x69) ⟶ (x24 x69 x71 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x24 x69 x70 ⟶ (x6 (x42 x69 x70) (x8 (x3 x70) x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x24 x69 x70 ⟶ (x2 (x42 x69 x70) (x4 (x4 (x3 x70))) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x24 x69 x70 ⟶ (x10 (x42 x69 x70) x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x24 x69 x70 ⟶ (x7 (x42 x69 x70) x70 ⟶ False) ⟶ False) ⟶ ((x67 = x36 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ x33 x69 ⟶ (x37 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x13 x70 ⟶ x2 x69 (x4 x70) ⟶ (x13 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ (x65 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x13 x70 ⟶ x2 x69 x70 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x13 x70 ⟶ x2 x69 x70 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x62 x70 ⟶ x2 x69 (x4 x70) ⟶ (x62 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x13 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x62 x70 ⟶ x2 x69 x70 ⟶ (x12 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x41 x70 ⟶ x2 x69 (x4 x70) ⟶ (x41 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x15 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x58 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x15 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x15 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x62 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x12 x69 ⟶ (x41 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x15 x70 ⟶ x2 x69 (x4 x70) ⟶ (x15 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ (x58 x69 ⟶ False) ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ (x58 x69 ⟶ False) ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ (x58 x69 ⟶ False) ⟶ x15 x69 ⟶ False) ⟶ (∀ x69 . (x12 x69 ⟶ False) ⟶ x15 x69 ⟶ False) ⟶ (∀ x69 . (x12 x69 ⟶ False) ⟶ x41 x69 ⟶ (x18 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x68 x70 ⟶ x2 x69 (x4 x70) ⟶ x55 x69 x70 ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x58 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x15 x69 ⟶ (x12 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x18 x69 ⟶ (x41 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x18 x69 ⟶ x12 x69 ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 x70) ⟶ x68 x69 ⟶ (x55 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x63 x70 ⟶ x11 x70 ⟶ x2 x69 (x4 x70) ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x68 x69 ⟶ (x30 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x68 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x68 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ x2 x69 (x4 x70) ⟶ (x55 x69 x70 ⟶ False) ⟶ x68 x69 ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x30 x69 ⟶ (x40 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x30 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x63 x69 ⟶ x11 x69 ⟶ x30 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x12 x70 ⟶ x2 x69 (x4 x70) ⟶ (x12 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x68 x70 ⟶ x2 x69 (x4 x70) ⟶ (x68 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x12 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x47 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x11 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x63 x69 ⟶ x11 x69 ⟶ (x63 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x7 x69 x70 ⟶ x10 x69 x70 ⟶ (x24 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x7 x69 x70 ⟶ x10 x69 x70 ⟶ (x10 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x1 x70 ⟶ x2 x69 (x4 (x4 (x3 x70))) ⟶ x7 x69 x70 ⟶ x10 x69 x70 ⟶ (x7 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x0 x69 x70 ⟶ x0 x70 x69 ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ x27 x69 ⟶ (x69 = x66 (x3 x69) (x5 x69) ⟶ False) ⟶ False) ⟶ (x7 x39 (x66 x38 (x9 x38 (x8 x38 x39))) ⟶ x24 x39 (x66 x38 (x9 x38 (x8 x38 x39))) ⟶ x2 x39 (x4 (x4 (x3 (x66 x38 (x9 x38 (x8 x38 x39)))))) ⟶ False) ⟶ ((x2 x39 (x4 (x4 x38)) ⟶ False) ⟶ False) ⟶ (x68 x38 ⟶ False) ⟶ False (proof)