// #TestSpec: rt-inconsistent:; vacuous:req1; inconsistent:; results:-1
// 2020-01-13: Spec checked by Elli
Input var1 is bool
Input var3 is bool
Input var4 is bool
Input var5 is bool

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

req1: Before "var1" It is always the case that If "var3" holds and is succeeded by "var4", then "var5" previously held