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