Query
?-
holdsAt(light_red,A).
A#>2,A#<3 ?
Model
holdsAt(light_red,A │{A#>2,A#<3}) , initiates(turn_on,light_on,2) , happens(turn_on,2) , trajectory(light_on,2,light_red,A │{A#>2,A#<3}) , not stoppedIn(2,light_on,A │{A#>2,A#<3}) , not -holdsAt(B │{B\=light_on},C │{C#=<0}) , not -holdsAt(B │{B\=light_on},D │{D#>0}) , not terminates(E │{E\=turn_off},B │{B\=light_on},F │{F#=<0}) , not terminates(turn_off,B │{B\=light_on},F │{F#=<0}) , not -holdsAt(light_on,G │{G#=<0}) , not -holdsAt(light_on,H │{H#>0}) , not terminates(I │{I\=turn_off},light_on,J │{J#=<0}) , terminates(turn_off,light_on,J │{J#=<0}) , not happens(turn_off,J │{J#=<0})
Justification
-
holdsAt(light_red,A │{A#>2,A#<3}) :-
-
initiates(turn_on,light_on,2),
-
happens(turn_on,2),
-
trajectory(light_on,2,light_red,A │{A#>2,A#<3}) :-
-
not stoppedIn(2,light_on,A │{A#>2,A#<3}) :-
-
not o_stoppedIn1(2,light_on,A │{A#>2,A#<3}) :-
-
forall(K,forall(L,not o_stoppedIn1(2,light_on,A │{A#>2,A#<3},K,L))) :-
-
forall(L,not o_stoppedIn1(2,light_on,A │{A#>2,A#<3},M │{M#=<2},L)) :-
-
not o_stoppedIn1(2,light_on,A │{A#>2,A#<3},M │{M#=<2},N) :-
-
forall(L,not o_stoppedIn1(2,light_on,A │{A#>2,A#<3},O │{O#>2},L)) :-
-
not o_stoppedIn1(2,light_on,A │{A#>2,A#<3},O │{O#>2},P) :-
-
not o_stoppedIn2(2,light_on,A │{A#>2,A#<3}) :-
-
forall(Q,forall(R,not o_stoppedIn2(2,light_on,A │{A#>2,A#<3},Q,R))) :-
-
forall(R,not o_stoppedIn2(2,light_on,A │{A#>2,A#<3},S │{S#=<2},R)) :-
-
not o_stoppedIn2(2,light_on,A │{A#>2,A#<3},S │{S#=<2},T) :-
-
forall(R,not o_stoppedIn2(2,light_on,A │{A#>2,A#<3},U │{U#>2},R)) :-
-
not o_stoppedIn2(2,light_on,A │{A#>2,A#<3},U │{U#>2},V) :-
-
add_to_query :-
-
o_nmr_check :-
-
not o_chk1 :-
-
not o__chk11 :-
-
forall(W,forall(X,not o__chk11(W,X))) :-
-
forall(X,not o__chk11(B │{B\=light_on},X)) :-
-
not o__chk11(B │{B\=light_on},C │{C#=<0}) :-
-
not -holdsAt(B │{B\=light_on},C │{C#=<0}) :-
-
not o_c_holdsAt1(B │{B\=light_on},C │{C#=<0}) :-
-
not o_c_holdsAt2(B │{B\=light_on},C │{C#=<0}) :-
-
forall(Y,forall(Z,not o_c_holdsAt2(B │{B\=light_on},C │{C#=<0},Y,Z))) :-
-
forall(Z,not o_c_holdsAt2(B │{B\=light_on},C │{C#=<0},A1,Z)) :-
-
not o_c_holdsAt2(B │{B\=light_on},C │{C#=<0},A1,B1) :-
-
not o__chk11(B │{B\=light_on},D │{D#>0}) :-
-
not -holdsAt(B │{B\=light_on},D │{D#>0}) :-
-
not o_c_holdsAt1(B │{B\=light_on},D │{D#>0}) :-
-
0 #< D,
-
not initiallyN(B │{B\=light_on}).
-
not o_c_holdsAt2(B │{B\=light_on},D │{D#>0}) :-
-
forall(C1,forall(D1,not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},C1,D1))) :-
-
forall(D1,not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},E1 │{E1#>0},D1)) :-
-
not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},E1 │{E1#>0},F1) :-
-
forall(D1,not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},F │{F#=<0},D1)) :-
-
not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},F │{F#=<0},E │{E\=turn_off}) :-
-
F #< D,
-
not terminates(E │{E\=turn_off},B │{B\=light_on},F │{F#=<0}) :-
-
not o_terminates1(E │{E\=turn_off},B │{B\=light_on},F │{F#=<0}) :-
-
not o_c_holdsAt2(B │{B\=light_on},D │{D#>0},F │{F#=<0},turn_off) :-
-
F #< D,
-
not terminates(turn_off,B │{B\=light_on},F │{F#=<0}) :-
-
not o_terminates1(turn_off,B │{B\=light_on},F │{F#=<0}) :-
-
turn_off=turn_off,
-
B \= light_on.
-
forall(X,not o__chk11(light_on,X)) :-
-
not o__chk11(light_on,G │{G#=<0}) :-
-
not -holdsAt(light_on,G │{G#=<0}) :-
-
not o_c_holdsAt1(light_on,G │{G#=<0}) :-
-
not o_c_holdsAt2(light_on,G │{G#=<0}) :-
-
forall(G1,forall(H1,not o_c_holdsAt2(light_on,G │{G#=<0},G1,H1))) :-
-
forall(H1,not o_c_holdsAt2(light_on,G │{G#=<0},I1,H1)) :-
-
not o_c_holdsAt2(light_on,G │{G#=<0},I1,J1) :-
-
not o__chk11(light_on,H │{H#>0}) :-
-
not -holdsAt(light_on,H │{H#>0}) :-
-
not o_c_holdsAt1(light_on,H │{H#>0}) :-
-
0 #< H,
-
not initiallyN(light_on).
-
not o_c_holdsAt2(light_on,H │{H#>0}) :-
-
forall(K1,forall(L1,not o_c_holdsAt2(light_on,H │{H#>0},K1,L1))) :-
-
forall(L1,not o_c_holdsAt2(light_on,H │{H#>0},M1 │{M1#>0},L1)) :-
-
not o_c_holdsAt2(light_on,H │{H#>0},M1 │{M1#>0},N1) :-
-
forall(L1,not o_c_holdsAt2(light_on,H │{H#>0},J │{J#=<0},L1)) :-
-
not o_c_holdsAt2(light_on,H │{H#>0},J │{J#=<0},I │{I\=turn_off}) :-
-
J #< H,
-
not terminates(I │{I\=turn_off},light_on,J │{J#=<0}) :-
-
not o_terminates1(I │{I\=turn_off},light_on,J │{J#=<0}) :-
-
not o_c_holdsAt2(light_on,H │{H#>0},J │{J#=<0},turn_off) :-
-
J #< H,
-
terminates(turn_off,light_on,J │{J#=<0}),
-
not happens(turn_off,J │{J#=<0}) :-
-
not o_happens1(turn_off,J │{J#=<0}) :-
-
not o_happens2(turn_off,J │{J#=<0}) :-
-
turn_off=turn_off,
-
J \= 4.
-
not o_happens3(turn_off,J │{J#=<0}) :-