In reply to peter:
Hi peter,
The waveform is generated by the formal tool as a counter example for an assertion that I have not shown. But the reason why I am mystified is because the input signals seem to be violating the constraint that I coded in my original question.