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

type
prop

theory
HotG

name
-

proof
PUgRF..

Megalodon
-

proofgold address
TMaNB..

creator
35135 PrPhD../65637..

owner
35137 PrPhD../c43c3..

term root
1f263..