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

type
prop

theory
HotG

name
-

proof
PUX5F..

Megalodon
-

proofgold address
TMaj3..

creator
35131 PrPhD../83e54..

owner
35137 PrPhD../3eeb6..

term root
342d4..