let check_contradictory (context: context) (literal: literal) : element option = let index = context.index#find (Term.request_negated_literal ~insert_db:false literal) in index#find_unifiable ~p_preserving:true literal.Term.atom