%%%%%%%%%%%%Begin auxiliary predicates

time(1..length).
path(1..level).
literal(F):- fluent(F).
literal(neg(F)):- fluent(F).
contrary(F, neg(F)):- fluent(F).
contrary(neg(F), F):- fluent(F).

new_branch(L, L1):-
    path(L), path(L1), L < L1.
h(F, T+1, P1):-
  	path(P), time(T), path(P1), P <= P1, sense(F),
	branch(F, T, P, P1).

used(T+1, P1):- 
  	path(P), time(T), path(P1), P <= P1, sense(F),
	branch(F, T, P, P1).

:- path(L), time(T), fluent(F), action(A),
   determines(A, F), occ(A, T, L),
   known(F, T, L).

h(G, T+1, L1):-
    time(T), path(L1), path(L), 
    literal(G),
    sense(F), L <= L1,
    branch(F, T, L, L1),
    h(G, T, L).

unknown(F, T, L):-
    path(L), time(T), fluent(F),
    not known(F, T, L).

known(F, T, L):-
    path(L), time(T), fluent(F),
    h(F, T, L).

known(F, T, L):-
    path(L), time(T), fluent(F), contrary(F, G),
    h(G, T, L).

used(1, 1).
used(T+1, L):- time(T), path(L), used(T, L).

1{occ(A, T, P) : action(A)}1:-
    time(T),
    path(P),
    used(T, P),
    not goal(T, P).

:-  time(T),  path(P),
     used(T, P),  action(A),
     occ(A,T,P), not possible(A, T, P).
%%%%% End auxiliary section

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%    Domain Description               %%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% Fluents %%%%

fluent(in(1)).
fluent(in(2)).
fluent(in(3)).
fluent(in(4)).
fluent(in(5)).
fluent(armed).
fluent(clogged).

%%% End of Fluents %%%


% non-inertial literals
noninertial(armed).
noninertial(neg(armed)).



%%% Actions %%%%

action(dunk(1)).
action(dunk(2)).
action(dunk(3)).
action(dunk(4)).
action(dunk(5)).
action(detect_metal(1)).
action(detect_metal(2)).
action(detect_metal(3)).
action(detect_metal(4)).
action(detect_metal(5)).
action(sniff(1)).
action(sniff(2)).
action(sniff(3)).
action(sniff(4)).
action(sniff(5)).
action(xray(1)).
action(xray(2)).
action(xray(3)).
action(xray(4)).
action(xray(5)).
action(listen_for_ticking(1)).
action(listen_for_ticking(2)).
action(listen_for_ticking(3)).
action(listen_for_ticking(4)).
action(listen_for_ticking(5)).

%%% End of Actions %%%


%%% Section: static causal laws %%%%
h(armed, T, P):-  time(T), path(P),
        h(in(1), T, P).
h(armed, T, P):-  time(T), path(P),
        h(in(2), T, P).
h(armed, T, P):-  time(T), path(P),
        h(in(3), T, P).
h(armed, T, P):-  time(T), path(P),
        h(in(4), T, P).
h(armed, T, P):-  time(T), path(P),
        h(in(5), T, P).
h(neg(armed), T, P):-  time(T), path(P),
        h(neg(in(1)), T, P), 
        h(neg(in(2)), T, P), 
        h(neg(in(3)), T, P), 
        h(neg(in(4)), T, P), 
        h(neg(in(5)), T, P).
h(in(1), T, P):-  time(T), path(P),
        h(neg(in(2)), T, P), 
        h(neg(in(3)), T, P), 
        h(neg(in(4)), T, P), 
        h(neg(in(5)), T, P), 
        h(armed, T, P).
h(in(2), T, P):-  time(T), path(P),
        h(neg(in(1)), T, P), 
        h(neg(in(3)), T, P), 
        h(neg(in(4)), T, P), 
        h(neg(in(5)), T, P), 
        h(armed, T, P).
h(in(3), T, P):-  time(T), path(P),
        h(neg(in(1)), T, P), 
        h(neg(in(2)), T, P), 
        h(neg(in(4)), T, P), 
        h(neg(in(5)), T, P), 
        h(armed, T, P).
h(in(4), T, P):-  time(T), path(P),
        h(neg(in(1)), T, P), 
        h(neg(in(2)), T, P), 
        h(neg(in(3)), T, P), 
        h(neg(in(5)), T, P), 
        h(armed, T, P).
