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 . x41 x43(x43 = x42False)x41 x42False)(∀ x42 x43 . x0 x42 x43x41 x43False)(∀ x42 . x41 x42(x42 = x40False)False)(∀ x42 x43 . x1 x42 x43(x41 x43False)(x0 x42 x43False)False)(∀ x42 . (x39 x42 x40 = x40False)False)(∀ x42 x43 . x0 x43 x42(x1 x43 x42False)False)((x38 x37False)False)(x41 x37False)(x36 x35False)((x2 x35False)False)((x34 x35False)False)((x2 x3False)False)((x33 x3False)False)((x34 x3False)False)(x41 x3False)((x2 x4False)False)((x33 x4False)False)((x34 x4False)False)(x41 x32False)((x33 x5False)False)((x34 x5False)False)((x6 x7False)False)((x2 x7False)False)((x34 x7False)False)((x31 x30False)False)((x41 x8False)False)((x34 x29False)False)(x41 x29False)((x2 x28False)False)((x34 x28False)False)(∀ x42 . (x39 x42 x42 = x42False)False)(∀ x42 . (x41 x42False)x34 x42x41 (x9 x42)False)(∀ x42 . (x41 x42False)x34 x42x41 (x27 x42)False)(∀ x42 x43 x44 x45 . (x34 (x10 (x11 x43 x42) (x11 x45 x44))False)False)(∀ x42 x43 . (x34 (x26 x42 x43)False)False)(∀ x42 . x41 x42(x41 (x9 x42)False)False)(∀ x42 x43 . (x34 (x25 (x11 x43 x42))False)False)(∀ x42 . x41 x42(x41 (x27 x42)False)False)(∀ x42 x43 . x41 (x10 x42 x43)False)(∀ x42 . x41 (x25 x42)False)(∀ x42 . x24 x42x34 x42(x24 (x9 x42)False)False)(∀ x42 . x24 x42x34 x42(x24 (x27 x42)False)False)(∀ x42 x43 . (x31 (x11 x42 x43)False)False)((x41 x40False)False)(∀ x42 x43 . x34 x43(x34 (x39 x43 x42)False)False)(∀ x42 x43 . (x2 (x25 (x11 x43 x42))False)False)(∀ x42 x43 . x34 x43x22 x43x2 x43(x41 (x23 x43 x42)False)False)(∀ x42 . (x24 x42False)x34 x42x2 x42x24 (x27 x42)False)(∀ x42 x43 . x34 x43x2 x43x34 x42x2 x42(x38 (x10 x43 x42)False)False)(∀ x42 . x34 x42x2 x42(x38 (x25 x42)False)False)(∀ x42 . x34 x42x2 x42(x36 x42False)x24 (x9 x42)False)(∀ x42 . x34 x42x2 x42x36 x42(x24 (x9 x42)False)False)(∀ x42 . x41 x42(x41 (x9 x42)False)False)(∀ x42 x43 . (x41 x43False)x34 x43x33 x43x2 x43x1 x42 (x27 x43)x41 (x23 x43 x42)False)(∀ x42 x43 . (x41 x43False)(x41 x42False)x41 (x26 x43 x42)False)(∀ x42 . x41 x42(x41 (x27 x42)False)False)(∀ x42 . x34 x42x33 x42x2 x42(x21 (x9 x42)False)False)(∀ x42 . (x1 (x12 x42) x42False)False)((x41 x20False)False)(∀ x42 . x34 x42x2 x42(x2 (x13 x42)False)False)(∀ x42 . x34 x42x2 x42(x34 (x13 x42)False)False)(∀ x42 x43 . (x11 x43 x42 = x10 (x10 x43 x42) (x25 x43)False)False)((x40 = x20False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x27 x43 = x27 (x27 x44)x34 x42x2 x42x23 x43 (x16 x43 x44) = x42x27 x42 = x9 (x39 (x27 x44) (x26 (x25 (x16 x43 x44)) (x9 (x27 x44))))x23 x42 (x15 x42 x43 x44) = x14 x44 (x16 x43 x44) (x15 x42 x43 x44)(x43 = x13 x44False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x27 x43 = x27 (x27 x44)x34 x42x2 x42x23 x43 (x16 x43 x44) = x42x27 x42 = x9 (x39 (x27 x44) (x26 (x25 (x16 x43 x44)) (x9 (x27 x44))))(x0 (x15 x42 x43 x44) (x27 x42)False)(x43 = x13 x44False)False)(∀ x42 x43 . x34 x43x2 x43x34 x42x2 x42x27 x42 = x27 (x27 x43)(x0 (x16 x42 x43) (x27 (x27 x43))False)(x42 = x13 x43False)False)(∀ x42 x43 x44 x45 . x34 x45x2 x45x34 x44x2 x44x44 = x13 x45x0 x42 (x27 (x27 x45))x0 x43 (x27 (x19 x42 x44 x45))(x23 (x19 x42 x44 x45) x43 = x14 x45 x42 x43False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x43 = x13 x44x0 x42 (x27 (x27 x44))(x27 (x19 x42 x43 x44) = x9 (x39 (x27 x44) (x26 (x25 x42) (x9 (x27 x44))))False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x43 = x13 x44x0 x42 (x27 (x27 x44))(x23 x43 x42 = x19 x42 x43 x44False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x43 = x13 x44x0 x42 (x27 (x27 x44))(x2 (x19 x42 x43 x44)False)False)(∀ x42 x43 x44 . x34 x44x2 x44x34 x43x2 x43x43 = x13 x44x0 x42 (x27 (x27 x44))(x34 (x19 x42 x43 x44)False)False)(∀ x42 x43 . x34 x43x2 x43x34 x42x2 x42x42 = x13 x43(x27 x42 = x27 (x27 x43)False)False)(∀ x42 x43 x44 . x34 x44x2 x44(x14 x44 x42 x43 = x23 x44 (x11 x42 x43)False)False)(∀ x42 x43 . (x39 x43 x42 = x39 x42 x43False)False)(∀ x42 x43 . (x10 x43 x42 = x10 x42 x43False)False)(∀ x42 x43 . x38 x43x1 x42 x43(x2 x42False)False)(∀ x42 x43 . x38 x43x1 x42 x43(x34 x42False)False)(∀ x42 . x41 x42(x38 x42False)False)(∀ x42 . x24 x42x34 x42x2 x42(x36 x42False)False)(∀ x42 . x24 x42x34 x42x2 x42(x2 x42False)False)(∀ x42 . x24 x42x34 x42x2 x42(x34 x42False)False)(∀ x42 . x34 x42x2 x42(x36 x42False)(x2 x42False)False)(∀ x42 . x34 x42x2 x42(x36 x42False)(x34 x42False)False)(∀ x42 . x34 x42x2 x42(x36 x42False)x24 x42False)(∀ x42 . x41 x42x34 x42(x33 x42False)False)(∀ x42 . x41 x42x34 x42(x34 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x36 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x2 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x34 x42False)False)(∀ x42 . x41 x42x34 x42(x22 x42False)False)(∀ x42 . x41 x42x34 x42(x34 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x6 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x2 x42False)False)(∀ x42 . x41 x42x34 x42x2 x42(x34 x42False)False)(∀ x42 . x41 x42(x34 x42False)False)(∀ x42 . x41 x42(x2 x42False)False)(∀ x42 x43 . x0 x42 x43x0 x43 x42False)(x34 (x23 (x13 x18) x17)x2 (x23 (x13 x18) x17)False)((x0 x17 (x27 (x13 x18))False)False)((x2 x18False)False)((x34 x18False)False)False
type
prop
theory
HotG
name
-
proof
PUKuA..
Megalodon
-
proofgold address
TMTex..
creator
35142 PrPhD../567e2..
owner
35144 PrPhD../a36b4..
term root
e70f5..