Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCUp../cb640..
PUgv7../100f6..
vout
PrCUp../55a63.. 0.04 bars
TMXeK../2264f.. ownership of 1139b.. as prop with payaddr PrGSy.. rights free controlledby PrGSy.. upto 0
TMEoH../876d1.. ownership of 1c285.. as prop with payaddr PrGSy.. rights free controlledby PrGSy.. upto 0
PUXFj../e4a26.. doc published by PrGSy..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 1139b..t13_pre_ff : ∀ 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 . (x75 x77 x76 ⟶ False) ⟶ (x75 (x72 (x71 x69 (x74 (x70 x69 x77) x68))) (x73 (x72 (x71 x69 (x70 x69 x77))) x68) ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x75 x77 x76 ⟶ False) ⟶ x72 (x71 x69 (x74 (x70 x69 x77) x68)) = x73 (x72 (x71 x69 (x70 x69 x77))) x68 ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . (x75 x78 x79 ⟶ False) ⟶ (x75 x77 x76 ⟶ False) ⟶ x66 x78 ⟶ x66 x79 ⟶ x66 x77 ⟶ x75 (x65 x78 x77) (x65 x79 x77) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ (x1 x78 x77 ⟶ False) ⟶ x3 x78 x77 x79 ⟶ x1 x79 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ (x1 x78 x79 ⟶ False) ⟶ x3 x78 x77 x79 ⟶ x1 x79 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 x79 . (x75 x79 x76 ⟶ False) ⟶ (x75 x77 x68 ⟶ False) ⟶ (x75 (x4 x77 x79) (x4 x77 x78) ⟶ False) ⟶ x66 x78 ⟶ x66 x79 ⟶ x66 x77 ⟶ x75 x79 x78 ⟶ False) ⟶ (∀ x77 x78 x79 . (x73 (x65 x77 x79) (x65 x78 x79) = x65 (x73 x77 x78) x79 ⟶ False) ⟶ x64 x79 ⟶ x64 x78 ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ (x3 (x5 x77 x78) x77 x78 ⟶ False) ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 x79 . (x0 x79 ⟶ False) ⟶ (x0 x77 ⟶ False) ⟶ (x3 x78 x79 x77 ⟶ False) ⟶ x1 x78 x77 ⟶ x1 x77 (x2 x79) ⟶ False) ⟶ (∀ x77 x78 . (x3 (x74 x78 x77) x7 x6 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 . (x3 (x70 x78 x77) x7 x6 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 x79 . (x65 (x65 x77 x78) x79 = x65 x77 (x65 x78 x79) ⟶ False) ⟶ x64 x79 ⟶ x64 x78 ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . (x73 (x73 x77 x78) x79 = x73 x77 (x73 x78 x79) ⟶ False) ⟶ x64 x79 ⟶ x64 x78 ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 x78 . (x1 (x71 x78 x77) x7 ⟶ False) ⟶ x1 x77 x7 ⟶ x1 x78 x7 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 (x73 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 (x65 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ x63 (x62 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ x8 (x62 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 (x65 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 (x65 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 (x65 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 (x73 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x73 (x61 x78) (x61 x77) = x61 (x73 x78 x77) ⟶ False) ⟶ x64 x77 ⟶ x64 x78 ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x78 x79 ⟶ False) ⟶ x9 x78 x77 ⟶ x1 x77 (x2 x79) ⟶ False) ⟶ (∀ x77 x78 . (x4 x78 x77 = x71 x78 x77 ⟶ False) ⟶ x1 x77 x7 ⟶ x1 x78 x7 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ x67 x78 ⟶ x67 x77 ⟶ x0 (x73 x77 x78) ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ x67 x78 ⟶ x67 x77 ⟶ x0 (x73 x78 x77) ⟶ False) ⟶ (∀ x77 x78 . (x1 (x10 x77 x78) x7 ⟶ False) ⟶ x66 x77 ⟶ x1 x78 x7 ⟶ False) ⟶ (∀ x77 x78 . (x75 x77 x78 ⟶ False) ⟶ (x75 (x10 x78 x68) x77 ⟶ False) ⟶ x60 x77 ⟶ x60 x78 ⟶ False) ⟶ (∀ x77 x78 . (x75 (x72 x78) (x72 x77) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x75 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . x0 x78 ⟶ x59 x77 x78 ⟶ x1 x77 (x2 x78) ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x79 ⟶ x9 x78 x77 ⟶ x1 x77 (x2 x79) ⟶ False) ⟶ (∀ x77 x78 . (x77 = x78 ⟶ False) ⟶ x58 x78 ⟶ x58 x77 ⟶ x75 x78 x77 ⟶ x75 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x59 x77 x78 ⟶ False) ⟶ x0 x77 ⟶ x1 x77 (x2 x78) ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x59 x77 x78 ⟶ False) ⟶ x0 x77 ⟶ x1 x77 (x2 x78) ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x63 (x62 x77 x78) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x8 (x62 x78 x77) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x8 (x73 x77 x78) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ (x8 (x73 x78 x77) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 (x62 x78 x77) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 (x73 x77 x78) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 (x73 x78 x77) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x8 (x62 x77 x78) ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 x78 . (x70 x78 x77 = x65 x78 x77 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 . (x10 x77 x78 = x10 x78 x77 ⟶ False) ⟶ x66 x77 ⟶ x1 x78 x7 ⟶ False) ⟶ (∀ x77 x78 . (x10 x77 x78 = x73 x77 x78 ⟶ False) ⟶ x66 x77 ⟶ x1 x78 x7 ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 x77 = x73 x78 x77 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 . (x74 x78 x77 = x74 x77 x78 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 . (x70 x78 x77 = x70 x77 x78 ⟶ False) ⟶ x67 x77 ⟶ x1 x78 x6 ⟶ False) ⟶ (∀ x77 x78 . (x62 (x61 x78) (x61 x77) = x62 x77 x78 ⟶ False) ⟶ x64 x77 ⟶ x64 x78 ⟶ False) ⟶ (∀ x77 x78 . (x75 x78 (x73 x78 x77) ⟶ False) ⟶ x67 x77 ⟶ x67 x78 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ x75 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ (x63 x78 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x75 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ x75 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x63 x78 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ x63 x77 ⟶ x75 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ x8 x77 ⟶ x75 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ x8 x77 ⟶ x75 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 (x61 x77) = x62 x78 x77 ⟶ False) ⟶ x64 x77 ⟶ x64 x78 ⟶ False) ⟶ (∀ x77 x78 . (x57 x78 x77 ⟶ False) ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . x9 x77 x78 ⟶ x9 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x60 (x62 x78 x77) ⟶ False) ⟶ x60 x77 ⟶ x60 x78 ⟶ False) ⟶ (∀ x77 x78 . (x60 (x65 x78 x77) ⟶ False) ⟶ x60 x77 ⟶ x60 x78 ⟶ False) ⟶ (∀ x77 x78 . (x60 (x73 x78 x77) ⟶ False) ⟶ x60 x77 ⟶ x60 x78 ⟶ False) ⟶ (∀ x77 x78 . (x66 (x62 x78 x77) ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ False) ⟶ (∀ x77 x78 . (x66 (x4 x78 x77) ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ False) ⟶ (∀ x77 x78 . (x66 (x65 x78 x77) ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ False) ⟶ (∀ x77 x78 . (x66 (x73 x78 x77) ⟶ False) ⟶ x66 x77 ⟶ x66 x78 ⟶ False) ⟶ (∀ x77 x78 . (x67 (x65 x78 x77) ⟶ False) ⟶ x67 x77 ⟶ x67 x78 ⟶ False) ⟶ (∀ x77 x78 . (x67 (x73 x78 x77) ⟶ False) ⟶ x67 x77 ⟶ x67 x78 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ x0 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x56 x78 ⟶ False) ⟶ x56 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x11 x78 ⟶ False) ⟶ x11 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x55 x78 ⟶ False) ⟶ x55 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x12 x78 ⟶ False) ⟶ x12 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x54 x78 ⟶ False) ⟶ x54 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x13 x78 ⟶ False) ⟶ x13 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x53 x78 ⟶ False) ⟶ x53 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x14 x78 ⟶ False) ⟶ x14 x77 ⟶ x1 x78 (x2 x77) ⟶ False) ⟶ (∀ x77 x78 . (x75 x77 x78 ⟶ False) ⟶ (x75 x78 x77 ⟶ False) ⟶ x58 x77 ⟶ x58 x78 ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 (x2 x77) ⟶ False) ⟶ x57 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x65 x78 x77 = x65 x77 x78 ⟶ False) ⟶ x64 x77 ⟶ x64 x78 ⟶ False) ⟶ (∀ x77 x78 . (x73 x78 x77 = x73 x77 x78 ⟶ False) ⟶ x64 x77 ⟶ x64 x78 ⟶ False) ⟶ (∀ x77 x78 . (x0 x78 ⟶ False) ⟶ (x9 x77 x78 ⟶ False) ⟶ x1 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ (x75 x77 x78 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 x78 . (x8 x78 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ (x75 x77 x78 ⟶ False) ⟶ x66 x78 ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 x77 ⟶ False) ⟶ x9 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x52 x78 ⟶ False) ⟶ x52 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x60 x78 ⟶ False) ⟶ x56 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x51 x78 ⟶ False) ⟶ x11 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x66 x78 ⟶ False) ⟶ x55 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x58 x78 ⟶ False) ⟶ x12 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x64 x78 ⟶ False) ⟶ x54 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x50 x78 ⟶ False) ⟶ x14 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 x78 . (x67 x78 ⟶ False) ⟶ x13 x77 ⟶ x1 x78 x77 ⟶ False) ⟶ (∀ x77 . (x55 x77 ⟶ False) ⟶ x1 x77 (x2 x7) ⟶ False) ⟶ (∀ x77 . (x13 x77 ⟶ False) ⟶ x1 x77 (x2 x6) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x1 (x49 x77) (x2 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x1 (x15 x77) (x2 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x78 ⟶ x9 x77 x78 ⟶ False) ⟶ (∀ x77 x78 . (x75 x78 x78 ⟶ False) ⟶ x58 x77 ⟶ x58 x78 ⟶ False) ⟶ (∀ x77 . (x63 x77 ⟶ False) ⟶ x66 x77 ⟶ x8 (x61 x77) ⟶ False) ⟶ (∀ x77 . (x8 x77 ⟶ False) ⟶ x66 x77 ⟶ x63 (x61 x77) ⟶ False) ⟶ (∀ x77 . (x65 x77 (x61 x68) = x61 x77 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . x8 x77 ⟶ x1 x77 x6 ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x59 (x49 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x66 x77 ⟶ False) ⟶ x1 x77 x7 ⟶ False) ⟶ (∀ x77 . (x13 x77 ⟶ False) ⟶ x1 x77 x6 ⟶ False) ⟶ (∀ x77 . (x67 x77 ⟶ False) ⟶ x1 x77 x16 ⟶ False) ⟶ (∀ x77 . (x63 x77 ⟶ False) ⟶ (x64 (x61 x77) ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x8 x77 ⟶ False) ⟶ (x64 (x61 x77) ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x72 (x72 x77) = x72 x77 ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x8 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x8 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x0 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x0 x77 ⟶ x63 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x0 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 . x58 x77 ⟶ x0 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ x0 (x15 x77) ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x58 x77 ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x58 x77 ⟶ False) ⟶ (∀ x77 . (x0 x77 ⟶ False) ⟶ (x8 x77 ⟶ False) ⟶ (x63 x77 ⟶ False) ⟶ x58 x77 ⟶ False) ⟶ (∀ x77 . (x65 x68 x77 = x77 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . (x62 x77 x76 = x77 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . (x73 x77 x76 = x77 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . (x65 x77 x76 = x76 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . (x52 x77 ⟶ False) ⟶ x17 x77 ⟶ x18 x77 ⟶ False) ⟶ (∀ x77 . (x61 (x61 x77) = x77 ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 . (x60 (x61 x77) ⟶ False) ⟶ x60 x77 ⟶ False) ⟶ (∀ x77 . (x60 (x72 x77) ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x66 (x61 x77) ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x64 (x61 x77) ⟶ False) ⟶ x60 x77 ⟶ False) ⟶ (∀ x77 . (x64 (x61 x77) ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x64 (x61 x77) ⟶ False) ⟶ x64 x77 ⟶ False) ⟶ (∀ x77 x78 . (x78 = x77 ⟶ False) ⟶ x0 x77 ⟶ x0 x78 ⟶ False) ⟶ (∀ x77 . x67 x77 ⟶ x8 x77 ⟶ False) ⟶ (∀ x77 . (x19 x77 ⟶ False) ⟶ x14 x77 ⟶ False) ⟶ (∀ x77 . (x48 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x20 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x18 x77 ⟶ False) ⟶ x52 x77 ⟶ False) ⟶ (∀ x77 . (x17 x77 ⟶ False) ⟶ x52 x77 ⟶ False) ⟶ (∀ x77 . (x52 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x52 x77 ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x52 x77 ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x60 x77 ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x56 x77 ⟶ False) ⟶ x13 x77 ⟶ False) ⟶ (∀ x77 . (x11 x77 ⟶ False) ⟶ x56 x77 ⟶ False) ⟶ (∀ x77 . (x66 x77 ⟶ False) ⟶ x60 x77 ⟶ False) ⟶ (∀ x77 . (x66 x77 ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x55 x77 ⟶ False) ⟶ x11 x77 ⟶ False) ⟶ (∀ x77 . (x58 x77 ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x58 x77 ⟶ False) ⟶ x67 x77 ⟶ False) ⟶ (∀ x77 . (x12 x77 ⟶ False) ⟶ x55 x77 ⟶ False) ⟶ (∀ x77 . (x64 x77 ⟶ False) ⟶ x66 x77 ⟶ False) ⟶ (∀ x77 . (x54 x77 ⟶ False) ⟶ x55 x77 ⟶ False) ⟶ (∀ x77 . (x13 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x53 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x14 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x67 x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 . (x77 = x47 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (x72 (x71 x69 (x74 (x70 x69 x21) x68)) = x72 (x71 x69 (x70 x69 x21)) ⟶ False) ⟶ (∀ x77 . x59 (x46 x77) x77 ⟶ False) ⟶ (x75 x22 (x61 x68) ⟶ False) ⟶ (x75 x68 (x61 x68) ⟶ False) ⟶ (x75 x69 (x61 x68) ⟶ False) ⟶ (x75 x21 x76 ⟶ False) ⟶ (x75 x68 x22 ⟶ False) ⟶ (x75 x69 x22 ⟶ False) ⟶ (x75 x69 x68 ⟶ False) ⟶ (∀ x77 . x0 (x2 x77) ⟶ False) ⟶ (x0 x23 ⟶ False) ⟶ (x0 x45 ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ (x0 x44 ⟶ False) ⟶ (x0 x25 ⟶ False) ⟶ (x0 x43 ⟶ False) ⟶ (x0 x26 ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ (x0 x16 ⟶ False) ⟶ (x0 x68 ⟶ False) ⟶ (x0 x69 ⟶ False) ⟶ ((x3 x22 x7 x6 ⟶ False) ⟶ False) ⟶ ((x3 x68 x7 x6 ⟶ False) ⟶ False) ⟶ ((x3 x69 x7 x6 ⟶ False) ⟶ False) ⟶ ((x3 x76 x7 x6 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 (x46 x77) (x2 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 (x27 x77) (x2 x77) ⟶ False) ⟶ False) ⟶ ((x62 (x61 x69) (x61 x68) = x61 x68 ⟶ False) ⟶ False) ⟶ ((x73 (x61 x68) (x61 x68) = x61 x69 ⟶ False) ⟶ False) ⟶ ((x75 (x61 x68) (x61 x68) ⟶ False) ⟶ False) ⟶ ((x62 (x61 x68) (x61 x68) = x22 ⟶ False) ⟶ False) ⟶ ((x62 (x61 x68) (x61 x69) = x68 ⟶ False) ⟶ False) ⟶ ((x62 (x61 x69) (x61 x69) = x22 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 (x41 x77) x77 ⟶ False) ⟶ False) ⟶ ((x62 (x61 x68) x22 = x61 x68 ⟶ False) ⟶ False) ⟶ ((x62 (x61 x68) x68 = x61 x69 ⟶ False) ⟶ False) ⟶ ((x62 (x61 x69) x22 = x61 x69 ⟶ False) ⟶ False) ⟶ ((x65 (x61 x69) x68 = x61 x69 ⟶ False) ⟶ False) ⟶ ((x73 (x61 x68) x22 = x61 x68 ⟶ False) ⟶ False) ⟶ ((x73 (x61 x69) x68 = x61 x68 ⟶ False) ⟶ False) ⟶ ((x65 x68 (x61 x69) = x61 x69 ⟶ False) ⟶ False) ⟶ ((x73 x22 (x61 x68) = x61 x68 ⟶ False) ⟶ False) ⟶ ((x73 x68 (x61 x69) = x61 x68 ⟶ False) ⟶ False) ⟶ ((x75 (x61 x68) x22 ⟶ False) ⟶ False) ⟶ ((x75 (x61 x68) x68 ⟶ False) ⟶ False) ⟶ ((x75 (x61 x68) x69 ⟶ False) ⟶ False) ⟶ ((x1 x43 (x2 x7) ⟶ False) ⟶ False) ⟶ ((x1 x6 (x2 x7) ⟶ False) ⟶ False) ⟶ ((x73 (x61 x68) x68 = x22 ⟶ False) ⟶ False) ⟶ ((x73 (x61 x68) x69 = x68 ⟶ False) ⟶ False) ⟶ ((x73 (x61 x69) x69 = x22 ⟶ False) ⟶ False) ⟶ ((x62 x22 (x61 x68) = x68 ⟶ False) ⟶ False) ⟶ ((x62 x22 (x61 x69) = x69 ⟶ False) ⟶ False) ⟶ ((x62 x68 (x61 x68) = x69 ⟶ False) ⟶ False) ⟶ ((x73 x68 (x61 x68) = x22 ⟶ False) ⟶ False) ⟶ ((x73 x69 (x61 x68) = x68 ⟶ False) ⟶ False) ⟶ ((x73 x69 (x61 x69) = x22 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x57 x77 x77 ⟶ False) ⟶ False) ⟶ ((x62 x22 x68 = x61 x68 ⟶ False) ⟶ False) ⟶ ((x62 x22 x69 = x61 x69 ⟶ False) ⟶ False) ⟶ ((x62 x68 x69 = x61 x68 ⟶ False) ⟶ False) ⟶ ((x1 x40 x7 ⟶ False) ⟶ False) ⟶ ((x1 x22 x7 ⟶ False) ⟶ False) ⟶ ((x1 x22 x6 ⟶ False) ⟶ False) ⟶ ((x1 x47 x16 ⟶ False) ⟶ False) ⟶ ((x1 x68 x7 ⟶ False) ⟶ False) ⟶ ((x1 x68 x6 ⟶ False) ⟶ False) ⟶ ((x1 x69 x7 ⟶ False) ⟶ False) ⟶ ((x1 x69 x6 ⟶ False) ⟶ False) ⟶ ((x75 x22 x22 ⟶ False) ⟶ False) ⟶ ((x75 x22 x68 ⟶ False) ⟶ False) ⟶ ((x75 x22 x69 ⟶ False) ⟶ False) ⟶ ((x75 x68 x68 ⟶ False) ⟶ False) ⟶ ((x75 x68 x69 ⟶ False) ⟶ False) ⟶ ((x75 x69 x69 ⟶ False) ⟶ False) ⟶ ((x62 x68 x22 = x68 ⟶ False) ⟶ False) ⟶ ((x62 x68 x68 = x22 ⟶ False) ⟶ False) ⟶ ((x62 x69 x22 = x69 ⟶ False) ⟶ False) ⟶ ((x62 x69 x68 = x68 ⟶ False) ⟶ False) ⟶ ((x62 x69 x69 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x22 x22 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x22 x68 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x22 x69 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x68 x22 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x68 x68 = x68 ⟶ False) ⟶ False) ⟶ ((x65 x68 x69 = x69 ⟶ False) ⟶ False) ⟶ ((x65 x69 x22 = x22 ⟶ False) ⟶ False) ⟶ ((x65 x69 x68 = x69 ⟶ False) ⟶ False) ⟶ ((x73 x22 x22 = x22 ⟶ False) ⟶ False) ⟶ ((x73 x22 x68 = x68 ⟶ False) ⟶ False) ⟶ ((x73 x22 x69 = x69 ⟶ False) ⟶ False) ⟶ ((x73 x68 x22 = x68 ⟶ False) ⟶ False) ⟶ ((x73 x68 x68 = x69 ⟶ False) ⟶ False) ⟶ ((x73 x69 x22 = x69 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x0 (x27 x77) ⟶ False) ⟶ False) ⟶ ((x61 (x61 x68) = x68 ⟶ False) ⟶ False) ⟶ ((x61 (x61 x69) = x69 ⟶ False) ⟶ False) ⟶ ((x63 x39 ⟶ False) ⟶ False) ⟶ ((x63 x28 ⟶ False) ⟶ False) ⟶ ((x63 x68 ⟶ False) ⟶ False) ⟶ ((x63 x69 ⟶ False) ⟶ False) ⟶ ((x8 x38 ⟶ False) ⟶ False) ⟶ ((x8 x29 ⟶ False) ⟶ False) ⟶ ((x20 x24 ⟶ False) ⟶ False) ⟶ ((x20 x16 ⟶ False) ⟶ False) ⟶ ((x20 x7 ⟶ False) ⟶ False) ⟶ ((x18 x25 ⟶ False) ⟶ False) ⟶ ((x17 x25 ⟶ False) ⟶ False) ⟶ ((x52 x25 ⟶ False) ⟶ False) ⟶ ((x52 x43 ⟶ False) ⟶ False) ⟶ ((x52 x30 ⟶ False) ⟶ False) ⟶ ((x52 x16 ⟶ False) ⟶ False) ⟶ ((x0 x31 ⟶ False) ⟶ False) ⟶ ((x0 x37 ⟶ False) ⟶ False) ⟶ ((x0 x32 ⟶ False) ⟶ False) ⟶ ((x0 x22 ⟶ False) ⟶ False) ⟶ ((x0 x47 ⟶ False) ⟶ False) ⟶ ((x60 x36 ⟶ False) ⟶ False) ⟶ ((x60 x40 ⟶ False) ⟶ False) ⟶ ((x66 x37 ⟶ False) ⟶ False) ⟶ ((x66 x29 ⟶ False) ⟶ False) ⟶ ((x66 x28 ⟶ False) ⟶ False) ⟶ ((x66 x33 ⟶ False) ⟶ False) ⟶ ((x66 x40 ⟶ False) ⟶ False) ⟶ ((x55 x7 ⟶ False) ⟶ False) ⟶ ((x58 x31 ⟶ False) ⟶ False) ⟶ ((x58 x37 ⟶ False) ⟶ False) ⟶ ((x58 x38 ⟶ False) ⟶ False) ⟶ ((x58 x29 ⟶ False) ⟶ False) ⟶ ((x58 x39 ⟶ False) ⟶ False) ⟶ ((x58 x28 ⟶ False) ⟶ False) ⟶ ((x58 x35 ⟶ False) ⟶ False) ⟶ ((x58 x40 ⟶ False) ⟶ False) ⟶ ((x64 x37 ⟶ False) ⟶ False) ⟶ ((x64 x29 ⟶ False) ⟶ False) ⟶ ((x64 x28 ⟶ False) ⟶ False) ⟶ ((x64 x40 ⟶ False) ⟶ False) ⟶ ((x13 x24 ⟶ False) ⟶ False) ⟶ ((x13 x26 ⟶ False) ⟶ False) ⟶ ((x13 x42 ⟶ False) ⟶ False) ⟶ ((x13 x16 ⟶ False) ⟶ False) ⟶ ((x14 x23 ⟶ False) ⟶ False) ⟶ ((x67 x45 ⟶ False) ⟶ False) ⟶ ((x67 x34 ⟶ False) ⟶ False) ⟶ ((x67 x21 ⟶ False) ⟶ False) ⟶ ((x61 x22 = x22 ⟶ False) ⟶ False) ⟶ ((x76 = x47 ⟶ False) ⟶ False) ⟶ ((x16 = x6 ⟶ False) ⟶ False) ⟶ False (proof)