true.
:- false.
s :- ap(s).
neg_s :- t, q.
neg_s :- t, r.
neg_s :- q, r.
ap(s) :- ok(s), not neg_s.
ap(t) :- ok(t), not neg_t.
ap(q) :- ok(q), not neg_q.
ap(r) :- ok(r), not neg_r.
ap(X) :- sname(X), apo(X, s), apo(X, t), apo(X, q), apo(X, r).
nhead(s) :- neg_s.
nhead(t) :- neg_t.
nhead(q) :- neg_q.
nhead(r) :- neg_r.
ok(X) :- in(X, Y), ok(Y), not ko(Y).
ok(X) :- name(X), not in(X, m1), not in(X, m2), not in(X, m3), not in(X, m4), not in(X, m5).
ok(X) :- sname(X), oko(X, m1), oko(X, m2), oko(X, m3), oko(X, m4), oko(X, m5).
bl(X) :- ok(X), in(s, X), neg_s.
bl(X) :- ok(X), in(s, X), neg_s.
bl(X) :- ok(X), in(t, X), neg_t.
bl(X) :- ok(X), in(t, X), neg_t.
bl(X) :- ok(X), in(q, X), neg_q.
bl(X) :- ok(X), in(q, X), neg_q.
bl(X) :- ok(X), in(r, X), neg_r.
bl(X) :- ok(X), in(r, X), neg_r.
in(s, m1).
in(t, m2).
in(q, m3).
in(r, m4).
in(q, m5).
in(r, m5).
t :- ap(t).
neg_t :- s, q.
neg_t :- s, r.
neg_t :- q, r.
q :- ap(q).
neg_q :- s, t.
neg_q :- s, r.
neg_q :- t, r.
r :- ap(r).
neg_r :- s, t.
neg_r :- s, q.
neg_r :- t, q.
prec(m1, m2) :- true.
prec(m2, m5) :- true.
neg_prec(Y, X) :- sname(X), sname(Y), prec(X, Y).
prec(X, Z) :- sname(X), sname(Z), sname(Y), prec(X, Y), prec(Y, Z).
sname(Y) :- in(X, Y).
apo(Y, X) :- sname(Y), name(X), not in(X, Y).
apo(X, Y) :- sname(X), name(Y), in(Y, X), ap(Y).
nap(X) :- sname(X), napo(X, s), napo(X, t), napo(X, q), napo(X, r).
napo(Y, X) :- sname(Y), name(X), not in(X, Y).
napo(X, Y) :- sname(X), name(Y), in(Y, X), not nhead(Y).
ko(X) :- bl(X).
oko(X, Y) :- sname(X), sname(Y), not prec(X, Y).
oko(X, Y) :- sname(X), sname(Y), prec(X, Y), ap(Y).
oko(X, Y) :- sname(X), sname(Y), prec(X, Y), bl(Y).
false :- s, neg_s.
false :- in(X, Y), neg_in(X, Y).
false :- t, neg_t.
false :- q, neg_q.
false :- r, neg_r.
false :- name(X), name(Y), prec(X, Y), neg_prec(X, Y).
name(r).
name(q).
name(t).
name(s).