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 . x57 x59(x59 = x58False)x57 x58False)(∀ x58 x59 . x0 x58 x59x57 x59False)(∀ x58 . x57 x58(x58 = x56False)False)(∀ x58 x59 x60 . x0 x58 x59x2 x59 (x1 x60)x57 x60False)(∀ x58 x59 x60 . x0 x59 x60x2 x60 (x1 x58)(x2 x59 x58False)False)(∀ x58 . (x3 x56 x58 = x56False)False)(∀ x58 x59 . x55 x59 x58(x2 x59 (x1 x58)False)False)(∀ x58 x59 . x2 x59 (x1 x58)(x55 x59 x58False)False)(∀ x58 . (x3 x58 x56 = x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58x7 x58 (x6 x58) = x8 x58 (x7 x58 (x6 x58))(x9 x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x54 (x6 x58) x58False)(x9 x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x2 (x6 x58) (x1 (x11 x58))False)(x9 x58False)False)(∀ x58 x59 . (x4 x59False)x10 x59x5 x59x9 x59x2 x58 (x1 (x11 x59))x54 x58 x59(x7 x59 x58 = x8 x59 (x7 x59 x58)False)False)(∀ x58 x59 . x2 x58 x59(x57 x59False)(x0 x58 x59False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58x53 (x8 x58 (x52 x58)) x58(x9 x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x53 (x52 x58) x58False)(x9 x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x2 (x52 x58) (x1 (x11 x58))False)(x9 x58False)False)(∀ x58 x59 . (x4 x59False)x10 x59x5 x59x9 x59x2 x58 (x1 (x11 x59))x53 x58 x59(x53 (x8 x59 x58) x59False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))(x7 x59 x58 = x51 (x11 x59) (x8 x59 (x51 (x11 x59) x58))False)False)(∀ x58 x59 . x0 x59 x58(x2 x59 x58False)False)(x57 x50False)(∀ x58 . (x55 x58 x58False)False)(∀ x58 . x10 x58x5 x58(x49 (x48 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x2 (x48 x58) (x1 (x11 x58))False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x53 (x47 x58) x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58x57 (x47 x58)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x2 (x47 x58) (x1 (x11 x58))False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58x13 (x12 x58) x58False)(∀ x58 . (x4 x58False)x10 x58x5 x58x57 (x12 x58)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x2 (x12 x58) (x1 (x11 x58))False)False)(∀ x58 . (x46 x58False)x46 (x45 x58)False)(∀ x58 . (x46 x58False)(x2 (x45 x58) (x1 x58)False)False)(∀ x58 . x10 x58x5 x58(x53 (x44 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x2 (x44 x58) (x1 (x11 x58))False)False)(∀ x58 . x5 x58(x13 (x43 x58) x58False)False)(∀ x58 . x5 x58(x2 (x43 x58) (x1 (x11 x58))False)False)(∀ x58 . (x57 x58False)(x46 (x42 x58)False)False)(∀ x58 . (x57 x58False)x57 (x42 x58)False)(∀ x58 . (x57 x58False)(x2 (x42 x58) (x1 x58)False)False)(∀ x58 . x5 x58(x15 (x14 x58) x58False)False)(∀ x58 . x5 x58(x2 (x14 x58) (x1 (x11 x58))False)False)(∀ x58 . (x57 x58False)(x17 (x16 x58) x58False)False)(∀ x58 . (x57 x58False)(x2 (x16 x58) (x1 x58)False)False)(∀ x58 . (x4 x58False)x19 x58x57 (x18 x58)False)(∀ x58 . (x4 x58False)x19 x58(x2 (x18 x58) (x1 (x11 x58))False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x53 (x20 x58) x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x54 (x20 x58) x58False)False)(∀ x58 . (x4 x58False)x10 x58x5 x58x57 (x20 x58)False)(∀ x58 . (x4 x58False)x10 x58x5 x58(x2 (x20 x58) (x1 (x11 x58))False)False)(∀ x58 . x17 (x21 x58) x58False)(∀ x58 . (x2 (x21 x58) (x1 x58)False)False)(x57 x22False)(∀ x58 . x10 x58x5 x58(x53 (x41 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x54 (x41 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x2 (x41 x58) (x1 (x11 x58))False)False)(∀ x58 . (x57 (x23 x58)False)False)(∀ x58 . (x2 (x23 x58) (x1 x58)False)False)(∀ x58 . (x24 x58False)x19 x58x46 (x25 x58)False)(∀ x58 . (x24 x58False)x19 x58(x2 (x25 x58) (x1 (x11 x58))False)False)(∀ x58 . (x4 x58False)x19 x58(x46 (x26 x58)False)False)(∀ x58 . (x4 x58False)x19 x58x57 (x26 x58)False)(∀ x58 . (x4 x58False)x19 x58(x2 (x26 x58) (x1 (x11 x58))False)False)((x57 x40False)False)(∀ x58 . x10 x58x5 x58(x54 (x27 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x2 (x27 x58) (x1 (x11 x58))False)False)(∀ x58 . (x57 x58False)x57 (x28 x58)False)(∀ x58 . (x57 x58False)(x2 (x28 x58) (x1 x58)False)False)(∀ x58 . x10 x58x5 x58(x54 (x29 x58) x58False)False)(∀ x58 . x10 x58x5 x58(x2 (x29 x58) (x1 (x11 x58))False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))(x7 x59 (x7 x59 x58) = x7 x59 x58False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))(x8 x59 (x8 x59 x58) = x8 x59 x58False)False)(∀ x58 x59 . x2 x58 (x1 x59)(x51 x59 (x51 x59 x58) = x58False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))(x54 (x8 x59 x58) x59False)False)(∀ x58 . (x30 x58False)x19 x58x31 (x11 x58)False)(∀ x58 . x30 x58x19 x58(x31 (x11 x58)False)False)(∀ x58 . x24 x58x19 x58(x46 (x11 x58)False)False)(∀ x58 . (x24 x58False)x19 x58x46 (x11 x58)False)(∀ x58 x59 . x10 x59x5 x59x54 x58 x59x2 x58 (x1 (x11 x59))(x53 (x51 (x11 x59) x58) x59False)False)(∀ x58 x59 . x10 x59x5 x59x53 x58 x59x2 x58 (x1 (x11 x59))(x54 (x51 (x11 x59) x58) x59False)False)(∀ x58 . (x4 x58False)x19 x58x57 (x11 x58)False)((x57 x56False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))(x53 (x7 x59 x58) x59False)False)(∀ x58 . x57 (x1 x58)False)(∀ x58 . x4 x58x19 x58(x57 (x11 x58)False)False)(∀ x58 x59 . x10 x59x5 x59x49 x58 x59x2 x58 (x1 (x11 x59))(x15 (x51 (x11 x59) x58) x59False)False)(∀ x58 x59 . x5 x59x13 x58 x59x2 x58 (x1 (x11 x59))(x57 (x8 x59 x58)False)False)(∀ x58 . (x2 (x39 x58) x58False)False)((x19 x32False)False)((x5 x38False)False)((x57 x33False)False)(∀ x58 . x5 x58(x19 x58False)False)(∀ x58 x59 . x2 x59 (x1 x58)(x2 (x51 x58 x59) (x1 x58)False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))(x2 (x7 x59 x58) (x1 (x11 x59))False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))(x2 (x8 x59 x58) (x1 (x11 x59))False)False)(∀ x58 x59 . x2 x59 (x1 x58)(x51 x58 x59 = x3 x58 x59False)False)((x56 = x33False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))(x8 x59 x58 = x51 (x11 x59) (x7 x59 (x51 (x11 x59) x58))False)False)(∀ x58 . x19 x58x34 x58 x56(x4 x58False)False)(∀ x58 . x5 x58x4 x58(x37 x58False)False)(∀ x58 . x19 x58x4 x58(x34 x58 x56False)False)(∀ x58 . x19 x58(x30 x58False)x24 x58False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x54 x58 x59x49 x58 x59(x57 x58False)False)(∀ x58 . x19 x58x24 x58(x30 x58False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x53 x58 x59x13 x58 x59(x49 x58 x59False)False)(∀ x58 x59 . x46 x59x2 x58 (x1 x59)(x46 x58False)False)(∀ x58 . x19 x58(x30 x58False)x30 x58False)(∀ x58 . x19 x58(x30 x58False)x4 x58False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x49 x58 x59(x13 x58 x59False)False)(∀ x58 x59 . x57 x59x2 x58 (x1 x59)x17 x58 x59False)(∀ x58 . x19 x58x4 x58(x30 x58False)False)(∀ x58 . x19 x58x4 x58(x4 x58False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x57 x58(x49 x58 x59False)False)(∀ x58 x59 . (x57 x59False)x2 x58 (x1 x59)x57 x58(x17 x58 x59False)False)(∀ x58 x59 . x5 x59x2 x58 (x1 (x11 x59))x57 x58(x13 x58 x59False)False)(∀ x58 x59 . (x57 x59False)x2 x58 (x1 x59)(x17 x58 x59False)x57 x58False)(∀ x58 . x19 x58(x24 x58False)x4 x58False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x57 x58(x53 x58 x59False)False)(∀ x58 x59 . x10 x59x5 x59x2 x58 (x1 (x11 x59))x57 x58(x54 x58 x59False)False)(∀ x58 x59 . x57 x59x2 x58 (x1 x59)(x57 x58False)False)(∀ x58 . x19 x58x4 x58(x24 x58False)False)(∀ x58 . x19 x58(x24 x58False)x4 x58False)(∀ x58 . x19 x58x34 x58 x50(x24 x58False)False)(∀ x58 . x19 x58x34 x58 x50x4 x58False)(∀ x58 . x19 x58(x4 x58False)x24 x58(x34 x58 x50False)False)(∀ x58 x59 . x0 x58 x59x0 x59 x58False)(∀ x58 . x2 x58 (x1 (x11 x35))x53 x58 x35(x8 x35 x58 = x7 x35 (x8 x35 x58)False)(x9 x35False)False)(x9 x35x8 x35 x36 = x7 x35 (x8 x35 x36)False)(x9 x35(x53 x36 x35False)False)(x9 x35(x2 x36 (x1 (x11 x35))False)False)((x5 x35False)False)((x10 x35False)False)(x4 x35False)False
type
prop
theory
HotG
name
-
proof
PUWpU..
Megalodon
-
proofgold address
TMUQy..
creator
35124 PrPhD../daacd..
owner
35125 PrPhD../6f396..
term root
1176d..