c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 49.0395 s
c decisions             : 1333960        (27202 /sec)