Search for blocks/addresses/...

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 . x59 x61x59 x60(x58 x61 x60False)(x57 x60False)(x56 x61False)False)(∀ x60 x61 . x0 x61(x61 = x60False)x0 x60False)(∀ x60 x61 . x59 x61x59 x60(x58 x61 x60False)(x56 x61False)(x57 x60False)False)(∀ x60 x61 . x1 x60 x61x0 x61False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60(x0 x61False)(x56 x60False)(x57 x61False)False)(∀ x60 . x0 x60(x60 = x2False)False)(∀ x60 x61 x62 . x1 x60 x61x54 x61 (x55 x62)x0 x62False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60(x0 x60False)(x57 x61False)(x56 x60False)False)(∀ x60 x61 x62 . x1 x61 x62x54 x62 (x55 x60)(x54 x61 x60False)False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60(x56 x60False)x56 x61False)(∀ x60 . x53 x60(x52 x60 x51 = x60False)False)(∀ x60 x61 . x3 x61 x60(x54 x61 (x55 x60)False)False)(∀ x60 x61 . x54 x61 (x55 x60)(x3 x61 x60False)False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60(x57 x61False)x57 x60False)(∀ x60 . x53 x60(x50 x49 x60 = x60False)False)(∀ x60 x61 . x54 x60 x61(x0 x61False)(x1 x60 x61False)False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60x57 x60(x57 x61False)False)(∀ x60 . x53 x60(x50 x60 x51 = x51False)False)(∀ x60 x61 . x59 x61x59 x60x58 (x48 x60) (x48 x61)(x58 x61 x60False)False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60(x58 (x48 x60) (x48 x61)False)False)(∀ x60 x61 . x1 x61 x60(x54 x61 x60False)False)(∀ x60 x61 . x59 x61x59 x60x58 x61 x60x56 x61(x56 x60False)False)((x54 x2 x47False)False)(∀ x60 . x53 x60(x4 x60 x51 = x60False)False)(∀ x60 x61 . x53 x61x53 x60(x52 (x48 x61) (x48 x60) = x52 x60 x61False)False)(∀ x60 x61 . x53 x61x53 x60(x4 (x48 x61) (x48 x60) = x48 (x4 x61 x60)False)False)(∀ x60 x61 x62 . x53 x62x53 x60x53 x61(x50 (x50 x62 x60) x61 = x50 x62 (x50 x60 x61)False)False)(∀ x60 x61 x62 . x53 x62x53 x60x53 x61(x4 (x4 x62 x60) x61 = x4 x62 (x4 x60 x61)False)False)(∀ x60 x61 x62 . x53 x62x53 x60x53 x61(x50 (x4 x62 x60) x61 = x4 (x50 x62 x61) (x50 x60 x61)False)False)((x54 x6 x5False)False)((x54 x6 x46False)False)((x7 x6 x5 x46False)False)((x56 x6False)False)(x0 x6False)(∀ x60 . x53 x60(x50 x60 (x48 x49) = x48 x60False)False)((x54 x49 x5False)False)((x54 x49 x46False)False)((x7 x49 x5 x46False)False)((x56 x49False)False)(x0 x49False)(∀ x60 x61 . x53 x61x53 x60(x4 x61 (x48 x60) = x52 x61 x60False)False)((x54 x8 x5False)False)((x54 x8 x46False)False)((x7 x8 x5 x46False)False)((x0 x8False)False)((x48 (x48 x6) = x6False)False)((x48 (x48 x49) = x49False)False)((x48 x6 = x48 x6False)False)((x48 x49 = x48 x49False)False)((x48 x8 = x8False)False)((x50 (x48 x6) x49 = x48 x6False)False)((x50 (x48 x6) x8 = x8False)False)((x50 x6 x49 = x6False)False)((x50 x6 x8 = x8False)False)((x50 x49 (x48 x6) = x48 x6False)False)((x50 x49 x6 = x6False)False)((x50 x49 x49 = x49False)False)((x50 x49 x8 = x8False)False)((x50 x8 (x48 x6) = x8False)False)((x50 x8 x6 = x8False)False)((x50 x8 x49 = x8False)False)((x50 x8 x8 = x8False)False)((x52 (x48 x6) (x48 x6) = x8False)False)((x52 (x48 x6) (x48 x49) = x48 x49False)False)((x52 (x48 x6) x8 = x48 x6False)False)((x52 (x48 x49) (x48 x6) = x49False)False)((x52 (x48 x49) (x48 x49) = x8False)False)((x52 (x48 x49) x49 = x48 x6False)False)((x52 (x48 x49) x8 = x48 x49False)False)((x52 x6 x6 = x8False)False)((x52 x6 x49 = x49False)False)((x52 x6 x8 = x6False)False)((x52 x49 (x48 x49) = x6False)False)((x52 x49 x6 = x48 x49False)False)((x52 x49 x49 = x8False)False)((x52 x49 x8 = x49False)False)((x52 x8 (x48 x6) = x6False)False)((x52 x8 (x48 x49) = x49False)False)((x52 x8 x6 = x48 x6False)False)((x52 x8 x49 = x48 x49False)False)((x52 x8 x8 = x8False)False)((x4 (x48 x6) x6 = x8False)False)((x4 (x48 x6) x49 = x48 x49False)False)((x4 (x48 x49) (x48 x49) = x48 x6False)False)((x4 (x48 x49) x6 = x49False)False)((x4 (x48 x49) x49 = x8False)False)((x4 (x48 x49) x8 = x48 x49False)False)((x4 x6 (x48 x6) = x8False)False)((x4 x6 (x48 x49) = x49False)False)((x4 x6 x8 = x6False)False)((x4 x49 (x48 x6) = x48 x49False)False)((x4 x49 (x48 x49) = x8False)False)((x4 x49 x49 = x6False)False)((x4 x49 x8 = x49False)False)((x4 x8 (x48 x6) = x48 x6False)False)((x4 x8 (x48 x49) = x48 x49False)False)((x4 x8 x6 = x6False)False)((x4 x8 x49 = x49False)False)((x4 x8 x8 = x8False)False)((x58 (x48 x6) (x48 x6)False)False)((x58 (x48 x6) (x48 x49)False)False)((x58 (x48 x6) x6False)False)((x58 (x48 x6) x49False)False)((x58 (x48 x6) x8False)False)(x58 (x48 x49) (x48 x6)False)((x58 (x48 x49) (x48 x49)False)False)((x58 (x48 x49) x6False)False)((x58 (x48 x49) x49False)False)((x58 (x48 x49) x8False)False)(x58 x6 (x48 x6)False)(x58 x6 (x48 x49)False)((x58 x6 x6False)False)(x58 x6 x49False)(x58 x6 x8False)(x58 x49 (x48 x6)False)(x58 x49 (x48 x49)False)((x58 x49 x6False)False)((x58 x49 x49False)False)(x58 x49 x8False)(x58 x8 (x48 x6)False)(x58 x8 (x48 x49)False)((x58 x8 x6False)False)((x58 x8 x49False)False)((x58 x8 x8False)False)(∀ x60 x61 . x45 x61x45 x60(x58 x61 x61False)False)(∀ x60 . (x3 x60 x60False)False)(∀ x60 x61 x62 . (x0 x62False)(x0 x60False)x54 x60 (x55 x62)x54 x61 x60(x7 x61 x62 x60False)False)(∀ x60 x61 x62 . (x0 x62False)(x0 x60False)x54 x60 (x55 x62)x7 x61 x62 x60(x54 x61 x60False)False)((x51 = x2False)False)((x46 = x47False)False)((x44 x43False)False)(x0 x43False)((x45 x42False)False)((x0 x42False)False)((x59 x41False)False)((x45 x41False)False)((x53 x41False)False)((x0 x41False)False)((x44 x40False)False)((x57 x9False)False)((x45 x9False)False)((x59 x10False)False)((x57 x10False)False)((x45 x10False)False)((x53 x10False)False)(x59 x11False)((x57 x11False)False)((x45 x11False)False)((x56 x39False)False)((x45 x39False)False)((x59 x38False)False)((x56 x38False)False)((x45 x38False)False)((x53 x38False)False)((x53 x37False)False)(x0 x37False)(x0 x36False)((x12 x13False)False)((x35 x13False)False)((x14 x13False)False)(x0 x13False)(x59 x15False)((x56 x15False)False)((x45 x15False)False)((x45 x34False)False)((x59 x16False)False)((x53 x33False)False)((x0 x17False)False)((x59 x32False)False)((x56 x32False)False)((x45 x32False)False)((x53 x32False)False)((x54 x32 x5False)False)((x12 x18False)False)(∀ x60 . x45 x60x1 x60 x5(x1 (x31 x60) x5False)False)(∀ x60 . x45 x60x1 (x31 x60) x5(x1 x60 x5False)False)(∀ x60 . x53 x60(x48 (x48 x60) = x60False)False)(∀ x60 . x45 x60(x31 (x31 x60) = x60False)False)(∀ x60 x61 . x59 x61x53 x60x61 = x60(x31 x61 = x48 x60False)False)(∀ x60 x61 . (x57 x61False)x59 x61(x57 x60False)x59 x60x57 (x4 x61 x60)False)(∀ x60 x61 . (x0 x61False)x53 x61(x0 x60False)x53 x60x0 (x50 x61 x60)False)(∀ x60 x61 . x59 x61x59 x60(x59 (x52 x61 x60)False)False)(∀ x60 x61 . x59 x61x59 x60(x59 (x50 x61 x60)False)False)(∀ x60 . (x0 x60False)x53 x60(x53 (x48 x60)False)False)(∀ x60 . (x0 x60False)x53 x60x0 (x48 x60)False)((x12 x47False)False)(x0 x47False)(∀ x60 x61 . x59 x61x59 x60(x59 (x4 x61 x60)False)False)((x57 x30False)False)(∀ x60 x61 . x53 x61x53 x60(x53 (x52 x61 x60)False)False)((x56 x29False)False)(∀ x60 . x59 x60(x59 (x48 x60)False)False)(∀ x60 . x59 x60(x53 (x48 x60)False)False)(∀ x60 x61 . x53 x61x53 x60(x53 (x50 x61 x60)False)False)((x45 x30False)False)(x59 x29False)(∀ x60 x61 . x53 x61x53 x60(x53 (x4 x61 x60)False)False)(∀ x60 x61 . (x57 x61False)x59 x61(x57 x60False)x59 x60x57 (x50 x61 x60)False)(∀ x60 x61 . (x56 x61False)x59 x61(x56 x60False)x59 x60x57 (x50 x61 x60)False)(∀ x60 x61 . (x56 x61False)x59 x61(x57 x60False)x59 x60x56 (x50 x60 x61)False)(∀ x60 x61 . (x56 x61False)x59 x61(x57 x60False)x59 x60x56 (x50 x61 x60)False)(∀ x60 x61 . x57 x61x59 x61(x57 x60False)x59 x60(x56 (x52 x60 x61)False)False)(∀ x60 x61 . x57 x61x59 x61(x57 x60False)x59 x60(x57 (x52 x61 x60)False)False)(∀ x60 x61 . x56 x61x59 x61(x56 x60False)x59 x60(x57 (x52 x60 x61)False)False)(∀ x60 . x59 x60(x59 (x31 x60)False)False)(∀ x60 . x59 x60(x45 (x31 x60)False)False)((x45 x29False)False)(x59 x30False)((x0 x2False)False)(∀ x60 x61 . x56 x61x59 x61(x56 x60False)x59 x60(x56 (x52 x61 x60)False)False)(∀ x60 x61 . (x57 x61False)x59 x61(x56 x60False)x59 x60x56 (x52 x60 x61)False)(∀ x60 . x45 x60x57 x60(x56 (x31 x60)False)False)(∀ x60 . x45 x60x57 x60(x45 (x31 x60)False)False)(∀ x60 x61 . (x57 x61False)x59 x61(x56 x60False)x59 x60x57 (x52 x61 x60)False)(∀ x60 . x45 x60x56 x60(x57 (x31 x60)False)False)(∀ x60 . x45 x60x56 x60(x45 (x31 x60)False)False)(∀ x60 . (x57 x60False)x59 x60x56 (x48 x60)False)(∀ x60 . (x57 x60False)x59 x60(x53 (x48 x60)False)False)(∀ x60 . x45 x60(x57 x60False)x56 (x31 x60)False)(∀ x60 . x45 x60(x57 x60False)(x45 (x31 x60)False)False)(∀ x60 . (x56 x60False)x59 x60x57 (x48 x60)False)(∀ x60 . (x56 x60False)x59 x60(x53 (x48 x60)False)False)(∀ x60 . x45 x60(x56 x60False)x57 (x31 x60)False)(∀ x60 . x45 x60(x56 x60False)(x45 (x31 x60)False)False)(∀ x60 x61 . x57 x61x59 x61(x56 x60False)x59 x60(x57 (x4 x60 x61)False)False)(∀ x60 x61 . x57 x61x59 x61(x56 x60False)x59 x60(x57 (x4 x61 x60)False)False)(∀ x60 x61 . x56 x61x59 x61(x57 x60False)x59 x60(x56 (x4 x60 x61)False)False)(∀ x60 x61 . x56 x61x59 x61(x57 x60False)x59 x60(x56 (x4 x61 x60)False)False)(∀ x60 x61 . (x56 x61False)x59 x61(x56 x60False)x59 x60x56 (x4 x61 x60)False)(∀ x60 x61 . (x0 x61False)(x0 x60False)x54 x60 (x55 x61)(x7 (x19 x60 x61) x61 x60False)False)(∀ x60 . (x54 (x28 x60) x60False)False)(∀ x60 x61 x62 . (x0 x62False)(x0 x60False)x54 x60 (x55 x62)x7 x61 x62 x60(x54 x61 x62False)False)((x7 x51 x5 x46False)False)((x54 x46 (x55 x5)False)False)(∀ x60 . x53 x60(x53 (x48 x60)False)False)(∀ x60 . x45 x60(x45 (x31 x60)False)False)(∀ x60 x61 . x53 x61x53 x60(x52 x61 x60 = x4 x61 (x48 x60)False)False)(∀ x60 x61 . x45 x61x45 x60(x59 x61False)(x61 = x29False)x60 = x29(x60 = x31 x61False)False)(∀ x60 x61 . x45 x61x45 x60(x59 x61False)(x61 = x29False)x60 = x31 x61(x60 = x29False)False)(∀ x60 x61 . x45 x61x45 x60x61 = x29x60 = x30(x60 = x31 x61False)False)(∀ x60 x61 . x45 x61x45 x60x61 = x29x60 = x31 x61(x60 = x30False)False)(∀ x60 x61 x62 . x45 x62x45 x60x59 x62x53 x61x62 = x61x60 = x48 x61(x60 = x31 x62False)False)(∀ x60 x61 . x45 x61x45 x60x59 x61x60 = x31 x61(x60 = x48 (x27 x60 x61)False)False)(∀ x60 x61 . x45 x61x45 x60x59 x61x60 = x31 x61(x61 = x27 x60 x61False)False)(∀ x60 x61 . x45 x61x45 x60x59 x61x60 = x31 x61(x53 (x27 x60 x61)False)False)((x30 = x20 x51 x5False)False)((x29 = x5False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x60 x5False)x60 = x29(x58 x61 x60False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x60 x5False)x61 = x30(x58 x61 x60False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x60 x5False)x58 x61 x60(x61 = x30False)(x60 = x29False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x61 x5False)x60 = x29(x58 x61 x60False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x61 x5False)x61 = x30(x58 x61 x60False)False)(∀ x60 x61 . x45 x61x45 x60(x1 x61 x5False)x58 x61 x60(x61 = x30False)(x60 = x29False)False)(∀ x60 x61 x62 x63 . x45 x63x45 x60x1 x63 x5x1 x60 x5x54 x62 x5x54 x61 x5x62 = x63x61 = x60x58 x62 x61(x58 x63 x60False)False)(∀ x60 x61 . x45 x61x45 x60x1 x61 x5x1 x60 x5x58 x61 x60(x58 (x26 x60 x61) (x25 x60 x61)False)False)(∀ x60 x61 . x45 x61x45 x60x1 x61 x5x1 x60 x5x58 x61 x60(x25 x60 x61 = x60False)False)(∀ x60 x61 . x45 x61x45 x60x1 x61 x5x1 x60 x5x58 x61 x60(x26 x60 x61 = x61False)False)(∀ x60 x61 . x45 x61x45 x60x1 x61 x5x1 x60 x5x58 x61 x60(x54 (x25 x60 x61) x5False)False)(∀ x60 x61 . x45 x61x45 x60x1 x61 x5x1 x60 x5x58 x61 x60(x54 (x26 x60 x61) x5False)False)(∀ x60 . x1 x60 x5(x59 x60False)False)(∀ x60 . x59 x60(x1 x60 x5False)False)(∀ x60 x61 . x45 x61x45 x60(x58 x61 x60False)(x58 x60 x61False)False)(∀ x60 x61 . x53 x61x53 x60(x50 x61 x60 = x50 x60 x61False)False)(∀ x60 x61 . x53 x61x53 x60(x4 x61 x60 = x4 x60 x61False)False)(∀ x60 . x0 x60(x24 x60False)False)(∀ x60 . x45 x60(x56 x60False)(x57 x60False)(x45 x60False)False)(∀ x60 . x45 x60(x56 x60False)(x57 x60False)(x0 x60False)False)(∀ x60 . x54 x60 x47(x44 x60False)False)(∀ x60 . x0 x60x45 x60x57 x60False)(∀ x60 . x0 x60x45 x60x56 x60False)(∀ x60 . x0 x60x45 x60(x45 x60False)False)(∀ x60 . x0 x60(x44 x60False)False)(∀ x60 . (x0 x60False)x45 x60(x56 x60False)(x57 x60False)False)(∀ x60 . (x0 x60False)x45 x60(x56 x60False)(x45 x60False)False)(∀ x60 . x44 x60(x12 x60False)False)(∀ x60 . x45 x60x57 x60x56 x60False)(∀ x60 . x45 x60x57 x60(x45 x60False)False)(∀ x60 . x45 x60x57 x60x0 x60False)(∀ x60 x61 . x12 x61x54 x60 x61(x12 x60False)False)(∀ x60 . (x0 x60False)x45 x60(x57 x60False)(x56 x60False)False)(∀ x60 . (x0 x60False)x45 x60(x57 x60False)(x45 x60False)False)(∀ x60 . x59 x60(x45 x60False)False)(∀ x60 . x0 x60(x23 x60False)False)(∀ x60 . x45 x60x56 x60x57 x60False)(∀ x60 . x45 x60x56 x60(x45 x60False)False)(∀ x60 . x45 x60x56 x60x0 x60False)(∀ x60 . x59 x60(x53 x60False)False)(∀ x60 . x0 x60(x12 x60False)False)(∀ x60 . x45 x60(x56 x60False)(x59 x60False)(x57 x60False)False)(∀ x60 . x45 x60(x56 x60False)(x59 x60False)(x45 x60False)False)(∀ x60 . x44 x60(x45 x60False)False)(∀ x60 . x44 x60(x59 x60False)False)(∀ x60 . x44 x60(x53 x60False)False)(∀ x60 . x14 x60x35 x60(x12 x60False)False)(∀ x60 . x45 x60(x57 x60False)(x59 x60False)(x56 x60False)False)(∀ x60 . x45 x60(x57 x60False)(x59 x60False)(x45 x60False)False)(∀ x60 . x54 x60 x5(x59 x60False)False)(∀ x60 . x54 x60 x5(x53 x60False)False)(∀ x60 . x54 x60 x5(x59 x60False)False)(∀ x60 . x12 x60(x35 x60False)False)(∀ x60 . x12 x60(x14 x60False)False)(∀ x60 x61 . x24 x61x54 x60 (x55 x61)(x24 x60False)False)(∀ x60 x61 . x1 x60 x61x1 x61 x60False)(x58 (x31 x22) (x31 x21)False)((x58 x21 x22False)False)((x45 x22False)False)((x45 x21False)False)False
type
prop
theory
HotG
name
-
proof
PUKXr..
Megalodon
-
proofgold address
TMa2Y..
creator
35119 PrPhD../b502a..
owner
35120 PrPhD../40e80..
term root
689f8..