Completed implementation of Reprensetation Theorem.

* Fixed: there was confusion with B_k(phi => psi). BLiteral etc. stored
  what was called neg_phi, but it actually was the positive antecedent phi.
  Storing the positive one seems much more intuitive, especially when
  handling simpliciation results TRIVIALLY_[TRUE|FALSE]. Therefore it
  is now just phi, and Belief::Reduce() negates it to perform reasoning
  (because Belief::Reduce() deviates from the paper for performance
  to avoid a huge formula which itself emulates a loop over the setups).

TODO: following improvements:
* Only do reduction for the correct sensing results.
  That would, however, mean to invert the reasoning order (currently it
  is innermost nesting first, it should be outermost nesting first),
  which sounds painful.
* Minimization of CNFs is suboptimal: (P ^ Q) v (~P ^ R) should be
  minimized to (~P v Q) ^ (P v R), but we also obtain a clause (Q v R).