h(in(5), T, P):-  time(T), path(P),
        h(neg(in(1)), T, P), 
        h(neg(in(2)), T, P), 
        h(neg(in(3)), T, P), 
        h(neg(in(4)), T, P), 
        h(armed, T, P).
h(neg(in(2)), T, P):-  time(T), path(P),
        h(in(1), T, P).
h(neg(in(3)), T, P):-  time(T), path(P),
        h(in(1), T, P).
h(neg(in(4)), T, P):-  time(T), path(P),
        h(in(1), T, P).
h(neg(in(5)), T, P):-  time(T), path(P),
        h(in(1), T, P).
h(neg(in(1)), T, P):-  time(T), path(P),
        h(in(2), T, P).
h(neg(in(3)), T, P):-  time(T), path(P),
        h(in(2), T, P).
h(neg(in(4)), T, P):-  time(T), path(P),
        h(in(2), T, P).
h(neg(in(5)), T, P):-  time(T), path(P),
        h(in(2), T, P).
h(neg(in(1)), T, P):-  time(T), path(P),
        h(in(3), T, P).
h(neg(in(2)), T, P):-  time(T), path(P),
        h(in(3), T, P).
h(neg(in(4)), T, P):-  time(T), path(P),
        h(in(3), T, P).
h(neg(in(5)), T, P):-  time(T), path(P),
        h(in(3), T, P).
h(neg(in(1)), T, P):-  time(T), path(P),
        h(in(4), T, P).
h(neg(in(2)), T, P):-  time(T), path(P),
        h(in(4), T, P).
h(neg(in(3)), T, P):-  time(T), path(P),
        h(in(4), T, P).
h(neg(in(5)), T, P):-  time(T), path(P),
        h(in(4), T, P).
h(neg(in(1)), T, P):-  time(T), path(P),
        h(in(5), T, P).
h(neg(in(2)), T, P):-  time(T), path(P),
        h(in(5), T, P).
h(neg(in(3)), T, P):-  time(T), path(P),
        h(in(5), T, P).
h(neg(in(4)), T, P):-  time(T), path(P),
        h(in(5), T, P).

%%% End section: static causal laws %%%%

%%% Section: dynamic causal laws %%%%
h(neg(in(1)), T+1, P):- time(T), path(P), 
        possible(dunk(1), T, P),
        occ(dunk(1),T,P), 
        h(in(1), T, P).
h(neg(in(2)), T+1, P):- time(T), path(P), 
        possible(dunk(2), T, P),
        occ(dunk(2),T,P), 
        h(in(2), T, P).
h(neg(in(3)), T+1, P):- time(T), path(P), 
        possible(dunk(3), T, P),
        occ(dunk(3),T,P), 
        h(in(3), T, P).
h(neg(in(4)), T+1, P):- time(T), path(P), 
        possible(dunk(4), T, P),
        occ(dunk(4),T,P), 
        h(in(4), T, P).
h(neg(in(5)), T+1, P):- time(T), path(P), 
        possible(dunk(5), T, P),
        occ(dunk(5),T,P), 
        h(in(5), T, P).
h(clogged, T+1, P):- time(T), path(P), 
        possible(dunk(1), T, P),
        occ(dunk(1),T,P), 
        h(neg(in(1)), T, P).
h(clogged, T+1, P):- time(T), path(P), 
        possible(dunk(2), T, P),
        occ(dunk(2),T,P), 
        h(neg(in(2)), T, P).
h(clogged, T+1, P):- time(T), path(P), 
        possible(dunk(3), T, P),
        occ(dunk(3),T,P), 
        h(neg(in(3)), T, P).
h(clogged, T+1, P):- time(T), path(P), 
        possible(dunk(4), T, P),
        occ(dunk(4),T,P), 
        h(neg(in(4)), T, P).
h(clogged, T+1, P):- time(T), path(P), 
        possible(dunk(5), T, P),
        occ(dunk(5),T,P), 
        h(neg(in(5)), T, P).

%%% End section: dynamic causal laws %%%%


%%% Section: Executability Conditions %%

possible(dunk(1), T, P):- time(T),path(P), 
        h(neg(clogged), T, P).
possible(dunk(2), T, P):- time(T),path(P), 
        h(neg(clogged), T, P).
