c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 48.7976 s
c decisions             : 1334911        (27356 /sec)