Search for blocks/addresses/...

Proofgold Signed Transaction

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