\begin{verbatim}

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

const length=5.

time(1..length).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%Intitially %%%%%%%%%%%%%%%%%%%%%

 initially(neg(p(f))).
 initially(p(g)).
 initially(neg(p(h))).

%%%%%%%%%%%%%%%%%%%A simple domain%%%%%%%%%%%%%%%%%%%%%%%%%%%

 action(a).
 action(b).
 action(c).
 action(d).
 action(e1).
 action(e2).
 action(null).

 set(fgh).
 in(f,fgh).
 in(g,fgh).
 in(h,fgh).

 fluent(p(f)).
 fluent(p(g)).
 fluent(p(h)).

 causes(a, p(f), set1).
 set(set1).
 in(neg(p(g)), set1).


 causes(b, neg(p(g)), nil).
 set(nil).

 causes(c, neg(p(f)), nil).

 causes(d, p(f), nil).
 causes(d, p(g), nil).
 causes(d, p(h), nil).

 causes(e1, p(g), nil).
 causes(e2, p(h), nil).

 exec(a, nil).
 exec(b, nil).
 exec(c, nil).
 exec(d, nil).
 exec(e1, nil).
 exec(e2, nil).
 exec(null, nil).

%%%% A simple Golog program -- test with 4 options for rest2%%%%%%%

 procedure(test).
 first(test, b).
 last(test, rest1).

 procedure(rest1).
 first(rest1, choice).
 last(rest1, rest2).

 choice_st(choice).
 in(a, choice).
 in(c, choice).
 in(d, choice).

 procedure(rest2).

% first(rest2, p(f)).
% first(rest2, rest3).
% first(rest2, rest4).
  first(rest2, rest5).

 last(rest2, null).

 forall(rest3, p(X)) :- in(X,fgh).
% rest3 is equivalent to \forall [X : fgh]. p(X)

 exists(rest4, p(X)) :- in(X,fgh).
% rest4 is equivalent to \exists [X : fgh]. p(X)

 forall(rest5, neg(p(X))) :- in(X, fgh).
% rest5 is equivalent to \forall [X : fgh]. \neg p(X)


%%%%The procedure test1 -- needs length >= 5%%%%%%%%%%

procedure(test1).
first(test1, while1).
last(test1, null).

while(while1, rest6, ch2).

exists(rest6, neg(p(X))) :- in(X, fgh).
% rest6 is equivalent to \exists [X : fgh]. ~p(X)

choice_st(ch2).
in(a, ch2).
in(b, ch2).
in(c, ch2).
in(e1, ch2).
in(e2, ch2).

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


goal(T)     :-
           time(T),
           unfold(test1, 1, T).

goal(T+1)   :-
        time(T),
        T < length,
        goal(T).

exists_plan :-
        goal(length).

:- not exists_plan.


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

literal(G)  :-
    fluent(G).

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

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

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

def_literal(G)  :-
    def_fluent(G).

def_literal(neg(G)) :-
    def_fluent(G).

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

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

 leq(T,T):- time(T).
 leq(Tb,Te):- time(Tb), time(Te), Tb < Te.

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

not_holds_set(S, T)   :-
    set(S),
    time(T),
    in(L,S),
    not holds(L,T).

holds_set(S, T)        :-
    set(S),
    time(T),
    not not_holds_set(S,T).

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

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

holds(F, T)   :-
    literal(F),
    literal(G),
    time(T),
    T < length,
    holds(G, T),
    static_causes(G,F).

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

executable(A,T)             :-
        action(A),
        time(T),
        set(S),
        T < length,
        exec(A,S),
        holds_set(S,T).


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

possible(A,T)   :-
    action(A),
    time(T),
    executable(A,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).

%%%%%%%%%%%%%%%  Global truths and constraints %%%%%%%%%%%%

holds(true, T):- time(T).

:- time(T), occurs(null,T).

