Search for blocks/addresses/...
Proofgold Asset
asset id
2f013a3bd95cc43c53ba1c0ef80c2601088b490488c8a859790f29cc79fc0529
asset hash
f38026460c8f34e528e46c358bcde17d0296aa223d4c6d3763f5aa82a1b51835
bday / block
21784
tx
97c92..
preasset
doc published by
Pr4zB..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
1d483..
:
∀ x0 x1 :
ι → ο
.
∀ x2 x3 x4 x5 x6 x7 .
(
∀ x8 :
ι → ο
.
x8
x2
⟶
x8
x3
⟶
x8
x4
⟶
x8
x5
⟶
x8
x6
⟶
x8
x7
⟶
∀ x9 .
x0
x9
⟶
x8
x9
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x1
x8
)
⟶
∀ x9 :
ι → ο
.
x9
x6
⟶
x9
x7
⟶
x9
x8
)
⟶
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
not
(
x1
x6
)
⟶
not
(
x1
x7
)
⟶
∀ x8 :
ι →
ι →
ι →
ι → ο
.
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x3
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x4
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x5
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x4
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x5
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x5
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x6
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x2
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x3
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x3
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x6
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x6
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x7
x9
)
)
⟶
∀ x9 :
ι →
ι →
ι →
ι → ο
.
(
∀ x10 x11 .
x0
x10
⟶
x0
x11
⟶
x9
x10
x11
x10
x11
)
⟶
(
∀ x10 x11 x12 x13 .
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x9
x10
x11
x12
x13
⟶
x9
x12
x13
x10
x11
)
⟶
(
∀ x10 x11 .
x0
x10
⟶
x0
x11
⟶
x9
x10
x11
x7
x7
)
⟶
(
∀ x10 .
x0
x10
⟶
x9
x6
x6
x7
x10
)
⟶
(
∀ x10 .
x0
x10
⟶
x9
x6
x7
x7
x10
)
⟶
x9
x2
x6
x4
x6
⟶
x9
x2
x6
x4
x7
⟶
x9
x2
x6
x5
x6
⟶
x9
x2
x6
x5
x7
⟶
x9
x2
x6
x7
x6
⟶
x9
x2
x7
x4
x7
⟶
x9
x2
x7
x5
x7
⟶
x9
x3
x6
x3
x7
⟶
x9
x3
x6
x5
x6
⟶
x9
x3
x6
x5
x7
⟶
x9
x3
x6
x6
x7
⟶
x9
x3
x6
x7
x6
⟶
x9
x3
x7
x5
x7
⟶
x9
x4
x6
x2
x7
⟶
x9
x4
x6
x4
x7
⟶
x9
x5
x6
x2
x7
⟶
x9
x5
x6
x3
x7
⟶
x9
x6
x6
x3
x7
⟶
x9
x7
x6
x2
x7
⟶
x9
x7
x6
x3
x7
⟶
x9
x7
x6
x6
x7
⟶
(
x4
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x6
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
∀ x10 .
x0
x10
⟶
∀ x11 .
x0
x11
⟶
∀ x12 .
x0
x12
⟶
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
∀ x15 .
x0
x15
⟶
∀ x16 .
x0
x16
⟶
∀ x17 .
x0
x17
⟶
∀ x18 .
x0
x18
⟶
∀ x19 .
x0
x19
⟶
∀ x20 .
x0
x20
⟶
∀ x21 .
x0
x21
⟶
not
(
x1
x11
)
⟶
x8
x10
x11
x12
x13
⟶
x8
x12
x13
x14
x15
⟶
x8
x14
x15
x16
x17
⟶
x8
x16
x17
x18
x19
⟶
x8
x18
x19
x20
x21
⟶
not
(
x9
x10
x11
x12
x13
)
⟶
not
(
x9
x10
x11
x14
x15
)
⟶
not
(
x9
x10
x11
x16
x17
)
⟶
not
(
x9
x10
x11
x18
x19
)
⟶
not
(
x9
x10
x11
x20
x21
)
⟶
not
(
x9
x12
x13
x14
x15
)
⟶
not
(
x9
x12
x13
x16
x17
)
⟶
not
(
x9
x12
x13
x18
x19
)
⟶
not
(
x9
x12
x13
x20
x21
)
⟶
not
(
x9
x14
x15
x16
x17
)
⟶
not
(
x9
x14
x15
x18
x19
)
⟶
not
(
x9
x14
x15
x20
x21
)
⟶
not
(
x9
x16
x17
x18
x19
)
⟶
not
(
x9
x16
x17
x20
x21
)
⟶
not
(
x9
x18
x19
x20
x21
)
⟶
False
Known
ab61b..
:
∀ x0 x1 :
ι → ο
.
∀ x2 x3 x4 x5 x6 x7 .
(
∀ x8 :
ι → ο
.
x8
x2
⟶
x8
x3
⟶
x8
x4
⟶
x8
x5
⟶
x8
x6
⟶
x8
x7
⟶
∀ x9 .
x0
x9
⟶
x8
x9
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x1
x8
)
⟶
∀ x9 :
ι → ο
.
x9
x6
⟶
x9
x7
⟶
x9
x8
)
⟶
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
not
(
x1
x6
)
⟶
not
(
x1
x7
)
⟶
∀ x8 :
ι →
ι →
ι →
ι → ο
.
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x4
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x6
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x2
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x3
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x2
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x3
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x3
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x4
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x4
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x5
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x5
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x6
x9
x6
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x6
x9
)
)
⟶
(
∀ x9 .
x0
x9
⟶
not
(
x8
x7
x9
x7
x9
)
)
⟶
∀ x9 :
ι →
ι →
ι →
ι → ο
.
(
∀ x10 x11 .
x0
x10
⟶
x0
x11
⟶
x9
x10
x11
x10
x11
)
⟶
(
∀ x10 x11 x12 x13 .
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x9
x10
x11
x12
x13
⟶
x9
x12
x13
x10
x11
)
⟶
(
∀ x10 x11 .
x0
x10
⟶
x0
x11
⟶
x9
x10
x11
x7
x7
)
⟶
(
∀ x10 .
x0
x10
⟶
x9
x6
x6
x7
x10
)
⟶
(
∀ x10 .
x0
x10
⟶
x9
x6
x7
x7
x10
)
⟶
x9
x2
x2
x4
x6
⟶
x9
x2
x2
x5
x6
⟶
x9
x3
x2
x4
x6
⟶
x9
x3
x2
x5
x6
⟶
x9
x4
x2
x4
x6
⟶
x9
x4
x2
x5
x7
⟶
x9
x4
x7
x6
x2
⟶
x9
x5
x2
x5
x6
⟶
x9
x6
x2
x6
x7
⟶
x9
x2
x6
x4
x6
⟶
x9
x2
x6
x4
x7
⟶
x9
x2
x6
x5
x6
⟶
x9
x2
x6
x5
x7
⟶
x9
x2
x6
x7
x6
⟶
x9
x2
x7
x4
x7
⟶
x9
x2
x7
x5
x7
⟶
x9
x3
x6
x3
x7
⟶
x9
x3
x6
x5
x6
⟶
x9
x3
x6
x5
x7
⟶
x9
x3
x6
x6
x7
⟶
x9
x3
x6
x7
x6
⟶
x9
x3
x7
x5
x7
⟶
x9
x4
x6
x2
x7
⟶
x9
x4
x6
x4
x7
⟶
x9
x5
x6
x2
x7
⟶
x9
x5
x6
x3
x7
⟶
x9
x6
x6
x3
x7
⟶
x9
x7
x6
x2
x7
⟶
x9
x7
x6
x3
x7
⟶
x9
x7
x6
x6
x7
⟶
(
x4
=
x5
⟶
∀ x10 : ο .
x10
)
⟶
(
x5
=
x6
⟶
∀ x10 : ο .
x10
)
⟶
(
x6
=
x7
⟶
∀ x10 : ο .
x10
)
⟶
(
∀ x10 :
ι → ο
.
x10
x2
⟶
x10
x3
⟶
x10
x4
⟶
x10
x5
⟶
∀ x11 .
x1
x11
⟶
x10
x11
)
⟶
(
∀ x10 .
x0
x10
⟶
∀ x11 .
x1
x11
⟶
∀ x12 .
x0
x12
⟶
∀ x13 .
x0
x13
⟶
not
(
x1
x13
)
⟶
x8
x10
x11
x12
x13
)
⟶
(
∀ x10 x11 x12 x13 .
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
∀ x14 : ο .
(
x8
x10
x11
x12
x13
⟶
x14
)
⟶
(
x9
x10
x11
x12
x13
⟶
x14
)
⟶
(
x8
x12
x13
x10
x11
⟶
x14
)
⟶
x14
)
⟶
∀ x10 x11 x12 :
ι →
ι → ι
.
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x10
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x10
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x10
x13
(
x10
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x10
x13
x2
=
x3
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x11
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x11
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x11
x13
(
x11
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x11
x13
x2
=
x4
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x12
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x12
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x12
x13
(
x12
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x12
x13
x2
=
x5
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x10
x13
x14
)
x15
(
x10
x15
x16
)
)
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x11
x13
x14
)
x15
(
x11
x15
x16
)
)
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x12
x13
x14
)
x15
(
x12
x15
x16
)
)
)
⟶
∀ x13 .
x1
x13
⟶
∀ x14 .
x0
x14
⟶
∀ x15 .
x0
x15
⟶
∀ x16 .
x0
x16
⟶
∀ x17 .
x0
x17
⟶
∀ x18 .
x0
x18
⟶
∀ x19 .
x0
x19
⟶
∀ x20 .
x0
x20
⟶
∀ x21 .
x0
x21
⟶
∀ x22 .
x0
x22
⟶
∀ x23 .
x0
x23
⟶
∀ x24 .
x0
x24
⟶
not
(
x1
x16
)
⟶
x8
x14
x13
x15
x16
⟶
x8
x15
x16
x17
x18
⟶
x8
x17
x18
x19
x20
⟶
x8
x19
x20
x21
x22
⟶
x8
x21
x22
x23
x24
⟶
not
(
x9
x14
x13
x15
x16
)
⟶
not
(
x9
x14
x13
x17
x18
)
⟶
not
(
x9
x14
x13
x19
x20
)
⟶
not
(
x9
x14
x13
x21
x22
)
⟶
not
(
x9
x14
x13
x23
x24
)
⟶
not
(
x9
x15
x16
x17
x18
)
⟶
not
(
x9
x15
x16
x19
x20
)
⟶
not
(
x9
x15
x16
x21
x22
)
⟶
not
(
x9
x15
x16
x23
x24
)
⟶
not
(
x9
x17
x18
x19
x20
)
⟶
not
(
x9
x17
x18
x21
x22
)
⟶
not
(
x9
x17
x18
x23
x24
)
⟶
not
(
x9
x19
x20
x21
x22
)
⟶
not
(
x9
x19
x20
x23
x24
)
⟶
not
(
x9
x21
x22
x23
x24
)
⟶
False
Known
3dd41..
:
∀ x0 x1 :
ι → ο
.
∀ x2 x3 x4 x5 x6 x7 .
(
∀ x8 :
ι → ο
.
x8
x2
⟶
x8
x3
⟶
x8
x4
⟶
x8
x5
⟶
x8
x6
⟶
x8
x7
⟶
∀ x9 .
x0
x9
⟶
x8
x9
)
⟶
(
∀ x8 :
ι → ο
.
x8
x2
⟶
x8
x3
⟶
x8
x4
⟶
x8
x5
⟶
∀ x9 .
x1
x9
⟶
x8
x9
)
⟶
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
(
x2
=
x3
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x4
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x5
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x6
⟶
∀ x8 : ο .
x8
)
⟶
(
x2
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
∀ x8 :
ι →
ι →
ι →
ι → ο
.
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x3
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x4
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x5
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x2
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x3
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x4
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x6
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x5
)
)
⟶
(
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
not
(
x8
x9
x7
x10
x6
)
)
⟶
∀ x9 :
ι →
ι →
ι →
ι → ο
.
(
∀ x10 x11 x12 x13 .
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
∀ x14 : ο .
(
x8
x10
x11
x12
x13
⟶
x14
)
⟶
(
x9
x10
x11
x12
x13
⟶
x14
)
⟶
(
x8
x12
x13
x10
x11
⟶
x14
)
⟶
x14
)
⟶
(
∀ x10 x11 x12 x13 .
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x9
x10
x11
x12
x13
⟶
x9
x12
x13
x10
x11
)
⟶
∀ x10 x11 x12 :
ι →
ι → ι
.
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x10
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x10
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x10
x13
(
x10
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x10
x13
x2
=
x3
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x11
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x11
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x11
x13
(
x11
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x11
x13
x2
=
x4
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x0
(
x12
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x1
x14
⟶
x1
(
x12
x13
x14
)
)
⟶
(
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
x12
x13
(
x12
x13
x14
)
=
x14
)
⟶
(
∀ x13 .
x0
x13
⟶
x12
x13
x2
=
x5
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x10
x13
x14
)
x15
(
x10
x15
x16
)
)
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x11
x13
x14
)
x15
(
x11
x15
x16
)
)
)
⟶
(
∀ x13 x14 x15 x16 .
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
not
(
x9
x13
x14
x15
x16
)
⟶
not
(
x9
x13
(
x12
x13
x14
)
x15
(
x12
x15
x16
)
)
)
⟶
∀ x13 .
x1
x13
⟶
∀ x14 .
x0
x14
⟶
∀ x15 .
x0
x15
⟶
∀ x16 .
x0
x16
⟶
x1
x16
⟶
∀ x17 .
x0
x17
⟶
∀ x18 .
x0
x18
⟶
∀ x19 .
x0
x19
⟶
∀ x20 .
x0
x20
⟶
∀ x21 .
x0
x21
⟶
∀ x22 .
x0
x22
⟶
∀ x23 .
x0
x23
⟶
∀ x24 .
x0
x24
⟶
not
(
x9
x14
x13
x15
x16
)
⟶
not
(
x9
x14
x13
x17
x18
)
⟶
not
(
x9
x14
x13
x19
x20
)
⟶
not
(
x9
x14
x13
x21
x22
)
⟶
not
(
x9
x14
x13
x23
x24
)
⟶
not
(
x9
x15
x16
x17
x18
)
⟶
not
(
x9
x15
x16
x19
x20
)
⟶
not
(
x9
x15
x16
x21
x22
)
⟶
not
(
x9
x15
x16
x23
x24
)
⟶
not
(
x9
x17
x18
x19
x20
)
⟶
not
(
x9
x17
x18
x21
x22
)
⟶
not
(
x9
x17
x18
x23
x24
)
⟶
not
(
x9
x19
x20
x21
x22
)
⟶
not
(
x9
x19
x20
x23
x24
)
⟶
not
(
x9
x21
x22
x23
x24
)
⟶
∀ x25 : ο .
(
∀ x26 .
x0
x26
⟶
∀ x27 .
x0
x27
⟶
x1
x27
⟶
∀ x28 .
x0
x28
⟶
∀ x29 .
x0
x29
⟶
∀ x30 .
x0
x30
⟶
∀ x31 .
x0
x31
⟶
∀ x32 .
x0
x32
⟶
∀ x33 .
x0
x33
⟶
∀ x34 .
x0
x34
⟶
∀ x35 .
x0
x35
⟶
∀ x36 .
x0
x36
⟶
x8
x26
x2
x28
x27
⟶
x8
x28
x27
x29
x30
⟶
x8
x29
x30
x31
x32
⟶
x8
x31
x32
x33
x34
⟶
x8
x33
x34
x35
x36
⟶
not
(
x9
x26
x2
x28
x27
)
⟶
not
(
x9
x26
x2
x29
x30
)
⟶
not
(
x9
x26
x2
x31
x32
)
⟶
not
(
x9
x26
x2
x33
x34
)
⟶
not
(
x9
x26
x2
x35
x36
)
⟶
not
(
x9
x28
x27
x29
x30
)
⟶
not
(
x9
x28
x27
x31
x32
)
⟶
not
(
x9
x28
x27
x33
x34
)
⟶
not
(
x9
x28
x27
x35
x36
)
⟶
not
(
x9
x29
x30
x31
x32
)
⟶
not
(
x9
x29
x30
x33
x34
)
⟶
not
(
x9
x29
x30
x35
x36
)
⟶
not
(
x9
x31
x32
x33
x34
)
⟶
not
(
x9
x31
x32
x35
x36
)
⟶
not
(
x9
x33
x34
x35
x36
)
⟶
x25
)
⟶
x25
Known
946c5..
:
∀ x0 :
ι → ο
.
∀ x1 x2 x3 x4 x5 x6 .
(
∀ x7 :
ι → ο
.
x7
x1
⟶
x7
x2
⟶
x7
x3
⟶
x7
x4
⟶
x7
x5
⟶
x7
x6
⟶
∀ x8 .
x0
x8
⟶
x7
x8
)
⟶
x0
x1
⟶
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
∀ x7 :
ι →
ι →
ι →
ι → ο
.
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x2
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x3
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x3
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x4
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x4
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x5
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x1
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x2
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x2
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x5
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x5
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x6
x8
)
)
⟶
∀ x8 :
ι →
ι →
ι →
ι → ο
.
(
∀ x9 x10 x11 x12 .
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x8
x9
x10
x11
x12
⟶
x8
x11
x12
x9
x10
)
⟶
(
∀ x9 x10 .
x0
x9
⟶
x0
x10
⟶
x8
x9
x10
x6
x6
)
⟶
(
∀ x9 .
x0
x9
⟶
x8
x5
x5
x6
x9
)
⟶
(
∀ x9 .
x0
x9
⟶
x8
x5
x6
x6
x9
)
⟶
x8
x1
x1
x1
x3
⟶
x8
x1
x1
x1
x5
⟶
x8
x1
x1
x2
x1
⟶
x8
x1
x1
x2
x2
⟶
x8
x1
x1
x2
x5
⟶
x8
x1
x1
x3
x3
⟶
x8
x1
x1
x3
x4
⟶
x8
x1
x1
x3
x5
⟶
x8
x1
x1
x4
x2
⟶
x8
x1
x1
x4
x3
⟶
x8
x1
x1
x4
x5
⟶
x8
x1
x1
x5
x3
⟶
x8
x1
x1
x5
x4
⟶
x8
x1
x1
x6
x1
⟶
x8
x1
x1
x6
x3
⟶
x8
x1
x1
x6
x4
⟶
x8
x1
x2
x1
x4
⟶
x8
x1
x2
x1
x6
⟶
x8
x1
x2
x2
x1
⟶
x8
x1
x2
x2
x2
⟶
x8
x1
x2
x2
x6
⟶
x8
x1
x2
x3
x3
⟶
x8
x1
x2
x3
x4
⟶
x8
x1
x2
x3
x6
⟶
x8
x1
x2
x4
x1
⟶
x8
x1
x2
x4
x4
⟶
x8
x1
x2
x4
x6
⟶
x8
x1
x2
x5
x3
⟶
x8
x1
x2
x5
x4
⟶
x8
x1
x2
x6
x2
⟶
x8
x1
x2
x6
x3
⟶
x8
x1
x2
x6
x4
⟶
x8
x1
x3
x1
x6
⟶
x8
x1
x3
x2
x3
⟶
x8
x1
x3
x2
x4
⟶
x8
x1
x3
x2
x5
⟶
x8
x1
x3
x3
x1
⟶
x8
x1
x3
x3
x2
⟶
x8
x1
x3
x3
x5
⟶
x8
x1
x3
x4
x1
⟶
x8
x1
x3
x4
x4
⟶
x8
x1
x3
x4
x6
⟶
x8
x1
x3
x5
x1
⟶
x8
x1
x3
x5
x2
⟶
x8
x1
x3
x6
x1
⟶
x8
x1
x3
x6
x2
⟶
x8
x1
x3
x6
x3
⟶
x8
x1
x4
x1
x5
⟶
x8
x1
x4
x2
x3
⟶
x8
x1
x4
x2
x4
⟶
x8
x1
x4
x2
x6
⟶
x8
x1
x4
x3
x1
⟶
x8
x1
x4
x3
x2
⟶
x8
x1
x4
x3
x6
⟶
x8
x1
x4
x4
x2
⟶
x8
x1
x4
x4
x3
⟶
x8
x1
x4
x4
x5
⟶
x8
x1
x4
x5
x1
⟶
x8
x1
x4
x5
x2
⟶
x8
x1
x4
x6
x1
⟶
x8
x1
x4
x6
x2
⟶
x8
x1
x4
x6
x4
⟶
x8
x1
x5
x2
x2
⟶
x8
x1
x5
x2
x3
⟶
x8
x1
x5
x3
x1
⟶
x8
x1
x5
x3
x4
⟶
x8
x1
x5
x3
x5
⟶
x8
x1
x5
x3
x6
⟶
x8
x1
x5
x4
x1
⟶
x8
x1
x5
x4
x4
⟶
x8
x1
x5
x4
x5
⟶
x8
x1
x5
x4
x6
⟶
x8
x1
x5
x5
x2
⟶
x8
x1
x5
x5
x3
⟶
x8
x1
x5
x6
x5
⟶
x8
x1
x6
x2
x1
⟶
x8
x1
x6
x2
x4
⟶
x8
x1
x6
x3
x2
⟶
x8
x1
x6
x3
x3
⟶
x8
x1
x6
x3
x5
⟶
x8
x1
x6
x3
x6
⟶
x8
x1
x6
x4
x2
⟶
x8
x1
x6
x4
x3
⟶
x8
x1
x6
x4
x5
⟶
x8
x1
x6
x4
x6
⟶
x8
x1
x6
x5
x1
⟶
x8
x1
x6
x5
x4
⟶
x8
x1
x6
x6
x5
⟶
x8
x2
x1
x2
x3
⟶
x8
x2
x1
x2
x6
⟶
x8
x2
x1
x3
x1
⟶
x8
x2
x1
x3
x5
⟶
x8
x2
x1
x4
x2
⟶
x8
x2
x1
x4
x3
⟶
x8
x2
x1
x4
x4
⟶
x8
x2
x1
x4
x5
⟶
x8
x2
x1
x5
x2
⟶
x8
x2
x1
x5
x3
⟶
x8
x2
x1
x5
x6
⟶
x8
x2
x1
x6
x2
⟶
x8
x2
x2
x2
x4
⟶
x8
x2
x2
x2
x5
⟶
x8
x2
x2
x3
x2
⟶
x8
x2
x2
x3
x6
⟶
x8
x2
x2
x4
x1
⟶
x8
x2
x2
x4
x3
⟶
x8
x2
x2
x4
x4
⟶
x8
x2
x2
x4
x6
⟶
x8
x2
x2
x5
x1
⟶
x8
x2
x2
x5
x4
⟶
x8
x2
x2
x5
x5
⟶
x8
x2
x2
x6
x1
⟶
x8
x2
x3
x2
x6
⟶
x8
x2
x3
x3
x3
⟶
x8
x2
x3
x3
x5
⟶
x8
x2
x3
x4
x1
⟶
x8
x2
x3
x4
x2
⟶
x8
x2
x3
x4
x4
⟶
x8
x2
x3
x4
x6
⟶
x8
x2
x3
x5
x1
⟶
x8
x2
x3
x5
x4
⟶
x8
x2
x3
x5
x6
⟶
x8
x2
x3
x6
x4
⟶
x8
x2
x4
x2
x5
⟶
x8
x2
x4
x3
x4
⟶
x8
x2
x4
x3
x6
⟶
x8
x2
x4
x4
x1
⟶
x8
x2
x4
x4
x2
⟶
x8
x2
x4
x4
x3
⟶
x8
x2
x4
x4
x5
⟶
x8
x2
x4
x5
x2
⟶
x8
x2
x4
x5
x3
⟶
x8
x2
x4
x5
x5
⟶
x8
x2
x4
x6
x3
⟶
x8
x2
x5
x2
x6
⟶
x8
x2
x5
x3
x2
⟶
x8
x2
x5
x3
x4
⟶
x8
x2
x5
x4
x5
⟶
x8
x2
x5
x4
x6
⟶
x8
x2
x5
x5
x6
⟶
x8
x2
x5
x6
x2
⟶
x8
x2
x5
x6
x4
⟶
x8
x2
x5
x6
x5
⟶
x8
x2
x6
x3
x1
⟶
x8
x2
x6
x3
x3
⟶
x8
x2
x6
x4
x5
⟶
x8
x2
x6
x4
x6
⟶
x8
x2
x6
x5
x5
⟶
x8
x2
x6
x6
x1
⟶
x8
x2
x6
x6
x3
⟶
x8
x2
x6
x6
x5
⟶
x8
x3
x1
x3
x2
⟶
x8
x3
x1
x3
x5
⟶
x8
x3
x1
x4
x2
⟶
x8
x3
x1
x4
x3
⟶
x8
x3
x1
x4
x6
⟶
x8
x3
x1
x5
x3
⟶
x8
x3
x1
x5
x4
⟶
x8
x3
x1
x6
x3
⟶
x8
x3
x1
x6
x5
⟶
x8
x3
x2
x3
x6
⟶
x8
x3
x2
x4
x1
⟶
x8
x3
x2
x4
x4
⟶
x8
x3
x2
x4
x5
⟶
x8
x3
x2
x5
x3
⟶
x8
x3
x2
x5
x4
⟶
x8
x3
x2
x6
x4
⟶
x8
x3
x2
x6
x5
⟶
x8
x3
x3
x3
x4
⟶
x8
x3
x3
x3
x5
⟶
x8
x3
x3
x4
x1
⟶
x8
x3
x3
x4
x4
⟶
x8
x3
x3
x4
x5
⟶
x8
x3
x3
x5
x1
⟶
x8
x3
x3
x5
x2
⟶
x8
x3
x3
x6
x1
⟶
x8
x3
x3
x6
x5
⟶
x8
x3
x4
x3
x6
⟶
x8
x3
x4
x4
x2
⟶
x8
x3
x4
x4
x3
⟶
x8
x3
x4
x4
x6
⟶
x8
x3
x4
x5
x1
⟶
x8
x3
x4
x5
x2
⟶
x8
x3
x4
x6
x2
⟶
x8
x3
x4
x6
x5
⟶
x8
x3
x5
x1
x6
⟶
x8
x3
x5
x3
x6
⟶
x8
x3
x5
x5
x2
⟶
x8
x3
x5
x5
x4
⟶
x8
x3
x6
x5
x1
⟶
x8
x3
x6
x5
x3
⟶