I've got the Lisp code for ordered unions of disjoint intervals working pretty reliably.
The inference capability is reasonable:
Given (if zerop(x-3) then 9 else 10) = 9, the system can deduce that x=3.
Also, (if plusp(x) then x*x else x*x) >=0 is always true (for real x).
Similarly, (if plusp(x) then x else -x) >=0 is always true (for real x).
I found that _half-intervals_, e.g., x<3 or x<=3 are interesting & useful in their own right, and not just as
the lower or upper bound of a full interval 0<x<=3.
Things to be done: rational approximations to real intervals: e.g., how to represent intervals like [-pi..pi), when pi itself is approximated by an interval with rational endpoints, which approximation might want to be automagically improved when necessary -- e.g., when comparing "pi)" with a half-interval like "22/7)".