let literal_equal (literal1: literal) (literal2: literal) : bool =
  literal1 == literal2
  ||
  begin
    not (literal1.literal_in_db && literal2.literal_in_db)
    &&
    (literal1.sign == literal2.sign)
    &&
    (term_equal literal1.atom literal2.atom)
  end