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 . x55 x57(x57 = x56False)x55 x56False)(∀ x56 x57 . (x0 x56 (x1 x56 x57)False)False)(∀ x56 x57 . x54 x56 x57x55 x57False)(∀ x56 . x55 x56(x56 = x2False)False)(∀ x56 x57 x58 . x54 x56 x57x52 x57 (x53 x58)x55 x58False)(∀ x56 x57 x58 . x3 x58x6 x58x4 x57 x58x4 x56 x58x4 x57 x56(x0 (x5 x57) (x5 x56)False)False)(∀ x56 x57 x58 . x3 x58x6 x58x4 x57 x58x4 x56 x58x0 (x5 x57) (x5 x56)(x4 x57 x56False)False)(∀ x56 x57 x58 . x54 x57 x58x52 x58 (x53 x56)(x52 x57 x56False)False)(∀ x56 x57 . x0 x57 x56(x52 x57 (x53 x56)False)False)(∀ x56 x57 . x52 x57 (x53 x56)(x0 x57 x56False)False)(∀ x56 x57 . x52 x56 x57(x55 x57False)(x54 x56 x57False)False)(∀ x56 x57 . x54 x57 x56(x52 x57 x56False)False)(∀ x56 . (x1 x56 x2 = x56False)False)(x55 x7False)(∀ x56 . (x0 x56 x56False)False)(∀ x56 . x3 x56x6 x56(x8 (x9 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x52 (x9 x56) (x53 (x5 x56))False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x12 (x11 x56) x56False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56x55 (x11 x56)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x52 (x11 x56) (x53 (x5 x56))False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56x50 (x51 x56) x56False)(∀ x56 . (x10 x56False)x3 x56x6 x56x55 (x51 x56)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x52 (x51 x56) (x53 (x5 x56))False)False)(∀ x56 . x3 x56x6 x56(x12 (x13 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x52 (x13 x56) (x53 (x5 x56))False)False)(∀ x56 . x6 x56(x50 (x14 x56) x56False)False)(∀ x56 . x6 x56(x52 (x14 x56) (x53 (x5 x56))False)False)(∀ x56 . x3 x56x6 x56(x3 (x15 x56)False)False)(∀ x56 . x3 x56x6 x56(x49 (x15 x56)False)False)(∀ x56 . x3 x56x6 x56(x4 (x15 x56) x56False)False)(∀ x56 . (x10 x56False)x47 x56x55 (x48 x56)False)(∀ x56 . (x10 x56False)x47 x56(x52 (x48 x56) (x53 (x5 x56))False)False)(∀ x56 . (x10 x56False)x6 x56(x49 (x46 x56)False)False)(∀ x56 . (x10 x56False)x6 x56x10 (x46 x56)False)(∀ x56 . (x10 x56False)x6 x56(x4 (x46 x56) x56False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x12 (x16 x56) x56False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x45 (x16 x56) x56False)False)(∀ x56 . (x10 x56False)x3 x56x6 x56x55 (x16 x56)False)(∀ x56 . (x10 x56False)x3 x56x6 x56(x52 (x16 x56) (x53 (x5 x56))False)False)(∀ x56 . x6 x56(x49 (x17 x56)False)False)(∀ x56 . x6 x56(x4 (x17 x56) x56False)False)(x55 x18False)(∀ x56 . x3 x56x6 x56(x12 (x44 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x45 (x44 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x52 (x44 x56) (x53 (x5 x56))False)False)((x3 x19False)False)((x49 x19False)False)(x10 x19False)((x6 x19False)False)(∀ x56 . (x20 x56False)x47 x56x21 (x22 x56)False)(∀ x56 . (x20 x56False)x47 x56(x52 (x22 x56) (x53 (x5 x56))False)False)(∀ x56 . (x10 x56False)x47 x56(x21 (x23 x56)False)False)(∀ x56 . (x10 x56False)x47 x56x55 (x23 x56)False)(∀ x56 . (x10 x56False)x47 x56(x52 (x23 x56) (x53 (x5 x56))False)False)((x55 x43False)False)(∀ x56 . x3 x56x6 x56(x45 (x24 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x52 (x24 x56) (x53 (x5 x56))False)False)((x49 x25False)False)((x6 x25False)False)((x3 x26False)False)((x49 x26False)False)((x10 x26False)False)((x6 x26False)False)((x49 x27False)False)((x10 x27False)False)((x6 x27False)False)(∀ x56 . x3 x56x6 x56(x45 (x42 x56) x56False)False)(∀ x56 . x3 x56x6 x56(x52 (x42 x56) (x53 (x5 x56))False)False)(∀ x56 . (x1 x56 x56 = x56False)False)(∀ x56 x57 x58 x59 . x52 x58 (x53 (x53 x59))x28 x59 x58 = x28 x57 x56(x58 = x56False)False)(∀ x56 x57 x58 x59 . x52 x58 (x53 (x53 x59))x28 x59 x58 = x28 x56 x57(x59 = x56False)False)(∀ x56 . (x29 x56False)x47 x56x30 (x5 x56)False)(∀ x56 x57 . (x55 x57False)x52 x56 (x53 (x53 x57))(x49 (x28 x57 x56)False)False)(∀ x56 x57 . (x55 x57False)x52 x56 (x53 (x53 x57))x10 (x28 x57 x56)False)(∀ x56 . x29 x56x47 x56(x30 (x5 x56)False)False)(∀ x56 x57 x58 . x3 x58x6 x58x45 x57 x58x52 x57 (x53 (x5 x58))x45 x56 x58x52 x56 (x53 (x5 x58))(x45 (x1 x57 x56) x58False)False)(∀ x56 . x20 x56x47 x56(x21 (x5 x56)False)False)(∀ x56 . (x10 x56False)x6 x56(x49 (x28 (x5 x56) (x31 x56))False)False)(∀ x56 . (x10 x56False)x6 x56x10 (x28 (x5 x56) (x31 x56))False)(∀ x56 . (x20 x56False)x47 x56x21 (x5 x56)False)(∀ x56 . x3 x56x6 x56(x3 (x28 (x5 x56) (x31 x56))False)False)(∀ x56 . x3 x56x6 x56(x49 (x28 (x5 x56) (x31 x56))False)False)(∀ x56 x57 . (x55 x57False)x55 (x1 x56 x57)False)(∀ x56 x57 x58 . x3 x58x6 x58x12 x57 x58x52 x57 (x53 (x5 x58))x12 x56 x58x52 x56 (x53 (x5 x58))(x12 (x1 x57 x56) x58False)False)(∀ x56 x57 . (x55 x57False)x55 (x1 x57 x56)False)(∀ x56 . (x10 x56False)x47 x56x55 (x5 x56)False)((x55 x2False)False)(∀ x56 . x10 x56x47 x56(x55 (x5 x56)False)False)(∀ x56 . x3 x56x6 x56x55 (x31 x56)False)(∀ x56 . (x52 (x32 x56) x56False)False)(∀ x56 . x6 x56(x4 (x41 x56) x56False)False)((x47 x33False)False)((x6 x40False)False)(∀ x56 . x6 x56(x52 (x31 x56) (x53 (x53 (x5 x56)))False)False)(∀ x56 x57 . x6 x57x4 x56 x57(x6 x56False)False)(∀ x56 . x6 x56(x47 x56False)False)(∀ x56 x57 x58 . (x10 x58False)x6 x58(x10 x57False)x4 x57 x58(x10 x56False)x4 x56 x58(x4 (x39 x58 x57 x56) x58False)False)(∀ x56 x57 x58 . (x10 x58False)x6 x58(x10 x57False)x4 x57 x58(x10 x56False)x4 x56 x58(x49 (x39 x58 x57 x56)False)False)(∀ x56 x57 x58 . (x10 x58False)x6 x58(x10 x57False)x4 x57 x58(x10 x56False)x4 x56 x58x10 (x39 x58 x57 x56)False)(∀ x56 x57 . x52 x57 (x53 (x53 x56))(x6 (x28 x56 x57)False)False)(∀ x56 x57 . x52 x57 (x53 (x53 x56))(x49 (x28 x56 x57)False)False)(∀ x56 x57 x58 x59 . (x10 x59False)x6 x59(x10 x58False)x4 x58 x59(x10 x57False)x4 x57 x59(x10 x56False)x49 x56x4 x56 x59x5 x56 = x1 (x5 x58) (x5 x57)(x56 = x39 x59 x58 x57False)False)(∀ x56 x57 x58 x59 . (x10 x59False)x6 x59(x10 x58False)x4 x58 x59(x10 x57False)x4 x57 x59(x10 x56False)x49 x56x4 x56 x59x56 = x39 x59 x58 x57(x5 x56 = x1 (x5 x58) (x5 x57)False)False)(∀ x56 x57 . (x1 x57 x56 = x1 x56 x57False)False)(∀ x56 x57 x58 . (x10 x58False)x6 x58(x10 x57False)x4 x57 x58(x10 x56False)x4 x56 x58(x39 x58 x57 x56 = x39 x58 x56 x57False)False)(∀ x56 . x47 x56x34 x56 x2(x10 x56False)False)(∀ x56 . x6 x56x10 x56(x38 x56False)False)(∀ x56 . x47 x56x10 x56(x34 x56 x2False)False)(∀ x56 . x47 x56(x29 x56False)x20 x56False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x45 x56 x57x8 x56 x57(x55 x56False)False)(∀ x56 . x47 x56x20 x56(x29 x56False)False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x12 x56 x57x50 x56 x57(x8 x56 x57False)False)(∀ x56 . x47 x56(x29 x56False)x29 x56False)(∀ x56 . x47 x56(x29 x56False)x10 x56False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x8 x56 x57(x50 x56 x57False)False)(∀ x56 . x47 x56x10 x56(x29 x56False)False)(∀ x56 . x47 x56x10 x56(x10 x56False)False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x55 x56(x8 x56 x57False)False)(∀ x56 x57 . x6 x57x52 x56 (x53 (x5 x57))x55 x56(x50 x56 x57False)False)(∀ x56 . x47 x56(x20 x56False)x10 x56False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x55 x56(x12 x56 x57False)False)(∀ x56 x57 . x3 x57x6 x57x52 x56 (x53 (x5 x57))x55 x56(x45 x56 x57False)False)(∀ x56 . x47 x56x10 x56(x20 x56False)False)(∀ x56 x57 . x3 x57x6 x57x4 x56 x57(x3 x56False)False)(∀ x56 . x47 x56(x20 x56False)x10 x56False)(∀ x56 . x47 x56x34 x56 x7(x20 x56False)False)(∀ x56 . x47 x56x34 x56 x7x10 x56False)(∀ x56 . x47 x56(x10 x56False)x20 x56(x34 x56 x7False)False)(∀ x56 x57 . x54 x56 x57x54 x57 x56False)(∀ x56 . x6 x56x49 x56(x56 = x28 (x5 x56) (x31 x56)False)False)(x4 x37 (x39 x35 x37 x36)False)((x4 x36 x35False)False)(x10 x36False)((x4 x37 x35False)False)(x10 x37False)((x6 x35False)False)((x3 x35False)False)(x10 x35False)False
type
prop
theory
HotG
name
-
proof
PUauk..
Megalodon
-
proofgold address
TMMP4..
creator
35136 PrPhD../d7598..
owner
35140 PrPhD../c377f..
term root
38a1d..