Added consistency modality G.

The new G or Guarantee modality tells the reasoner that the knowledge
base can be assumed to be consistent, which rules out split terms /
assignment literals when K / M and B operators are evaluated.

To have an effect on conditional only-believing, KB statements like
   KB: B alpha ==> beta
can now be equipped with a G operator
   KB: G B alpha ==> beta
for faster consistency checks during the construction of the system of
spheres.

Also fixed a bug in Formula::Bel::Clone().