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

type
prop

theory
HotG

name
-

proof
PUepM..

Megalodon
-

proofgold address
TMJ4J..

creator
35138 PrPhD../1fe6e..

owner
35140 PrPhD../0ba4b..

term root
31810..