Proofgold Proposition

∀ 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 . (x76 x80 ⟶ False) ⟶ (x60 x80 ⟶ False) ⟶ x75 x80 ⟶ x61 x80 ⟶ x74 x80 ⟶ x62 x80 ⟶ x73 x80 ⟶ x63 x80 ⟶ x72 x80 ⟶ x64 x80 ⟶ x71 x80 ⟶ x65 x80 ⟶ x69 x79 (x70 x80) ⟶ x69 x77 (x70 x80) ⟶ x69 x78 (x70 x80) ⟶ (x66 (x70 x80) (x68 x80) x79 (x66 (x70 x80) (x67 x80) x77 x78) = x66 (x70 x80) (x67 x80) (x66 (x70 x80) (x68 x80) x79 x77) (x66 (x70 x80) (x68 x80) x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x78 ⟶ (x78 = x77 ⟶ False) ⟶ x0 x77 ⟶ False) ⟶ (∀ x77 x78 . x59 x77 x78 ⟶ x0 x78 ⟶ False) ⟶ (∀ x77 . x0 x77 ⟶ (x77 = x1 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x59 x77 x78 ⟶ x69 x78 (x58 x79) ⟶ x0 x79 ⟶ False) ⟶ (∀ x77 x78 x79 . x59 x78 x79 ⟶ x69 x79 (x58 x77) ⟶ (x69 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x57 x78 x77 ⟶ (x69 x78 (x58 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x69 x78 (x58 x77) ⟶ (x57 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x69 x77 x78 ⟶ (x0 x78 ⟶ False) ⟶ (x59 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x59 x78 x77 ⟶ (x69 x78 x77 ⟶ False) ⟶ False) ⟶ (x0 x56 ⟶ False) ⟶ (∀ x77 . (x57 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ x72 x79 ⟶ x55 x79 ⟶ x69 x77 (x70 x79) ⟶ x69 x78 (x70 x79) ⟶ (x54 x79 x77 x78 = x53 x79 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . x2 x80 ⟶ x4 x80 (x5 x77 x77) x77 ⟶ x69 x80 (x58 (x5 (x5 x77 x77) x77)) ⟶ x69 x78 x77 ⟶ x69 x79 x77 ⟶ (x66 x77 x80 x78 x79 = x3 x80 x78 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ x0 (x52 x77) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ (x69 (x52 x77) (x58 (x70 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x51 x77 ⟶ x49 (x48 x77) ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x51 x77 ⟶ (x69 (x48 x77) (x58 (x70 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ (x49 (x47 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ x0 (x47 x77) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ (x69 (x47 x77) (x58 (x70 x77)) ⟶ False) ⟶ False) ⟶ ((x50 x6 ⟶ False) ⟶ False) ⟶ (x76 x6 ⟶ False) ⟶ ((x7 x6 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x46 (x45 x77 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x8 (x45 x78 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x44 (x45 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x0 (x45 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x69 (x45 x77 x78) (x58 (x5 x78 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x7 x77 ⟶ x9 (x10 x77) x77 ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x7 x77 ⟶ (x69 (x10 x77) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x9 (x11 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x69 (x11 x77) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x12 x77 ⟶ False) ⟶ x51 x77 ⟶ x13 (x70 x77) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ x51 x77 ⟶ (x13 (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x50 x77 ⟶ x51 x77 ⟶ (x49 (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x50 x77 ⟶ False) ⟶ x51 x77 ⟶ x49 (x70 x77) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ x51 x77 ⟶ x0 (x70 x77) ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ x51 x77 ⟶ (x0 (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x9 (x14 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x69 x77 x78 ⟶ (x42 (x43 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x69 (x15 x77) x77 ⟶ False) ⟶ False) ⟶ ((x65 x41 ⟶ False) ⟶ False) ⟶ ((x16 x17 ⟶ False) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ ((x55 x20 ⟶ False) ⟶ False) ⟶ ((x7 x36 ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x51 x35 ⟶ False) ⟶ False) ⟶ ((x23 x24 ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x69 (x34 x77) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x55 x77 ⟶ (x69 (x25 x77) (x58 (x5 (x5 (x70 x77) (x70 x77)) (x70 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x55 x77 ⟶ (x4 (x25 x77) (x5 (x70 x77) (x70 x77)) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x55 x77 ⟶ (x2 (x25 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x78 x79 ⟶ x42 x77 x79 x78 ⟶ (x69 x77 (x58 (x5 (x5 x79 x79) x79)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x78 x79 ⟶ x42 x77 x79 x78 ⟶ (x4 x77 (x5 x79 x79) x79 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x78 x79 ⟶ x42 x77 x79 x78 ⟶ (x2 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x16 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x21 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x16 x77 ⟶ (x40 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x16 x77 ⟶ (x18 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x40 x77 ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x40 x77 ⟶ (x7 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x18 x77 ⟶ (x55 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x18 x77 ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x38 x77 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x55 x77 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x23 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x21 x77 ⟶ (x7 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x23 x77 ⟶ (x51 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ x72 x79 ⟶ x55 x79 ⟶ x69 x77 (x70 x79) ⟶ x69 x78 (x70 x79) ⟶ (x69 (x54 x79 x77 x78) (x70 x79) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x55 x79 ⟶ x69 x77 (x70 x79) ⟶ x69 x78 (x70 x79) ⟶ (x69 (x53 x79 x77 x78) (x70 x79) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . x2 x80 ⟶ x4 x80 (x5 x77 x77) x77 ⟶ x69 x80 (x58 (x5 (x5 x77 x77) x77)) ⟶ x69 x78 x77 ⟶ x69 x79 x77 ⟶ (x69 (x66 x77 x80 x78 x79) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x69 (x14 x77) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ x65 x77 ⟶ (x42 (x68 x77) (x70 x77) (x14 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x61 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x63 x77 ⟶ x72 x77 ⟶ x64 x77 ⟶ x71 x77 ⟶ x65 x77 ⟶ (x69 (x67 x77) (x58 (x5 (x5 (x70 x77) (x70 x77)) (x70 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x61 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x63 x77 ⟶ x72 x77 ⟶ x64 x77 ⟶ x71 x77 ⟶ x65 x77 ⟶ (x4 (x67 x77) (x5 (x70 x77) (x70 x77)) (x70 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x76 x77 ⟶ False) ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x61 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x63 x77 ⟶ x72 x77 ⟶ x64 x77 ⟶ x71 x77 ⟶ x65 x77 ⟶ (x2 (x67 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x7 x77 ⟶ (x14 x77 = x34 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ x65 x77 ⟶ (x68 x77 = x25 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x44 x79 ⟶ x2 x79 ⟶ (x3 x79 x77 x78 = x27 x79 (x28 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x55 x79 ⟶ x69 x77 (x70 x79) ⟶ x69 x78 (x70 x79) ⟶ (x53 x79 x77 x78 = x66 (x70 x79) (x25 x79) x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ x72 x79 ⟶ x55 x79 ⟶ x69 x77 (x70 x79) ⟶ x69 x78 (x70 x79) ⟶ (x54 x79 x77 x78 = x54 x79 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x33 x77 x1 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x76 x77 ⟶ (x33 x77 x1 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x12 x77 ⟶ False) ⟶ x50 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x50 x77 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x12 x77 ⟶ False) ⟶ x12 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x12 x77 ⟶ False) ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x76 x77 ⟶ (x12 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x76 x77 ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x79 ⟶ x69 x77 (x58 (x5 x78 x79)) ⟶ (x0 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x40 x77 ⟶ (x60 x77 ⟶ False) ⟶ x50 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x79 ⟶ x69 x77 (x58 (x5 x79 x78)) ⟶ (x0 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x50 x77 ⟶ False) ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x79 (x58 (x5 x77 x78)) ⟶ (x46 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x79 (x58 (x5 x78 x77)) ⟶ (x8 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ (x64 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ (x72 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ (x63 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ (x61 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x71 x77 ⟶ x26 x77 ⟶ x60 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x76 x77 ⟶ (x50 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x69 x79 (x58 (x5 x77 x78)) ⟶ (x44 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x61 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x63 x77 ⟶ x72 x77 ⟶ x64 x77 ⟶ x71 x77 ⟶ (x26 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x65 x77 ⟶ (x60 x77 ⟶ False) ⟶ x75 x77 ⟶ x61 x77 ⟶ x74 x77 ⟶ x62 x77 ⟶ x73 x77 ⟶ x63 x77 ⟶ x72 x77 ⟶ x64 x77 ⟶ x71 x77 ⟶ x60 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x50 x77 ⟶ False) ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x33 x77 x56 ⟶ (x50 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ x33 x77 x56 ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 . x51 x77 ⟶ (x76 x77 ⟶ False) ⟶ x50 x77 ⟶ (x33 x77 x56 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x59 x77 x78 ⟶ x59 x78 x77 ⟶ False) ⟶ (x66 (x70 x29) (x68 x29) (x66 (x70 x29) (x67 x29) x32 x30) x31 = x66 (x70 x29) (x67 x29) (x66 (x70 x29) (x68 x29) x32 x31) (x66 (x70 x29) (x68 x29) x30 x31) ⟶ False) ⟶ ((x69 x31 (x70 x29) ⟶ False) ⟶ False) ⟶ ((x69 x30 (x70 x29) ⟶ False) ⟶ False) ⟶ ((x69 x32 (x70 x29) ⟶ False) ⟶ False) ⟶ ((x65 x29 ⟶ False) ⟶ False) ⟶ ((x71 x29 ⟶ False) ⟶ False) ⟶ ((x64 x29 ⟶ False) ⟶ False) ⟶ ((x72 x29 ⟶ False) ⟶ False) ⟶ ((x63 x29 ⟶ False) ⟶ False) ⟶ ((x73 x29 ⟶ False) ⟶ False) ⟶ ((x62 x29 ⟶ False) ⟶ False) ⟶ ((x74 x29 ⟶ False) ⟶ False) ⟶ ((x61 x29 ⟶ False) ⟶ False) ⟶ ((x75 x29 ⟶ False) ⟶ False) ⟶ (x60 x29 ⟶ False) ⟶ (x76 x29 ⟶ False) ⟶ False

type
prop

theory
HotG

name
-

proof
PUNpv..

Megalodon
-

proofgold address
TMSCM..

creator
35137 PrPhD../7ff5b..

owner
35140 PrPhD../9d0c1..

term root
f1214..