c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.153976 s c decisions : 12202 (79246 /sec)