c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.002999 s c decisions : 53 (17673 /sec)