c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 11.8482 s
c decisions             : 375061         (31656 /sec)