[BUG?] Dynamic Consistency Check (DCC) does not preserve semantics

[jinulee-v]

While experimenting, I have found an unexpected behavior regarding the following code.

a :- b(c(d(X))).
b(c(O)) :- e(O).
e(h).
?- not a.
% Model: {e(h)  b(c(h))   not b(c(X | X \notin {h}))   not a}

While normal execution can find a correct model+proof, running with option --dcc fails to find a valid model in this case.

Is there a recursion depth limit for --dcc, that I can manually modify?

Minimal pairs (success with --dcc)

a :- b(c(d(X))).
b(c(h)). % Induction does not have to continue further
?- not a.

a :- b(d(X)). % Only two layers deep
b(O) :- e(O).
e(h).
?- not a.