gather(A,X,X1) :- atomic(A),!,
	X = [A|X1].
gather(F,X,X1) :- functor(F,_,N),!,
	gather_args(0,N,F,X,X1).
gather_args(N,N1,_,X,X) :- N =:= N1,!.
gather_args(N,N1,F,X,X1) :- 
	N0 is N+1,arg(N0,F,A), 
	gather(A,X,X0),gather_args(N0,N1,F,X0,X1).


itl(A,C,T,X,X) :- atomic(A),!,
	itl_variable(C,A,T).
itl_variable(C,A,T) :-
	true(C,A,C,C1),!,

	itl_false(C,A,F,X0,X1).
itl_true(C,A,T,X,X) :-true.
itl_true(_,_,X,X) :-true.

true([],A,C,[A|C]):-!.
true([A|_],A,C,C):-!.
true([not(A)|_],A,C,C):-!,fail.
true([_|T],A,C,C1):-!,true(T,A,C,C1).

false([],A,C,[A|C]):-!.
false([not(A)|_],A,C,C):-!.
false([A|_],A,C,C):-!,fail.
false([_|T],A,C,C1):-!,false(T,A,C,C1).