RBOX:
	INCLUSION(R-, S)
	TRANSITIVE(S)
TBOX:
	INCLUSION(A, !(B || C || D))
	INCLUSION(B, !(A || C || D))
	INCLUSION(C, !(A || B || D))
	INCLUSION(D, !(A || B || C))

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

	a : EXISTS(R, EXISTS(R, FORALL(S, E))) 
END