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