c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 42.7515 s
c decisions             : 1195873        (27973 /sec)