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 . x0 x44 x45x2 x45 (x1 x46)x43 x46False)(∀ x44 x45 x46 . x0 x45 x46x2 x46 (x1 x44)(x2 x45 x44False)False)(∀ x44 x45 . x3 x45 x44(x2 x45 (x1 x44)False)False)(∀ x44 x45 . x2 x45 (x1 x44)(x3 x45 x44False)False)(∀ x44 x45 . x2 x44 x45(x43 x45False)(x0 x44 x45False)False)(∀ x44 x45 x46 . x3 x45 x46x3 x46 x44(x3 x45 x44False)False)(∀ x44 x45 . x0 x45 x44(x2 x45 x44False)False)(∀ x44 . (x3 x44 x44False)False)((x4 x5False)False)(x43 x5False)(∀ x44 . (x6 x44False)x6 (x7 x44)False)(∀ x44 . (x6 x44False)(x2 (x7 x44) (x1 x44)False)False)(∀ x44 . (x43 x44False)(x6 (x8 x44)False)False)(∀ x44 . (x43 x44False)x43 (x8 x44)False)(∀ x44 . (x43 x44False)(x2 (x8 x44) (x1 x44)False)False)(x41 x40False)((x9 x40False)False)((x39 x40False)False)(∀ x44 . (x43 x44False)(x11 (x10 x44) x44False)False)(∀ x44 . (x43 x44False)(x2 (x10 x44) (x1 x44)False)False)((x9 x12False)False)((x38 x12False)False)((x39 x12False)False)(x43 x12False)(∀ x44 . x11 (x13 x44) x44False)(∀ x44 . (x2 (x13 x44) (x1 x44)False)False)((x9 x14False)False)((x38 x14False)False)((x39 x14False)False)(x43 x37False)(∀ x44 . (x43 (x15 x44)False)False)(∀ x44 . (x2 (x15 x44) (x1 x44)False)False)((x38 x16False)False)((x39 x16False)False)((x17 x18False)False)((x9 x18False)False)((x39 x18False)False)((x43 x36False)False)(∀ x44 . (x43 x44False)x43 (x19 x44)False)(∀ x44 . (x43 x44False)(x2 (x19 x44) (x1 x44)False)False)((x39 x20False)False)(x43 x20False)((x9 x21False)False)((x39 x21False)False)(∀ x44 . (x43 x44False)x39 x44x43 (x22 x44)False)(∀ x44 . (x43 x44False)x39 x44x43 (x35 x44)False)(∀ x44 . x43 x44(x43 (x22 x44)False)False)(∀ x44 . x43 x44(x43 (x35 x44)False)False)(∀ x44 . x6 x44x39 x44(x6 (x22 x44)False)False)(∀ x44 . x6 x44x39 x44(x6 (x35 x44)False)False)((x43 x42False)False)(∀ x44 . x43 (x1 x44)False)(∀ x44 . (x6 x44False)x39 x44x9 x44x6 (x35 x44)False)(∀ x44 . x39 x44x9 x44(x41 x44False)x6 (x22 x44)False)(∀ x44 . x39 x44x9 x44x41 x44(x6 (x22 x44)False)False)(∀ x44 . x43 x44(x43 (x22 x44)False)False)(∀ x44 . x43 x44(x43 (x35 x44)False)False)(∀ x44 . x39 x44x38 x44x9 x44(x34 (x22 x44)False)False)(∀ x44 . (x2 (x23 x44) x44False)False)((x43 x33False)False)(∀ x44 x45 . x0 (x24 x44 x45) x44(x3 x45 x44False)False)(∀ x44 x45 . (x0 (x24 x44 x45) x45False)(x3 x45 x44False)False)(∀ x44 x45 x46 . x3 x45 x46x0 x44 x45(x0 x44 x46False)False)((x42 = x33False)False)(∀ x44 x45 x46 . (x3 (x22 (x27 x44 x45 x46)) x45False)(x0 (x26 x44 x45 x46) x44False)(x44 = x25 x46 x45False)False)(∀ x44 x45 x46 . (x35 (x27 x44 x45 x46) = x46False)(x0 (x26 x44 x45 x46) x44False)(x44 = x25 x46 x45False)False)(∀ x44 x45 x46 . (x26 x44 x45 x46 = x27 x44 x45 x46False)(x0 (x26 x44 x45 x46) x44False)(x44 = x25 x46 x45False)False)(∀ x44 x45 x46 . (x9 (x27 x44 x45 x46)False)(x0 (x26 x44 x45 x46) x44False)(x44 = x25 x46 x45False)False)(∀ x44 x45 x46 . (x39 (x27 x44 x45 x46)False)(x0 (x26 x44 x45 x46) x44False)(x44 = x25 x46 x45False)False)(∀ x44 x45 x46 x47 . x0 (x26 x47 x45 x46) x47x39 x44x9 x44x26 x47 x45 x46 = x44x35 x44 = x46x3 (x22 x44) x45(x47 = x25 x46 x45False)False)(∀ x44 x45 x46 x47 x48 . x48 = x25 x46 x47x39 x44x9 x44x45 = x44x35 x44 = x46x3 (x22 x44) x47(x0 x45 x48False)False)(∀ x44 x45 x46 x47 . x47 = x25 x45 x46x0 x44 x47(x3 (x22 (x32 x44 x47 x46 x45)) x46False)False)(∀ x44 x45 x46 x47 . x47 = x25 x45 x46x0 x44 x47(x35 (x32 x44 x47 x46 x45) = x45False)False)(∀ x44 x45 x46 x47 . x47 = x25 x45 x46x0 x44 x47(x44 = x32 x44 x47 x46 x45False)False)(∀ x44 x45 x46 x47 . x47 = x25 x45 x46x0 x44 x47(x9 (x32 x44 x47 x46 x45)False)False)(∀ x44 x45 x46 x47 . x47 = x25 x45 x46x0 x44 x47(x39 (x32 x44 x47 x46 x45)False)False)(∀ x44 x45 . x4 x45x2 x44 (x1 x45)(x4 x44False)False)(∀ x44 x45 . x4 x45x2 x44 x45(x9 x44False)False)(∀ x44 x45 . x4 x45x2 x44 x45(x39 x44False)False)(∀ x44 . x43 x44(x4 x44False)False)(∀ x44 . x6 x44x39 x44x9 x44(x41 x44False)False)(∀ x44 . x6 x44x39 x44x9 x44(x9 x44False)False)(∀ x44 . x6 x44x39 x44x9 x44(x39 x44False)False)(∀ x44 x45 . x6 x45x2 x44 (x1 x45)(x6 x44False)False)(∀ x44 . x39 x44x9 x44(x41 x44False)(x9 x44False)False)(∀ x44 . x39 x44x9 x44(x41 x44False)(x39 x44False)False)(∀ x44 . x39 x44x9 x44(x41 x44False)x6 x44False)(∀ x44 x45 . x43 x45x2 x44 (x1 x45)x11 x44 x45False)(∀ x44 . x43 x44x39 x44(x38 x44False)False)(∀ x44 . x43 x44x39 x44(x39 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x41 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x9 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x39 x44False)False)(∀ x44 x45 . (x43 x45False)x2 x44 (x1 x45)x43 x44(x11 x44 x45False)False)(∀ x44 . x43 x44x39 x44(x28 x44False)False)(∀ x44 . x43 x44x39 x44(x39 x44False)False)(∀ x44 x45 . x39 x45x9 x45x2 x44 (x1 x45)(x9 x44False)False)(∀ x44 x45 . (x43 x45False)x2 x44 (x1 x45)(x11 x44 x45False)x43 x44False)(∀ x44 x45 . x39 x45x2 x44 (x1 x45)(x39 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x17 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x9 x44False)False)(∀ x44 . x43 x44x39 x44x9 x44(x39 x44False)False)(∀ x44 x45 . x43 x45x2 x44 (x1 x45)(x43 x44False)False)(∀ x44 . x43 x44(x39 x44False)False)(∀ x44 . x43 x44(x9 x44False)False)(∀ x44 x45 . x0 x44 x45x0 x45 x44False)(x3 (x25 x31 x29) (x25 x31 x30)False)((x3 x29 x30False)False)False
type
prop
theory
HotG
name
-
proof
PUhRx..
Megalodon
-
proofgold address
TMHDm..
creator
35132 PrPhD../14883..
owner
35137 PrPhD../56f65..
term root
ad38d..