c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.005999 s c decisions : 161 (26838 /sec)