c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.004999 s c decisions : 267 (53411 /sec)