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 . (x29 x33False)x22 x33x28 x33x23 x33x27 x33x25 x30 (x24 x33)x25 x32 (x24 x33)x25 x31 (x24 x33)(x26 x33 (x26 x33 x31 x32) (x26 x33 (x26 x33 x30 x30) x32) = x26 x33 (x26 x33 x32 (x26 x33 (x26 x33 x31 x31) x30)) (x26 x33 x32 (x26 x33 (x26 x33 x31 x31) x30))False)False)((x2 x1 x0False)False)((x27 x1False)False)((x3 x4False)False)((x23 x4False)False)((x28 x4False)False)((x22 x4False)False)(x29 x4False)((x27 x4False)False)(∀ x30 . (x5 x30False)x7 x30x6 (x24 x30)False)(∀ x30 . x5 x30x7 x30(x6 (x24 x30)False)False)(∀ x30 . x8 x30x7 x30(x9 (x24 x30)False)False)(∀ x30 . (x8 x30False)x7 x30x9 (x24 x30)False)(∀ x30 . (x29 x30False)x7 x30x10 (x24 x30)False)(∀ x30 . x29 x30x7 x30(x10 (x24 x30)False)False)(∀ x30 . (x25 (x11 x30) x30False)False)((x7 x21False)False)((x27 x12False)False)(∀ x30 . x27 x30(x7 x30False)False)(∀ x30 x31 x32 . (x29 x32False)x27 x32x25 x31 (x24 x32)x25 x30 (x24 x32)(x25 (x26 x32 x31 x30) (x24 x32)False)False)(∀ x30 . (x29 x30False)x27 x30x26 x30 (x26 x30 (x19 x30) (x26 x30 (x18 x30) (x20 x30))) (x26 x30 (x19 x30) (x26 x30 (x18 x30) (x20 x30))) = x26 x30 (x26 x30 (x26 x30 (x18 x30) (x18 x30)) (x19 x30)) (x26 x30 (x26 x30 (x20 x30) (x20 x30)) (x19 x30))(x23 x30False)False)(∀ x30 . (x29 x30False)x27 x30(x25 (x20 x30) (x24 x30)False)(x23 x30False)False)(∀ x30 . (x29 x30False)x27 x30(x25 (x18 x30) (x24 x30)False)(x23 x30False)False)(∀ x30 . (x29 x30False)x27 x30(x25 (x19 x30) (x24 x30)False)(x23 x30False)False)(∀ x30 x31 x32 x33 . (x29 x33False)x27 x33x23 x33x25 x30 (x24 x33)x25 x32 (x24 x33)x25 x31 (x24 x33)(x26 x33 (x26 x33 x30 (x26 x33 x32 x31)) (x26 x33 x30 (x26 x33 x32 x31)) = x26 x33 (x26 x33 (x26 x33 x32 x32) x30) (x26 x33 (x26 x33 x31 x31) x30)False)False)(∀ x30 . x7 x30x2 x30 x13(x29 x30False)False)(∀ x30 . x7 x30x29 x30(x2 x30 x13False)False)(∀ x30 . x7 x30(x5 x30False)x8 x30False)(∀ x30 . x7 x30x8 x30(x5 x30False)False)(∀ x30 . x7 x30(x5 x30False)x5 x30False)(∀ x30 . x7 x30(x5 x30False)x29 x30False)(∀ x30 . x7 x30x29 x30(x5 x30False)False)(∀ x30 . x7 x30x29 x30(x29 x30False)False)(∀ x30 . x27 x30x2 x30 x0(x23 x30False)False)(∀ x30 . x27 x30x2 x30 x0(x28 x30False)False)(∀ x30 . x27 x30x2 x30 x0(x22 x30False)False)(∀ x30 . x27 x30x2 x30 x0(x2 x30 x0False)False)(∀ x30 . x7 x30(x8 x30False)x29 x30False)(∀ x30 . x7 x30x29 x30(x8 x30False)False)(∀ x30 . x27 x30(x29 x30False)x8 x30(x3 x30False)False)(∀ x30 . x27 x30(x29 x30False)x8 x30x29 x30False)(∀ x30 . x7 x30(x8 x30False)x29 x30False)(∀ x30 . x7 x30x2 x30 x0(x8 x30False)False)(∀ x30 . x7 x30x2 x30 x0x29 x30False)(∀ x30 . x7 x30(x29 x30False)x8 x30(x2 x30 x0False)False)(x26 x17 (x26 x17 (x26 x17 x16 x16) (x26 x17 (x26 x17 x14 x14) x15)) (x26 x17 (x26 x17 x15 (x26 x17 (x26 x17 x15 x15) x14)) (x26 x17 x15 (x26 x17 (x26 x17 x15 x15) x14))) = x26 x17 (x26 x17 (x26 x17 (x26 x17 x14 x14) x15) (x26 x17 x16 x15)) (x26 x17 (x26 x17 (x26 x17 x14 x14) x15) (x26 x17 x16 x15))False)((x25 x14 (x24 x17)False)False)((x25 x15 (x24 x17)False)False)((x25 x16 (x24 x17)False)False)((x27 x17False)False)((x23 x17False)False)((x28 x17False)False)((x22 x17False)False)(x29 x17False)False
as obj
-
as prop
7fddd..
theory
HotG
stx
d7645..
address
TMcYG..