inequality solver now only splits on disequalities when complete
fixed  model generation bug; commented out attempt at inequality propagation