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 . x58 x60(x60 = x59False)x58 x59False)(∀ x59 x60 . x0 x59 x60x58 x60False)(∀ x59 . x58 x59(x59 = x57False)False)(∀ x59 x60 x61 . x0 x59 x60x2 x60 (x1 x61)x58 x61False)(∀ x59 x60 x61 . x0 x60 x61x2 x61 (x1 x59)(x2 x60 x59False)False)(∀ x59 x60 . x3 x60 x59(x2 x60 (x1 x59)False)False)(∀ x59 x60 . x2 x60 (x1 x59)(x3 x60 x59False)False)(∀ x59 x60 . x2 x59 x60(x58 x60False)(x0 x59 x60False)False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x1 (x53 x61)))(x0 x59 (x54 x60 x59 x61)False)(x0 (x54 x60 x59 x61) x60False)x60 = x57False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x1 (x53 x61)))(x4 (x54 x60 x59 x61) x61False)(x0 (x54 x60 x59 x61) x60False)x60 = x57False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x1 (x53 x61)))(x51 (x54 x60 x59 x61) x61False)(x0 (x54 x60 x59 x61) x60False)x60 = x57False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x1 (x53 x61)))x0 (x54 x60 x59 x61) x60x51 (x54 x60 x59 x61) x61x4 (x54 x60 x59 x61) x61x0 x59 (x54 x60 x59 x61)x60 = x57False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x1 (x53 x61)))(x2 (x54 x60 x59 x61) (x1 (x53 x61))False)x60 = x57False)(∀ x59 x60 . x0 x60 x59(x2 x60 x59False)False)(x58 x50False)(∀ x59 . (x3 x59 x59False)False)(∀ x59 x60 . x2 x59 (x1 (x1 x60))(x49 x60 x59 = x48 x59False)False)(∀ x59 . x52 x59x55 x59(x5 (x6 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x2 (x6 x59) (x1 (x53 x59))False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x4 (x7 x59) x59False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59x58 (x7 x59)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x2 (x7 x59) (x1 (x53 x59))False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59x46 (x47 x59) x59False)(∀ x59 . (x56 x59False)x52 x59x55 x59x58 (x47 x59)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x2 (x47 x59) (x1 (x53 x59))False)False)(∀ x59 . (x8 x59False)x8 (x9 x59)False)(∀ x59 . (x8 x59False)(x2 (x9 x59) (x1 x59)False)False)(∀ x59 . x52 x59x55 x59(x4 (x10 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x2 (x10 x59) (x1 (x53 x59))False)False)(∀ x59 . x55 x59(x46 (x11 x59) x59False)False)(∀ x59 . x55 x59(x2 (x11 x59) (x1 (x53 x59))False)False)(∀ x59 . (x58 x59False)(x8 (x12 x59)False)False)(∀ x59 . (x58 x59False)x58 (x12 x59)False)(∀ x59 . (x58 x59False)(x2 (x12 x59) (x1 x59)False)False)(∀ x59 . (x58 x59False)(x44 (x45 x59) x59False)False)(∀ x59 . (x58 x59False)(x2 (x45 x59) (x1 x59)False)False)(∀ x59 . (x56 x59False)x42 x59x58 (x43 x59)False)(∀ x59 . (x56 x59False)x42 x59(x2 (x43 x59) (x1 (x53 x59))False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x4 (x41 x59) x59False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x51 (x41 x59) x59False)False)(∀ x59 . (x56 x59False)x52 x59x55 x59x58 (x41 x59)False)(∀ x59 . (x56 x59False)x52 x59x55 x59(x2 (x41 x59) (x1 (x53 x59))False)False)(∀ x59 . x44 (x40 x59) x59False)(∀ x59 . (x2 (x40 x59) (x1 x59)False)False)(x58 x39False)(∀ x59 . x52 x59x55 x59(x4 (x13 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x51 (x13 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x2 (x13 x59) (x1 (x53 x59))False)False)(∀ x59 . (x58 (x38 x59)False)False)(∀ x59 . (x2 (x38 x59) (x1 x59)False)False)(∀ x59 . (x37 x59False)x42 x59x8 (x36 x59)False)(∀ x59 . (x37 x59False)x42 x59(x2 (x36 x59) (x1 (x53 x59))False)False)(∀ x59 . (x56 x59False)x42 x59(x8 (x35 x59)False)False)(∀ x59 . (x56 x59False)x42 x59x58 (x35 x59)False)(∀ x59 . (x56 x59False)x42 x59(x2 (x35 x59) (x1 (x53 x59))False)False)((x58 x14False)False)(∀ x59 . x52 x59x55 x59(x51 (x34 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x2 (x34 x59) (x1 (x53 x59))False)False)(∀ x59 . (x58 x59False)x58 (x33 x59)False)(∀ x59 . (x58 x59False)(x2 (x33 x59) (x1 x59)False)False)(∀ x59 . x55 x59(x58 (x32 x59)False)False)(∀ x59 . x55 x59(x2 (x32 x59) (x1 (x53 x59))False)False)(∀ x59 . x52 x59x55 x59(x51 (x31 x59) x59False)False)(∀ x59 . x52 x59x55 x59(x2 (x31 x59) (x1 (x53 x59))False)False)(∀ x59 . (x30 x59False)x42 x59x29 (x53 x59)False)(∀ x59 . x30 x59x42 x59(x29 (x53 x59)False)False)(∀ x59 . x37 x59x42 x59(x8 (x53 x59)False)False)(∀ x59 . (x37 x59False)x42 x59x8 (x53 x59)False)(∀ x59 . (x56 x59False)x42 x59x58 (x53 x59)False)((x58 x57False)False)(∀ x59 . x58 (x1 x59)False)(∀ x59 . x56 x59x42 x59(x58 (x53 x59)False)False)(∀ x59 . (x2 (x28 x59) x59False)False)((x42 x15False)False)((x55 x27False)False)(∀ x59 . x55 x59(x42 x59False)False)(∀ x59 x60 . x2 x60 (x1 (x1 x59))(x2 (x49 x59 x60) (x1 x59)False)False)(∀ x59 x60 . (x56 x60False)x52 x60x55 x60x2 x59 (x53 x60)(x2 (x16 x60 x59) (x1 (x53 x60))False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x2 x60 (x1 (x1 (x53 x62)))(x0 x59 (x26 x60 x61 x59 x62)False)(x0 (x26 x60 x61 x59 x62) x60False)x49 (x53 x62) x60 = x61(x61 = x16 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x2 x60 (x1 (x1 (x53 x62)))(x4 (x26 x60 x61 x59 x62) x62False)(x0 (x26 x60 x61 x59 x62) x60False)x49 (x53 x62) x60 = x61(x61 = x16 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x2 x60 (x1 (x1 (x53 x62)))(x51 (x26 x60 x61 x59 x62) x62False)(x0 (x26 x60 x61 x59 x62) x60False)x49 (x53 x62) x60 = x61(x61 = x16 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x2 x60 (x1 (x1 (x53 x62)))x0 (x26 x60 x61 x59 x62) x60x51 (x26 x60 x61 x59 x62) x62x4 (x26 x60 x61 x59 x62) x62x0 x59 (x26 x60 x61 x59 x62)x49 (x53 x62) x60 = x61(x61 = x16 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x2 x60 (x1 (x1 (x53 x62)))(x2 (x26 x60 x61 x59 x62) (x1 (x53 x62))False)x49 (x53 x62) x60 = x61(x61 = x16 x62 x59False)False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x53 x61))x60 = x16 x61 x59(x49 (x53 x61) (x17 x60 x59 x61) = x60False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x61 = x16 x62 x59x2 x60 (x1 (x53 x62))x51 x60 x62x4 x60 x62x0 x59 x60(x0 x60 (x17 x61 x59 x62)False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x61 = x16 x62 x59x2 x60 (x1 (x53 x62))x0 x60 (x17 x61 x59 x62)(x0 x59 x60False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x61 = x16 x62 x59x2 x60 (x1 (x53 x62))x0 x60 (x17 x61 x59 x62)(x4 x60 x62False)False)(∀ x59 x60 x61 x62 . (x56 x62False)x52 x62x55 x62x2 x59 (x53 x62)x2 x61 (x1 (x53 x62))x61 = x16 x62 x59x2 x60 (x1 (x53 x62))x0 x60 (x17 x61 x59 x62)(x51 x60 x62False)False)(∀ x59 x60 x61 . (x56 x61False)x52 x61x55 x61x2 x59 (x53 x61)x2 x60 (x1 (x53 x61))x60 = x16 x61 x59(x2 (x17 x60 x59 x61) (x1 (x1 (x53 x61)))False)False)(∀ x59 x60 . x60 = x57x59 = x57(x59 = x48 x60False)False)(∀ x59 x60 . x60 = x57x59 = x48 x60(x59 = x57False)False)(∀ x59 x60 x61 . (x61 = x57False)x0 x59 x61(x0 (x18 x60 x61) x59False)(x0 (x18 x60 x61) x60False)(x60 = x48 x61False)False)(∀ x59 x60 . (x60 = x57False)x0 (x18 x59 x60) x59x0 (x18 x59 x60) (x25 x59 x60)(x59 = x48 x60False)False)(∀ x59 x60 . (x60 = x57False)x0 (x18 x59 x60) x59(x0 (x25 x59 x60) x60False)(x59 = x48 x60False)False)(∀ x59 x60 x61 . (x61 = x57False)x59 = x48 x61x0 x60 (x24 x60 x59 x61)(x0 x60 x59False)False)(∀ x59 x60 x61 . (x61 = x57False)x59 = x48 x61(x0 (x24 x60 x59 x61) x61False)(x0 x60 x59False)False)(∀ x59 x60 x61 x62 . (x62 = x57False)x59 = x48 x62x0 x61 x59x0 x60 x62(x0 x61 x60False)False)(∀ x59 . x42 x59x19 x59 x57(x56 x59False)False)(∀ x59 . x55 x59x56 x59(x23 x59False)False)(∀ x59 . x42 x59x56 x59(x19 x59 x57False)False)(∀ x59 . x42 x59(x30 x59False)x37 x59False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x51 x59 x60x5 x59 x60(x58 x59False)False)(∀ x59 . x42 x59x37 x59(x30 x59False)False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x4 x59 x60x46 x59 x60(x5 x59 x60False)False)(∀ x59 x60 . x8 x60x2 x59 (x1 x60)(x8 x59False)False)(∀ x59 . x42 x59(x30 x59False)x30 x59False)(∀ x59 . x42 x59(x30 x59False)x56 x59False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x5 x59 x60(x46 x59 x60False)False)(∀ x59 x60 . x58 x60x2 x59 (x1 x60)x44 x59 x60False)(∀ x59 . x42 x59x56 x59(x30 x59False)False)(∀ x59 . x42 x59x56 x59(x56 x59False)False)(∀ x59 x60 . x55 x60x2 x59 (x1 (x53 x60))x58 x59(x20 x59 x60False)False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x58 x59(x5 x59 x60False)False)(∀ x59 x60 . (x58 x60False)x2 x59 (x1 x60)x58 x59(x44 x59 x60False)False)(∀ x59 x60 . x55 x60x2 x59 (x1 (x53 x60))x58 x59(x46 x59 x60False)False)(∀ x59 x60 . (x58 x60False)x2 x59 (x1 x60)(x44 x59 x60False)x58 x59False)(∀ x59 . x42 x59(x37 x59False)x56 x59False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x58 x59(x4 x59 x60False)False)(∀ x59 x60 . x52 x60x55 x60x2 x59 (x1 (x53 x60))x58 x59(x51 x59 x60False)False)(∀ x59 x60 . x58 x60x2 x59 (x1 x60)(x58 x59False)False)(∀ x59 . x42 x59x56 x59(x37 x59False)False)(∀ x59 . x42 x59(x37 x59False)x56 x59False)(∀ x59 . x42 x59x19 x59 x50(x37 x59False)False)(∀ x59 . x42 x59x19 x59 x50x56 x59False)(∀ x59 . x42 x59(x56 x59False)x37 x59(x19 x59 x50False)False)(∀ x59 x60 . x0 x59 x60x0 x60 x59False)(x0 x22 (x16 x21 x22)False)((x2 x22 (x53 x21)False)False)((x55 x21False)False)((x52 x21False)False)(x56 x21False)False
type
prop
theory
HotG
name
-
proof
PUPDV..
Megalodon
-
proofgold address
TMHws..
creator
35128 PrPhD../39fb9..
owner
35131 PrPhD../a0267..
term root
6d6ec..