off rlabout;



rlset reals;


{}


rp3sol :=
d1 > 0 and d1 - 1 <= 0 and a - 1 > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2
*d1 - 2 < 0 and a + 2*d1 - 1 >= 0 and (d1 - 1 = 0 or 2*d1 - 1 < 0) or d1 > 0 and
 4*d1 - 1 < 0 and a > 0 and a - 1 <= 0 and a - 2*d1 = 0 and a - d1 >= 0 and a - 
d1 - 1 < 0 and a + d1 - 1 = 0 and (a - 1 = 0 or a - d1 > 0) and (a - 1 = 0 or a 
- d1 = 0) or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - 2 <= 0 and a - d1 - 1 > 0 
and 2*a - d1 - 1 < 0 and (d1 - 1 < 0 or a - 2 < 0) and (d1 - 1 < 0 or a - 1 <= 0
) and (a - 2 = 0 or a - 1 < 0) and (d1 - 1 = 0 or a - 1 < 0) and (a - 1 > 0 or 
d1 - 1 = 0 and a - 1 = 0) or d1 > 0 and d1 - 1 < 0 and a > 0 and a - 1 <= 0 and 
a - 2*d1 > 0 and a - d1 >= 0 and a - d1 - 1 < 0 and a + d1 - 1 = 0 and 2*a - d1 
- 1 = 0 and (a - 1 = 0 or a - d1 > 0) and (a - 1 = 0 or a - d1 = 0) or d1 > 0 
and a - 1 <= 0 and a - 2*d1 > 0 and a - d1 = 0 and 2*a - 1 >= 0 and 2*a - d1 - 1
 < 0 and (a - 1 = 0 or a + d1 - 1 < 0) and (a - 1 = 0 or 2*a - 1 = 0) and (a + 
d1 - 1 > 0 or 2*a - 1 = 0) or d1 > 0 and a > 0 and a - 1 <= 0 and a - 2*d1 > 0 
and a - d1 = 0 and a + d1 - 1 >= 0 and 2*a - d1 - 1 < 0 and (a - 1 = 0 or a + d1
 - 1 > 0) and (d1 - 1 > 0 or a - 1 = 0 or a + d1 - 1 = 0) and (d1 - 1 < 0 or a -
 1 = 0) or d1 > 0 and a > 0 and a - 1 <= 0 and a - 2*d1 > 0 and a - d1 = 0 and a
 + d1 - 1 > 0 and 2*a - d1 - 1 < 0 and (d1 - 1 > 0 or a - 1 = 0) and (d1 - 1 < 0
 or a - 1 = 0) or d1 > 0 and a - 1 > 0 and a - 2*d1 - 1 > 0 and a - d1 - 1 = 0 
and 2*a - 3*d1 - 2 < 0 or d1 > 0 and a - 1 >= 0 and a - 2*d1 - 1 > 0 and a - d1 
- 1 = 0 and 2*a - 3*d1 - 2 < 0 or d1 > 0 and a - 2 <= 0 and a - 1 >= 0 and a - 2
*d1 - 1 > 0 and a - d1 - 1 = 0 and (d1 - 2 < 0 or a - 2 < 0) and (d1 - 1 < 0 or 
a - 2 < 0) and (a - 2 = 0 or a - 1 = 0) or d1 > 0 and a - 2 <= 0 and a - 1 >= 0 
and a - 2*d1 - 1 > 0 and a - d1 - 1 = 0 and (d1 - 1 < 0 or a - 2 < 0) and (a - 2
 = 0 or a - 1 = 0) or d1 > 0 and d1 - 1 < 0 and a - 2 >= 0 and a - 2*d1 - 2 > 0 
