RBOX:
TBOX:
ABOX:
	a : FORALL(r*, p)
	r(a,b)
	b : EXISTS(({a}? + r)*, !p)
END