c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.006998 s c decisions : 225 (32152 /sec)