If we assume that all $A,B,C,D$ are real, we can use cylindrical algebraic decomposition (CAD) to simplify such an expression (in general, CAD can handle logical formulas involving polynomial (in)equalities). Sage has an interface to QEPCAD (QEPCAD itself, however, I believe is not shipped with sage, so has to be installed) which is one of the most popular implementations of CAD. Here is how QEPCAD simplifies your expression:

```
sage: from sage.interfaces.qepcad import qepcad_formula, qepcad, qformula
sage: var("A,B,C,D")
sage: qf = qepcad_formula
sage: expr = qf.or_([qf.and_([A<=B, B<=C]), qf.and_([A<=D, D<=C]), qf.and_([B<=A, A<=D, D<=C]), qf.and_([D>=C, A<=B, B<=C]), qf.and_([B<=A, D>=C])])
sage: qepcad(expr)
[ B - A >= 0 /\ C - B >= 0 ] \/ [ D - A >= 0 /\ D - C <= 0 ] \/ [ B - A <= 0 /\ D - C >= 0 ]
```

to try to answer, I tried the code below (which must surely not be correct) but the kernel never stops !

From the manual :

"Formulas consist of the following operators:

& – and

| – or

~ – not

^ – xor

-> – if-then

<-> – if and only if

Operators can be applied to variables that consist of a leading letter and trailing underscores and alphanumerics. Parentheses may be used to explicitly show order of operation."

Your code uses symbols not in the above list ; no wonder that it can't compile...

More important : "A>=B" is a predicative assertion, not a proposition. First-order predicate logic is a horse of another color...