Search for blocks/addresses/...
Proofgold Asset
asset id
4eccb8f024066bd7efd56e6bc1990a30e49ff8d9d58dd9bf40767d2ca2966472
asset hash
ea10a79dcc7779f3070d925fec2d8bc64d8afffa727fdf62495ed72e40fac8f1
bday / block
39537
tx
f050c..
preasset
doc published by
Pr4zB..
Param
4402e..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
cf2df..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
Subq
Subq
:
ι
→
ι
→
ο
Param
setminus
setminus
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
u10
:
ι
Param
a0244..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
62379..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2e38c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0897f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
306f8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9ed6a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fee51..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bae07..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cd4ee..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
22563..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bdc7f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
dfb78..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f8ada..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d3342..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0f762..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
55451..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f380c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
42e23..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8bcec..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1c6c9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
754da..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a4ce7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
60a51..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ea33e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9fce6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0aaf4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ce3b4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
27e6e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a89de..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f5fe1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fd185..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b7bfe..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
86078..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d29be..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5cc7a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
49015..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9dea4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f0075..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0a362..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6b1e6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e9c43..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a3d78..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
11982..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fe4dd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b5215..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f982a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f1135..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5c669..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8faa8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
458ae..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
22989..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
83885..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b7bbc..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9f4c9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
be274..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
14707..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4f588..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
218e4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0e6a7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0809e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6f746..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6e201..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
311f0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f9cba..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3cb02..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6d791..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fa7d9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fc088..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e974a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
33f3e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
87bb9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d0a24..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3ad6c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
77953..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fcbed..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ff800..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f98b7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6f07c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
60dbb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f1c88..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
97406..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0d539..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4b1cb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
72942..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
47362..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d8b5d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
55171..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1465e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ce338..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6dee7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ea964..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d1a27..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
60a50..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c059e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e9db0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
77203..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
133c1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bc7ef..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9e253..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
68ab4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
81575..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
86385..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7c588..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b019a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3d346..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
69895..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1a764..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
51ac7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f78c3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
39cca..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
34ea6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6caea..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5411..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
948b4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
58295..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4a04b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
68a6f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5d868..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8629d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ea11f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2005f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
de50b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3369f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f9d60..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ff926..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
71397..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2560b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
48a66..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
289d9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
37c80..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5a5ea..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
dd8d8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c6a41..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c2a1e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
15aa1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ccc6b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0446d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7683c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
96c77..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
07f55..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
93e63..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c222a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c61bd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
02f40..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b1def..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e68b8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5bc1a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8befb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8fb7c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9bc89..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3d118..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
33b5a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a2f4a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
79b37..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d833d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
23d0b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c1005..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
61f8f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ab383..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
856bc..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
788a1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3906f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c9658..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b72b8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cf898..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f5373..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
48106..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d4ea7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c1146..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ca8ce..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3f609..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3656c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9eb9c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
33102..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
48a69..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d9cea..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a56d9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5f015..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
903bc..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4a22a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
74e48..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
20d20..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
43c4e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f8fdb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
66dda..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3429e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
28e6a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d9823..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1b9db..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b6bd6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
26830..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
03c1b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0d1ce..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
11d3d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
53762..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1ccbe..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
73f56..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5a83..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7861e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
94275..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2ad4c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5b49..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6b6c2..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a0b66..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6d19b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
08d9f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
99903..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8a782..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
47dfa..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
22755..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3f29d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
518d7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
99ac9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
99fe6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2427f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d09b6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2997a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5904d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3c675..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
79a0f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a79f5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c3712..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f0b8a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ff600..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
87daf..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b4530..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
66bd0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
558af..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
52ac0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4c6fc..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4a27c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bde2c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
89b0b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cc2aa..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
34b68..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ed7e5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Known
87262..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
(
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
x1
x4
x5
⟶
x1
x5
x4
)
⟶
atleastp
u10
x3
⟶
4402e..
x3
x1
⟶
cf2df..
x3
x1
⟶
∀ x4 : ο .
(
a0244..
x0
x1
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
62379..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
2e38c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0897f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
306f8..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9ed6a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fee51..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
bae07..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
cd4ee..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
22563..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
bdc7f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
dfb78..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f8ada..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d3342..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0f762..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
55451..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f380c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
42e23..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
8bcec..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
1c6c9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
754da..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
a4ce7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
60a51..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ea33e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9fce6..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0aaf4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ce3b4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
27e6e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
a89de..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f5fe1..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fd185..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b7bfe..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
86078..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d29be..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5cc7a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
49015..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9dea4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f0075..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0a362..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6b1e6..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e9c43..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
a3d78..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
11982..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fe4dd..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b5215..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f982a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f1135..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5c669..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
8faa8..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
458ae..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
22989..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
83885..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b7bbc..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9f4c9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
be274..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
14707..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
4f588..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
218e4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0e6a7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0809e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6f746..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6e201..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
311f0..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f9cba..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3cb02..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6d791..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fa7d9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fc088..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e974a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
33f3e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
87bb9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d0a24..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3ad6c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
77953..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fcbed..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ff800..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f98b7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6f07c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
60dbb..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f1c88..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
97406..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0d539..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
4b1cb..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
72942..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
47362..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d8b5d..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
55171..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
1465e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ce338..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6dee7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ea964..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d1a27..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
60a50..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c059e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e9db0..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
77203..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
133c1..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
bc7ef..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9e253..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
68ab4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
81575..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
86385..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
7c588..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b019a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3d346..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
69895..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
1a764..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
51ac7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f78c3..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
39cca..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
34ea6..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6caea..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e5411..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
948b4..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
58295..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
4a04b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
68a6f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5d868..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
8629d..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ea11f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
2005f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
de50b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3369f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f9d60..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ff926..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
71397..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
2560b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
48a66..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
289d9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
37c80..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5a5ea..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
dd8d8..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c6a41..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c2a1e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
15aa1..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ccc6b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0446d..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
7683c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
96c77..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
07f55..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
93e63..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c222a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c61bd..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
02f40..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b1def..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e68b8..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5bc1a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
8befb..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
8fb7c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9bc89..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3d118..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
33b5a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
a2f4a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
79b37..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d833d..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
23d0b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c1005..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
61f8f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ab383..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
856bc..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
788a1..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3906f..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c9658..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b72b8..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
cf898..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f5373..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
48106..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d4ea7..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c1146..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ca8ce..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3f609..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3656c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9eb9c..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
33102..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
48a69..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d9cea..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
a56d9..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
5f015..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
903bc..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
4a22a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
74e48..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
20d20..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
43c4e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f8fdb..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
66dda..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
3429e..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
28e6a..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d9823..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
1b9db..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b6bd6..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
26830..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
03c1b..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0d1ce..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
11d3d..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
53762..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
1ccbe..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
73f56..
x1
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
x4
)
⟶
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