let unify_literals_ ~(recompute:bool) ?(p_preserving: bool = false)
  (subst: subst) (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
      subst literal1.Term.atom offset1 literal2.Term.atom offset2
  else
    raise (UNIFICATION_FAIL )