// #TestSpec: rt-inconsistent:; vacuous:; inconsistent:req1, req2; results: 1
Input D is bool

req1: Globally, it is never the case that "D" holds.
req2: Globally, it is always the case that "D" holds.