Search for blocks/addresses/...

Proofgold Address

address
PUWP8aBpBuobs3NQUMhWAPrcLHWn3DaCuYb
total
0
mg
-
conjpub
-
current assets
46373../59312.. bday: 21030 doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known 56696.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)(∀ x8 . x0 x8not (x1 x8)∀ x9 : ι → ο . x9 x6x9 x7x9 x8)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7∀ x8 : ι → ι → ι → ι → ο . (∀ x9 . x0 x9∀ x10 . x0 x10not (x8 x9 x7 x10 x6))(∀ x9 . x0 x9not (x8 x2 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x2 x9))(∀ x9 . x0 x9not (x8 x4 x9 x2 x9))(∀ x9 . x0 x9not (x8 x5 x9 x2 x9))(∀ x9 . x0 x9not (x8 x6 x9 x2 x9))(∀ x9 . x0 x9not (x8 x7 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x3 x9))(∀ x9 . x0 x9not (x8 x5 x9 x3 x9))(∀ x9 . x0 x9not (x8 x6 x9 x3 x9))(∀ x9 . x0 x9not (x8 x7 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x4 x9))(∀ x9 . x0 x9not (x8 x6 x9 x4 x9))(∀ x9 . x0 x9not (x8 x7 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x5 x9))(∀ x9 . x0 x9not (x8 x7 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x7 x9))∀ x9 : ι → ι → ι → ι → ο . (∀ x10 x11 . x0 x10x0 x11x9 x10 x11 x7 x7)(∀ x10 . x0 x10x9 x6 x6 x7 x10)(∀ x10 . x0 x10x9 x6 x7 x7 x10)x9 x2 x6 x2 x7x9 x2 x6 x3 x6x9 x2 x6 x3 x7x9 x2 x6 x4 x6x9 x2 x6 x4 x7x9 x2 x6 x5 x6x9 x2 x6 x5 x7x9 x2 x6 x6 x6x9 x2 x6 x6 x7x9 x2 x6 x7 x6x9 x2 x7 x3 x7x9 x2 x7 x4 x7x9 x2 x7 x5 x7x9 x2 x7 x6 x7x9 x3 x6 x2 x7x9 x3 x6 x3 x7x9 x3 x6 x4 x6x9 x3 x6 x4 x7x9 x3 x6 x5 x6x9 x3 x6 x5 x7x9 x3 x6 x6 x6x9 x3 x6 x6 x7x9 x3 x6 x7 x6x9 x3 x7 x4 x7x9 x3 x7 x5 x7x9 x3 x7 x6 x7x9 x4 x6 x2 x7x9 x4 x6 x3 x7x9 x4 x6 x4 x7x9 x4 x6 x5 x6x9 x4 x6 x5 x7x9 x4 x6 x6 x6x9 x4 x6 x6 x7x9 x4 x6 x7 x6x9 x4 x7 x5 x7x9 x4 x7 x6 x7x9 x5 x6 x2 x7x9 x5 x6 x3 x7x9 x5 x6 x4 x7x9 x5 x6 x5 x7x9 x5 x6 x6 x6x9 x5 x6 x6 x7x9 x5 x6 x7 x6x9 x5 x7 x6 x7x9 x6 x6 x2 x7x9 x6 x6 x3 x7x9 x6 x6 x4 x7x9 x6 x6 x5 x7x9 x6 x6 x6 x7x9 x7 x6 x2 x7x9 x7 x6 x3 x7x9 x7 x6 x4 x7x9 x7 x6 x5 x7x9 x7 x6 x6 x7∀ x10 . x0 x10∀ x11 . x0 x11∀ x12 . x0 x12∀ x13 . x0 x13not (x1 x10)not (x1 x11)not (x1 x12)not (x1 x13)∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16∀ x17 . x0 x17x8 x14 x10 x15 x11x8 x15 x11 x16 x12x8 x16 x12 x17 x13not (x9 x14 x10 x15 x11)not (x9 x14 x10 x16 x12)not (x9 x14 x10 x17 x13)not (x9 x15 x11 x16 x12)not (x9 x15 x11 x17 x13)not (x9 x16 x12 x17 x13)∀ x18 : ο . (x14 = x2x10 = x6x15 = x3x11 = x6x16 = x6x12 = x6x17 = x2x13 = x7x18)(x14 = x4x10 = x6x15 = x5x11 = x6x16 = x6x12 = x6x17 = x5x13 = x7x18)(x14 = x4x10 = x6x15 = x5x11 = x6x16 = x6x12 = x6x17 = x6x13 = x7x18)(x14 = x4x10 = x6x15 = x5x11 = x6x16 = x7x12 = x6x17 = x5x13 = x7x18)(x14 = x2x10 = x6x15 = x6x11 = x6x16 = x2x12 = x7x17 = x6x13 = x7x18)(x14 = x4x10 = x6x15 = x5x11 = x6x16 = x5x12 = x7x17 = x6x13 = x7x18)(x14 = x4x10 = x6x15 = x6x11 = x6x16 = x5x12 = x7x17 = x6x13 = x7x18)(x14 = x5x10 = x6x15 = x6x11 = x6x16 = x4x12 = x7x17 = x5x13 = x7x18)(x14 = x5x10 = x6x15 = x6x11 = x6x16 = x4x12 = x7x17 = x6x13 = x7x18)(x14 = x5x10 = x6x15 = x6x11 = x6x16 = x5x12 = x7x17 = x6x13 = x7x18)(x14 = x5x10 = x6x15 = x7x11 = x6x16 = x4x12 = x7x17 = x5x13 = x7x18)(x14 = x2x10 = x6x15 = x2x11 = x7x16 = x3x12 = x7x17 = x6x13 = x7x18)(x14 = x5x10 = x6x15 = x4x11 = x7x16 = x5x12 = x7x17 = x6x13 = x7x18)(x14 = x6x10 = x6x15 = x4x11 = x7x16 = x5x12 = x7x17 = x6x13 = x7x18)x18
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem d55c8.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)(∀ x8 . x0 x8not (x1 x8)∀ x9 : ι → ο . x9 x6x9 x7x9 x8)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7∀ x8 : ι → ι → ι → ι → ο . (∀ x9 . x0 x9∀ x10 . x0 x10not (x8 x9 x7 x10 x6))(∀ x9 . x0 x9not (x8 x2 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x2 x9))(∀ x9 . x0 x9not (x8 x4 x9 x2 x9))(∀ x9 . x0 x9not (x8 x5 x9 x2 x9))(∀ x9 . x0 x9not (x8 x6 x9 x2 x9))(∀ x9 . x0 x9not (x8 x7 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x3 x9))(∀ x9 . x0 x9not (x8 x5 x9 x3 x9))(∀ x9 . x0 x9not (x8 x6 x9 x3 x9))(∀ x9 . x0 x9not (x8 x7 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x4 x9))(∀ x9 . x0 x9not (x8 x6 x9 x4 x9))(∀ x9 . x0 x9not (x8 x7 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x5 x9))(∀ x9 . x0 x9not (x8 x7 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x7 x9))∀ x9 : ι → ι → ι → ι → ο . (∀ x10 x11 . x0 x10x0 x11x9 x10 x11 x7 x7)(∀ x10 . x0 x10x9 x6 x6 x7 x10)(∀ x10 . x0 x10x9 x6 x7 x7 x10)x9 x2 x6 x2 x7x9 x2 x6 x3 x6x9 x2 x6 x3 x7x9 x2 x6 x4 x6x9 x2 x6 x4 x7x9 x2 x6 x5 x6x9 x2 x6 x5 x7x9 x2 x6 x6 x6x9 x2 x6 x6 x7x9 x2 x6 x7 x6x9 x2 x7 x3 x7x9 x2 x7 x4 x7x9 x2 x7 x5 x7x9 x2 x7 x6 x7x9 x3 x6 x2 x7x9 x3 x6 x3 x7x9 x3 x6 x4 x6x9 x3 x6 x4 x7x9 x3 x6 x5 x6x9 x3 x6 x5 x7x9 x3 x6 x6 x6x9 x3 x6 x6 x7x9 x3 x6 x7 x6x9 x3 x7 x4 x7x9 x3 x7 x5 x7x9 x3 x7 x6 x7x9 x4 x6 x2 x7x9 x4 x6 x3 x7x9 x4 x6 x4 x7x9 x4 x6 x5 x6x9 x4 x6 x5 x7x9 x4 x6 x6 x6x9 x4 x6 x6 x7x9 x4 x6 x7 x6x9 x4 x7 x5 x7x9 x4 x7 x6 x7x9 x5 x6 x2 x7x9 x5 x6 x3 x7x9 x5 x6 x4 x7x9 x5 x6 x5 x7x9 x5 x6 x6 x6x9 x5 x6 x6 x7x9 x5 x6 x7 x6x9 x5 x7 x6 x7x9 x6 x6 x2 x7x9 x6 x6 x3 x7x9 x6 x6 x4 x7x9 x6 x6 x5 x7x9 x6 x6 x6 x7x9 x7 x6 x2 x7x9 x7 x6 x3 x7x9 x7 x6 x4 x7x9 x7 x6 x5 x7x9 x7 x6 x6 x7(∀ x10 x11 . x0 x10x0 x11x9 x10 x11 x10 x11)(∀ x10 x11 x12 x13 . x0 x10x0 x11x0 x12x0 x13x9 x10 x11 x12 x13x9 x12 x13 x10 x11)(x4 = x5∀ x10 : ο . x10)(x5 = x6∀ x10 : ο . x10)(x6 = x7∀ x10 : ο . x10)∀ x10 . x0 x10∀ x11 . x0 x11∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16∀ x17 . x0 x17∀ x18 . x0 x18∀ x19 . x0 x19not (x1 x11)not (x1 x13)not (x1 x15)not (x1 x17)not (x1 x19)x8 x10 x11 x12 x13x8 x12 x13 x14 x15x8 x14 x15 x16 x17x8 x16 x17 x18 x19not (x9 x10 x11 x12 x13)not (x9 x10 x11 x14 x15)not (x9 x10 x11 x16 x17)not (x9 x10 x11 x18 x19)not (x9 x12 x13 x14 x15)not (x9 x12 x13 x16 x17)not (x9 x12 x13 x18 x19)not (x9 x14 x15 x16 x17)not (x9 x14 x15 x18 x19)not (x9 x16 x17 x18 x19)∀ x20 : ο . (x10 = x4x11 = x6x12 = x5x13 = x6x14 = x6x15 = x6x16 = x5x17 = x7x18 = x6x19 = x7x20)(x10 = x5x11 = x6x12 = x6x13 = x6x14 = x4x15 = x7x16 = x5x17 = x7x18 = x6x19 = x7x20)x20 (proof)
Theorem 807bb.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)(∀ x8 . x0 x8not (x1 x8)∀ x9 : ι → ο . x9 x6x9 x7x9 x8)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7∀ x8 : ι → ι → ι → ι → ο . (∀ x9 . x0 x9∀ x10 . x0 x10not (x8 x9 x7 x10 x6))(∀ x9 . x0 x9not (x8 x2 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x2 x9))(∀ x9 . x0 x9not (x8 x4 x9 x2 x9))(∀ x9 . x0 x9not (x8 x5 x9 x2 x9))(∀ x9 . x0 x9not (x8 x6 x9 x2 x9))(∀ x9 . x0 x9not (x8 x7 x9 x2 x9))(∀ x9 . x0 x9not (x8 x3 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x3 x9))(∀ x9 . x0 x9not (x8 x5 x9 x3 x9))(∀ x9 . x0 x9not (x8 x6 x9 x3 x9))(∀ x9 . x0 x9not (x8 x7 x9 x3 x9))(∀ x9 . x0 x9not (x8 x4 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x4 x9))(∀ x9 . x0 x9not (x8 x6 x9 x4 x9))(∀ x9 . x0 x9not (x8 x7 x9 x4 x9))(∀ x9 . x0 x9not (x8 x5 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x5 x9))(∀ x9 . x0 x9not (x8 x7 x9 x5 x9))(∀ x9 . x0 x9not (x8 x6 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x6 x9))(∀ x9 . x0 x9not (x8 x7 x9 x7 x9))∀ x9 : ι → ι → ι → ι → ο . (∀ x10 x11 . x0 x10x0 x11x9 x10 x11 x7 x7)(∀ x10 . x0 x10x9 x6 x6 x7 x10)(∀ x10 . x0 x10x9 x6 x7 x7 x10)x9 x2 x6 x2 x7x9 x2 x6 x3 x6x9 x2 x6 x3 x7x9 x2 x6 x4 x6x9 x2 x6 x4 x7x9 x2 x6 x5 x6x9 x2 x6 x5 x7x9 x2 x6 x6 x6x9 x2 x6 x6 x7x9 x2 x6 x7 x6x9 x2 x7 x3 x7x9 x2 x7 x4 x7x9 x2 x7 x5 x7x9 x2 x7 x6 x7x9 x3 x6 x2 x7x9 x3 x6 x3 x7x9 x3 x6 x4 x6x9 x3 x6 x4 x7x9 x3 x6 x5 x6x9 x3 x6 x5 x7x9 x3 x6 x6 x6x9 x3 x6 x6 x7x9 x3 x6 x7 x6x9 x3 x7 x4 x7x9 x3 x7 x5 x7x9 x3 x7 x6 x7x9 x4 x6 x2 x7x9 x4 x6 x3 x7x9 x4 x6 x4 x7x9 x4 x6 x5 x6x9 x4 x6 x5 x7x9 x4 x6 x6 x6x9 x4 x6 x6 x7x9 x4 x6 x7 x6x9 x4 x7 x5 x7x9 x4 x7 x6 x7x9 x5 x6 x2 x7x9 x5 x6 x3 x7x9 x5 x6 x4 x7x9 x5 x6 x5 x7x9 x5 x6 x6 x6x9 x5 x6 x6 x7x9 x5 x6 x7 x6x9 x5 x7 x6 x7x9 x6 x6 x2 x7x9 x6 x6 x3 x7x9 x6 x6 x4 x7x9 x6 x6 x5 x7x9 x6 x6 x6 x7x9 x7 x6 x2 x7x9 x7 x6 x3 x7x9 x7 x6 x4 x7x9 x7 x6 x5 x7x9 x7 x6 x6 x7(∀ x10 x11 . x0 x10x0 x11x9 x10 x11 x10 x11)(∀ x10 x11 x12 x13 . x0 x10x0 x11x0 x12x0 x13x9 x10 x11 x12 x13x9 x12 x13 x10 x11)(x4 = x5∀ x10 : ο . x10)(x5 = x6∀ x10 : ο . x10)(x6 = x7∀ x10 : ο . x10)∀ x10 . x0 x10∀ x11 . x0 x11∀ x12 . x0 x12∀ x13 . x0 x13∀ x14 . x0 x14∀ x15 . x0 x15∀ x16 . x0 x16∀ x17 . x0 x17∀ x18 . x0 x18∀ x19 . x0 x19∀ x20 . x0 x20∀ x21 . x0 x21not (x1 x11)not (x1 x13)not (x1 x15)not (x1 x17)not (x1 x19)not (x1 x21)x8 x10 x11 x12 x13x8 x12 x13 x14 x15x8 x14 x15 x16 x17x8 x16 x17 x18 x19x8 x18 x19 x20 x21not (x9 x10 x11 x12 x13)not (x9 x10 x11 x14 x15)not (x9 x10 x11 x16 x17)not (x9 x10 x11 x18 x19)not (x9 x10 x11 x20 x21)not (x9 x12 x13 x14 x15)not (x9 x12 x13 x16 x17)not (x9 x12 x13 x18 x19)not (x9 x12 x13 x20 x21)not (x9 x14 x15 x16 x17)not (x9 x14 x15 x18 x19)not (x9 x14 x15 x20 x21)not (x9 x16 x17 x18 x19)not (x9 x16 x17 x20 x21)not (x9 x18 x19 x20 x21)False (proof)

previous assets