Earlier quoted context omitted.
I don't know much about this area. What about "x ∈ ℕ ∧ x > 2 ∧ x < 5 ∧ x % 2 = 0 implies x = 4." can't be expressed in common languages? Don't lots of solver systems have support for sets, and deriving facts from statements about them?
Just in case somebody might benefit from finding out how easy it is in python with z3 >>> from z3 import Int, solve >>> x = Int('x') >>> solve([x > 2, x
If anything, this seems to support the original claim.