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 . x68 x70(x70 = x69False)x68 x69False)(∀ x69 x70 . x0 x69 x70x68 x70False)(∀ x69 . x68 x69(x69 = x67False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x6 x69 (x5 x70)(x7 x69 x70False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x7 x69 x70(x6 x69 (x5 x70)False)False)(∀ x69 x70 x71 . x0 x69 x70x2 x70 (x4 x71)x68 x71False)(∀ x69 x70 x71 . x0 x70 x71x2 x71 (x4 x69)(x2 x70 x69False)False)(∀ x69 x70 . x2 x69 (x4 (x4 x70))(x6 x69 (x8 x70 x69)False)False)(∀ x69 x70 . x6 x70 x69(x2 x70 (x4 x69)False)False)(∀ x69 x70 . x2 x70 (x4 x69)(x6 x70 x69False)False)(∀ x69 x70 . x2 x69 x70(x68 x70False)(x0 x69 x70False)False)(∀ x69 x70 x71 . x6 x70 x71x6 x71 x69(x6 x70 x69False)False)(∀ x69 x70 . x0 x70 x69(x2 x70 x69False)False)(∀ x69 x70 . x2 x69 (x4 (x4 x70))(x6 x69 (x9 x70 x69)False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 (x4 x70))(x2 x69 (x4 (x4 (x3 (x66 x70 (x9 x70 x69)))))False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 (x4 x70))(x10 x69 (x66 x70 (x9 x70 x69))False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 (x4 x70))(x7 x69 (x66 x70 (x9 x70 x69))False)False)(∀ x69 . (x6 x69 x69False)False)((x65 x64False)False)((x11 x64False)False)((x63 x64False)False)(x68 x64False)((x62 x61False)False)((x12 x61False)False)(x68 x61False)((x13 x14False)False)(x68 x14False)(∀ x69 . (x15 x69False)(x12 (x16 x69)False)False)(∀ x69 . (x15 x69False)x15 (x16 x69)False)(∀ x69 . (x15 x69False)(x2 (x16 x69) (x4 x69)False)False)(∀ x69 . (x15 x69False)x15 (x60 x69)False)(∀ x69 . (x15 x69False)(x2 (x60 x69) (x4 x69)False)False)(x12 x59False)((x11 x59False)False)((x63 x59False)False)(∀ x69 . (x68 x69False)(x15 (x17 x69)False)False)(∀ x69 . (x68 x69False)x68 (x17 x69)False)(∀ x69 . (x68 x69False)(x2 (x17 x69) (x4 x69)False)False)(x58 x57False)((x11 x57False)False)((x63 x57False)False)((x18 x19False)False)(∀ x69 . (x68 x69False)(x55 (x56 x69) x69False)False)(∀ x69 . (x68 x69False)(x2 (x56 x69) (x4 x69)False)False)(∀ x69 . x55 (x54 x69) x69False)(∀ x69 . (x2 (x54 x69) (x4 x69)False)False)((x12 x53False)False)((x11 x53False)False)((x63 x53False)False)(x68 x53False)(x68 x52False)(∀ x69 . (x68 (x20 x69)False)False)(∀ x69 . (x2 (x20 x69) (x4 x69)False)False)((x21 x22False)False)((x11 x22False)False)((x63 x22False)False)(x68 x51False)((x58 x51False)False)((x11 x51False)False)((x63 x51False)False)(∀ x69 . (x68 x69False)(x12 (x50 x69)False)False)(∀ x69 . (x68 x69False)x68 (x50 x69)False)(∀ x69 . (x68 x69False)(x2 (x50 x69) (x4 x69)False)False)(∀ x69 . x1 x69(x24 (x23 x69) x69False)False)(∀ x69 . x1 x69(x7 (x23 x69) x69False)False)(∀ x69 . x1 x69(x2 (x23 x69) (x4 (x4 (x3 x69)))False)False)((x68 x49False)False)(∀ x69 . x1 x69(x7 (x25 x69) x69False)False)(∀ x69 . x1 x69(x2 (x25 x69) (x4 (x4 (x3 x69)))False)False)(∀ x69 . (x68 x69False)x68 (x26 x69)False)(∀ x69 . (x68 x69False)(x2 (x26 x69) (x4 x69)False)False)((x27 x28False)False)((x1 x28False)False)((x11 x29False)False)((x63 x29False)False)((x30 x31False)False)((x11 x31False)False)((x63 x31False)False)((x12 x48False)False)(x68 x48False)((x47 x46False)False)((x11 x46False)False)((x63 x46False)False)(∀ x69 . x1 x69(x10 (x32 x69) x69False)False)(∀ x69 . x1 x69(x7 (x32 x69) x69False)False)(∀ x69 . x1 x69(x2 (x32 x69) (x4 (x4 (x3 x69)))False)False)((x27 x45False)False)((x33 x45False)False)((x1 x45False)False)(∀ x69 x70 x71 x72 . x2 x71 (x4 (x4 x72))x66 x72 x71 = x66 x70 x69(x71 = x69False)False)(∀ x69 x70 x71 x72 . x2 x71 (x4 (x4 x72))x66 x72 x71 = x66 x69 x70(x72 = x69False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 (x4 x70))(x27 (x66 x70 x69)False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 (x4 x70))x33 (x66 x70 x69)False)(∀ x69 . (x33 x69False)x1 x69(x27 (x66 (x3 x69) (x5 x69))False)False)(∀ x69 . (x33 x69False)x1 x69x33 (x66 (x3 x69) (x5 x69))False)(∀ x69 . x1 x69(x24 (x5 x69) x69False)False)(∀ x69 . x12 x69(x62 (x4 x69)False)False)(∀ x69 x70 . x2 x70 (x4 (x4 x69))x68 (x8 x69 x70)False)((x68 x67False)False)(∀ x69 . x1 x69(x7 (x5 x69) x69False)False)(∀ x69 . x68 (x4 x69)False)(∀ x69 . x1 x69(x10 (x5 x69) x69False)False)(∀ x69 . x12 x69(x12 (x4 x69)False)False)(∀ x69 . (x2 (x34 x69) x69False)False)((x44 x43False)False)((x1 x35False)False)(∀ x69 . x1 x69(x2 (x5 x69) (x4 (x4 (x3 x69)))False)False)((x68 x36False)False)(∀ x69 . x1 x69(x44 x69False)False)(∀ x69 x70 . x2 x70 (x4 (x4 x69))(x2 (x8 x69 x70) (x4 (x4 x69))False)False)(∀ x69 x70 . x2 x70 (x4 (x4 x69))(x2 (x9 x69 x70) (x4 (x4 x69))False)False)(∀ x69 x70 . x2 x70 (x4 (x4 x69))(x1 (x66 x69 x70)False)False)(∀ x69 x70 . x2 x70 (x4 (x4 x69))(x27 (x66 x69 x70)False)False)(∀ x69 x70 x71 . x1 x71x2 x69 (x4 (x4 (x3 x71)))x7 x70 x71x10 x70 x71x2 x70 (x4 (x4 (x3 x71)))x6 x70 (x8 (x3 x71) x69)(x24 x69 x71False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x24 x69 x70(x6 (x42 x69 x70) (x8 (x3 x70) x69)False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x24 x69 x70(x2 (x42 x69 x70) (x4 (x4 (x3 x70)))False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x24 x69 x70(x10 (x42 x69 x70) x70False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x24 x69 x70(x7 (x42 x69 x70) x70False)False)((x67 = x36False)False)(∀ x69 . x1 x69x33 x69(x37 x69False)False)(∀ x69 x70 . x13 x70x2 x69 (x4 x70)(x13 x69False)False)(∀ x69 . x68 x69x63 x69(x65 x69False)False)(∀ x69 . x68 x69x63 x69(x63 x69False)False)(∀ x69 x70 . x13 x70x2 x69 x70(x11 x69False)False)(∀ x69 x70 . x13 x70x2 x69 x70(x63 x69False)False)(∀ x69 x70 . x62 x70x2 x69 (x4 x70)(x62 x69False)False)(∀ x69 . x68 x69(x13 x69False)False)(∀ x69 x70 . x62 x70x2 x69 x70(x12 x69False)False)(∀ x69 x70 . x41 x70x2 x69 (x4 x70)(x41 x69False)False)(∀ x69 . x15 x69x63 x69x11 x69(x58 x69False)False)(∀ x69 . x15 x69x63 x69x11 x69(x11 x69False)False)(∀ x69 . x15 x69x63 x69x11 x69(x63 x69False)False)(∀ x69 . x68 x69(x62 x69False)False)(∀ x69 . x12 x69(x41 x69False)False)(∀ x69 x70 . x15 x70x2 x69 (x4 x70)(x15 x69False)False)(∀ x69 . x63 x69x11 x69(x58 x69False)(x11 x69False)False)(∀ x69 . x63 x69x11 x69(x58 x69False)(x63 x69False)False)(∀ x69 . x63 x69x11 x69(x58 x69False)x15 x69False)(∀ x69 . (x12 x69False)x15 x69False)(∀ x69 . (x12 x69False)x41 x69(x18 x69False)False)(∀ x69 x70 . x68 x70x2 x69 (x4 x70)x55 x69 x70False)(∀ x69 . x68 x69x63 x69x11 x69(x58 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x11 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x63 x69False)False)(∀ x69 . x15 x69(x12 x69False)False)(∀ x69 . x18 x69(x41 x69False)False)(∀ x69 . x18 x69x12 x69False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 x70)x68 x69(x55 x69 x70False)False)(∀ x69 x70 . x63 x70x11 x70x2 x69 (x4 x70)(x11 x69False)False)(∀ x69 . x63 x69x11 x69x68 x69(x30 x69False)False)(∀ x69 . x63 x69x11 x69x68 x69(x11 x69False)False)(∀ x69 . x63 x69x11 x69x68 x69(x63 x69False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x4 x70)(x55 x69 x70False)x68 x69False)(∀ x69 . x68 x69x63 x69x11 x69(x21 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x11 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x63 x69False)False)(∀ x69 . x63 x69x11 x69x30 x69(x40 x69False)False)(∀ x69 . x63 x69x11 x69x30 x69(x11 x69False)False)(∀ x69 . x63 x69x11 x69x30 x69(x63 x69False)False)(∀ x69 x70 . x12 x70x2 x69 (x4 x70)(x12 x69False)False)(∀ x69 x70 . x68 x70x2 x69 (x4 x70)(x68 x69False)False)(∀ x69 . x68 x69(x11 x69False)False)(∀ x69 . x68 x69(x12 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x47 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x11 x69False)False)(∀ x69 . x68 x69x63 x69x11 x69(x63 x69False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x7 x69 x70x10 x69 x70(x24 x69 x70False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x7 x69 x70x10 x69 x70(x10 x69 x70False)False)(∀ x69 x70 . x1 x70x2 x69 (x4 (x4 (x3 x70)))x7 x69 x70x10 x69 x70(x7 x69 x70False)False)(∀ x69 x70 . x0 x69 x70x0 x70 x69False)(∀ x69 . x1 x69x27 x69(x69 = x66 (x3 x69) (x5 x69)False)False)(x7 x39 (x66 x38 (x9 x38 (x8 x38 x39)))x24 x39 (x66 x38 (x9 x38 (x8 x38 x39)))x2 x39 (x4 (x4 (x3 (x66 x38 (x9 x38 (x8 x38 x39))))))False)((x2 x39 (x4 (x4 x38))False)False)(x68 x38False)False
type
prop
theory
HotG
name
-
proof
PURos..
Megalodon
-
proofgold address
TMFPG..
creator
35128 PrPhD../9a4f4..
owner
35131 PrPhD../8bc7e..
term root
c3c1a..