%%%%%%%%%%%%%%%%%%%%   Unfolding    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 unfold(P,Tb,Te):-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    time(Te1),
    leq(Tb, Te1),
    leq(Te1,Te),
    procedure(P),
    first(P,P1),
    unfold(P1,Tb,Te1),
    last(P,P2),
    unfold(P2,Te1,Te).

 unfold(A,Tb,Tb+1):-
    time(Tb),
    action(A),
    neq(A, null),
    occurs(A,Tb).

 unfold(A,Tb,Tb):-
    time(Tb),
    action(A),
    A = null.

 unfold(N,Tb,Te):-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    choice_st(N),
    in(P1,N),
    unfold(P1,Tb,Te).

 unfold(F,Tb,Tb):-
    time(Tb),
    formula(F),
    holds_formula(F,Tb).

 unfold(F,Tb,Tb):-
    time(Tb),
    literal(F),
    holds(F,Tb).

 unfold(I,Tb,Te):-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    if(I,F,P1,P2),
    holds_formula(F,Tb),
    unfold(P1,Tb,Te).

 unfold(I,Tb,Te):-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    if(I,F,P1,P2),
    not holds_formula(F,Tb),
    unfold(P2,Tb,Te).

 unfold(W,Tb,Te):-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    while(W,F,P),
    holds_formula(F,Tb),
    time(Te1),
    leq(Tb, Te1),
    leq(Te1,Te),
    unfold(P,Tb,Te1),
    unfold(W,Te1,Te).

 unfold(W,Tb,Tb):-
    time(Tb),
    while(W,F,P),
    not holds_formula(F,Tb).

 unfold(S,Tb, Te)   :-
    time(Tb),
    time(Te),
    leq(Tb,Te),
    choice_arg(S,F,P),
    holds(F,Tb),
    unfold(P, Tb, Te).

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

 holds_formula(F,T) :-
    time(T),
    disj(F),
    in(F1, F),
    holds_formula(F1,T).

 not_holds_conj_formula(F,T) :-
    time(T),
    conj(F),
    in(F1, F),
    not holds_formula(F1, T).

 holds_formula(F,T) :-
    time(T),
    conj(F),
    not not_holds_conj_formula(F).

 holds_formula(F,T) :-
    time(T),
    negation(F, F1),
    not holds_formula(F1,T).

 holds_formula(F,T) :-
    time(T),
    literal(F),
    holds(F,T).

 holds_formula(F, T) :-
    time(T),
    exists(F, F1),
    holds_formula(F1, T).

 not_holds_forall_formula(F, T) :-
    time(T),
    forall(F, F1),
    not holds_formula(F1, T).

 holds_formula(F, T) :-
    time(T),
    forall(F, F1),
    not not_holds_forall_formula(F, T).


forumla(F)  :-  disj(F).
forumla(F)  :-  conj(F).
formula(F)  :-  literal(F).
formula(F)  :-  negation(F,F1).
formula(F1) :-  negation(F,F1).
formula(F)  :-  exists(F, F1).
formula(F1) :-  exists(F, F1).
formula(F)  :-  forall(F, F1).
formula(F1) :-  forall(F, F1).

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

 hide time(T).
 hide action(A).
 hide causes(A,F,L).
 hide initially(F).
 hide contrary(F,G).
 hide fluent(F).
 hide literal(L).
 hide not_occurs(A,T).
 hide possible(A,T).
 hide exists_plan.
 hide finally(X).
 hide goal(T).
 hide not_goal(T).
 hide static_causes(X,Y).
 hide def_fluent(X).
 hide def_literal(X).

 hide unfold(P,T1,T2).
 hide first(P,P1).
 hide last(P,P2).
 hide procedure(P).
 hide choice_st(P).
 hide if(I,P,P1,P2).
 hide while(W,F,P).
 hide holds_formula(C,T).
 hide not_holds_formula(C, T).
 hide formula(C).

 hide set(S).
 hide in(F,S).
 hide holds_set(S, T).
 hide not_holds_set(S,T).
 hide leq(T1,T2).
 hide executable(A, T).
 hide holds(F, T).
 hide exec(A,L).
 hide choice_arg(X,Y,Z).

 hide conj(F).
 hide disj(F).
 hide negation(F,G).
 hide exists(F,F1).
 hide forall(F,F1).
 hide not_holds_conj_formula(C, T).
 hide not_holds_forall_formula(C, T).

\end{verbatim}