c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.285956 s
c decisions             : 20324          (71074 /sec)