%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Verification if guessed set in(X) is in res_gr(F)
% input: AF F=(A,R)
% guess all conflict free sets U of F
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
in(X) :- not out(X), arg(X).
out(X) :- not in(X), arg(X).
:- in(X), in(Y), att(X,Y).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% HELPERS --- as usual
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
lt(X,Y) :- arg(X),arg(Y), X t is stable in mr
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
defeated(N,X) :- mr(N,X), mr(N,Y), t(N,Y), defeatN(N,Y,X).
not_defeated(N,X) :- mr(N,X), not defeated(N,X).
:- not t(N,X), not_defeated(N,X), mr(N,X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% (T \cap W)+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
tw_plus(N,Y) :- t(N,X), mr(N,X), defeatN(N,X,Y).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% next iteration
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
arg_set(M,X) :- cut(N,X), not mr(N,X), not tw_plus(N,X), succ(N,M), not true(N).
inU(M,X) :- t(N,X), not mr(N,X), succ(N,M), not true(N).