%* ordering *%
lt(X,Y) :- arg(X), arg(Y), X < Y.
nsucc(X,Z) :- lt(X,Y), lt(Y,Z).
succ(X,Y) :- lt(X,Y), not nsucc(X,Y).
ninf(Y) :- lt(X,Y).
inf(X) :- arg(X), not ninf(X).
nsup(X) :- lt(X,Y).
sup(X) :- arg(X), not nsup(X).
%* guess a resolution *%
res(X,Y) :- defeat(X,Y), defeat(Y,X), not res(Y,X), X!=Y.
res(X,Y) :- defeat(X,Y), not defeat(Y,X).
res(X,X) :- defeat(X,X).
%* defended upto like in grounded case*%
defended_upto(X,Y) :- inf(Y), arg(X), not res(Y,X).
defended_upto(X,Y) :- inf(Y), in(Z), res(Z,Y),res(Y,X).
defended_upto(X,Y) :- succ(Z,Y), defended_upto(X,Z), not res(Y,X).
defended_upto(X,Y) :- succ(Z,Y), defended_upto(X,Z),in(V), res(V,Y), res(Y,X).
defended(X) :- sup(Y), defended_upto(X,Y).
in(X) :- defended(X).
%* minimize s.t. no proper subset is also a answer set *%
#minimize [ in(X) ].