Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../9541d..
PUbrB../ff70d..
vout
PrPhD../d12d7.. 3.38 bars
TMFko../dcb75.. ownership of fc0a3.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMMCJ../dec65.. ownership of 97acb.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUgLj../17290.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem fc0a3.. : ∀ 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 . x66 = x64 ⟶ (x63 x65 x66 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x66 = x64 ⟶ (x63 x66 x65 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x63 x65 x66 = x64 ⟶ (x65 = x64 ⟶ False) ⟶ (x66 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ (x66 = x65 ⟶ False) ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 x66 . x62 x65 x66 ⟶ x0 x66 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x65 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x60 x67 = x65 ⟶ x60 x66 = x65 ⟶ (x56 x67 x66 = x57 (x58 x65) (x59 x67 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x62 x65 x66 ⟶ x2 x66 (x1 x67) ⟶ x0 x67 ⟶ False) ⟶ (∀ x65 x66 x67 . x62 x66 x67 ⟶ x2 x67 (x1 x65) ⟶ (x2 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x3 x65 = x64 ⟶ (x65 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x60 x65 = x64 ⟶ (x65 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x4 x66 x65 ⟶ (x2 x66 (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x2 x66 (x1 x65) ⟶ (x4 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x2 x65 x66 ⟶ (x0 x66 ⟶ False) ⟶ (x62 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x54 x65 x64 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x66 x65 ⟶ (x2 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x4 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 x67) ⟶ (x5 x67 x65 x66 = x54 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x52 x66 x65 ⟶ (x53 x65 x66 = x60 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x55 x70 ⟶ x7 x70 x65 x66 ⟶ x2 x70 (x1 (x63 x65 x66)) ⟶ x55 x67 ⟶ x7 x67 x69 x68 ⟶ x2 x67 (x1 (x63 x69 x68)) ⟶ (x6 x65 x69 x66 x68 x70 x67 = x59 x70 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x58 x65 = x51 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x55 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x52 (x8 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x9 (x8 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 (x8 x65) ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ (x0 x11 ⟶ False) ⟶ (∀ x65 . (x12 x65 ⟶ False) ⟶ x12 (x13 x65) ⟶ False) ⟶ (∀ x65 . (x12 x65 ⟶ False) ⟶ (x2 (x13 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x55 (x14 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x50 (x14 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x52 (x14 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x14 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ (x12 (x15 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x0 (x15 x65) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ (x2 (x15 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (x49 x48 ⟶ False) ⟶ ((x55 x48 ⟶ False) ⟶ False) ⟶ ((x61 x48 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ (x17 (x16 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ (x2 (x16 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ ((x55 x18 ⟶ False) ⟶ False) ⟶ ((x9 x18 ⟶ False) ⟶ False) ⟶ ((x61 x18 ⟶ False) ⟶ False) ⟶ (x0 x18 ⟶ False) ⟶ (∀ x65 . x17 (x19 x65) x65 ⟶ False) ⟶ (∀ x65 . (x2 (x19 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x50 (x20 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x52 (x20 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x20 x65 x66) ⟶ False) ⟶ False) ⟶ ((x55 x47 ⟶ False) ⟶ False) ⟶ ((x9 x47 ⟶ False) ⟶ False) ⟶ ((x61 x47 ⟶ False) ⟶ False) ⟶ (x0 x21 ⟶ False) ⟶ (∀ x65 . (x0 (x46 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x46 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ ((x9 x45 ⟶ False) ⟶ False) ⟶ ((x61 x45 ⟶ False) ⟶ False) ⟶ ((x44 x43 ⟶ False) ⟶ False) ⟶ ((x55 x43 ⟶ False) ⟶ False) ⟶ ((x61 x43 ⟶ False) ⟶ False) ⟶ ((x0 x22 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x0 (x42 x65) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ (x2 (x42 x65) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x50 (x41 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x52 (x41 x66 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x41 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 (x41 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x2 (x41 x65 x66) (x1 (x63 x66 x65)) ⟶ False) ⟶ False) ⟶ ((x61 x23 ⟶ False) ⟶ False) ⟶ (x0 x23 ⟶ False) ⟶ ((x55 x24 ⟶ False) ⟶ False) ⟶ ((x61 x24 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 x67) ⟶ (x5 x67 x66 x66 = x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x54 x65 x65 = x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x63 x67 (x63 x65 x66))) ⟶ (x61 (x3 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x61 x65 ⟶ x0 (x3 x65) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x2 x68 (x1 (x63 (x63 x66 x65) x67)) ⟶ (x61 (x60 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x61 x65 ⟶ x0 (x60 x65) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x61 (x25 (x26 x66 x65) (x26 x68 x67)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x44 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x44 x65 ⟶ (x44 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x44 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x44 x65 ⟶ (x61 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x63 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x50 x67 x65 ⟶ x61 x66 ⟶ (x50 (x54 x67 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x40 (x26 x66 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 (x25 x65 x66) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x52 x67 x65 ⟶ x61 x66 ⟶ (x52 (x57 x67 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x52 x67 x66 ⟶ x61 x65 ⟶ (x61 (x57 x67 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 (x40 x65) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x52 x67 x65 ⟶ x61 x66 ⟶ (x52 (x54 x67 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x0 (x56 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 (x56 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 (x56 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x50 x67 x65 ⟶ x61 x66 ⟶ (x50 (x57 x66 x67) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x50 x67 x66 ⟶ x61 x65 ⟶ (x61 (x57 x65 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 . x12 x65 ⟶ x61 x65 ⟶ (x12 (x3 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x12 x65 ⟶ x61 x65 ⟶ (x12 (x60 x65) ⟶ False) ⟶ False) ⟶ ((x0 x64 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 (x1 x65) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ (x61 (x54 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x0 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x0 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x55 (x40 (x26 x66 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x38 x66 ⟶ x55 x66 ⟶ (x0 (x39 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x12 x65 ⟶ False) ⟶ x61 x65 ⟶ x55 x65 ⟶ x12 (x60 x65) ⟶ False) ⟶ (∀ x65 x66 x67 . x10 x67 ⟶ x61 x65 ⟶ x50 x65 x67 ⟶ x55 x65 ⟶ (x55 (x39 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x10 x67 ⟶ x61 x65 ⟶ x50 x65 x67 ⟶ x55 x65 ⟶ (x61 (x39 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x61 x65 ⟶ x9 x65 ⟶ (x9 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x61 x65 ⟶ x9 x65 ⟶ (x61 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x10 (x25 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ (x10 (x40 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ (x61 (x57 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ (x0 (x57 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ x12 (x3 x65) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ (x61 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ (x0 (x57 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ x49 x65 ⟶ (x12 (x3 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x0 (x3 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x61 x66 ⟶ x9 x66 ⟶ x55 x66 ⟶ x2 x65 (x60 x66) ⟶ x0 (x39 x66 x65) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x0 (x63 x66 x65) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x0 (x60 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x9 x65 ⟶ x55 x65 ⟶ (x37 (x3 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x27 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 x67) ⟶ (x2 (x5 x67 x65 x66) (x1 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x61 (x57 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x52 x66 x65 ⟶ (x2 (x53 x65 x66) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x55 x70 ⟶ x7 x70 x65 x66 ⟶ x2 x70 (x1 (x63 x65 x66)) ⟶ x55 x67 ⟶ x7 x67 x69 x68 ⟶ x2 x67 (x1 (x63 x69 x68)) ⟶ (x2 (x6 x65 x69 x66 x68 x70 x67) (x1 (x63 (x63 x65 x69) (x63 x66 x68))) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x55 x70 ⟶ x7 x70 x65 x66 ⟶ x2 x70 (x1 (x63 x65 x66)) ⟶ x55 x67 ⟶ x7 x67 x69 x68 ⟶ x2 x67 (x1 (x63 x69 x68)) ⟶ (x7 (x6 x65 x69 x66 x68 x70 x67) (x63 x65 x69) (x63 x66 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . x55 x70 ⟶ x7 x70 x65 x66 ⟶ x2 x70 (x1 (x63 x65 x66)) ⟶ x55 x67 ⟶ x7 x67 x69 x68 ⟶ x2 x67 (x1 (x63 x69 x68)) ⟶ (x55 (x6 x65 x69 x66 x68 x70 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 (x59 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 (x59 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 (x56 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x2 (x58 x65) (x1 (x63 x65 (x63 x65 x65))) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x7 (x58 x65) x65 (x63 x65 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x55 (x58 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x55 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 (x51 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x60 x65 = x63 (x60 x67) (x60 x66) ⟶ x28 x65 (x30 x65 x66 x67) (x29 x65 x66 x67) = x26 (x39 x67 (x30 x65 x66 x67)) (x39 x66 (x29 x65 x66 x67)) ⟶ (x65 = x59 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x60 x65 = x63 (x60 x67) (x60 x66) ⟶ (x62 (x29 x65 x66 x67) (x60 x66) ⟶ False) ⟶ (x65 = x59 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x60 x65 = x63 (x60 x67) (x60 x66) ⟶ (x62 (x30 x65 x66 x67) (x60 x67) ⟶ False) ⟶ (x65 = x59 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 . x61 x69 ⟶ x55 x69 ⟶ x61 x68 ⟶ x55 x68 ⟶ x61 x67 ⟶ x55 x67 ⟶ x67 = x59 x69 x68 ⟶ x62 x65 (x60 x69) ⟶ x62 x66 (x60 x68) ⟶ (x28 x67 x65 x66 = x26 (x39 x69 x65) (x39 x68 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x65 = x59 x67 x66 ⟶ (x60 x65 = x63 (x60 x67) (x60 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x60 x65 = x54 (x60 x67) (x60 x66) ⟶ x39 x65 (x36 x65 x66 x67) = x26 (x39 x67 (x36 x65 x66 x67)) (x39 x66 (x36 x65 x66 x67)) ⟶ (x65 = x56 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x60 x65 = x54 (x60 x67) (x60 x66) ⟶ (x62 (x36 x65 x66 x67) (x60 x65) ⟶ False) ⟶ (x65 = x56 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x61 x68 ⟶ x55 x68 ⟶ x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x66 = x56 x68 x67 ⟶ x62 x65 (x60 x66) ⟶ (x39 x66 x65 = x26 (x39 x68 x65) (x39 x67 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ x61 x66 ⟶ x55 x66 ⟶ x61 x65 ⟶ x55 x65 ⟶ x65 = x56 x67 x66 ⟶ (x60 x65 = x54 (x60 x67) (x60 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x26 x66 x65 = x25 (x25 x66 x65) (x40 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x63 x66 x67)) ⟶ x67 = x64 ⟶ x65 = x64 ⟶ (x7 x65 x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x63 x66 x67)) ⟶ x67 = x64 ⟶ x7 x65 x66 x67 ⟶ (x65 = x64 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 (x63 x65 x67)) ⟶ (x67 = x64 ⟶ False) ⟶ x65 = x53 x65 x66 ⟶ (x7 x66 x65 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x65 (x1 (x63 x66 x67)) ⟶ (x67 = x64 ⟶ False) ⟶ x7 x65 x66 x67 ⟶ (x66 = x53 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x55 x67 ⟶ (x28 x67 x65 x66 = x39 x67 (x26 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x66 (x1 x67) ⟶ (x5 x67 x65 x66 = x5 x67 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x54 x66 x65 = x54 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x25 x66 x65 = x25 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x10 x66 ⟶ x2 x65 (x1 x66) ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x50 x65 x66 ⟶ (x50 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x50 x65 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x50 x65 x66 ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x10 x66 ⟶ x2 x65 x66 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x10 x66 ⟶ x2 x65 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x52 x65 x66 ⟶ (x52 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x52 x65 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x61 x65 ⟶ x52 x65 x66 ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x10 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x50 x67 x65 ⟶ x2 x66 (x1 x67) ⟶ (x50 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x12 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x12 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x12 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x12 x66 ⟶ x2 x65 (x1 x66) ⟶ (x12 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x61 x67 ⟶ x52 x67 x65 ⟶ x2 x66 (x1 x67) ⟶ (x52 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ x12 x65 ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x2 x65 (x1 x66) ⟶ x17 x65 x66 ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x67 ⟶ x2 x65 (x1 (x63 x66 x67)) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ (x9 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x2 x65 (x1 x66) ⟶ x0 x65 ⟶ (x17 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x67 ⟶ x2 x65 (x1 (x63 x67 x66)) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ (x38 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x55 x66 ⟶ x2 x65 (x1 x66) ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ x2 x65 (x1 x66) ⟶ (x17 x65 x66 ⟶ False) ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x63 x65 x66)) ⟶ (x50 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x63 x66 x65)) ⟶ (x52 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x61 x66 ⟶ x2 x65 (x1 x66) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x44 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x61 x65 ⟶ x55 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ x2 x65 (x1 x66) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x2 x67 (x1 (x63 x65 x66)) ⟶ (x61 x67 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x62 x65 x66 ⟶ x62 x66 x65 ⟶ False) ⟶ (x56 x31 x32 = x57 (x58 x35) (x6 x35 x35 x33 x34 x31 x32) ⟶ False) ⟶ ((x2 x32 (x1 (x63 x35 x34)) ⟶ False) ⟶ False) ⟶ ((x7 x32 x35 x34 ⟶ False) ⟶ False) ⟶ ((x55 x32 ⟶ False) ⟶ False) ⟶ ((x2 x31 (x1 (x63 x35 x33)) ⟶ False) ⟶ False) ⟶ ((x7 x31 x35 x33 ⟶ False) ⟶ False) ⟶ ((x55 x31 ⟶ False) ⟶ False) ⟶ False (proof)