Input A is int
Internal B is int 
Internal C is int 
Internal D is int 
Internal E is int
Output F is int 
Input G is int
Internal H is int 
Internal I is int  
Output J is int
Output K is bool

req1: Globally, it is always the case that if "A == 1" holds then "B == 2" holds after at most 10 time units.
req7: Globally, it is always the case that if "G == 2" holds then "H == 2" holds after at most 12 time units.
req2: Globally, it is always the case that if "B == 2 && H == 2" holds then "C == 2" holds after at most 12 time units.

req3: Globally, it is always the case that if "C == 2" holds then "D == 2" holds after at most 12 time units.
req4: Globally, it is always the case that if "D == 2" holds then "E == 2" holds after at most 12 time units.
req5: Globally, it is always the case that if "E == 2" holds then "F == 2" holds after at most 12 time units.
req6: Globally, it is always the case that if "F == 2" holds then "G == 2" holds after at most 12 time units.

req8: Globally, it is always the case that if "H == 2 && F == 2" holds then "I == 2" holds after at most 12 time units.
req9: Globally, it is always the case that if "I == 2" holds then "J == 2 && K" holds after at most 12 time units.