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 . x48 x50(x50 = x49False)x48 x49False)(∀ x49 x50 . x0 x49 x50x48 x50False)(∀ x49 . x48 x49(x49 = x47False)False)(∀ x49 x50 x51 . x0 x49 x50x2 x50 (x1 x51)x48 x51False)(∀ x49 x50 x51 . x46 x51x46 x49x46 x50(x45 x51 (x45 x49 x50) = x45 (x45 x51 x49) x50False)False)(∀ x49 x50 x51 . x0 x50 x51x2 x51 (x1 x49)(x2 x50 x49False)False)(∀ x49 . x46 x49(x44 x49 x43 = x49False)False)(∀ x49 x50 . x3 x50 x49(x2 x50 (x1 x49)False)False)(∀ x49 x50 . x2 x50 (x1 x49)(x3 x50 x49False)False)(∀ x49 . x46 x49(x45 x4 x49 = x49False)False)(∀ x49 x50 . x2 x49 x50(x48 x50False)(x0 x49 x50False)False)(∀ x49 . x46 x49(x45 x49 x43 = x43False)False)(∀ x49 x50 . x0 x50 x49(x2 x50 x49False)False)((x2 x47 x5False)False)(∀ x49 x50 . x46 x50x46 x49(x44 (x42 x50) (x42 x49) = x44 x49 x50False)False)(∀ x49 x50 x51 . x46 x51x46 x49x46 x50(x45 (x45 x51 x49) x50 = x45 x51 (x45 x49 x50)False)False)((x2 x40 x41False)False)((x2 x40 x6False)False)((x39 x40 x41 x6False)False)((x7 x40False)False)(x48 x40False)(∀ x49 . x46 x49(x45 x49 (x42 x4) = x42 x49False)False)((x2 x4 x41False)False)((x2 x4 x6False)False)((x39 x4 x41 x6False)False)((x7 x4False)False)(x48 x4False)(∀ x49 x50 . x46 x50x46 x49(x45 (x8 x50) (x8 x49) = x8 (x45 x50 x49)False)False)((x2 x38 x41False)False)((x2 x38 x6False)False)((x39 x38 x41 x6False)False)((x48 x38False)False)((x42 (x42 x40) = x40False)False)((x42 (x42 x4) = x4False)False)((x42 x40 = x42 x40False)False)((x42 x4 = x42 x4False)False)((x42 x38 = x38False)False)((x45 (x42 x40) x4 = x42 x40False)False)((x45 (x42 x40) x38 = x38False)False)((x45 x40 x4 = x40False)False)((x45 x40 x38 = x38False)False)((x45 x4 (x42 x40) = x42 x40False)False)((x45 x4 x40 = x40False)False)((x45 x4 x4 = x4False)False)((x45 x4 x38 = x38False)False)((x45 x38 (x42 x40) = x38False)False)((x45 x38 x40 = x38False)False)((x45 x38 x4 = x38False)False)((x45 x38 x38 = x38False)False)((x44 (x42 x40) (x42 x40) = x38False)False)((x44 (x42 x40) (x42 x4) = x42 x4False)False)((x44 (x42 x40) x38 = x42 x40False)False)((x44 (x42 x4) (x42 x40) = x4False)False)((x44 (x42 x4) (x42 x4) = x38False)False)((x44 (x42 x4) x4 = x42 x40False)False)((x44 (x42 x4) x38 = x42 x4False)False)((x44 x40 x40 = x38False)False)((x44 x40 x4 = x4False)False)((x44 x40 x38 = x40False)False)((x44 x4 (x42 x4) = x40False)False)((x44 x4 x40 = x42 x4False)False)((x44 x4 x4 = x38False)False)((x44 x4 x38 = x4False)False)((x44 x38 (x42 x40) = x40False)False)((x44 x38 (x42 x4) = x4False)False)((x44 x38 x40 = x42 x40False)False)((x44 x38 x4 = x42 x4False)False)((x44 x38 x38 = x38False)False)(∀ x49 . (x3 x49 x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x2 x49 (x1 x51)x2 x50 x49(x39 x50 x51 x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x2 x49 (x1 x51)x39 x50 x51 x49(x2 x50 x49False)False)((x43 = x47False)False)((x6 = x5False)False)((x9 x10False)False)(x48 x10False)((x11 x12False)False)((x48 x12False)False)((x13 x14False)False)((x11 x14False)False)((x46 x14False)False)((x48 x14False)False)((x9 x15False)False)((x37 x36False)False)((x11 x36False)False)((x13 x35False)False)((x37 x35False)False)((x11 x35False)False)((x46 x35False)False)((x7 x34False)False)((x11 x34False)False)((x13 x33False)False)((x7 x33False)False)((x11 x33False)False)((x46 x33False)False)((x46 x32False)False)(x48 x32False)(x48 x31False)((x16 x17False)False)((x30 x17False)False)((x18 x17False)False)(x48 x17False)((x11 x19False)False)((x13 x29False)False)((x46 x20False)False)((x48 x28False)False)((x16 x21False)False)(∀ x49 . x46 x49(x8 (x8 x49) = x49False)False)(∀ x49 . x46 x49(x42 (x42 x49) = x49False)False)(∀ x49 x50 . (x48 x50False)x46 x50(x48 x49False)x46 x49x48 (x45 x50 x49)False)(∀ x49 x50 . x13 x50x13 x49(x13 (x44 x50 x49)False)False)(∀ x49 . (x48 x49False)x46 x49(x46 (x8 x49)False)False)(∀ x49 . (x48 x49False)x46 x49x48 (x8 x49)False)(∀ x49 x50 . x13 x50x13 x49(x13 (x45 x50 x49)False)False)(∀ x49 . (x48 x49False)x46 x49(x46 (x42 x49)False)False)(∀ x49 . (x48 x49False)x46 x49x48 (x42 x49)False)((x16 x5False)False)(x48 x5False)(∀ x49 . x13 x49(x13 (x8 x49)False)False)(∀ x49 . x13 x49(x46 (x8 x49)False)False)(∀ x49 x50 . x46 x50x46 x49(x46 (x44 x50 x49)False)False)(∀ x49 . x13 x49(x13 (x42 x49)False)False)(∀ x49 . x13 x49(x46 (x42 x49)False)False)(∀ x49 x50 . x46 x50x46 x49(x46 (x45 x50 x49)False)False)(∀ x49 . (x37 x49False)x13 x49x37 (x8 x49)False)(∀ x49 . (x37 x49False)x13 x49(x46 (x8 x49)False)False)(∀ x49 . x37 x49x13 x49(x37 (x8 x49)False)False)(∀ x49 . x37 x49x13 x49(x46 (x8 x49)False)False)(∀ x49 . (x7 x49False)x13 x49x7 (x8 x49)False)(∀ x49 . (x7 x49False)x13 x49(x46 (x8 x49)False)False)(∀ x49 . x7 x49x13 x49(x7 (x8 x49)False)False)(∀ x49 . x7 x49x13 x49(x46 (x8 x49)False)False)(∀ x49 x50 . (x37 x50False)x13 x50(x37 x49False)x13 x49x37 (x45 x50 x49)False)(∀ x49 x50 . (x7 x50False)x13 x50(x7 x49False)x13 x49x37 (x45 x50 x49)False)(∀ x49 x50 . (x7 x50False)x13 x50(x37 x49False)x13 x49x7 (x45 x49 x50)False)(∀ x49 x50 . (x7 x50False)x13 x50(x37 x49False)x13 x49x7 (x45 x50 x49)False)(∀ x49 x50 . x37 x50x13 x50(x37 x49False)x13 x49(x7 (x44 x49 x50)False)False)(∀ x49 x50 . x37 x50x13 x50(x37 x49False)x13 x49(x37 (x44 x50 x49)False)False)(∀ x49 x50 . x7 x50x13 x50(x7 x49False)x13 x49(x37 (x44 x49 x50)False)False)((x48 x47False)False)(∀ x49 x50 . x7 x50x13 x50(x7 x49False)x13 x49(x7 (x44 x50 x49)False)False)(∀ x49 x50 . (x37 x50False)x13 x50(x7 x49False)x13 x49x7 (x44 x49 x50)False)(∀ x49 x50 . (x37 x50False)x13 x50(x7 x49False)x13 x49x37 (x44 x50 x49)False)(∀ x49 . (x37 x49False)x13 x49x7 (x42 x49)False)(∀ x49 . (x37 x49False)x13 x49(x46 (x42 x49)False)False)(∀ x49 . (x7 x49False)x13 x49x37 (x42 x49)False)(∀ x49 . (x7 x49False)x13 x49(x46 (x42 x49)False)False)(∀ x49 x50 . (x48 x50False)(x48 x49False)x2 x49 (x1 x50)(x39 (x27 x49 x50) x50 x49False)False)(∀ x49 . (x2 (x22 x49) x49False)False)(∀ x49 x50 x51 . (x48 x51False)(x48 x49False)x2 x49 (x1 x51)x39 x50 x51 x49(x2 x50 x51False)False)((x39 x43 x41 x6False)False)(∀ x49 . x46 x49(x46 (x8 x49)False)False)((x2 x6 (x1 x41)False)False)(∀ x49 . x46 x49(x46 (x42 x49)False)False)(∀ x49 x50 . x46 x50x46 x49x50 = x43x49 = x43(x49 = x8 x50False)False)(∀ x49 x50 . x46 x50x46 x49x50 = x43x49 = x8 x50(x49 = x43False)False)(∀ x49 x50 . x46 x50x46 x49(x50 = x43False)x45 x50 x49 = x4(x49 = x8 x50False)False)(∀ x49 x50 . x46 x50x46 x49(x50 = x43False)x49 = x8 x50(x45 x50 x49 = x4False)False)(∀ x49 x50 . x46 x50x46 x49(x45 x50 x49 = x45 x49 x50False)False)(∀ x49 . x48 x49(x26 x49False)False)(∀ x49 . x11 x49(x7 x49False)(x37 x49False)(x11 x49False)False)(∀ x49 . x11 x49(x7 x49False)(x37 x49False)(x48 x49False)False)(∀ x49 . x2 x49 x5(x9 x49False)False)(∀ x49 . x48 x49x11 x49x37 x49False)(∀ x49 . x48 x49x11 x49x7 x49False)(∀ x49 . x48 x49x11 x49(x11 x49False)False)(∀ x49 . x48 x49(x9 x49False)False)(∀ x49 . (x48 x49False)x11 x49(x7 x49False)(x37 x49False)False)(∀ x49 . (x48 x49False)x11 x49(x7 x49False)(x11 x49False)False)(∀ x49 . x9 x49(x16 x49False)False)(∀ x49 . x11 x49x37 x49x7 x49False)(∀ x49 . x11 x49x37 x49(x11 x49False)False)(∀ x49 . x11 x49x37 x49x48 x49False)(∀ x49 x50 . x16 x50x2 x49 x50(x16 x49False)False)(∀ x49 . (x48 x49False)x11 x49(x37 x49False)(x7 x49False)False)(∀ x49 . (x48 x49False)x11 x49(x37 x49False)(x11 x49False)False)(∀ x49 . x13 x49(x11 x49False)False)(∀ x49 . x48 x49(x25 x49False)False)(∀ x49 . x11 x49x7 x49x37 x49False)(∀ x49 . x11 x49x7 x49(x11 x49False)False)(∀ x49 . x11 x49x7 x49x48 x49False)(∀ x49 . x13 x49(x46 x49False)False)(∀ x49 . x48 x49(x16 x49False)False)(∀ x49 . x9 x49(x11 x49False)False)(∀ x49 . x9 x49(x13 x49False)False)(∀ x49 . x9 x49(x46 x49False)False)(∀ x49 . x18 x49x30 x49(x16 x49False)False)(∀ x49 . x2 x49 x41(x13 x49False)False)(∀ x49 . x2 x49 x41(x46 x49False)False)(∀ x49 . x16 x49(x30 x49False)False)(∀ x49 . x16 x49(x18 x49False)False)(∀ x49 x50 . x26 x50x2 x49 (x1 x50)(x26 x49False)False)(∀ x49 x50 . x0 x49 x50x0 x50 x49False)(x24 = x42 x4False)(x23 = x43False)((x45 x24 x23 = x42 x23False)False)((x46 x24False)False)((x46 x23False)False)False
as obj
-
as prop
25211..
theory
HotG
stx
a192b..
address
TMU96..