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 x56 : ι → ι . ∀ x57 : ι → ι → ο . ∀ x58 : ι → ο . ∀ x59 : ι → ι . ∀ x60 : ι → ι → ο . ∀ x61 : ι → ο . ∀ x62 . ∀ x63 : ι → ο . ∀ x64 . ∀ x65 : ι → ο . (∀ x66 x67 . x65 x67(x67 = x66False)x65 x66False)(∀ x66 x67 . x0 x66 x67x65 x67False)(∀ x66 . x65 x66(x66 = x64False)False)(∀ x66 x67 x68 . x0 x66 x67x2 x67 (x1 x68)x65 x68False)(∀ x66 x67 x68 . x0 x67 x68x2 x68 (x1 x66)(x2 x67 x66False)False)(∀ x66 x67 . x3 x67 x66(x2 x67 (x1 x66)False)False)(∀ x66 x67 . x2 x67 (x1 x66)(x3 x67 x66False)False)(∀ x66 x67 . x2 x66 x67(x65 x67False)(x0 x66 x67False)False)(∀ x66 x67 . x0 x67 x66(x2 x67 x66False)False)(∀ x66 . (x3 x66 x66False)False)((x63 x62False)False)(x65 x62False)(∀ x66 . x61 x66x58 x66(x60 (x59 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x2 (x59 x66) (x1 (x4 x66))False)False)(∀ x66 . x61 x66x58 x66(x57 (x56 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x2 (x56 x66) (x1 (x4 x66))False)False)(∀ x66 . x58 x66(x54 (x55 x66) x66False)False)(∀ x66 . x58 x66(x2 (x55 x66) (x1 (x4 x66))False)False)((x53 x52False)False)((x5 x52False)False)((x51 x52False)False)((x65 x52False)False)(∀ x66 . (x65 x66False)(x49 (x50 x66) x66False)False)(∀ x66 . (x65 x66False)(x2 (x50 x66) (x1 x66)False)False)(∀ x66 . x49 (x48 x66) x66False)(∀ x66 . (x2 (x48 x66) (x1 x66)False)False)((x47 x46False)False)((x6 x46False)False)(x65 x46False)(x65 x7False)(∀ x66 . x61 x66x58 x66(x57 (x45 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x8 (x45 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x2 (x45 x66) (x1 (x4 x66))False)False)(∀ x66 . (x65 (x9 x66)False)False)(∀ x66 . (x2 (x9 x66) (x1 x66)False)False)((x10 x11False)False)((x44 x11False)False)((x6 x12False)False)(x65 x12False)((x53 x13False)False)((x65 x43False)False)(∀ x66 . x61 x66x58 x66(x8 (x14 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x2 (x14 x66) (x1 (x4 x66))False)False)(∀ x66 . (x65 x66False)x65 (x15 x66)False)(∀ x66 . (x65 x66False)(x2 (x15 x66) (x1 x66)False)False)((x44 x16False)False)(x65 x16False)((x6 x17False)False)(x65 x17False)(∀ x66 . x61 x66x58 x66(x8 (x18 x66) x66False)False)(∀ x66 . x61 x66x58 x66(x2 (x18 x66) (x1 (x4 x66))False)False)(∀ x66 x67 . x58 x67x2 x66 (x1 (x4 x67))(x19 x67 (x19 x67 x66) = x19 x67 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x1 (x4 x67)))(x42 x67 (x42 x67 x66) = x42 x67 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))(x8 (x19 x67 x66) x67False)False)((x65 x64False)False)(∀ x66 . x65 (x1 x66)False)(∀ x66 x67 . x58 x67x54 x66 x67x2 x66 (x1 (x4 x67))(x65 (x19 x67 x66)False)False)(∀ x66 . (x2 (x20 x66) x66False)False)((x41 x40False)False)((x58 x21False)False)(∀ x66 . x58 x66(x41 x66False)False)(∀ x66 x67 . x58 x67x2 x66 (x1 (x4 x67))(x2 (x19 x67 x66) (x1 (x4 x67))False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x1 (x4 x67)))(x2 (x42 x67 x66) (x1 (x1 (x4 x67)))False)False)(∀ x66 x67 . x0 (x22 x66 x67) x66(x3 x67 x66False)False)(∀ x66 x67 . (x0 (x22 x66 x67) x67False)(x3 x67 x66False)False)(∀ x66 x67 x68 . x3 x67 x68x0 x66 x67(x0 x66 x68False)False)(∀ x66 x67 x68 . x61 x68x58 x68x2 x67 (x1 (x1 (x4 x68)))x2 x66 (x1 (x1 (x4 x68)))(x0 (x39 x66 x67 x68) x67False)(x0 (x38 x66 x67 x68) x66False)(x66 = x42 x68 x67False)False)(∀ x66 x67 x68 . x61 x68x58 x68x2 x67 (x1 (x1 (x4 x68)))x2 x66 (x1 (x1 (x4 x68)))(x38 x66 x67 x68 = x19 x68 (x39 x66 x67 x68)False)(x0 (x38 x66 x67 x68) x66False)(x66 = x42 x68 x67False)False)(∀ x66 x67 x68 . x61 x68x58 x68x2 x67 (x1 (x1 (x4 x68)))x2 x66 (x1 (x1 (x4 x68)))(x2 (x39 x66 x67 x68) (x1 (x4 x68))False)(x0 (x38 x66 x67 x68) x66False)(x66 = x42 x68 x67False)False)(∀ x66 x67 x68 x69 . x61 x69x58 x69x2 x68 (x1 (x1 (x4 x69)))x2 x66 (x1 (x1 (x4 x69)))x0 (x38 x66 x68 x69) x66x2 x67 (x1 (x4 x69))x38 x66 x68 x69 = x19 x69 x67x0 x67 x68(x66 = x42 x69 x68False)False)(∀ x66 x67 x68 . x61 x68x58 x68x2 x67 (x1 (x1 (x4 x68)))x2 x66 (x1 (x1 (x4 x68)))(x2 (x38 x66 x67 x68) (x1 (x4 x68))False)(x66 = x42 x68 x67False)False)(∀ x66 x67 x68 x69 x70 . x61 x70x58 x70x2 x69 (x1 (x1 (x4 x70)))x2 x66 (x1 (x1 (x4 x70)))x66 = x42 x70 x69x2 x67 (x1 (x4 x70))x2 x68 (x1 (x4 x70))x67 = x19 x70 x68x0 x68 x69(x0 x67 x66False)False)(∀ x66 x67 x68 x69 . x61 x69x58 x69x2 x68 (x1 (x1 (x4 x69)))x2 x66 (x1 (x1 (x4 x69)))x66 = x42 x69 x68x2 x67 (x1 (x4 x69))x0 x67 x66(x0 (x37 x67 x66 x68 x69) x68False)False)(∀ x66 x67 x68 x69 . x61 x69x58 x69x2 x68 (x1 (x1 (x4 x69)))x2 x66 (x1 (x1 (x4 x69)))x66 = x42 x69 x68x2 x67 (x1 (x4 x69))x0 x67 x66(x67 = x19 x69 (x37 x67 x66 x68 x69)False)False)(∀ x66 x67 x68 x69 . x61 x69x58 x69x2 x68 (x1 (x1 (x4 x69)))x2 x66 (x1 (x1 (x4 x69)))x66 = x42 x69 x68x2 x67 (x1 (x4 x69))x0 x67 x66(x2 (x37 x67 x66 x68 x69) (x1 (x4 x69))False)False)(∀ x66 . x63 x66(x23 x66False)False)(∀ x66 . x65 x66(x63 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x8 x66 x67x60 x66 x67(x65 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x57 x66 x67x54 x66 x67(x60 x66 x67False)False)(∀ x66 . x25 x66(x24 x66False)False)(∀ x66 . x53 x66(x5 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x60 x66 x67(x54 x66 x67False)False)(∀ x66 x67 . x65 x67x2 x66 (x1 x67)x49 x66 x67False)(∀ x66 . x65 x66x44 x66(x10 x66False)False)(∀ x66 . x65 x66x44 x66(x44 x66False)False)(∀ x66 . x25 x66(x26 x66False)False)(∀ x66 . x44 x66x65 x66(x36 x66False)False)(∀ x66 . x44 x66x65 x66(x44 x66False)False)(∀ x66 . x53 x66(x51 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x65 x66(x60 x66 x67False)False)(∀ x66 x67 . (x65 x67False)x2 x66 (x1 x67)x65 x66(x49 x66 x67False)False)(∀ x66 . x65 x66x44 x66(x27 x66False)False)(∀ x66 . x65 x66x44 x66(x44 x66False)False)(∀ x66 . x28 x66(x25 x66False)False)(∀ x66 . x35 x66(x53 x66False)False)(∀ x66 x67 . x58 x67x2 x66 (x1 (x4 x67))x65 x66(x54 x66 x67False)False)(∀ x66 x67 . (x65 x67False)x2 x66 (x1 x67)(x49 x66 x67False)x65 x66False)(∀ x66 x67 . x44 x67x2 x66 (x1 x67)(x44 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x65 x66(x57 x66 x67False)False)(∀ x66 . x29 x66(x28 x66False)False)(∀ x66 . x65 x66(x47 x66False)False)(∀ x66 x67 . x6 x67x2 x66 (x1 x67)(x6 x66False)False)(∀ x66 x67 . x29 x67x2 x66 (x1 x67)(x29 x66False)False)(∀ x66 x67 . x28 x67x2 x66 (x1 x67)(x28 x66False)False)(∀ x66 x67 . x25 x67x2 x66 (x1 x67)(x25 x66False)False)(∀ x66 x67 . x26 x67x2 x66 (x1 x67)(x26 x66False)False)(∀ x66 x67 . x61 x67x58 x67x2 x66 (x1 (x4 x67))x65 x66(x8 x66 x67False)False)(∀ x66 x67 . x65 x67x2 x66 (x1 x67)(x65 x66False)False)(∀ x66 . x65 x66(x44 x66False)False)(∀ x66 . x6 x66(x29 x66False)False)(∀ x66 . x44 x66x65 x66(x36 x66False)False)(∀ x66 . x44 x66x65 x66(x44 x66False)False)(∀ x66 x67 . x24 x67x2 x66 (x1 x67)(x24 x66False)False)(∀ x66 . x65 x66(x6 x66False)False)(∀ x66 x67 . x6 x67x2 x66 x67(x35 x66False)False)(∀ x66 x67 . x29 x67x2 x66 x67(x30 x66False)False)(∀ x66 x67 . x28 x67x2 x66 x67(x34 x66False)False)(∀ x66 x67 . x25 x67x2 x66 x67(x53 x66False)False)(∀ x66 x67 . x26 x67x2 x66 x67(x5 x66False)False)(∀ x66 x67 . x24 x67x2 x66 x67(x51 x66False)False)(∀ x66 x67 . x63 x67x2 x66 (x1 x67)(x63 x66False)False)(∀ x66 x67 . x63 x67x2 x66 x67(x36 x66False)False)(∀ x66 x67 . x0 x66 x67x0 x67 x66False)(x3 (x42 x32 x33) (x42 x32 x31)False)((x3 x33 x31False)False)((x2 x31 (x1 (x1 (x4 x32)))False)False)((x2 x33 (x1 (x1 (x4 x32)))False)False)((x58 x32False)False)((x61 x32False)False)False
type
prop
theory
HotG
name
-
proof
PUX5F..
Megalodon
-
proofgold address
TMaj3..
creator
35131 PrPhD../83e54..
owner
35137 PrPhD../3eeb6..
term root
342d4..