and a - d1 = 0 and a + d1 - 2 < 0 and a + 2*d1 - 4 = 0 or d1 > 0 and d1 - 1 < 0 
and a > 0 and a - 1 < 0 and a - 3*d1 > 0 and a - 2*d1 - 1 >= 0 and a - d1 = 0 
and a + d1 - 2 = 0 or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - 1 < 0 and a - 2*
d1 > 0 and a - d1 = 0 and a + d1 - 1 >= 0 and (d1 - 1 = 0 or 2*d1 - 1 < 0) and (
d1 - 1 = 0 or a + d1 - 1 = 0) and (2*d1 - 1 > 0 or a + d1 - 1 = 0) or d1 - 1 > 0
 and a - 2 <= 0 and a - 1 >= 0 and a - 2*d1 - 1 >= 0 and a - d1 - 1 >= 0 and a +
 d1 - 2 < 0 and 2*a - d1 - 3 <= 0 and 2*a - d1 - 2 >= 0 and (2*a - 2*d1 - 3 >= 0
 or 2*a - d1 - 3 < 0) and (a - 1 = 0 or a - d1 - 1 = 0 and 2*a - d1 - 2 > 0) and
 (a - 2 = 0 or a - 1 = 0) and (a - 1 = 0 or 2*a - d1 - 2 = 0) and (a - 1 = 0 or 
2*a - d1 - 3 = 0) and (a - 1 = 0 or 2*a - d1 - 3 = 0 or 2*a - d1 - 2 = 0) and (a
 - 2 = 0 or a - 1 = 0 or a - 2*d1 - 1 = 0 and a - d1 - 1 > 0 and 2*a - d1 - 2 = 
0) or d1 > 0 and 2*d1 - 1 <= 0 and a > 0 and a - 1 <= 0 and a - d1 > 0 and a + 
d1 - 1 = 0 and 2*a + d1 - 1 < 0 and (2*d1 - 1 < 0 or a - 1 = 0) and (2*d1 - 1 = 
0 or a - 1 = 0 or a + 2*d1 - 1 < 0) and (a - 1 = 0 or a + 2*d1 - 1 > 0) or d1 > 
0 and d1 - 1 <= 0 and a > 0 and a - 2 <= 0 and a - d1 - 1 > 0 and 2*a - d1 - 1 <
 0 and (d1 - 1 < 0 or a - 2 < 0) and (d1 - 1 = 0 or a - 1 < 0) and (a - 1 > 0 or
 d1 - 1 = 0 and a - 1 = 0) and (a - 2 = 0 or a - 1 < 0) or d1 > 0 and a > 0 and 
a - 1 <= 0 and a - 2*d1 - 1 > 0 and a - d1 > 0 and a - d1 - 2 <= 0 and a + d1 - 
1 <= 0 and 2*a - d1 - 2 <= 0 and (a - 1 = 0 or a - d1 - 1 > 0) and (a - 1 = 0 or
 a + d1 - 1 = 0) and (a - d1 - 2 = 0 or a - d1 - 1 < 0 or 2*a - d1 - 2 = 0) and 
(a - 1 = 0 or a - d1 - 2 = 0 or a - d1 - 1 < 0 or 2*a - d1 - 2 = 0) or d1 > 0 
and d1 - 1 <= 0 and a - 1 <= 0 and a - d1 > 0 and a + d1 - 1 <= 0 and 2*a - 1 >=
 0 and 2*a + d1 - 1 < 0 and (d1 - 1 < 0 or 2*a - 1 > 0) and (2*d1 - 1 < 0 or 2*a
 - 1 > 0) and (a - 1 = 0 or 2*a - 1 = 0) and (a - 1 = 0 or a + d1 - 1 = 0) and (
d1 - 1 = 0 or a + d1 - 1 = 0) or d1 - 1 <= 0 and 2*d1 - 1 > 0 and a > 0 and a - 
1 < 0 and a - 2*d1 > 0 and a - d1 = 0 and a + d1 - 1 >= 0 and (d1 - 1 = 0 or a +
 d1 - 1 = 0) or d1 <= 0 and d1 < 0 and d1 > 0 and 2*d1 - 1 < 0 and a - 1 = 0 or 
d1 > 0 and d1 - 1 < 0 and a > 0 and a - 1 <= 0 and a - d1 >= 0 and a + d1 - 1 = 
0 and a + 2*d1 - 1 < 0 and 2*a + d1 - 2 = 0 and (a - 1 = 0 or a - d1 > 0) and (a
 - 1 = 0 or a - d1 = 0) or d1 > 0 and d1 - 1 <= 0 and a - 1 > 0 and a - d1 >= 0 
