// #TestSpec: rt-inconsistent:req2+req1; vacuous:; inconsistent:; results: 4
Input a is bool

req1: Globally, it is always the case that once "a" becomes satisfied, it holds for less than "5" time units.
req2: Globally, it is always the case that once "a" becomes satisfied, it holds for at least "15" time units.

// silently enforces !a
// we want value completeness to detect this issue