possible(dunk(3), T, P):- time(T),path(P), 
        h(neg(clogged), T, P).
possible(dunk(4), T, P):- time(T),path(P), 
        h(neg(clogged), T, P).
possible(dunk(5), T, P):- time(T),path(P), 
        h(neg(clogged), T, P).
possible(detect_metal(1), T, P):- time(T),path(P).
possible(detect_metal(2), T, P):- time(T),path(P).
possible(detect_metal(3), T, P):- time(T),path(P).
possible(detect_metal(4), T, P):- time(T),path(P).
possible(detect_metal(5), T, P):- time(T),path(P).
possible(sniff(1), T, P):- time(T),path(P).
possible(sniff(2), T, P):- time(T),path(P).
possible(sniff(3), T, P):- time(T),path(P).
possible(sniff(4), T, P):- time(T),path(P).
possible(sniff(5), T, P):- time(T),path(P).
possible(xray(1), T, P):- time(T),path(P).
possible(xray(2), T, P):- time(T),path(P).
possible(xray(3), T, P):- time(T),path(P).
possible(xray(4), T, P):- time(T),path(P).
possible(xray(5), T, P):- time(T),path(P).
possible(listen_for_ticking(1), T, P):- time(T),path(P).
possible(listen_for_ticking(2), T, P):- time(T),path(P).
possible(listen_for_ticking(3), T, P):- time(T),path(P).
possible(listen_for_ticking(4), T, P):- time(T),path(P).
possible(listen_for_ticking(5), T, P):- time(T),path(P).

%%% End of section: Executability Conditions %%%%


%%% Section: Abnormality of fluent %%

possibly_h(F, T, P):-
              literal(F), literal(G),
              contrary(F, G),
              time(T), path(P),
              not h(G, T, P).



ab(in(1), T, P):- time(T),path(P),
          occ(dunk(1), T, P), 
          possibly_h(in(1), T, P).

ab(in(2), T, P):- time(T),path(P),
          occ(dunk(2), T, P), 
          possibly_h(in(2), T, P).

ab(in(3), T, P):- time(T),path(P),
          occ(dunk(3), T, P), 
          possibly_h(in(3), T, P).

ab(in(4), T, P):- time(T),path(P),
          occ(dunk(4), T, P), 
          possibly_h(in(4), T, P).

ab(in(5), T, P):- time(T),path(P),
          occ(dunk(5), T, P), 
          possibly_h(in(5), T, P).

ab(neg(clogged), T, P):- time(T),path(P),
          occ(dunk(1), T, P), 
          possibly_h(neg(in(1)), T, P).

ab(neg(clogged), T, P):- time(T),path(P),
          occ(dunk(2), T, P), 
          possibly_h(neg(in(2)), T, P).

ab(neg(clogged), T, P):- time(T),path(P),
          occ(dunk(3), T, P), 
          possibly_h(neg(in(3)), T, P).

ab(neg(clogged), T, P):- time(T),path(P),
          occ(dunk(4), T, P), 
          possibly_h(neg(in(4)), T, P).

ab(neg(clogged), T, P):- time(T),path(P),
          occ(dunk(5), T, P), 
          possibly_h(neg(in(5)), T, P).

h(F, T+1, P):-
              literal(F), 
              time(T), path(P),
              h(F, T, P),
              not noninertial(F),
              literal(G), contrary(F, G),
              not h(G, T+1, P),
              not ab(F, T, P).

%%% End Section: Abnormality of fluent %%



%%% Section: Sensing Actions %%
sense(in(1)).
sense(neg(in(1))).
branch(in(1), T, P, P):-
        time(T), path(P), possible(detect_metal(1), T, P), occ(detect_metal(1), T, P).

