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 . (x31 (x30 x35 x34 x36 x37) (x29 x35 x34 x36 x37) = x37False)x36 = x32 x35 x34x33 x37 x36False)(∀ x34 x35 x36 x37 . (x1 (x2 x35 x34 x36 x37) (x3 x35 x34 x36 x37) = x37False)x36 = x0 x35 x34x33 x37 x36False)(∀ x34 x35 x36 x37 . (x33 (x29 x35 x34 x36 x37) x34False)x36 = x32 x35 x34x33 x37 x36False)(∀ x34 x35 x36 x37 . (x33 (x30 x35 x34 x36 x37) x35False)x36 = x32 x35 x34x33 x37 x36False)(∀ x34 x35 x36 x37 . (x33 (x3 x35 x34 x36 x37) x34False)x36 = x0 x35 x34x33 x37 x36False)(∀ x34 x35 x36 x37 . (x33 (x2 x35 x34 x36 x37) x35False)x36 = x0 x35 x34x33 x37 x36False)(∀ x34 x35 x36 . (x34 = x0 x36 x35False)(x1 (x27 x36 x35 x34) (x28 x36 x35 x34) = x26 x36 x35 x34False)(x33 (x26 x36 x35 x34) x34False)False)(∀ x34 x35 x36 . (x34 = x32 x36 x35False)(x31 (x5 x36 x35 x34) (x4 x36 x35 x34) = x6 x36 x35 x34False)(x33 (x6 x36 x35 x34) x34False)False)(∀ x34 x35 x36 x37 x38 . (x38 = x0 x36 x37False)x26 x36 x37 x38 = x1 x35 x34x33 x34 x37x33 x35 x36x33 (x26 x36 x37 x38) x38False)(∀ x34 x35 x36 x37 x38 . (x38 = x32 x36 x37False)x6 x36 x37 x38 = x31 x35 x34x33 x34 x37x33 x35 x36x33 (x6 x36 x37 x38) x38False)(∀ x34 x35 x36 . (x35 = x0 x36 x34False)(x33 (x26 x36 x34 x35) x35False)(x33 (x28 x36 x34 x35) x34False)False)(∀ x34 x35 x36 . (x35 = x0 x34 x36False)(x33 (x26 x34 x36 x35) x35False)(x33 (x27 x34 x36 x35) x34False)False)(∀ x34 x35 x36 . (x35 = x32 x36 x34False)(x33 (x6 x36 x34 x35) x35False)(x33 (x4 x36 x34 x35) x34False)False)(∀ x34 x35 x36 . (x35 = x32 x34 x36False)(x33 (x6 x34 x36 x35) x35False)(x33 (x5 x34 x36 x35) x34False)False)(∀ x34 x35 x36 x37 x38 x39 . (x33 x38 x39False)x39 = x0 x35 x34x38 = x1 x36 x37x33 x37 x34x33 x36 x35False)(∀ x34 x35 x36 x37 x38 x39 . (x33 x38 x39False)x39 = x32 x35 x34x38 = x31 x36 x37x33 x37 x34x33 x36 x35False)(∀ x34 x35 . (x25 x35 x34False)x33 (x24 x35 x34) x34False)(∀ x34 x35 x36 . (x7 x35 x36False)x33 x35 x34x7 x34 (x8 x36)False)(∀ x34 x35 . x23 x35x22 x34 x35x7 x34 (x8 x35)False)(∀ x34 x35 x36 . x23 x36x33 x35 x34x7 x34 (x8 x36)False)(∀ x34 x35 x36 . (x33 x35 x36False)x25 x34 x36x33 x35 x34False)(∀ x34 x35 . (x23 x35False)(x22 x34 x35False)x23 x34x7 x34 (x8 x35)False)(∀ x34 x35 . (x23 x35False)(x22 x34 x35False)x23 x34x7 x34 (x8 x35)False)(∀ x34 x35 . (x25 x34 x35False)(x33 (x24 x34 x35) x34False)False)(∀ x34 x35 . (x23 x35False)x23 (x1 x35 x34)False)(∀ x34 x35 . (x23 x35False)x23 (x1 x34 x35)False)(∀ x34 x35 . (x25 x35 x34False)x7 x35 (x8 x34)False)(∀ x34 x35 . x33 x34 x35x33 x35 x34False)(∀ x34 x35 . (x23 x35False)x23 x34x7 x35 (x8 x34)False)(∀ x34 x35 . (x7 x35 (x8 x34)False)x25 x35 x34False)(∀ x34 x35 . (x23 x35False)(x33 x34 x35False)x7 x34 x35False)(∀ x34 x35 . (x7 x35 x34False)x33 x35 x34False)(∀ x34 . (x23 x34False)(x7 (x21 x34) (x8 x34)False)False)(∀ x34 . (x23 x34False)(x7 (x9 x34) (x8 x34)False)False)(∀ x34 x35 . x23 x35x33 x34 x35False)(∀ x34 . (x23 x34False)(x22 (x21 x34) x34False)False)(∀ x34 . (x23 x34False)x23 (x9 x34)False)(∀ x34 x35 . (x35 = x34False)x23 x34x23 x35False)(∀ x34 . (x34 = x20False)x23 x34False)(x25 (x0 x11 (x32 x12 x10)) (x32 (x0 x11 x12) (x0 x11 x10))False)(∀ x34 . x22 (x19 x34) x34False)(∀ x34 . x23 (x8 x34)False)(x23 x18False)(∀ x34 x35 x36 . (x31 (x1 x36 x34) (x1 x36 x35) = x1 x36 (x31 x34 x35)False)False)(∀ x34 x35 . (x31 x35 x34 = x31 x34 x35False)False)(∀ x34 x35 . (x1 x35 x34 = x1 x34 x35False)False)(∀ x34 x35 . (x0 x35 x34 = x0 x34 x35False)False)(∀ x34 x35 . (x32 x35 x34 = x32 x34 x35False)False)(∀ x34 . (x7 (x19 x34) (x8 x34)False)False)(∀ x34 . (x7 (x13 x34) (x8 x34)False)False)((x7 x10 (x8 (x8 x17))False)False)((x7 x12 (x8 (x8 x17))False)False)((x7 x11 (x8 (x8 x17))False)False)(∀ x34 . (x7 (x14 x34) x34False)False)(∀ x34 . (x31 x34 x34 = x34False)False)(∀ x34 . (x1 x34 x34 = x34False)False)(∀ x34 . (x25 x34 x34False)False)(∀ x34 . (x1 x34 x20 = x34False)False)(∀ x34 . (x31 x34 x20 = x20False)False)(∀ x34 . (x23 (x13 x34)False)False)((x23 x16False)False)((x23 x15False)False)((x23 x20False)False)((x15 = x20False)False)False
as obj
-
as prop
c4959..l32_interva1
theory
HotG
stx
47e30..
address
TMZpN..l32_interva1