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$



rlgsn rp3sol;


false


end;

