corrected a bug in dimacs solution verification
A NO-PUSH version, unsat detected via subsumption only
An OLDPUSH version, standard clause propagation (pushing) after each iteration (phase)