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 . x56 x58(x58 = x57False)x56 x57False)(∀ x57 x58 . x0 x57 x58x56 x58False)(∀ x57 . x56 x57(x57 = x55False)False)(∀ x57 x58 x59 . x0 x57 x58x2 x58 (x1 x59)x56 x59False)(∀ x57 x58 x59 . x0 x58 x59x2 x59 (x1 x57)(x2 x58 x57False)False)(∀ x57 . (x3 x55 x57 = x55False)False)(∀ x57 x58 . x54 x58 x57(x2 x58 (x1 x57)False)False)(∀ x57 x58 . x2 x58 (x1 x57)(x54 x58 x57False)False)(∀ x57 . (x3 x57 x55 = x57False)False)(∀ x57 x58 x59 . x0 x58 x59x0 x57 x59x0 x57 (x4 x59 x58)False)(∀ x57 x58 . x0 x58 x57(x0 (x4 x57 x58) x57False)False)(∀ x57 x58 . x2 x57 x58(x56 x58False)(x0 x57 x58False)False)(∀ x57 x58 . x0 x58 x57(x2 x58 x57False)False)((x2 x55 x5False)False)(∀ x57 . (x53 x57 x55 = x57False)False)(∀ x57 x58 . x6 x58x6 x57x7 x58 x57(x7 x57 x58False)False)((x2 x51 x52False)False)((x2 x51 x8False)False)((x50 x51 x52 x8False)False)((x9 x51False)False)(x56 x51False)(∀ x57 . (x54 x57 x57False)False)(∀ x57 x58 x59 . (x56 x59False)(x56 x57False)x2 x57 (x1 x59)x2 x58 x57(x50 x58 x59 x57False)False)(∀ x57 x58 x59 . (x56 x59False)(x56 x57False)x2 x57 (x1 x59)x50 x58 x59 x57(x2 x58 x57False)False)(∀ x57 x58 . (x49 x57 x58 = x3 x57 x58False)False)((x8 = x5False)False)((x48 x47False)False)(x56 x47False)(∀ x57 . (x56 x57False)(x45 (x46 x57) x57False)False)(∀ x57 . (x56 x57False)(x2 (x46 x57) (x1 x57)False)False)((x48 x44False)False)(∀ x57 . x45 (x10 x57) x57False)(∀ x57 . (x2 (x10 x57) (x1 x57)False)False)(x56 x11False)(∀ x57 . (x56 (x43 x57)False)False)(∀ x57 . (x2 (x43 x57) (x1 x57)False)False)((x6 x42False)False)((x12 x42False)False)((x41 x42False)False)(x56 x42False)((x56 x40False)False)((x2 x40 x13False)False)((x56 x39False)False)(∀ x57 . (x56 x57False)x56 (x14 x57)False)(∀ x57 . (x56 x57False)(x2 (x14 x57) (x1 x57)False)False)((x6 x15False)False)((x6 x38False)False)(x56 x38False)((x2 x38 x13False)False)(∀ x57 . (x53 x57 x57 = x57False)False)(∀ x57 x58 . x2 x58 x5x57 = x37 x58 x51(x0 x57 x36False)False)(∀ x57 . x0 x57 x36(x57 = x37 (x16 x57) x51False)False)(∀ x57 . x0 x57 x36(x2 (x16 x57) x5False)False)(∀ x57 x58 x59 . x2 x59 x5x2 x57 x5x58 = x37 x59 x57x7 x59 x57(x57 = x55False)(x0 x58 x17False)False)(∀ x57 . x0 x57 x17x35 x57 = x55False)(∀ x57 . x0 x57 x17(x7 (x18 x57) (x35 x57)False)False)(∀ x57 . x0 x57 x17(x57 = x37 (x18 x57) (x35 x57)False)False)(∀ x57 . x0 x57 x17(x2 (x35 x57) x5False)False)(∀ x57 . x0 x57 x17(x2 (x18 x57) x5False)False)(∀ x57 x58 x59 . x2 x59 (x1 x13)x57 = x59x0 (x19 x59 x57) x59x2 x58 x13x0 x58 x59(x21 x58 (x20 x59 x57)False)(x0 x57 x22False)False)(∀ x57 x58 x59 . x2 x59 (x1 x13)x57 = x59(x21 (x19 x59 x57) (x20 x59 x57)False)x2 x58 x13x0 x58 x59(x21 x58 (x20 x59 x57)False)(x0 x57 x22False)False)(∀ x57 x58 x59 . x2 x59 (x1 x13)x57 = x59(x2 (x19 x59 x57) x13False)x2 x58 x13x0 x58 x59(x21 x58 (x20 x59 x57)False)(x0 x57 x22False)False)(∀ x57 x58 . x2 x58 (x1 x13)x57 = x58(x0 (x20 x58 x57) x58False)(x0 x57 x22False)False)(∀ x57 x58 . x2 x58 (x1 x13)x57 = x58(x2 (x20 x58 x57) x13False)(x0 x57 x22False)False)(∀ x57 x58 . x0 x58 x22x2 x57 x13x0 x57 (x33 x58)x21 (x34 x57 x58) x57False)(∀ x57 x58 . x0 x58 x22x2 x57 x13x0 x57 (x33 x58)(x0 (x34 x57 x58) (x33 x58)False)False)(∀ x57 x58 . x0 x58 x22x2 x57 x13x0 x57 (x33 x58)(x2 (x34 x57 x58) x13False)False)(∀ x57 x58 x59 . x0 x59 x22x2 x57 x13x0 x57 (x33 x59)x2 x58 x13x21 x58 x57(x0 x58 (x33 x59)False)False)(∀ x57 . x0 x57 x22(x57 = x33 x57False)False)(∀ x57 . x0 x57 x22(x2 (x33 x57) (x1 x13)False)False)((x6 x5False)False)(x56 x5False)(∀ x57 x58 . (x56 x58False)x56 (x53 x57 x58)False)(∀ x57 x58 . (x56 x58False)x56 (x53 x58 x57)False)(∀ x57 x58 . x56 (x32 x57 x58)False)(x56 x13False)(∀ x57 . x56 (x31 x57)False)((x56 x55False)False)(∀ x57 . x56 (x1 x57)False)(∀ x57 x58 . x6 x58x6 x57(x6 (x53 x58 x57)False)False)(∀ x57 x58 . (x56 x58False)(x56 x57False)x2 x57 (x1 x58)(x50 (x30 x57 x58) x58 x57False)False)(∀ x57 . (x2 (x23 x57) x57False)False)((x56 x29False)False)(∀ x57 x58 x59 . (x56 x59False)(x56 x57False)x2 x57 (x1 x59)x50 x58 x59 x57(x2 x58 x59False)False)(∀ x57 x58 . (x2 (x49 x57 x58) (x1 x57)False)False)((x2 x8 (x1 x52)False)False)((x13 = x53 (x49 x17 x36) x5False)False)(∀ x57 x58 . (x37 x58 x57 = x32 (x32 x58 x57) (x31 x58)False)False)(∀ x57 x58 . x0 (x28 x57 x58) x57(x54 x58 x57False)False)(∀ x57 x58 . (x0 (x28 x57 x58) x58False)(x54 x58 x57False)False)(∀ x57 x58 x59 . x54 x58 x59x0 x57 x58(x0 x57 x59False)False)((x55 = x29False)False)(∀ x57 x58 . x2 x58 x13x2 x57 x13(x21 x58 x57False)(x21 x57 x58False)False)(∀ x57 x58 . (x53 x58 x57 = x53 x57 x58False)False)(∀ x57 x58 . (x32 x58 x57 = x32 x57 x58False)False)(∀ x57 . x56 x57(x24 x57False)False)(∀ x57 . x2 x57 x5(x48 x57False)False)(∀ x57 . x56 x57(x48 x57False)False)(∀ x57 . x48 x57(x6 x57False)False)(∀ x57 x58 . x6 x58x2 x57 x58(x6 x57False)False)(∀ x57 x58 . x56 x58x2 x57 (x1 x58)x45 x57 x58False)(∀ x57 . x56 x57(x25 x57False)False)(∀ x57 x58 . (x56 x58False)x2 x57 (x1 x58)x56 x57(x45 x57 x58False)False)(∀ x57 . x56 x57(x6 x57False)False)(∀ x57 x58 . (x56 x58False)x2 x57 (x1 x58)(x45 x57 x58False)x56 x57False)(∀ x57 x58 . x6 x58x2 x57 x58(x6 x57False)False)(∀ x57 . x41 x57x12 x57(x6 x57False)False)(∀ x57 x58 . x56 x58x2 x57 (x1 x58)(x56 x57False)False)(∀ x57 . x6 x57(x12 x57False)False)(∀ x57 . x6 x57(x41 x57False)False)(∀ x57 . x2 x57 x13x6 x57(x48 x57False)False)(∀ x57 . x2 x57 x13x6 x57(x6 x57False)False)(∀ x57 x58 . x24 x58x2 x57 (x1 x58)(x24 x57False)False)(∀ x57 x58 . x0 x57 x58x0 x58 x57False)(x54 x26 x27False)(x54 x27 x26False)((x0 x26 x22False)False)((x0 x27 x22False)False)False
type
prop
theory
HotG
name
-
proof
PUTiP..
Megalodon
-
proofgold address
TMbqv..
creator
35144 PrPhD../ee486..
owner
35145 PrPhD../a5bdd..
term root
d4ee5..