The evaluator of the logic system is complete: if there is a solution, the evaluator will always find it in finite time.
Is it also terminating? So if there is no solution it will tell you so.
The evaluator used in the yesterday's message -- no. It is merely complete; if no solution exists, it may terminate, but it is not obliged to. It depends on the formulation of the problem. We do have a refutationally complete evaluator, which does find a contradiction if one exists. It easily handles the problems like (in Prolog notation) X = 1, repeat, X = 2 and more complex problems. It might work for the de-typechecker, I haven't tried. Alas, it takes _too_ much time at present for problems I really want it to use; those problems, in addition to large depth, have a very large breadth...