Search for blocks/addresses/...

Proofgold Asset

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