// #TestSpec: rt-inconsistent:req1+req2; vacuous:; inconsistent:; results:-1
CONST time_at_least is 30.0
Input var3 is bool
Input var4 is bool
CONST MAX_TIME is 50.0
Input var1 is bool

Constraint_assumption: Globally it is always the case that "!var1" holds

req1: Before "var1" It is always the case that If "var3" holds, then "var4" holds after at most "MAX_TIME" time units for at least "time_at_least" time units
req2: Before "var1" It is always the case that After "var3" holds for at least "MAX_TIME" time units, then "!var4" holds