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 . x27 x29(x29 = x28False)x27 x28False)(∀ x28 x29 . x0 x28 x29x27 x29False)(∀ x28 . x27 x28(x28 = x26False)False)(∀ x28 x29 x30 . x0 x28 x29x2 x29 (x1 x30)x27 x30False)(∀ x28 x29 x30 . x0 x29 x30x2 x30 (x1 x28)(x2 x29 x28False)False)(∀ x28 x29 . x3 x29 x28(x2 x29 (x1 x28)False)False)(∀ x28 x29 . x2 x29 (x1 x28)(x3 x29 x28False)False)(∀ x28 x29 x30 . (x27 x30False)x6 x30 x28x2 x30 (x1 (x1 x28))(x27 x29False)x6 x29 x28x2 x29 (x1 (x1 x28))(x4 (x5 x30 x29) x29 = x29False)False)(∀ x28 x29 . x2 x28 x29(x27 x29False)(x0 x28 x29False)False)(∀ x28 x29 . x0 x29 x28(x2 x29 x28False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30x24 x30 x28 x29(x24 x30 x29 x28False)False)(∀ x28 . (x3 x28 x28False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30(x24 x30 x28 x28False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30x28 = x29(x24 x30 x28 x29False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30x24 x30 x28 x29(x28 = x29False)False)(∀ x28 . (x27 x28False)(x8 (x7 x28) x28False)False)(∀ x28 . (x27 x28False)(x2 (x7 x28) (x1 x28)False)False)(∀ x28 . x8 (x9 x28) x28False)(∀ x28 . (x2 (x9 x28) (x1 x28)False)False)(x27 x10False)(∀ x28 . (x27 (x23 x28)False)False)(∀ x28 . (x2 (x23 x28) (x1 x28)False)False)(∀ x28 . (x6 (x22 x28) x28False)False)(∀ x28 . x27 (x22 x28)False)(∀ x28 . (x2 (x22 x28) (x1 (x1 x28))False)False)((x27 x11False)False)(∀ x28 . (x27 x28False)x27 (x21 x28)False)(∀ x28 . (x27 x28False)(x2 (x21 x28) (x1 x28)False)False)(∀ x28 . (x27 x28False)x27 (x20 x28)False)(∀ x28 . (x27 x28False)(x25 (x20 x28) x28False)False)(∀ x28 x29 . (x27 x29False)(x27 x28False)x25 x28 x29(x2 x28 (x1 (x1 x29))False)False)(∀ x28 x29 . (x27 x29False)(x27 x28False)x25 x28 x29(x6 x28 x29False)False)(∀ x28 x29 . (x27 x29False)(x27 x28False)x25 x28 x29x27 x28False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30x27 (x12 x30 x28 x29)False)((x27 x26False)False)(∀ x28 . x27 (x1 x28)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30x27 (x19 x30 x28 x29)False)(∀ x28 . (x2 (x13 x28) x28False)False)(∀ x28 . (x25 (x18 x28) x28False)False)((x27 x14False)False)(∀ x28 x29 . x25 x29 x28(x2 x29 (x1 (x1 x28))False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30(x25 (x12 x30 x28 x29) x30False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30(x25 (x19 x30 x28 x29) x30False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30(x12 x30 x28 x29 = x4 x28 x29False)False)(∀ x28 x29 x30 . (x27 x30False)(x27 x28False)x25 x28 x30(x27 x29False)x25 x29 x30(x19 x30 x28 x29 = x5 x28 x29False)False)((x26 = x14False)False)(∀ x28 x29 . (x5 x29 x28 = x5 x28 x29False)False)(∀ x28 x29 . (x4 x29 x28 = x4 x28 x29False)False)(∀ x28 x29 . x27 x29x2 x28 (x1 x29)x8 x28 x29False)(∀ x28 x29 . (x27 x29False)x2 x28 (x1 x29)x27 x28(x8 x28 x29False)False)(∀ x28 x29 . (x27 x29False)x2 x28 (x1 x29)(x8 x28 x29False)x27 x28False)(∀ x28 x29 . x27 x29x2 x28 (x1 x29)(x27 x28False)False)(∀ x28 x29 . x0 x28 x29x0 x29 x28False)(x24 x15 (x12 x15 (x19 x15 x17 x16) x16) x16False)((x25 x16 x15False)False)(x27 x16False)((x25 x17 x15False)False)(x27 x17False)(x27 x15False)False
type
prop
theory
HotG
name
-
proof
PUT4x..
Megalodon
-
proofgold address
TMMZz..
creator
35143 PrPhD../c78b2..
owner
35144 PrPhD../da631..
term root
cf16c..