Search for blocks/addresses/...

Proofgold Asset

asset id
074a4d2d672d2867bcdda97bfa18241906c1e3bbde869d744de87b4167c7c950
asset hash
348664d9236d11292e083d96d3f09476e29037b6cce7b9568a067f4e8c3c1b08
bday / block
35122
tx
f9985..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem e4654.. : ∀ 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 : ι → ο . ∀ x78 . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x77 x83 ⟶ x2 x83 (x1 (x73 x80 x81)) ⟶ x77 x82 ⟶ x2 x82 (x1 (x73 x80 x81)) ⟶ x74 x80 x83 = x74 x80 x82 ⟶ x75 x83 (x76 x82 x83 x81 x80) = x75 x82 (x76 x82 x83 x81 x80) ⟶ (x83 = x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x77 x83 ⟶ x2 x83 (x1 (x73 x80 x81)) ⟶ x77 x82 ⟶ x2 x82 (x1 (x73 x80 x81)) ⟶ x74 x80 x83 = x74 x80 x82 ⟶ (x0 (x76 x82 x83 x81 x80) (x74 x80 x83) ⟶ False) ⟶ (x83 = x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x77 x83 ⟶ x2 x83 (x1 (x73 x80 x81)) ⟶ x77 x82 ⟶ x2 x82 (x1 (x73 x80 x81)) ⟶ x74 x80 x83 = x74 x80 x82 ⟶ (x2 (x76 x82 x83 x81 x80) x80 ⟶ False) ⟶ (x83 = x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x72 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x72 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 x71 ⟶ x2 x80 x70 ⟶ x81 = x80 ⟶ (x69 x81 = x68 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x4 x81 ⟶ (x75 (x6 x81) x80 = x5 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x83 (x1 (x73 x82 x81)) ⟶ x2 x80 (x1 (x73 x82 x81)) ⟶ x67 x82 x81 x83 x80 ⟶ (x67 x82 x81 x80 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x83 (x1 (x73 x82 x81)) ⟶ x2 x80 (x1 (x73 x82 x81)) ⟶ (x67 x82 x81 x83 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x72 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x83 (x1 (x73 x82 x81)) ⟶ x2 x80 (x1 (x73 x82 x81)) ⟶ x83 = x80 ⟶ (x67 x82 x81 x83 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x83 (x1 (x73 x82 x81)) ⟶ x2 x80 (x1 (x73 x82 x81)) ⟶ x67 x82 x81 x83 x80 ⟶ (x83 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x8 x81 x82 x80 = x6 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x66 x81 ⟶ (x65 x81 x80 = x75 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x10 x81 x80 ⟶ (x74 x80 x81 = x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x68 x80 = x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x5 x80 = x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x62 x81 ⟶ (x61 x81 x80 = x75 x81 x80 ⟶ False) ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x79 x12 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ ((x11 x14 ⟶ False) ⟶ False) ⟶ ((x64 x14 ⟶ False) ⟶ False) ⟶ ((x79 x14 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x16 (x15 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x15 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x11 x18 ⟶ False) ⟶ False) ⟶ ((x13 x19 ⟶ False) ⟶ False) ⟶ ((x17 x19 ⟶ False) ⟶ False) ⟶ ((x11 x19 ⟶ False) ⟶ False) ⟶ ((x64 x19 ⟶ False) ⟶ False) ⟶ (∀ x80 . x16 (x20 x80) x80 ⟶ False) ⟶ (∀ x80 . (x2 (x20 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x60 x22 ⟶ False) ⟶ False) ⟶ (x79 x22 ⟶ False) ⟶ ((x59 x58 ⟶ False) ⟶ False) ⟶ ((x11 x58 ⟶ False) ⟶ False) ⟶ ((x13 x57 ⟶ False) ⟶ False) ⟶ ((x59 x57 ⟶ False) ⟶ False) ⟶ ((x11 x57 ⟶ False) ⟶ False) ⟶ ((x64 x57 ⟶ False) ⟶ False) ⟶ (x79 x56 ⟶ False) ⟶ (∀ x80 . (x79 (x23 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x23 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x24 x25 ⟶ False) ⟶ False) ⟶ ((x55 x54 ⟶ False) ⟶ False) ⟶ (x79 x54 ⟶ False) ⟶ ((x2 x54 (x1 x70) ⟶ False) ⟶ False) ⟶ ((x60 x26 ⟶ False) ⟶ False) ⟶ (x79 x26 ⟶ False) ⟶ ((x11 x27 ⟶ False) ⟶ False) ⟶ ((x13 x53 ⟶ False) ⟶ False) ⟶ ((x79 x28 ⟶ False) ⟶ False) ⟶ ((x52 x51 ⟶ False) ⟶ False) ⟶ ((x77 x51 ⟶ False) ⟶ False) ⟶ ((x3 x51 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x29 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x29 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x30 (x31 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x10 (x31 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x3 (x31 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 (x31 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x2 (x31 x80 x81) (x1 (x73 x81 x80)) ⟶ False) ⟶ False) ⟶ ((x24 x50 ⟶ False) ⟶ False) ⟶ ((x13 x50 ⟶ False) ⟶ False) ⟶ ((x64 x50 ⟶ False) ⟶ False) ⟶ ((x11 x50 ⟶ False) ⟶ False) ⟶ ((x2 x50 x70 ⟶ False) ⟶ False) ⟶ ((x60 x32 ⟶ False) ⟶ False) ⟶ (x79 x32 ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x8 x81 x82 (x8 x81 x82 x80) = x8 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x77 x80 ⟶ x4 x80 ⟶ (x6 (x6 x80) = x6 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 x71 ⟶ (x69 (x69 x80) = x69 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x68 (x68 x80) = x68 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x5 (x5 x80) = x5 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x63 (x63 x80) = x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ (x52 (x73 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x2 x83 (x1 (x73 (x73 x81 x80) x82)) ⟶ (x3 (x9 x83) ⟶ False) ⟶ False) ⟶ (x33 x70 ⟶ False) ⟶ (∀ x80 x81 . x49 x81 ⟶ (x30 (x73 x80 x81) x48 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ (x30 (x73 x80 x81) x35 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x47 x81 ⟶ (x66 (x73 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x36 x81 ⟶ (x62 (x73 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ (x4 (x73 x80 x81) ⟶ False) ⟶ False) ⟶ (x33 x35 ⟶ False) ⟶ (x33 x48 ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x52 x81 ⟶ (x37 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x30 x81 x48 ⟶ x77 x81 ⟶ (x46 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x30 x81 x35 ⟶ x77 x81 ⟶ (x24 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x66 x81 ⟶ (x13 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x62 x81 ⟶ (x11 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x4 x81 ⟶ (x64 (x75 x81 x80) ⟶ False) ⟶ False) ⟶ (x79 x71 ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x21 x48 ⟶ False) ⟶ False) ⟶ ((x21 x35 ⟶ False) ⟶ False) ⟶ ((x21 x70 ⟶ False) ⟶ False) ⟶ (x79 x48 ⟶ False) ⟶ ((x34 x35 ⟶ False) ⟶ False) ⟶ (x79 x35 ⟶ False) ⟶ ((x47 x70 ⟶ False) ⟶ False) ⟶ ((x36 x71 ⟶ False) ⟶ False) ⟶ ((x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 (x1 x80) ⟶ False) ⟶ (x79 x70 ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x79 (x73 x81 x80) ⟶ False) ⟶ (∀ x80 . (x2 (x38 x80) x80 ⟶ False) ⟶ False) ⟶ ((x79 x45 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x2 (x8 x81 x82 x80) (x1 (x73 x81 x70)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x77 (x8 x81 x82 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x77 x80 ⟶ x4 x80 ⟶ (x66 (x6 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x77 x80 ⟶ x4 x80 ⟶ (x77 (x6 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x77 x80 ⟶ x4 x80 ⟶ (x3 (x6 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 x71 ⟶ (x2 (x69 x80) x71 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x66 x81 ⟶ (x2 (x65 x81 x80) x70 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x10 x81 x80 ⟶ (x2 (x74 x80 x81) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x70)) ⟶ (x2 (x39 x81 x80) (x1 (x73 x81 x71)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x70)) ⟶ (x77 (x39 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x2 (x68 x80) x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x2 (x5 x80) x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ (x13 (x63 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x62 x81 ⟶ (x2 (x61 x81 x80) x71 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x81 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ (x2 (x40 x81 x80) (x1 (x73 x81 x71)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x81 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ (x77 (x40 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x77 x80 ⟶ x2 x80 (x1 (x73 x81 x70)) ⟶ (x39 x81 x80 = x80 ⟶ False) ⟶ False) ⟶ ((x78 = x45 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x4 x81 ⟶ x3 x80 ⟶ x77 x80 ⟶ x66 x80 ⟶ x9 x80 = x9 x81 ⟶ x75 x80 (x41 x80 x81) = x5 (x75 x81 (x41 x80 x81)) ⟶ (x80 = x6 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x4 x81 ⟶ x3 x80 ⟶ x77 x80 ⟶ x66 x80 ⟶ x9 x80 = x9 x81 ⟶ (x0 (x41 x80 x81) (x9 x80) ⟶ False) ⟶ (x80 = x6 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x3 x82 ⟶ x77 x82 ⟶ x4 x82 ⟶ x3 x80 ⟶ x77 x80 ⟶ x66 x80 ⟶ x80 = x6 x82 ⟶ x0 x81 (x9 x80) ⟶ (x75 x80 x81 = x5 (x75 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x77 x81 ⟶ x4 x81 ⟶ x3 x80 ⟶ x77 x80 ⟶ x66 x80 ⟶ x80 = x6 x81 ⟶ (x9 x80 = x9 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x82 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ x77 x81 ⟶ x2 x81 (x1 (x73 x82 x71)) ⟶ x9 x81 = x9 x80 ⟶ x61 x81 (x42 x81 x80 x82) = x69 (x61 x80 (x42 x81 x80 x82)) ⟶ (x81 = x40 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x82 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ x77 x81 ⟶ x2 x81 (x1 (x73 x82 x71)) ⟶ x9 x81 = x9 x80 ⟶ (x0 (x42 x81 x80 x82) (x9 x81) ⟶ False) ⟶ (x81 = x40 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x82 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ x77 x81 ⟶ x2 x81 (x1 (x73 x82 x71)) ⟶ x9 x81 = x9 x80 ⟶ (x2 (x42 x81 x80 x82) x82 ⟶ False) ⟶ (x81 = x40 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . (x79 x83 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x83 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ x77 x81 ⟶ x2 x81 (x1 (x73 x83 x71)) ⟶ x81 = x40 x83 x80 ⟶ x2 x82 x83 ⟶ x0 x82 (x9 x81) ⟶ (x61 x81 x82 = x69 (x61 x80 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ x3 x80 ⟶ x10 x80 x82 ⟶ x30 x80 x71 ⟶ x77 x80 ⟶ x77 x81 ⟶ x2 x81 (x1 (x73 x82 x71)) ⟶ x81 = x40 x82 x80 ⟶ (x9 x81 = x9 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x3 x80 ⟶ (x52 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x3 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x35) ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x59 x80 ⟶ False) ⟶ (x17 x80 ⟶ False) ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x59 x80 ⟶ False) ⟶ (x17 x80 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x70) ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x11 x80 ⟶ x17 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x11 x80 ⟶ x59 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x11 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x30 x80 x35 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x71) ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ (x59 x80 ⟶ False) ⟶ (x17 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ (x59 x80 ⟶ False) ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x66 x80 ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x66 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x17 x80 ⟶ x59 x80 ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x17 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x17 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x66 x80 ⟶ (x62 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x66 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x47 x80 ⟶ (x7 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ (x17 x80 ⟶ False) ⟶ (x59 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x11 x80 ⟶ (x17 x80 ⟶ False) ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x35 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x35 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ x16 x80 x81 ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x47 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x59 x80 ⟶ x17 x80 ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x59 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ x59 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x48 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x48 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ x79 x80 ⟶ (x16 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x73 x82 x81)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ x17 x80 ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x34 x80 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x70 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x70 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x48 ⟶ (x30 x80 x35 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x48 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x16 x80 x81 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x73 x80 x81)) ⟶ (x30 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x73 x81 x80)) ⟶ (x10 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x46 x80 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x49 x80 ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x71 ⟶ (x62 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x30 x80 x71 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x21 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ x2 x80 (x1 x81) ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x49 x81 ⟶ x2 x80 (x1 x81) ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x2 x80 (x1 x81) ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x60 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x52 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x47 x81 ⟶ x2 x80 (x1 x81) ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x49 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x30 x80 x48 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x36 x81 ⟶ x2 x80 (x1 x81) ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 x71 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 x70 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x30 x80 x48 ⟶ False) ⟶ False) ⟶ (∀ x80 . x3 x80 ⟶ x52 x80 ⟶ (x3 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x73 x80 x81)) ⟶ (x3 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x37 x80 ⟶ (x55 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x34 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x30 x80 x35 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x2 x80 (x1 x81) ⟶ (x7 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x47 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x60 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x36 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x62 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ x2 x80 x81 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x2 x80 (x1 (x73 x81 x82)) ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x49 x81 ⟶ x2 x80 x81 ⟶ (x46 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x52 x81 ⟶ x2 x80 (x1 x81) ⟶ (x52 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x2 x80 x81 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x30 x81 x48 ⟶ x2 x80 (x1 x81) ⟶ (x30 x80 x48 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x47 x81 ⟶ x2 x80 x81 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x30 x81 x35 ⟶ x2 x80 (x1 x81) ⟶ (x30 x80 x35 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x36 x81 ⟶ x2 x80 x81 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x66 x81 ⟶ x2 x80 (x1 x81) ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x7 x81 ⟶ x2 x80 x81 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x62 x81 ⟶ x2 x80 (x1 x81) ⟶ (x62 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 ⟶ x4 x81 ⟶ x2 x80 (x1 x81) ⟶ (x4 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x48) ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (x67 x44 x71 (x40 x44 (x39 x44 x43)) (x39 x44 (x8 x44 x70 x43)) ⟶ False) ⟶ ((x2 x43 (x1 (x73 x44 x70)) ⟶ False) ⟶ False) ⟶ ((x77 x43 ⟶ False) ⟶ False) ⟶ (x79 x44 ⟶ False) ⟶ False (proof)