Activate simplifications on restarts.
Start rewriting of completion.
FIXME: for some reason the same model is produced several times.
Fix bug with multiple models.
More simplifications on normal rules.
Revise nontight.