
:- use_module(library(clpq)).
:- use_module(library(lists)).

abstract(Phi, Preds, ConjSet) :-
	{Phi},
	checkentailed(Preds, 1, [], ConjSet).

checkentailed([Pred|Preds], N, Acc, ConjSet) :-
	N1 is N+1,
	( entailed(Pred) ->
	    checkentailed(Preds, N1, [N|Acc], ConjSet)
	;
	    checkentailed(Preds, N1, Acc, ConjSet)
	).
checkentailed([], _, RevConjSet, ConjSet) :- rev(RevConjSet, ConjSet).















































