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 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
SNo
x7
⟶
SNo
x8
⟶
SNo
x9
⟶
SNo
x10
⟶
SNo
x11
⟶
SNo
x12
⟶
SNo
x13
⟶
SNo
x14
⟶
SNo
x15
⟶
SNo
x16
⟶
SNo
x17
⟶
SNo
x18
⟶
SNo
x19
⟶
SNo
x20
⟶
SNo
x21
⟶
SNo
x22
⟶
SNo
x23
⟶
SNo
x24
⟶
SNo
x25
⟶
SNo
x26
⟶
SNo
x27
⟶
SNo
x28
⟶
SNo
x29
⟶
SNo
x30
⟶
SNo
x31
⟶
SNo
x32
⟶
SNo
x33
⟶
SNo
x34
⟶
SNo
x35
⟶
SNo
x36
⟶
SNo
x37
⟶
SNo
x38
⟶
SNo
x39
⟶
SNo
x40
⟶
SNo
x41
⟶
SNo
x42
⟶
minus_SNo
(
add_SNo
(
minus_SNo
x0
)
(
add_SNo
(
minus_SNo
x1
)
(
add_SNo
(
minus_SNo
x2
)
(
add_SNo
(
minus_SNo
x3
)
(
add_SNo
(
minus_SNo
x4
)
(
add_SNo
(
minus_SNo
x5
)
(
add_SNo
(
minus_SNo
x6
)
(
add_SNo
(
minus_SNo
x7
)
(
add_SNo
(
minus_SNo
x8
)
(
add_SNo
(
minus_SNo
x9
)
(
add_SNo
(
minus_SNo
x10
)
(
add_SNo
(
minus_SNo
x11
)
(
add_SNo
(
minus_SNo
x12
)
(
add_SNo
(
minus_SNo
x13
)
(
add_SNo
(
minus_SNo
x14
)
(
add_SNo
(
minus_SNo
x15
)
(
add_SNo
(
minus_SNo
x16
)
(
add_SNo
(
minus_SNo
x17
)
(
add_SNo
(
minus_SNo
x18
)
(
add_SNo
(
minus_SNo
x19
)
(
add_SNo
(
minus_SNo
x20
)
(
add_SNo
(
minus_SNo
x21
)
(
add_SNo
(
minus_SNo
x22
)
(
add_SNo
(
minus_SNo
x23
)
(
add_SNo
(
minus_SNo
x24
)
(
add_SNo
(
minus_SNo
x25
)
(
add_SNo
(
minus_SNo
x26
)
(
add_SNo
(
minus_SNo
x27
)
(
add_SNo
(
minus_SNo
x28
)
(
add_SNo
(
minus_SNo
x29
)
(
add_SNo
(
minus_SNo
x30
)
(
add_SNo
(
minus_SNo
x31
)
(
add_SNo
(
minus_SNo
x32
)
(
add_SNo
(
minus_SNo
x33
)
(
add_SNo
(
minus_SNo
x34
)
(
add_SNo
(
minus_SNo
x35
)
(
add_SNo
(
minus_SNo
x36
)
(
add_SNo
(
minus_SNo
x37
)
(
add_SNo
(
minus_SNo
x38
)
(
add_SNo
(
minus_SNo
x39
)
(
add_SNo
(
minus_SNo
x40
)
(
add_SNo
(
minus_SNo
x41
)
x42
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
add_SNo
x0
(
add_SNo
x1
(
add_SNo
x2
(
add_SNo
x3
(
add_SNo
x4
(
add_SNo
x5
(
add_SNo
x6
(
add_SNo
x7
(
add_SNo
x8
(
add_SNo
x9
(
add_SNo
x10
(
add_SNo
x11
(
add_SNo
x12
(
add_SNo
x13
(
add_SNo
x14
(
add_SNo
x15
(
add_SNo
x16
(
add_SNo
x17
(
add_SNo
x18
(
add_SNo
x19
(
add_SNo
x20
(
add_SNo
x21
(
add_SNo
x22
(
add_SNo
x23
(
add_SNo
x24
(
add_SNo
x25
(
add_SNo
x26
(
add_SNo
x27
(
add_SNo
x28
(
add_SNo
x29
(
add_SNo
x30
(
add_SNo
x31
(
add_SNo
x32
(
add_SNo
x33
(
add_SNo
x34
(
add_SNo
x35
(
add_SNo
x36
(
add_SNo
x37
(
add_SNo
x38
(
add_SNo
x39
(
add_SNo
x40
(
add_SNo
x41
(
minus_SNo
x42
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
as obj
-
as prop
3bb0e..
theory
HotG
stx
5ed54..
address
TMXAu..