1{branch(neg(in(1)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(detect_metal(1), T, P), occ(detect_metal(1), T, P).
sense(in(2)).
sense(neg(in(2))).
branch(in(2), T, P, P):-
        time(T), path(P), possible(detect_metal(2), T, P), occ(detect_metal(2), T, P).

1{branch(neg(in(2)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(detect_metal(2), T, P), occ(detect_metal(2), T, P).
sense(in(3)).
sense(neg(in(3))).
branch(in(3), T, P, P):-
        time(T), path(P), possible(detect_metal(3), T, P), occ(detect_metal(3), T, P).

1{branch(neg(in(3)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(detect_metal(3), T, P), occ(detect_metal(3), T, P).
sense(in(4)).
sense(neg(in(4))).
branch(in(4), T, P, P):-
        time(T), path(P), possible(detect_metal(4), T, P), occ(detect_metal(4), T, P).

1{branch(neg(in(4)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(detect_metal(4), T, P), occ(detect_metal(4), T, P).
sense(in(5)).
sense(neg(in(5))).
branch(in(5), T, P, P):-
        time(T), path(P), possible(detect_metal(5), T, P), occ(detect_metal(5), T, P).

1{branch(neg(in(5)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(detect_metal(5), T, P), occ(detect_metal(5), T, P).
sense(in(1)).
sense(neg(in(1))).
branch(in(1), T, P, P):-
        time(T), path(P), possible(sniff(1), T, P), occ(sniff(1), T, P).

1{branch(neg(in(1)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(sniff(1), T, P), occ(sniff(1), T, P).
sense(in(2)).
sense(neg(in(2))).
branch(in(2), T, P, P):-
        time(T), path(P), possible(sniff(2), T, P), occ(sniff(2), T, P).

1{branch(neg(in(2)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(sniff(2), T, P), occ(sniff(2), T, P).
sense(in(3)).
sense(neg(in(3))).
branch(in(3), T, P, P):-
        time(T), path(P), possible(sniff(3), T, P), occ(sniff(3), T, P).

1{branch(neg(in(3)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(sniff(3), T, P), occ(sniff(3), T, P).
sense(in(4)).
sense(neg(in(4))).
branch(in(4), T, P, P):-
        time(T), path(P), possible(sniff(4), T, P), occ(sniff(4), T, P).

1{branch(neg(in(4)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(sniff(4), T, P), occ(sniff(4), T, P).
sense(in(5)).
sense(neg(in(5))).
branch(in(5), T, P, P):-
        time(T), path(P), possible(sniff(5), T, P), occ(sniff(5), T, P).

1{branch(neg(in(5)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(sniff(5), T, P), occ(sniff(5), T, P).
sense(in(1)).
sense(neg(in(1))).
branch(in(1), T, P, P):-
        time(T), path(P), possible(xray(1), T, P), occ(xray(1), T, P).

1{branch(neg(in(1)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(xray(1), T, P), occ(xray(1), T, P).
sense(in(2)).
sense(neg(in(2))).
branch(in(2), T, P, P):-
        time(T), path(P), possible(xray(2), T, P), occ(xray(2), T, P).

1{branch(neg(in(2)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(xray(2), T, P), occ(xray(2), T, P).
sense(in(3)).
sense(neg(in(3))).
branch(in(3), T, P, P):-
        time(T), path(P), possible(xray(3), T, P), occ(xray(3), T, P).

1{branch(neg(in(3)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(xray(3), T, P), occ(xray(3), T, P).
sense(in(4)).
sense(neg(in(4))).
branch(in(4), T, P, P):-
        time(T), path(P), possible(xray(4), T, P), occ(xray(4), T, P).

1{branch(neg(in(4)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(xray(4), T, P), occ(xray(4), T, P).
sense(in(5)).
sense(neg(in(5))).
branch(in(5), T, P, P):-
        time(T), path(P), possible(xray(5), T, P), occ(xray(5), T, P).

1{branch(neg(in(5)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(xray(5), T, P), occ(xray(5), T, P).
sense(in(1)).
sense(neg(in(1))).
branch(in(1), T, P, P):-
        time(T), path(P), possible(listen_for_ticking(1), T, P), occ(listen_for_ticking(1), T, P).

1{branch(neg(in(1)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(listen_for_ticking(1), T, P), occ(listen_for_ticking(1), T, P).
sense(in(2)).
sense(neg(in(2))).
branch(in(2), T, P, P):-
        time(T), path(P), possible(listen_for_ticking(2), T, P), occ(listen_for_ticking(2), T, P).

1{branch(neg(in(2)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(listen_for_ticking(2), T, P), occ(listen_for_ticking(2), T, P).
sense(in(3)).
sense(neg(in(3))).
branch(in(3), T, P, P):-
        time(T), path(P), possible(listen_for_ticking(3), T, P), occ(listen_for_ticking(3), T, P).

1{branch(neg(in(3)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(listen_for_ticking(3), T, P), occ(listen_for_ticking(3), T, P).
sense(in(4)).
sense(neg(in(4))).
branch(in(4), T, P, P):-
        time(T), path(P), possible(listen_for_ticking(4), T, P), occ(listen_for_ticking(4), T, P).

1{branch(neg(in(4)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(listen_for_ticking(4), T, P), occ(listen_for_ticking(4), T, P).
sense(in(5)).
sense(neg(in(5))).
branch(in(5), T, P, P):-
        time(T), path(P), possible(listen_for_ticking(5), T, P), occ(listen_for_ticking(5), T, P).

1{branch(neg(in(5)), T, P, P1):new_branch(P, P1)}1:-
        time(T), path(P), possible(listen_for_ticking(5), T, P), occ(listen_for_ticking(5), T, P).

:- time(T), path(P1), path(P2),
    path(L1), P1 <= P2, L1 <= P2,
    sense(F), sense(G), neq(F,G),
    domain(F,V), domain(G,V1),
    branch(F,V,T,P1,P2),
    branch(G,V,T,L1,P2).

:- time(T), T > 1,
    path(P1), path(P2), P1 < P2,
    sense(F), domain(F,V),
    branch(F,V,T,P1,P2), used(T,P2).



determines(detect_metal(1), in(1)).
determines(detect_metal(2), in(2)).
determines(detect_metal(3), in(3)).
determines(detect_metal(4), in(4)).
determines(detect_metal(5), in(5)).
determines(detect_metal(1), neg(in(1))).
determines(detect_metal(2), neg(in(2))).
determines(detect_metal(3), neg(in(3))).
determines(detect_metal(4), neg(in(4))).
determines(detect_metal(5), neg(in(5))).
determines(sniff(1), in(1)).
determines(sniff(2), in(2)).
determines(sniff(3), in(3)).
determines(sniff(4), in(4)).
determines(sniff(5), in(5)).
determines(sniff(1), neg(in(1))).
determines(sniff(2), neg(in(2))).
determines(sniff(3), neg(in(3))).
determines(sniff(4), neg(in(4))).
determines(sniff(5), neg(in(5))).
determines(xray(1), in(1)).
determines(xray(2), in(2)).
determines(xray(3), in(3)).
determines(xray(4), in(4)).
determines(xray(5), in(5)).
determines(xray(1), neg(in(1))).
determines(xray(2), neg(in(2))).
determines(xray(3), neg(in(3))).
determines(xray(4), neg(in(4))).
determines(xray(5), neg(in(5))).
determines(listen_for_ticking(1), in(1)).
determines(listen_for_ticking(2), in(2)).
determines(listen_for_ticking(3), in(3)).
determines(listen_for_ticking(4), in(4)).
determines(listen_for_ticking(5), in(5)).
determines(listen_for_ticking(1), neg(in(1))).
determines(listen_for_ticking(2), neg(in(2))).
determines(listen_for_ticking(3), neg(in(3))).
determines(listen_for_ticking(4), neg(in(4))).
determines(listen_for_ticking(5), neg(in(5))).

%%% End of section: Sensing Actions %%%%


%%% Section: Initial %%

h(armed, 1, 1).
h(neg(clogged), 1, 1).

%%% End of section: Initial %%%%


%%% Section: Goal %%

goal(T, P):-
         time(T), path(P),
         h(neg(armed), T, P),
         h(neg(clogged), T, P).
goal(T+1, P):-
    time(T), path(P),
    goal(T, P).

ggoal(P):- path(P), time(T), used(T, P), goal(length, P).
:- path(P), used(length, P), not ggoal(P).

%%% End of section: Goal %%%%

:-  time(T),  path(P),
    literal (P),  literal(G),
    contrary(F,G), h(F, T, P), h(G, T, P).

hide time(T).
hide path(L).
hide action(A).
hide determines(A,F).
hide contrary(F,G).
hide fluent(F).
hide literal(L).
hide unknown(F, T, L).
hide known(F, T, L).
hide used(T, L).
hide sense(F).
%hide ggoal(L).
hide goal(T,L).
hide new_branch(L, L1).
hide executable(A,S).
hide possible(A, T, L).
hide ab(F, T, L).
hide h(F, T, L).
hide noninertial(F).
hide possibly_h(F, T, L).