let unify_literals ~(recompute:bool) ?(p_preserving: bool = false)
  (literal1: literal) (offset1: int) (literal2: literal) (offset2: int) : subst =

  if literal1.Term.sign == literal2.Term.sign then
    unify_terms ~recompute:recompute ~p_preserving:p_preserving
      literal1.Term.atom offset1 literal2.Term.atom offset2
  else
    raise (UNIFICATION_FAIL )