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 . x43 x45(x45 = x44False)x43 x44False)(∀ x44 x45 . x0 x44 x45x43 x45False)(∀ x44 . x43 x44(x44 = x42False)False)(∀ x44 x45 x46 . x1 x46x6 x46x0 (x4 x44 x45) (x5 (x2 x46))(x3 (x2 x46) x44 x45 = x3 x46 x45 x44False)False)(∀ x44 x45 x46 . x1 x46x6 x46x0 (x4 x45 x44) (x5 (x2 x46))(x0 (x4 x44 x45) (x5 x46)False)False)(∀ x44 x45 x46 . x1 x46x6 x46x0 (x4 x45 x44) (x5 x46)(x0 (x4 x44 x45) (x5 (x2 x46))False)False)(∀ x44 x45 x46 x47 . x1 x47x6 x47x1 x46x6 x46x0 x45 (x5 x47)x46 = x39 x47 x45x0 x44 (x5 x46)(x0 (x39 x46 x44) (x41 (x40 x47))False)False)(∀ x44 x45 x46 x47 . x1 x47x6 x47x1 x46x6 x46x0 x45 (x5 x47)x46 = x39 x47 x45x0 x44 (x5 x46)(x3 (x40 x47) x45 x44 = x39 x46 x44False)False)(∀ x44 x45 x46 x47 . x1 x47x6 x47x1 x46x6 x46x0 x45 (x5 x47)x46 = x39 x47 x45x0 x44 (x5 x46)(x0 (x4 x45 x44) (x5 (x40 x47))False)False)(∀ x44 x45 . x7 x44 x45(x43 x45False)(x0 x44 x45False)False)(∀ x44 x45 . x0 x45 x44(x7 x45 x44False)False)((x8 x9False)False)(x43 x9False)(x10 x11False)((x6 x11False)False)((x1 x11False)False)((x6 x38False)False)((x12 x38False)False)((x1 x38False)False)(x43 x38False)((x6 x37False)False)((x12 x37False)False)((x1 x37False)False)(x43 x13False)((x12 x36False)False)((x1 x36False)False)((x35 x34False)False)((x6 x34False)False)((x1 x34False)False)((x14 x15False)False)((x43 x33False)False)((x1 x16False)False)(x43 x16False)((x6 x17False)False)((x1 x17False)False)(∀ x44 . (x43 x44False)x1 x44x43 (x41 x44)False)(∀ x44 . (x43 x44False)x1 x44x43 (x5 x44)False)(∀ x44 x45 x46 x47 . (x1 (x18 (x4 x45 x44) (x4 x47 x46))False)False)(∀ x44 . x43 x44(x43 (x41 x44)False)False)(∀ x44 x45 . (x1 (x19 (x4 x45 x44))False)False)(∀ x44 . x43 x44(x43 (x5 x44)False)False)(∀ x44 x45 . x43 (x18 x44 x45)False)(∀ x44 . x43 (x19 x44)False)(∀ x44 . x20 x44x1 x44(x20 (x41 x44)False)False)(∀ x44 . x20 x44x1 x44(x20 (x5 x44)False)False)(∀ x44 x45 . (x14 (x4 x44 x45)False)False)((x43 x42False)False)(∀ x44 x45 . (x6 (x19 (x4 x45 x44))False)False)(∀ x44 x45 . x1 x45x32 x45x6 x45(x43 (x39 x45 x44)False)False)(∀ x44 . (x20 x44False)x1 x44x6 x44x20 (x5 x44)False)(∀ x44 x45 . x1 x45x6 x45x1 x44x6 x44(x8 (x18 x45 x44)False)False)(∀ x44 . x1 x44x6 x44(x8 (x19 x44)False)False)(∀ x44 . x1 x44x6 x44(x10 x44False)x20 (x41 x44)False)(∀ x44 . x1 x44x6 x44x10 x44(x20 (x41 x44)False)False)(∀ x44 . x43 x44(x43 (x41 x44)False)False)(∀ x44 x45 . (x43 x45False)x1 x45x12 x45x6 x45x7 x44 (x5 x45)x43 (x39 x45 x44)False)(∀ x44 . x43 x44(x43 (x5 x44)False)False)(∀ x44 . x1 x44x12 x44x6 x44(x21 (x41 x44)False)False)(∀ x44 . (x7 (x31 x44) x44False)False)((x43 x22False)False)(∀ x44 . x1 x44x6 x44(x6 (x30 x44)False)False)(∀ x44 . x1 x44x6 x44(x1 (x30 x44)False)False)(∀ x44 . x1 x44x6 x44(x6 (x40 x44)False)False)(∀ x44 . x1 x44x6 x44(x1 (x40 x44)False)False)(∀ x44 . x1 x44x6 x44(x6 (x2 x44)False)False)(∀ x44 . x1 x44x6 x44(x1 (x2 x44)False)False)(∀ x44 x45 . (x4 x45 x44 = x18 (x18 x45 x44) (x19 x45)False)False)(∀ x44 . x1 x44x6 x44(x30 x44 = x2 (x40 x44)False)False)(∀ x44 x45 . x1 x45x6 x45(x29 x44 x45 = x39 x45 (x28 x44 x45)False)(x0 (x29 x44 x45) x44False)(x44 = x41 x45False)False)(∀ x44 x45 . x1 x45x6 x45(x0 (x28 x44 x45) (x5 x45)False)(x0 (x29 x44 x45) x44False)(x44 = x41 x45False)False)(∀ x44 x45 x46 . x1 x46x6 x46x0 (x29 x45 x46) x45x0 x44 (x5 x46)x29 x45 x46 = x39 x46 x44(x45 = x41 x46False)False)(∀ x44 x45 x46 x47 . x1 x47x6 x47x46 = x41 x47x0 x44 (x5 x47)x45 = x39 x47 x44(x0 x45 x46False)False)(∀ x44 x45 x46 . x1 x46x6 x46x45 = x41 x46x0 x44 x45(x44 = x39 x46 (x27 x44 x45 x46)False)False)(∀ x44 x45 x46 . x1 x46x6 x46x45 = x41 x46x0 x44 x45(x0 (x27 x44 x45 x46) (x5 x46)False)False)((x42 = x22False)False)(∀ x44 x45 x46 . x1 x46x6 x46(x3 x46 x44 x45 = x39 x46 (x4 x44 x45)False)False)(∀ x44 x45 . (x18 x45 x44 = x18 x44 x45False)False)(∀ x44 x45 . x8 x45x7 x44 x45(x6 x44False)False)(∀ x44 x45 . x8 x45x7 x44 x45(x1 x44False)False)(∀ x44 . x43 x44(x8 x44False)False)(∀ x44 . x20 x44x1 x44x6 x44(x10 x44False)False)(∀ x44 . x20 x44x1 x44x6 x44(x6 x44False)False)(∀ x44 . x20 x44x1 x44x6 x44(x1 x44False)False)(∀ x44 . x1 x44x6 x44(x10 x44False)(x6 x44False)False)(∀ x44 . x1 x44x6 x44(x10 x44False)(x1 x44False)False)(∀ x44 . x1 x44x6 x44(x10 x44False)x20 x44False)(∀ x44 . x43 x44x1 x44(x12 x44False)False)(∀ x44 . x43 x44x1 x44(x1 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x10 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x6 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x1 x44False)False)(∀ x44 . x43 x44x1 x44(x32 x44False)False)(∀ x44 . x43 x44x1 x44(x1 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x35 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x6 x44False)False)(∀ x44 . x43 x44x1 x44x6 x44(x1 x44False)False)(∀ x44 . x43 x44(x1 x44False)False)(∀ x44 . x43 x44(x6 x44False)False)(∀ x44 x45 . x0 x44 x45x0 x45 x44False)(x0 (x4 x23 x26) (x5 (x30 x25))x3 (x30 x25) x23 x26 = x39 x24 x23x0 (x39 x24 x23) (x41 (x30 x25))False)((x0 x23 (x5 x24)False)False)((x24 = x39 x25 x26False)False)((x0 x26 (x5 x25)False)False)((x6 x24False)False)((x1 x24False)False)((x6 x25False)False)((x1 x25False)False)False
type
prop
theory
HotG
name
-
proof
PUaZC..
Megalodon
-
proofgold address
TMStg..
creator
35129 PrPhD../a33c9..
owner
35137 PrPhD../2333f..
term root
f7e77..