and a + d1 - 1 = 0 and a + 2*d1 - 2 <= 0 and 2*a + 3*d1 - 3 < 0 and (d1 - 1 = 0 
or a + 2*d1 - 2 < 0) and (d1 - 1 = 0 or a + 2*d1 - 2 = 0) and (a - d1 = 0 and a 
+ 2*d1 - 2 = 0 or d1 - 1 < 0 and a + 2*d1 - 2 < 0) and (d1 - 1 = 0 or a - d1 = 0
) or d1 > 0 and d1 - 1 <= 0 and a - 1 > 0 and a - d1 >= 0 and a + d1 - 2 <= 0 
and a + d1 - 1 >= 0 and 2*a + 3*d1 - 3 < 0 and (2*d1 - 1 <= 0 or a + d1 - 2 < 0)
 and (d1 - 1 = 0 or 2*d1 - 1 <= 0 or a + 2*d1 - 2 < 0) and (a - d1 > 0 or a + 2*
d1 - 2 <= 0) and (d1 - 1 = 0 or 2*d1 - 1 < 0 or a + 2*d1 - 2 <= 0) and (d1 - 1 =
 0 or a + 2*d1 - 2 <= 0) and (a + d1 - 1 = 0 or a + 2*d1 - 2 <= 0) and (a - d1 =
 0 or 2*d1 - 1 >= 0 and a + d1 - 1 > 0 or 2*d1 - 1 < 0 and a + d1 - 1 = 0) and (
d1 - 1 = 0 or a + d1 - 1 = 0) and (a + d1 - 2 = 0 or a + d1 - 1 = 0 or 2*d1 - 1 
> 0 and a + 2*d1 - 2 >= 0) and (a - d1 = 0 or a + d1 - 2 = 0) and (a + d1 - 2 = 
0 or a + 2*d1 - 2 >= 0 or d1 - 1 < 0 and a + d1 - 1 = 0) and (a - d1 = 0 or 2*d1
 - 1 >= 0 and a + 2*d1 - 2 > 0) or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - 2*d1
 > 0 and a - d1 = 0 and a + d1 - 1 >= 0 and 2*a - d1 - 1 < 0 and (a - 1 >= 0 or 
a + d1 - 1 > 0) and (d1 - 1 = 0 or a + d1 - 1 = 0) and (d1 - 1 = 0 or a - 1 < 0)
 and (d1 - 1 = 0 and a - 1 = 0 or d1 - 1 < 0 and a - 1 < 0) and (a - 1 = 0 or a 
+ d1 - 1 = 0) and (d1 - 1 < 0 or a - 1 >= 0) or d1 > 0 and d1 - 1 < 0 and a > 0 
and a - 1 < 0 and a - 3*d1 > 0 and a - d1 = 0 and a + d1 - 2 >= 0 and a + 3*d1 -
 2 = 0 or d1 > 0 and d1 - 1 < 0 and a - 1 > 0 and a + d1 - 1 = 0 and a + 2*d1 - 
2 = 0 and a + 3*d1 - 2 = 0 and 2*a + 3*d1 - 3 < 0 and 2*a + 3*d1 - 2 > 0 or d1 -
 1 < 0 and 2*d1 - 1 >= 0 and a - 1 > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a +
 2*d1 - 2 = 0 and 2*a + 3*d1 - 3 < 0 or d1 > 0 and d1 - 1 <= 0 and a > 0 and a -
 2*d1 > 0 and a - d1 = 0 and a + d1 - 1 >= 0 and 2*a - d1 - 1 < 0 and (a - 1 >= 
0 or a + d1 - 1 > 0) and (d1 - 1 = 0 or a + d1 - 1 = 0) and (d1 - 1 = 0 or a - 1
 < 0) and (d1 - 1 < 0 or a - 1 = 0) and (a - 1 = 0 or a + d1 - 1 = 0) and (d1 - 
1 < 0 or a - 1 >= 0) or d1 > 0 and d1 - 1 < 0 and a - 1 <= 0 and a + d1 - 1 = 0 
and a + 2*d1 - 1 < 0 and 2*a - 1 >= 0 and 2*a + d1 - 1 > 0 and (2*d1 - 1 < 0 or 
2*a - 1 > 0) and (a - 1 = 0 or 2*a - 1 = 0) or d1 > 0 and d1 - 1 < 0 and a - 2 
<= 0 and a - 1 >= 0 and a - 2*d1 - 1 > 0 and 2*a - d1 - 3 < 0 and 2*a - d1 - 2 
>= 0 and (a - d1 - 1 >= 0 or a + d1 - 1 >= 0) and (a - 1 = 0 or a - d1 - 1 <= 0 
or a + d1 - 1 > 0) and (a - 1 = 0 or a - d1 - 1 < 0) and (a - 2 = 0 or a - 1 = 0
) and (a - 1 = 0 or 2*a - d1 - 2 = 0) and (a - d1 - 1 < 0 or a - d1 - 1 = 0 and 
a + d1 - 1 <= 0) and (a - 1 = 0 or a - d1 - 1 > 0) and (a - 2 = 0 or a - 1 = 0 
or a - d1 - 1 < 0 and 2*a - d1 - 2 = 0) or d1 > 0 and d1 - 1 <= 0 and a - 2 <= 0
 and a - 1 >= 0 and a - 2*d1 - 1 > 0 and a - d1 >= 0 and a - d1 - 1 < 0 and a + 
