c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.013997 s c decisions : 779 (55655 /sec)