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 . x45 x47(x47 = x46False)x45 x46False)(∀ x46 x47 . x0 x46 x47x45 x47False)(∀ x46 . x45 x46(x46 = x44False)False)(∀ x46 x47 x48 . x0 x46 x47x2 x47 (x1 x48)x45 x48False)(∀ x46 x47 x48 . x0 x47 x48x2 x48 (x1 x46)(x2 x47 x46False)False)(∀ x46 . x3 x46(x4 x46 x5 = x46False)False)(∀ x46 x47 . x43 x47 x46(x2 x47 (x1 x46)False)False)(∀ x46 x47 . x2 x47 (x1 x46)(x43 x47 x46False)False)(∀ x46 . x3 x46(x42 x41 x46 = x46False)False)(∀ x46 x47 . x2 x46 x47(x45 x47False)(x0 x46 x47False)False)(∀ x46 . x3 x46(x42 x46 x5 = x5False)False)(∀ x46 x47 . x0 x47 x46(x2 x47 x46False)False)((x2 x44 x40False)False)(∀ x46 . x3 x46(x6 x46 x5 = x46False)False)(∀ x46 x47 . x3 x47x3 x46(x4 (x39 x47) (x39 x46) = x4 x46 x47False)False)(∀ x46 x47 . x3 x47x3 x46(x6 (x39 x47) (x39 x46) = x39 (x6 x47 x46)False)False)(∀ x46 x47 x48 . x3 x48x3 x46x3 x47(x42 (x42 x48 x46) x47 = x42 x48 (x42 x46 x47)False)False)(∀ x46 x47 x48 . x3 x48x3 x46x3 x47(x6 (x6 x48 x46) x47 = x6 x48 (x6 x46 x47)False)False)(∀ x46 x47 x48 . x3 x48x3 x46x3 x47(x42 (x6 x48 x46) x47 = x6 (x42 x48 x47) (x42 x46 x47)False)False)((x2 x8 x7False)False)((x2 x8 x38False)False)((x9 x8 x7 x38False)False)((x37 x8False)False)(x45 x8False)(∀ x46 . x3 x46(x42 x46 (x39 x41) = x39 x46False)False)((x2 x41 x7False)False)((x2 x41 x38False)False)((x9 x41 x7 x38False)False)((x37 x41False)False)(x45 x41False)(∀ x46 x47 . x3 x47x3 x46(x6 x47 (x39 x46) = x4 x47 x46False)False)((x2 x10 x7False)False)((x2 x10 x38False)False)((x9 x10 x7 x38False)False)((x45 x10False)False)((x39 (x39 x8) = x8False)False)((x39 (x39 x41) = x41False)False)((x39 x8 = x39 x8False)False)((x39 x41 = x39 x41False)False)((x39 x10 = x10False)False)((x42 (x39 x8) x41 = x39 x8False)False)((x42 (x39 x8) x10 = x10False)False)((x42 x8 x41 = x8False)False)((x42 x8 x10 = x10False)False)((x42 x41 (x39 x8) = x39 x8False)False)((x42 x41 x8 = x8False)False)((x42 x41 x41 = x41False)False)((x42 x41 x10 = x10False)False)((x42 x10 (x39 x8) = x10False)False)((x42 x10 x8 = x10False)False)((x42 x10 x41 = x10False)False)((x42 x10 x10 = x10False)False)((x4 (x39 x8) (x39 x8) = x10False)False)((x4 (x39 x8) (x39 x41) = x39 x41False)False)((x4 (x39 x8) x10 = x39 x8False)False)((x4 (x39 x41) (x39 x8) = x41False)False)((x4 (x39 x41) (x39 x41) = x10False)False)((x4 (x39 x41) x41 = x39 x8False)False)((x4 (x39 x41) x10 = x39 x41False)False)((x4 x8 x8 = x10False)False)((x4 x8 x41 = x41False)False)((x4 x8 x10 = x8False)False)((x4 x41 (x39 x41) = x8False)False)((x4 x41 x8 = x39 x41False)False)((x4 x41 x41 = x10False)False)((x4 x41 x10 = x41False)False)((x4 x10 (x39 x8) = x8False)False)((x4 x10 (x39 x41) = x41False)False)((x4 x10 x8 = x39 x8False)False)((x4 x10 x41 = x39 x41False)False)((x4 x10 x10 = x10False)False)((x6 (x39 x8) x8 = x10False)False)((x6 (x39 x8) x41 = x39 x41False)False)((x6 (x39 x41) (x39 x41) = x39 x8False)False)((x6 (x39 x41) x8 = x41False)False)((x6 (x39 x41) x41 = x10False)False)((x6 (x39 x41) x10 = x39 x41False)False)((x6 x8 (x39 x8) = x10False)False)((x6 x8 (x39 x41) = x41False)False)((x6 x8 x10 = x8False)False)((x6 x41 (x39 x8) = x39 x41False)False)((x6 x41 (x39 x41) = x10False)False)((x6 x41 x41 = x8False)False)((x6 x41 x10 = x41False)False)((x6 x10 (x39 x8) = x39 x8False)False)((x6 x10 (x39 x41) = x39 x41False)False)((x6 x10 x8 = x8False)False)((x6 x10 x41 = x41False)False)((x6 x10 x10 = x10False)False)(∀ x46 . (x43 x46 x46False)False)(∀ x46 x47 x48 . (x45 x48False)(x45 x46False)x2 x46 (x1 x48)x2 x47 x46(x9 x47 x48 x46False)False)(∀ x46 x47 x48 . (x45 x48False)(x45 x46False)x2 x46 (x1 x48)x9 x47 x48 x46(x2 x47 x46False)False)((x5 = x44False)False)((x38 = x40False)False)((x36 x35False)False)(x45 x35False)((x36 x34False)False)((x3 x11False)False)(x45 x11False)((x12 x13False)False)((x33 x13False)False)((x14 x13False)False)(x45 x13False)((x3 x15False)False)((x32 x31False)False)((x12 x16False)False)(∀ x46 . x3 x46(x39 (x39 x46) = x46False)False)(∀ x46 . x32 x46(x17 (x17 x46) = x46False)False)(∀ x46 x47 . x32 x47x32 x46(x30 x47 x47 = x47False)False)(∀ x46 x47 . x32 x47x32 x46(x18 x47 x47 = x47False)False)(∀ x46 x47 . x32 x47x32 x46(x32 (x29 x47 x46)False)False)(∀ x46 x47 . (x45 x47False)x3 x47(x45 x46False)x3 x46x45 (x42 x47 x46)False)(∀ x46 . (x45 x46False)x3 x46(x3 (x39 x46)False)False)(∀ x46 . (x45 x46False)x3 x46x45 (x39 x46)False)(∀ x46 x47 . x32 x47x32 x46(x32 (x28 x47 x46)False)False)((x12 x40False)False)(x45 x40False)(∀ x46 x47 . x32 x47x32 x46(x32 (x19 x47 x46)False)False)(∀ x46 x47 . x3 x47x3 x46(x3 (x4 x47 x46)False)False)(∀ x46 x47 . x32 x47x32 x46(x32 (x30 x47 x46)False)False)(∀ x46 x47 . x3 x47x3 x46(x3 (x42 x47 x46)False)False)(∀ x46 x47 . x32 x47x32 x46(x32 (x18 x47 x46)False)False)(∀ x46 x47 . x3 x47x3 x46(x3 (x6 x47 x46)False)False)((x32 x20False)False)((x32 x27False)False)(∀ x46 x47 . (x45 x47False)(x45 x46False)x2 x46 (x1 x47)(x9 (x21 x46 x47) x47 x46False)False)(∀ x46 . (x2 (x26 x46) x46False)False)(∀ x46 x47 x48 . (x45 x48False)(x45 x46False)x2 x46 (x1 x48)x9 x47 x48 x46(x2 x47 x48False)False)((x9 x5 x7 x38False)False)((x2 x38 (x1 x7)False)False)(∀ x46 . x3 x46(x3 (x39 x46)False)False)(∀ x46 . x32 x46(x32 (x17 x46)False)False)(∀ x46 x47 . x32 x47x32 x46(x28 x47 x46 = x18 (x19 x47 x46) (x19 x46 x47)False)False)(∀ x46 x47 . x32 x47x32 x46(x19 x47 x46 = x30 (x17 x47) x46False)False)(∀ x46 x47 . x32 x47x32 x46(x30 x47 x46 = x17 (x18 (x17 x47) (x17 x46))False)False)(∀ x46 x47 . x32 x47x32 x46(x18 x47 x46 = x42 x47 x46False)False)(∀ x46 . x32 x46(x17 x46 = x4 x41 x46False)False)(∀ x46 . x46 = x20(x32 x46False)False)(∀ x46 . x46 = x27(x32 x46False)False)(∀ x46 . x32 x46(x46 = x27False)(x46 = x20False)False)((x20 = x41False)False)((x27 = x5False)False)(∀ x46 x47 . x32 x47x32 x46(x29 x47 x46 = x17 (x28 x47 x46)False)False)(∀ x46 x47 . x32 x47x32 x46(x28 x47 x46 = x28 x46 x47False)False)(∀ x46 x47 . x32 x47x32 x46(x30 x47 x46 = x30 x46 x47False)False)(∀ x46 x47 . x32 x47x32 x46(x18 x47 x46 = x18 x46 x47False)False)(∀ x46 x47 . x3 x47x3 x46(x42 x47 x46 = x42 x46 x47False)False)(∀ x46 x47 . x3 x47x3 x46(x6 x47 x46 = x6 x46 x47False)False)(∀ x46 x47 . x32 x47x32 x46(x29 x47 x46 = x29 x46 x47False)False)(∀ x46 . x45 x46(x22 x46False)False)(∀ x46 . x2 x46 x40(x36 x46False)False)(∀ x46 . x45 x46(x36 x46False)False)(∀ x46 . x36 x46(x12 x46False)False)(∀ x46 x47 . x12 x47x2 x46 x47(x12 x46False)False)(∀ x46 . x45 x46(x25 x46False)False)(∀ x46 . x45 x46(x12 x46False)False)(∀ x46 . x36 x46(x3 x46False)False)(∀ x46 . x14 x46x33 x46(x12 x46False)False)(∀ x46 . x2 x46 x7(x3 x46False)False)(∀ x46 . x32 x46(x36 x46False)False)(∀ x46 . x12 x46(x33 x46False)False)(∀ x46 . x12 x46(x14 x46False)False)(∀ x46 x47 . x22 x47x2 x46 (x1 x47)(x22 x46False)False)(∀ x46 x47 . x0 x46 x47x0 x47 x46False)(x29 x24 (x30 x24 x23) = x18 (x17 x24) x23False)((x32 x23False)False)((x32 x24False)False)False
type
prop
theory
HotG
name
-
proof
PURHq..
Megalodon
-
proofgold address
TMScg..
creator
35145 PrPhD../d8821..
owner
35148 PrPhD../e6125..
term root
0849c..