c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.001999 s c decisions : 23 (11506 /sec)