c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 2.0027 s
c decisions             : 174159         (86962 /sec)