char cplex_version[] = "\nAMPL/CPLEX(20000909)\n";