* Complete rewriting of paramodulation code (thanks to Maxime Denes),
that is abstract over the data type embedded in the fisrt order
theory the procedure is able to handle.
* Complete rewriting of paramodulation code (thanks to Maxime Denes),
that is abstract over the data type embedded in the fisrt order
theory the procedure is able to handle.