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

type
prop

theory
HotG

name
-

proof
PUN2c..

Megalodon
-

proofgold address
TMQts..

creator
35136 PrPhD../2eed0..

owner
35140 PrPhD../70fd2..

term root
7590d..