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