Search for blocks/addresses/...

Proofgold Address

address
PUbH3yxPe9oFFp3mrqBmY14JDh98HcLz2mz
total
0
mg
-
conjpub
-
current assets
4925b../8a12e.. bday: 21598 doc published by Pr4zB..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known 02702.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 x4 x5 x6 . (∀ x7 : ι → ο . x7 x1x7 x2x7 x3x7 x4x7 x5x7 x6∀ x8 . x0 x8x7 x8)x0 x1x0 x2x0 x3x0 x4x0 x5x0 x6∀ x7 : ι → ι → ι → ι → ο . (∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x2 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x3 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x3 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x4))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x4))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x5))(∀ x8 . x0 x8not (x7 x1 x8 x1 x8))(∀ x8 . x0 x8not (x7 x2 x8 x1 x8))(∀ x8 . x0 x8not (x7 x3 x8 x1 x8))(∀ x8 . x0 x8not (x7 x4 x8 x1 x8))(∀ x8 . x0 x8not (x7 x5 x8 x1 x8))(∀ x8 . x0 x8not (x7 x6 x8 x1 x8))(∀ x8 . x0 x8not (x7 x2 x8 x2 x8))(∀ x8 . x0 x8not (x7 x3 x8 x2 x8))(∀ x8 . x0 x8not (x7 x4 x8 x2 x8))(∀ x8 . x0 x8not (x7 x5 x8 x2 x8))(∀ x8 . x0 x8not (x7 x6 x8 x2 x8))(∀ x8 . x0 x8not (x7 x3 x8 x3 x8))(∀ x8 . x0 x8not (x7 x4 x8 x3 x8))(∀ x8 . x0 x8not (x7 x5 x8 x3 x8))(∀ x8 . x0 x8not (x7 x6 x8 x3 x8))(∀ x8 . x0 x8not (x7 x4 x8 x4 x8))(∀ x8 . x0 x8not (x7 x5 x8 x4 x8))(∀ x8 . x0 x8not (x7 x6 x8 x4 x8))(∀ x8 . x0 x8not (x7 x5 x8 x5 x8))(∀ x8 . x0 x8not (x7 x6 x8 x5 x8))(∀ x8 . x0 x8not (x7 x6 x8 x6 x8))∀ x8 : ι → ι → ι → ι → ο . (∀ x9 x10 x11 x12 . x0 x9x0 x10x0 x11x0 x12x8 x9 x10 x11 x12x8 x11 x12 x9 x10)(∀ x9 x10 . x0 x9x0 x10x8 x9 x10 x6 x6)(∀ x9 . x0 x9x8 x5 x5 x6 x9)(∀ x9 . x0 x9x8 x5 x6 x6 x9)x8 x1 x1 x1 x3x8 x1 x1 x1 x5x8 x1 x1 x2 x1x8 x1 x1 x2 x2x8 x1 x1 x2 x5x8 x1 x1 x3 x3x8 x1 x1 x3 x4x8 x1 x1 x3 x5x8 x1 x1 x4 x2x8 x1 x1 x4 x3x8 x1 x1 x4 x5x8 x1 x1 x5 x3x8 x1 x1 x5 x4x8 x1 x1 x6 x1x8 x1 x1 x6 x3x8 x1 x1 x6 x4x8 x1 x2 x1 x4x8 x1 x2 x1 x6x8 x1 x2 x2 x1x8 x1 x2 x2 x2x8 x1 x2 x2 x6x8 x1 x2 x3 x3x8 x1 x2 x3 x4x8 x1 x2 x3 x6x8 x1 x2 x4 x1x8 x1 x2 x4 x4x8 x1 x2 x4 x6x8 x1 x2 x5 x3x8 x1 x2 x5 x4x8 x1 x2 x6 x2x8 x1 x2 x6 x3x8 x1 x2 x6 x4x8 x1 x3 x1 x6x8 x1 x3 x2 x3x8 x1 x3 x2 x4x8 x1 x3 x2 x5x8 x1 x3 x3 x1x8 x1 x3 x3 x2x8 x1 x3 x3 x5x8 x1 x3 x4 x1x8 x1 x3 x4 x4x8 x1 x3 x4 x6x8 x1 x3 x5 x1x8 x1 x3 x5 x2x8 x1 x3 x6 x1x8 x1 x3 x6 x2x8 x1 x3 x6 x3x8 x1 x4 x1 x5x8 x1 x4 x2 x3x8 x1 x4 x2 x4x8 x1 x4 x2 x6x8 x1 x4 x3 x1x8 x1 x4 x3 x2x8 x1 x4 x3 x6x8 x1 x4 x4 x2x8 x1 x4 x4 x3x8 x1 x4 x4 x5x8 x1 x4 x5 x1x8 x1 x4 x5 x2x8 x1 x4 x6 x1x8 x1 x4 x6 x2x8 x1 x4 x6 x4x8 x1 x5 x2 x2x8 x1 x5 x2 x3x8 x1 x5 x3 x1x8 x1 x5 x3 x4x8 x1 x5 x3 x5x8 x1 x5 x3 x6x8 x1 x5 x4 x1x8 x1 x5 x4 x4x8 x1 x5 x4 x5x8 x1 x5 x4 x6x8 x1 x5 x5 x2x8 x1 x5 x5 x3x8 x1 x5 x6 x5x8 x1 x6 x2 x1x8 x1 x6 x2 x4x8 x1 x6 x3 x2x8 x1 x6 x3 x3x8 x1 x6 x3 x5x8 x1 x6 x3 x6x8 x1 x6 x4 x2x8 x1 x6 x4 x3x8 x1 x6 x4 x5x8 x1 x6 x4 x6x8 x1 x6 x5 x1x8 x1 x6 x5 x4x8 x1 x6 x6 x5x8 x2 x1 x2 x3x8 x2 x1 x2 x6x8 x2 x1 x3 x1x8 x2 x1 x3 x5x8 x2 x1 x4 x2x8 x2 x1 x4 x3x8 x2 x1 x4 x4x8 x2 x1 x4 x5x8 x2 x1 x5 x2x8 x2 x1 x5 x3x8 x2 x1 x5 x6x8 x2 x1 x6 x2x8 x2 x2 x2 x4x8 x2 x2 x2 x5x8 x2 x2 x3 x2x8 x2 x2 x3 x6x8 x2 x2 x4 x1x8 x2 x2 x4 x3x8 x2 x2 x4 x4x8 x2 x2 x4 x6x8 x2 x2 x5 x1x8 x2 x2 x5 x4x8 x2 x2 x5 x5x8 x2 x2 x6 x1x8 x2 x3 x2 x6x8 x2 x3 x3 x3x8 x2 x3 x3 x5x8 x2 x3 x4 x1x8 x2 x3 x4 x2x8 x2 x3 x4 x4x8 x2 x3 x4 x6x8 x2 x3 x5 x1x8 x2 x3 x5 x4x8 x2 x3 x5 x6x8 x2 x3 x6 x4x8 x2 x4 x2 x5x8 x2 x4 x3 x4x8 x2 x4 x3 x6x8 x2 x4 x4 x1x8 x2 x4 x4 x2x8 x2 x4 x4 x3x8 x2 x4 x4 x5x8 x2 x4 x5 x2x8 x2 x4 x5 x3x8 x2 x4 x5 x5x8 x2 x4 x6 x3x8 x2 x5 x2 x6x8 x2 x5 x3 x2x8 x2 x5 x3 x4x8 x2 x5 x4 x5x8 x2 x5 x4 x6x8 x2 x5 x5 x6x8 x2 x5 x6 x2x8 x2 x5 x6 x4x8 x2 x5 x6 x5x8 x2 x6 x3 x1x8 x2 x6 x3 x3x8 x2 x6 x4 x5x8 x2 x6 x4 x6x8 x2 x6 x5 x5x8 x2 x6 x6 x1x8 x2 x6 x6 x3x8 x2 x6 x6 x5x8 x3 x1 x3 x2x8 x3 x1 x3 x5x8 x3 x1 x4 x2x8 x3 x1 x4 x3x8 x3 x1 x4 x6x8 x3 x1 x5 x3x8 x3 x1 x5 x4x8 x3 x1 x6 x3x8 x3 x1 x6 x5x8 x3 x2 x3 x6x8 x3 x2 x4 x1x8 x3 x2 x4 x4x8 x3 x2 x4 x5x8 x3 x2 x5 x3x8 x3 x2 x5 x4x8 x3 x2 x6 x4x8 x3 x2 x6 x5x8 x3 x3 x3 x4x8 x3 x3 x3 x5x8 x3 x3 x4 x1x8 x3 x3 x4 x4x8 x3 x3 x4 x5x8 x3 x3 x5 x1x8 x3 x3 x5 x2x8 x3 x3 x6 x1x8 x3 x3 x6 x5x8 x3 x4 x3 x6x8 x3 x4 x4 x2x8 x3 x4 x4 x3x8 x3 x4 x4 x6x8 x3 x4 x5 x1x8 x3 x4 x5 x2x8 x3 x4 x6 x2x8 x3 x4 x6 x5x8 x3 x5 x1 x6x8 x3 x5 x3 x6x8 x3 x5 x5 x2x8 x3 x5 x5 x4x8 x3 x6 x5 x1x8 x3 x6 x5 x3x8 x4 x1 x4 x2x8 x4 x1 x4 x5x8 x4 x1 x5 x3x8 x4 x1 x5 x6x8 x4 x1 x6 x1x8 x4 x1 x6 x2x8 x4 x1 x6 x5x8 x4 x2 x4 x6x8 x4 x2 x5 x4x8 x4 x2 x5 x5x8 x4 x2 x6 x1x8 x4 x2 x6 x2x8 x4 x2 x6 x5x8 x4 x3 x4 x4x8 x4 x3 x4 x6x8 x4 x3 x5 x1x8 x4 x3 x5 x6x8 x4 x3 x6 x3x8 x4 x3 x6 x4x8 x4 x3 x6 x5x8 x4 x4 x4 x5x8 x4 x4 x5 x2x8 x4 x4 x5 x5x8 x4 x4 x6 x3x8 x4 x4 x6 x4x8 x4 x4 x6 x5x8 x4 x5 x1 x6x8 x4 x5 x2 x6x8 x4 x5 x6 x2x8 x4 x5 x6 x3x8 x4 x6 x6 x1x8 x4 x6 x6 x4x8 x5 x1 x5 x3x8 x5 x1 x5 x4x8 x5 x1 x5 x6x8 x5 x1 x6 x1x8 x5 x1 x6 x2x8 x5 x2 x5 x3x8 x5 x2 x5 x4x8 x5 x2 x5 x5x8 x5 x2 x6 x1x8 x5 x2 x6 x2x8 x5 x3 x5 x6x8 x5 x3 x6 x3x8 x5 x3 x6 x4x8 x5 x4 x5 x5x8 x5 x4 x6 x3x8 x5 x4 x6 x4x8 x5 x5 x2 x6x8 x6 x1 x6 x4x8 x6 x2 x6 x3x8 x6 x5 x1 x6x8 x6 x5 x2 x6x8 x6 x5 x5 x6∀ x9 . x0 x9∀ x10 . x0 x10∀ x11 . x0 x11x7 x6 x1 x9 x3x7 x9 x3 x10 x11not (x8 x6 x1 x9 x3)not (x8 x6 x1 x10 x11)not (x8 x9 x3 x10 x11)∀ x12 : ο . (x9 = x2x10 = x1x11 = x6x12)(x9 = x2x10 = x2x11 = x4x12)(x9 = x2x10 = x2x11 = x5x12)(x9 = x2x10 = x3x11 = x4x12)(x9 = x2x10 = x3x11 = x6x12)(x9 = x2x10 = x4x11 = x3x12)(x9 = x2x10 = x4x11 = x5x12)(x9 = x2x10 = x5x11 = x3x12)(x9 = x2x10 = x6x11 = x3x12)(x9 = x2x10 = x6x11 = x5x12)(x9 = x4x10 = x1x11 = x5x12)(x9 = x4x10 = x2x11 = x5x12)(x9 = x4x10 = x3x11 = x5x12)(x9 = x4x10 = x3x11 = x6x12)(x9 = x4x10 = x4x11 = x5x12)(x9 = x4x10 = x5x11 = x3x12)(x9 = x4x10 = x5x11 = x4x12)(x9 = x5x10 = x1x11 = x6x12)(x9 = x5x10 = x2x11 = x5x12)(x9 = x5x10 = x3x11 = x4x12)(x9 = x5x10 = x3x11 = x5x12)(x9 = x5x10 = x4x11 = x4x12)(x9 = x5x10 = x4x11 = x5x12)(x9 = x5x10 = x5x11 = x4x12)(x9 = x5x10 = x6x11 = x5x12)(x9 = x6x10 = x1x11 = x5x12)(x9 = x6x10 = x1x11 = x6x12)(x9 = x6x10 = x2x11 = x5x12)(x9 = x6x10 = x3x11 = x4x12)(x9 = x6x10 = x3x11 = x5x12)(x9 = x6x10 = x3x11 = x6x12)(x9 = x6x10 = x6x11 = x5x12)x12
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem 49b04.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 x4 x5 x6 . (∀ x7 : ι → ο . x7 x1x7 x2x7 x3x7 x4x7 x5x7 x6∀ x8 . x0 x8x7 x8)x0 x1x0 x2x0 x3x0 x4x0 x5x0 x6∀ x7 : ι → ι → ι → ι → ο . (∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x2 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x3 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x1))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x3 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x2))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x4 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x3))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x5 x9 x4))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x4))(∀ x8 . x0 x8∀ x9 . x0 x9not (x7 x8 x6 x9 x5))(∀ x8 . x0 x8not (x7 x1 x8 x1 x8))(∀ x8 . x0 x8not (x7 x2 x8 x1 x8))(∀ x8 . x0 x8not (x7 x3 x8 x1 x8))(∀ x8 . x0 x8not (x7 x4 x8 x1 x8))(∀ x8 . x0 x8not (x7 x5 x8 x1 x8))(∀ x8 . x0 x8not (x7 x6 x8 x1 x8))(∀ x8 . x0 x8not (x7 x2 x8 x2 x8))(∀ x8 . x0 x8not (x7 x3 x8 x2 x8))(∀ x8 . x0 x8not (x7 x4 x8 x2 x8))(∀ x8 . x0 x8not (x7 x5 x8 x2 x8))(∀ x8 . x0 x8not (x7 x6 x8 x2 x8))(∀ x8 . x0 x8not (x7 x3 x8 x3 x8))(∀ x8 . x0 x8not (x7 x4 x8 x3 x8))(∀ x8 . x0 x8not (x7 x5 x8 x3 x8))(∀ x8 . x0 x8not (x7 x6 x8 x3 x8))(∀ x8 . x0 x8not (x7 x4 x8 x4 x8))(∀ x8 . x0 x8not (x7 x5 x8 x4 x8))(∀ x8 . x0 x8not (x7 x6 x8 x4 x8))(∀ x8 . x0 x8not (x7 x5 x8 x5 x8))(∀ x8 . x0 x8not (x7 x6 x8 x5 x8))(∀ x8 . x0 x8not (x7 x6 x8 x6 x8))∀ x8 : ι → ι → ι → ι → ο . (∀ x9 x10 x11 x12 . x0 x9x0 x10x0 x11x0 x12x8 x9 x10 x11 x12x8 x11 x12 x9 x10)(∀ x9 x10 . x0 x9x0 x10x8 x9 x10 x6 x6)(∀ x9 . x0 x9x8 x5 x5 x6 x9)(∀ x9 . x0 x9x8 x5 x6 x6 x9)x8 x1 x1 x1 x3x8 x1 x1 x1 x5x8 x1 x1 x2 x1x8 x1 x1 x2 x2x8 x1 x1 x2 x5x8 x1 x1 x3 x3x8 x1 x1 x3 x4x8 x1 x1 x3 x5x8 x1 x1 x4 x2x8 x1 x1 x4 x3x8 x1 x1 x4 x5x8 x1 x1 x5 x3x8 x1 x1 x5 x4x8 x1 x1 x6 x1x8 x1 x1 x6 x3x8 x1 x1 x6 x4x8 x1 x2 x1 x4x8 x1 x2 x1 x6x8 x1 x2 x2 x1x8 x1 x2 x2 x2x8 x1 x2 x2 x6x8 x1 x2 x3 x3x8 x1 x2 x3 x4x8 x1 x2 x3 x6x8 x1 x2 x4 x1x8 x1 x2 x4 x4x8 x1 x2 x4 x6x8 x1 x2 x5 x3x8 x1 x2 x5 x4x8 x1 x2 x6 x2x8 x1 x2 x6 x3x8 x1 x2 x6 x4x8 x1 x3 x1 x6x8 x1 x3 x2 x3x8 x1 x3 x2 x4x8 x1 x3 x2 x5x8 x1 x3 x3 x1x8 x1 x3 x3 x2x8 x1 x3 x3 x5x8 x1 x3 x4 x1x8 x1 x3 x4 x4x8 x1 x3 x4 x6x8 x1 x3 x5 x1x8 x1 x3 x5 x2x8 x1 x3 x6 x1x8 x1 x3 x6 x2x8 x1 x3 x6 x3x8 x1 x4 x1 x5x8 x1 x4 x2 x3x8 x1 x4 x2 x4x8 x1 x4 x2 x6x8 x1 x4 x3 x1x8 x1 x4 x3 x2x8 x1 x4 x3 x6x8 x1 x4 x4 x2x8 x1 x4 x4 x3x8 x1 x4 x4 x5x8 x1 x4 x5 x1x8 x1 x4 x5 x2x8 x1 x4 x6 x1x8 x1 x4 x6 x2x8 x1 x4 x6 x4x8 x1 x5 x2 x2x8 x1 x5 x2 x3x8 x1 x5 x3 x1x8 x1 x5 x3 x4x8 x1 x5 x3 x5x8 x1 x5 x3 x6x8 x1 x5 x4 x1x8 x1 x5 x4 x4x8 x1 x5 x4 x5x8 x1 x5 x4 x6x8 x1 x5 x5 x2x8 x1 x5 x5 x3x8 x1 x5 x6 x5x8 x1 x6 x2 x1x8 x1 x6 x2 x4x8 x1 x6 x3 x2x8 x1 x6 x3 x3x8 x1 x6 x3 x5x8 x1 x6 x3 x6x8 x1 x6 x4 x2x8 x1 x6 x4 x3x8 x1 x6 x4 x5x8 x1 x6 x4 x6x8 x1 x6 x5 x1x8 x1 x6 x5 x4x8 x1 x6 x6 x5x8 x2 x1 x2 x3x8 x2 x1 x2 x6x8 x2 x1 x3 x1x8 x2 x1 x3 x5x8 x2 x1 x4 x2x8 x2 x1 x4 x3x8 x2 x1 x4 x4x8 x2 x1 x4 x5x8 x2 x1 x5 x2x8 x2 x1 x5 x3x8 x2 x1 x5 x6x8 x2 x1 x6 x2x8 x2 x2 x2 x4x8 x2 x2 x2 x5x8 x2 x2 x3 x2x8 x2 x2 x3 x6x8 x2 x2 x4 x1x8 x2 x2 x4 x3x8 x2 x2 x4 x4x8 x2 x2 x4 x6x8 x2 x2 x5 x1x8 x2 x2 x5 x4x8 x2 x2 x5 x5x8 x2 x2 x6 x1x8 x2 x3 x2 x6x8 x2 x3 x3 x3x8 x2 x3 x3 x5x8 x2 x3 x4 x1x8 x2 x3 x4 x2x8 x2 x3 x4 x4x8 x2 x3 x4 x6x8 x2 x3 x5 x1x8 x2 x3 x5 x4x8 x2 x3 x5 x6x8 x2 x3 x6 x4x8 x2 x4 x2 x5x8 x2 x4 x3 x4x8 x2 x4 x3 x6x8 x2 x4 x4 x1x8 x2 x4 x4 x2x8 x2 x4 x4 x3x8 x2 x4 x4 x5x8 x2 x4 x5 x2x8 x2 x4 x5 x3x8 x2 x4 x5 x5x8 x2 x4 x6 x3x8 x2 x5 x2 x6x8 x2 x5 x3 x2x8 x2 x5 x3 x4x8 x2 x5 x4 x5x8 x2 x5 x4 x6x8 x2 x5 x5 x6x8 x2 x5 x6 x2x8 x2 x5 x6 x4x8 x2 x5 x6 x5x8 x2 x6 x3 x1x8 x2 x6 x3 x3x8 x2 x6 x4 x5x8 x2 x6 x4 x6x8 x2 x6 x5 x5x8 x2 x6 x6 x1x8 x2 x6 x6 x3x8 x2 x6 x6 x5x8 x3 x1 x3 x2x8 x3 x1 x3 x5x8 x3 x1 x4 x2x8 x3 x1 x4 x3x8 x3 x1 x4 x6x8 x3 x1 x5 x3x8 x3 x1 x5 x4x8 x3 x1 x6 x3x8 x3 x1 x6 x5x8 x3 x2 x3 x6x8 x3 x2 x4 x1x8 x3 x2 x4 x4x8 x3 x2 x4 x5x8 x3 x2 x5 x3x8 x3 x2 x5 x4x8 x3 x2 x6 x4x8 x3 x2 x6 x5x8 x3 x3 x3 x4x8 x3 x3 x3 x5x8 x3 x3 x4 x1x8 x3 x3 x4 x4x8 x3 x3 x4 x5x8 x3 x3 x5 x1x8 x3 x3 x5 x2x8 x3 x3 x6 x1x8 x3 x3 x6 x5x8 x3 x4 x3 x6x8 x3 x4 x4 x2x8 x3 x4 x4 x3x8 x3 x4 x4 x6x8 x3 x4 x5 x1x8 x3 x4 x5 x2x8 x3 x4 x6 x2x8 x3 x4 x6 x5x8 x3 x5 x1 x6x8 x3 x5 x3 x6x8 x3 x5 x5 x2x8 x3 x5 x5 x4x8 x3 x6 x5 x1x8 x3 x6 x5 x3x8 x4 x1 x4 x2x8 x4 x1 x4 x5x8 x4 x1 x5 x3x8 x4 x1 x5 x6x8 x4 x1 x6 x1x8 x4 x1 x6 x2x8 x4 x1 x6 x5x8 x4 x2 x4 x6x8 x4 x2 x5 x4x8 x4 x2 x5 x5x8 x4 x2 x6 x1x8 x4 x2 x6 x2x8 x4 x2 x6 x5x8 x4 x3 x4 x4x8 x4 x3 x4 x6x8 x4 x3 x5 x1x8 x4 x3 x5 x6x8 x4 x3 x6 x3x8 x4 x3 x6 x4x8 x4 x3 x6 x5x8 x4 x4 x4 x5x8 x4 x4 x5 x2x8 x4 x4 x5 x5x8 x4 x4 x6 x3x8 x4 x4 x6 x4x8 x4 x4 x6 x5x8 x4 x5 x1 x6x8 x4 x5 x2 x6x8 x4 x5 x6 x2x8 x4 x5 x6 x3x8 x4 x6 x6 x1x8 x4 x6 x6 x4x8 x5 x1 x5 x3x8 x5 x1 x5 x4x8 x5 x1 x5 x6x8 x5 x1 x6 x1x8 x5 x1 x6 x2x8 x5 x2 x5 x3x8 x5 x2 x5 x4x8 x5 x2 x5 x5x8 x5 x2 x6 x1x8 x5 x2 x6 x2x8 x5 x3 x5 x6x8 x5 x3 x6 x3x8 x5 x3 x6 x4x8 x5 x4 x5 x5x8 x5 x4 x6 x3x8 x5 x4 x6 x4x8 x5 x5 x2 x6x8 x6 x1 x6 x4x8 x6 x2 x6 x3x8 x6 x5 x1 x6x8 x6 x5 x2 x6x8 x6 x5 x5 x6(x1 = x2∀ x9 : ο . x9)(x1 = x3∀ x9 : ο . x9)(x1 = x4∀ x9 : ο . x9)(x1 = x5∀ x9 : ο . x9)(x1 = x6∀ x9 : ο . x9)(x2 = x3∀ x9 : ο . x9)(x2 = x4∀ x9 : ο . x9)(x2 = x5∀ x9 : ο . x9)(x2 = x6∀ x9 : ο . x9)(x3 = x4∀ x9 : ο . x9)(x3 = x5∀ x9 : ο . x9)(x3 = x6∀ x9 : ο . x9)(x4 = x5∀ x9 : ο . x9)(x4 = x6∀ x9 : ο . x9)(x5 = x6∀ x9 : ο . x9)∀ x9 . x0 x9∀ x10 . x0 x10x7 x6 x1 x2 x3x7 x2 x3 x9 x10not (x8 x6 x1 x2 x3)not (x8 x6 x1 x9 x10)not (x8 x2 x3 x9 x10)∀ x11 . x0 x11∀ x12 . x0 x12x7 x9 x10 x11 x12not (x8 x6 x1 x11 x12)not (x8 x2 x3 x11 x12)not (x8 x9 x10 x11 x12)∀ x13 : ο . (x9 = x2x10 = x4x11 = x6x12 = x5x13)(x9 = x2x10 = x5x11 = x1x12 = x6x13)(x9 = x2x10 = x5x11 = x3x12 = x6x13)(x9 = x3x10 = x4x11 = x1x12 = x6x13)(x9 = x3x10 = x4x11 = x4x12 = x5x13)(x9 = x4x10 = x3x11 = x2x12 = x5x13)(x9 = x4x10 = x3x11 = x3x12 = x6x13)(x9 = x4x10 = x3x11 = x4x12 = x5x13)(x9 = x4x10 = x3x11 = x5x12 = x3x13)(x9 = x4x10 = x5x11 = x3x12 = x6x13)(x9 = x4x10 = x5x11 = x6x12 = x5x13)(x9 = x5x10 = x3x11 = x1x12 = x6x13)(x9 = x5x10 = x3x11 = x2x12 = x5x13)(x9 = x5x10 = x3x11 = x3x12 = x4x13)(x9 = x5x10 = x3x11 = x4x12 = x5x13)(x9 = x5x10 = x3x11 = x6x12 = x5x13)(x9 = x6x10 = x3x11 = x1x12 = x6x13)(x9 = x6x10 = x3x11 = x2x12 = x5x13)(x9 = x6x10 = x3x11 = x3x12 = x4x13)(x9 = x6x10 = x3x11 = x3x12 = x6x13)(x9 = x6x10 = x3x11 = x6x12 = x5x13)(x9 = x6x10 = x5x11 = x3x12 = x6x13)x13 (proof)

previous assets