Search for blocks/addresses/...

Proofgold Asset

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