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