Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9)(∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5∀ x9 . x1 x9x8 x9)(∀ x8 . x0 x8not (x1 x8)∀ x9 : ι → ο . x9 x6x9 x7x9 x8)x0 x2x0 x3x0 x4x0 x5x0 x6x0 x7x1 x2x1 x3x1 x4x1 x5not (x1 x6)not (x1 x7)(x2 = x3∀ x8 : ο . x8)(x2 = x4∀ x8 : ο . x8)(x2 = x5∀ x8 : ο . x8)(x2 = x6∀ x8 : ο . x8)(x2 = x7∀ x8 : ο . x8)(x3 = x4∀ x8 : ο . x8)(x3 = x5∀ x8 : ο . x8)(x3 = x6∀ x8 : ο . x8)(x3 = x7∀ x8 : ο . x8)(x4 = x5∀ x8 : ο . x8)(x4 = x6∀ x8 : ο . x8)(x4 = x7∀ x8 : ο . x8)(x5 = x6∀ x8 : ο . x8)(x5 = x7∀ x8 : ο . x8)(x6 = x7∀ x8 : ο . x8)∀ x8 x9 x10 : ι → ι → ι . (∀ x11 . x0 x11∀ x12 . x0 x12x0 (x8 x11 x12))(∀ x11 . x0 x11∀ x12 . x1 x12x1 (x8 x11 x12))(∀ x11 . x0 x11∀ x12 . x0 x12x8 x11 (x8 x11 x12) = x12)(∀ x11 . x0 x11x8 x11 x2 = x3)(∀ x11 . x0 x11∀ x12 . x0 x12x0 (x9 x11 x12))(∀ x11 . x0 x11∀ x12 . x1 x12x1 (x9 x11 x12))(∀ x11 . x0 x11∀ x12 . x0 x12x9 x11 (x9 x11 x12) = x12)(∀ x11 . x0 x11x9 x11 x2 = x4)(∀ x11 . x0 x11∀ x12 . x0 x12x0 (x10 x11 x12))(∀ x11 . x0 x11∀ x12 . x1 x12x1 (x10 x11 x12))(∀ x11 . x0 x11∀ x12 . x0 x12x10 x11 (x10 x11 x12) = x12)(∀ x11 . x0 x11x10 x11 x2 = x5)∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . not (x11 x12 x13 x12 x13))(∀ x12 x13 x14 x15 x16 x17 . x0 x16x0 x17x11 x12 x13 x14 x15x11 x14 x15 x16 x17x11 x12 x13 x16 x17)(∀ x12 . x0 x12∀ x13 . x1 x13∀ x14 . x0 x14∀ x15 . x0 x15not (x1 x15)x11 x12 x13 x14 x15)(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x3 x13 x2))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x4 x13 x2))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x5 x13 x2))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x6 x13 x2))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x7 x13 x2))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x4 x13 x3))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x5 x13 x3))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x6 x13 x3))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x7 x13 x3))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x5 x13 x4))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x6 x13 x4))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x7 x13 x4))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x6 x13 x5))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x7 x13 x5))(∀ x12 . x0 x12∀ x13 . x0 x13not (x11 x12 x7 x13 x6))(∀ x12 . x0 x12not (x11 x2 x12 x2 x12))(∀ x12 . x0 x12not (x11 x3 x12 x2 x12))(∀ x12 . x0 x12not (x11 x4 x12 x2 x12))(∀ x12 . x0 x12not (x11 x5 x12 x2 x12))(∀ x12 . x0 x12not (x11 x6 x12 x2 x12))(∀ x12 . x0 x12not (x11 x7 x12 x2 x12))(∀ x12 . x0 x12not (x11 x3 x12 x3 x12))(∀ x12 . x0 x12not (x11 x4 x12 x3 x12))(∀ x12 . x0 x12not (x11 x5 x12 x3 x12))(∀ x12 . x0 x12not (x11 x6 x12 x3 x12))(∀ x12 . x0 x12not (x11 x7 x12 x3 x12))(∀ x12 . x0 x12not (x11 x4 x12 x4 x12))(∀ x12 . x0 x12not (x11 x5 x12 x4 x12))(∀ x12 . x0 x12not (x11 x6 x12 x4 x12))(∀ x12 . x0 x12not (x11 x7 x12 x4 x12))(∀ x12 . x0 x12not (x11 x5 x12 x5 x12))(∀ x12 . x0 x12not (x11 x6 x12 x5 x12))(∀ x12 . x0 x12not (x11 x7 x12 x5 x12))(∀ x12 . x0 x12not (x11 x6 x12 x6 x12))(∀ x12 . x0 x12not (x11 x7 x12 x6 x12))(∀ x12 . x0 x12not (x11 x7 x12 x7 x12))∀ x12 : ι → ι → ι → ι → ο . (∀ x13 x14 x15 x16 . x0 x13x0 x14x0 x15x0 x16∀ x17 : ο . (x11 x13 x14 x15 x16x17)(x12 x13 x14 x15 x16x17)(x11 x15 x16 x13 x14x17)x17)(∀ x13 x14 x15 x16 . x0 x13x0 x14x0 x15x0 x16not (x12 x13 x14 x15 x16)not (x12 x13 (x8 x13 x14) x15 (x8 x15 x16)))(∀ x13 x14 x15 x16 . x0 x13x0 x14x0 x15x0 x16not (x12 x13 x14 x15 x16)not (x12 x13 (x9 x13 x14) x15 (x9 x15 x16)))(∀ x13 x14 x15 x16 . x0 x13x0 x14x0 x15x0 x16not (x12 x13 x14 x15 x16)not (x12 x13 (x10 x13 x14) x15 (x10 x15 x16)))(∀ x13 x14 . x0 x13x0 x14x12 x13 x14 x13 x14)(∀ x13 x14 x15 x16 . x0 x13x0 x14x0 x15x0 x16x12 x13 x14 x15 x16x12 x15 x16 x13 x14)(∀ x13 x14 . x0 x13x0 x14x12 x13 x14 x7 x7)(∀ x13 . x0 x13x12 x6 x6 x7 x13)(∀ x13 . x0 x13x12 x6 x7 x7 x13)x12 x2 x2 x2 x4x12 x2 x2 x2 x6x12 x2 x2 x3 x2x12 x2 x2 x3 x3x12 x2 x2 x3 x6x12 x2 x2 x4 x4x12 x2 x2 x4 x5x12 x2 x2 x4 x6x12 x2 x2 x5 x3x12 x2 x2 x5 x4x12 x2 x2 x5 x6x12 x2 x2 x6 x4x12 x2 x2 x6 x5x12 x2 x2 x7 x2x12 x2 x2 x7 x4x12 x2 x2 x7 x5x12 x2 x3 x2 x5x12 x2 x3 x2 x7x12 x2 x3 x3 x2x12 x2 x3 x3 x3x12 x2 x3 x3 x7x12 x2 x3 x4 x4x12 x2 x3 x4 x5x12 x2 x3 x4 x7x12 x2 x3 x5 x2x12 x2 x3 x5 x5x12 x2 x3 x5 x7x12 x2 x3 x6 x4x12 x2 x3 x6 x5x12 x2 x3 x7 x3x12 x2 x3 x7 x4x12 x2 x3 x7 x5x12 x2 x4 x2 x7x12 x2 x4 x3 x4x12 x2 x4 x3 x5x12 x2 x4 x3 x6x12 x2 x4 x4 x2x12 x2 x4 x4 x3x12 x2 x4 x4 x6x12 x2 x4 x5 x2x12 x2 x4 x5 x5x12 x2 x4 x5 x7x12 x2 x4 x6 x2x12 x2 x4 x6 x3x12 x2 x4 x7 x2x12 x2 x4 x7 x3x12 x2 x4 x7 x4x12 x2 x5 x2 x6x12 x2 x5 x3 x4x12 x2 x5 x3 x5x12 x2 x5 x3 x7x12 x2 x5 x4 x2x12 x2 x5 x4 x3x12 x2 x5 x4 x7x12 x2 x5 x5 x3x12 x2 x5 x5 x4x12 x2 x5 x5 x6x12 x2 x5 x6 x2x12 x2 x5 x6 x3x12 x2 x5 x7 x2x12 x2 x5 x7 x3x12 x2 x5 x7 x5x12 x2 x6 x3 x3x12 x2 x6 x3 x4x12 x2 x6 x4 x2x12 x2 x6 x4 x5x12 x2 x6 x4 x6x12 x2 x6 x4 x7x12 x2 x6 x5 x2x12 x2 x6 x5 x5x12 x2 x6 x5 x6x12 x2 x6 x5 x7x12 x2 x6 x6 x3x12 x2 x6 x6 x4x12 x2 x6 x7 x6x12 x2 x7 x3 x2x12 x2 x7 x3 x5x12 x2 x7 x4 x3x12 x2 x7 x4 x4x12 x2 x7 x4 x6x12 x2 x7 x4 x7x12 x2 x7 x5 x3x12 x2 x7 x5 x4x12 x2 x7 x5 x6x12 x2 x7 x5 x7x12 x2 x7 x6 x2x12 x2 x7 x6 x5x12 x2 x7 x7 x6x12 x3 x2 x3 x4x12 x3 x2 x3 x7x12 x3 x2 x4 x2x12 x3 x2 x4 x6x12 x3 x2 x5 x3x12 x3 x2 x5 x4x12 x3 x2 x5 x5x12 x3 x2 x5 x6x12 x3 x2 x6 x3x12 x3 x2 x6 x4x12 x3 x2 x6 x7x12 x3 x2 x7 x3x12 x3 x3 x3 x5x12 x3 x3 x3 x6x12 x3 x3 x4 x3x12 x3 x3 x4 x7x12 x3 x3 x5 x2x12 x3 x3 x5 x4x12 x3 x3 x5 x5x12 x3 x3 x5 x7x12 x3 x3 x6 x2x12 x3 x3 x6 x5x12 x3 x3 x6 x6x12 x3 x3 x7 x2x12 x3 x4 x3 x7x12 x3 x4 x4 x4x12 x3 x4 x4 x6x12 x3 x4 x5 x2x12 x3 x4 x5 x3x12 x3 x4 x5 x5x12 x3 x4 x5 x7x12 x3 x4 x6 x2x12 x3 x4 x6 x5x12 x3 x4 x6 x7x12 x3 x4 x7 x5x12 x3 x5 x3 x6x12 x3 x5 x4 x5x12 x3 x5 x4 x7x12 x3 x5 x5 x2x12 x3 x5 x5 x3x12 x3 x5 x5 x4x12 x3 x5 x5 x6x12 x3 x5 x6 x3x12 x3 x5 x6 x4x12 x3 x5 x6 x6x12 x3 x5 x7 x4x12 x3 x6 x3 x7x12 x3 x6 x4 x3x12 x3 x6 x4 x5x12 x3 x6 x5 x6x12 x3 x6 x5 x7x12 x3 x6 x6 x7x12 x3 x6 x7 x3x12 x3 x6 x7 x5x12 x3 x6 x7 x6x12 x3 x7 x4 x2x12 x3 x7 x4 x4x12 x3 x7 x5 x6x12 x3 x7 x5 x7x12 x3 x7 x6 x6x12 x3 x7 x7 x2x12 x3 x7 x7 x4x12 x3 x7 x7 x6x12 x4 x2 x4 x3x12 x4 x2 x4 x6x12 x4 x2 x5 x3x12 x4 x2 x5 x4x12 x4 x2 x5 x7x12 x4 x2 x6 x4x12 x4 x2 x6 x5x12 x4 x2 x7 x4x12 x4 x2 x7 x6x12 x4 x3 x4 x7x12 x4 x3 x5 x2x12 x4 x3 x5 x5x12 x4 x3 x5 x6x12 x4 x3 x6 x4x12 x4 x3 x6 x5x12 x4 x3 x7 x5x12 x4 x3 x7 x6x12 x4 x4 x4 x5x12 x4 x4 x4 x6x12 x4 x4 x5 x2x12 x4 x4 x5 x5x12 x4 x4 x5 x6x12 x4 x4 x6 x2x12 x4 x4 x6 x3x12 x4 x4 x7 x2x12 x4 x4 x7 x6x12 x4 x5 x4 x7x12 x4 x5 x5 x3x12 x4 x5 x5 x4x12 x4 x5 x5 x7x12 x4 x5 x6 x2x12 x4 x5 x6 x3x12 x4 x5 x7 x3x12 x4 x5 x7 x6x12 x4 x6 x2 x7x12 x4 x6 x4 x7x12 x4 x6 x6 x3x12 x4 x6 x6 x5x12 x4 x7 x6 x2x12 x4 x7 x6 x4x12 x5 x2 x5 x3x12 x5 x2 x5 x6x12 x5 x2 x6 x4x12 x5 x2 x6 x7x12 x5 x2 x7 x2x12 x5 x2 x7 x3x12 x5 x2 x7 x6x12 x5 x3 x5 x7x12 x5 x3 x6 x5x12 x5 x3 x6 x6x12 x5 x3 x7 x2x12 x5 x3 x7 x3x12 x5 x3 x7 x6x12 x5 x4 x5 x5x12 x5 x4 x5 x7x12 x5 x4 x6 x2x12 x5 x4 x6 x7x12 x5 x4 x7 x4x12 x5 x4 x7 x5x12 x5 x4 x7 x6x12 x5 x5 x5 x6x12 x5 x5 x6 x3x12 x5 x5 x6 x6x12 x5 x5 x7 x4x12 x5 x5 x7 x5x12 x5 x5 x7 x6x12 x5 x6 x2 x7x12 x5 x6 x3 x7x12 x5 x6 x7 x3x12 x5 x6 x7 x4x12 x5 x7 x7 x2x12 x5 x7 x7 x5x12 x6 x2 x6 x4x12 x6 x2 x6 x5x12 x6 x2 x6 x7x12 x6 x2 x7 x2x12 x6 x2 x7 x3x12 x6 x3 x6 x4x12 x6 x3 x6 x5x12 x6 x3 x6 x6x12 x6 x3 x7 x2x12 x6 x3 x7 x3x12 x6 x4 x6 x7x12 x6 x4 x7 x4x12 x6 x4 x7 x5x12 x6 x5 x6 x6x12 x6 x5 x7 x4x12 x6 x5 x7 x5x12 x6 x6 x3 x7x12 x7 x2 x7 x5x12 x7 x3 x7 x4x12 x7 x6 x2 x7x12 x7 x6 x3 x7x12 x7 x6 x6 x7∀ 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 x21x11 x7 x2 x13 x3x11 x13 x3 x14 x15x11 x14 x15 x16 x17x11 x16 x17 x18 x19x11 x18 x19 x20 x21not (x12 x7 x2 x13 x3)not (x12 x7 x2 x14 x15)not (x12 x7 x2 x16 x17)not (x12 x7 x2 x18 x19)not (x12 x7 x2 x20 x21)not (x12 x13 x3 x14 x15)not (x12 x13 x3 x16 x17)not (x12 x13 x3 x18 x19)not (x12 x13 x3 x20 x21)not (x12 x14 x15 x16 x17)not (x12 x14 x15 x18 x19)not (x12 x14 x15 x20 x21)not (x12 x16 x17 x18 x19)not (x12 x16 x17 x20 x21)not (x12 x18 x19 x20 x21)False
as obj
-
as prop
095f0..
theory
HotG
stx
206a4..
address
TMPK4..