RBOX:
	INCLUSION(R, S)
TBOX:
	INCLUSION(A, LEQ(01, S, B))
	INCLUSION(A, EXISTS(R, B))
ABOX:
	a : EXISTS(S-, A)
	a : !B
END