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 . (x37 x42False)x26 x38x35 x38 x42 x36x27 x38 (x29 (x28 x42 x36))x26 x41x35 x41 x42 x36x27 x41 (x29 (x28 x42 x36))x27 x39 (x29 (x30 x42))x34 x40 x42x31 x42 x38 x41(x31 x42 (x33 x42 x38 x39 x40) (x32 x42 x41 x39 x40)False)False)(∀ x38 x39 . x37 x39(x39 = x38False)x37 x38False)(∀ x38 x39 . x25 x38 x39x37 x39False)(∀ x38 . x37 x38(x38 = x0False)False)(∀ x38 x39 x40 . x25 x38 x39x27 x39 (x29 x40)x37 x40False)(∀ x38 x39 x40 . x25 x39 x40x27 x40 (x29 x38)(x27 x39 x38False)False)(∀ x38 x39 . x24 x39 x38(x27 x39 (x29 x38)False)False)(∀ x38 x39 . x27 x39 (x29 x38)(x24 x39 x38False)False)(∀ x38 x39 . x27 x38 x39(x37 x39False)(x25 x38 x39False)False)(∀ x38 x39 . x25 x39 x38(x27 x39 x38False)False)(∀ x38 x39 x40 x41 x42 . (x37 x42False)x26 x38x35 x38 x42 x36x27 x38 (x29 (x28 x42 x36))x27 x41 (x29 (x30 x42))x34 x39 x42x34 x40 x42x22 x41 x42(x23 x42 x36 (x33 x42 (x33 x42 x38 x41 x39) x41 x40) (x33 x42 (x33 x42 x38 x41 x40) x41 x39)False)False)(∀ x38 x39 x40 x41 x42 . (x37 x42False)x26 x38x35 x38 x42 x36x27 x38 (x29 (x28 x42 x36))x26 x41x35 x41 x42 x36x27 x41 (x29 (x28 x42 x36))x27 x39 (x29 (x30 x42))x34 x40 x42x31 x42 x38 x41(x31 x42 (x33 x42 x38 x39 x40) (x33 x42 x41 x39 x40)False)False)(∀ x38 x39 x40 x41 . x26 x41x35 x41 x38 x39x27 x41 (x29 (x28 x38 x39))x26 x40x35 x40 x38 x39x27 x40 (x29 (x28 x38 x39))x23 x38 x39 x41 x40(x23 x38 x39 x40 x41False)False)(∀ x38 x39 x40 x41 . x26 x41x35 x41 x38 x39x27 x41 (x29 (x28 x38 x39))x26 x40x35 x40 x38 x39x27 x40 (x29 (x28 x38 x39))(x23 x38 x39 x41 x41False)False)(∀ x38 . (x24 x38 x38False)False)(∀ x38 x39 x40 . (x37 x40False)x26 x38x35 x38 x40 x36x27 x38 (x29 (x28 x40 x36))x26 x39x35 x39 x40 x36x27 x39 (x29 (x28 x40 x36))(x31 x40 x38 x38False)False)(∀ x38 x39 x40 x41 . x26 x41x35 x41 x38 x39x27 x41 (x29 (x28 x38 x39))x26 x40x35 x40 x38 x39x27 x40 (x29 (x28 x38 x39))x41 = x40(x23 x38 x39 x41 x40False)False)(∀ x38 x39 x40 x41 . x26 x41x35 x41 x38 x39x27 x41 (x29 (x28 x38 x39))x26 x40x35 x40 x38 x39x27 x40 (x29 (x28 x38 x39))x23 x38 x39 x41 x40(x41 = x40False)False)(∀ x38 . (x21 x38 = x29 x38False)False)(∀ x38 . (x30 x38 = x1 x38False)False)(∀ x38 . (x37 x38False)(x19 (x20 x38)False)False)(∀ x38 . (x37 x38False)x37 (x20 x38)False)(∀ x38 . (x37 x38False)(x34 (x20 x38) x38False)False)(∀ x38 . (x2 (x3 x38) x38False)False)(∀ x38 . x37 (x3 x38)False)(∀ x38 . (x27 (x3 x38) (x29 (x29 (x21 x38)))False)False)(x37 x18False)(∀ x38 . (x37 x38False)(x19 (x4 x38)False)False)(∀ x38 . (x37 x38False)x37 (x4 x38)False)(∀ x38 . (x37 x38False)(x34 (x4 x38) x38False)False)((x37 x17False)False)(∀ x38 . (x2 (x5 x38) x38False)False)(∀ x38 . (x27 (x5 x38) (x29 (x29 (x21 x38)))False)False)(x37 x36False)((x37 x0False)False)(∀ x38 . (x27 (x6 x38) x38False)False)(∀ x38 . (x34 (x16 x38) x38False)False)((x37 x7False)False)(∀ x38 x39 . x34 x39 x38(x27 x39 (x29 (x29 x38))False)False)(∀ x38 . (x27 (x21 x38) (x29 (x29 x38))False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x27 (x32 x41 x38 x40 x39) (x29 (x28 x41 x36))False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x35 (x32 x41 x38 x40 x39) x41 x36False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x26 (x32 x41 x38 x40 x39)False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x27 (x33 x41 x38 x40 x39) (x29 (x28 x41 x36))False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x35 (x33 x41 x38 x40 x39) x41 x36False)False)(∀ x38 x39 x40 x41 . (x37 x41False)x26 x38x35 x38 x41 x36x27 x38 (x29 (x28 x41 x36))x27 x40 (x29 (x30 x41))x34 x39 x41(x26 (x33 x41 x38 x40 x39)False)False)(∀ x38 . (x27 (x30 x38) (x29 (x29 (x21 x38)))False)False)(∀ x38 . (x2 (x30 x38) x38False)False)((x0 = x7False)False)(∀ x38 x39 . x27 x39 (x29 (x28 x38 x36))x26 x39x35 x39 x38 x36(x8 x39False)False)(∀ x38 x39 . x27 x39 (x29 (x28 x38 x36))x26 x39x35 x39 x38 x36(x35 x39 x38 x36False)False)(∀ x38 x39 . x27 x39 (x29 (x28 x38 x36))x26 x39x35 x39 x38 x36(x26 x39False)False)(∀ x38 . x27 x38 x36(x15 x38False)False)(∀ x38 x39 . x34 x39 x38(x19 x39False)False)(∀ x38 . x37 x38(x14 x38False)False)(∀ x38 x39 . (x37 x39False)x34 x38 x39x37 x38False)(∀ x38 x39 . x25 x38 x39x25 x39 x38False)(x31 x9 (x33 x9 (x33 x9 x10 x12 x11) x12 x13) (x33 x9 (x32 x9 x10 x12 x13) x12 x11)False)((x22 x12 x9False)False)((x34 x13 x9False)False)((x34 x11 x9False)False)((x27 x12 (x29 (x30 x9))False)False)((x27 x10 (x29 (x28 x9 x36))False)False)((x35 x10 x9 x36False)False)((x26 x10False)False)(x37 x9False)False
type
prop
theory
HotG
name
-
proof
PUWgR..
Megalodon
-
proofgold address
TMbz3..
creator
35121 PrPhD../f1c90..
owner
35124 PrPhD../e02df..
term root
1a260..