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

type
prop

theory
HotG

name
-

proof
PUPc1..

Megalodon
-

proofgold address
TMPaQ..

creator
35132 PrPhD../e2379..

owner
35137 PrPhD../78050..

term root
47571..