d1 - 1 >= 0 and 2*a - d1 - 3 < 0 and 2*a - d1 - 2 >= 0 and (d1 - 1 < 0 or a - 1 
> 0) and (d1 - 1 < 0 or a - 1 = 0 or 2*a - 3 > 0) and (a - 1 = 0 or a - d1 > 0) 
and (a - 1 = 0 or 2*a - d1 - 2 > 0) and (a - 1 = 0 or a - d1 = 0) and (d1 - 1 = 
0 or a - 1 = 0) and (a - 2 = 0 or a - d1 = 0 or 2*a - d1 - 2 = 0) or d1 > 0 and 
d1 - 1 <= 0 and a > 0 and a - 1 <= 0 and a - 2*d1 - 1 > 0 and a - d1 - 1 >= 0 
and 2*a - d1 - 2 <= 0 and (a - d1 - 1 = 0 or a + d1 - 1 <= 0) and (a - 1 = 0 or 
a - d1 - 1 > 0 and 2*a - d1 - 2 = 0) and (d1 - 1 = 0 or a + d1 - 1 >= 0) or d1 >
 0 and d1 - 1 <= 0 and a - 1 >= 0 and a - d1 - 1 = 0 and a + d1 - 1 < 0 and (d1 
- 1 < 0 or a - 2 > 0) and (d1 - 1 = 0 or a - 1 = 0) and (a - 2 > 0 or a - 1 = 0)
 or d1 > 0 and d1 - 1 < 0 and a > 0 and a - 1 < 0 and a - d1 = 0 and a + d1 - 1 
= 0 and a + 2*d1 - 2 <= 0 and a + 3*d1 - 2 < 0 and 2*a + 3*d1 - 3 > 0 and (a + 2
*d1 - 2 = 0 or 2*a + d1 - 2 >= 0) or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - d1
 >= 0 and a + d1 - 2 < 0 and a + d1 - 1 >= 0 and a + 2*d1 - 2 <= 0 and a + 3*d1 
- 2 < 0 and 2*a + 3*d1 - 3 > 0 and (d1 - 1 = 0 or a + d1 - 1 > 0 or a + 2*d1 - 2
 = 0) and (2*d1 - 1 >= 0 or a - 1 > 0 or a + 2*d1 - 2 = 0) and (d1 - 1 = 0 or a 
+ d1 - 1 = 0 or a + 2*d1 - 2 < 0) and (d1 - 1 = 0 or a - 1 <= 0 or a + 2*d1 - 2 
< 0) and (d1 - 1 = 0 or a + d1 - 1 = 0) and (d1 - 1 = 0 or a - d1 = 0) and (a + 
d1 - 1 = 0 or a - 1 <= 0 and a + 2*d1 - 2 = 0) and (a + d1 - 1 = 0 or a - d1 = 0
 and a + 2*d1 - 2 = 0) or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - d1 >= 0 and a
 + d1 - 2 <= 0 and a + d1 - 1 >= 0 and a + 3*d1 - 2 < 0 and 2*a + 3*d1 - 3 > 0 
