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 . x48 x50(x50 = x49False)x48 x49False)(∀ x49 x50 . x0 x49 x50x48 x50False)(∀ x49 . x48 x49(x49 = x47False)False)(∀ x49 . x1 x49(x2 x49 x3 = x49False)False)(∀ x49 x50 x51 . x0 x49 x50x45 x50 (x46 x51)x48 x51False)(∀ x49 . x1 x49(x2 x4 x49 = x4False)False)(∀ x49 x50 x51 . x0 x50 x51x45 x51 (x46 x49)(x45 x50 x49False)False)(∀ x49 . x1 x49(x5 x49 x4 = x49False)False)(∀ x49 . x1 x49(x2 x49 x4 = x4False)False)(∀ x49 x50 . x6 x50 x49(x45 x50 (x46 x49)False)False)(∀ x49 x50 . x45 x50 (x46 x49)(x6 x50 x49False)False)(∀ x49 . x1 x49(x7 x3 x49 = x49False)False)(∀ x49 x50 . x45 x49 x50(x48 x50False)(x0 x49 x50False)False)(∀ x49 . x1 x49(x7 x49 x4 = x4False)False)(∀ x49 x50 . x0 x50 x49(x45 x50 x49False)False)((x45 x47 x8False)False)(∀ x49 x50 . x1 x50x1 x49x7 x49 x50 = x44 x50(x50 = x4False)(x49 = x44 x3False)False)(∀ x49 x50 . x1 x50x1 x49(x5 (x44 x50) (x44 x49) = x5 x49 x50False)False)(∀ x49 x50 x51 . x1 x51x1 x49x1 x50(x7 (x7 x51 x49) x50 = x7 x51 (x7 x49 x50)False)False)(∀ x49 x50 x51 . x1 x51x1 x49x1 x50(x7 x51 (x2 x49 x50) = x2 (x7 x51 x49) x50False)False)((x45 x42 x43False)False)((x45 x42 x9False)False)((x41 x42 x43 x9False)False)((x10 x42False)False)(x48 x42False)(∀ x49 . x1 x49(x7 x49 (x44 x3) = x44 x49False)False)((x45 x3 x43False)False)((x45 x3 x9False)False)((x41 x3 x43 x9False)False)((x10 x3False)False)(x48 x3False)((x45 x11 x43False)False)((x45 x11 x9False)False)((x41 x11 x43 x9False)False)((x48 x11False)False)((x44 (x2 (x44 x3) x42) = x2 x3 x42False)False)((x44 (x2 x3 x42) = x2 (x44 x3) x42False)False)((x44 (x44 x42) = x42False)False)((x44 (x44 x3) = x3False)False)((x44 x42 = x44 x42False)False)((x44 x3 = x44 x3False)False)((x44 x11 = x11False)False)((x7 (x2 (x44 x3) x42) (x44 x42) = x3False)False)((x7 (x2 (x44 x3) x42) x42 = x44 x3False)False)((x7 (x2 (x44 x3) x42) x3 = x2 (x44 x3) x42False)False)((x7 (x2 x3 x42) (x44 x42) = x44 x3False)False)((x7 (x2 x3 x42) x42 = x3False)False)((x7 (x2 x3 x42) x3 = x2 x3 x42False)False)((x7 (x2 x3 x42) x11 = x11False)False)((x7 (x44 x42) (x2 (x44 x3) x42) = x3False)False)((x7 (x44 x42) (x2 x3 x42) = x44 x3False)False)((x7 (x44 x42) x3 = x44 x42False)False)((x7 (x44 x42) x11 = x11False)False)((x7 x42 (x2 (x44 x3) x42) = x44 x3False)False)((x7 x42 (x2 x3 x42) = x3False)False)((x7 x42 x3 = x42False)False)((x7 x42 x11 = x11False)False)((x7 x3 (x2 (x44 x3) x42) = x2 (x44 x3) x42False)False)((x7 x3 (x2 x3 x42) = x2 x3 x42False)False)((x7 x3 (x44 x42) = x44 x42False)False)((x7 x3 x42 = x42False)False)((x7 x3 x3 = x3False)False)((x7 x3 x11 = x11False)False)((x7 x11 (x2 x3 x42) = x11False)False)((x7 x11 (x44 x42) = x11False)False)((x7 x11 x42 = x11False)False)((x7 x11 x3 = x11False)False)((x7 x11 x11 = x11False)False)((x2 (x44 x42) x42 = x44 x3False)False)((x2 (x44 x3) x42 = x2 (x44 x3) x42False)False)((x2 (x44 x3) x3 = x44 x3False)False)((x2 x42 x42 = x3False)False)((x2 x42 x3 = x42False)False)((x2 x3 (x2 (x44 x3) x42) = x44 x42False)False)((x2 x3 (x2 x3 x42) = x42False)False)((x2 x3 (x44 x42) = x2 (x44 x3) x42False)False)((x2 x3 (x44 x3) = x44 x3False)False)((x2 x3 x42 = x2 x3 x42False)False)((x2 x3 x3 = x3False)False)((x5 (x2 (x44 x3) x42) (x2 (x44 x3) x42) = x11False)False)((x5 (x2 (x44 x3) x42) (x2 x3 x42) = x44 x3False)False)((x5 (x2 (x44 x3) x42) (x44 x3) = x2 x3 x42False)False)((x5 (x2 (x44 x3) x42) x11 = x2 (x44 x3) x42False)False)((x5 (x2 x3 x42) (x2 (x44 x3) x42) = x3False)False)((x5 (x2 x3 x42) (x2 x3 x42) = x11False)False)((x5 (x2 x3 x42) x3 = x2 (x44 x3) x42False)False)((x5 (x2 x3 x42) x11 = x2 x3 x42False)False)((x5 (x44 x42) (x44 x42) = x11False)False)((x5 (x44 x42) (x44 x3) = x44 x3False)False)((x5 (x44 x42) x11 = x44 x42False)False)((x5 (x44 x3) (x2 (x44 x3) x42) = x2 (x44 x3) x42False)False)((x5 (x44 x3) (x44 x42) = x3False)False)((x5 (x44 x3) (x44 x3) = x11False)False)((x5 (x44 x3) x3 = x44 x42False)False)((x5 (x44 x3) x11 = x44 x3False)False)((x5 x42 x42 = x11False)False)((x5 x42 x3 = x3False)False)((x5 x42 x11 = x42False)False)((x5 x3 (x2 x3 x42) = x2 x3 x42False)False)((x5 x3 (x44 x3) = x42False)False)((x5 x3 x42 = x44 x3False)False)((x5 x3 x3 = x11False)False)((x5 x3 x11 = x3False)False)((x5 x11 (x2 (x44 x3) x42) = x2 x3 x42False)False)((x5 x11 (x2 x3 x42) = x2 (x44 x3) x42False)False)((x5 x11 (x44 x42) = x42False)False)((x5 x11 (x44 x3) = x3False)False)((x5 x11 x42 = x44 x42False)False)((x5 x11 x3 = x44 x3False)False)((x5 x11 x11 = x11False)False)(∀ x49 . (x6 x49 x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x45 x49 (x46 x51)x45 x50 x49(x41 x50 x51 x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x45 x49 (x46 x51)x41 x50 x51 x49(x45 x50 x49False)False)((x4 = x47False)False)((x9 = x8False)False)((x12 x13False)False)(x48 x13False)((x14 x15False)False)((x48 x15False)False)((x16 x17False)False)((x14 x17False)False)((x1 x17False)False)((x48 x17False)False)((x12 x18False)False)((x40 x39False)False)((x14 x39False)False)((x16 x38False)False)((x40 x38False)False)((x14 x38False)False)((x1 x38False)False)((x10 x37False)False)((x14 x37False)False)((x16 x36False)False)((x10 x36False)False)((x14 x36False)False)((x1 x36False)False)((x1 x35False)False)(x48 x35False)(x48 x34False)((x19 x20False)False)((x33 x20False)False)((x21 x20False)False)(x48 x20False)((x14 x22False)False)((x16 x32False)False)((x1 x23False)False)((x48 x31False)False)((x19 x24False)False)(∀ x49 x50 . x1 x50x1 x49(x50 = x4False)(x7 (x2 x49 x50) x50 = x49False)False)(∀ x49 . x1 x49(x44 (x44 x49) = x49False)False)(∀ x49 x50 . (x48 x50False)x1 x50(x48 x49False)x1 x49x48 (x2 x50 x49)False)(∀ x49 x50 . x16 x50x16 x49(x16 (x2 x50 x49)False)False)(∀ x49 x50 . (x48 x50False)x1 x50(x48 x49False)x1 x49x48 (x7 x50 x49)False)(∀ x49 x50 . x16 x50x16 x49(x16 (x5 x50 x49)False)False)(∀ x49 x50 . x16 x50x16 x49(x16 (x7 x50 x49)False)False)(∀ x49 . (x48 x49False)x1 x49(x1 (x44 x49)False)False)(∀ x49 . (x48 x49False)x1 x49x48 (x44 x49)False)((x19 x8False)False)(x48 x8False)(∀ x49 x50 . x1 x50x1 x49(x1 (x2 x50 x49)False)False)(∀ x49 x50 . x1 x50x1 x49(x1 (x5 x50 x49)False)False)(∀ x49 . x16 x49(x16 (x44 x49)False)False)(∀ x49 . x16 x49(x1 (x44 x49)False)False)(∀ x49 x50 . x1 x50x1 x49(x1 (x7 x50 x49)False)False)(∀ x49 x50 . (x10 x50False)x16 x50(x10 x49False)x16 x49x40 (x2 x50 x49)False)(∀ x49 x50 . (x40 x50False)x16 x50(x40 x49False)x16 x49x40 (x2 x50 x49)False)(∀ x49 x50 . (x40 x50False)x16 x50(x10 x49False)x16 x49x10 (x2 x49 x50)False)(∀ x49 x50 . (x40 x50False)x16 x50(x10 x49False)x16 x49x10 (x2 x50 x49)False)(∀ x49 x50 . (x40 x50False)x16 x50(x40 x49False)x16 x49x40 (x7 x50 x49)False)(∀ x49 x50 . (x10 x50False)x16 x50(x10 x49False)x16 x49x40 (x7 x50 x49)False)(∀ x49 x50 . (x10 x50False)x16 x50(x40 x49False)x16 x49x10 (x7 x49 x50)False)(∀ x49 x50 . (x10 x50False)x16 x50(x40 x49False)x16 x49x10 (x7 x50 x49)False)(∀ x49 x50 . x40 x50x16 x50(x40 x49False)x16 x49(x10 (x5 x49 x50)False)False)(∀ x49 x50 . x40 x50x16 x50(x40 x49False)x16 x49(x40 (x5 x50 x49)False)False)(∀ x49 x50 . x10 x50x16 x50(x10 x49False)x16 x49(x40 (x5 x49 x50)False)False)((x48 x47False)False)(∀ x49 x50 . x10 x50x16 x50(x10 x49False)x16 x49(x10 (x5 x50 x49)False)False)(∀ x49 x50 . (x40 x50False)x16 x50(x10 x49False)x16 x49x10 (x5 x49 x50)False)(∀ x49 x50 . (x40 x50False)x16 x50(x10 x49False)x16 x49x40 (x5 x50 x49)False)(∀ x49 . (x40 x49False)x16 x49x10 (x44 x49)False)(∀ x49 . (x40 x49False)x16 x49(x1 (x44 x49)False)False)(∀ x49 . (x10 x49False)x16 x49x40 (x44 x49)False)(∀ x49 . (x10 x49False)x16 x49(x1 (x44 x49)False)False)(∀ x49 x50 . (x48 x50False)(x48 x49False)x45 x49 (x46 x50)(x41 (x25 x49 x50) x50 x49False)False)(∀ x49 . (x45 (x30 x49) x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x45 x49 (x46 x51)x41 x50 x51 x49(x45 x50 x51False)False)((x41 x4 x43 x9False)False)((x45 x9 (x46 x43)False)False)(∀ x49 . x1 x49(x1 (x44 x49)False)False)(∀ x49 x50 . x1 x50x1 x49(x7 x50 x49 = x7 x49 x50False)False)(∀ x49 . x48 x49(x29 x49False)False)(∀ x49 . x14 x49(x10 x49False)(x40 x49False)(x14 x49False)False)(∀ x49 . x14 x49(x10 x49False)(x40 x49False)(x48 x49False)False)(∀ x49 . x45 x49 x8(x12 x49False)False)(∀ x49 . x48 x49x14 x49x40 x49False)(∀ x49 . x48 x49x14 x49x10 x49False)(∀ x49 . x48 x49x14 x49(x14 x49False)False)(∀ x49 . x48 x49(x12 x49False)False)(∀ x49 . (x48 x49False)x14 x49(x10 x49False)(x40 x49False)False)(∀ x49 . (x48 x49False)x14 x49(x10 x49False)(x14 x49False)False)(∀ x49 . x12 x49(x19 x49False)False)(∀ x49 . x14 x49x40 x49x10 x49False)(∀ x49 . x14 x49x40 x49(x14 x49False)False)(∀ x49 . x14 x49x40 x49x48 x49False)(∀ x49 x50 . x19 x50x45 x49 x50(x19 x49False)False)(∀ x49 . (x48 x49False)x14 x49(x40 x49False)(x10 x49False)False)(∀ x49 . (x48 x49False)x14 x49(x40 x49False)(x14 x49False)False)(∀ x49 . x16 x49(x14 x49False)False)(∀ x49 . x48 x49(x28 x49False)False)(∀ x49 . x14 x49x10 x49x40 x49False)(∀ x49 . x14 x49x10 x49(x14 x49False)False)(∀ x49 . x14 x49x10 x49x48 x49False)(∀ x49 . x16 x49(x1 x49False)False)(∀ x49 . x48 x49(x19 x49False)False)(∀ x49 . x12 x49(x14 x49False)False)(∀ x49 . x12 x49(x16 x49False)False)(∀ x49 . x12 x49(x1 x49False)False)(∀ x49 . x21 x49x33 x49(x19 x49False)False)(∀ x49 . x45 x49 x43(x16 x49False)False)(∀ x49 . x45 x49 x43(x1 x49False)False)(∀ x49 . x19 x49(x33 x49False)False)(∀ x49 . x19 x49(x21 x49False)False)(∀ x49 x50 . x29 x50x45 x49 (x46 x50)(x29 x49False)False)(∀ x49 x50 . x0 x49 x50x0 x50 x49False)(x27 = x44 x3False)(x26 = x4False)((x2 x26 x27 = x44 x26False)False)((x1 x27False)False)((x1 x26False)False)False
type
prop
theory
HotG
name
-
proof
PUSp9..
Megalodon
-
proofgold address
TMdBb..
creator
35123 PrPhD../cc9b2..
owner
35125 PrPhD../2fad5..
term root
a5ec5..