I will assume your variables can take on arbitrarily real numbers. Build a weighted directed graph that represents all known inequalities, with one vertex per element (i.e., $n+m$ vertices in total). In particular, apply 'eq' and 'lt' to all ${n+m \choose 2}$ pairs of elements. Then:
If $x < y$ (i.e., $\textsf{lt}(x,y)$ returns true), where $x,y$ are two elements, add a directed edge $x \to y$ with length $-1$.
If $x \le y$ (i.e., $\textsf{lt}(y,x)$ returns false), add a directed edge $x \to y$ with length 0.
If $x=y$ (i.e., $\textsf{eq}(x,y)$ returns true), then add directed edges $x \to y$ and $y \to x$ with length 0.
If $x\ne y$ (i.e., $\textsf{eq}(x,y)$ returns false), do nothing and add no edges.
Let $d(x,y)$ be the length of the shortest path from $x$ to $y$ in this graph. If $d(x,y)=c$, then we will be guaranteed that $x \le y + c$, and this is the optimal $c$ for which this is true (i.e., it is the smallest $c$ for which this is true).
Compute a new bipartite graph $G$ with an edge $a_i\to b_j$ of length $d(a_i,b_j)$ for each $a_i,b_j$. This can be computed with the Floyd-Warshall algorithm, for example.
Find the minimum-weight perfect matching in this bipartite graph. This is an instance of the assignment problem, and hence can be solved in polynomial time with standard algorithms. If the total weight of the matching is $w$, then we can conclude that
$$a_1+\dots+a_n \le b_1+\dots+b_m + w.$$
Consequently, if $w \le 0$, then we can conclude that $a_1+\dots+a_n \le b_1+\dots+b_m$ and we can return "true" to the original question.
Solve another assignment problem for the bipartite graph with edges $b_j \to a_i$ of length $d(a_i,b_j)$ for each $a_i,b_j$. In this way, we obtain $w'$ such that
$$b_1+\dots+b_m \le a_1+\dots+a_n + w'.$$
If $w' \le 0$, return "false" to the original question.
Otherwise, return "unknown".
This takes $O(nm)$ calls to the binary operations and $O((nm)^{2.5} \log n)$ running time.
This works for this very specific problem. A more general approach is to use linear programming: if you want to check whether $(I_1 \land \cdots \land I_k) \implies J$, where the $I$'s and $J$ are linear inequalities, then check whether the system of inequalities $I_1 \land \cdots \land I_k \land \neg J$ is satisfiable using linear programming. This will let you support more general mathematical expressions and more general relationships between the variables, as long as they are all linear functions/inequalities of the variables. In your problem, after you call 'lt' and 'eq' on all pairs of elements, each operation that returns something other than "unknown" gives you an inequality or equality $I_i$ on two variables. Here $J$ is the inequality $a_1+\dots+a_n \le b_1+\dots+b_m$. So, you could apply linear programming directly to your problem. This approach also supports more general operations, as long as they are all linear.
My answer above essentially solved the linear programming problem for the special case where $I_1,\dots,I_k$ are all inequalities with a difference of two variables, and $J$ has the form $a_1+\dots+a_n \le b_1+\dots+b_m$. I used a standard data structure for representing differences of two variables (the graph), and then combined it with an algorithm for the assignment problem to capture the one additional inequality with multiple variables.
