if you allow something to be true only if something else is not true, your solution space is no longer monotonic. meaning that a result you thought was part of the solution can later be retracted. if there is a cycle (trivially "a if not a"), then you may not ever arrive at an answer. that might seem simple to detect, but that cycle can exist through an arbitrary number of rules and data dependencies, so in the limit is undecidable.
ideally, as in this solver, you could keep adding terms you could show to be correct from the data and rules at hand until they and all their consequences have been found, and which point you can stop (fixed point). but negation screws up this plan.
there are various restrictions on negation, solver heuristics, and partial conservative proofs of termination that can be applied. but this is where your beautiful simple declarative world starts getting sad and messy.
[edit: I'd like to leave this because I wish I understood the problem with negation earlier, but I just skimmed and missed stratification, Frank thoughtfully explains below]