true.
:- false.
a :- ap(1).
ap(1) :- ok(1), b, not c.
ap(2) :- ok(2), a, not d.
ap(3) :- ok(3), not y.
ap(X) :- sname(X), apo(X, 1), apo(X, 2), apo(X, 3).
nhead(1) :- neg_a.
nhead(2) :- neg_b.
nhead(3) :- neg_x.
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, m12).
ok(X) :- sname(X), oko(X, m1), oko(X, m2), oko(X, m3), oko(X, m12).
b :- ap(2).
bl(X) :- ok(X), in(1, X), not b, nap(X).
bl(X) :- ok(X), in(1, X), c.
bl(X) :- ok(X), in(1, X), neg_a.
bl(X) :- ok(X), in(2, X), not a, nap(X).
bl(X) :- ok(X), in(2, X), d.
bl(X) :- ok(X), in(2, X), neg_b.
bl(X) :- ok(X), in(3, X), y.
bl(X) :- ok(X), in(3, X), neg_x.
in(1, m1).
in(2, m2).
in(3, m3).
in(1, m12).
in(2, m12).
nap(X) :- sname(X), napo(X, 1), napo(X, 2), napo(X, 3).
x :- ap(3).
prec(m3, m12) :- 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).
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 :- a, neg_a.
false :- b, neg_b.
false :- c, neg_c.
false :- in(X, Y), neg_in(X, Y).
false :- d, neg_d.
false :- x, neg_x.
false :- y, neg_y.
false :- name(X), name(Y), prec(X, Y), neg_prec(X, Y).
name(3).
name(2).
name(1).