c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.015997 s c decisions : 1118 (69888 /sec)