Grounder incorrectly simplifies definitions.

[Ruben Lapauw]

http://dtai.cs.kuleuven.be/krr/idp-ide/?src=1b62f4dd5edecd305b00a891bd307537

The theory has Reachable always true for all pairs of nodes in a way that the grounder cannot simplify depending on T being always true in the grounder.

The first theory has T always true in a way the grounder cannot determine. The grounding is correct and this is unsat.

The second theory has T always true in the structure. The grounder simplifies until Reachable is propagated with lifted propagation. Then the definition of Reachable is simplified to it's completion which misses loops.

The verbosity allows to compare the groundings of both.