and (2*d1 - 1 > 0 or a - 1 >= 0 or a + 2*d1 - 2 >= 0) and (a - d1 - 1 >= 0 or a 
+ d1 - 2 < 0) and (a - 1 >= 0 or a + d1 - 2 < 0) and (d1 - 1 = 0 or 2*d1 - 1 <= 
0 or a + 2*d1 - 2 < 0) and (a - 1 > 0 or a + d1 - 1 = 0 or a + 2*d1 - 2 <= 0) 
and (d1 - 1 = 0 or a + 2*d1 - 2 <= 0) and (a + d1 - 1 = 0 or a + 2*d1 - 2 <= 0) 
and (a - d1 > 0 or a + 2*d1 - 2 <= 0) and (d1 - 1 = 0 or 2*d1 - 1 < 0 or a + 2*
d1 - 2 <= 0) and (2*d1 - 1 >= 0 or a - d1 = 0 or a + d1 - 1 = 0) and (d1 - 1 = 0
 or a + d1 - 1 = 0) and (a - d1 = 0 or 2*d1 - 1 >= 0 and a + 2*d1 - 2 > 0) and (
a + d1 - 2 = 0 or a + d1 - 1 = 0 or 2*d1 - 1 > 0 and a + 2*d1 - 2 >= 0) and (a -
 d1 = 0 or a + d1 - 2 = 0 or 2*d1 - 1 < 0 and a - 1 <= 0 and a + 2*d1 - 2 < 0) 
and (a + d1 - 2 = 0 or a + d1 - 1 = 0 or a + 2*d1 - 2 >= 0) or d1 > 0 and d1 - 1
 <= 0 and a > 0 and a - 2 <= 0 and a - d1 - 1 > 0 and 2*a - d1 - 1 < 0 and (d1 -
 1 < 0 or a - 2 < 0) and (d1 - 1 = 0 or a - 1 > 0) and (d1 - 1 = 0 or a - 1 < 0)
 and (a - 1 > 0 or d1 - 1 = 0 and a - 1 = 0) and (a - 2 = 0 or a - 1 < 0) or d1 
- 1 < 0 and 2*d1 - 1 > 0 and a - 1 > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a +
 2*d1 - 2 < 0 or d1 > 0 and d1 - 1 <= 0 and a - 1 >= 0 and a - d1 - 1 = 0 and a 
+ d1 - 1 < 0 and (d1 - 1 < 0 or a - 2 > 0) and (d1 - 1 = 0 or a - 1 = 0) or d1 >
 0 and d1 - 1 <= 0 and a > 0 and a - 2 <= 0 and a - d1 - 1 > 0 and 2*a - d1 - 1 
<= 0 and (d1 - 1 < 0 or a - 2 < 0) and (d1 - 1 = 0 or a - 1 > 0) and (d1 - 1 = 0
 or a - 1 < 0) and (a - 1 > 0 or d1 - 1 = 0 and a - 1 = 0) and (a - 2 = 0 or a -
 1 < 0) or d1 > 0 and 2*d1 - 1 < 0 and a > 0 and a - 1 <= 0 and a - d1 = 0 and a
 + d1 - 1 = 0 and a + 2*d1 - 2 > 0 or d1 > 0 and 2*d1 - 1 < 0 and a - 1 > 0 and 
a - 2*d1 < 0 and a - d1 = 0 and a + d1 - 1 = 0 or d1 > 0 and 2*d1 - 1 < 0 and a 
- 1 > 0 and a - 2*d1 < 0 and a - d1 = 0 and a + d1 - 1 = 0 and 2*a - d1 - 1 <= 0
 or d1 = 0 and d1 < 0 and d1 > 0 and d1 - 1 < 0 and a - 1 = 0 or d1 > 0 and d1 -
 1 <= 0 and a - 1 > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 < 0 and
 a + 2*d1 - 1 >= 0 or d1 - 1 = 0 and a = 0 and a > 0 and a - 2 > 0 and a - 1 = 0
 and 2*a - 1 < 0 or d1 > 0 and d1 - 1 < 0 and a > 0 and a - 1 <= 0 and a - d1 >=
 0 and a + d1 - 1 = 0 and a + 2*d1 - 1 < 0 and 2*a + d1 - 1 > 0 and (a - 1 = 0 
or a - d1 > 0) and (a - 1 = 0 or a - d1 = 0) or d1 - 1 < 0 and 2*d1 - 1 >= 0 and
 a > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 = 0 and a + 3*d1 - 2 <
 0 and 2*a + 3*d1 - 3 > 0 or d1 > 0 and d1 - 1 <= 0 and a - 1 <= 0 and a + d1 - 
1 <= 0 and a + 2*d1 - 1 < 0 and 2*a - 1 >= 0 and (d1 - 1 < 0 or 2*a - 1 > 0) and
 (2*d1 - 1 < 0 or 2*a - 1 > 0) and (a - 1 = 0 or 2*a - 1 = 0) and (a - 1 = 0 or 
a + d1 - 1 = 0) and (d1 - 1 = 0 or a + d1 - 1 = 0) or d1 > 0 and d1 - 1 <= 0 and
 a - 1 <= 0 and a + d1 - 1 <= 0 and a + 2*d1 - 1 < 0 and 2*a - 1 >= 0 and 2*a + 
