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 . x55 x57(x57 = x56False)x55 x56False)(∀ x56 x57 . x0 x56 x57x55 x57False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))x53 x58x54 x58x0 x58 (x51 x56 x57 x59)(x52 x59 x58False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))x54 x58x48 x58 (x49 (x50 x56 x57))x0 x58 (x51 x56 x57 x59)(x1 x58 x56False)False)(∀ x56 . x55 x56(x56 = x47False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))x0 x58 (x51 x56 x57 x59)(x48 x58 (x49 (x50 x56 x57))False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))x0 x58 (x51 x56 x57 x59)(x54 x58False)False)(∀ x56 x57 x58 . x0 x56 x57x48 x57 (x49 x58)x55 x58False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x54 x59x48 x59 (x49 (x50 x56 x57))x53 x58x54 x58x52 x60 x58x46 x56 x57 x59 x60(x52 x59 x58False)False)(∀ x56 x57 x58 . x0 x57 x58x48 x58 (x49 x56)(x48 x57 x56False)False)(∀ x56 x57 . x45 x57 x56(x48 x57 (x49 x56)False)False)(∀ x56 x57 . x48 x57 (x49 x56)(x45 x57 x56False)False)(∀ x56 x57 . x48 x56 x57(x55 x57False)(x0 x56 x57False)False)(∀ x56 x57 . x0 x57 x56(x48 x57 x56False)False)(∀ x56 x57 . x53 x57x54 x57x53 x56x54 x56x52 x57 x56(x52 x56 x57False)False)(∀ x56 . (x45 x56 x56False)False)(∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57))(x46 x56 x57 x58 x58False)False)(∀ x56 x57 . x53 x57x54 x57x53 x56x54 x56(x52 x57 x57False)False)(∀ x56 x57 x58 x59 . x48 x59 (x49 (x50 x58 x57))x45 x59 x56(x46 x58 x57 x59 x56False)False)(∀ x56 x57 x58 x59 . x48 x59 (x49 (x50 x58 x57))x46 x58 x57 x59 x56(x45 x59 x56False)False)(∀ x56 . (x54 (x44 x56)False)False)(∀ x56 . (x2 (x44 x56) x56False)False)(∀ x56 . (x43 (x44 x56)False)False)(∀ x56 . (x53 (x44 x56)False)False)((x42 x41False)False)(x55 x41False)(∀ x56 . (x40 x56False)x40 (x39 x56)False)(∀ x56 . (x40 x56False)(x48 (x39 x56) (x49 x56)False)False)(∀ x56 x57 . (x54 (x38 x56 x57)False)False)(∀ x56 x57 . (x3 (x38 x56 x57) x56False)False)(∀ x56 x57 . (x2 (x38 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x38 x56 x57)False)False)(∀ x56 . (x55 x56False)(x40 (x37 x56)False)False)(∀ x56 . (x55 x56False)x55 (x37 x56)False)(∀ x56 . (x55 x56False)(x48 (x37 x56) (x49 x56)False)False)(x4 x5False)((x54 x5False)False)((x53 x5False)False)(∀ x56 . (x55 x56False)(x35 (x36 x56) x56False)False)(∀ x56 . (x55 x56False)(x48 (x36 x56) (x49 x56)False)False)((x54 x34False)False)((x43 x34False)False)((x53 x34False)False)(x55 x34False)(∀ x56 . x35 (x33 x56) x56False)(∀ x56 . (x48 (x33 x56) (x49 x56)False)False)(∀ x56 x57 . (x3 (x32 x56 x57) x56False)False)(∀ x56 x57 . (x2 (x32 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x32 x56 x57)False)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)x55 (x6 x56 x57)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)(x54 (x6 x56 x57)False)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)(x3 (x6 x56 x57) x56False)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)(x2 (x6 x56 x57) x57False)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)(x53 (x6 x56 x57)False)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)(x48 (x6 x56 x57) (x49 (x50 x57 x56))False)False)((x54 x7False)False)((x43 x7False)False)((x53 x7False)False)(x55 x31False)(∀ x56 . (x55 (x8 x56)False)False)(∀ x56 . (x48 (x8 x56) (x49 x56)False)False)((x43 x9False)False)((x53 x9False)False)((x10 x11False)False)((x54 x11False)False)((x53 x11False)False)((x55 x30False)False)(∀ x56 . (x55 x56False)x55 (x12 x56)False)(∀ x56 . (x55 x56False)(x48 (x12 x56) (x49 x56)False)False)(∀ x56 x57 . (x3 (x13 x56 x57) x56False)False)(∀ x56 x57 . (x2 (x13 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x13 x56 x57)False)False)(∀ x56 x57 . (x55 (x13 x56 x57)False)False)(∀ x56 x57 . (x48 (x13 x56 x57) (x49 (x50 x57 x56))False)False)((x53 x29False)False)(x55 x29False)(∀ x56 x57 . (x54 (x28 x56 x57)False)False)(∀ x56 x57 . (x3 (x28 x56 x57) x56False)False)(∀ x56 x57 . (x2 (x28 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x28 x56 x57)False)False)(∀ x56 x57 . (x48 (x28 x56 x57) (x49 (x50 x57 x56))False)False)(∀ x56 x57 . (x14 (x15 x56 x57) x57 x56False)False)(∀ x56 x57 . (x54 (x15 x56 x57)False)False)(∀ x56 x57 . (x3 (x15 x56 x57) x56False)False)(∀ x56 x57 . (x2 (x15 x57 x56) x56False)False)(∀ x56 x57 . (x53 (x15 x56 x57)False)False)(∀ x56 x57 . (x48 (x15 x56 x57) (x49 (x50 x57 x56))False)False)((x54 x16False)False)((x53 x16False)False)(∀ x56 x57 . (x53 (x50 x56 x57)False)False)(∀ x56 x57 x58 . (x55 x58False)x55 x56x54 x57x48 x57 (x49 (x50 x58 x56))(x55 (x51 x58 x56 x57)False)False)((x55 x47False)False)(∀ x56 . x55 (x49 x56)False)(∀ x56 x57 . (x55 x57False)(x55 x56False)x55 (x50 x57 x56)False)(∀ x56 . (x48 (x27 x56) x56False)False)((x55 x17False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))(x52 x59 (x26 x58 x59 x57 x56)False)(x0 (x25 x58 x59 x57 x56) x58False)(x58 = x51 x56 x57 x59False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))(x1 (x26 x58 x59 x57 x56) x56False)(x0 (x25 x58 x59 x57 x56) x58False)(x58 = x51 x56 x57 x59False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))(x26 x58 x59 x57 x56 = x25 x58 x59 x57 x56False)(x0 (x25 x58 x59 x57 x56) x58False)(x58 = x51 x56 x57 x59False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))(x48 (x26 x58 x59 x57 x56) (x49 (x50 x56 x57))False)(x0 (x25 x58 x59 x57 x56) x58False)(x58 = x51 x56 x57 x59False)False)(∀ x56 x57 x58 x59 . x54 x59x48 x59 (x49 (x50 x56 x57))(x54 (x26 x58 x59 x57 x56)False)(x0 (x25 x58 x59 x57 x56) x58False)(x58 = x51 x56 x57 x59False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x0 (x25 x59 x60 x57 x56) x59x54 x58x48 x58 (x49 (x50 x56 x57))x58 = x25 x59 x60 x57 x56x1 x58 x56x52 x60 x58(x59 = x51 x56 x57 x60False)False)(∀ x56 x57 x58 x59 x60 x61 . x54 x61x48 x61 (x49 (x50 x56 x57))x60 = x51 x56 x57 x61x54 x58x48 x58 (x49 (x50 x56 x57))x58 = x59x1 x58 x56x52 x61 x58(x0 x59 x60False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x59 = x51 x56 x57 x60x0 x58 x59(x52 x60 (x18 x58 x59 x60 x57 x56)False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x59 = x51 x56 x57 x60x0 x58 x59(x1 (x18 x58 x59 x60 x57 x56) x56False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x59 = x51 x56 x57 x60x0 x58 x59(x18 x58 x59 x60 x57 x56 = x58False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x59 = x51 x56 x57 x60x0 x58 x59(x48 (x18 x58 x59 x60 x57 x56) (x49 (x50 x56 x57))False)False)(∀ x56 x57 x58 x59 x60 . x54 x60x48 x60 (x49 (x50 x56 x57))x59 = x51 x56 x57 x60x0 x58 x59(x54 (x18 x58 x59 x60 x57 x56)False)False)(∀ x56 x57 . x0 (x24 x56 x57) x56(x45 x57 x56False)False)(∀ x56 x57 . (x0 (x24 x56 x57) x57False)(x45 x57 x56False)False)(∀ x56 x57 x58 . x45 x57 x58x0 x56 x57(x0 x56 x58False)False)((x47 = x17False)False)(∀ x56 x57 . x42 x57x48 x56 (x49 x57)(x42 x56False)False)(∀ x56 x57 . x55 x57x53 x56x3 x56 x57(x3 x56 x57False)False)(∀ x56 x57 . x55 x57x53 x56x3 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x3 x56 x57(x55 x56False)False)(∀ x56 x57 . x42 x57x48 x56 x57(x54 x56False)False)(∀ x56 x57 . x42 x57x48 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x2 x56 x57(x2 x56 x57False)False)(∀ x56 x57 . x55 x57x53 x56x2 x56 x57(x53 x56False)False)(∀ x56 x57 . x55 x57x53 x56x2 x56 x57(x55 x56False)False)(∀ x56 . x55 x56(x42 x56False)False)(∀ x56 x57 x58 . x53 x58x3 x58 x56x48 x57 (x49 x58)(x3 x57 x56False)False)(∀ x56 . x40 x56x53 x56x54 x56(x4 x56False)False)(∀ x56 . x40 x56x53 x56x54 x56(x54 x56False)False)(∀ x56 . x40 x56x53 x56x54 x56(x53 x56False)False)(∀ x56 x57 . x40 x57x48 x56 (x49 x57)(x40 x56False)False)(∀ x56 x57 x58 . x53 x58x2 x58 x56x48 x57 (x49 x58)(x2 x57 x56False)False)(∀ x56 . x53 x56x54 x56(x4 x56False)(x54 x56False)False)(∀ x56 . x53 x56x54 x56(x4 x56False)(x53 x56False)False)(∀ x56 . x53 x56x54 x56(x4 x56False)x40 x56False)(∀ x56 x57 . x55 x57x48 x56 (x49 x57)x35 x56 x57False)(∀ x56 x57 x58 . x55 x58x48 x56 (x49 (x50 x57 x58))(x55 x56False)False)(∀ x56 . x55 x56x53 x56(x43 x56False)False)(∀ x56 . x55 x56x53 x56(x53 x56False)False)(∀ x56 x57 . x48 x57 (x49 (x50 x56 x56))x14 x57 x56 x56(x1 x57 x56False)False)(∀ x56 . x55 x56x53 x56x54 x56(x4 x56False)False)(∀ x56 . x55 x56x53 x56x54 x56(x54 x56False)False)(∀ x56 . x55 x56x53 x56x54 x56(x53 x56False)False)(∀ x56 x57 . (x55 x57False)x48 x56 (x49 x57)x55 x56(x35 x56 x57False)False)(∀ x56 x57 x58 . x55 x58x48 x56 (x49 (x50 x58 x57))(x55 x56False)False)(∀ x56 . x55 x56x53 x56(x19 x56False)False)(∀ x56 . x55 x56x53 x56(x53 x56False)False)(∀ x56 x57 x58 . (x55 x58False)x48 x56 (x49 (x50 x57 x58))x14 x56 x57 x58(x1 x56 x57False)False)(∀ x56 x57 . x53 x57x54 x57x48 x56 (x49 x57)(x54 x56False)False)(∀ x56 x57 . (x55 x57False)x48 x56 (x49 x57)(x35 x56 x57False)x55 x56False)(∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57))(x3 x58 x57False)False)(∀ x56 x57 x58 . x48 x58 (x49 (x50 x57 x56))(x2 x58 x57False)False)(∀ x56 x57 . x53 x57x48 x56 (x49 x57)(x53 x56False)False)(∀ x56 x57 x58 . (x55 x58False)x55 x56x48 x57 (x49 (x50 x58 x56))x1 x57 x58False)(∀ x56 x57 x58 . x55 x58x48 x56 (x49 (x50 x58 x57))x14 x56 x58 x57(x1 x56 x58False)False)(∀ x56 . x55 x56x53 x56x54 x56(x10 x56False)False)(∀ x56 . x55 x56x53 x56x54 x56(x54 x56False)False)(∀ x56 . x55 x56x53 x56x54 x56(x53 x56False)False)(∀ x56 x57 . x55 x57x48 x56 (x49 x57)(x55 x56False)False)(∀ x56 x57 x58 . x48 x58 (x49 (x50 x56 x57))(x53 x58False)False)(∀ x56 . x55 x56(x53 x56False)False)(∀ x56 x57 x58 . x55 x58x48 x56 (x49 (x50 x58 x57))(x1 x56 x58False)False)(∀ x56 x57 x58 . x48 x57 (x49 (x50 x58 x56))x1 x57 x58(x14 x57 x58 x56False)False)(∀ x56 . x55 x56(x54 x56False)False)(∀ x56 x57 . x0 x56 x57x0 x57 x56False)(x45 (x51 x20 x21 x23) (x51 x20 x21 x22)False)((x46 x20 x21 x22 x23False)False)((x48 x22 (x49 (x50 x20 x21))False)False)((x54 x22False)False)((x48 x23 (x49 (x50 x20 x21))False)False)((x54 x23False)False)False
as obj
-
as prop
75510..
theory
HotG
stx
bc90b..
address
TMKNJ..