\begin{verbatim}

const length=9.
const no_pts=8.

time(1..length).

location(1..no_pts).

vehicle(v).

initially(edge(1,2)).
initially(edge(2,3)).
initially(edge(3,4)).
initially(edge(4,8)).
initially(edge(8,7)).
initially(edge(7,6)).
initially(edge(6,5)).
initially(edge(5,1)).
initially(edge(2,6)).
initially(edge(7,3)).

initially(at(v,3)).

finally(at(v,2)).

not_goal(T):- time(T),
    literal(X),
    finally(X),
    not holds(X,T).

goal(T) :- time(T),
    not not_goal(T).

exists_plan :-
    goal(length).

:- not exists_plan.


%Defining what are fluents and
%what are actions.

fluent(at(V,X)) :-
    vehicle(V),
    location(X).

fluent(edge(X,Y))   :-
    location(X),
    location(Y).

action(move(V,X,Y)) :-
    vehicle(V),
    location(X),
    location(Y).

%Effects of actions and executability conditions.

impossible_if(move(V,L,LL), neg(at(V,L)))   :-
    vehicle(V),
    location(L),
    location(LL).

impossible_if(move(V,L1,L2), neg(edge(L1,L2)))  :-
    vehicle(V),
    location(L1),
    location(L2).


%executable(move(V,L,LL), T)    :-
%   vehicle(V),
%   location(L),
%   location(LL),
%   time(T),
%   T < length,
%   holds(at(V,L),T),
%   holds(edge(L,LL), T),
%   neq(L,LL).


causes(move(V,L,LL), at(V, LL)) :-
    vehicle(V),
        location(L),
        location(LL).

causes(move(V,L,LL), neg(at(V,L)))  :-
    vehicle(V),
        location(L),
        location(LL).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


literal(G)  :-
    fluent(G).

literal(neg(G)) :-
    fluent(G).

contrary(F, neg(F)) :-
    fluent(F).

contrary(neg(F), F) :-
    fluent(F).

%Defining Execeutability

not_executable(A,T)     :-
    action(A),
    time(T),
    impossible_if(A,B),
    holds(B,T).

executable(A,T)     :-
    action(A),
    time(T),
    not not_executable(A,T).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

holds(F, 1) :-
    literal(F),
    initially(F).

holds(neg(F), 1)    :-
    fluent(F),
    not holds(F,1).

holds(F, T+1)   :-
    literal(F),
    time(T),
    T < length,
    action(A),
    executable(A,T),
    occurs(A,T),
    causes(A,F).

holds(F, T+1)   :-
        literal(F),
    literal(G),
    contrary(F,G),
        time(T),
        T < length,
    holds(F,T),
    not holds(G, T+1).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

possible(A,T)   :-
    action(A),
    executable(A,T),
    time(T),
    not goal(T).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

occurs(A,T) :-
    action(A),
    time(T),
    possible(A,T),
    not not_occurs(A,T).

not_occurs(A,T) :-
    action(A),
    action(AA),
    time(T),
    occurs(AA,T),
    neq(A,AA).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

hide time(T).
hide action(A).
hide causes(A,F).
hide initially(F).
hide contrary(F,G).
hide fluent(F).
hide literal(L).
hide executable(A,T).
hide holds(F,T).
hide not_occurs(A,T).
hide possible(A,T).
hide at(X,Y).
hide exists_plan.
hide finally(X).
hide goal(T).
hide not_goal(T).
hide impossible_if(X,Y).
hide location(L).
hide not_executable(A,T).
hide vehicle(V).

\end{verbatim}