c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.162975 s c decisions : 12409 (76141 /sec)