Function exists_until 

pub fn exists_until(
    graph: &[NQuin],
    start: u64,
    phi: u64,
    psi: u64,
    next: u64,
    holds: u64,
) -> bool

E[φ U ψ] — SOME path on which phi holds at every state until psi becomes true. Zero-heap BFS constrained to phi-states.