Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../58c42..
PUcaK../18116..
vout
PrNUD../bb9cc.. 0.04 bars
TMYBG../e4736.. ownership of c9a16.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMJ53../20d37.. ownership of 4745d.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUcCq../fd1a0.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c9a16.. : ∀ 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 ⟶ (x72 = x71 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 x72 . (x2 (x1 x71) (x0 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x69 x71 x72 ⟶ x70 x72 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x71 = x3 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x69 x71 x72 ⟶ x67 x72 (x68 x73) ⟶ x70 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x69 x72 x73 ⟶ x67 x73 (x68 x71) ⟶ (x67 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x2 x72 x71 ⟶ (x67 x72 (x68 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 (x68 x71) ⟶ (x2 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x71 x72 ⟶ (x70 x72 ⟶ False) ⟶ (x69 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x69 x72 x71 ⟶ (x67 x72 x71 ⟶ False) ⟶ False) ⟶ (x70 x66 ⟶ False) ⟶ (∀ x71 . (x2 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x67 x71 (x68 x73) ⟶ x67 x72 x71 ⟶ (x65 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x67 x71 (x68 x73) ⟶ x65 x72 x73 x71 ⟶ (x67 x72 x71 ⟶ False) ⟶ False) ⟶ ((x64 = x3 ⟶ False) ⟶ False) ⟶ ((x4 = x5 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x59 x71 ⟶ x62 x71 ⟶ (x60 (x61 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x59 x71 ⟶ x62 x71 ⟶ x70 (x61 x71) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x59 x71 ⟶ x62 x71 ⟶ (x67 (x61 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ x6 (x7 x71) ⟶ False) ⟶ (∀ x71 . (x6 x71 ⟶ False) ⟶ (x67 (x7 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x60 (x8 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x67 (x8 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x6 (x9 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x9 x71) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x67 (x9 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ ((x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x11 (x10 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x67 (x10 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ x70 (x12 x71) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ (x67 (x12 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . x11 (x14 x71) x71 ⟶ False) ⟶ (∀ x71 . (x67 (x14 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ (x70 x15 ⟶ False) ⟶ (∀ x71 . (x70 (x55 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x67 (x55 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ ((x54 x53 ⟶ False) ⟶ False) ⟶ ((x16 x53 ⟶ False) ⟶ False) ⟶ ((x59 x52 ⟶ False) ⟶ False) ⟶ ((x17 x52 ⟶ False) ⟶ False) ⟶ (x63 x52 ⟶ False) ⟶ ((x62 x52 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x51 x71 ⟶ False) ⟶ x13 x71 ⟶ x6 (x50 x71) ⟶ False) ⟶ (∀ x71 . (x51 x71 ⟶ False) ⟶ x13 x71 ⟶ (x67 (x50 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ (x6 (x49 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ x70 (x49 x71) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ (x67 (x49 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ ((x70 x18 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ x70 (x48 x71) ⟶ False) ⟶ (∀ x71 . (x70 x71 ⟶ False) ⟶ (x67 (x48 x71) (x68 x71) ⟶ False) ⟶ False) ⟶ ((x16 x47 ⟶ False) ⟶ False) ⟶ (x70 x47 ⟶ False) ⟶ ((x17 x46 ⟶ False) ⟶ False) ⟶ ((x62 x46 ⟶ False) ⟶ False) ⟶ ((x59 x45 ⟶ False) ⟶ False) ⟶ ((x17 x45 ⟶ False) ⟶ False) ⟶ ((x63 x45 ⟶ False) ⟶ False) ⟶ ((x62 x45 ⟶ False) ⟶ False) ⟶ ((x17 x44 ⟶ False) ⟶ False) ⟶ ((x63 x44 ⟶ False) ⟶ False) ⟶ ((x62 x44 ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x19 (x20 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x67 (x20 x71) (x68 (x58 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x67 x73 (x68 (x68 x74)) ⟶ x21 x74 x73 = x21 x72 x71 ⟶ (x73 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x67 x73 (x68 (x68 x74)) ⟶ x21 x74 x73 = x21 x71 x72 ⟶ (x74 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x22 x71 ⟶ False) ⟶ x13 x71 ⟶ x23 (x58 x71) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x67 x71 (x68 (x68 x72)) ⟶ (x17 (x21 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x67 x71 (x68 (x68 x72)) ⟶ x63 (x21 x72 x71) ⟶ False) ⟶ (∀ x71 . x22 x71 ⟶ x13 x71 ⟶ (x23 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x51 x71 ⟶ x13 x71 ⟶ (x6 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x62 x71 ⟶ (x17 (x21 (x58 x71) (x43 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x62 x71 ⟶ x63 (x21 (x58 x71) (x43 x71)) ⟶ False) ⟶ (∀ x71 . (x51 x71 ⟶ False) ⟶ x13 x71 ⟶ x6 (x58 x71) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x59 (x21 (x58 x71) (x43 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ (x17 (x21 (x58 x71) (x43 x71)) ⟶ False) ⟶ False) ⟶ ((x59 x24 ⟶ False) ⟶ False) ⟶ ((x17 x24 ⟶ False) ⟶ False) ⟶ (x63 x24 ⟶ False) ⟶ (∀ x71 x72 . x70 (x0 x71 x72) ⟶ False) ⟶ (∀ x71 . x70 (x1 x71) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 (x42 x73 x72 x71) ⟶ False) ⟶ (∀ x71 . (x63 x71 ⟶ False) ⟶ x13 x71 ⟶ x70 (x58 x71) ⟶ False) ⟶ (∀ x71 x72 . (x63 x72 ⟶ False) ⟶ x59 x72 ⟶ x62 x72 ⟶ x67 x71 (x58 x72) ⟶ (x41 (x1 x71) x72 ⟶ False) ⟶ False) ⟶ ((x70 x3 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 (x68 x71) ⟶ False) ⟶ (∀ x71 . x63 x71 ⟶ x13 x71 ⟶ (x70 (x58 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x59 x71 ⟶ x62 x71 ⟶ x70 (x43 x71) ⟶ False) ⟶ ((x57 x5 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x67 x71 (x68 x72) ⟶ (x65 (x40 x71 x72) x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x67 (x25 x71) x71 ⟶ False) ⟶ False) ⟶ ((x13 x39 ⟶ False) ⟶ False) ⟶ ((x62 x26 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ (x67 (x43 x71) (x68 (x68 (x58 x71))) ⟶ False) ⟶ False) ⟶ ((x70 x27 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x70 x73 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ x67 x71 (x68 x73) ⟶ x65 x72 x73 x71 ⟶ (x67 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ (x13 x71 ⟶ False) ⟶ False) ⟶ ((x62 x24 ⟶ False) ⟶ False) ⟶ ((x17 x24 ⟶ False) ⟶ False) ⟶ ((x65 x64 x38 x4 ⟶ False) ⟶ False) ⟶ ((x67 x4 (x68 x38) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 (x68 (x68 x71)) ⟶ (x62 (x21 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x67 x72 (x68 (x68 x71)) ⟶ (x17 (x21 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 . x17 x71 ⟶ x62 x71 ⟶ x58 x71 = x0 x64 x66 ⟶ x43 x71 = x42 x3 (x1 x66) (x0 x64 x66) ⟶ (x71 = x24 ⟶ False) ⟶ False) ⟶ (∀ x71 . x17 x71 ⟶ x62 x71 ⟶ x71 = x24 ⟶ (x43 x71 = x42 x3 (x1 x66) (x0 x64 x66) ⟶ False) ⟶ False) ⟶ (∀ x71 . x17 x71 ⟶ x62 x71 ⟶ x71 = x24 ⟶ (x58 x71 = x0 x64 x66 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ x19 x71 x72 ⟶ x69 (x30 x72) x71 ⟶ (x69 (x29 x72) x71 ⟶ False) ⟶ (x28 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ x19 x71 x72 ⟶ x69 (x29 x72) x71 ⟶ (x69 (x30 x72) x71 ⟶ False) ⟶ (x28 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ x29 x71 = x30 x71 ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ (x67 (x30 x71) (x58 x71) ⟶ False) ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ (x67 (x29 x71) (x58 x71) ⟶ False) ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ x63 x71 ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ x69 x72 (x31 x72 x71 x73) ⟶ x69 x71 (x31 x72 x71 x73) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ x69 x72 (x31 x72 x71 x73) ⟶ (x69 x72 (x31 x72 x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ (x69 x71 (x31 x72 x71 x73) ⟶ False) ⟶ x69 x71 (x31 x72 x71 x73) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ (x69 x71 (x31 x72 x71 x73) ⟶ False) ⟶ (x69 x72 (x31 x72 x71 x73) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ (x19 (x31 x72 x71 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x62 x73 ⟶ x28 x73 ⟶ (x63 x73 ⟶ False) ⟶ x67 x71 (x58 x73) ⟶ x67 x72 (x58 x73) ⟶ (x71 = x72 ⟶ False) ⟶ (x67 (x31 x72 x71 x73) (x68 (x58 x73)) ⟶ False) ⟶ False) ⟶ ((x3 = x27 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x37 x71 x72 x73 = x73 ⟶ False) ⟶ (x37 x71 x72 x73 = x72 ⟶ False) ⟶ (x69 (x37 x71 x72 x73) x71 ⟶ False) ⟶ (x71 = x0 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x69 (x37 x71 x72 x73) x71 ⟶ x37 x71 x72 x73 = x72 ⟶ (x71 = x0 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x69 (x37 x71 x72 x73) x71 ⟶ x37 x71 x72 x73 = x73 ⟶ (x71 = x0 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x73 = x0 x71 x72 ⟶ x74 = x72 ⟶ (x69 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x73 = x0 x72 x71 ⟶ x74 = x72 ⟶ (x69 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x74 = x0 x72 x73 ⟶ x69 x71 x74 ⟶ (x71 = x72 ⟶ False) ⟶ (x71 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ x69 x71 (x43 x72) ⟶ (x19 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x62 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ x19 x71 x72 ⟶ (x69 x71 (x43 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x36 x72 x71 = x71 ⟶ False) ⟶ (x69 (x36 x72 x71) x72 ⟶ False) ⟶ (x72 = x1 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x69 (x36 x72 x71) x72 ⟶ x36 x72 x71 = x71 ⟶ (x72 = x1 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x72 = x1 x73 ⟶ x71 = x73 ⟶ (x69 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x72 = x1 x73 ⟶ x69 x71 x72 ⟶ (x71 = x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . (x35 x71 x74 x73 x72 = x72 ⟶ False) ⟶ (x35 x71 x74 x73 x72 = x73 ⟶ False) ⟶ (x35 x71 x74 x73 x72 = x74 ⟶ False) ⟶ (x69 (x35 x71 x74 x73 x72) x71 ⟶ False) ⟶ (x71 = x42 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x69 (x35 x71 x74 x73 x72) x71 ⟶ x35 x71 x74 x73 x72 = x74 ⟶ (x71 = x42 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x69 (x35 x71 x74 x73 x72) x71 ⟶ x35 x71 x74 x73 x72 = x73 ⟶ (x71 = x42 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 . x69 (x35 x71 x74 x73 x72) x71 ⟶ x35 x71 x74 x73 x72 = x72 ⟶ (x71 = x42 x72 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 . x74 = x42 x71 x72 x73 ⟶ x75 = x73 ⟶ (x69 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 . x74 = x42 x71 x73 x72 ⟶ x75 = x73 ⟶ (x69 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 . x74 = x42 x73 x71 x72 ⟶ x75 = x73 ⟶ (x69 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 x74 x75 . x75 = x42 x74 x73 x72 ⟶ x69 x71 x75 ⟶ (x71 = x74 ⟶ False) ⟶ (x71 = x73 ⟶ False) ⟶ (x71 = x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x0 x72 x71 = x0 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x32 x71 x3 ⟶ (x63 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ x63 x71 ⟶ (x28 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x63 x71 ⟶ (x32 x71 x3 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x22 x71 ⟶ False) ⟶ x51 x71 ⟶ False) ⟶ (∀ x71 x72 . x33 x72 ⟶ x67 x71 (x68 x72) ⟶ (x33 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x51 x71 ⟶ (x22 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x23 x71 ⟶ (x33 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x6 x72 ⟶ x67 x71 (x68 x72) ⟶ (x6 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x22 x71 ⟶ False) ⟶ x22 x71 ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x22 x71 ⟶ False) ⟶ x63 x71 ⟶ False) ⟶ (∀ x71 . (x23 x71 ⟶ False) ⟶ x33 x71 ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x67 x71 (x68 x72) ⟶ x11 x71 x72 ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x63 x71 ⟶ (x22 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x63 x71 ⟶ (x63 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x16 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x16 x71 ⟶ (x16 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x57 x71 ⟶ (x33 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x57 x71 ⟶ x23 x71 ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x67 x71 (x68 x72) ⟶ x70 x71 ⟶ (x11 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x16 x71 ⟶ (x34 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ x16 x71 ⟶ (x16 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x70 x72 ⟶ False) ⟶ x67 x71 (x68 x72) ⟶ (x11 x71 x72 ⟶ False) ⟶ x70 x71 ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x51 x71 ⟶ False) ⟶ x63 x71 ⟶ False) ⟶ (∀ x71 x72 . x16 x72 ⟶ x67 x71 (x68 x72) ⟶ (x16 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x59 x72 ⟶ x62 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ x70 x71 ⟶ (x60 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x22 x72 ⟶ x13 x72 ⟶ x67 x71 (x68 (x58 x72)) ⟶ (x23 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x67 x71 (x68 x72) ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x63 x71 ⟶ (x51 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x16 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x51 x71 ⟶ False) ⟶ x63 x71 ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x32 x71 x66 ⟶ (x51 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ x32 x71 x66 ⟶ x63 x71 ⟶ False) ⟶ (∀ x71 . x13 x71 ⟶ (x63 x71 ⟶ False) ⟶ x51 x71 ⟶ (x32 x71 x66 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x69 x71 x72 ⟶ x69 x72 x71 ⟶ False) ⟶ (∀ x71 . x62 x71 ⟶ x17 x71 ⟶ (x71 = x21 (x58 x71) (x43 x71) ⟶ False) ⟶ False) ⟶ (x28 x24 ⟶ False) ⟶ False (proof)