Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ 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 x60 . x58 x60(x60 = x59False)x58 x59False)(∀ x59 x60 . x0 x59 x60x58 x60False)(∀ x59 . x58 x59(x59 = x57False)False)(∀ x59 x60 x61 . x0 x59 x60x2 x60 (x1 x61)x58 x61False)(∀ x59 x60 x61 . x0 x60 x61x2 x61 (x1 x59)(x2 x60 x59False)False)(∀ x59 x60 . x3 x60 x59(x2 x60 (x1 x59)False)False)(∀ x59 x60 . x2 x60 (x1 x59)(x3 x60 x59False)False)(∀ x59 x60 . x2 x59 x60(x58 x60False)(x0 x59 x60False)False)(∀ x59 x60 . x0 x60 x59(x2 x60 x59False)False)(x58 x4False)(∀ x59 . (x3 x59 x59False)False)(∀ x59 x60 x61 . (x58 x61False)(x58 x59False)x2 x59 (x1 x61)x2 x60 x59(x5 x60 x61 x59False)False)(∀ x59 x60 x61 . (x58 x61False)(x58 x59False)x2 x59 (x1 x61)x5 x60 x61 x59(x2 x60 x59False)False)(∀ x59 x60 . (x58 x60False)x2 x59 x60(x6 x60 x59 = x7 x59False)False)((x56 x55False)False)(x58 x55False)(∀ x59 . (x54 x59False)x54 (x53 x59)False)(∀ x59 . (x54 x59False)(x2 (x53 x59) (x1 x59)False)False)(∀ x59 . (x58 x59False)(x54 (x52 x59)False)False)(∀ x59 . (x58 x59False)x58 (x52 x59)False)(∀ x59 . (x58 x59False)(x2 (x52 x59) (x1 x59)False)False)(x8 x9False)((x51 x9False)False)((x10 x9False)False)(∀ x59 . (x58 x59False)(x49 (x50 x59) x59False)False)(∀ x59 . (x58 x59False)(x2 (x50 x59) (x1 x59)False)False)(∀ x59 . (x48 x59False)x46 x59x58 (x47 x59)False)(∀ x59 . (x48 x59False)x46 x59(x2 (x47 x59) (x1 (x11 x59))False)False)((x51 x45False)False)((x12 x45False)False)((x10 x45False)False)(x58 x45False)(∀ x59 . x49 (x44 x59) x59False)(∀ x59 . (x2 (x44 x59) (x1 x59)False)False)((x51 x43False)False)((x12 x43False)False)((x10 x43False)False)(x58 x13False)(∀ x59 . (x58 (x42 x59)False)False)(∀ x59 . (x2 (x42 x59) (x1 x59)False)False)((x12 x41False)False)((x10 x41False)False)((x40 x39False)False)((x51 x39False)False)((x10 x39False)False)(x58 x14False)((x8 x14False)False)((x51 x14False)False)((x10 x14False)False)(∀ x59 . (x15 x59False)x46 x59x54 (x16 x59)False)(∀ x59 . (x15 x59False)x46 x59(x2 (x16 x59) (x1 (x11 x59))False)False)(∀ x59 . (x48 x59False)x46 x59(x54 (x17 x59)False)False)(∀ x59 . (x48 x59False)x46 x59x58 (x17 x59)False)(∀ x59 . (x48 x59False)x46 x59(x2 (x17 x59) (x1 (x11 x59))False)False)((x58 x38False)False)(∀ x59 . (x58 x59False)x58 (x18 x59)False)(∀ x59 . (x58 x59False)(x2 (x18 x59) (x1 x59)False)False)((x10 x19False)False)(x58 x19False)((x51 x20False)False)((x10 x20False)False)((x21 x22False)False)((x51 x22False)False)((x10 x22False)False)(∀ x59 . (x37 x59False)x46 x59x36 (x11 x59)False)(∀ x59 . x37 x59x46 x59(x36 (x11 x59)False)False)(∀ x59 . x15 x59x46 x59(x54 (x11 x59)False)False)(∀ x59 . (x15 x59False)x46 x59x54 (x11 x59)False)(∀ x59 . x58 (x7 x59)False)(∀ x59 . (x48 x59False)x46 x59x58 (x11 x59)False)((x58 x57False)False)(∀ x59 . x58 (x1 x59)False)(∀ x59 . x48 x59x46 x59(x58 (x11 x59)False)False)(∀ x59 . x10 x59x51 x59(x56 (x7 x59)False)False)(∀ x59 x60 . (x58 x60False)(x58 x59False)x2 x59 (x1 x60)(x5 (x35 x59 x60) x60 x59False)False)(∀ x59 . (x2 (x23 x59) x59False)False)((x46 x34False)False)(∀ x59 x60 . (x48 x60False)x46 x60(x58 x59False)x2 x59 (x1 (x11 x60))(x5 (x24 x60 x59) (x11 x60) x59False)False)((x58 x33False)False)(∀ x59 x60 x61 . (x58 x61False)(x58 x59False)x2 x59 (x1 x61)x5 x60 x61 x59(x2 x60 x61False)False)(∀ x59 x60 . (x58 x60False)x2 x59 x60(x2 (x6 x60 x59) (x1 x60)False)False)(∀ x59 x60 . x0 (x25 x59 x60) x59(x3 x60 x59False)False)(∀ x59 x60 . (x0 (x25 x59 x60) x60False)(x3 x60 x59False)False)(∀ x59 x60 x61 . x3 x60 x61x0 x59 x60(x0 x59 x61False)False)((x57 = x33False)False)(∀ x59 x60 . (x26 x60 x59 = x59False)(x0 (x26 x60 x59) x60False)(x60 = x7 x59False)False)(∀ x59 x60 . x0 (x26 x60 x59) x60x26 x60 x59 = x59(x60 = x7 x59False)False)(∀ x59 x60 x61 . x60 = x7 x61x59 = x61(x0 x59 x60False)False)(∀ x59 x60 x61 . x60 = x7 x61x0 x59 x60(x59 = x61False)False)(∀ x59 x60 . x3 x60 x59x3 x59 x60(x60 = x59False)False)(∀ x59 x60 . x59 = x60(x3 x60 x59False)False)(∀ x59 x60 . x60 = x59(x3 x60 x59False)False)(∀ x59 . x46 x59x32 x59 x57(x48 x59False)False)(∀ x59 x60 . x56 x60x2 x59 (x1 x60)(x56 x59False)False)(∀ x59 . x46 x59x48 x59(x32 x59 x57False)False)(∀ x59 x60 . x56 x60x2 x59 x60(x51 x59False)False)(∀ x59 x60 . x56 x60x2 x59 x60(x10 x59False)False)(∀ x59 . x46 x59(x37 x59False)x15 x59False)(∀ x59 . x58 x59(x56 x59False)False)(∀ x59 . x46 x59x15 x59(x37 x59False)False)(∀ x59 . x54 x59x10 x59x51 x59(x8 x59False)False)(∀ x59 . x54 x59x10 x59x51 x59(x51 x59False)False)(∀ x59 . x54 x59x10 x59x51 x59(x10 x59False)False)(∀ x59 x60 . x54 x60x2 x59 (x1 x60)(x54 x59False)False)(∀ x59 . x46 x59(x37 x59False)x37 x59False)(∀ x59 . x46 x59(x37 x59False)x48 x59False)(∀ x59 . x10 x59x51 x59(x8 x59False)(x51 x59False)False)(∀ x59 . x10 x59x51 x59(x8 x59False)(x10 x59False)False)(∀ x59 . x10 x59x51 x59(x8 x59False)x54 x59False)(∀ x59 x60 . x58 x60x2 x59 (x1 x60)x49 x59 x60False)(∀ x59 . x46 x59x48 x59(x37 x59False)False)(∀ x59 . x46 x59x48 x59(x48 x59False)False)(∀ x59 . x58 x59x10 x59(x12 x59False)False)(∀ x59 . x58 x59x10 x59(x10 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x8 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x51 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x10 x59False)False)(∀ x59 x60 . (x58 x60False)x2 x59 (x1 x60)x58 x59(x49 x59 x60False)False)(∀ x59 . x58 x59x10 x59(x31 x59False)False)(∀ x59 . x58 x59x10 x59(x10 x59False)False)(∀ x59 x60 . x10 x60x51 x60x2 x59 (x1 x60)(x51 x59False)False)(∀ x59 . x10 x59x51 x59x58 x59(x21 x59False)False)(∀ x59 . x10 x59x51 x59x58 x59(x51 x59False)False)(∀ x59 . x10 x59x51 x59x58 x59(x10 x59False)False)(∀ x59 x60 . (x58 x60False)x2 x59 (x1 x60)(x49 x59 x60False)x58 x59False)(∀ x59 . x46 x59(x15 x59False)x48 x59False)(∀ x59 x60 . x10 x60x2 x59 (x1 x60)(x10 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x40 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x51 x59False)False)(∀ x59 . x58 x59x10 x59x51 x59(x10 x59False)False)(∀ x59 . x10 x59x51 x59x21 x59(x30 x59False)False)(∀ x59 . x10 x59x51 x59x21 x59(x51 x59False)False)(∀ x59 . x10 x59x51 x59x21 x59(x10 x59False)False)(∀ x59 x60 . x58 x60x2 x59 (x1 x60)(x58 x59False)False)(∀ x59 . x46 x59x48 x59(x15 x59False)False)(∀ x59 . x58 x59(x10 x59False)False)(∀ x59 . x58 x59(x51 x59False)False)(∀ x59 . x46 x59(x15 x59False)x48 x59False)(∀ x59 . x46 x59x32 x59 x4(x15 x59False)False)(∀ x59 . x46 x59x32 x59 x4x48 x59False)(∀ x59 . x46 x59(x48 x59False)x15 x59(x32 x59 x4False)False)(∀ x59 x60 . x0 x59 x60x0 x60 x59False)(x27 = x6 (x11 x28) x29False)((x11 x28 = x6 (x11 x28) x29False)False)((x2 x29 (x11 x28)False)False)((x2 x27 (x1 (x11 x28))False)False)(x58 x27False)((x46 x28False)False)(x48 x28False)False
as obj
-
as prop
cdb7b..
theory
HotG
stx
89b0b..
address
TML3N..