c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.004999 s c decisions : 269 (53811 /sec)