Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../98635..
PUcRU../4a2d9..
vout
PrNUD../fed12.. 0.01 bars
TMGSc../3ce9d.. ownership of 26bca.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMGja../b0d99.. ownership of 2b41b.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUV53../ea84f.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 26bca.. : ∀ 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 . x70 x72 ⟶ x70 x71 ⟶ (x69 x72 x71 ⟶ False) ⟶ (x68 x71 ⟶ False) ⟶ (x67 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x0 x73 ⟶ x0 x71 ⟶ x1 x72 ⟶ (x3 x72 (x4 x73 x71) = x2 (x3 x72 x73) (x3 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x66 x72 ⟶ (x72 = x71 ⟶ False) ⟶ x66 x71 ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x69 x72 x71 ⟶ False) ⟶ (x67 x72 ⟶ False) ⟶ (x68 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x71 x72 ⟶ x66 x72 ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ (x66 x72 ⟶ False) ⟶ (x67 x71 ⟶ False) ⟶ (x68 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x71 = x64 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x5 x71 x6 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x71 x72 ⟶ x62 x72 (x63 x73) ⟶ x66 x73 ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ (x66 x71 ⟶ False) ⟶ (x68 x72 ⟶ False) ⟶ (x67 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x5 x61 x71 = x61 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x65 x72 x73 ⟶ x62 x73 (x63 x71) ⟶ (x62 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ (x67 x71 ⟶ False) ⟶ x67 x72 ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x7 x71 x61 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x60 x72 x71 ⟶ (x62 x72 (x63 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 (x63 x71) ⟶ (x60 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ (x68 x72 ⟶ False) ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x2 x6 x71 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x71 x72 ⟶ (x66 x72 ⟶ False) ⟶ (x65 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ x68 x71 ⟶ (x68 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x2 x71 x61 = x61 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x72 x71 ⟶ (x62 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x72 x71 ⟶ x67 x72 ⟶ (x67 x71 ⟶ False) ⟶ False) ⟶ ((x62 x64 x8 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x4 x71 x61 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ x69 x61 x72 ⟶ x69 x6 x71 ⟶ (x69 x72 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x0 x71 ⟶ x69 x6 x72 ⟶ (x69 x6 (x3 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ x0 x71 ⟶ x69 x72 x71 ⟶ (x71 = x4 x72 (x9 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ x0 x71 ⟶ x69 x72 x71 ⟶ (x0 (x9 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x7 (x10 x72) (x10 x71) = x7 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x4 (x10 x72) (x10 x71) = x10 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x1 x73 ⟶ x1 x71 ⟶ x1 x72 ⟶ (x2 (x2 x73 x71) x72 = x2 x73 (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x1 x73 ⟶ x1 x71 ⟶ x1 x72 ⟶ (x4 (x4 x73 x71) x72 = x4 x73 (x4 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x1 x73 ⟶ x1 x71 ⟶ x1 x72 ⟶ (x2 (x4 x73 x71) x72 = x4 (x2 x73 x72) (x2 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x1 x73 ⟶ x1 x71 ⟶ x1 x72 ⟶ (x2 x73 (x5 x71 x72) = x5 (x2 x73 x71) x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x5 x6 x71 = x11 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x2 x71 (x10 x6) = x10 x71 ⟶ False) ⟶ False) ⟶ ((x62 x6 x12 ⟶ False) ⟶ False) ⟶ ((x62 x6 x59 ⟶ False) ⟶ False) ⟶ ((x13 x6 x12 x59 ⟶ False) ⟶ False) ⟶ ((x67 x6 ⟶ False) ⟶ False) ⟶ (x66 x6 ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x4 x72 (x10 x71) = x7 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x2 x72 (x11 x71) = x5 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x5 (x11 x72) (x11 x71) = x5 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x2 (x11 x72) (x11 x71) = x11 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ ((x62 x58 x12 ⟶ False) ⟶ False) ⟶ ((x62 x58 x59 ⟶ False) ⟶ False) ⟶ ((x13 x58 x12 x59 ⟶ False) ⟶ False) ⟶ ((x66 x58 ⟶ False) ⟶ False) ⟶ ((x10 (x10 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x10 x6 = x10 x6 ⟶ False) ⟶ False) ⟶ ((x10 x58 = x58 ⟶ False) ⟶ False) ⟶ ((x2 x6 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x2 x6 x58 = x58 ⟶ False) ⟶ False) ⟶ ((x2 x58 x6 = x58 ⟶ False) ⟶ False) ⟶ ((x2 x58 x58 = x58 ⟶ False) ⟶ False) ⟶ ((x5 (x10 x6) x6 = x10 x6 ⟶ False) ⟶ False) ⟶ ((x5 x6 (x10 x6) = x10 x6 ⟶ False) ⟶ False) ⟶ ((x5 x6 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x7 (x10 x6) (x10 x6) = x58 ⟶ False) ⟶ False) ⟶ ((x7 (x10 x6) x58 = x10 x6 ⟶ False) ⟶ False) ⟶ ((x7 x6 x6 = x58 ⟶ False) ⟶ False) ⟶ ((x7 x6 x58 = x6 ⟶ False) ⟶ False) ⟶ ((x7 x58 (x10 x6) = x6 ⟶ False) ⟶ False) ⟶ ((x7 x58 x6 = x10 x6 ⟶ False) ⟶ False) ⟶ ((x7 x58 x58 = x58 ⟶ False) ⟶ False) ⟶ ((x4 (x10 x6) x6 = x58 ⟶ False) ⟶ False) ⟶ ((x4 (x10 x6) x58 = x10 x6 ⟶ False) ⟶ False) ⟶ ((x4 x6 (x10 x6) = x58 ⟶ False) ⟶ False) ⟶ ((x4 x6 x58 = x6 ⟶ False) ⟶ False) ⟶ ((x4 x58 (x10 x6) = x10 x6 ⟶ False) ⟶ False) ⟶ ((x4 x58 x6 = x6 ⟶ False) ⟶ False) ⟶ ((x4 x58 x58 = x58 ⟶ False) ⟶ False) ⟶ ((x69 (x10 x6) (x10 x6) ⟶ False) ⟶ False) ⟶ ((x69 (x10 x6) x6 ⟶ False) ⟶ False) ⟶ ((x69 (x10 x6) x58 ⟶ False) ⟶ False) ⟶ (x69 x6 (x10 x6) ⟶ False) ⟶ ((x69 x6 x6 ⟶ False) ⟶ False) ⟶ (x69 x6 x58 ⟶ False) ⟶ (x69 x58 (x10 x6) ⟶ False) ⟶ ((x69 x58 x6 ⟶ False) ⟶ False) ⟶ ((x69 x58 x58 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ x14 x71 ⟶ (x69 x72 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x60 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x66 x73 ⟶ False) ⟶ (x66 x71 ⟶ False) ⟶ x62 x71 (x63 x73) ⟶ x62 x72 x71 ⟶ (x13 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x66 x73 ⟶ False) ⟶ (x66 x71 ⟶ False) ⟶ x62 x71 (x63 x73) ⟶ x13 x72 x73 x71 ⟶ (x62 x72 x71 ⟶ False) ⟶ False) ⟶ ((x61 = x64 ⟶ False) ⟶ False) ⟶ ((x59 = x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 x59 ⟶ x0 x71 ⟶ (x15 x72 x71 = x4 x72 x71 ⟶ False) ⟶ False) ⟶ ((x0 x57 ⟶ False) ⟶ False) ⟶ (x66 x57 ⟶ False) ⟶ ((x14 x56 ⟶ False) ⟶ False) ⟶ ((x66 x56 ⟶ False) ⟶ False) ⟶ ((x70 x55 ⟶ False) ⟶ False) ⟶ ((x14 x55 ⟶ False) ⟶ False) ⟶ ((x1 x55 ⟶ False) ⟶ False) ⟶ ((x66 x55 ⟶ False) ⟶ False) ⟶ ((x0 x54 ⟶ False) ⟶ False) ⟶ ((x68 x16 ⟶ False) ⟶ False) ⟶ ((x14 x16 ⟶ False) ⟶ False) ⟶ ((x70 x17 ⟶ False) ⟶ False) ⟶ ((x68 x17 ⟶ False) ⟶ False) ⟶ ((x14 x17 ⟶ False) ⟶ False) ⟶ ((x1 x17 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x53 x19 ⟶ False) ⟶ False) ⟶ (x66 x19 ⟶ False) ⟶ ((x67 x52 ⟶ False) ⟶ False) ⟶ ((x14 x52 ⟶ False) ⟶ False) ⟶ ((x70 x51 ⟶ False) ⟶ False) ⟶ ((x67 x51 ⟶ False) ⟶ False) ⟶ ((x14 x51 ⟶ False) ⟶ False) ⟶ ((x1 x51 ⟶ False) ⟶ False) ⟶ (x66 x50 ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x22 x48 ⟶ False) ⟶ False) ⟶ ((x47 x48 ⟶ False) ⟶ False) ⟶ (x66 x48 ⟶ False) ⟶ ((x49 x46 ⟶ False) ⟶ False) ⟶ (x66 x46 ⟶ False) ⟶ ((x62 x46 (x63 x12) ⟶ False) ⟶ False) ⟶ ((x53 x23 ⟶ False) ⟶ False) ⟶ (x66 x23 ⟶ False) ⟶ ((x24 x25 ⟶ False) ⟶ False) ⟶ ((x14 x45 ⟶ False) ⟶ False) ⟶ ((x70 x26 ⟶ False) ⟶ False) ⟶ ((x66 x44 ⟶ False) ⟶ False) ⟶ ((x20 x27 ⟶ False) ⟶ False) ⟶ ((x70 x27 ⟶ False) ⟶ False) ⟶ ((x1 x27 ⟶ False) ⟶ False) ⟶ ((x14 x27 ⟶ False) ⟶ False) ⟶ ((x62 x27 x12 ⟶ False) ⟶ False) ⟶ ((x49 x43 ⟶ False) ⟶ False) ⟶ ((x53 x28 ⟶ False) ⟶ False) ⟶ (x66 x28 ⟶ False) ⟶ ((x24 x29 ⟶ False) ⟶ False) ⟶ ((x70 x29 ⟶ False) ⟶ False) ⟶ ((x1 x29 ⟶ False) ⟶ False) ⟶ ((x14 x29 ⟶ False) ⟶ False) ⟶ ((x62 x29 x12 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x11 (x11 x71) = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x10 (x10 x71) = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x4 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x5 x72 x71) ⟶ False) ⟶ False) ⟶ (x42 x12 ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x20 x71 ⟶ (x20 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x20 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ ((x49 x8 ⟶ False) ⟶ False) ⟶ (x66 x8 ⟶ False) ⟶ ((x53 x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x20 x71 ⟶ (x20 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x20 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ ((x18 x8 ⟶ False) ⟶ False) ⟶ ((x18 x12 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x70 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x20 x72 ⟶ x20 x71 ⟶ (x20 (x5 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ x0 x71 ⟶ (x0 (x3 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ (x66 x71 ⟶ False) ⟶ x0 x71 ⟶ x66 (x4 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . x24 x72 ⟶ x24 x71 ⟶ (x24 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x70 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x20 x72 ⟶ x20 x71 ⟶ (x20 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x0 x71 ⟶ (x1 (x3 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ (x66 x71 ⟶ False) ⟶ x0 x71 ⟶ x66 (x4 x72 x71) ⟶ False) ⟶ ((x41 x12 ⟶ False) ⟶ False) ⟶ (∀ x71 . x24 x71 ⟶ (x24 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x24 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x67 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x5 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x5 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x5 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x5 x72 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x11 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x20 x72 ⟶ x20 x71 ⟶ (x20 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x0 x71 ⟶ (x70 (x3 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ x0 x71 ⟶ (x0 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x24 x72 ⟶ x24 x71 ⟶ (x24 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x68 x71 ⟶ x70 x71 ⟶ (x68 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x68 x71 ⟶ x70 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x11 x71) ⟶ False) ⟶ (∀ x71 . (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x67 x71 ⟶ x70 x71 ⟶ (x67 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x67 x71 ⟶ x70 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x2 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x67 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x2 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x67 x72 ⟶ False) ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x2 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x67 x72 ⟶ False) ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x2 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . x68 x72 ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x67 (x7 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x68 x72 ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x68 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x68 (x7 x71 x72) ⟶ False) ⟶ False) ⟶ ((x66 x64 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x20 x72 ⟶ x20 x71 ⟶ (x20 (x2 x72 x71) ⟶ False) ⟶ False) ⟶ (x66 x12 ⟶ False) ⟶ (∀ x71 x72 . x0 x72 ⟶ x0 x71 ⟶ (x0 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x24 x72 ⟶ x24 x71 ⟶ (x24 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x67 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x7 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x68 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x7 x72 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x10 x71) ⟶ False) ⟶ (∀ x71 . (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x68 (x10 x71) ⟶ False) ⟶ (∀ x71 . (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x68 x72 ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x68 (x4 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x68 x72 ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ (x68 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x67 (x4 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 ⟶ x70 x72 ⟶ (x68 x71 ⟶ False) ⟶ x70 x71 ⟶ (x67 (x4 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x67 x72 ⟶ False) ⟶ x70 x72 ⟶ (x67 x71 ⟶ False) ⟶ x70 x71 ⟶ x67 (x4 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x66 x72 ⟶ False) ⟶ (x66 x71 ⟶ False) ⟶ x62 x71 (x63 x72) ⟶ (x13 (x30 x71 x72) x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x62 (x40 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x66 x73 ⟶ False) ⟶ (x66 x71 ⟶ False) ⟶ x62 x71 (x63 x73) ⟶ x13 x72 x73 x71 ⟶ (x62 x72 x73 ⟶ False) ⟶ False) ⟶ ((x13 x61 x12 x59 ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x1 (x11 x71) ⟶ False) ⟶ False) ⟶ ((x62 x59 (x63 x12) ⟶ False) ⟶ False) ⟶ (∀ x71 . x1 x71 ⟶ (x1 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 x59 ⟶ x0 x71 ⟶ (x13 (x15 x72 x71) x12 x59 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x5 x72 x71 = x2 x72 (x11 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x7 x72 x71 = x4 x72 (x10 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x14 x72 ⟶ x14 x71 ⟶ (x69 x72 x71 ⟶ False) ⟶ (x69 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x2 x72 x71 = x2 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x1 x72 ⟶ x1 x71 ⟶ (x4 x72 x71 = x4 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 x59 ⟶ x0 x71 ⟶ (x15 x72 x71 = x15 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ (x67 x71 ⟶ False) ⟶ (x68 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ (x67 x71 ⟶ False) ⟶ (x68 x71 ⟶ False) ⟶ (x66 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 x8 ⟶ (x0 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 (x63 x12) ⟶ (x41 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ x14 x71 ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ x14 x71 ⟶ x67 x71 ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ x14 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x0 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 x71 ⟶ False) ⟶ x14 x71 ⟶ (x67 x71 ⟶ False) ⟶ (x68 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 x71 ⟶ False) ⟶ x14 x71 ⟶ (x67 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x49 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x68 x71 ⟶ x67 x71 ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x68 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x68 x71 ⟶ x66 x71 ⟶ False) ⟶ (∀ x71 x72 . x49 x72 ⟶ x62 x71 x72 ⟶ (x49 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x41 x71 ⟶ (x32 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 x71 ⟶ False) ⟶ x14 x71 ⟶ (x68 x71 ⟶ False) ⟶ (x67 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x66 x71 ⟶ False) ⟶ x14 x71 ⟶ (x68 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x33 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x41 x71 ⟶ (x39 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x67 x71 ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x67 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x67 x71 ⟶ x66 x71 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x1 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x49 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x0 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x38 x71 ⟶ (x41 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x24 x71 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x24 x71 ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x47 x71 ⟶ x22 x71 ⟶ (x49 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 x59 ⟶ x68 x71 ⟶ False) ⟶ (∀ x71 . x34 x71 ⟶ (x38 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x24 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x18 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 x59 ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x53 x72 ⟶ x62 x71 (x63 x72) ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x34 x72 ⟶ x62 x71 (x63 x72) ⟶ (x34 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x38 x72 ⟶ x62 x71 (x63 x72) ⟶ (x38 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x41 x72 ⟶ x62 x71 (x63 x72) ⟶ (x41 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x39 x72 ⟶ x62 x71 (x63 x72) ⟶ (x39 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 x12 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x20 x71 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x49 x71 ⟶ (x22 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x49 x71 ⟶ (x47 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x0 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x0 x71 ⟶ (x49 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x53 x71 ⟶ (x34 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x32 x72 ⟶ x62 x71 (x63 x72) ⟶ (x32 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x66 x71 ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x53 x72 ⟶ x62 x71 x72 ⟶ (x0 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x34 x72 ⟶ x62 x71 x72 ⟶ (x24 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x38 x72 ⟶ x62 x71 x72 ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x41 x72 ⟶ x62 x71 x72 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x39 x72 ⟶ x62 x71 x72 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x32 x72 ⟶ x62 x71 x72 ⟶ (x1 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 (x63 x59) ⟶ (x53 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x31 x72 ⟶ x62 x71 (x63 x72) ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x65 x71 x72 ⟶ x65 x72 x71 ⟶ False) ⟶ (x69 (x3 x36 x35) (x3 x36 x37) ⟶ False) ⟶ ((x69 x6 x36 ⟶ False) ⟶ False) ⟶ ((x69 x35 x37 ⟶ False) ⟶ False) ⟶ ((x0 x37 ⟶ False) ⟶ False) ⟶ ((x70 x36 ⟶ False) ⟶ False) ⟶ ((x13 x35 x12 x59 ⟶ False) ⟶ False) ⟶ False (proof)