========== Reachable Symbolic Configurations ==========
(idle1 idle2 idle3 , id = (i0 ) ,
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t + d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 <= 0 and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 <= 0 and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t + d and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t + d and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t + d and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t + d and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 trying2 idle3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 waiting2 idle3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 2 * d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= 2 * d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 waiting2 idle3 , id = (i2 ) ,
x1 > t and x2 >= 0 and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t - d and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t + d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t - d and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 cs2 idle3 , id = (i2 ) ,
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t + d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t and x1 - x3 <= 0 and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 2 * t and x2 > t and x3 >= 2 * t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 2 * t and x2 > t and x3 >= 2 * t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t + d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 2 * t and x2 > t and x3 >= 0 and x2 - x1 < - t and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 2 * t and x1 - x2 <= 0 and x1 - x3 < - t and x2 - x3 < - t, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 idle2 trying3 , id = (i0 ) ,
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 trying2 trying3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 waiting2 trying3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t + d and x3 <= d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= d and x2 - x1 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 <= d and x1 - x2 < - t and x1 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t + d and x3 <= d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 waiting2 trying3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= 2 * d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 idle2 waiting3 , id = (i0 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= 2 * d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 2 * d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 idle2 waiting3 , id = (i3 ) ,
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 >= 0 and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 <= 0 and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t - d and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t + d and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t - d and x1 - x2 < - t and x1 - x3 < - t + d and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 < - t and x1 - x3 <= 0 and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0
)
(idle1 trying2 waiting3 , id = (i0 ) ,
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= d and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 < - t + d and x2 <= d and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 <= d and x1 - x2 <= 0 and x1 - x3 < - t and x2 <= d and x2 - x1 <= d and x2 - x3 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 < - t + d and x2 <= d and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 trying2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= 2 * d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 waiting2 waiting3 , id = (i0 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 waiting2 waiting3 , id = (i2 ) ,
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 2 * d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 waiting2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= 2 * d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(idle1 cs2 waiting3 , id = (i2 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 2 * t and x2 > t and x3 >= 2 * t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 2 * d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 idle2 cs3 , id = (i3 ) ,
x1 >= 2 * t and x2 >= 2 * t and x3 > t and x1 - x2 <= 2 * d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 2 * t and x3 > t and x1 - x2 < - t and x1 - x3 <= 0 and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 2 * t and x2 >= 2 * t and x3 > t and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x2 <= 0 and x1 - x3 < - t and x2 - x3 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 <= 0 and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 < - t + d and x2 - x1 <= 0 and x2 - x3 < - t + d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 2 * d and x2 - x1 < - t and x2 - x3 < - t + d and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t + d and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 < - t and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 <= 0 and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 < - t + d and x2 - x1 <= 0 and x2 - x3 < - t + d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(idle1 waiting2 cs3 , id = (i3 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 2 * d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 2 * t and x2 >= 2 * t and x3 > t and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d = 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t + d and x1 - x3 < - t + d and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(trying1 idle2 idle3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 trying2 idle3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 idle3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 <= d and x1 - x2 < - t and x1 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 idle3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= 2 * d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 idle2 trying3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 trying2 trying3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 trying3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 >= 0 and x1 <= d and x1 - x2 < - t and x1 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 <= d and x1 - x2 < - t and x1 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 trying3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 idle2 waiting3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 > t and x1 <= d and x1 - x2 <= d and x1 - x3 < - t and x2 <= d and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 idle2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= 2 * d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 trying2 waiting3 , id = (i0 ) ,
x1 >= 0 and x2 >= 0 and x3 > t and x1 <= d and x1 - x2 <= 0 and x1 - x3 < - t and x2 <= d and x2 - x1 <= d and x2 - x3 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 <= d and x1 - x2 <= d and x1 - x3 < - t and x2 <= d and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 trying2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 waiting3 , id = (i0 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 <= d and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 waiting3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(trying1 waiting2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= d and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 idle3 , id = (i0 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= 2 * d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 idle3 , id = (i1 ) ,
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t - d and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t + d and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t - d and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t + d and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(waiting1 trying2 idle3 , id = (i0 ) ,
x1 > t and x2 >= 0 and x3 >= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 <= d and x3 <= d and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= d and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 idle3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= 2 * d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 idle3 , id = (i0 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 idle3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 idle3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= 2 * d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 cs2 idle3 , id = (i2 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= d and x2 - x1 <= 0 and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 trying3 , id = (i0 ) ,
x1 > t and x2 >= 0 and x3 >= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= d and x2 - x1 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 trying3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= 2 * d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 trying3 , id = (i0 ) ,
x1 > t and x2 >= 0 and x3 >= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 <= d and x3 <= d and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 >= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 trying3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 trying3 , id = (i0 ) ,
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= d and x2 - x1 <= 0 and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 trying3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= d and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 trying3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= 0 and x3 <= d and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 waiting3 , id = (i0 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 waiting3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= 2 * d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 > t and x3 > t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= 2 * d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 waiting3 , id = (i0 ) ,
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= d and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 waiting3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 trying2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 <= d and x1 - x2 <= 0 and x1 - x3 <= d and x2 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 waiting3 , id = (i2 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 waiting3 , id = (i1 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 waiting3 , id = (i3 ) ,
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 >= 0 and x2 >= 0 and x3 >= 0 and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 cs2 waiting3 , id = (i2 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 idle2 cs3 , id = (i3 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= 2 * d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= d and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(waiting1 waiting2 cs3 , id = (i3 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= d and x1 - x3 <= d and x2 - x1 <= 0 and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= d and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(cs1 idle2 idle3 , id = (i1 ) ,
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 2 * t and x3 >= 2 * t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= 2 * d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 <= 0 and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 >= 2 * t and x1 - x3 < - t and x2 - x1 <= 0 and x2 - x3 < - t, - t < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 >= 0 and x2 - x1 < - t and x2 - x3 <= 0 and x3 - x1 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 >= 0 and x2 - x1 < - t and x3 - x1 < - t and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 <= 0 and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 <= 0 and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d = 0 and
t - 2 * d < 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 2 * t and x3 >= 2 * t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 2 * d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= 2 * d and x3 - x1 < - t + d and x3 - x2 < - t, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t + d and x2 - x3 < - t and x3 - x1 <= 2 * d, - t < 0 and
- t - d < 0 and
- t + d < 0 and
- d < 0
)
(cs1 waiting2 idle3 , id = (i1 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 >= 0 and x1 - x2 <= 0 and x2 - x1 <= d and x3 - x1 < - t and x3 - x2 < - t, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= 2 * d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(cs1 idle2 waiting3 , id = (i1 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= 2 * d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 0 and x3 > t and x1 - x3 <= 0 and x2 - x1 < - t and x2 - x3 < - t and x3 - x1 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 >= 2 * t and x3 >= 2 * t and x1 - x2 < - t and x1 - x3 < - t and x2 - x3 <= 0 and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
(cs1 waiting2 waiting3 , id = (i1 ) ,
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= d and x3 - x1 <= d and x3 - x2 <= 0, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0 ->
x1 > t and x2 > t and x3 > t and x1 - x2 <= 0 and x1 - x3 <= 0 and x2 - x1 <= d and x2 - x3 <= 0 and x3 - x1 <= d and x3 - x2 <= d, - t < 0 and
- t - 2 * d < 0 and
- t - d < 0 and
- t + d <= 0 and
- d < 0
)
========== Correspondence with Symbolic Graph ==========
[ 0 -- ( idle1 idle2 idle3 , id = (i0 ) , 0)]
[ 1 -- ( idle1 idle2 trying3 , id = (i0 ) , 0)]
[ 2 -- ( idle1 trying2 idle3 , id = (i0 ) , 0)]
[ 3 -- ( trying1 idle2 idle3 , id = (i0 ) , 0)]
[ 4 -- ( trying1 idle2 trying3 , id = (i0 ) , 0)]
[ 5 -- ( trying1 trying2 idle3 , id = (i0 ) , 0)]
[ 6 -- ( waiting1 idle2 idle3 , id = (i1 ) , 0)]
[ 7 -- ( cs1 idle2 idle3 , id = (i1 ) , 0)]
[ 8 -- ( trying1 trying2 trying3 , id = (i0 ) , 0)]
[ 9 -- ( trying1 waiting2 idle3 , id = (i2 ) , 0)]
[ 10 -- ( waiting1 trying2 idle3 , id = (i1 ) , 0)]
[ 11 -- ( waiting1 waiting2 idle3 , id = (i2 ) , 0)]
[ 12 -- ( waiting1 cs2 idle3 , id = (i2 ) , 0)]
[ 13 -- ( idle1 waiting2 idle3 , id = (i2 ) , 0)]
[ 14 -- ( idle1 cs2 idle3 , id = (i2 ) , 0)]
[ 15 -- ( waiting1 idle2 idle3 , id = (i0 ) , 0)]
[ 16 -- ( waiting1 idle2 trying3 , id = (i0 ) , 0)]
[ 17 -- ( waiting1 trying2 idle3 , id = (i0 ) , 0)]
[ 18 -- ( waiting1 trying2 trying3 , id = (i0 ) , 0)]
[ 19 -- ( idle1 trying2 trying3 , id = (i0 ) , 0)]
[ 20 -- ( waiting1 waiting2 idle3 , id = (i1 ) , 0)]
[ 21 -- ( cs1 waiting2 idle3 , id = (i1 ) , 0)]
[ 22 -- ( idle1 waiting2 idle3 , id = (i0 ) , 0)]
[ 23 -- ( idle1 waiting2 trying3 , id = (i0 ) , 0)]
[ 24 -- ( trying1 waiting2 idle3 , id = (i0 ) , 0)]
[ 25 -- ( trying1 waiting2 trying3 , id = (i0 ) , 0)]
[ 26 -- ( idle1 idle2 waiting3 , id = (i3 ) , 0)]
[ 27 -- ( trying1 idle2 waiting3 , id = (i3 ) , 0)]
[ 28 -- ( waiting1 idle2 trying3 , id = (i1 ) , 0)]
[ 29 -- ( waiting1 idle2 waiting3 , id = (i3 ) , 0)]
[ 30 -- ( waiting1 idle2 cs3 , id = (i3 ) , 0)]
[ 31 -- ( idle1 idle2 cs3 , id = (i3 ) , 0)]
[ 32 -- ( idle1 trying2 waiting3 , id = (i3 ) , 0)]
[ 33 -- ( idle1 waiting2 trying3 , id = (i2 ) , 0)]
[ 34 -- ( trying1 trying2 waiting3 , id = (i3 ) , 0)]
[ 35 -- ( trying1 waiting2 trying3 , id = (i2 ) , 0)]
[ 36 -- ( waiting1 trying2 trying3 , id = (i1 ) , 0)]
[ 37 -- ( waiting1 trying2 waiting3 , id = (i3 ) , 0)]
[ 38 -- ( waiting1 waiting2 trying3 , id = (i2 ) , 0)]
[ 39 -- ( waiting1 waiting2 waiting3 , id = (i3 ) , 0)]
[ 40 -- ( waiting1 waiting2 cs3 , id = (i3 ) , 0)]
[ 41 -- ( idle1 waiting2 waiting3 , id = (i3 ) , 0)]
[ 42 -- ( idle1 waiting2 cs3 , id = (i3 ) , 0)]
[ 43 -- ( waiting1 waiting2 waiting3 , id = (i2 ) , 0)]
[ 44 -- ( waiting1 cs2 waiting3 , id = (i2 ) , 0)]
[ 45 -- ( idle1 waiting2 waiting3 , id = (i2 ) , 0)]
[ 46 -- ( idle1 cs2 waiting3 , id = (i2 ) , 0)]
[ 47 -- ( idle1 idle2 waiting3 , id = (i0 ) , 0)]
[ 48 -- ( idle1 trying2 waiting3 , id = (i0 ) , 0)]
[ 49 -- ( trying1 idle2 waiting3 , id = (i0 ) , 0)]
[ 50 -- ( trying1 trying2 waiting3 , id = (i0 ) , 0)]
[ 51 -- ( waiting1 idle2 waiting3 , id = (i1 ) , 0)]
[ 52 -- ( cs1 idle2 waiting3 , id = (i1 ) , 0)]
[ 53 -- ( trying1 waiting2 waiting3 , id = (i2 ) , 0)]
[ 54 -- ( waiting1 trying2 waiting3 , id = (i1 ) , 0)]
[ 55 -- ( trying1 waiting2 waiting3 , id = (i3 ) , 0)]
[ 56 -- ( waiting1 waiting2 trying3 , id = (i1 ) , 0)]
[ 57 -- ( waiting1 waiting2 idle3 , id = (i0 ) , 0)]
[ 58 -- ( waiting1 waiting2 trying3 , id = (i0 ) , 0)]
[ 59 -- ( waiting1 waiting2 waiting3 , id = (i1 ) , 0)]
[ 60 -- ( cs1 waiting2 waiting3 , id = (i1 ) , 0)]
[ 61 -- ( idle1 waiting2 waiting3 , id = (i0 ) , 0)]
[ 62 -- ( trying1 waiting2 waiting3 , id = (i0 ) , 0)]
[ 63 -- ( waiting1 idle2 waiting3 , id = (i0 ) , 0)]
[ 64 -- ( waiting1 trying2 waiting3 , id = (i0 ) , 0)]
========== Time Statistics ==========
child : 0.00
self : 53.48
---------------
total : 53.48