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 x57x55 x57False)(∀ x56 . x55 x56(x56 = x54False)False)(∀ x56 x57 x58 . x0 x56 x57x2 x57 (x1 x58)x55 x58False)(∀ x56 x57 x58 . x0 x57 x58x2 x58 (x1 x56)(x2 x57 x56False)False)(∀ x56 x57 . x3 x57 x56(x2 x57 (x1 x56)False)False)(∀ x56 x57 . x2 x57 (x1 x56)(x3 x57 x56False)False)(∀ x56 x57 . x2 x56 x57(x55 x57False)(x0 x56 x57False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x0 x58 (x52 x59)x0 x58 x56x0 (x51 x59 x58) x57(x0 x58 (x50 x56 (x49 x59 x56 x57))False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x0 x58 (x50 x56 (x49 x59 x56 x57))(x0 (x51 x59 x58) x57False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x0 x58 (x50 x57 (x49 x59 x57 x56))(x0 x58 x57False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x0 x58 (x50 x56 (x49 x59 x56 x57))(x0 x58 (x52 x59)False)False)(∀ x56 x57 . x0 x57 x56(x2 x57 x56False)False)(∀ x56 . (x3 x56 x56False)False)(∀ x56 x57 . x53 x57x47 x57 x56(x50 x56 x57 = x52 x57False)False)(∀ x56 x57 . x53 x57x4 x57 x56(x5 x56 x57 = x57False)False)(∀ x56 x57 . x53 x57x47 x57 x56(x46 x57 x56 = x57False)False)(∀ x56 x57 . x53 x57(x5 x56 (x5 x56 x57) = x5 x56 x57False)False)(∀ x56 x57 . x53 x57(x46 (x46 x57 x56) x56 = x46 x57 x56False)False)(∀ x56 . x53 x56(x46 x56 (x52 x56) = x56False)False)(∀ x56 . (x48 (x45 x56)False)False)(∀ x56 . (x47 (x45 x56) x56False)False)(∀ x56 . (x44 (x45 x56)False)False)(∀ x56 . (x53 (x45 x56)False)False)((x43 x42False)False)(x55 x42False)(∀ x56 . (x41 x56False)x41 (x40 x56)False)(∀ x56 . (x41 x56False)(x2 (x40 x56) (x1 x56)False)False)(∀ x56 x57 . (x48 (x39 x56 x57)False)False)(∀ x56 x57 . (x4 (x39 x56 x57) x56False)False)(∀ x56 x57 . (x47 (x39 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x39 x56 x57)False)False)(∀ x56 . (x55 x56False)(x41 (x38 x56)False)False)(∀ x56 . (x55 x56False)x55 (x38 x56)False)(∀ x56 . (x55 x56False)(x2 (x38 x56) (x1 x56)False)False)(x6 x7False)((x48 x7False)False)((x53 x7False)False)(∀ x56 . (x55 x56False)(x36 (x37 x56) x56False)False)(∀ x56 . (x55 x56False)(x2 (x37 x56) (x1 x56)False)False)((x48 x35False)False)((x44 x35False)False)((x53 x35False)False)(x55 x35False)(∀ x56 . x36 (x34 x56) x56False)(∀ x56 . (x2 (x34 x56) (x1 x56)False)False)(∀ x56 x57 . (x4 (x33 x56 x57) x56False)False)(∀ x56 x57 . (x47 (x33 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x33 x56 x57)False)False)((x48 x8False)False)((x44 x8False)False)((x53 x8False)False)(x55 x32False)(∀ x56 . (x55 (x9 x56)False)False)(∀ x56 . (x2 (x9 x56) (x1 x56)False)False)((x44 x10False)False)((x53 x10False)False)((x11 x12False)False)((x48 x12False)False)((x53 x12False)False)((x55 x31False)False)(∀ x56 . (x55 x56False)x55 (x13 x56)False)(∀ x56 . (x55 x56False)(x2 (x13 x56) (x1 x56)False)False)(∀ x56 x57 . (x4 (x14 x56 x57) x56False)False)(∀ x56 x57 . (x47 (x14 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x14 x56 x57)False)False)(∀ x56 x57 . (x55 (x14 x56 x57)False)False)(∀ x56 x57 . (x2 (x14 x56 x57) (x1 (x15 x57 x56))False)False)((x53 x30False)False)(x55 x30False)(∀ x56 x57 . (x48 (x29 x56 x57)False)False)(∀ x56 x57 . (x4 (x29 x56 x57) x56False)False)(∀ x56 x57 . (x47 (x29 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x29 x56 x57)False)False)(∀ x56 x57 . (x2 (x29 x56 x57) (x1 (x15 x57 x56))False)False)((x48 x16False)False)((x53 x16False)False)(∀ x56 x57 . x53 x57x48 x57(x48 (x5 x56 x57)False)False)(∀ x56 x57 . x53 x57x48 x57(x53 (x5 x56 x57)False)False)(∀ x56 x57 x58 x59 . x2 x59 (x1 (x15 (x15 x57 x56) x58))(x53 (x52 x59)False)False)(∀ x56 . (x55 x56False)x53 x56x55 (x52 x56)False)(∀ x56 x57 . x53 x57x48 x57(x48 (x46 x57 x56)False)False)(∀ x56 x57 . x53 x57x48 x57(x53 (x46 x57 x56)False)False)(∀ x56 x57 . (x53 (x15 x56 x57)False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x56(x4 (x5 x57 x58) x56False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x57(x4 (x5 x56 x58) x56False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x57(x53 (x5 x56 x58)False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x56(x47 (x5 x57 x58) x56False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x57(x53 (x5 x56 x58)False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x56(x47 (x46 x58 x57) x56False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x57(x47 (x46 x58 x56) x56False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x57(x53 (x46 x58 x56)False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x56(x4 (x46 x58 x57) x56False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x57(x53 (x46 x58 x56)False)False)(∀ x56 . x41 x56x53 x56(x41 (x52 x56)False)False)(∀ x56 x57 . x53 x57x17 x57(x17 (x46 x57 x56)False)False)(∀ x56 x57 . x53 x57x17 x57(x53 (x46 x57 x56)False)False)(∀ x56 x57 . x55 x57x53 x57(x55 (x18 x57 x56)False)False)((x55 x54False)False)(∀ x56 . x55 (x1 x56)False)(∀ x56 x57 . x53 x57x55 x56(x55 (x18 x57 x56)False)False)(∀ x56 x57 . x53 x57x17 x57x48 x57(x55 (x51 x57 x56)False)False)(∀ x56 x57 . x53 x57x55 x56(x53 (x5 x56 x57)False)False)(∀ x56 x57 . x53 x57x55 x56(x55 (x5 x56 x57)False)False)(∀ x56 . (x41 x56False)x53 x56x48 x56x41 (x52 x56)False)(∀ x56 x57 . x55 x57x53 x57(x53 (x46 x57 x56)False)False)(∀ x56 x57 . x55 x57x53 x57(x55 (x46 x57 x56)False)False)(∀ x56 x57 x58 . x43 x58x53 x56x4 x56 x58x48 x56(x48 (x51 x56 x57)False)False)(∀ x56 x57 x58 . x43 x58x53 x56x4 x56 x58x48 x56(x53 (x51 x56 x57)False)False)(∀ x56 x57 . x53 x57x55 x56(x53 (x46 x57 x56)False)False)(∀ x56 x57 . x53 x57x55 x56(x55 (x46 x57 x56)False)False)(∀ x56 x57 . (x55 x57False)x53 x57(x55 x56False)x2 x56 (x1 (x52 x57))x55 (x18 x57 x56)False)(∀ x56 x57 . (x55 x57False)x53 x57x44 x57x48 x57x2 x56 (x52 x57)x55 (x51 x57 x56)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)x55 (x15 x57 x56)False)(∀ x56 x57 . (x55 x57False)x53 x57(x55 x56False)x2 x56 (x1 (x52 x57))(x53 (x46 x57 x56)False)False)(∀ x56 x57 . (x55 x57False)x53 x57(x55 x56False)x2 x56 (x1 (x52 x57))x55 (x46 x57 x56)False)(∀ x56 . x55 x56(x55 (x52 x56)False)False)(∀ x56 . (x2 (x19 x56) x56False)False)((x55 x28False)False)(∀ x56 x57 . x53 x57(x53 (x5 x56 x57)False)False)(∀ x56 x57 . x53 x57(x53 (x46 x57 x56)False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x2 (x49 x58 x57 x56) (x1 (x15 x57 x56))False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x48 (x49 x58 x57 x56)False)False)(∀ x56 x57 . x53 x57x47 x57 x56(x2 (x50 x56 x57) (x1 x56)False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x27 x56 x57 x58 = x51 x58 (x26 x56 x57 x58)False)(x0 (x27 x56 x57 x58) x56False)(x56 = x18 x58 x57False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x0 (x26 x56 x57 x58) x57False)(x0 (x27 x56 x57 x58) x56False)(x56 = x18 x58 x57False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x0 (x26 x56 x57 x58) (x52 x58)False)(x0 (x27 x56 x57 x58) x56False)(x56 = x18 x58 x57False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x0 (x27 x58 x57 x59) x58x0 x56 (x52 x59)x0 x56 x57x27 x58 x57 x59 = x51 x59 x56(x58 = x18 x59 x57False)False)(∀ x56 x57 x58 x59 x60 . x53 x60x48 x60x59 = x18 x60 x58x0 x56 (x52 x60)x0 x56 x58x57 = x51 x60 x56(x0 x57 x59False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x58 = x18 x59 x57x0 x56 x58(x56 = x51 x59 (x20 x56 x58 x57 x59)False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x58 = x18 x59 x57x0 x56 x58(x0 (x20 x56 x58 x57 x59) x57False)False)(∀ x56 x57 x58 x59 . x53 x59x48 x59x58 = x18 x59 x57x0 x56 x58(x0 (x20 x56 x58 x57 x59) (x52 x59)False)False)(∀ x56 x57 . x0 (x25 x56 x57) x56(x3 x57 x56False)False)(∀ x56 x57 . (x0 (x25 x56 x57) x57False)(x3 x57 x56False)False)(∀ x56 x57 x58 . x3 x57 x58x0 x56 x57(x0 x56 x58False)False)((x54 = x28False)False)(∀ x56 x57 . x53 x57x47 x57 x56x50 x56 x57 = x56(x24 x57 x56False)False)(∀ x56 x57 . x53 x57x47 x57 x56x24 x57 x56(x50 x56 x57 = x56False)False)(∀ x56 x57 x58 . x53 x58x48 x58(x49 x58 x57 x56 = x46 (x5 x56 x58) x57False)False)(∀ x56 x57 . x3 x57 x56x3 x56 x57(x57 = x56False)False)(∀ x56 x57 . x56 = x57(x3 x57 x56False)False)(∀ x56 x57 . x57 = x56(x3 x57 x56False)False)(∀ x56 x57 . x43 x57x2 x56 (x1 x57)(x43 x56False)False)(∀ x56 x57 . x55 x57x53 x56x4 x56 x57(x4 x56 x57False)False)(∀ x56 x57 . x55 x57x53 x56x4 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x4 x56 x57(x55 x56False)False)(∀ x56 x57 . x43 x57x2 x56 x57(x48 x56False)False)(∀ x56 x57 . x43 x57x2 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x47 x56 x57(x47 x56 x57False)False)(∀ x56 x57 . x55 x57x53 x56x47 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x47 x56 x57(x55 x56False)False)(∀ x56 . x55 x56(x43 x56False)False)(∀ x56 x57 x58 . x53 x58x4 x58 x56x2 x57 (x1 x58)(x4 x57 x56False)False)(∀ x56 . x41 x56x53 x56x48 x56(x6 x56False)False)(∀ x56 . x41 x56x53 x56x48 x56(x48 x56False)False)(∀ x56 . x41 x56x53 x56x48 x56(x53 x56False)False)(∀ x56 x57 . x41 x57x2 x56 (x1 x57)(x41 x56False)False)(∀ x56 x57 x58 . x53 x58x47 x58 x56x2 x57 (x1 x58)(x47 x57 x56False)False)(∀ x56 . x53 x56x48 x56(x6 x56False)(x48 x56False)False)(∀ x56 . x53 x56x48 x56(x6 x56False)(x53 x56False)False)(∀ x56 . x53 x56x48 x56(x6 x56False)x41 x56False)(∀ x56 x57 . x55 x57x2 x56 (x1 x57)x36 x56 x57False)(∀ x56 x57 x58 . x55 x58x2 x56 (x1 (x15 x57 x58))(x55 x56False)False)(∀ x56 . x55 x56x53 x56(x44 x56False)False)(∀ x56 . x55 x56x53 x56(x53 x56False)False)(∀ x56 . x55 x56x53 x56x48 x56(x6 x56False)False)(∀ x56 . x55 x56x53 x56x48 x56(x48 x56False)False)(∀ x56 . x55 x56x53 x56x48 x56(x53 x56False)False)(∀ x56 x57 . (x55 x57False)x2 x56 (x1 x57)x55 x56(x36 x56 x57False)False)(∀ x56 x57 x58 . x55 x58x2 x56 (x1 (x15 x58 x57))(x55 x56False)False)(∀ x56 . x55 x56x53 x56(x17 x56False)False)(∀ x56 . x55 x56x53 x56(x53 x56False)False)(∀ x56 x57 . x53 x57x48 x57x2 x56 (x1 x57)(x48 x56False)False)(∀ x56 x57 . (x55 x57False)x2 x56 (x1 x57)(x36 x56 x57False)x55 x56False)(∀ x56 x57 x58 . x2 x58 (x1 (x15 x56 x57))(x4 x58 x57False)False)(∀ x56 x57 x58 . x2 x58 (x1 (x15 x57 x56))(x47 x58 x57False)False)(∀ x56 x57 . x53 x57x2 x56 (x1 x57)(x53 x56False)False)(∀ x56 x57 x58 . (x55 x58False)x55 x56x2 x57 (x1 (x15 x58 x56))x24 x57 x58False)(∀ x56 . x55 x56x53 x56x48 x56(x11 x56False)False)(∀ x56 . x55 x56x53 x56x48 x56(x48 x56False)False)(∀ x56 . x55 x56x53 x56x48 x56(x53 x56False)False)(∀ x56 x57 . x55 x57x2 x56 (x1 x57)(x55 x56False)False)(∀ x56 x57 x58 . x2 x58 (x1 (x15 x56 x57))(x53 x58False)False)(∀ x56 . x55 x56(x53 x56False)False)(∀ x56 x57 x58 . x55 x58x2 x56 (x1 (x15 x58 x57))(x24 x56 x58False)False)(∀ x56 . x55 x56(x48 x56False)False)(∀ x56 x57 . x0 x56 x57x0 x57 x56False)(x24 (x49 x22 x21 x23) x21False)((x3 (x18 x22 x21) x23False)False)((x3 x21 (x52 x22)False)False)((x48 x22False)False)((x53 x22False)False)False
type
prop
theory
HotG
name
-
proof
PUgRF..
Megalodon
-
proofgold address
TMaNB..
creator
35135 PrPhD../65637..
owner
35137 PrPhD../c43c3..
term root
1f263..