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 . x37 x39(x39 = x38False)x37 x38False)(∀ x38 x39 . x0 x38 x39x37 x39False)(∀ x38 . x37 x38(x38 = x36False)False)(∀ x38 x39 x40 . x0 x38 x39x2 x39 (x1 x40)x37 x40False)(∀ x38 x39 x40 . x0 x39 x40x2 x40 (x1 x38)(x2 x39 x38False)False)(∀ x38 x39 . x3 x39 x38(x2 x39 (x1 x38)False)False)(∀ x38 x39 . x2 x39 (x1 x38)(x3 x39 x38False)False)(∀ x38 x39 . x2 x38 x39(x37 x39False)(x0 x38 x39False)False)(∀ x38 x39 . x0 x39 x38(x2 x39 x38False)False)(∀ x38 x39 x40 . x4 x40x8 x40x0 x39 (x5 x40)x38 = x7 x40 x39(x0 (x6 x39 x38) x40False)False)(∀ x38 x39 x40 . x4 x40x8 x40x0 (x6 x39 x38) x40(x38 = x7 x40 x39False)False)(∀ x38 x39 x40 . x4 x40x8 x40x0 (x6 x39 x38) x40(x0 x39 (x5 x40)False)False)(∀ x38 x39 . x4 x39x4 x38x3 x39 x38(x3 (x35 x39) (x35 x38)False)False)(∀ x38 x39 . x4 x39x4 x38x3 x39 x38(x3 (x5 x39) (x5 x38)False)False)(∀ x38 . (x3 x38 x38False)False)((x9 x10False)False)(x37 x10False)(x11 x12False)((x8 x12False)False)((x4 x12False)False)((x8 x34False)False)((x13 x34False)False)((x4 x34False)False)(x37 x34False)((x8 x33False)False)((x13 x33False)False)((x4 x33False)False)((x13 x14False)False)((x4 x14False)False)((x15 x16False)False)((x8 x16False)False)((x4 x16False)False)((x32 x31False)False)((x4 x17False)False)(x37 x17False)((x8 x18False)False)((x4 x18False)False)(∀ x38 . (x37 x38False)x4 x38x37 (x35 x38)False)(∀ x38 . (x37 x38False)x4 x38x37 (x5 x38)False)(∀ x38 x39 x40 x41 . (x4 (x19 (x6 x39 x38) (x6 x41 x40))False)False)(∀ x38 . x37 x38(x37 (x35 x38)False)False)(∀ x38 x39 . (x4 (x20 (x6 x39 x38))False)False)(∀ x38 . x37 x38(x37 (x5 x38)False)False)(∀ x38 . x21 x38x4 x38(x21 (x35 x38)False)False)(∀ x38 . x21 x38x4 x38(x21 (x5 x38)False)False)(∀ x38 x39 . (x32 (x6 x38 x39)False)False)(∀ x38 x39 . (x8 (x20 (x6 x39 x38))False)False)(∀ x38 x39 . x4 x39x22 x39x8 x39(x37 (x7 x39 x38)False)False)(∀ x38 . (x21 x38False)x4 x38x8 x38x21 (x5 x38)False)(∀ x38 x39 . x4 x39x8 x39x4 x38x8 x38(x9 (x19 x39 x38)False)False)(∀ x38 . x4 x38x8 x38(x9 (x20 x38)False)False)(∀ x38 . x4 x38x8 x38(x11 x38False)x21 (x35 x38)False)(∀ x38 . x4 x38x8 x38x11 x38(x21 (x35 x38)False)False)(∀ x38 . x37 x38(x37 (x35 x38)False)False)(∀ x38 x39 . (x37 x39False)x4 x39x13 x39x8 x39x2 x38 (x5 x39)x37 (x7 x39 x38)False)(∀ x38 . x37 x38(x37 (x5 x38)False)False)(∀ x38 . x4 x38x13 x38x8 x38(x30 (x35 x38)False)False)(∀ x38 . (x2 (x23 x38) x38False)False)((x37 x29False)False)(∀ x38 x39 . (x6 x39 x38 = x19 (x19 x39 x38) (x20 x39)False)False)(∀ x38 x39 . x4 x39x0 (x6 (x28 x38 x39) (x27 x38 x39)) x38(x3 x39 x38False)False)(∀ x38 x39 . x4 x39(x0 (x6 (x28 x38 x39) (x27 x38 x39)) x39False)(x3 x39 x38False)False)(∀ x38 x39 x40 x41 . x4 x41x3 x41 x38x0 (x6 x39 x40) x41(x0 (x6 x39 x40) x38False)False)((x36 = x29False)False)(∀ x38 x39 x40 . x4 x40x8 x40(x0 x39 (x5 x40)False)x38 = x36(x38 = x7 x40 x39False)False)(∀ x38 x39 x40 . x4 x40x8 x40(x0 x39 (x5 x40)False)x38 = x7 x40 x39(x38 = x36False)False)(∀ x38 x39 x40 . x4 x40x8 x40x0 x39 (x5 x40)x0 (x6 x39 x38) x40(x38 = x7 x40 x39False)False)(∀ x38 x39 x40 . x4 x40x8 x40x0 x39 (x5 x40)x38 = x7 x40 x39(x0 (x6 x39 x38) x40False)False)(∀ x38 x39 . (x19 x39 x38 = x19 x38 x39False)False)(∀ x38 x39 . x9 x39x2 x38 (x1 x39)(x9 x38False)False)(∀ x38 x39 . x9 x39x2 x38 x39(x8 x38False)False)(∀ x38 x39 . x9 x39x2 x38 x39(x4 x38False)False)(∀ x38 . x37 x38(x9 x38False)False)(∀ x38 . x21 x38x4 x38x8 x38(x11 x38False)False)(∀ x38 . x21 x38x4 x38x8 x38(x8 x38False)False)(∀ x38 . x21 x38x4 x38x8 x38(x4 x38False)False)(∀ x38 . x4 x38x8 x38(x11 x38False)(x8 x38False)False)(∀ x38 . x4 x38x8 x38(x11 x38False)(x4 x38False)False)(∀ x38 . x4 x38x8 x38(x11 x38False)x21 x38False)(∀ x38 . x37 x38x4 x38(x13 x38False)False)(∀ x38 . x37 x38x4 x38(x4 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x11 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x8 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x4 x38False)False)(∀ x38 . x37 x38x4 x38(x22 x38False)False)(∀ x38 . x37 x38x4 x38(x4 x38False)False)(∀ x38 x39 . x4 x39x8 x39x2 x38 (x1 x39)(x8 x38False)False)(∀ x38 x39 . x4 x39x2 x38 (x1 x39)(x4 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x15 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x8 x38False)False)(∀ x38 . x37 x38x4 x38x8 x38(x4 x38False)False)(∀ x38 . x37 x38(x4 x38False)False)(∀ x38 . x37 x38(x8 x38False)False)(∀ x38 x39 . x0 x38 x39x0 x39 x38False)(∀ x38 . x0 x38 (x5 x26)(x7 x26 x38 = x7 x25 x38False)(x3 x26 x25False)False)((x3 (x5 x26) (x5 x25)False)(x3 x26 x25False)False)(x3 x26 x25x3 (x5 x26) (x5 x25)x7 x26 x24 = x7 x25 x24False)(x3 x26 x25x3 (x5 x26) (x5 x25)(x0 x24 (x5 x26)False)False)((x8 x25False)False)((x4 x25False)False)((x8 x26False)False)((x4 x26False)False)False
type
prop
theory
HotG
name
-
proof
PUeSw..
Megalodon
-
proofgold address
TMRTE..
creator
35128 PrPhD../9e06f..
owner
35131 PrPhD../2a89b..
term root
da987..