Query:

Answer:

Model:

Justification: Expand All+1-1Collapse All

• global_constraint :-
  • not o_chk_1 :-
    • vertex(a),
    • reachable(a) :-
      • in(d,a) :-
        • edge(d,a),
        • proved(edge(d,a)).
      • reachable(d) :-
        • in(c,d) :-
          • edge(c,d),
          • proved(edge(c,d)).
        • reachable(c) :-
          • in(b,c) :-
            • edge(b,c),
            • proved(edge(b,c)).
          • reachable(b) :-
            • in(a,b) :-
              • edge(a,b),
              • proved(edge(a,b)).
    • vertex(b),
    • proved(reachable(b)),
    • vertex(c),
    • proved(reachable(c)),
    • vertex(d),
    • proved(reachable(d)).
  • not o_chk_2 :-
    • proved(in(a,b)),
    • edge(a,c),
    • ex(a,c) :-
      • proved(edge(a,c)).
    • proved(in(b,c)),
    • edge(b,d),
    • ex(b,d) :-
      • proved(edge(b,d)).
    • proved(in(c,d)),
    • proved(in(d,a)).
  • not o_chk_3 :-
    • proved(in(a,b)),
    • proved(in(b,c)),
    • proved(in(c,d)),
    • proved(in(d,a)).