Alloy* does not stop solving in a very small higher-order space

Question

I'm using Alloy* hola-0.2.jar to represent and study higher-order problems. The following code check isAR for 1 but exactly 1 Node, exactly 1 Edge should fail with only one counterexample.

Yes, Alloy* finds the counterexample quickly. However, when I click "Next" to try to find another counterexample, the solver never finish it. (I run this for at least 3 hours in my macbook pro.)

Indeed, by theory, no more counterexample exists. So Alloy* should state No counterexample found. Assertion may be valid. But, it never pop up.

I'm aware that solving higher-order problems requires more computational effort. However this problem of mine is very small. So I doubt my code. What's the problem?

// a Heyting Algebra of subgraphs of a given graph

sig Node {}
sig Edge {
    source: Node,
    target: Node}
fun Edge.proj : set Node { this.source + this.target}
pred isGraph[ns: set Node, es: set Edge] {es.proj in ns}

// Cmpl[sns,ses,cns,ces] means: a pseudo-complement of a subgraph s is a subgraph c.
pred Cmpl[sns: set Node, ses: set Edge, cns: set Node, ces: set Edge] { 
    !((cns!=none or ces!=none) and Node in sns and Edge in ses)
    Node in sns + cns
    Edge in ses + ces
    all ns: set Node | all es: set Edge when isGraph[ns,es] and (Node in sns + ns) and (Edge in ses + es)|
        (cns in ns and ces in es)
}

/* An element x of a Heyting algebra H is called regular 
 * if x = ¬y for some y in H. 
 */

pred isRegular [xns: set Node, xes: set Edge] {
    some yns: set Node | some yes: set Edge when isGraph[yns,yes]|
        one cyns: set Node | one cyes: set Edge |
            isGraph[cyns,cyes] and Cmpl[yns,yes,cyns,cyes] and (cyns=xns and cyes=xes)
}

assert isAR { // is always regular?
    all subns: set Node, subes: set Edge when isGraph[subns,subes] |
        isRegular[subns,subes]
} 

check isAR for 1 but exactly 1 Node, exactly 1 Edge 
// this should fail with 1 couterexample (by theory)