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 . x53 x55x53 x54(x52 x55 x54False)(x51 x54False)(x50 x55False)False)(∀ x54 x55 . x0 x55(x55 = x54False)x0 x54False)(∀ x54 x55 . x53 x55x53 x54(x52 x55 x54False)(x50 x55False)(x51 x54False)False)(∀ x54 x55 . x1 x54 x55x0 x55False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54(x0 x55False)(x50 x54False)(x51 x55False)False)(∀ x54 . x0 x54(x54 = x2False)False)(∀ x54 x55 x56 . x1 x54 x55x48 x55 (x49 x56)x0 x56False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54(x0 x54False)(x51 x55False)(x50 x54False)False)(∀ x54 x55 x56 . x1 x55 x56x48 x56 (x49 x54)(x48 x55 x54False)False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54(x50 x54False)x50 x55False)(∀ x54 x55 . x47 x55 x54(x48 x55 (x49 x54)False)False)(∀ x54 x55 . x48 x55 (x49 x54)(x47 x55 x54False)False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54(x51 x55False)x51 x54False)(∀ x54 . x3 x54(x4 x5 x54 = x54False)False)(∀ x54 x55 . x48 x54 x55(x0 x55False)(x1 x54 x55False)False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54x51 x54(x51 x55False)False)(∀ x54 x55 . x1 x55 x54(x48 x55 x54False)False)(∀ x54 x55 . x53 x55x53 x54x52 x55 x54x50 x55(x50 x54False)False)((x48 x2 x46False)False)(∀ x54 x55 . x3 x55x3 x54(x7 (x6 x55) (x6 x54) = x7 x54 x55False)False)(∀ x54 x55 . x3 x55x3 x54(x45 (x6 x55) (x6 x54) = x6 (x45 x55 x54)False)False)(∀ x54 x55 x56 . x3 x56x3 x54x3 x55(x4 (x4 x56 x54) x55 = x4 x56 (x4 x54 x55)False)False)(∀ x54 x55 x56 . x3 x56x3 x54x3 x55(x45 (x45 x56 x54) x55 = x45 x56 (x45 x54 x55)False)False)(∀ x54 x55 x56 . x3 x56x3 x54x3 x55(x4 (x45 x56 x54) x55 = x45 (x4 x56 x55) (x4 x54 x55)False)False)((x48 x43 x44False)False)((x48 x43 x8False)False)((x42 x43 x44 x8False)False)((x50 x43False)False)(x0 x43False)(∀ x54 . x3 x54(x4 x54 (x6 x5) = x6 x54False)False)((x48 x5 x44False)False)((x48 x5 x8False)False)((x42 x5 x44 x8False)False)((x50 x5False)False)(x0 x5False)(∀ x54 x55 . x3 x55x3 x54(x45 x55 (x6 x54) = x7 x55 x54False)False)((x48 x41 x44False)False)((x48 x41 x8False)False)((x42 x41 x44 x8False)False)((x0 x41False)False)((x6 (x6 x43) = x43False)False)((x6 (x6 x5) = x5False)False)((x6 x43 = x6 x43False)False)((x6 x5 = x6 x5False)False)((x6 x41 = x41False)False)((x4 (x6 x43) x5 = x6 x43False)False)((x4 (x6 x43) x41 = x41False)False)((x4 x43 x5 = x43False)False)((x4 x43 x41 = x41False)False)((x4 x5 (x6 x43) = x6 x43False)False)((x4 x5 x43 = x43False)False)((x4 x5 x5 = x5False)False)((x4 x5 x41 = x41False)False)((x4 x41 (x6 x43) = x41False)False)((x4 x41 x43 = x41False)False)((x4 x41 x5 = x41False)False)((x4 x41 x41 = x41False)False)((x7 (x6 x43) (x6 x43) = x41False)False)((x7 (x6 x43) (x6 x5) = x6 x5False)False)((x7 (x6 x43) x41 = x6 x43False)False)((x7 (x6 x5) (x6 x43) = x5False)False)((x7 (x6 x5) (x6 x5) = x41False)False)((x7 (x6 x5) x5 = x6 x43False)False)((x7 (x6 x5) x41 = x6 x5False)False)((x7 x43 x43 = x41False)False)((x7 x43 x5 = x5False)False)((x7 x43 x41 = x43False)False)((x7 x5 (x6 x5) = x43False)False)((x7 x5 x43 = x6 x5False)False)((x7 x5 x5 = x41False)False)((x7 x5 x41 = x5False)False)((x7 x41 (x6 x43) = x43False)False)((x7 x41 (x6 x5) = x5False)False)((x7 x41 x43 = x6 x43False)False)((x7 x41 x5 = x6 x5False)False)((x7 x41 x41 = x41False)False)((x45 (x6 x43) x43 = x41False)False)((x45 (x6 x43) x5 = x6 x5False)False)((x45 (x6 x5) (x6 x5) = x6 x43False)False)((x45 (x6 x5) x43 = x5False)False)((x45 (x6 x5) x5 = x41False)False)((x45 (x6 x5) x41 = x6 x5False)False)((x45 x43 (x6 x43) = x41False)False)((x45 x43 (x6 x5) = x5False)False)((x45 x43 x41 = x43False)False)((x45 x5 (x6 x43) = x6 x5False)False)((x45 x5 (x6 x5) = x41False)False)((x45 x5 x5 = x43False)False)((x45 x5 x41 = x5False)False)((x45 x41 (x6 x43) = x6 x43False)False)((x45 x41 (x6 x5) = x6 x5False)False)((x45 x41 x43 = x43False)False)((x45 x41 x5 = x5False)False)((x45 x41 x41 = x41False)False)((x52 (x6 x43) (x6 x43)False)False)((x52 (x6 x43) (x6 x5)False)False)((x52 (x6 x43) x43False)False)((x52 (x6 x43) x5False)False)((x52 (x6 x43) x41False)False)(x52 (x6 x5) (x6 x43)False)((x52 (x6 x5) (x6 x5)False)False)((x52 (x6 x5) x43False)False)((x52 (x6 x5) x5False)False)((x52 (x6 x5) x41False)False)(x52 x43 (x6 x43)False)(x52 x43 (x6 x5)False)((x52 x43 x43False)False)(x52 x43 x5False)(x52 x43 x41False)(x52 x5 (x6 x43)False)(x52 x5 (x6 x5)False)((x52 x5 x43False)False)((x52 x5 x5False)False)(x52 x5 x41False)(x52 x41 (x6 x43)False)(x52 x41 (x6 x5)False)((x52 x41 x43False)False)((x52 x41 x5False)False)((x52 x41 x41False)False)(∀ x54 x55 . x9 x55x9 x54(x52 x55 x55False)False)(∀ x54 . (x47 x54 x54False)False)(∀ x54 x55 x56 . (x0 x56False)(x0 x54False)x48 x54 (x49 x56)x48 x55 x54(x42 x55 x56 x54False)False)(∀ x54 x55 x56 . (x0 x56False)(x0 x54False)x48 x54 (x49 x56)x42 x55 x56 x54(x48 x55 x54False)False)((x8 = x46False)False)(∀ x54 . x40 x54(x39 x54 = x6 x54False)False)(∀ x54 x55 . x53 x55x53 x54(x10 x55 x54 = x4 x55 x54False)False)((x9 x38False)False)((x0 x38False)False)((x53 x37False)False)((x9 x37False)False)((x3 x37False)False)((x0 x37False)False)((x51 x36False)False)((x9 x36False)False)((x53 x35False)False)((x51 x35False)False)((x9 x35False)False)((x3 x35False)False)((x34 x33False)False)((x11 x33False)False)(x0 x33False)((x50 x12False)False)((x9 x12False)False)((x53 x13False)False)((x50 x13False)False)((x9 x13False)False)((x3 x13False)False)(x0 x14False)((x11 x32False)False)(x0 x32False)((x9 x31False)False)((x53 x15False)False)((x0 x30False)False)((x11 x16False)False)(x0 x16False)(∀ x54 x55 . x53 x55x53 x54(x52 x5 (x17 x55)False)(x52 x5 x54False)x52 x5 (x10 (x17 x55) x54)False)(∀ x54 . x3 x54(x6 (x6 x54) = x54False)False)(∀ x54 . x40 x54(x39 (x39 x54) = x54False)False)(∀ x54 x55 . (x51 x55False)x53 x55(x51 x54False)x53 x54x51 (x45 x55 x54)False)(∀ x54 x55 . x53 x55x53 x54(x53 (x7 x55 x54)False)False)(∀ x54 x55 . x53 x55x53 x54(x53 (x4 x55 x54)False)False)((x11 x46False)False)(∀ x54 x55 . x53 x55x53 x54(x53 (x45 x55 x54)False)False)((x18 x19False)False)((x34 x46False)False)((x34 x19False)False)((x34 x44False)False)(∀ x54 . x53 x54(x53 (x6 x54)False)False)(∀ x54 . x53 x54(x3 (x6 x54)False)False)((x20 x44False)False)(∀ x54 . x53 x54(x53 (x17 x54)False)False)(∀ x54 x55 . (x51 x55False)x53 x55(x51 x54False)x53 x54x51 (x4 x55 x54)False)(∀ x54 x55 . (x50 x55False)x53 x55(x50 x54False)x53 x54x51 (x4 x55 x54)False)(∀ x54 x55 . (x50 x55False)x53 x55(x51 x54False)x53 x54x50 (x4 x54 x55)False)(∀ x54 x55 . (x50 x55False)x53 x55(x51 x54False)x53 x54x50 (x4 x55 x54)False)(∀ x54 x55 . x51 x55x53 x55(x51 x54False)x53 x54(x50 (x7 x54 x55)False)False)(∀ x54 x55 . x51 x55x53 x55(x51 x54False)x53 x54(x51 (x7 x55 x54)False)False)(∀ x54 x55 . x50 x55x53 x55(x50 x54False)x53 x54(x51 (x7 x54 x55)False)False)((x0 x2False)False)(∀ x54 . x3 x54(x3 (x17 x54)False)False)(∀ x54 x55 . x50 x55x53 x55(x50 x54False)x53 x54(x50 (x7 x55 x54)False)False)(∀ x54 x55 . (x51 x55False)x53 x55(x50 x54False)x53 x54x50 (x7 x54 x55)False)(∀ x54 x55 . (x51 x55False)x53 x55(x50 x54False)x53 x54x51 (x7 x55 x54)False)(∀ x54 . (x51 x54False)x53 x54x50 (x6 x54)False)(∀ x54 . (x51 x54False)x53 x54(x3 (x6 x54)False)False)(∀ x54 . (x50 x54False)x53 x54x51 (x6 x54)False)(∀ x54 . (x50 x54False)x53 x54(x3 (x6 x54)False)False)(∀ x54 x55 . x51 x55x53 x55(x50 x54False)x53 x54(x51 (x45 x54 x55)False)False)(∀ x54 x55 . x51 x55x53 x55(x50 x54False)x53 x54(x51 (x45 x55 x54)False)False)(∀ x54 x55 . x50 x55x53 x55(x51 x54False)x53 x54(x50 (x45 x54 x55)False)False)(∀ x54 x55 . x50 x55x53 x55(x51 x54False)x53 x54(x50 (x45 x55 x54)False)False)(∀ x54 x55 . (x50 x55False)x53 x55(x50 x54False)x53 x54x50 (x45 x55 x54)False)(∀ x54 x55 . (x0 x55False)(x0 x54False)x48 x54 (x49 x55)(x42 (x29 x54 x55) x55 x54False)False)(∀ x54 . (x48 (x21 x54) x54False)False)(∀ x54 x55 x56 . (x0 x56False)(x0 x54False)x48 x54 (x49 x56)x42 x55 x56 x54(x48 x55 x56False)False)((x48 x8 (x49 x44)False)False)(∀ x54 . x3 x54(x3 (x6 x54)False)False)(∀ x54 . x40 x54(x48 (x39 x54) x19False)False)(∀ x54 x55 . x53 x55x53 x54(x48 (x10 x55 x54) x44False)False)(∀ x54 x55 . x3 x55x3 x54(x7 x55 x54 = x45 x55 (x6 x54)False)False)(∀ x54 . x3 x54(x17 x54 = x4 x54 x54False)False)(∀ x54 x55 . x9 x55x9 x54(x52 x55 x54False)(x52 x54 x55False)False)(∀ x54 x55 . x3 x55x3 x54(x4 x55 x54 = x4 x54 x55False)False)(∀ x54 x55 . x3 x55x3 x54(x45 x55 x54 = x45 x54 x55False)False)(∀ x54 x55 . x53 x55x53 x54(x10 x55 x54 = x10 x54 x55False)False)(∀ x54 . x9 x54(x50 x54False)(x51 x54False)(x9 x54False)False)(∀ x54 . x9 x54(x50 x54False)(x51 x54False)(x0 x54False)False)(∀ x54 . x48 x54 (x49 x44)(x20 x54False)False)(∀ x54 . x0 x54x9 x54x51 x54False)(∀ x54 . x0 x54x9 x54x50 x54False)(∀ x54 . x0 x54x9 x54(x9 x54False)False)(∀ x54 . (x0 x54False)x9 x54(x50 x54False)(x51 x54False)False)(∀ x54 . (x0 x54False)x9 x54(x50 x54False)(x9 x54False)False)(∀ x54 . x9 x54x51 x54x50 x54False)(∀ x54 . x9 x54x51 x54(x9 x54False)False)(∀ x54 . x9 x54x51 x54x0 x54False)(∀ x54 . x20 x54(x28 x54False)False)(∀ x54 . (x0 x54False)x9 x54(x51 x54False)(x50 x54False)False)(∀ x54 . (x0 x54False)x9 x54(x51 x54False)(x9 x54False)False)(∀ x54 . x53 x54(x9 x54False)False)(∀ x54 . x20 x54(x27 x54False)False)(∀ x54 . x9 x54x50 x54x51 x54False)(∀ x54 . x9 x54x50 x54(x9 x54False)False)(∀ x54 . x9 x54x50 x54x0 x54False)(∀ x54 . x53 x54(x3 x54False)False)(∀ x54 . x22 x54(x20 x54False)False)(∀ x54 . x26 x54(x9 x54False)False)(∀ x54 . x26 x54(x53 x54False)False)(∀ x54 . x18 x54(x22 x54False)False)(∀ x54 . x0 x54(x34 x54False)False)(∀ x54 . x48 x54 x8(x11 x54False)False)(∀ x54 x55 . x11 x55x48 x54 (x49 x55)(x11 x54False)False)(∀ x54 x55 . x18 x55x48 x54 (x49 x55)(x18 x54False)False)(∀ x54 x55 . x22 x55x48 x54 (x49 x55)(x22 x54False)False)(∀ x54 x55 . x20 x55x48 x54 (x49 x55)(x20 x54False)False)(∀ x54 x55 . x27 x55x48 x54 (x49 x55)(x27 x54False)False)(∀ x54 . x48 x54 x44(x53 x54False)False)(∀ x54 . x11 x54(x18 x54False)False)(∀ x54 x55 . x28 x55x48 x54 (x49 x55)(x28 x54False)False)(∀ x54 . x0 x54(x11 x54False)False)(∀ x54 x55 . x11 x55x48 x54 x55(x26 x54False)False)(∀ x54 x55 . x18 x55x48 x54 x55(x40 x54False)False)(∀ x54 x55 . x22 x55x48 x54 x55(x25 x54False)False)(∀ x54 x55 . x20 x55x48 x54 x55(x53 x54False)False)(∀ x54 x55 . x27 x55x48 x54 x55(x9 x54False)False)(∀ x54 x55 . x28 x55x48 x54 x55(x3 x54False)False)(∀ x54 . x48 x54 (x49 x8)(x11 x54False)False)(∀ x54 . x48 x54 (x49 x19)(x18 x54False)False)(∀ x54 x55 . x1 x54 x55x1 x55 x54False)((x10 x23 x24 = x39 x5False)False)(x52 x5 (x17 x24)False)(x52 x5 (x17 x23)False)((x53 x24False)False)((x53 x23False)False)False
type
prop
theory
HotG
name
-
proof
PUfby..
Megalodon
-
proofgold address
TMWAG..
creator
35129 PrPhD../f94ed..
owner
35137 PrPhD../76965..
term root
77b98..