d1 - 1 > 0 and (d1 - 1 < 0 or 2*a - 1 > 0) and (2*d1 - 1 < 0 or 2*a - 1 > 0) and
 (a - 1 = 0 or 2*a - 1 = 0) and (a - 1 = 0 or a + d1 - 1 = 0) and (d1 - 1 = 0 or
 a + d1 - 1 = 0) or d1 > 0 and d1 - 1 <= 0 and a - 1 <= 0 and a - 2*d1 > 0 and a
 - d1 = 0 and 2*a - 1 >= 0 and 2*a - d1 - 1 < 0 and (d1 - 1 = 0 or 2*a - 1 > 0) 
and (d1 - 1 = 0 or 2*a - 1 = 0) and (d1 - 1 = 0 or a - 1 < 0) or d1 > 0 and a > 
0 and a - 1 <= 0 and a - 2*d1 > 0 and a - d1 >= 0 and a - d1 - 1 <= 0 and (a - 
d1 - 1 = 0 or 2*a - d1 - 1 < 0) and (a - 1 = 0 or 2*a - 1 < 0) and (a - 1 = 0 or
 a - d1 = 0 or 2*a - 1 < 0) and (d1 - 1 = 0 or a - 1 < 0) and (a - d1 = 0 or a -
 d1 - 1 = 0 or 2*a - d1 - 1 < 0) and (2*a - 1 <= 0 or 2*a - d1 - 1 > 0) and (a -
 d1 = 0 or 2*a - d1 - 1 > 0) and (a - 1 = 0 or 2*a - 1 >= 0 and 2*a - d1 - 1 < 0
) and (a - 1 = 0 or a - d1 = 0 and 2*a - 1 >= 0 and 2*a - d1 - 1 < 0 or a - d1 >
 0 and 2*a - d1 - 1 >= 0) or d1 > 0 and d1 - 1 <= 0 and a > 0 and a - 2*d1 > 0 
and a - d1 = 0 and 2*a - 1 < 0 and 2*a - d1 < 0 or d1 > 0 and d1 - 1 <= 0 and a 
> 0 and a - 2*d1 > 0 and a - d1 >= 0 and a - d1 - 1 < 0 and 2*a - 1 < 0 and 2*a 
- d1 < 0 and (d1 - 1 = 0 or a - d1 = 0) or d1 - 1 <= 0 and 2*d1 - 1 > 0 and a > 
0 and a - 1 < 0 and a - 2*d1 > 0 and a - d1 = 0 and a + d1 - 1 = 0$



rltab rp3sol;


