Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../850cc..
PULYx../de4cf..
vout
PrNUD../f9cf7.. 0.04 bars
TMKJA../bc0d3.. ownership of 274ae.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMKag../d92ca.. ownership of 71d95.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUgXP../8a869.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 274ae.. : ∀ 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 . x77 x79 ⟶ x77 x78 ⟶ (x76 x79 x78 ⟶ False) ⟶ (x75 x78 ⟶ False) ⟶ (x74 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x0 x80 ⟶ x0 x78 ⟶ x1 x79 ⟶ (x3 x79 (x4 x80 x78) = x2 (x3 x79 x80) (x3 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x73 x79 ⟶ (x79 = x78 ⟶ False) ⟶ x73 x78 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ (x76 x79 x78 ⟶ False) ⟶ (x74 x79 ⟶ False) ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x72 x78 x79 ⟶ x73 x79 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ (x73 x79 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ (x75 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x78 = x71 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x72 x78 x79 ⟶ x6 x79 (x5 x80) ⟶ x73 x80 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ (x73 x78 ⟶ False) ⟶ (x75 x79 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x72 x79 x80 ⟶ x6 x80 (x5 x78) ⟶ (x6 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ (x74 x78 ⟶ False) ⟶ x74 x79 ⟶ False) ⟶ (∀ x78 x79 . x7 x79 x78 ⟶ (x6 x79 (x5 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x6 x79 (x5 x78) ⟶ (x7 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ (x75 x79 ⟶ False) ⟶ x75 x78 ⟶ False) ⟶ (∀ x78 . x1 x78 ⟶ (x2 x70 x78 = x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x6 x78 x79 ⟶ (x73 x79 ⟶ False) ⟶ (x72 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ x75 x78 ⟶ (x75 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x72 x79 x78 ⟶ (x6 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ x76 x79 x78 ⟶ x74 x79 ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ ((x6 x71 x8 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x76 x79 x78 ⟶ (x78 = x4 x79 (x69 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x76 x79 x78 ⟶ (x0 (x69 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x1 x78 ⟶ (x67 (x68 x79) (x68 x78) = x67 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x1 x78 ⟶ (x4 (x68 x79) (x68 x78) = x68 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x1 x80 ⟶ x1 x78 ⟶ x1 x79 ⟶ (x2 (x2 x80 x78) x79 = x2 x80 (x2 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x1 x80 ⟶ x1 x78 ⟶ x1 x79 ⟶ (x4 (x4 x80 x78) x79 = x4 x80 (x4 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x1 x80 ⟶ x1 x78 ⟶ x1 x79 ⟶ (x2 (x4 x80 x78) x79 = x4 (x2 x80 x79) (x2 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 . x1 x78 ⟶ (x2 x78 (x68 x70) = x68 x78 ⟶ False) ⟶ False) ⟶ ((x6 x70 x66 ⟶ False) ⟶ False) ⟶ ((x6 x70 x9 ⟶ False) ⟶ False) ⟶ ((x65 x70 x66 x9 ⟶ False) ⟶ False) ⟶ ((x74 x70 ⟶ False) ⟶ False) ⟶ (x73 x70 ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x1 x78 ⟶ (x4 x79 (x68 x78) = x67 x79 x78 ⟶ False) ⟶ False) ⟶ ((x6 x64 x66 ⟶ False) ⟶ False) ⟶ ((x6 x64 x9 ⟶ False) ⟶ False) ⟶ ((x65 x64 x66 x9 ⟶ False) ⟶ False) ⟶ ((x73 x64 ⟶ False) ⟶ False) ⟶ ((x68 (x68 x70) = x70 ⟶ False) ⟶ False) ⟶ ((x68 x70 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x68 x64 = x64 ⟶ False) ⟶ False) ⟶ ((x2 x70 x70 = x70 ⟶ False) ⟶ False) ⟶ ((x2 x70 x64 = x64 ⟶ False) ⟶ False) ⟶ ((x2 x64 x70 = x64 ⟶ False) ⟶ False) ⟶ ((x2 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ ((x67 (x68 x70) (x68 x70) = x64 ⟶ False) ⟶ False) ⟶ ((x67 (x68 x70) x64 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x67 x70 x70 = x64 ⟶ False) ⟶ False) ⟶ ((x67 x70 x64 = x70 ⟶ False) ⟶ False) ⟶ ((x67 x64 (x68 x70) = x70 ⟶ False) ⟶ False) ⟶ ((x67 x64 x70 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x67 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ ((x4 (x68 x70) x70 = x64 ⟶ False) ⟶ False) ⟶ ((x4 (x68 x70) x64 = x68 x70 ⟶ False) ⟶ False) ⟶ ((x4 x70 (x68 x70) = x64 ⟶ False) ⟶ False) ⟶ ((x4 x70 x64 = x70 ⟶ False) ⟶ False) ⟶ ((x4 x64 (x68 x70) = x68 x70 ⟶ False) ⟶ False) ⟶ ((x4 x64 x70 = x70 ⟶ False) ⟶ False) ⟶ ((x4 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ ((x76 (x68 x70) (x68 x70) ⟶ False) ⟶ False) ⟶ ((x76 (x68 x70) x70 ⟶ False) ⟶ False) ⟶ ((x76 (x68 x70) x64 ⟶ False) ⟶ False) ⟶ (x76 x70 (x68 x70) ⟶ False) ⟶ ((x76 x70 x70 ⟶ False) ⟶ False) ⟶ (x76 x70 x64 ⟶ False) ⟶ (x76 x64 (x68 x70) ⟶ False) ⟶ ((x76 x64 x70 ⟶ False) ⟶ False) ⟶ ((x76 x64 x64 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x63 x79 ⟶ x63 x78 ⟶ (x76 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x7 x78 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ (x62 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x10 x79 ⟶ x10 x78 ⟶ (x11 x79 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x11 x79 x78 ⟶ (x62 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x62 x79 x78 ⟶ (x11 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x73 x80 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ x6 x78 (x5 x80) ⟶ x6 x79 x78 ⟶ (x65 x79 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x73 x80 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ x6 x78 (x5 x80) ⟶ x65 x79 x80 x78 ⟶ (x6 x79 x78 ⟶ False) ⟶ False) ⟶ ((x9 = x8 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ ((x61 x13 ⟶ False) ⟶ False) ⟶ (x73 x13 ⟶ False) ⟶ (∀ x78 . (x60 x78 ⟶ False) ⟶ (x61 (x59 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x60 x78 ⟶ False) ⟶ x60 (x59 x78) ⟶ False) ⟶ (∀ x78 . (x60 x78 ⟶ False) ⟶ (x6 (x59 x78) (x5 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ (x14 (x15 x78) x70 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ (x6 (x15 x78) (x5 x78) ⟶ False) ⟶ False) ⟶ ((x0 x16 ⟶ False) ⟶ False) ⟶ (x73 x16 ⟶ False) ⟶ (∀ x78 . x17 x78 ⟶ (x14 (x18 x78) x78 ⟶ False) ⟶ False) ⟶ ((x63 x58 ⟶ False) ⟶ False) ⟶ ((x73 x58 ⟶ False) ⟶ False) ⟶ ((x77 x57 ⟶ False) ⟶ False) ⟶ ((x63 x57 ⟶ False) ⟶ False) ⟶ ((x1 x57 ⟶ False) ⟶ False) ⟶ ((x73 x57 ⟶ False) ⟶ False) ⟶ ((x0 x56 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x61 x78 ⟶ False) ⟶ x61 (x19 x78) ⟶ False) ⟶ (∀ x78 . (x61 x78 ⟶ False) ⟶ (x6 (x19 x78) (x5 x78) ⟶ False) ⟶ False) ⟶ ((x75 x20 ⟶ False) ⟶ False) ⟶ ((x63 x20 ⟶ False) ⟶ False) ⟶ ((x77 x21 ⟶ False) ⟶ False) ⟶ ((x75 x21 ⟶ False) ⟶ False) ⟶ ((x63 x21 ⟶ False) ⟶ False) ⟶ ((x1 x21 ⟶ False) ⟶ False) ⟶ ((x17 x22 ⟶ False) ⟶ False) ⟶ ((x61 x22 ⟶ False) ⟶ False) ⟶ ((x77 x22 ⟶ False) ⟶ False) ⟶ ((x63 x22 ⟶ False) ⟶ False) ⟶ ((x1 x22 ⟶ False) ⟶ False) ⟶ ((x0 x22 ⟶ False) ⟶ False) ⟶ ((x23 x22 ⟶ False) ⟶ False) ⟶ ((x55 x22 ⟶ False) ⟶ False) ⟶ ((x24 x22 ⟶ False) ⟶ False) ⟶ (x73 x22 ⟶ False) ⟶ ((x6 x22 x9 ⟶ False) ⟶ False) ⟶ (x61 x54 ⟶ False) ⟶ ((x74 x25 ⟶ False) ⟶ False) ⟶ ((x63 x25 ⟶ False) ⟶ False) ⟶ ((x77 x26 ⟶ False) ⟶ False) ⟶ ((x74 x26 ⟶ False) ⟶ False) ⟶ ((x63 x26 ⟶ False) ⟶ False) ⟶ ((x1 x26 ⟶ False) ⟶ False) ⟶ (x73 x27 ⟶ False) ⟶ ((x23 x53 ⟶ False) ⟶ False) ⟶ ((x55 x53 ⟶ False) ⟶ False) ⟶ ((x24 x53 ⟶ False) ⟶ False) ⟶ (x73 x53 ⟶ False) ⟶ ((x23 x52 ⟶ False) ⟶ False) ⟶ (x73 x52 ⟶ False) ⟶ ((x6 x52 (x5 x66) ⟶ False) ⟶ False) ⟶ ((x10 x28 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ (x61 (x51 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x73 (x51 x78) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ (x6 (x51 x78) (x5 x78) ⟶ False) ⟶ False) ⟶ ((x17 x29 ⟶ False) ⟶ False) ⟶ ((x61 x29 ⟶ False) ⟶ False) ⟶ ((x23 x29 ⟶ False) ⟶ False) ⟶ ((x55 x29 ⟶ False) ⟶ False) ⟶ ((x24 x29 ⟶ False) ⟶ False) ⟶ ((x63 x50 ⟶ False) ⟶ False) ⟶ ((x77 x30 ⟶ False) ⟶ False) ⟶ ((x73 x49 ⟶ False) ⟶ False) ⟶ ((x23 x31 ⟶ False) ⟶ False) ⟶ ((x17 x48 ⟶ False) ⟶ False) ⟶ ((x61 x48 ⟶ False) ⟶ False) ⟶ ((x77 x48 ⟶ False) ⟶ False) ⟶ ((x63 x48 ⟶ False) ⟶ False) ⟶ ((x1 x48 ⟶ False) ⟶ False) ⟶ ((x0 x48 ⟶ False) ⟶ False) ⟶ ((x23 x48 ⟶ False) ⟶ False) ⟶ ((x55 x48 ⟶ False) ⟶ False) ⟶ ((x24 x48 ⟶ False) ⟶ False) ⟶ (x73 x48 ⟶ False) ⟶ ((x10 x47 ⟶ False) ⟶ False) ⟶ ((x77 x47 ⟶ False) ⟶ False) ⟶ ((x1 x47 ⟶ False) ⟶ False) ⟶ ((x63 x47 ⟶ False) ⟶ False) ⟶ ((x6 x47 x66 ⟶ False) ⟶ False) ⟶ ((x61 x32 ⟶ False) ⟶ False) ⟶ (x73 x32 ⟶ False) ⟶ ((x17 x33 ⟶ False) ⟶ False) ⟶ (∀ x78 . x1 x78 ⟶ (x68 (x68 x78) = x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x75 x79 ⟶ False) ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ x75 (x4 x79 x78) ⟶ False) ⟶ (∀ x78 . (x61 x78 ⟶ False) ⟶ x61 (x5 x78) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ (x77 (x67 x79 x78) ⟶ False) ⟶ False) ⟶ (x61 x8 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ (x77 (x2 x79 x78) ⟶ False) ⟶ False) ⟶ ((x23 x8 ⟶ False) ⟶ False) ⟶ (x73 x8 ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x77 x78 ⟶ (x77 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ ((x34 x8 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ (x0 (x3 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ (x73 x78 ⟶ False) ⟶ x0 x78 ⟶ x73 (x4 x78 x79) ⟶ False) ⟶ (∀ x78 x79 . x10 x79 ⟶ x10 x78 ⟶ (x10 (x67 x79 x78) ⟶ False) ⟶ False) ⟶ ((x17 x8 ⟶ False) ⟶ False) ⟶ (∀ x78 . x77 x78 ⟶ (x77 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . x77 x78 ⟶ (x1 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x0 x78 ⟶ (x1 (x3 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ (x73 x78 ⟶ False) ⟶ x0 x78 ⟶ x73 (x4 x79 x78) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x10 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x1 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . x61 x78 ⟶ (x12 (x5 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x77 x79 ⟶ x0 x78 ⟶ (x77 (x3 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ (x0 (x2 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x10 x79 ⟶ x10 x78 ⟶ (x10 (x2 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x75 x79 ⟶ False) ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ x75 (x2 x79 x78) ⟶ False) ⟶ (∀ x78 x79 . (x74 x79 ⟶ False) ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ x75 (x2 x79 x78) ⟶ False) ⟶ (∀ x78 x79 . (x74 x79 ⟶ False) ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ x74 (x2 x78 x79) ⟶ False) ⟶ (∀ x78 x79 . (x74 x79 ⟶ False) ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ x74 (x2 x79 x78) ⟶ False) ⟶ (∀ x78 x79 . x75 x79 ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ (x74 (x67 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x75 x79 ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ (x75 (x67 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x74 x79 ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ (x75 (x67 x78 x79) ⟶ False) ⟶ False) ⟶ ((x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ (x0 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x10 x79 ⟶ x10 x78 ⟶ (x10 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x46 (x5 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x74 x79 ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ (x74 (x67 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x45 (x5 x78) ⟶ False) ⟶ (∀ x78 x79 . (x75 x79 ⟶ False) ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ x74 (x67 x78 x79) ⟶ False) ⟶ (∀ x78 x79 . (x75 x79 ⟶ False) ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ x75 (x67 x79 x78) ⟶ False) ⟶ (∀ x78 . x61 x78 ⟶ (x61 (x5 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ x74 (x68 x78) ⟶ False) ⟶ (∀ x78 . (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ (x1 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 . (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ x75 (x68 x78) ⟶ False) ⟶ (∀ x78 . (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ (x1 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x75 x79 ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ (x75 (x4 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x75 x79 ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ (x75 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x74 x79 ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ (x74 (x4 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x74 x79 ⟶ x77 x79 ⟶ (x75 x78 ⟶ False) ⟶ x77 x78 ⟶ (x74 (x4 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . (x74 x79 ⟶ False) ⟶ x77 x79 ⟶ (x74 x78 ⟶ False) ⟶ x77 x78 ⟶ x74 (x4 x79 x78) ⟶ False) ⟶ (∀ x78 x79 . (x73 x79 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ x6 x78 (x5 x79) ⟶ (x65 (x35 x78 x79) x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x6 (x44 x78) x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . (x73 x80 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ x6 x78 (x5 x80) ⟶ x65 x79 x80 x78 ⟶ (x6 x79 x80 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x5 x66) ⟶ False) ⟶ False) ⟶ (∀ x78 . x1 x78 ⟶ (x1 (x68 x78) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 x80 . x0 x80 ⟶ x0 x78 ⟶ x0 x79 ⟶ x78 = x2 x80 x79 ⟶ (x62 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x62 x79 x78 ⟶ (x78 = x2 x79 (x36 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x0 x79 ⟶ x0 x78 ⟶ x62 x79 x78 ⟶ (x0 (x36 x78 x79) ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x63 x79 ⟶ x63 x78 ⟶ (x76 x79 x78 ⟶ False) ⟶ (x76 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x1 x78 ⟶ (x2 x79 x78 = x2 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x1 x79 ⟶ x1 x78 ⟶ (x4 x79 x78 = x4 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x43 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x14 x78 x70 ⟶ (x60 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x14 x78 x70 ⟶ x73 x78 ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ (x74 x78 ⟶ False) ⟶ (x75 x78 ⟶ False) ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ (x74 x78 ⟶ False) ⟶ (x75 x78 ⟶ False) ⟶ (x73 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x6 x78 x8 ⟶ (x0 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x12 x79 ⟶ x6 x78 (x5 x79) ⟶ (x12 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x14 x78 x71 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ x63 x78 ⟶ x75 x78 ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ x63 x78 ⟶ x74 x78 ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ x63 x78 ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x0 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x12 x79 ⟶ x6 x78 x79 ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x14 x78 x71 ⟶ (x73 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x63 x78 ⟶ (x74 x78 ⟶ False) ⟶ (x75 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x63 x78 ⟶ (x74 x78 ⟶ False) ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x12 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x23 x78 ⟶ x61 x78 ⟶ (x0 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x75 x78 ⟶ x74 x78 ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x75 x78 ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x75 x78 ⟶ x73 x78 ⟶ False) ⟶ (∀ x78 x79 . x23 x79 ⟶ x6 x78 x79 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x61 x78 ⟶ False) ⟶ x60 x78 ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x63 x78 ⟶ (x75 x78 ⟶ False) ⟶ (x74 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x63 x78 ⟶ (x75 x78 ⟶ False) ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x77 x78 ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x42 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x60 x78 ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x6 x78 x8 ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x74 x78 ⟶ x75 x78 ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x74 x78 ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x63 x78 ⟶ x74 x78 ⟶ x73 x78 ⟶ False) ⟶ (∀ x78 . x77 x78 ⟶ (x1 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ x75 x78 ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x0 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x10 x78 ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x17 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x63 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x24 x78 ⟶ x55 x78 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x6 x78 x9 ⟶ x75 x78 ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x10 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x37 x78 ⟶ x38 x78 ⟶ (x46 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x61 x79 ⟶ x6 x78 (x5 x79) ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x17 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x6 x78 x66 ⟶ (x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x23 x78 ⟶ (x55 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x23 x78 ⟶ (x24 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x0 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x0 x78 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x46 x78 ⟶ (x38 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x46 x78 ⟶ (x37 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x73 x78 ⟶ (x61 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x17 x78 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . x45 x78 ⟶ (x60 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x43 x79 ⟶ x6 x78 (x5 x79) ⟶ (x43 x78 ⟶ False) ⟶ False) ⟶ (∀ x78 . (x73 x78 ⟶ False) ⟶ x60 x78 ⟶ (x14 x78 x70 ⟶ False) ⟶ False) ⟶ (∀ x78 x79 . x72 x78 x79 ⟶ x72 x79 x78 ⟶ False) ⟶ (x62 (x3 x41 x40) (x3 x41 x39) ⟶ False) ⟶ ((x76 x40 x39 ⟶ False) ⟶ False) ⟶ ((x0 x41 ⟶ False) ⟶ False) ⟶ ((x0 x39 ⟶ False) ⟶ False) ⟶ ((x0 x40 ⟶ False) ⟶ False) ⟶ False (proof)