c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.008998 s c decisions : 504 (56012 /sec)