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 . x46 x48(x48 = x47False)x46 x47False)(∀ x47 x48 . x0 x47 x48x46 x48False)(∀ x47 . x46 x47(x47 = x45False)False)(∀ x47 x48 . x1 x47 x48(x46 x48False)(x0 x47 x48False)False)(∀ x47 x48 x49 x50 . x44 x48 x50 = x44 x47 x49(x50 = x49False)False)(∀ x47 x48 x49 x50 . x44 x50 x48 = x44 x49 x47(x50 = x49False)False)(∀ x47 x48 . x0 x48 x47(x1 x48 x47False)False)((x2 x3False)False)(x46 x3False)(x4 x5False)((x43 x5False)False)((x6 x5False)False)((x43 x42False)False)((x7 x42False)False)((x6 x42False)False)(x46 x42False)((x43 x41False)False)((x7 x41False)False)((x6 x41False)False)(x8 x9False)(x46 x40False)((x7 x10False)False)((x6 x10False)False)((x11 x12False)False)((x43 x12False)False)((x6 x12False)False)(x46 x39False)((x4 x39False)False)((x43 x39False)False)((x6 x39False)False)((x8 x38False)False)(x46 x38False)((x46 x37False)False)((x6 x13False)False)(x46 x13False)((x43 x14False)False)((x6 x14False)False)((x15 x16False)False)((x43 x16False)False)((x6 x16False)False)(∀ x47 . (x46 x47False)x6 x47x46 (x36 x47)False)(∀ x47 x48 . x6 x48x43 x48x15 x48(x43 (x17 x48 x47)False)False)(∀ x47 x48 . x6 x48x43 x48x15 x48(x6 (x17 x48 x47)False)False)(∀ x47 x48 x49 x50 . (x6 (x18 (x44 x48 x47) (x44 x50 x49))False)False)(∀ x47 x48 . (x6 (x35 (x44 x48 x47))False)False)(∀ x47 x48 . x46 (x18 x47 x48)False)(∀ x47 . (x8 (x35 x47)False)False)(∀ x47 . x46 (x35 x47)False)(∀ x47 . x8 x47x6 x47(x8 (x36 x47)False)False)(∀ x47 x48 . x46 (x44 x47 x48)False)((x46 x45False)False)(∀ x47 x48 . (x43 (x35 (x44 x48 x47))False)False)(∀ x47 x48 . x6 x48x34 x48x43 x48(x46 (x17 x48 x47)False)False)(∀ x47 . (x8 x47False)x6 x47x43 x47x8 (x36 x47)False)(∀ x47 x48 . x6 x48x43 x48x6 x47x43 x47(x2 (x18 x48 x47)False)False)(∀ x47 . x6 x47x43 x47(x2 (x35 x47)False)False)(∀ x47 x48 . (x46 x48False)x6 x48x7 x48x43 x48x1 x47 (x36 x48)x46 (x17 x48 x47)False)(∀ x47 . x46 x47(x46 (x36 x47)False)False)(∀ x47 . (x1 (x33 x47) x47False)False)((x46 x19False)False)(∀ x47 . x6 x47x43 x47(x43 (x32 x47)False)False)(∀ x47 . x6 x47x43 x47(x6 (x32 x47)False)False)(∀ x47 x48 . (x44 x48 x47 = x18 (x18 x48 x47) (x35 x48)False)False)((x45 = x19False)False)(∀ x47 x48 . x6 x48x43 x48x6 x47x43 x47(x0 (x44 (x31 x47 x48) (x30 x47 x48)) (x36 x48)False)(x0 (x26 x47 x48) (x36 x47)False)x29 x47 (x28 x47 x48) (x27 x47 x48) = x29 x48 (x27 x47 x48) (x28 x47 x48)(x47 = x32 x48False)False)(∀ x47 x48 . x6 x48x43 x48x6 x47x43 x47(x0 (x44 (x31 x47 x48) (x30 x47 x48)) (x36 x48)False)(x0 (x26 x47 x48) (x36 x47)False)(x0 (x44 (x27 x47 x48) (x28 x47 x48)) (x36 x48)False)(x47 = x32 x48False)False)(∀ x47 x48 . x6 x48x43 x48x6 x47x43 x47(x26 x47 x48 = x44 (x30 x47 x48) (x31 x47 x48)False)(x0 (x26 x47 x48) (x36 x47)False)x29 x47 (x28 x47 x48) (x27 x47 x48) = x29 x48 (x27 x47 x48) (x28 x47 x48)(x47 = x32 x48False)False)(∀ x47 x48 . x6 x48x43 x48x6 x47x43 x47(x26 x47 x48 = x44 (x30 x47 x48) (x31 x47 x48)False)(x0 (x26 x47 x48) (x36 x47)False)(x0 (x44 (x27 x47 x48) (x28 x47 x48)) (x36 x48)False)(x47 = x32 x48False)False)(∀ x47 x48 x49 x50 . x6 x50x43 x50x6 x49x43 x49x0 (x26 x49 x50) (x36 x49)x26 x49 x50 = x44 x47 x48x0 (x44 x48 x47) (x36 x50)x29 x49 (x28 x49 x50) (x27 x49 x50) = x29 x50 (x27 x49 x50) (x28 x49 x50)(x49 = x32 x50False)False)(∀ x47 x48 x49 x50 . x6 x50x43 x50x6 x49x43 x49x0 (x26 x49 x50) (x36 x49)x26 x49 x50 = x44 x47 x48x0 (x44 x48 x47) (x36 x50)(x0 (x44 (x27 x49 x50) (x28 x49 x50)) (x36 x50)False)(x49 = x32 x50False)False)(∀ x47 x48 x49 x50 . x6 x50x43 x50x6 x49x43 x49x49 = x32 x50x0 (x44 x47 x48) (x36 x50)(x29 x49 x48 x47 = x29 x50 x47 x48False)False)(∀ x47 x48 x49 x50 x51 . x6 x51x43 x51x6 x50x43 x50x50 = x32 x51x47 = x44 x49 x48x0 (x44 x48 x49) (x36 x51)(x0 x47 (x36 x50)False)False)(∀ x47 x48 x49 . x6 x49x43 x49x6 x48x43 x48x48 = x32 x49x0 x47 (x36 x48)(x0 (x44 (x24 x47 x48 x49) (x25 x47 x48 x49)) (x36 x49)False)False)(∀ x47 x48 x49 . x6 x49x43 x49x6 x48x43 x48x48 = x32 x49x0 x47 (x36 x48)(x47 = x44 (x25 x47 x48 x49) (x24 x47 x48 x49)False)False)(∀ x47 x48 x49 . x6 x49x43 x49(x29 x49 x47 x48 = x17 x49 (x44 x47 x48)False)False)(∀ x47 x48 . (x18 x48 x47 = x18 x47 x48False)False)(∀ x47 x48 . x2 x48x1 x47 x48(x43 x47False)False)(∀ x47 x48 . x2 x48x1 x47 x48(x6 x47False)False)(∀ x47 . x46 x47(x2 x47False)False)(∀ x47 . x8 x47x6 x47x43 x47(x4 x47False)False)(∀ x47 . x8 x47x6 x47x43 x47(x43 x47False)False)(∀ x47 . x8 x47x6 x47x43 x47(x6 x47False)False)(∀ x47 . x6 x47x43 x47(x4 x47False)(x43 x47False)False)(∀ x47 . x6 x47x43 x47(x4 x47False)(x6 x47False)False)(∀ x47 . x6 x47x43 x47(x4 x47False)x8 x47False)(∀ x47 . x46 x47x6 x47(x7 x47False)False)(∀ x47 . x46 x47x6 x47(x6 x47False)False)(∀ x47 . x46 x47x6 x47x43 x47(x4 x47False)False)(∀ x47 . x46 x47x6 x47x43 x47(x43 x47False)False)(∀ x47 . x46 x47x6 x47x43 x47(x6 x47False)False)(∀ x47 . x46 x47x6 x47(x34 x47False)False)(∀ x47 . x46 x47x6 x47(x6 x47False)False)(∀ x47 . x6 x47x43 x47x46 x47(x15 x47False)False)(∀ x47 . x6 x47x43 x47x46 x47(x43 x47False)False)(∀ x47 . x6 x47x43 x47x46 x47(x6 x47False)False)(∀ x47 . (x8 x47False)x46 x47False)(∀ x47 . x46 x47x6 x47x43 x47(x11 x47False)False)(∀ x47 . x46 x47x6 x47x43 x47(x43 x47False)False)(∀ x47 . x46 x47x6 x47x43 x47(x6 x47False)False)(∀ x47 . x6 x47x43 x47x15 x47(x20 x47False)False)(∀ x47 . x6 x47x43 x47x15 x47(x43 x47False)False)(∀ x47 . x6 x47x43 x47x15 x47(x6 x47False)False)(∀ x47 . x46 x47(x8 x47False)False)(∀ x47 . x46 x47(x6 x47False)False)(∀ x47 . x46 x47(x43 x47False)False)(∀ x47 x48 . x0 x47 x48x0 x48 x47False)((x0 (x44 x22 x21) (x36 (x32 x23))False)(x0 (x44 x21 x22) (x36 x23)False)False)(x0 (x44 x21 x22) (x36 x23)x0 (x44 x22 x21) (x36 (x32 x23))False)((x43 x23False)False)((x6 x23False)False)False
type
prop
theory
HotG
name
-
proof
PUa3w..
Megalodon
-
proofgold address
TMZtb..
creator
35132 PrPhD../fec2d..
owner
35137 PrPhD../ecf76..
term root
49238..