type 'a substitution = (int * 'a foterm) list
-type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
type direction = Left2Right | Right2Left | Nodir