Warning: regression in unary maximum. Agressive pruning with case splitting. Minor numerical optimizations: sets for solved form of inequalities sides; pruning redundant ineqn candidates (when differ by constant from stronger ones).