c UNSATISFIABLE s UNSATISFIABLE c CPU time : 0.035994 s c decisions : 3649 (101378 /sec)