(set-option :backend none)
(declare-datatype Node ( ( |1| ) ( |2| ) ( |3| )))
(declare-fun Edge (Node Node) Bool)
(declare-fun phi (Node Node Node) Bool)
(x-interpret-pred Edge
(x-set
(|1| |2|)
(|2| |3|)
(|1| |3|)
)
)
(assert (forall ((x Node) (y Node) (z Node))
(=> (and (Edge x y) (Edge y z) (Edge x z))
(phi x y z)
)))
(assert (forall ((x Node)) (Edge x x)))
(assert (exists ((x Node) (y Node)) (Edge x y)))
(x-ground)
(x-debug solver groundings)
(check-sat)
------- RESULTS ------------------
(declare-datatype Node ((|1|) (|2|) (|3|)))
(declare-fun Edge (Node Node) Bool)
(declare-fun phi (Node Node Node) Bool)
(assert (phi |1| |2| |3|))
(assert false)
Groundings:
=== x ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node.G AS G
FROM _xmt_sort_node
=== y ======================================
-- Join(0)
SELECT _xmt_sort_node_1.G AS y,
_xmt_sort_node_1.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
=== (Edge x y) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_2.a_1 AS x,
_xmt_interp_edge_UF_2.a_2 AS y,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_2.a_1 AS x,
_xmt_interp_edge_G_2.a_2 AS y,
_xmt_interp_edge_G_2.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_2
=== (not (Edge x y)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_2.a_1 AS x,
_xmt_interp_edge_UF_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_2
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"false" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_2.a_1 AS x,
_xmt_interp_edge_G_2.a_2 AS y,
not_(_xmt_interp_edge_G_2.G) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_2
=== z ======================================
-- Join(0)
SELECT _xmt_sort_node_4.G AS z,
_xmt_sort_node_4.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
=== (Edge y z) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_5.a_1 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_5.a_1 AS y,
_xmt_interp_edge_UF_5.a_2 AS z,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_5
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_5.a_1 AS y,
_xmt_interp_edge_G_5.a_2 AS z,
_xmt_interp_edge_G_5.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_5
=== (not (Edge y z)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_5.a_1 AS y,
_xmt_interp_edge_UF_5.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_5
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_5.a_1 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
"false" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_5.a_1 AS y,
_xmt_interp_edge_G_5.a_2 AS z,
not_(_xmt_interp_edge_G_5.G) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_5
=== (Edge x z) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_7.a_1 AS x,
_xmt_interp_edge_TU_7.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_7.a_1 AS x,
_xmt_interp_edge_UF_7.a_2 AS z,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_7
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_7.a_1 AS x,
_xmt_interp_edge_G_7.a_2 AS z,
_xmt_interp_edge_G_7.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_7
=== (not (Edge x z)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_7.a_1 AS x,
_xmt_interp_edge_UF_7.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_7
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_7.a_1 AS x,
_xmt_interp_edge_TU_7.a_2 AS z,
"false" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_7.a_1 AS x,
_xmt_interp_edge_G_7.a_2 AS z,
not_(_xmt_interp_edge_G_7.G) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_7
=== (phi x y z) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_1.G AS y,
_xmt_sort_node_4.G AS z,
apply("phi", _xmt_sort_node.G, _xmt_sort_node_1.G, _xmt_sort_node_4.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node AS _xmt_sort_node_4
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_1.G AS y,
_xmt_sort_node_4.G AS z,
apply("phi", _xmt_sort_node.G, _xmt_sort_node_1.G, _xmt_sort_node_4.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node AS _xmt_sort_node_4
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_1.G AS y,
_xmt_sort_node_4.G AS z,
apply("phi", _xmt_sort_node.G, _xmt_sort_node_1.G, _xmt_sort_node_4.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node AS _xmt_sort_node_4
=== (or (not (Edge x y)) (not (Edge y z)) (not (Edge x z)) (phi x y z)) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT x, y, z,
or_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT negate_3_UF.x AS x,
negate_3_UF.y AS y,
_xmt_sort_node_4.G AS z,
negate_3_UF.G AS G
FROM (-- Join(22)
SELECT _xmt_interp_edge_UF_2.a_1 AS x,
_xmt_interp_edge_UF_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_2
) AS negate_3_UF
JOIN _xmt_sort_node AS _xmt_sort_node_4
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS x,
negate_6_UF.y AS y,
negate_6_UF.z AS z,
negate_6_UF.G AS G
FROM (-- Join(22)
SELECT _xmt_interp_edge_UF_5.a_1 AS y,
_xmt_interp_edge_UF_5.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_5
) AS negate_6_UF
JOIN _xmt_sort_node
UNION ALL
-- Join(14)
SELECT negate_8_UF.x AS x,
_xmt_sort_node_1.G AS y,
negate_8_UF.z AS z,
negate_8_UF.G AS G
FROM (-- Join(22)
SELECT _xmt_interp_edge_UF_7.a_1 AS x,
_xmt_interp_edge_UF_7.a_2 AS z,
"true" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_7
) AS negate_8_UF
JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_1.G AS y,
_xmt_sort_node_4.G AS z,
apply("phi", _xmt_sort_node.G, _xmt_sort_node_1.G, _xmt_sort_node_4.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node AS _xmt_sort_node_4)
WHERE G <> "false")
GROUP BY x, y, z
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_2.a_1 AS x,
_xmt_interp_edge_G_2.a_2 AS y,
_xmt_interp_edge_G_5.a_2 AS z,
or_(not_(_xmt_interp_edge_G_2.G), not_(_xmt_interp_edge_G_5.G), not_(_xmt_interp_edge_G_7.G), apply("phi", _xmt_interp_edge_G_2.a_1, _xmt_interp_edge_G_2.a_2, _xmt_interp_edge_G_5.a_2)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_2
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_5
ON _xmt_interp_edge_G_2.a_2 = _xmt_interp_edge_G_5.a_1
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_7
ON _xmt_interp_edge_G_2.a_1 = _xmt_interp_edge_G_7.a_1
AND _xmt_interp_edge_G_5.a_2 = _xmt_interp_edge_G_7.a_2
=== (top) (forall ((x Node) (y Node) (z Node)) (or (not (Edge x y)) (not (Edge y z)) (not (Edge x z)) (phi x y z))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, NULL AS z, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, NULL AS z, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
=== (Edge x x) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_12.a_1 AS x,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_12
WHERE _xmt_interp_edge_TU_12.a_1 = _xmt_interp_edge_TU_12.a_2
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_12.a_1 AS x,
_xmt_interp_edge_G_12.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_12
WHERE _xmt_interp_edge_G_12.a_1 = _xmt_interp_edge_G_12.a_2
=== (top) (forall ((x Node)) (Edge x x)) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
----- F ------------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
=== (top) (exists ((x Node) (y Node)) (Edge x y)) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2)
----- F ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "false" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "false" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2)
=== (top) (and (forall ((x Node) (y Node) (z Node)) (or (not (Edge x y)) (not (Edge y z)) (not (Edge x z)) (phi x y z))) (forall ((x Node)) (Edge x x)) (exists ((x Node) (y Node)) (Edge x y))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT and_(Agg_11_TU.G, Agg_13_TU.G, Agg_14_TU.G) AS G
FROM (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, NULL AS z, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
) AS Agg_11_TU
JOIN (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
) AS Agg_13_TU
JOIN (-- Agg (8)
SELECT or_aggregate(G) as G
FROM (-- Join(15)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2)
) AS Agg_14_TU
----- F ------------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- exclude(7)
SELECT *
FROM (-- Agg (14)
SELECT G as G
FROM (-- Join(21)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
UNION ALL
-- Agg (14)
SELECT G as G
FROM (-- Join(21)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
UNION ALL
-- Agg (14)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "false" AS G
UNION ALL
-- Join(21)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2))
WHERE G <> "true")
----- G ------------------------------------------------------------
-- Join(0)
SELECT and_(Agg_11_G.G, Agg_13_G.G, Agg_14_G.G) AS G
FROM (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, NULL AS z, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
_xmt_interp_edge_TU_5.a_2 AS z,
apply("phi", _xmt_interp_edge_TU_2.a_1, _xmt_interp_edge_TU_2.a_2, _xmt_interp_edge_TU_5.a_2) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
ON _xmt_interp_edge_TU_2.a_2 = _xmt_interp_edge_TU_5.a_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_7
ON _xmt_interp_edge_TU_2.a_1 = _xmt_interp_edge_TU_7.a_1
AND _xmt_interp_edge_TU_5.a_2 = _xmt_interp_edge_TU_7.a_2)
) AS Agg_11_G
JOIN (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_UF_12.a_1 AS x,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_12
WHERE _xmt_interp_edge_UF_12.a_1 = _xmt_interp_edge_UF_12.a_2)
) AS Agg_13_G
JOIN (-- Agg (8)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "false" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_2.a_1 AS x,
_xmt_interp_edge_TU_2.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_2)
) AS Agg_14_G
===========================================
(check-sat)