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

type
prop

theory
HotG

name
-

proof
PURwk..

Megalodon
-

proofgold address
TMKCy..

creator
35150 PrPhD../40c96..

owner
35153 PrPhD../eadd5..

term root
07380..