c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.005999 s c decisions : 183 (30505 /sec)