RBOX:
TBOX:
	INCLUSION(A, !(B || C || D))
	INCLUSION(B, !(A || C || D))
	INCLUSION(C, !(A || B || D))
	INCLUSION(D, !(A || B || C))

	INCLUSION(E, LEQ(2000, R, A || B || C || D))
ABOX:
	a : GEQ(1000, R, A || B) 
	a : GEQ(1000, R, A || C) 
	a : GEQ(1000, R, A || D) 
	a : GEQ(1000, R, B || C) 
	a : GEQ(1000, R, B || D) 
	a : GEQ(1000, R, C || D) 

	a : EXISTS(R, EXISTS(R, EXISTS(R, {a} && E))) 
END