Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../5cd6e..
PUXX6../e7360..
vout
PrPhD../96df6.. 3.41 bars
TMJGB../dd125.. ownership of 8ff5a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMd3C../f51de.. ownership of 9e692.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUfP7../ab295.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 8ff5a.. : ∀ 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 . x1 x69 ⟶ (x4 x5 x69 = x2 x3 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x66 x5 x65 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x4 x3 x69 = x6 (x2 x5 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x66 x3 x65 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x4 x5 x69 = x2 x3 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x64 x5 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x4 x3 x69 = x6 (x2 x5 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x1 x69 ⟶ (x64 x3 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x0 x69 x70 ⟶ x8 x70 (x7 x71) ⟶ x68 x71 ⟶ False) ⟶ (∀ x69 x70 x71 . x0 x70 x71 ⟶ x8 x71 (x7 x69) ⟶ (x8 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x9 x70 x69 ⟶ (x8 x70 (x7 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 (x7 x69) ⟶ (x9 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x69 x70 ⟶ (x68 x70 ⟶ False) ⟶ (x0 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x63 x71 ⟶ x8 x71 (x7 x65) ⟶ x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ x66 x70 x69 ⟶ x9 x71 x69 ⟶ (x66 x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x0 x70 x69 ⟶ (x8 x70 x69 ⟶ False) ⟶ False) ⟶ ((x8 x67 x60 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 . x63 x72 ⟶ x8 x72 (x7 x65) ⟶ x62 x71 ⟶ x8 x71 (x7 (x61 x65 x65)) ⟶ x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ x9 x72 (x11 x65 (x10 x65 x65 x65 x71 x70)) ⟶ x66 x71 x72 ⟶ x66 x70 x72 ⟶ x8 x69 x65 ⟶ x0 x69 x72 ⟶ (x2 (x13 (x10 x65 x65 x65 x71 x70) x72) x69 = x12 (x4 x71 x69) (x4 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x63 x71 ⟶ x8 x71 (x7 x65) ⟶ x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ x62 x69 ⟶ x8 x69 (x7 (x61 x65 x65)) ⟶ x9 x71 (x11 x65 (x10 x65 x65 x65 x70 x69)) ⟶ x66 x70 x71 ⟶ x66 x69 x71 ⟶ (x66 (x10 x65 x65 x65 x70 x69) x71 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x14 x70 ⟶ x14 x69 ⟶ (x16 (x15 x70) (x15 x69) = x16 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x14 x70 ⟶ x14 x69 ⟶ (x59 (x15 x70) (x15 x69) = x15 (x59 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x14 x71 ⟶ x14 x69 ⟶ x14 x70 ⟶ (x59 (x59 x71 x69) x70 = x59 x71 (x59 x69 x70) ⟶ False) ⟶ False) ⟶ ((x8 x58 x65 ⟶ False) ⟶ False) ⟶ ((x8 x58 x17 ⟶ False) ⟶ False) ⟶ ((x57 x58 x65 x17 ⟶ False) ⟶ False) ⟶ ((x18 x58 ⟶ False) ⟶ False) ⟶ (x68 x58 ⟶ False) ⟶ (∀ x69 x70 . x14 x70 ⟶ x14 x69 ⟶ (x59 x70 (x15 x69) = x16 x70 x69 ⟶ False) ⟶ False) ⟶ ((x15 (x15 x58) = x58 ⟶ False) ⟶ False) ⟶ ((x15 x58 = x15 x58 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x9 x69 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . (x68 x71 ⟶ False) ⟶ (x68 x69 ⟶ False) ⟶ x8 x69 (x7 x71) ⟶ x8 x70 x69 ⟶ (x57 x70 x71 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . (x68 x71 ⟶ False) ⟶ (x68 x69 ⟶ False) ⟶ x8 x69 (x7 x71) ⟶ x57 x70 x71 x69 ⟶ (x8 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 x65 ⟶ x1 x69 ⟶ (x19 x70 x69 = x16 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 x65 ⟶ x1 x69 ⟶ (x12 x70 x69 = x59 x70 x69 ⟶ False) ⟶ False) ⟶ ((x17 = x60 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 x73 . x56 x73 ⟶ x56 x69 ⟶ x62 x72 ⟶ x8 x72 (x7 (x61 x70 x73)) ⟶ x62 x71 ⟶ x8 x71 (x7 (x61 x70 x69)) ⟶ (x10 x70 x73 x69 x72 x71 = x55 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x21 x70 ⟶ (x2 x70 x69 = x22 x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x53 x70 x69 ⟶ (x11 x69 x70 = x54 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 x65 ⟶ (x6 x69 = x15 x69 ⟶ False) ⟶ False) ⟶ ((x52 x51 ⟶ False) ⟶ False) ⟶ ((x23 x51 ⟶ False) ⟶ False) ⟶ (x68 x51 ⟶ False) ⟶ ((x23 x24 ⟶ False) ⟶ False) ⟶ (x68 x24 ⟶ False) ⟶ ((x25 x26 ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x62 x49 ⟶ False) ⟶ False) ⟶ ((x20 x49 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x27 (x28 x69 x70) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x53 (x28 x70 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x20 (x28 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 (x28 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x8 (x28 x69 x70) (x7 (x61 x70 x69)) ⟶ False) ⟶ False) ⟶ ((x63 x48 ⟶ False) ⟶ False) ⟶ ((x56 x48 ⟶ False) ⟶ False) ⟶ ((x47 x48 ⟶ False) ⟶ False) ⟶ ((x29 x48 ⟶ False) ⟶ False) ⟶ ((x8 x48 (x7 x65) ⟶ False) ⟶ False) ⟶ ((x23 x30 ⟶ False) ⟶ False) ⟶ (x68 x30 ⟶ False) ⟶ ((x25 x31 ⟶ False) ⟶ False) ⟶ ((x1 x31 ⟶ False) ⟶ False) ⟶ ((x14 x31 ⟶ False) ⟶ False) ⟶ ((x46 x31 ⟶ False) ⟶ False) ⟶ ((x8 x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x69 . x14 x69 ⟶ (x15 (x15 x69) = x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 x65 ⟶ (x6 (x6 x69) = x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x23 x70 ⟶ (x50 (x61 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 . x8 x72 (x7 (x61 (x61 x70 x69) x71)) ⟶ (x20 (x54 x72) ⟶ False) ⟶ False) ⟶ (x45 x65 ⟶ False) ⟶ (∀ x69 x70 . x32 x70 ⟶ (x27 (x61 x69 x70) x33 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x44 x70 ⟶ (x27 (x61 x69 x70) x43 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x56 x70 ⟶ (x21 (x61 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x47 x70 ⟶ (x42 (x61 x69 x70) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x29 x70 ⟶ (x34 (x61 x69 x70) ⟶ False) ⟶ False) ⟶ (x45 x43 ⟶ False) ⟶ (x45 x33 ⟶ False) ⟶ ((x23 x60 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x50 x70 ⟶ (x35 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x27 x70 x33 ⟶ x62 x70 ⟶ (x25 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x27 x70 x43 ⟶ x62 x70 ⟶ (x36 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x21 x70 ⟶ (x1 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x42 x70 ⟶ (x46 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x34 x70 ⟶ (x14 (x22 x70 x69) ⟶ False) ⟶ False) ⟶ ((x32 x33 ⟶ False) ⟶ False) ⟶ ((x52 x60 ⟶ False) ⟶ False) ⟶ ((x52 x33 ⟶ False) ⟶ False) ⟶ ((x52 x43 ⟶ False) ⟶ False) ⟶ ((x52 x65 ⟶ False) ⟶ False) ⟶ (x68 x33 ⟶ False) ⟶ ((x44 x43 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x25 x70 ⟶ x25 x69 ⟶ (x25 (x16 x70 x69) ⟶ False) ⟶ False) ⟶ (x68 x43 ⟶ False) ⟶ ((x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x69 . x25 x69 ⟶ (x25 (x15 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x25 x69 ⟶ (x14 (x15 x69) ⟶ False) ⟶ False) ⟶ (x68 x65 ⟶ False) ⟶ (∀ x69 x70 . x25 x70 ⟶ x25 x69 ⟶ (x25 (x59 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . (x68 x70 ⟶ False) ⟶ (x68 x69 ⟶ False) ⟶ x8 x69 (x7 x70) ⟶ (x57 (x37 x69 x70) x70 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . (x8 (x41 x69) x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . (x68 x71 ⟶ False) ⟶ (x68 x69 ⟶ False) ⟶ x8 x69 (x7 x71) ⟶ x57 x70 x71 x69 ⟶ (x8 x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 x65 ⟶ x1 x69 ⟶ (x8 (x19 x70 x69) x65 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 x65 ⟶ x1 x69 ⟶ (x8 (x12 x70 x69) x65 ⟶ False) ⟶ False) ⟶ ((x8 x17 (x7 x65) ⟶ False) ⟶ False) ⟶ (∀ x69 . x14 x69 ⟶ (x14 (x15 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 x73 . x56 x73 ⟶ x56 x69 ⟶ x62 x72 ⟶ x8 x72 (x7 (x61 x70 x73)) ⟶ x62 x71 ⟶ x8 x71 (x7 (x61 x70 x69)) ⟶ (x8 (x10 x70 x73 x69 x72 x71) (x7 (x61 x70 x65)) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 x73 . x56 x73 ⟶ x56 x69 ⟶ x62 x72 ⟶ x8 x72 (x7 (x61 x70 x73)) ⟶ x62 x71 ⟶ x8 x71 (x7 (x61 x70 x69)) ⟶ (x62 (x10 x70 x73 x69 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ (x8 (x13 x70 x69) (x7 (x61 x65 x65)) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ (x62 (x13 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x34 x70 ⟶ x20 x69 ⟶ x62 x69 ⟶ x34 x69 ⟶ (x62 (x55 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x34 x70 ⟶ x20 x69 ⟶ x62 x69 ⟶ x34 x69 ⟶ (x20 (x55 x70 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x21 x70 ⟶ (x8 (x2 x70 x69) x65 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x53 x70 x69 ⟶ (x8 (x11 x69 x70) (x7 x69) ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 x65 ⟶ (x8 (x6 x69) x65 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x62 x70 ⟶ x8 x70 (x7 (x61 x65 x65)) ⟶ x1 x69 ⟶ (x8 (x4 x70 x69) x65 ⟶ False) ⟶ False) ⟶ ((x8 x3 (x7 (x61 x65 x65)) ⟶ False) ⟶ False) ⟶ ((x38 x3 x65 x65 ⟶ False) ⟶ False) ⟶ ((x62 x3 ⟶ False) ⟶ False) ⟶ ((x8 x5 (x7 (x61 x65 x65)) ⟶ False) ⟶ False) ⟶ ((x38 x5 x65 x65 ⟶ False) ⟶ False) ⟶ ((x62 x5 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x8 x70 x65 ⟶ x1 x69 ⟶ (x12 x70 x69 = x12 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 x72 x73 . x56 x73 ⟶ x56 x69 ⟶ x62 x72 ⟶ x8 x72 (x7 (x61 x70 x73)) ⟶ x62 x71 ⟶ x8 x71 (x7 (x61 x70 x69)) ⟶ (x10 x70 x73 x69 x72 x71 = x10 x70 x73 x69 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x14 x70 ⟶ x14 x69 ⟶ (x59 x70 x69 = x59 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x62 x70 ⟶ x34 x70 ⟶ x20 x69 ⟶ x62 x69 ⟶ x34 x69 ⟶ (x55 x70 x69 = x55 x69 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x20 x69 ⟶ (x50 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ x20 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 (x7 x43) ⟶ (x44 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 (x7 x65) ⟶ (x56 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x27 x69 x43 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x21 x69 ⟶ (x34 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x21 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x21 x69 ⟶ (x42 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x21 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x56 x69 ⟶ (x29 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x43 ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x43 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x68 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x68 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x56 x69 ⟶ (x47 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x33 ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x33 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x68 x71 ⟶ x8 x69 (x7 (x61 x71 x70)) ⟶ (x68 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x44 x69 ⟶ (x56 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x25 x69 ⟶ (x1 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x17 ⟶ (x50 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x17 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x65 ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x65 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x33 ⟶ (x27 x69 x43 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x27 x69 x33 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x8 x71 (x7 (x61 x69 x70)) ⟶ (x27 x71 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x8 x71 (x7 (x61 x70 x69)) ⟶ (x53 x71 x70 ⟶ False) ⟶ False) ⟶ (∀ x69 . x32 x69 ⟶ (x44 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x35 x69 ⟶ (x25 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x52 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 x17 ⟶ (x23 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x23 x70 ⟶ x8 x69 (x7 x70) ⟶ (x23 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x32 x70 ⟶ x8 x69 (x7 x70) ⟶ (x32 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x44 x70 ⟶ x8 x69 (x7 x70) ⟶ (x44 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x23 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x50 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x56 x70 ⟶ x8 x69 (x7 x70) ⟶ (x56 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x32 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x27 x69 x33 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x47 x70 ⟶ x8 x69 (x7 x70) ⟶ (x47 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x27 x69 x33 ⟶ False) ⟶ False) ⟶ (∀ x69 . x20 x69 ⟶ x50 x69 ⟶ (x20 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x8 x71 (x7 (x61 x69 x70)) ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x69 . x23 x69 ⟶ (x32 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 x33 ⟶ (x25 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x44 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x27 x69 x43 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x29 x70 ⟶ x8 x69 (x7 x70) ⟶ (x29 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x56 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x68 x69 ⟶ (x23 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x47 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x42 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x23 x70 ⟶ x8 x69 x70 ⟶ (x35 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 x71 . x29 x71 ⟶ x8 x69 (x7 (x61 x70 x71)) ⟶ (x34 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x32 x70 ⟶ x8 x69 x70 ⟶ (x25 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x50 x70 ⟶ x8 x69 (x7 x70) ⟶ (x50 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x44 x70 ⟶ x8 x69 x70 ⟶ (x36 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x27 x70 x33 ⟶ x8 x69 (x7 x70) ⟶ (x27 x69 x33 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x56 x70 ⟶ x8 x69 x70 ⟶ (x1 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x27 x70 x43 ⟶ x8 x69 (x7 x70) ⟶ (x27 x69 x43 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x47 x70 ⟶ x8 x69 x70 ⟶ (x46 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x21 x70 ⟶ x8 x69 (x7 x70) ⟶ (x21 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x29 x70 ⟶ x8 x69 x70 ⟶ (x14 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x42 x70 ⟶ x8 x69 (x7 x70) ⟶ (x42 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 (x7 x17) ⟶ (x23 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x20 x70 ⟶ x34 x70 ⟶ x8 x69 (x7 x70) ⟶ (x34 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 . x8 x69 (x7 x33) ⟶ (x32 x69 ⟶ False) ⟶ False) ⟶ (∀ x69 x70 . x0 x69 x70 ⟶ x0 x70 x69 ⟶ False) ⟶ (x66 (x10 x65 x65 x65 x5 x3) x39 ⟶ x2 (x13 (x10 x65 x65 x65 x5 x3) x39) x40 = x19 (x2 x3 x40) (x2 x5 x40) ⟶ False) ⟶ (x66 (x10 x65 x65 x65 x5 x3) x39 ⟶ (x0 x40 x39 ⟶ False) ⟶ False) ⟶ (x66 (x10 x65 x65 x65 x5 x3) x39 ⟶ (x8 x40 x65 ⟶ False) ⟶ False) ⟶ ((x9 x39 (x11 x65 (x10 x65 x65 x65 x5 x3)) ⟶ False) ⟶ False) ⟶ ((x8 x39 (x7 x65) ⟶ False) ⟶ False) ⟶ ((x63 x39 ⟶ False) ⟶ False) ⟶ False (proof)