Refactored Formula, introduces explicitly objective formulas.

That come's at a price: have some generic base classes for Junction and
Quantifier to avoid duplicate code, and have ObjCopy() and ObjRegress()
variants because unique_ptr has no support for polymorphism (wow).