************************************************************
    *  IMITATOR 2.9.2-working "Butter Incaberry"               *
    *                                                          *
    *                     Etienne Andre, Ulrich Kuehne et al.  *
    *                                             2009 - 2017  *
    *                       LSV, ENS de Cachan & CNRS, France  *
    *                       LIPN, Universite Paris 13, France  *
    *                                         www.imitator.fr  *
    *                                                          *
    *                   Build: 2363 (2017-06-08 17:40:33 UTC)  *
    *                                       explorder/5c40e39  *
    ************************************************************
    Analysis time: Sat Jun 17, 2017 02:10:21
    
    Model: /media/gia/Data/Example-Models/flipflop-P/flipflop-P.imi
    Mode: EF-synthesis.
    Exploration order: layer-based BFS.
    Considering fixpoint variant with bidirectional inclusion of symbolic zones (instead of equality).
    Merging technique of [AFS13] enabled.
    The cartography will be drawn.
    The result will be written to a file.
    The trace set(s) will be generated in a graphical mode.
    Description of states will be output.
    
    Abstract model built after 0.018 second.
    Memory for abstract model: 1536.972 KiB (i.e., 393465 words)
    
    Starting running algorithm AGsafe…
    
    Computing post^1 from 1 state.
    Computing post^2 from 1 state.
    Computing post^3 from 2 states.
    Computing post^4 from 5 states.
      [AGsafe] Found a new state violating the property.
      2 states merged within 12 states.
    Computing post^5 from 10 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      5 states merged within 16 states.
    Computing post^6 from 11 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      5 states merged within 17 states.
    Computing post^7 from 12 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
      2 states merged within 15 states.
    Computing post^8 from 13 states.
      2 states merged within 15 states.
    Computing post^9 from 13 states.
    Computing post^10 from 6 states.
    
    Fixpoint reached at a depth of 11: 103 states with 125 transitions in the final state space.
    
      [AGsafe] Algorithm completed after 37.341 seconds.
    
    Final constraint such that the system is correct:
     dG1_l >= 0
    & dG3_l >= 0
    & tSetup >= 0
    & dG4_l >= 0
    & tHold > dG1_u
    & tHI > dG2_u
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tLO >= tSetup
    OR
      tHI >= tHold
    & tSetup >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG1_l > dG2_u
    & dG2_l > dG3_u
    & tHI > dG2_u + dG4_u
    & dG1_l > tSetup
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & tHold >= 0
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      tHold >= dG2_l
    & tHold + dG1_l > dG2_u
    & dG2_l >= 0
    & dG1_l >= 0
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG3_l > dG4_u
    & dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG3_l >= 0
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG1_l > dG2_u
    & dG2_l > tHold
    & dG3_u >= dG3_l
    & tHold >= 0
    & dG3_u >= dG2_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      dG1_l >= 0
    & dG2_l > tHold
    & dG3_l > dG4_u
    & tHold > dG1_u
    & tHI > dG3_u + dG4_u
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG2_u >= dG2_l
    & dG4_l >= 0
    & tSetup >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & dG2_l > dG3_u
    & dG3_l >= 0
    & tSetup >= 0
    & tHI > dG3_l
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG2_l > dG1_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & tHold >= dG2_l
    & tHI >= tHold
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & tHI >= tHold
    & dG3_l >= 0
    & tSetup >= 0
    & dG4_u >= dG4_l
    & dG2_l > dG3_u
    & tHold >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG2_u + dG4_u
    & dG2_u >= dG1_l
    & dG1_l > tSetup
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & dG1_l >= 0
    & dG3_l >= 0
    & tHold >= dG2_l
    & tHI > dG3_u + dG4_u
    & dG2_l > dG1_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG1_u >= dG3_l
    & tSetup >= 0
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG4_u >= dG3_l
    & dG3_u >= dG2_l
    OR
      dG4_l >= 0
    & dG2_u >= dG3_l
    & dG2_u >= dG1_l
    & dG3_l >= 0
    & dG2_l > tHold
    & tSetup > dG1_u
    & tHold + dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & tHI >= tHold
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      dG3_l > tHold + dG1_u
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold + dG1_u
    & dG4_u >= dG4_l
    & dG1_l >= 0
    & tSetup >= 0
    & tHold >= 0
    & dG2_u >= dG2_l
    & dG1_u >= tHold
    & dG3_u >= dG3_l
    & tLO >= tSetup
    & dG4_u >= dG3_l
    & dG1_u >= dG1_l
    OR
      tHI > dG2_u
    & dG3_l >= 0
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG4_u >= dG4_l
    & dG2_l >= 0
    & dG1_u >= dG1_l
    & tHold >= dG2_l
    & dG1_l >= 0
    & dG1_u >= tHold
    & dG4_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG3_l >= 0
    & tHold >= dG2_l
    & tSetup >= 0
    & tHold + dG1_l > dG2_u
    & dG4_l >= 0
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG2_u
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & tHI >= tHold
    & dG1_u >= dG1_l
    & dG1_u >= dG2_l
    & dG1_u + dG4_u >= tHI
    & dG2_u + dG4_u >= tHI
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG1_l >= 0
    & dG2_u >= tHI
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & dG3_l > dG4_u
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & tHI >= tHold
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & dG1_u + dG4_u >= tHI
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    & tSetup >= 0
    & tLO >= tSetup
    OR
      tHold >= 0
    & tHI >= tHold
    & dG2_l > dG3_u
    & tHI > dG2_u + dG4_u
    & dG3_l > dG4_u
    & dG1_l > dG2_u
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    & tSetup >= dG1_l
    OR
      tHold >= 0
    & tHI >= tHold
    & tHI > dG2_u + dG4_u
    & tSetup > dG1_u
    & dG1_l > dG2_u
    & dG3_l >= 0
    & dG4_l >= 0
    & dG2_l > dG3_u
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & dG4_u >= dG3_l
    & tLO >= tSetup
    OR
      dG3_l >= 0
    & tHold >= dG2_l
    & dG4_l >= 0
    & dG1_l > dG2_u
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG2_u >= dG2_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & dG4_u >= dG3_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG3_l >= 0
    & dG4_l >= 0
    & tHI >= tHold
    & dG2_u >= dG2_l
    & dG3_u >= dG2_l
    & dG4_u >= dG4_l
    & tHold >= dG2_l
    & dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & tHI > dG2_u + dG4_u
    & tSetup > dG1_u
    & dG3_u >= dG3_l
    & dG1_u >= dG1_l
    & dG2_l >= 0
    & dG4_u >= dG3_l
    & tLO >= tSetup
    OR
      tHI >= tHold
    & tHold >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG2_l > tHold
    & dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG2_u >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG2_u >= dG2_l
    & tHold >= dG2_l
    & dG3_l > dG4_u
    & dG2_l > dG1_u
    & tHI > dG3_u + dG4_u
    & tHI >= tHold
    & dG4_l >= 0
    & tSetup >= 0
    & dG1_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    OR
      tHI > dG2_u
    & dG3_l >= 0
    & tSetup >= 0
    & dG4_l >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG2_l > dG1_u
    & tHI > dG3_u + dG4_u
    & tHold + dG1_l > dG2_u
    & tHI > dG1_u + dG4_u
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG1_u >= tSetup
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & dG1_u >= tHold
    & tLO >= tSetup
    OR
      dG2_l > tHold
    & dG2_u >= dG1_l
    & dG4_l >= 0
    & tHold >= 0
    & dG2_u + dG4_u >= tHI
    & dG4_u >= dG3_l
    & tSetup >= 0
    & dG3_l >= 0
    & tHI > dG3_u + dG4_u
    & dG1_l > tSetup
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG2_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      tHI > dG2_u
    & dG4_l >= 0
    & dG3_l > dG1_u
    & tHold >= dG2_l
    & dG2_l > dG1_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_l >= 0
    & tLO >= tSetup
    & tSetup >= dG1_l
    OR
      tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & dG2_l > dG1_u
    & dG2_u >= dG2_l
    & dG4_l >= 0
    & dG3_l >= 0
    & dG1_l >= 0
    & dG1_u >= dG3_l
    & dG4_u >= dG4_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tHI >= tHold
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & dG2_u >= dG3_l
    & dG2_l >= 0
    & tHI >= tHold
    & dG1_l >= 0
    & dG3_l >= 0
    & tHold + dG1_l > dG2_u
    & tHI + tHold > dG2_l + dG3_l
    & tSetup > dG1_u
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & tHold >= dG2_l
    & dG2_u >= dG1_l
    & dG1_u >= dG1_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      dG2_u >= dG1_l
    & tHI >= tHold
    & dG2_l > dG3_u
    & tHold >= 0
    & dG4_l >= 0
    & dG1_l >= 0
    & dG3_l > dG4_u
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u + dG4_u >= tHI
    & dG1_u >= tHold
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    & tSetup >= dG1_l
    OR
      dG1_l >= 0
    & dG2_l > tHold
    & tSetup >= dG1_l
    & dG2_u >= dG1_l
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG1_u >= tSetup
    & dG1_u + dG4_u >= tHI
    & dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & dG3_l >= 0
    & tHold >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & tHI >= dG2_l + dG3_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG1_l >= 0
    & tSetup > dG1_u
    & dG3_l > dG4_u
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & dG1_u >= dG1_l
    & dG2_u >= dG1_l
    & dG1_u + dG4_u >= tHI
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG2_l
    & tHold >= 0
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG2_l > dG1_u
    & tHold >= 0
    & tHI > dG1_u + dG4_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_l >= 0
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & tHold + dG1_u >= dG3_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= tHold
    & dG2_u >= tHI
    & tLO >= tSetup
    OR
      dG1_l >= 0
    & tSetup >= 0
    & tHold > dG1_u
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_l >= 0
    & tHold > dG1_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tSetup
    & dG1_u >= dG2_l
    & tHI >= dG2_l + dG3_l
    & tHI >= tHold
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    OR
      dG2_l > dG1_u
    & dG2_u >= tHold + dG1_l
    & tHI > dG1_u + dG4_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG3_l >= 0
    & tHold >= 0
    & dG4_l >= 0
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & tHold + dG1_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= tHold
    & dG3_u >= dG3_l
    & tSetup >= 0
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & tHold >= 0
    & tHI > dG1_u + dG4_u
    & dG3_l >= 0
    & dG4_l >= 0
    & dG3_u >= dG3_l
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold + dG1_u
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & tHold + dG1_u >= dG3_l
    & dG1_u >= tHold
    & dG3_u + dG4_u >= dG2_l + dG3_l
    & tSetup >= 0
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      dG1_u >= dG1_l
    & dG2_l >= 0
    & dG3_l >= 0
    & dG4_l >= 0
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & tHold > dG1_u
    & dG4_u >= dG4_l
    & dG1_l >= 0
    & dG3_u >= dG2_l
    & dG1_u >= dG2_l
    & dG2_u >= tHold + dG1_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      tHold + dG1_u >= dG3_l
    & tHI + dG1_u > dG3_u + dG4_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_l >= 0
    & dG3_l >= 0
    & dG1_l >= 0
    & tHold >= 0
    & tSetup >= dG1_l
    & tHI > dG2_u
    & dG2_l > dG1_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tHold
    & dG4_u >= dG3_l
    & dG1_u >= tSetup
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG2_l > tHold + dG1_u
    & tHI > dG3_u + dG4_u
    & tHold >= 0
    & tHold + dG1_u >= dG3_l
    & dG3_l >= 0
    & dG1_u >= dG1_l
    & dG1_l >= 0
    & dG1_u >= tHold
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & tSetup >= dG1_l
    & tLO >= tSetup
    & dG4_u >= dG3_l
    & dG3_u >= dG2_l
    OR
      tHold >= 0
    & dG3_l >= 0
    & dG1_l >= 0
    & dG3_u >= dG3_l
    & dG2_u >= dG3_l
    & tHI > dG1_u + dG4_u
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold
    & tSetup > dG1_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tHold
    & tHold + dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & dG3_u >= dG2_l
    & dG4_u >= dG3_l
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG4_l >= 0
    & tHold >= dG2_l
    & dG3_l > dG4_u
    & tHI > dG2_u
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG1_l > dG2_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG2_u + dG4_u >= tHI
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tSetup >= 0
    & dG2_l > dG3_u
    & dG2_u + dG4_u >= tHI
    & tHold >= 0
    & dG2_l > tHold
    & dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & tHI >= tHold
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG1_u >= dG1_l
    OR
      dG2_u + dG4_u >= tHI
    & tHold >= 0
    & tSetup >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG1_l > dG2_u
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold
    & tHI >= tHold
    & dG2_u >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    & dG1_u >= dG1_l
    OR
      dG1_u >= tSetup
    & tSetup >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG3_u + dG4_u
    & dG1_l > dG2_u
    & dG1_u >= dG1_l
    & tHold >= dG2_l
    & tHI >= tHold
    & dG3_l >= 0
    & tLO >= tSetup
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= tHI
    OR
      tHold >= 0
    & dG1_u >= tHold
    & dG2_l > dG3_u
    & dG1_l > dG2_u
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & tHI >= tHold
    & dG2_u + dG4_u >= tHI
    & dG2_u >= dG2_l
    & dG4_l >= 0
    & dG3_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tHold >= dG2_l
    & dG1_l >= 0
    & dG2_u >= tHI
    & dG2_l >= 0
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & tHI >= tHold
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      dG1_l >= 0
    & dG2_u >= dG1_l
    & tSetup >= 0
    & dG4_l >= 0
    & tHold + dG1_l > dG2_u
    & tHold >= dG2_l
    & dG2_l > dG3_u
    & dG3_l > dG4_u
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & tHI > dG1_u + dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG1_l >= 0
    & tHold >= dG2_l
    & tSetup >= 0
    & tHold + dG1_l > dG2_u
    & tHI > dG1_u + dG4_u
    & tHI > dG2_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG2_u >= dG1_l
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & dG3_l >= 0
    & dG2_u >= dG2_l
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG1_u >= tSetup
    & tHI >= tHold
    & dG3_u >= dG3_l
    & dG1_u >= dG2_l
    & tLO >= tSetup
    OR
      tHI >= tHold
    & dG2_u >= dG2_l
    & tHold >= dG2_l
    & dG4_l >= 0
    & dG3_l > dG1_u
    & tHI > dG2_u
    & dG2_l > dG1_u
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG3_u >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tSetup >= 0
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG4_l >= 0
    & dG2_u >= dG1_l
    & dG2_l > tHold
    & dG3_l > dG4_u
    & tHI > dG1_u + dG4_u
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & tHold + dG1_l > dG2_u
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG1_u >= tHold
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG1_u >= dG1_l
    OR
      tSetup >= 0
    & dG3_l >= 0
    & dG4_l >= 0
    & tHI > dG1_u + dG4_u
    & dG2_l > tHold
    & tHold + dG1_l > dG2_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG1_u >= tSetup
    & dG1_u >= dG1_l
    & dG2_u >= dG1_l
    & dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    OR
      dG3_l >= 0
    & dG2_u >= tHI
    & dG4_l >= 0
    & tHold > dG1_u
    & tHI > dG3_u + dG4_u
    & tHI > dG1_u + dG4_u
    & dG1_l > tSetup
    & dG2_l > tHold
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & tSetup >= 0
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG3_l >= 0
    & dG1_l >= 0
    & dG4_l >= 0
    & tHold > dG1_u
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold
    & dG4_u >= dG4_l
    & dG1_u >= tSetup
    & dG2_u >= tHI
    & dG2_u >= dG2_l
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & tHold + dG1_l > dG2_u
    & tHold > dG1_u
    & dG4_l >= 0
    & dG2_u >= tHI
    & dG4_u >= dG4_l
    & tHold >= dG2_l
    & dG1_u >= dG1_l
    & tHI >= tHold
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tSetup >= 0
    & dG2_u >= tHI
    & dG3_l >= 0
    & dG4_l >= 0
    & tHold + dG1_l > dG2_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHold > dG1_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tSetup
    & dG1_u >= dG2_l
    & tHI >= dG2_l + dG3_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tHI >= tHold
    & tLO >= tSetup
    OR
      dG2_u >= tHI
    & tSetup >= 0
    & dG2_u >= dG1_l
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & tHold + dG1_l > dG2_u
    & dG2_l + dG3_l > tHI
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tSetup
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG2_l
    & tHI >= tHold
    & tLO >= tSetup
    OR
      tHold >= dG2_l
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > dG1_u
    & dG3_l > dG1_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG1_l >= 0
    & dG1_u >= dG1_l
    & dG3_u >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= tHI
    & tSetup >= 0
    & tLO >= tSetup
    OR
      dG2_l + dG3_l > dG3_u + dG4_u
    & tSetup >= 0
    & dG2_u >= tHI
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_l > tSetup
    & dG2_l > dG1_u
    & tHI > dG3_u + dG4_u
    & tHold + dG1_l > dG2_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= tHold
    & dG1_u >= dG1_l
    & tLO >= tSetup
    OR
      dG2_l + dG3_l > dG3_u + dG4_u
    & dG2_l > dG3_u
    & tHI > dG1_u + dG4_u
    & dG1_l > tSetup
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_u >= dG1_l
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & dG2_u >= tHI
    & dG3_u >= dG3_l
    & tSetup >= 0
    & tHold >= dG2_l
    & tLO >= tSetup
    OR
      dG1_l >= 0
    & dG2_u >= dG1_l
    & dG4_l >= 0
    & dG3_l >= 0
    & dG2_l > dG3_u
    & tHI + dG1_u > dG3_l + dG3_u
    & tHold + dG1_l > dG2_u
    & tHI > dG1_u + dG4_u
    & tSetup > dG1_u
    & tHI > dG3_l
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & tHold >= dG2_l
    & dG1_u >= dG3_l
    & dG3_u >= dG3_l
    & tHI >= tHold
    & dG1_u >= dG1_l
    & tLO >= tSetup
    & dG4_u >= dG3_l
    OR
      tHold + dG1_l > dG2_u
    & dG1_u >= dG1_l
    & dG1_u + dG4_u >= tHI
    & dG1_l >= 0
    & tHold >= dG2_l
    & dG4_l >= 0
    & tHI > dG2_u
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG2_u >= dG1_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & tSetup >= dG1_l
    & dG3_u >= dG3_l
    OR
      dG1_u + dG4_u >= tHI
    & tHold + dG1_l > dG2_u
    & dG1_u >= dG2_l
    & dG3_l >= 0
    & tHold >= dG2_l
    & dG1_l >= 0
    & tSetup >= dG1_l
    & dG4_l >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG2_u
    & dG4_u >= dG4_l
    & dG2_u >= dG1_l
    & dG1_u >= tSetup
    & tHI >= tHold
    & dG4_u >= dG3_l
    & tHI >= dG2_l + dG3_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tHI >= tHold
    & dG2_u >= dG1_l
    & dG4_l >= 0
    & tSetup >= dG1_l
    & tHI > dG3_u + dG4_u
    & dG2_l + dG3_l > tHI
    & tHI > dG2_u
    & dG4_u >= dG4_l
    & dG1_u >= tSetup
    & dG2_u >= dG2_l
    & tHold >= dG2_l
    & dG1_u >= dG2_l
    & dG1_l >= 0
    & tLO >= tSetup
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    OR
      dG1_l >= 0
    & dG4_l >= 0
    & dG2_l >= 0
    & tHI >= tHold
    & tHold + dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG2_u
    & tSetup > dG1_u
    & tHold >= dG2_l
    & dG4_u >= dG4_l
    & dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & dG2_u >= dG1_l
    & dG4_u >= dG3_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tHI > dG2_u
    & tHI >= tHold
    & dG1_l >= 0
    & dG2_l >= 0
    & dG3_l >= 0
    & dG4_l >= 0
    & tSetup > dG1_u
    & tHold + dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & tHI > dG1_u + dG4_u
    & dG4_u >= dG4_l
    & tHold >= dG2_l
    & dG3_u >= dG2_l
    & dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & dG2_u >= dG3_l
    & dG1_u >= dG1_l
    & dG4_u >= dG3_l
    & dG2_u >= dG1_l
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & dG1_u + dG4_u >= tHI
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG3_l >= 0
    & tHold + dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG2_l > dG1_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= tHold
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & tLO >= tSetup
    OR
      tHold >= 0
    & dG2_u >= dG1_l
    & dG1_l >= 0
    & dG4_l >= 0
    & dG3_l > dG2_u
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & tHold + dG1_u >= dG2_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    OR
      dG3_l >= 0
    & tHold > dG1_u
    & dG1_l >= 0
    & dG2_u >= tHI
    & dG4_l >= 0
    & dG2_l > tHold
    & tHI > dG1_u + dG4_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG3_u >= dG3_l
    & dG1_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & tSetup >= dG1_l
    & tLO >= tSetup
    OR
      dG2_l > dG3_u
    & dG3_l >= 0
    & dG2_u >= tHI
    & dG1_l >= 0
    & dG4_l >= 0
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & tHold > dG1_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & dG4_u >= dG3_l
    & tHI >= tHold
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG3_u >= dG2_l
    & dG1_l >= 0
    & tHI >= tHold
    & dG2_l >= 0
    & dG3_l > dG4_u
    & tHI > dG3_u + dG4_u
    & tHold > dG1_u
    & tSetup > dG1_u
    & dG1_u >= dG2_l
    & dG2_u >= tHI
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG4_l >= 0
    & dG3_l >= 0
    & tHI >= tHold
    & dG2_l >= 0
    & dG1_u >= dG1_l
    & dG4_u >= dG4_l
    & dG1_u >= dG2_l
    & dG3_u >= dG2_l
    & tHI > dG1_u + dG4_u
    & dG1_l >= 0
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tHold > dG1_u
    & dG2_u >= tHI
    & tLO >= tSetup
    OR
      dG2_u >= dG1_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_u >= dG1_l
    & dG2_l >= 0
    & tHI >= tHold
    & dG4_u >= dG4_l
    & dG1_l >= 0
    & dG3_u >= dG2_l
    & tHold >= dG2_l
    & dG2_u >= tHI
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    OR
      dG1_u >= dG1_l
    & tHI >= tHold
    & dG4_l >= 0
    & dG2_l + dG3_l > tHI
    & tHI > dG3_u + dG4_u
    & dG1_l > tSetup
    & dG4_u >= dG4_l
    & tSetup >= 0
    & tHold >= dG2_l
    & dG4_u >= dG3_l
    & dG3_u >= dG3_l
    & dG1_u >= dG2_l
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    OR
      tHI > dG1_u + dG4_u
    & tHold >= 0
    & dG1_l >= 0
    & tSetup >= 0
    & dG4_l >= 0
    & tHI > dG2_u
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & dG2_u >= tHold + dG1_l
    & dG1_u >= dG1_l
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tHI > dG1_u + dG4_u
    & tHold >= 0
    & tSetup >= 0
    & dG2_u >= dG2_l
    & dG1_l >= 0
    & tHI > dG2_u
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG1_u >= dG1_l
    & dG2_u >= tHold + dG1_l
    & dG4_l >= 0
    & dG3_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG1_u >= tHold
    & dG1_u >= tSetup
    & dG3_u >= dG3_l
    & dG1_u >= dG2_l
    & tLO >= tSetup
    OR
      tSetup >= 0
    & dG4_l >= 0
    & tHold >= 0
    & dG1_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold + dG1_u
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tSetup
    & dG3_l >= 0
    & dG1_u >= tHold
    & dG3_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    & dG2_u >= dG2_l
    & tLO >= tSetup
    & dG3_u + dG4_u >= dG2_l + dG3_l
    OR
      dG1_l >= 0
    & dG3_l > dG4_u
    & dG2_l > tHold + dG1_u
    & tHI > dG3_u + dG4_u
    & tSetup >= 0
    & tHold >= 0
    & dG4_l >= 0
    & dG2_u >= dG2_l
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG1_u >= tHold
    & tLO >= tSetup
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    OR
      tHold >= 0
    & dG3_l >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG1_u >= dG1_l
    & tSetup >= 0
    & tHI >= tHold
    & dG1_l >= 0
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > dG1_u
    & dG4_u >= dG4_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tHold
    & dG1_u >= tSetup
    & dG1_u + dG4_u >= tHI
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG2_u >= tHI
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      tHold + dG1_u >= dG3_l
    & tHI + dG1_u > dG3_l + dG3_u
    & dG2_l > dG3_u
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & tHold >= 0
    & dG3_l >= 0
    & dG1_l >= 0
    & tHI > dG2_u
    & tSetup > dG1_u
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tHold
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG4_l >= 0
    & dG2_l > tHold + dG1_u
    & tHI > dG1_u + dG4_u
    & dG2_l > dG3_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tHold + dG1_u >= dG3_l
    & tHold >= 0
    & dG1_l >= 0
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & dG3_u >= dG3_l
    & dG1_u >= tHold
    & dG3_l >= 0
    & tLO >= tSetup
    & dG3_u + dG4_u >= dG2_l + dG3_l
    OR
      dG3_l >= 0
    & dG1_l >= 0
    & tHold >= dG2_l
    & dG1_u + dG4_u >= tHI
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI >= dG2_l + dG3_l
    & tSetup >= dG1_l
    & tHI >= tHold
    & dG1_u >= tSetup
    & dG1_u >= tHold
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG2_l >= 0
    & tHold >= 0
    & dG4_l >= 0
    & dG2_u >= tHold + dG1_l
    & dG1_l >= 0
    & tHI > dG1_u + dG4_u
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG1_u + dG3_u > dG2_l
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG3_u >= dG3_l
    & tHold + dG1_u >= dG2_l
    & dG3_u >= dG2_l
    & dG1_u >= tHold
    & tLO >= tSetup
    OR
      dG2_l >= 0
    & dG1_l >= 0
    & dG3_u >= dG3_l
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG3_u >= dG2_l
    & tHold >= dG2_l
    & tHI > dG1_u + dG4_u
    & dG2_u >= tHold + dG1_l
    & dG4_u >= dG3_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG2_u >= tHI
    & dG1_u >= dG1_l
    & dG3_l >= 0
    & dG1_u >= tHold
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG3_l >= 0
    & dG2_l >= 0
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG1_l > dG2_u
    & tHold > dG1_u
    & tSetup > dG1_u
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG2_u + dG4_u >= tHI
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG1_u >= tHold
    & tHold >= dG2_l
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG1_l > dG2_u
    & tHI >= tHold
    & dG2_u + dG4_u >= tHI
    & tLO >= tSetup
    & dG2_l >= 0
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    OR
      tSetup >= 0
    & tHold + dG1_l > dG2_u
    & tHold >= dG2_l
    & dG1_u + dG4_u >= tHI
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & dG1_l > tSetup
    & tHI > dG2_u
    & dG3_l > dG4_u
    & dG4_u >= dG4_l
    & tHI >= tHold
    & dG2_u >= dG1_l
    & dG2_u >= dG2_l
    & dG2_u + dG4_u >= tHI
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG2_u >= dG1_l
    & tHI >= tHold
    & dG2_u + dG4_u >= tHI
    & dG2_l > dG3_u
    & tHold + dG1_l > dG2_u
    & tSetup >= 0
    & dG4_l >= 0
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & dG3_l > dG4_u
    & dG1_l > tSetup
    & dG4_u >= dG4_l
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & dG1_u + dG4_u >= tHI
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    OR
      dG2_u >= dG2_l
    & dG1_u + dG4_u >= tHI
    & tSetup >= 0
    & dG3_l >= 0
    & dG1_u >= dG2_l
    & dG4_l >= 0
    & tHI >= tHold
    & tHI > dG3_u + dG4_u
    & dG1_l > tSetup
    & dG2_u > dG3_l
    & dG1_u > dG3_l
    & tHold + dG1_l > dG2_u
    & dG2_l > tHold
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= dG1_l
    & tLO >= tSetup
    & dG1_u >= dG1_l
    & dG2_u >= tHI
    OR
      dG2_u >= dG1_l
    & tSetup >= 0
    & tHold >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_u + dG4_u >= tHI
    & dG1_u >= dG1_l
    & dG4_u >= dG4_l
    & dG1_u >= tSetup
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHold + dG1_l > dG2_u
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & tHI >= dG2_l + dG3_l
    & dG1_u >= tHold
    & tHI >= tHold
    & tLO >= tSetup
    & dG2_u >= tHI
    OR
      dG3_l >= 0
    & tHI >= tHold
    & tHold + dG1_l > dG2_u
    & dG4_l >= 0
    & dG2_l > tHold
    & dG2_l + dG3_l > tHI
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG1_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & dG2_u >= dG2_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG2_l
    & tLO >= tSetup
    OR
      dG2_u >= dG1_l
    & dG3_l > dG4_u
    & dG2_u >= dG2_l
    & tHI > dG1_u + dG4_u
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & tHold + dG1_l > dG2_u
    & dG2_l > tHold
    & dG3_u >= dG3_l
    & dG1_u >= tHold
    & tLO >= tSetup
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG2_l
    & dG1_u >= dG1_l
    OR
      dG4_l >= 0
    & dG2_l > dG3_u
    & dG3_l > dG1_u
    & tHold + dG1_l > dG2_u
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= dG2_l
    & dG2_u >= tHI
    & dG1_u >= dG1_l
    & dG4_u >= dG3_l
    & tHI >= tHold
    & tLO >= tSetup
    & tSetup >= dG1_l
    & dG3_u >= dG3_l
    OR
      dG1_l >= 0
    & tHI > dG1_u + dG4_u
    & dG2_l > dG3_u
    & dG3_l > dG4_u
    & dG2_u >= tHI
    & dG1_u >= dG1_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    OR
      dG1_l >= 0
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tHI > dG1_u + dG4_u
    & dG4_l >= 0
    & tSetup >= dG1_l
    & dG3_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG1_u >= tSetup
    & dG1_u >= tHold
    & dG2_u >= tHI
    & tLO >= tSetup
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    OR
      dG1_l >= 0
    & dG2_u >= dG1_l
    & tHI >= tHold
    & dG4_u >= dG3_l
    & dG4_l >= 0
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & dG4_u >= dG4_l
    & dG3_l >= 0
    & dG1_u >= dG1_l
    & dG2_u >= tHI
    & dG1_u >= tHold
    & tLO >= tSetup
    & tHold >= dG2_l
    & dG3_u >= dG3_l
    & dG1_u + dG4_u >= tHI
    OR
      dG2_l >= 0
    & dG3_u >= dG3_l
    & tHI > dG1_u + dG4_u
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & tHold + dG1_l > dG2_u
    & dG3_u >= dG2_l
    & tHold >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & tLO >= tSetup
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & dG2_u >= tHI
    OR
      dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & tHold >= 0
    & dG4_l >= 0
    & dG2_u + dG4_u >= tHI
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & dG1_l > tSetup
    & dG2_l > dG3_u
    & dG3_l > dG4_u
    & dG4_u >= dG4_l
    & dG1_u >= tHold
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    & tSetup >= 0
    & dG3_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    OR
      dG3_l >= 0
    & dG2_u + dG4_u >= tHI
    & dG1_u >= dG1_l
    & tHI >= tHold
    & dG4_l >= 0
    & dG1_l > tSetup
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tHI >= dG2_l + dG3_l
    & dG4_u >= dG3_l
    & tSetup >= 0
    & dG1_u + dG4_u >= tHI
    & tHold >= dG2_l
    & dG1_u >= tHold
    & dG3_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    OR
      dG1_u >= dG1_l
    & tHold >= 0
    & dG4_l >= 0
    & dG2_l > dG3_u
    & tHI >= tHold
    & dG3_l > dG4_u
    & dG2_l > tHold
    & dG1_l > tSetup
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & dG2_u >= tHI
    & tSetup >= 0
    & dG2_u >= dG2_l
    & dG1_u >= tHold
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG4_l >= 0
    & dG2_l > tHold
    & tSetup >= 0
    & dG1_u >= dG2_l
    & dG3_l >= 0
    & dG4_u >= dG4_l
    & dG1_l > tSetup
    & dG2_u >= tHI
    & dG4_u >= dG3_l
    & tHold >= 0
    & dG1_u >= dG1_l
    & tHI >= dG2_l + dG3_l
    & dG2_u >= tHold + dG1_l
    & dG2_l + dG3_l > dG3_u + dG4_u
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      dG3_l >= 0
    & tHI >= tHold
    & tSetup >= 0
    & dG1_u >= dG1_l
    & tHold >= 0
    & dG1_l >= 0
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l + dG3_l > tHI
    & dG2_l > tHold
    & dG4_u >= dG4_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tSetup
    & dG2_u >= dG2_l
    & dG2_u >= tHI
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG2_l
    & tLO >= tSetup
    OR
      dG2_l > dG3_u
    & dG1_u >= dG3_l
    & dG4_l >= 0
    & dG1_u >= dG1_l
    & dG3_l >= 0
    & tHI > dG2_u
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & tHold > dG1_u
    & dG4_u >= dG4_l
    & tHold >= dG2_l
    & dG4_u >= dG3_l
    & dG1_l >= 0
    & tLO >= tSetup
    & dG3_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    OR
      dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & tHI > dG2_u
    & dG3_l > dG4_u
    & dG1_u >= tHold
    & dG4_u >= dG4_l
    & dG1_l >= 0
    & dG1_u + dG4_u >= tHI
    & tHold >= dG2_l
    & dG2_u >= tHold + dG1_l
    & tLO >= tSetup
    & tSetup >= dG1_l
    & dG3_u >= dG3_l
    OR
      dG2_u >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG2_u >= dG3_l
    & dG1_l >= 0
    & tHI > dG2_u
    & dG2_l > tHold
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG1_u >= dG1_l
    & dG2_u >= tHold + dG1_l
    & dG1_u + dG4_u >= tHI
    & dG3_u >= dG2_l
    & tHold >= 0
    & tLO >= tSetup
    OR
      tHold >= dG2_l
    & dG1_u >= dG1_l
    & dG2_l >= 0
    & dG4_l >= 0
    & tHI > dG3_u + dG4_u
    & tSetup > dG1_u
    & dG3_l > dG4_u
    & tHI > dG2_u
    & dG4_u >= dG4_l
    & dG3_u >= dG2_l
    & dG1_u >= tHold
    & dG1_l >= 0
    & dG2_u >= tHold + dG1_l
    & dG1_u + dG4_u >= tHI
    & tLO >= tSetup
    & dG3_u >= dG3_l
    OR
      tHI > dG3_u + dG4_u
    & tHI >= tHold
    & dG1_l >= 0
    & dG1_u >= dG3_l
    & dG2_l > dG3_u
    & tSetup > dG1_u
    & tHI > dG1_u + dG4_u
    & dG2_u >= tHold + dG1_l
    & dG1_u >= dG1_l
    & tLO >= tSetup
    & tHold >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= tHI
    OR
      dG2_u >= tHI
    & dG4_l >= 0
    & dG1_l >= 0
    & dG2_l + dG3_l > tHI
    & tHI > dG3_u + dG4_u
    & dG4_u >= dG4_l
    & tSetup >= dG1_l
    & dG1_u >= tSetup
    & tHold >= dG2_l
    & dG1_u >= dG2_l
    & tHI >= tHold
    & tLO >= tSetup
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= tHold + dG1_l
    OR
      tHold + dG1_u >= dG3_l
    & dG3_u >= dG3_l
    & tHold >= 0
    & dG1_l >= 0
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG2_l > dG3_u
    & dG2_l > tHold
    & tHI > dG1_u + dG4_u
    & dG2_u >= tHold + dG1_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG2_u >= tHI
    & dG1_u >= dG1_l
    & dG3_l >= 0
    & dG1_u >= tHold
    & tLO >= tSetup
    OR
      tHI >= tHold
    & dG1_u >= tHold
    & dG2_u >= dG2_l
    & dG3_l >= 0
    & dG4_l >= 0
    & dG1_u + dG4_u >= tHI
    & dG1_l >= 0
    & tSetup > dG1_u
    & tHI > dG3_u + dG4_u
    & dG2_l > tHold
    & dG4_u >= dG4_l
    & dG2_u >= tHold + dG1_l
    & dG1_u >= dG1_l
    & dG3_u >= dG3_l
    & tLO >= tSetup
    & tHold >= 0
    & dG4_u >= dG3_l
    & dG2_u >= tHI
    OR
      tHI > dG3_u + dG4_u
    & tHI > dG2_u
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold >= 0
    & dG1_l >= 0
    & dG1_u >= dG2_l
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG2_l > tHold
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tSetup
    & dG2_l + dG3_l > tHI
    OR
      tHI > dG3_u + dG4_u
    & tHI >= tHold
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold > dG1_u
    & dG1_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_u >= dG2_l
    & dG3_l > dG1_u
    & dG1_u >= dG1_l
    & dG2_l > tHold
    & dG2_u >= tHold + dG1_l
    & dG2_u >= tHI
    OR
      tHI > dG3_u + dG4_u
    & tHI >= tHold
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold >= dG2_l
    & dG1_l >= 0
    & dG2_l > dG3_u
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG3_l > dG1_u
    & dG1_u >= dG1_l
    & dG2_u >= tHold + dG1_l
    & dG2_u >= tHI
    OR
      tHI > dG3_u + dG4_u
    & tHI > dG1_u + dG4_u
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold >= 0
    & dG1_l >= 0
    & dG2_l > dG3_u
    & dG3_l > dG4_u
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG2_u >= dG2_l
    & dG1_u >= dG1_l
    & dG1_u >= tHold
    & dG2_l > tHold
    & dG2_u >= tHold + dG1_l
    & dG2_u >= tHI
    OR
      tHI > dG1_u + dG4_u
    & tLO >= tSetup
    & tSetup >= dG1_l
    & tHold >= 0
    & dG1_l >= 0
    & dG1_u >= dG2_l
    & dG2_l + dG3_l > dG3_u + dG4_u
    & dG3_l >= 0
    & dG4_l >= 0
    & dG4_u >= dG4_l
    & dG3_u >= dG3_l
    & dG4_u >= dG3_l
    & dG2_l > tHold
    & dG2_u >= tHold + dG1_l
    & dG1_u >= tSetup
    & dG2_u >= tHI
    This good constraint is exact (sound and complete)

    11.729 MiB (i.e., 1537452 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-layerBFS-incl2-merge-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 103
    Number of transitions                   : 125
    Number of computed states               : 126
    Total computation time                  : 87.626 seconds
    States/second in state space            : 1.1 (103/87.626 seconds)
    Computed states/second                  : 1.4 (126/87.626 seconds)
    Estimated memory                        : 15.332 MiB (i.e., 2009624 words of size 8)
    
    Generating graphical output to '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-layerBFS-incl2-merge-EF-statespace.jpg'…
    Writing the states description to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-layerBFS-incl2-merge-EF-statespace.states'…
    
    Drawing the cartography…
    Plot cartography in 2D projected on parameters tHI and tLO to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-layerBFS-incl2-merge-EF_cart.png'.
    
    ------------------------------------------------------------
     Statistics: Algorithm counters
    ------------------------------------------------------------
    main algorithm                          : 87.643 seconds
    ------------------------------------------------------------
     Statistics: Parsing counters
    ------------------------------------------------------------
    model parsing                           : 0.015 second
    ------------------------------------------------------------
     Statistics: State computation counters
    ------------------------------------------------------------
    number of state comparisons             : 437
    number of constraints comparisons       : 427
    number of new states <= old             : 5
    number of new states >= old             : 2
    StateSpace.merging attempts             : 239
    StateSpace.merges                       : 16
    StatesMerging.merging attempts          : 0
    StatesMerging.merges                    : 0
    ------------------------------------------------------------
     Statistics: Graphics-related counters
    ------------------------------------------------------------
    state space drawing                     : 0.737 second
    cartography drawing                     : 0.620 second
    ------------------------------------------------------------
     Statistics: Global counter
    ------------------------------------------------------------
    total                                   : 93.183 seconds

    IMITATOR successfully terminated (after 93.185 seconds)
    Estimated memory used: 45.075 MiB (i.e., 5908085 words of size 8)