Issue with the SPeCS Containment Solver in relation to the UNION operator

For two queries where one has to check for containment relation in between them.

Query 1:

PREFIX saref: <https://saref.etsi.org/core/> 
PREFIX dahccsensors: <https://dahcc.idlab.ugent.be/Homelab/SensorsAndActuators/> 
PREFIX ex: <https://rsp.js> 
SELECT ?o2
WHERE { 
{ ?s saref:hasValue ?o . ?s saref:relatesToProperty dahccsensors:x . } 
UNION
{ ?s saref:hasValue ?o2 . ?s saref:relatesToProperty dahccsensors:y . }
}

Query 2:

PREFIX dahccsensors: <https://dahcc.idlab.ugent.be/Homelab/SensorsAndActuators/> 
PREFIX saref: <https://saref.etsi.org/core/> 
PREFIX ex: <https://rsp.js> 
SELECT ?o2 
WHERE
{ 
?s saref:hasValue ?o2 . ?s saref:relatesToProperty dahccsensors:y . 
}

Semantically from looking at the queries, you can see that the Query 2 is contained in Query 1.

However, the SPeCS Containment Solver provides a negative containment result with the two SPARQL Queries.

The SMT formula generated for the two queries when doing a containment check is,

; ------------ Sort and Predicate -------------------
(declare-sort RDFValue 0)
 
(declare-fun P (RDFValue RDFValue RDFValue RDFValue) Bool)
 
(declare-fun f_str (RDFValue) RDFValue)
(declare-fun f_xsd_string (RDFValue) RDFValue)
(declare-fun f_datatype (RDFValue) RDFValue)
(declare-fun f_lcase (RDFValue) RDFValue)
(declare-fun f_round (RDFValue) RDFValue)
(declare-fun f_abs (RDFValue) RDFValue)
 
(declare-fun f_isliteral (RDFValue) Bool)
(declare-fun f_isuri (RDFValue) Bool)
(declare-fun f_contains (RDFValue RDFValue) Bool)
(declare-fun f_regex (RDFValue RDFValue) Bool)
 
(declare-fun f_add (RDFValue RDFValue) RDFValue)
(declare-fun f_sub (RDFValue RDFValue) RDFValue)
(declare-fun f_mul (RDFValue RDFValue) RDFValue)
(declare-fun f_div (RDFValue RDFValue) RDFValue)
 
(declare-fun f_lt (RDFValue RDFValue) Bool)
(declare-fun f_gt (RDFValue RDFValue) Bool)
(declare-fun f_leq (RDFValue RDFValue) Bool)
(declare-fun f_geq (RDFValue RDFValue) Bool)
 
(declare-fun f_bound (RDFValue) Bool)
 
(declare-const <default_graph> RDFValue)
 
; Ensure quads default to default graph
(assert 
  (forall ((s RDFValue) (p RDFValue) (o RDFValue) (g RDFValue))
    (=> (P s p o g) (P s p o <default_graph>))
  )
)
 
; ------------ IRIs ---------------------------------
(declare-const <p0_Resourse> RDFValue)
(declare-const <p1_x> RDFValue)
(declare-const <p1_y> RDFValue)
(declare-const <p3_hasValue> RDFValue)
(declare-const <p3_relatesToProperty> RDFValue)
(declare-const <p_Property> RDFValue)
 
; ------------ Variables ----------------------------
(declare-const <v2_o> RDFValue)
(declare-const <v2_s> RDFValue)
 
; ------------ Assumption (from Query 1) ------------
(assert 
  (and 
    (P <v2_s> <p3_hasValue> <v2_o> <default_graph>) 
    (P <v2_s> <p3_relatesToProperty> <p1_x> <default_graph>)
  )
)
 
; ------------ Conjecture (from Query 2) ------------
(assert 
  (not 
    (exists ((<v1_o2> RDFValue) (<v1_s> RDFValue)) 
      (and 
        (P <v1_s> <p3_hasValue> <v1_o2> <default_graph>) 
        (P <v1_s> <p3_relatesToProperty> <p1_y> <default_graph>) 
        (= <v1_o2> <v2_o2>)
      )
    )
  )
)
 
; ------------ Check-Sat ----------------------------
(check-sat)
 

Here one can see that the formula only models the first branch of the UNION query (i.e the AccelerationX) and not the second (with AccelerationY)

which is,

(assert 
  (and 
    (P <v2_s> <p3_hasValue> <v2_o> <default_graph>) 
    (P <v2_s> <p3_relatesToProperty> <p1_x> <default_graph>) 
  )
)

The Query 2, with which I was trying to find a containment relation works with the second branch (AccelerationY) which the SPeCS solver ignored to create the formula, thus giving a false containment result.

Instead it should have been the following formula,

(assert
  (or
    (and
      (P <v2_s> <p3_hasValue> <v2_o2> <default_graph>)
      (P <v2_s> <p3_relatesToProperty> <p1_x> <default_graph>)
    )
    (and
      (P <v2_s> <p3_hasValue> <v2_o2> <default_graph>)
      (P <v2_s> <p3_relatesToProperty> <p1_y> <default_graph>)
    )
  )
)

which would have provided a valid containment relation in between the both queries.