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 : ι → ι . ∀ x68 : ι → ι → ι . ∀ x69 : ι → ι → ο . ∀ x70 : ι → ο . (∀ x71 x72 . x70 x72(x72 = x71False)x70 x71False)(∀ x71 x72 . x0 x71 x72x70 x72False)(∀ x71 x72 . (x69 (x68 x72 x71) x71False)False)(∀ x71 . x70 x71(x71 = x1False)False)(∀ x71 x72 x73 . x0 x71 x72x66 x72 (x67 x73)x70 x73False)(∀ x71 x72 x73 . x0 x72 x73x66 x73 (x67 x71)(x66 x72 x71False)False)(∀ x71 . (x68 x1 x71 = x1False)False)(∀ x71 x72 x73 . x0 x72 x73x0 x72 x71x69 x73 x71False)(∀ x71 x72 . (x69 x72 x71False)(x0 (x65 x71 x72) x71False)False)(∀ x71 x72 . (x69 x71 x72False)(x0 (x65 x72 x71) x71False)False)(∀ x71 x72 . x64 x72 x71(x66 x72 (x67 x71)False)False)(∀ x71 x72 . x66 x72 (x67 x71)(x64 x72 x71False)False)(∀ x71 x72 . x63 x72x59 x72x0 x71 (x62 x72)(x0 (x61 x72 x71) (x60 x72)False)False)(∀ x71 . (x68 x71 x1 = x71False)False)(∀ x71 x72 . x0 x72 x71(x64 (x58 x72) x71False)False)(∀ x71 x72 . x64 (x58 x72) x71(x0 x72 x71False)False)(∀ x71 x72 . x66 x71 x72(x70 x72False)(x0 x71 x72False)False)(∀ x71 . (x2 x71 x1 = x1False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71x57 x72x57 x71(x61 x71 (x55 x71 x72) = x61 x72 (x54 x71 x72)False)(x57 (x56 x72 x71)False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71x57 x72x57 x71(x0 (x54 x71 x72) (x3 (x62 x72) (x62 x71))False)(x57 (x56 x72 x71)False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71x57 x72x57 x71(x0 (x55 x71 x72) (x62 x71)False)(x57 (x56 x72 x71)False)False)(∀ x71 x72 . x0 x72 x71(x66 x72 x71False)False)(∀ x71 x72 . (x64 (x2 x71 x72) x71False)False)(∀ x71 x72 . x69 x71 x72(x69 x72 x71False)False)(∀ x71 . (x64 x71 x71False)False)(∀ x71 x72 . (x3 x71 x72 = x68 x71 x72False)False)(∀ x71 . (x53 x71False)x53 (x52 x71)False)(∀ x71 . (x53 x71False)(x66 (x52 x71) (x67 x71)False)False)(∀ x71 . (x70 x71False)(x53 (x51 x71)False)False)(∀ x71 . (x70 x71False)x70 (x51 x71)False)(∀ x71 . (x70 x71False)(x66 (x51 x71) (x67 x71)False)False)((x4 x5False)False)(x70 x5False)((x6 x5False)False)((x50 x49False)False)((x70 x49False)False)((x48 x47False)False)((x50 x47False)False)((x46 x47False)False)((x70 x47False)False)(∀ x71 . (x70 x71False)(x44 (x45 x71) x71False)False)(∀ x71 . (x70 x71False)(x66 (x45 x71) (x67 x71)False)False)((x43 x42False)False)((x50 x42False)False)((x48 x41False)False)((x43 x41False)False)((x50 x41False)False)((x46 x41False)False)(∀ x71 . x44 (x40 x71) x71False)(∀ x71 . (x66 (x40 x71) (x67 x71)False)False)((x39 x38False)False)((x7 x38False)False)(x70 x38False)(x53 x8False)((x37 x36False)False)((x50 x36False)False)((x48 x35False)False)((x37 x35False)False)((x50 x35False)False)((x46 x35False)False)(x70 x34False)(∀ x71 . (x70 (x9 x71)False)False)(∀ x71 . (x66 (x9 x71) (x67 x71)False)False)((x7 x10False)False)(x70 x10False)((x53 x11False)False)(x70 x11False)((x50 x12False)False)((x48 x33False)False)((x70 x13False)False)(∀ x71 . (x70 x71False)x70 (x32 x71)False)(∀ x71 . (x70 x71False)(x66 (x32 x71) (x67 x71)False)False)((x7 x31False)False)(x70 x31False)(∀ x71 . (x2 x71 x71 = x71False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71(x56 x72 x72 = x72False)False)(∀ x71 . x48 x71(x30 (x58 x71)False)False)(∀ x71 . x50 x71(x6 (x58 x71)False)False)(∀ x71 . x46 x71(x29 (x58 x71)False)False)(∀ x71 x72 . x7 x72(x7 (x68 x72 x71)False)False)(∀ x71 x72 . x28 x72(x28 (x68 x72 x71)False)False)(∀ x71 x72 . x14 x72(x14 (x68 x72 x71)False)False)(∀ x71 x72 . x30 x72(x30 (x68 x72 x71)False)False)(∀ x71 x72 . x6 x72(x6 (x68 x72 x71)False)False)(∀ x71 x72 . x29 x72(x29 (x68 x72 x71)False)False)(∀ x71 x72 . x7 x72(x7 (x2 x71 x72)False)False)(∀ x71 x72 . x7 x72(x7 (x2 x72 x71)False)False)(∀ x71 x72 . x28 x72(x28 (x2 x71 x72)False)False)(∀ x71 x72 . x28 x72(x28 (x2 x72 x71)False)False)(∀ x71 x72 . x14 x72(x14 (x2 x71 x72)False)False)(∀ x71 x72 . x14 x72(x14 (x2 x72 x71)False)False)(∀ x71 x72 . x30 x72(x30 (x2 x71 x72)False)False)(∀ x71 x72 . x30 x72(x30 (x2 x72 x71)False)False)(∀ x71 x72 . x6 x72(x6 (x2 x71 x72)False)False)(∀ x71 x72 . x6 x72(x6 (x2 x72 x71)False)False)(∀ x71 x72 . x29 x72(x29 (x2 x71 x72)False)False)(∀ x71 x72 . x29 x72(x29 (x2 x72 x71)False)False)(∀ x71 . (x53 (x58 x71)False)False)(∀ x71 . x70 (x58 x71)False)((x70 x1False)False)(∀ x71 . x70 (x67 x71)False)(∀ x71 x72 . x6 x72x4 x72x6 x71x4 x71(x4 (x2 x72 x71)False)False)(∀ x71 . x27 x71(x7 (x58 x71)False)False)(∀ x71 . x15 x71(x28 (x58 x71)False)False)(∀ x71 . x26 x71(x14 (x58 x71)False)False)(∀ x71 . (x66 (x16 x71) x71False)False)(∀ x71 x72 . (x66 (x3 x71 x72) (x67 x71)False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71(x59 (x56 x72 x71)False)False)(∀ x71 x72 . x63 x72x59 x72x63 x71x59 x71(x63 (x56 x72 x71)False)False)(∀ x71 x72 x73 . (x0 (x17 x71 x72 x73) x72False)(x0 (x17 x71 x72 x73) x71False)(x71 = x2 x73 x72False)False)(∀ x71 x72 x73 . (x0 (x17 x71 x72 x73) x73False)(x0 (x17 x71 x72 x73) x71False)(x71 = x2 x73 x72False)False)(∀ x71 x72 x73 . x0 (x17 x71 x72 x73) x71x0 (x17 x71 x72 x73) x73x0 (x17 x71 x72 x73) x72(x71 = x2 x73 x72False)False)(∀ x71 x72 x73 x74 . x74 = x2 x72 x73x0 x71 x72x0 x71 x73(x0 x71 x74False)False)(∀ x71 x72 x73 x74 . x72 = x2 x71 x73x0 x74 x72(x0 x74 x73False)False)(∀ x71 x72 x73 x74 . x72 = x2 x73 x71x0 x74 x72(x0 x74 x73False)False)(∀ x71 . x63 x71x59 x71x18 x71 = x19 x71(x57 x71False)False)(∀ x71 . x63 x71x59 x71(x61 x71 (x18 x71) = x61 x71 (x19 x71)False)(x57 x71False)False)(∀ x71 . x63 x71x59 x71(x0 (x19 x71) (x62 x71)False)(x57 x71False)False)(∀ x71 . x63 x71x59 x71(x0 (x18 x71) (x62 x71)False)(x57 x71False)False)(∀ x71 x72 x73 . x63 x73x59 x73x57 x73x0 x71 (x62 x73)x0 x72 (x62 x73)x61 x73 x71 = x61 x73 x72(x71 = x72False)False)(∀ x71 x72 . (x25 x72 x71 = x71False)(x0 (x25 x72 x71) x72False)(x72 = x58 x71False)False)(∀ x71 x72 . x0 (x25 x72 x71) x72x25 x72 x71 = x71(x72 = x58 x71False)False)(∀ x71 x72 x73 . x72 = x58 x73x71 = x73(x0 x71 x72False)False)(∀ x71 x72 x73 . x72 = x58 x73x0 x71 x72(x71 = x73False)False)(∀ x71 x72 . (x2 x72 x71 = x2 x71 x72False)False)(∀ x71 . x7 x71(x20 x71False)False)(∀ x71 . x7 x71(x7 x71False)False)(∀ x71 . x28 x71(x70 x71False)x20 x71(x21 x71False)False)(∀ x71 . x28 x71(x70 x71False)x20 x71x70 x71False)(∀ x71 . x28 x71(x70 x71False)x20 x71(x28 x71False)False)(∀ x71 . x50 x71(x37 x71False)(x43 x71False)(x50 x71False)False)(∀ x71 . x50 x71(x37 x71False)(x43 x71False)(x70 x71False)False)(∀ x71 . x70 x71x50 x71x43 x71False)(∀ x71 . x70 x71x50 x71x37 x71False)(∀ x71 . x70 x71x50 x71(x50 x71False)False)(∀ x71 . (x70 x71False)x50 x71(x37 x71False)(x43 x71False)False)(∀ x71 . (x70 x71False)x50 x71(x37 x71False)(x50 x71False)False)(∀ x71 . x50 x71x43 x71x37 x71False)(∀ x71 . x50 x71x43 x71(x50 x71False)False)(∀ x71 . x50 x71x43 x71x70 x71False)(∀ x71 x72 . x53 x72x66 x71 (x67 x72)(x53 x71False)False)(∀ x71 . x30 x71(x29 x71False)False)(∀ x71 . (x70 x71False)x50 x71(x43 x71False)(x37 x71False)False)(∀ x71 . (x70 x71False)x50 x71(x43 x71False)(x50 x71False)False)(∀ x71 . x48 x71(x50 x71False)False)(∀ x71 x72 . x70 x72x66 x71 (x67 x72)x44 x71 x72False)(∀ x71 . x30 x71(x6 x71False)False)(∀ x71 . x7 x71(x70 x71False)(x21 x71False)False)(∀ x71 . x7 x71(x70 x71False)x70 x71False)(∀ x71 . x7 x71(x70 x71False)(x7 x71False)False)(∀ x71 . x50 x71x37 x71x43 x71False)(∀ x71 . x50 x71x37 x71(x50 x71False)False)(∀ x71 . x50 x71x37 x71x70 x71False)(∀ x71 . x48 x71(x46 x71False)False)(∀ x71 x72 . (x70 x72False)x66 x71 (x67 x72)x70 x71(x44 x71 x72False)False)(∀ x71 . x14 x71(x30 x71False)False)(∀ x71 . (x53 x71False)x70 x71False)(∀ x71 . x27 x71(x50 x71False)False)(∀ x71 . x27 x71(x48 x71False)False)(∀ x71 x72 . (x70 x72False)x66 x71 (x67 x72)(x44 x71 x72False)x70 x71False)(∀ x71 . x28 x71(x14 x71False)False)(∀ x71 . x70 x71(x39 x71False)False)(∀ x71 x72 . x7 x72x66 x71 (x67 x72)(x7 x71False)False)(∀ x71 x72 . x28 x72x66 x71 (x67 x72)(x28 x71False)False)(∀ x71 x72 . x14 x72x66 x71 (x67 x72)(x14 x71False)False)(∀ x71 x72 . x30 x72x66 x71 (x67 x72)(x30 x71False)False)(∀ x71 x72 . x6 x72x66 x71 (x67 x72)(x6 x71False)False)(∀ x71 . x70 x71(x53 x71False)False)(∀ x71 x72 . x70 x72x66 x71 (x67 x72)(x70 x71False)False)(∀ x71 . x7 x71(x28 x71False)False)(∀ x71 x72 . x29 x72x66 x71 (x67 x72)(x29 x71False)False)(∀ x71 . x70 x71(x7 x71False)False)(∀ x71 x72 . x7 x72x66 x71 x72(x27 x71False)False)(∀ x71 . x6 x71x21 x71x70 x71False)(∀ x71 . x6 x71x21 x71(x6 x71False)False)(∀ x71 x72 . x28 x72x66 x71 x72(x15 x71False)False)(∀ x71 . x6 x71x70 x71(x4 x71False)False)(∀ x71 . x6 x71x70 x71(x6 x71False)False)(∀ x71 x72 . x14 x72x66 x71 x72(x26 x71False)False)(∀ x71 x72 . x30 x72x66 x71 x72(x48 x71False)False)(∀ x71 x72 . x6 x72x66 x71 x72(x50 x71False)False)(∀ x71 x72 . x29 x72x66 x71 x72(x46 x71False)False)(∀ x71 . x30 x71x21 x71(x20 x71False)False)(∀ x71 . x30 x71x21 x71(x30 x71False)False)(∀ x71 x72 . x0 x71 x72x0 x72 x71False)(x57 (x56 x23 x22)False)((x2 (x60 x23) (x60 x22) = x58 (x61 x23 x24)False)False)((x2 (x62 x23) (x62 x22) = x58 x24False)False)((x57 x22False)False)((x57 x23False)False)((x59 x22False)False)((x63 x22False)False)((x59 x23False)False)((x63 x23False)False)False
type
prop
theory
HotG
name
-
proof
PUMgb..
Megalodon
-
proofgold address
TMH9f..
creator
35130 PrPhD../6a4d1..
owner
35137 PrPhD../841c7..
term root
9cfac..