RBOX:
TBOX:
	INCLUSION(E, FORALL(R, FORALL(R, !A || !{a})))
	INCLUSION(E, FORALL(R, FORALL(R, !B || !{a})))
	INCLUSION(E, FORALL(R, FORALL(R, !C || !E)))
	INCLUSION(E, FORALL(R, FORALL(R, !D || !E)))
ABOX:
	a : EXISTS(R, EXISTS(R, {a} && E))
	a : A || B || C || D
END