c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.05999 s
c decisions             : 6033           (100567 /sec)