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 x61(x61 = x60False)x59 x60False)(∀ x60 x61 . x0 x60 x61x59 x61False)(∀ x60 . x59 x60(x60 = x58False)False)(∀ x60 x61 x62 . x0 x60 x61x2 x61 (x1 x62)x59 x62False)(∀ x60 x61 x62 . x0 x61 x62x2 x62 (x1 x60)(x2 x61 x60False)False)(∀ x60 x61 . x3 x61 x60(x2 x61 (x1 x60)False)False)(∀ x60 x61 . x2 x61 (x1 x60)(x3 x61 x60False)False)(∀ x60 . x4 x60(x5 x6 x60 = x60False)False)(∀ x60 x61 . x4 x61x4 x60(x56 (x57 x61 x60) = x55 (x56 x61) (x56 x60)False)False)(∀ x60 x61 . x2 x60 x61(x59 x61False)(x0 x60 x61False)False)(∀ x60 x61 . x0 x61 x60(x2 x61 x60False)False)((x2 x58 x7False)False)(∀ x60 x61 . x4 x61x4 x60(x53 (x54 x61) (x54 x60) = x53 x60 x61False)False)(∀ x60 x61 . x4 x61x4 x60(x57 (x54 x61) (x54 x60) = x54 (x57 x61 x60)False)False)(∀ x60 x61 x62 . x4 x62x4 x60x4 x61(x5 (x5 x62 x60) x61 = x5 x62 (x5 x60 x61)False)False)(∀ x60 x61 x62 . x4 x62x4 x60x4 x61(x57 (x57 x62 x60) x61 = x57 x62 (x57 x60 x61)False)False)(∀ x60 x61 x62 . x4 x62x4 x60x4 x61(x5 (x57 x62 x60) x61 = x57 (x5 x62 x61) (x5 x60 x61)False)False)(∀ x60 . x4 x60(x5 x60 (x54 x6) = x54 x60False)False)((x2 x6 x52False)False)((x2 x6 x8False)False)((x51 x6 x52 x8False)False)((x9 x6False)False)(x59 x6False)(∀ x60 x61 . x4 x61x4 x60(x57 x61 (x54 x60) = x53 x61 x60False)False)((x2 x50 x52False)False)((x2 x50 x8False)False)((x51 x50 x52 x8False)False)((x59 x50False)False)((x54 (x54 x6) = x6False)False)((x54 x6 = x54 x6False)False)((x54 x50 = x50False)False)((x5 x6 x6 = x6False)False)((x5 x6 x50 = x50False)False)((x5 x50 x6 = x50False)False)((x5 x50 x50 = x50False)False)((x53 (x54 x6) (x54 x6) = x50False)False)((x53 (x54 x6) x50 = x54 x6False)False)((x53 x6 x6 = x50False)False)((x53 x6 x50 = x6False)False)((x53 x50 (x54 x6) = x6False)False)((x53 x50 x6 = x54 x6False)False)((x53 x50 x50 = x50False)False)((x57 (x54 x6) x6 = x50False)False)((x57 (x54 x6) x50 = x54 x6False)False)((x57 x6 (x54 x6) = x50False)False)((x57 x6 x50 = x6False)False)((x57 x50 (x54 x6) = x54 x6False)False)((x57 x50 x6 = x6False)False)((x57 x50 x50 = x50False)False)(∀ x60 . (x3 x60 x60False)False)(∀ x60 x61 x62 . (x59 x62False)(x59 x60False)x2 x60 (x1 x62)x2 x61 x60(x51 x61 x62 x60False)False)(∀ x60 x61 x62 . (x59 x62False)(x59 x60False)x2 x60 (x1 x62)x51 x61 x62 x60(x2 x61 x60False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x48 x61 x60 = x5 x61 x60False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x55 x61 x60 = x57 x61 x60False)False)((x8 = x7False)False)(∀ x60 . x4 x60(x56 x60 = x10 x60False)False)((x47 x46False)False)((x59 x46False)False)((x45 x44False)False)((x47 x44False)False)((x4 x44False)False)((x59 x44False)False)((x43 x42False)False)((x47 x42False)False)((x45 x41False)False)((x43 x41False)False)((x47 x41False)False)((x4 x41False)False)((x40 x39False)False)((x11 x39False)False)(x59 x39False)((x9 x12False)False)((x47 x12False)False)((x45 x13False)False)((x9 x13False)False)((x47 x13False)False)((x4 x13False)False)((x4 x14False)False)(x59 x14False)(x59 x15False)((x11 x38False)False)(x59 x38False)((x37 x36False)False)((x47 x16False)False)((x45 x35False)False)((x4 x17False)False)((x59 x34False)False)((x11 x18False)False)(x59 x18False)((x37 x19False)False)((x45 x19False)False)((x4 x19False)False)((x47 x19False)False)((x2 x19 x52False)False)(∀ x60 . x4 x60(x54 (x54 x60) = x60False)False)(∀ x60 . x4 x60(x56 (x56 x60) = x60False)False)(∀ x60 . x4 x60(x10 (x10 x60) = x60False)False)(∀ x60 x61 . (x43 x61False)x45 x61(x43 x60False)x45 x60x43 (x57 x61 x60)False)(x33 x49False)(∀ x60 x61 . (x59 x61False)x4 x61(x59 x60False)x4 x60x59 (x5 x61 x60)False)(x33 x52False)(∀ x60 x61 . x45 x61x45 x60(x45 (x53 x61 x60)False)False)(∀ x60 x61 . x45 x61x45 x60(x45 (x5 x61 x60)False)False)(∀ x60 . (x59 x60False)x4 x60(x4 (x54 x60)False)False)(∀ x60 . (x59 x60False)x4 x60x59 (x54 x60)False)((x11 x7False)False)(∀ x60 x61 . x45 x61x45 x60(x45 (x57 x61 x60)False)False)((x40 x7False)False)((x40 x52False)False)((x40 x49False)False)(∀ x60 x61 . x4 x61x4 x60(x4 (x53 x61 x60)False)False)(∀ x60 x61 . x37 x61x37 x60(x37 (x53 x61 x60)False)False)(∀ x60 . x45 x60(x45 (x54 x60)False)False)(∀ x60 . x45 x60(x4 (x54 x60)False)False)(∀ x60 x61 . x4 x61x4 x60(x4 (x5 x61 x60)False)False)((x20 x52False)False)(∀ x60 . x37 x60(x37 (x54 x60)False)False)(∀ x60 . x37 x60(x4 (x54 x60)False)False)(∀ x60 x61 . x4 x61x4 x60(x4 (x57 x61 x60)False)False)(x59 x49False)(∀ x60 x61 . x37 x61x37 x60(x37 (x5 x61 x60)False)False)(∀ x60 x61 . (x43 x61False)x45 x61(x43 x60False)x45 x60x43 (x5 x61 x60)False)(∀ x60 x61 . (x9 x61False)x45 x61(x9 x60False)x45 x60x43 (x5 x61 x60)False)(∀ x60 x61 . (x9 x61False)x45 x61(x43 x60False)x45 x60x9 (x5 x60 x61)False)(∀ x60 x61 . (x9 x61False)x45 x61(x43 x60False)x45 x60x9 (x5 x61 x60)False)(∀ x60 x61 . x43 x61x45 x61(x43 x60False)x45 x60(x9 (x53 x60 x61)False)False)(∀ x60 x61 . x43 x61x45 x61(x43 x60False)x45 x60(x43 (x53 x61 x60)False)False)(∀ x60 x61 . x9 x61x45 x61(x9 x60False)x45 x60(x43 (x53 x60 x61)False)False)((x59 x58False)False)(x59 x52False)((x32 x49False)False)(∀ x60 x61 . x37 x61x37 x60(x37 (x57 x61 x60)False)False)(∀ x60 x61 . x9 x61x45 x61(x9 x60False)x45 x60(x9 (x53 x61 x60)False)False)(∀ x60 x61 . (x43 x61False)x45 x61(x9 x60False)x45 x60x9 (x53 x60 x61)False)(∀ x60 x61 . (x43 x61False)x45 x61(x9 x60False)x45 x60x43 (x53 x61 x60)False)(∀ x60 . (x43 x60False)x45 x60x9 (x54 x60)False)(∀ x60 . (x43 x60False)x45 x60(x4 (x54 x60)False)False)(∀ x60 . (x9 x60False)x45 x60x43 (x54 x60)False)(∀ x60 . (x9 x60False)x45 x60(x4 (x54 x60)False)False)(∀ x60 x61 . x43 x61x45 x61(x9 x60False)x45 x60(x43 (x57 x60 x61)False)False)(∀ x60 x61 . x43 x61x45 x61(x9 x60False)x45 x60(x43 (x57 x61 x60)False)False)(∀ x60 x61 . x9 x61x45 x61(x43 x60False)x45 x60(x9 (x57 x60 x61)False)False)(∀ x60 x61 . x9 x61x45 x61(x43 x60False)x45 x60(x9 (x57 x61 x60)False)False)(∀ x60 x61 . (x9 x61False)x45 x61(x9 x60False)x45 x60x9 (x57 x61 x60)False)(∀ x60 x61 . (x59 x61False)(x59 x60False)x2 x60 (x1 x61)(x51 (x31 x60 x61) x61 x60False)False)(∀ x60 . (x2 (x21 x60) x60False)False)(∀ x60 x61 x62 . (x59 x62False)(x59 x60False)x2 x60 (x1 x62)x51 x61 x62 x60(x2 x61 x62False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x2 (x48 x61 x60) x49False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x2 (x55 x61 x60) x49False)False)((x2 x8 (x1 x52)False)False)(∀ x60 . x4 x60(x4 (x54 x60)False)False)(∀ x60 x61 . x4 x61x4 x60(x2 (x22 x61 x60) x49False)False)(∀ x60 . x4 x60(x2 (x56 x60) x49False)False)(∀ x60 . x4 x60(x4 (x10 x60)False)False)(∀ x60 x61 . x4 x61x4 x60(x53 x61 x60 = x57 x61 (x54 x60)False)False)(∀ x60 x61 . x4 x61x4 x60(x22 x61 x60 = x5 x61 (x56 x60)False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x48 x61 x60 = x48 x60 x61False)False)(∀ x60 x61 . x2 x61 x49x2 x60 x49(x55 x61 x60 = x55 x60 x61False)False)(∀ x60 x61 . x4 x61x4 x60(x5 x61 x60 = x5 x60 x61False)False)(∀ x60 x61 . x4 x61x4 x60(x57 x61 x60 = x57 x60 x61False)False)(∀ x60 . x47 x60(x9 x60False)(x43 x60False)(x47 x60False)False)(∀ x60 . x47 x60(x9 x60False)(x43 x60False)(x59 x60False)False)(∀ x60 . x2 x60 (x1 x52)(x20 x60False)False)(∀ x60 . x59 x60x47 x60x43 x60False)(∀ x60 . x59 x60x47 x60x9 x60False)(∀ x60 . x59 x60x47 x60(x47 x60False)False)(∀ x60 . (x59 x60False)x47 x60(x9 x60False)(x43 x60False)False)(∀ x60 . (x59 x60False)x47 x60(x9 x60False)(x47 x60False)False)(∀ x60 . x2 x60 (x1 x49)(x32 x60False)False)(∀ x60 . x47 x60x43 x60x9 x60False)(∀ x60 . x47 x60x43 x60(x47 x60False)False)(∀ x60 . x47 x60x43 x60x59 x60False)(∀ x60 . x20 x60(x32 x60False)False)(∀ x60 . (x59 x60False)x47 x60(x43 x60False)(x9 x60False)False)(∀ x60 . (x59 x60False)x47 x60(x43 x60False)(x47 x60False)False)(∀ x60 . x45 x60(x47 x60False)False)(∀ x60 . x20 x60(x30 x60False)False)(∀ x60 . x47 x60x9 x60x43 x60False)(∀ x60 . x47 x60x9 x60(x47 x60False)False)(∀ x60 . x47 x60x9 x60x59 x60False)(∀ x60 . x45 x60(x4 x60False)False)(∀ x60 . x2 x60 x49(x4 x60False)False)(∀ x60 . x29 x60(x20 x60False)False)(∀ x60 . x37 x60(x45 x60False)False)(∀ x60 . x28 x60(x47 x60False)False)(∀ x60 . x28 x60(x45 x60False)False)(∀ x60 . x28 x60(x4 x60False)False)(∀ x60 . x23 x60(x29 x60False)False)(∀ x60 . x28 x60(x37 x60False)False)(∀ x60 . x59 x60(x40 x60False)False)(∀ x60 . x2 x60 x8(x11 x60False)False)(∀ x60 x61 . x11 x61x2 x60 (x1 x61)(x11 x60False)False)(∀ x60 x61 . x23 x61x2 x60 (x1 x61)(x23 x60False)False)(∀ x60 x61 . x29 x61x2 x60 (x1 x61)(x29 x60False)False)(∀ x60 x61 . x20 x61x2 x60 (x1 x61)(x20 x60False)False)(∀ x60 x61 . x30 x61x2 x60 (x1 x61)(x30 x60False)False)(∀ x60 . x2 x60 x52(x45 x60False)False)(∀ x60 . x2 x60 x52(x4 x60False)False)(∀ x60 . x11 x60(x23 x60False)False)(∀ x60 x61 . x32 x61x2 x60 (x1 x61)(x32 x60False)False)(∀ x60 . x59 x60(x11 x60False)False)(∀ x60 x61 . x11 x61x2 x60 x61(x28 x60False)False)(∀ x60 x61 . x23 x61x2 x60 x61(x37 x60False)False)(∀ x60 x61 . x29 x61x2 x60 x61(x24 x60False)False)(∀ x60 x61 . x20 x61x2 x60 x61(x45 x60False)False)(∀ x60 x61 . x30 x61x2 x60 x61(x47 x60False)False)(∀ x60 x61 . x32 x61x2 x60 x61(x4 x60False)False)(∀ x60 . x2 x60 (x1 x8)(x11 x60False)False)(∀ x60 x61 . x0 x60 x61x0 x61 x60False)(x22 x27 (x55 x26 x25) = x55 (x22 x27 x26) (x22 x27 x25)False)((x2 x25 x49False)False)((x2 x26 x49False)False)((x2 x27 x49False)False)False
type
prop
theory
HotG
name
-
proof
PUdfa..
Megalodon
-
proofgold address
TMM3i..
creator
35127 PrPhD../b661a..
owner
35131 PrPhD../23bff..
term root
27b9b..