c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.35364 s
c decisions             : 126884         (53910 /sec)