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

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