(a - 1 > 0 and (

(d1 - 1 > 0 and (a - 2*d1 - 1 > 0 and a - d1 - 1 = 0 and 2*a - 3*d1 - 2 < 0)) or

 (d1 - 1 = 0 and ((a = 0 and a <= 0 and a > 0 and a - 1 >= 0 and a + 1 < 0)

 or (a = 0 and a < 0 and a - 1 = 0 and a + 1 >= 0)

 or (a - 3 > 0 and a - 2 = 0 and 2*a - 5 < 0))) or (d1 - 1 < 0 and (d1 > 0 and (

true and ((2*d1 - 1 < 0 and a - 2*d1 < 0 and a - d1 = 0 and a + d1 - 1 = 0) or (

2*d1 - 1 < 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 < 0

 and a + 2*d1 - 1 >= 0) or (2*d1 - 1 >= 0 and a - d1 = 0 and a + d1 - 1 = 0

 and a + 2*d1 - 2 = 0 and a + 3*d1 - 2 < 0 and 2*a + 3*d1 - 3 > 0) or (

2*d1 - 1 >= 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 = 0

 and 2*a + 3*d1 - 3 < 0)

 or (2*d1 - 1 > 0 and a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 < 0) or (

a - 2 >= 0 and a - 2*d1 - 2 > 0 and a - d1 = 0 and a + d1 - 2 < 0

 and a + 2*d1 - 4 = 0)

 or (a - 2*d1 - 1 > 0 and a - d1 - 1 = 0 and 2*a - 3*d1 - 2 < 0) or (a - d1 = 0

 and a + d1 - 1 = 0 and a + 2*d1 - 2 <= 0 and a + 3*d1 - 2 < 0

 and 2*a + 3*d1 - 3 > 0 and (2*d1 - 1 <= 0 or a + 2*d1 - 2 < 0)) or (a - d1 = 0

 and a + d1 - 1 = 0 and a + 2*d1 - 2 <= 0 and 2*a + 3*d1 - 3 < 0

 and (2*d1 - 1 <= 0 or a + 2*d1 - 2 < 0))

 or (a - d1 = 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 < 0 and a + 2*d1 - 1 >= 0) 

or (a + d1 - 1 = 0 and a + 2*d1 - 2 = 0 and a + 3*d1 - 2 = 0

 and 2*a + 3*d1 - 3 < 0 and 2*a + 3*d1 - 2 > 0))))))) or (a - 1 = 0 and (

(d1 = 0 and d1 < 0 and d1 > 0)

 or (d1 = 0 and d1 < 0 and d1 > 0 and d1 - 1 <= 0 and d1 - 1 < 0)

 or (d1 = 0 and d1 < 0 and d1 > 0 and d1 - 1 <= 0 and d1 - 1 < 0 and d1 + 1 > 0)

 or (d1 = 0 and d1 < 0 and d1 > 0 and d1 - 1 < 0)

 or (d1 = 0 and d1 < 0 and d1 > 0 and d1 - 1 < 0 and d1 + 1 > 0) or (d1 = 0

 and d1 > 0 and d1 - 1 = 0 and d1 - 1 <= 0 and d1 - 1 < 0 and 2*d1 - 1 < 0)

 or (d1 = 0 and d1 > 0 and d1 - 1 = 0 and 2*d1 - 1 < 0 and 2*d1 - 1 > 0)

 or (d1 = 0 and d1 > 0 and d1 - 1 <= 0 and 2*d1 - 1 = 0 and 4*d1 - 1 < 0)

 or (d1 = 0 and d1 > 0 and d1 - 1 < 0 and d1 + 1 < 0 and 2*d1 - 1 <= 0) or (

d1 = 0 and d1 - 1 = 0 and d1 - 1 < 0 and 2*d1 - 1 = 0 and 2*d1 - 1 >= 0

 and 3*d1 - 1 < 0 and 3*d1 - 1 > 0) or (d1 <= 0 and d1 < 0 and d1 >= 0

 and d1 > 0 and d1 - 1 <= 0 and d1 - 1 < 0 and d1 + 1 > 0

 and (d1 = 0 or d1 - 1 = 0)) or (d1 <= 0 and d1 < 0 and d1 >= 0 and d1 > 0

 and d1 - 1 <= 0 and (d1 = 0 or d1 <= 0) and (d1 >= 0 or d1 - 1 = 0)) or (

d1 <= 0 and d1 < 0 and d1 >= 0 and d1 > 0 and d1 - 1 < 0 and d1 + 1 >= 0

 and (d1 = 0 or d1 > 0 or d1 + 1 = 0)) or (d1 <= 0 and d1 < 0 and d1 > 0

 and d1 - 1 <= 0 and d1 + 1 > 0 and (d1 = 0 or d1 - 1 = 0))

 or (d1 <= 0 and d1 < 0 and d1 > 0 and d1 - 1 <= 0 and (d1 = 0 or d1 - 1 = 0)) 

or (d1 <= 0 and d1 < 0 and d1 > 0 and d1 - 1 < 0 and d1 + 1 > 0

 and (d1 <= 0 or d1 >= 0) and (d1 > 0 or (d1 = 0 and d1 <= 0))) or (d1 <= 0

 and d1 > 0 and d1 - 1 <= 0 and d1 - 1 < 0 and d1 + 1 < 0

 and (d1 = 0 or d1 - 1 = 0)) or (d1 <= 0 and d1 - 1 < 0 and d1 - 1 > 0

 and d1 + 1 >= 0 and (d1 + 1 > 0 or 2*d1 + 1 <= 0))

 or (d1 >= 0 and d1 > 0 and d1 - 1 = 0 and d1 - 1 > 0 and 2*d1 - 1 < 0) or (

d1 >= 0 and d1 > 0 and d1 - 1 <= 0 and 3*d1 - 1 < 0 and 3*d1 - 1 > 0

 and (d1 = 0 or d1 - 1 = 0) and (d1 = 0 or d1 - 1 = 0 or 2*d1 - 1 >= 0)

 and (d1 = 0 or d1 - 1 = 0 or (2*d1 - 1 >= 0 and 2*d1 - 1 > 0))

 and (d1 = 0 or 2*d1 - 1 <= 0) and (d1 <= 0 or d1 - 1 < 0)

 and (d1 - 1 = 0 or 2*d1 - 1 <= 0)

 and (d1 - 1 = 0 or 2*d1 - 1 <= 0 or 2*d1 - 1 < 0)

 and (d1 - 1 = 0 or 2*d1 - 1 < 0)

 and (d1 - 1 = 0 or (2*d1 - 1 >= 0 and 2*d1 - 1 > 0))

 and (d1 - 1 < 0 or 2*d1 - 1 <= 0))

 or (d1 > 0 and d1 - 1 = 0 and d1 - 1 > 0 and 2*d1 - 1 < 0))) or (a - 1 < 0 and 

((d1 - 1 > 0 and (a > 0 and a - 2*d1 - 1 > 0 and a - d1 - 2 <= 0

 and a - d1 - 1 > 0 and a + d1 - 1 = 0 and 2*a - d1 - 2 <= 0

 and (a - d1 - 2 = 0 or 2*a - d1 - 2 = 0))) or (d1 - 1 = 0 and ((a = 0 and a > 0

 and a - 3 <= 0 and a - 3 > 0 and a - 2 > 0 and 2*a - 3 <= 0

 and (a - 3 = 0 or 2*a - 3 = 0))

 or (a = 0 and a > 0 and a - 2 > 0 and a - 1 = 0)

 or (a <= 0 and a > 0 and a - 3 > 0 and a - 2 > 0 and 2*a - 3 = 0)

 or (a >= 0 and a > 0 and a - 2 > 0 and a - 1 = 0)

 or (a > 0 and a - 2 < 0 and a - 2 > 0 and a - 1 >= 0 and 2*a - 1 < 0)

 or (a > 0 and a - 2 > 0 and a - 1 = 0 and 2*a - 1 < 0)

 or (a - 2 > 0 and a - 1 = 0 and a - 1 < 0 and 2*a - 1 >= 0))) or (d1 - 1 < 0 

and (a > 0 and (d1 > 0 and ((a - d1 > 0 and (a + d1 - 1 = 0 and (a - d1 - 1 > 0 

and (a - 2*d1 - 1 > 0

 and (2*a - d1 - 2 = 0 or (a - d1 - 2 = 0 and 2*a - d1 - 2 < 0)))))) or (

a - d1 = 0 and ((2*d1 - 1 < 0 and a - 2*d1 > 0 and a + d1 - 1 = 0)

 or (2*d1 - 1 < 0 and a + d1 - 1 = 0 and a + 2*d1 - 2 > 0) or (2*d1 - 1 >= 0

 and a + d1 - 1 = 0 and a + 2*d1 - 2 = 0 and a + 3*d1 - 2 < 0

 and 2*a + 3*d1 - 3 > 0) or (2*d1 - 1 > 0 and a - 2*d1 > 0 and a + d1 - 1 = 0)

 or (a - 3*d1 > 0 and a - 2*d1 - 1 >= 0 and a + d1 - 2 = 0)

 or (a - 3*d1 > 0 and a + d1 - 2 >= 0 and a + 3*d1 - 2 = 0)

 or (a - 2*d1 > 0 and 2*a - 1 < 0 and 2*a - d1 < 0) or (a + d1 - 1 = 0

 and a + 2*d1 - 2 = 0 and a + 3*d1 - 2 < 0 and 2*a + 3*d1 - 3 > 0) or (

a + d1 - 1 = 0 and a + 2*d1 - 2 <= 0 and a + 3*d1 - 2 < 0 and 2*a + 3*d1 - 3 > 0

 and (2*d1 - 1 <= 0 or a + 2*d1 - 2 < 0) and (2*d1 - 1 > 0 or a + 2*d1 - 2 = 0))

 or (a + d1 - 1 = 0 and a + 2*d1 - 2 <= 0 and a + 3*d1 - 2 < 0

 and 2*a + 3*d1 - 3 > 0 and (a + 2*d1 - 2 = 0 or 2*a + d1 - 2 >= 0))))))))))


end;

