// #TestSpec: rt-inconsistent:; vacuous:req1; inconsistent:; results:-1
Input var1 is bool
Input var2 is bool
Input var3 is bool
Input var4 is bool
Input var5 is bool
Input var6 is bool

Constraint_assumption1: Globally it is always the case that "!var3" holds
Constraint_assumption2: Globally it is always the case that "var1" holds
Constraint_assumption3: Globally it is always the case that "!var2" holds

req1: After "var1" until "var2" It is always the case that If "var3" holds, then "var4" eventually holds and is succeeded by "var5" where "var6" does not hold between "var4" and "var5"