Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../94a9c..
PULfo../d344b..
vout
PrPhD../74961.. 3.41 bars
TMGoV../4ad63.. ownership of b1641.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMUi8../450eb.. ownership of bcc85.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUXey../0809b.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem b1641.. : ∀ 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 . x73 x75 ⟶ (x75 = x74 ⟶ False) ⟶ x73 x74 ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x73 x75 ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x74 = x72 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x74 x75 ⟶ x2 x75 (x1 x76) ⟶ x73 x76 ⟶ False) ⟶ (∀ x74 x75 x76 . x0 x75 x76 ⟶ x2 x76 (x1 x74) ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 ⟶ x3 x74 ⟶ x5 x75 x74 ⟶ (x4 x74 ⟶ False) ⟶ x4 x75 ⟶ False) ⟶ (∀ x74 x75 . x71 x75 x74 ⟶ (x2 x75 (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x75 (x1 x74) ⟶ (x71 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x2 x74 x75 ⟶ (x73 x75 ⟶ False) ⟶ (x0 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x75 x74 ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 ⟶ x3 x74 ⟶ x5 x75 x74 ⟶ x4 x75 ⟶ (x4 x74 ⟶ False) ⟶ False) ⟶ ((x2 x72 x6 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x2 x74 x76 ⟶ x70 x75 (x67 x68 x69) ⟶ x61 x75 ⟶ x65 x75 x76 x66 ⟶ x2 x75 (x1 (x64 x76 x66)) ⟶ (x5 (x62 x75 x74) (x62 (x63 x76) x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ x2 x74 x76 ⟶ x70 x75 (x67 x68 x69) ⟶ x61 x75 ⟶ x65 x75 x76 x66 ⟶ x2 x75 (x1 (x64 x76 x66)) ⟶ (x5 (x62 (x7 x76) x74) (x62 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . x61 x77 ⟶ x65 x77 x74 x75 ⟶ x2 x77 (x1 (x64 x74 x75)) ⟶ x61 x76 ⟶ x65 x76 x74 x75 ⟶ x2 x76 (x1 (x64 x74 x75)) ⟶ x60 x74 x75 x77 x76 ⟶ (x60 x74 x75 x76 x77 ⟶ False) ⟶ False) ⟶ ((x2 x69 x66 ⟶ False) ⟶ False) ⟶ ((x2 x69 x59 ⟶ False) ⟶ False) ⟶ ((x8 x69 x66 x59 ⟶ False) ⟶ False) ⟶ ((x4 x69 ⟶ False) ⟶ False) ⟶ (x73 x69 ⟶ False) ⟶ ((x5 x69 x69 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . x61 x77 ⟶ x65 x77 x74 x75 ⟶ x2 x77 (x1 (x64 x74 x75)) ⟶ x61 x76 ⟶ x65 x76 x74 x75 ⟶ x2 x76 (x1 (x64 x74 x75)) ⟶ (x60 x74 x75 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x58 x75 ⟶ x58 x74 ⟶ (x5 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x71 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . x61 x77 ⟶ x65 x77 x74 x75 ⟶ x2 x77 (x1 (x64 x74 x75)) ⟶ x61 x76 ⟶ x65 x76 x74 x75 ⟶ x2 x76 (x1 (x64 x74 x75)) ⟶ x77 = x76 ⟶ (x60 x74 x75 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 x77 . x61 x77 ⟶ x65 x77 x74 x75 ⟶ x2 x77 (x1 (x64 x74 x75)) ⟶ x61 x76 ⟶ x65 x76 x74 x75 ⟶ x2 x76 (x1 (x64 x74 x75)) ⟶ x60 x74 x75 x77 x76 ⟶ (x77 = x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x2 x75 x74 ⟶ (x8 x75 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x8 x75 x76 x74 ⟶ (x2 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x57 x74 x75 = x56 x74 x75 ⟶ False) ⟶ False) ⟶ ((x68 = x72 ⟶ False) ⟶ False) ⟶ ((x59 = x6 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x9 x74 x75 = x56 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x54 x75 ⟶ (x62 x75 x74 = x53 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 ⟶ x3 x74 ⟶ (x67 x75 x74 = x10 x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x51 (x52 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x52 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . x51 (x50 x74) x74 ⟶ False) ⟶ (∀ x74 . (x2 (x50 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x11 x48 ⟶ False) ⟶ False) ⟶ (x73 x48 ⟶ False) ⟶ (x73 x12 ⟶ False) ⟶ (∀ x74 . (x73 (x47 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x47 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ ((x11 x46 ⟶ False) ⟶ False) ⟶ (x73 x46 ⟶ False) ⟶ ((x73 x45 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x61 x14 ⟶ False) ⟶ False) ⟶ ((x55 x14 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ x73 (x44 x74) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x44 x74) (x1 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x70 (x43 x74 x75) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x15 (x43 x75 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x55 (x43 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 (x43 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x43 x74 x75) (x1 (x64 x75 x74)) ⟶ False) ⟶ False) ⟶ ((x11 x16 ⟶ False) ⟶ False) ⟶ (x73 x16 ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x42 x18 ⟶ False) ⟶ False) ⟶ ((x19 x18 ⟶ False) ⟶ False) ⟶ ((x41 x18 ⟶ False) ⟶ False) ⟶ (x73 x18 ⟶ False) ⟶ ((x2 x18 (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x11 x75 ⟶ (x13 (x64 x74 x75) ⟶ False) ⟶ False) ⟶ (x40 x66 ⟶ False) ⟶ (∀ x74 x75 . x20 x75 ⟶ (x70 (x64 x74 x75) x21 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x39 x75 ⟶ (x70 (x64 x74 x75) x38 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x42 x75 ⟶ (x54 (x64 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x19 x75 ⟶ (x37 (x64 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x41 x75 ⟶ (x22 (x64 x74 x75) ⟶ False) ⟶ False) ⟶ (x40 x38 ⟶ False) ⟶ (x40 x21 ⟶ False) ⟶ ((x11 x6 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x13 x75 ⟶ (x23 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x70 x75 x21 ⟶ x61 x75 ⟶ (x36 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x70 x75 x38 ⟶ x61 x75 ⟶ (x24 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x54 x75 ⟶ (x3 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x37 x75 ⟶ (x58 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x22 x75 ⟶ (x35 (x53 x75 x74) ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x49 x6 ⟶ False) ⟶ False) ⟶ ((x49 x21 ⟶ False) ⟶ False) ⟶ ((x49 x38 ⟶ False) ⟶ False) ⟶ ((x49 x66 ⟶ False) ⟶ False) ⟶ (x73 x21 ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 (x34 x74 x75) ⟶ False) ⟶ (x73 x38 ⟶ False) ⟶ ((x42 x66 ⟶ False) ⟶ False) ⟶ ((x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 (x1 x74) ⟶ False) ⟶ (x73 x66 ⟶ False) ⟶ (∀ x74 x75 . x23 x75 ⟶ x23 x74 ⟶ (x11 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x36 x75 ⟶ x36 x74 ⟶ (x20 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x24 x75 ⟶ x24 x74 ⟶ (x39 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 ⟶ x3 x74 ⟶ (x42 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x58 x75 ⟶ x58 x74 ⟶ (x19 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x35 x75 ⟶ x35 x74 ⟶ (x41 (x34 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x73 (x64 x75 x74) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ (x8 (x25 x74 x75) x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x2 (x33 x74) x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . (x73 x76 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ x2 x74 (x1 x76) ⟶ x8 x75 x76 x74 ⟶ (x2 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x57 x75 x74) (x1 (x64 x74 x66)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x61 (x57 x74 x75) ⟶ False) ⟶ False) ⟶ ((x8 x68 x66 x59 ⟶ False) ⟶ False) ⟶ ((x2 x59 (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x2 (x32 x75 x74) (x1 (x64 (x64 x75 x74) x66)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x65 (x32 x75 x74) (x64 x75 x74) x66 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x61 (x32 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x70 (x32 x75 x74) (x67 x68 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x63 x74) (x1 (x64 x74 x66)) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x65 (x63 x74) x74 x66 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x61 (x63 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x70 (x63 x74) (x67 x68 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x2 (x9 x75 x74) (x1 (x64 x74 (x34 x72 x69))) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x65 (x9 x75 x74) x74 (x34 x72 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x61 (x9 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x2 (x26 x75 x74) (x1 (x64 (x64 x75 x74) x66)) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x65 (x26 x75 x74) (x64 x75 x74) x66 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x61 (x26 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x70 (x26 x75 x74) (x67 x68 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x2 (x7 x74) (x1 (x64 x74 x66)) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x65 (x7 x74) x74 x66 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x61 (x7 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x70 (x7 x74) (x67 x68 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x61 (x56 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x55 (x56 x74 x75) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x61 x75 ⟶ x54 x75 ⟶ (x2 (x62 x75 x74) x66 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x3 x75 ⟶ x3 x74 ⟶ (x2 (x67 x75 x74) (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x63 x74 = x57 x74 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . (x73 x74 ⟶ False) ⟶ (x7 x74 = x57 x72 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x32 x75 x74 = x9 (x64 x75 x74) (x64 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ (x73 x74 ⟶ False) ⟶ (x26 x75 x74 = x9 x72 (x64 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x58 x75 ⟶ x58 x74 ⟶ (x5 x75 x74 ⟶ False) ⟶ (x5 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x34 x75 x74 = x34 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x55 x74 ⟶ (x13 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ x55 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x38) ⟶ (x39 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x66) ⟶ (x42 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x70 x74 x38 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x54 x74 ⟶ (x22 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x54 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x54 x74 ⟶ (x37 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x54 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x42 x74 ⟶ (x41 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x66) ⟶ x73 x74 ⟶ (x17 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x38 ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x38 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x2 x74 (x1 x75) ⟶ x51 x74 x75 ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x42 x74 ⟶ (x19 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x21 ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x21 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ x73 x74 ⟶ (x51 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x73 x76 ⟶ x2 x74 (x1 (x64 x76 x75)) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x39 x74 ⟶ (x42 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x59 ⟶ (x13 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x59 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x66 ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x66 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x21 ⟶ (x70 x74 x38 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x70 x74 x21 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 x75) ⟶ (x51 x74 x75 ⟶ False) ⟶ x73 x74 ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x64 x74 x75)) ⟶ (x70 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x64 x75 x74)) ⟶ (x15 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x74 . x20 x74 ⟶ (x39 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x49 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 x59 ⟶ (x11 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x11 x75 ⟶ x2 x74 (x1 x75) ⟶ (x11 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x20 x75 ⟶ x2 x74 (x1 x75) ⟶ (x20 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x39 x75 ⟶ x2 x74 (x1 x75) ⟶ (x39 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x11 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x13 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x42 x75 ⟶ x2 x74 (x1 x75) ⟶ (x42 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x20 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x70 x74 x21 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x19 x75 ⟶ x2 x74 (x1 x75) ⟶ (x19 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x70 x74 x21 ⟶ False) ⟶ False) ⟶ (∀ x74 . x55 x74 ⟶ x13 x74 ⟶ (x55 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x73 x75 ⟶ x2 x74 (x1 x75) ⟶ (x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x2 x76 (x1 (x64 x74 x75)) ⟶ (x55 x76 ⟶ False) ⟶ False) ⟶ (∀ x74 . x11 x74 ⟶ (x20 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x66) ⟶ x17 x74 ⟶ (x27 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 (x64 x75 x66)) ⟶ x70 x74 (x67 x68 x69) ⟶ x61 x74 ⟶ x65 x74 x75 x66 ⟶ (x65 x74 x75 x66 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 (x64 x75 x66)) ⟶ x70 x74 (x67 x68 x69) ⟶ x61 x74 ⟶ x65 x74 x75 x66 ⟶ (x61 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . (x73 x75 ⟶ False) ⟶ x2 x74 (x1 (x64 x75 x66)) ⟶ x70 x74 (x67 x68 x69) ⟶ x61 x74 ⟶ x65 x74 x75 x66 ⟶ (x70 x74 (x67 x68 x69) ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x39 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x70 x74 x38 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x41 x75 ⟶ x2 x74 (x1 x75) ⟶ (x41 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x42 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x73 x74 ⟶ (x11 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x19 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x37 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x11 x75 ⟶ x2 x74 x75 ⟶ (x23 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 x76 . x41 x76 ⟶ x2 x74 (x1 (x64 x75 x76)) ⟶ (x22 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x20 x75 ⟶ x2 x74 x75 ⟶ (x36 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x13 x75 ⟶ x2 x74 (x1 x75) ⟶ (x13 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x39 x75 ⟶ x2 x74 x75 ⟶ (x24 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x70 x75 x21 ⟶ x2 x74 (x1 x75) ⟶ (x70 x74 x21 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x42 x75 ⟶ x2 x74 x75 ⟶ (x3 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x70 x75 x38 ⟶ x2 x74 (x1 x75) ⟶ (x70 x74 x38 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x19 x75 ⟶ x2 x74 x75 ⟶ (x58 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x54 x75 ⟶ x2 x74 (x1 x75) ⟶ (x54 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x41 x75 ⟶ x2 x74 x75 ⟶ (x35 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x37 x75 ⟶ x2 x74 (x1 x75) ⟶ (x37 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x59) ⟶ (x11 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x55 x75 ⟶ x22 x75 ⟶ x2 x74 (x1 x75) ⟶ (x22 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 . x2 x74 (x1 x21) ⟶ (x20 x74 ⟶ False) ⟶ False) ⟶ (∀ x74 x75 . x0 x74 x75 ⟶ x0 x75 x74 ⟶ False) ⟶ (x5 (x62 (x26 x29 x28) x30) (x62 x31 x30) ⟶ x5 (x62 x31 x30) (x62 (x32 x29 x28) x30) ⟶ False) ⟶ ((x2 x31 (x1 (x64 (x64 x29 x28) x66)) ⟶ False) ⟶ False) ⟶ ((x65 x31 (x64 x29 x28) x66 ⟶ False) ⟶ False) ⟶ ((x61 x31 ⟶ False) ⟶ False) ⟶ ((x70 x31 (x67 x68 x69) ⟶ False) ⟶ False) ⟶ ((x2 x30 (x64 x29 x28) ⟶ False) ⟶ False) ⟶ (x73 x28 ⟶ False) ⟶ (x73 x29 ⟶ False) ⟶ False (proof)