Query
?-
holdsAt(light_red, A).
A = { 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 ∉ [light_on]} , { C│ C ≤ 0} ) , not -holdsAt( { B ∉ [light_on]} , { D│ D>0} ) , not terminates( { E ∉ [turn_off]} , { B ∉ [light_on]} , { F│ F ≤ 0} ) , not terminates(turn_off, { B ∉ [light_on]} , { F│ F ≤ 0} ) , not -holdsAt(light_on, { G│ G ≤ 0} ) , not -holdsAt(light_on, { H│ H>0} ) , not terminates( { 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} ) :-
-
2.<. { A│ A>2, A<3} ,
-
{ A│ A>2, A<3} .<.2+1.
-
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) :-
-
2.<. { O│ O>2} ,
-
{ O│ O>2} .>=. { A│ A>2, A<3} .
-
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) :-
-
2.<. { U│ U>2} ,
-
{ U│ U>2} .>=. { A│ A>2, A<3} .
-
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 ∉ [light_on]} , X)) :-
-
not o__chk11( { B ∉ [light_on]} , { C│ C ≤ 0} ) :-
-
not -holdsAt( { B ∉ [light_on]} , { C│ C ≤ 0} ) :-
-
not o_c_holdsAt1( { B ∉ [light_on]} , { C│ C ≤ 0} ) :-
-
not o_c_holdsAt2( { B ∉ [light_on]} , { C│ C ≤ 0} ) :-
-
forall( Y,forall( Z,not o_c_holdsAt2( { B ∉ [light_on]} , { C│ C ≤ 0} , Y, Z))) :-
-
forall( Z,not o_c_holdsAt2( { B ∉ [light_on]} , { C│ C ≤ 0} , A1, Z)) :-
-
not o_c_holdsAt2( { B ∉ [light_on]} , { C│ C ≤ 0} , A1, B1) :-
-
not o__chk11( { B ∉ [light_on]} , { D│ D>0} ) :-
-
not -holdsAt( { B ∉ [light_on]} , { D│ D>0} ) :-
-
not o_c_holdsAt1( { B ∉ [light_on]} , { D│ D>0} ) :-
-
0.<. { D│ D>0} ,
-
not initiallyN( { B ∉ [light_on]} ).
-
not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} ) :-
-
forall( C1,forall( D1,not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , C1, D1))) :-
-
forall( D1,not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , { E1│ E1>0} , D1)) :-
-
not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , { E1│ E1>0} , F1) :-
-
{ E1│ E1>0} .>=. { D│ D>0} .
-
forall( D1,not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , { F│ F ≤ 0} , D1)) :-
-
not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , { F│ F ≤ 0} , { E ∉ [turn_off]} ) :-
-
{ F│ F ≤ 0} .<. { D│ D>0} ,
-
not terminates( { E ∉ [turn_off]} , { B ∉ [light_on]} , { F│ F ≤ 0} ) :-
-
not o_terminates1( { E ∉ [turn_off]} , { B ∉ [light_on]} , { F│ F ≤ 0} ) :-
-
{ E ∉ [turn_off]} \=turn_off.
-
not o_c_holdsAt2( { B ∉ [light_on]} , { D│ D>0} , { F│ F ≤ 0} ,turn_off) :-
-
{ F│ F ≤ 0} .<. { D│ D>0} ,
-
not terminates(turn_off, { B ∉ [light_on]} , { F│ F ≤ 0} ) :-
-
not o_terminates1(turn_off, { B ∉ [light_on]} , { F│ F ≤ 0} ) :-
-
turn_off=turn_off,
-
{ B ∉ [light_on]} \=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│ H>0} ,
-
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) :-
-
{ M1│ M1>0} .>=. { H│ H>0} .
-
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 ∉ [turn_off]} ) :-
-
{ J│ J ≤ 0} .<. { H│ H>0} ,
-
not terminates( { I ∉ [turn_off]} ,light_on, { J│ J ≤ 0} ) :-
-
not o_terminates1( { I ∉ [turn_off]} ,light_on, { J│ J ≤ 0} ) :-
-
{ I ∉ [turn_off]} \=turn_off.
-
not o_c_holdsAt2(light_on, { H│ H>0} , { J│ J ≤ 0} ,turn_off) :-
-
{ J│ J ≤ 0} .<. { H│ H>0} ,
-
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│ J ≤ 0} \=4.
-
not o_happens3(turn_off, { J│ J ≤ 0} ) :-