c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.176973 s c decisions : 19486 (110107 /sec)