c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.009998 s c decisions : 468 (46809 /sec)