mintime(T) :- est(Fv1,T), not timeLessThan(T).
timeLessThan(T) :- est(Fv1,T), est(Fv2,T1), T1<T.

maxtime(T) :- let(Fv1,T), not timeGreaterThan(T).
timeGreaterThan(T) :- let(Fv1,T), let(Fv2,T1), T1>T.

times(T) :- mintime(T).
times(T) :- times(T1), T=T1+1, T<=MAX, maxtime(MAX).

time(I,T) | non_time(I,T) :- 
	task(I,D), times(T), 
	est(I,S), S<=T, End=T+D,
	let(I,E), End<=E.

:- task(I,Fv1), not exactlyOneScheduling(I).
exactlyOneScheduling(I) :- time(I,T), not atLeastTwoScheduling(I).
atLeastTwoScheduling(I) :- time(I,T1), time(I,T2), T1 != T2.

:- prec(I1,I2), task(I1,D), time(I1,T1), time(I2,T2), End1 = T1+D, T2 < End1.

:- disj(I1,I2), task(I1,D1), task(I2,D2), time(I1,T1), time(I2,T2), 
   End1 = T1+D1, End2=T2+D2, T1<=T2, T2 < End1.

:- disj(I1,I2), task(I1,D1), task(I2,D2), time(I1,T1), time(I2,T2), 
   End1 = T1+D1, End2=T2+D2, T2<=T1, T1 < End2.