/*
*/

Input I1 is bool
Internal H1 is bool
Internal H2 is bool
Output O1 is bool

req1: Globally, it is always the case that if "H1" holds for at least "5" time units, then "H2" holds afterwards for at least "10" time units

req2: Globally, it is always the case that if "I1" holds, then "H1" holds as well
req3: Globally, it is always the case that if "H2" holds, then "O1" holds as well