c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.009998 s c decisions : 647 (64713 /sec)